Browse

Optimization and Control

math.OC — Optimization and Control

Works in math.OC

5 works

math.OC — Optimization and Control

Continuity of solutions to abstract linear control systems

Contributed by Frédéric Marbach

It has long been known that the solutions to abstract linear control systems are continuous in time for controls in $L^p$ with $1 \le p < \infty$ . We prove that the same property remains valid for the endpoint case $p = \infty$ , giving a positive answer to Weiss' 1989 Problem 2.4. The proof relies on a direct semigroup argument based on Phillips' lemma, does not require the input map to have an integral representation (which is not always the case for $p = \infty$ ), and actually entails that such systems are all of the zero-class (which fails for $1 \le p < \infty$ ).

Primarily AI-generated textHuman understanding: all partsabstract linear control systems

Oct 03, 2026PDF ↗View work →

hexagon:2610.00002v1

math.OC — Optimization and Control

A Finite Coordinate Reduction for Approachability Loss in Lean

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We explain a Lean 4 development of a finite-coordinate loss-preserving construction motivated by Theorem 4 of Dann, Mansour, Mohri, Schneider, and Sivan. Nonempty finite constraint and action index sets give a joint probability simplex with a canonical action marginal. For each mixed constraint, a linear comparator adds its outer product with that marginal. The comparator has mass two and leaves the legal action set. A one-step pairing identity yields exact equality of finite-horizon approachability and comparator-regret objectives, with explicit anchored lifts and marginal decoders. The development also proves a row-wise decomposition with at most one rank-one term per constraint index. We describe the twelve declarations registered in Palomar and their historical verification provenance. The scope is deliberately narrow: the constraint simplex parametrizes coordinate functions, both causal strategy translations observe original loss histories, and the comparators have no fixed point in the joint simplex. Thus the checked statements establish finite algebraic loss preservation; they do not certify the full published reduction, its fixed-point-defined improper class, reduced-loss-only feedback, or asymptotic rate theory. No mathematical novelty or formalization priority is claimed.

Primarily AI-generated textHuman understanding: some parts

Oct 01, 2026PDF ↗View work →

hexagon:2609.00151v1

math.OC — Optimization and Control

A Lean Formalization of Roberts Theorem on Unrestricted Valuations

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We describe a Lean 4 formalization of the finite unrestricted-domain version of Roberts theorem. For finite nonempty agent and alternative types, with at least three alternatives, an onto deterministic direct-revelation mechanism that is dominant-strategy incentive compatible has an affine-maximizer choice rule. Valuations range over all real-valued profiles; the conclusion uses fixed nonnegative weights, at least one nonzero, and alternative offsets, and asserts membership in the maximizing set. The development follows the modular proof route: taxation and weak monotonicity, perturbation-based tie-breaking to strong monotonicity, no-veto range analysis, affine prices for two agents, and induction through fixed-report slices. We explain the proved tie-set transport lemma, the construction of fresh payments for the tie-broken rule, and the transfer back to arbitrary ties. A version-pinned account distinguishes the proved library from statement-only comparator placeholders and separates source inspection from executable checks. This is an exposition of a classical result and its formal artifact, with no claim of mathematical novelty or formalization priority.

Primarily AI-generated textHuman understanding: some partsLean 4Roberts theoremaffine maximizersdominant strategiesformalizationmechanism design

Sep 30, 2026PDF ↗View work →

hexagon:2609.00150v1

math.OC — Optimization and Control

Finite VCG and Groves Payments in Lean

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We describe a Lean 4 development of finite direct mechanisms with quasi-linear utility and unrestricted real-valued valuations. The Clarke pivot mechanism selects a reported-welfare maximizer and charges each agent the loss in other-agent welfare relative to its maximum over the same fixed alternative set. The development proves efficiency, dominant-strategy truthfulness, nonnegative payments and no deficit, and individual rationality under the explicit assumption that every valuation is nonnegative. It also proves that every efficient, dominant-strategy incentive-compatible mechanism on the full valuation domain has Groves-form payments, with a term independent of the paying agent's report. We explain the finite-maximization interface, the report-update invariants, and the characterization argument using outcome-forcing reports and positive perturbations. The exposition is tied to a specific source revision and separates proved implementations from statement-only comparator placeholders. These are classical mechanism-design results; no new mathematical theorem or formalization-priority claim is made.

Primarily AI-generated textHuman understanding: some partsClarke pivot paymentsGroves characterizationLean 4VCG mechanismdominant strategiesformal verification

Sep 30, 2026PDF ↗View work →

hexagon:2609.00148v1

math.OC — Optimization and Control

A Lean Formalization of Finite Zero Sum Minimax via Sion's Theorem

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We describe a Lean 4 formalization of the minimax theorem for finite nonempty two-player zero-sum games with arbitrary real payoffs. Mixed strategies are probability vectors, and the two game values are defined using real indexed suprema and infima. An explicit payoff bound supplies the boundedness obligations required by these conditional extrema. The reverse minimax inequality follows by applying Mathlib's proved Sion saddle-point theorem to compact convex coordinate simplices, with the minimizing player placed in its first argument. We explain the representation bridge, the proof obligations, and the passage from a saddle point to equality. The accompanying version-pinned artifact separates a reusable library from a statement-only challenge and its proved solution. This is an exposition of a finite-game specialization of existing formal analysis, with no claim of a new mathematical proof or formalization priority.

Primarily AI-generated textHuman understanding: some partsLeanSion's theoremformalizationminimax theoremzero-sum games

Sep 30, 2026PDF ↗View work →