Operations Research

Completed

Algorithmic Game Theory·Captain: mikedeng1

Theory of Games and Economic Behavior IV: The Characteristic Function of a Zero-Sum n-Person GameTextbook

Motivation

Chapter VI of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; 3rd ed. 1953) opens the general theory of zero-sum games with more than two players. The authors propose to describe everything that can be said about coalitions, compensations between partners and fights between coalitions through one numerical object, the characteristic function $v(S)$ : the amount a group of players $S$ can secure for itself against all the others (25.2.1). The whole later theory of the book (imputations, domination, solutions, simple games, decomposition) is built on this set function, and the same object, under the name "coalitional game" or "TU game", is the starting point of cooperative game theory as a field (cores, Shapley value, nucleolus).

§§25–27 settle two foundational questions about it. First, which set functions arise as characteristic functions of actual games? Second, which characteristic functions describe the same strategic situation, and how is a canonical representative chosen? The answers (a complete characterization by three conditions, and the reduced form under strategic equivalence) are what later chapters, and much of the cooperative literature, use when they take "a characteristic function" as a primitive without reference to any game.

Setting

A zero-sum $n$ -person game in normalized form $\Gamma$ (11.2.3, 25.1.3) has players $k = 1, \dots, n$ . Player $k$ chooses a pure strategy $\tau_k \in \{1, \dots, \beta_k\}$ , $\beta_k \geqq 1$ , uninformed about the others' choices, and then receives the real amount $\mathcal H_k(\tau_1, \dots, \tau_n)$ , subject to (25:1)

\sum_{k=1}^n \mathcal H_k(\tau_1, \dots, \tau_n) \equiv 0 .

Let $I = \{1, \dots, n\}$ and, for $S \subseteq I$ , $-S = I \setminus S$ . The book defines $v(S)$ in 25.1.3 through a fictitious two-person game: all players of $S$ form one composite player $1'$ , all players of $-S$ another, $2'$ . The pure strategies of $1'$ are the aggregates $\tau^S$ (one choice $\tau_k$ for each $k \in S$ ), those of $2'$ are the aggregates $\tau^{-S}$ , and $1'$ receives (25:2)

\overline{\mathcal H}(\tau^S, \tau^{-S}) = \sum_{k \in S} \mathcal H_k(\tau_1, \dots, \tau_n).

A mixed strategy of $1'$ is a probability vector $\xi$ on the set of all aggregates $\tau^S$ , and one of $2'$ is a probability vector $\eta$ on the aggregates $\tau^{-S}$ . With $K(\xi, \eta) = \sum_{\tau^S, \tau^{-S}} \overline{\mathcal H}(\tau^S, \tau^{-S})\, \xi_{\tau^S} \eta_{\tau^{-S}}$ ,

v(S) = \operatorname{Max}_\xi \operatorname{Min}_\eta K(\xi, \eta) = \operatorname{Min}_\eta \operatorname{Max}_\xi K(\xi, \eta).

The coalition therefore randomizes jointly: $\xi$ is one distribution over its members' strategy tuples, not a product of independent mixtures. The empty set and $I$ are coalitions too (footnote 2, p. 241).

The three conditions of 25.3.1 on a set function $v$ are

\text{(25:3:a)}\ v(\ominus) = 0, \qquad \text{(25:3:b)}\ v(-S) = -v(S), \qquad \text{(25:3:c)}\ v(S \cup T) \geqq v(S) + v(T) \ \text{ if } S \cap T = \ominus .

From 26.2 on, every set function satisfying them is called a characteristic function.

Two such functions are strategically equivalent (27.1) if $v'(S) = v(S) + \sum_{k \in S} \alpha^0_k$ for numbers $\alpha^0_k$ with $\sum_k \alpha^0_k = 0$ ((27:1), (27:2)). A function is reduced if all one-element coalitions have the same value, (27:3); with that common value written $-\gamma$ , (27:5). A game is inessential if the reduced form of its characteristic function is $\equiv 0$ , and essential otherwise (27.3).

Formalization targets

Goal: the characterization of characteristic functions (26.2)

v \text{ satisfies (25:3:a)–(25:3:c)} \iff \exists\, \Gamma \text{ zero-sum } n\text{-person game with } v_\Gamma = v .

The "only if" half is 25.3.1; the "if" half is 26.1.1, which requires a single game $\Gamma$ realizing $v$ on every coalition simultaneously.

Milestones

25.3.1: every $v_\Gamma$ satisfies (25:3:a)–(25:3:c).
(25:A): the three conditions are equivalent to $v(S_1) + \dots + v(S_p) \leqq 0$ on decompositions of $I$ for $p = 1, 2, 3$ , with equality for $p = 1, 2$ .
26.1.1: every $v$ satisfying (25:3:a)–(25:3:c) is $v_\Gamma$ for some game $\Gamma$ .
(27:A): every characteristic function is strategically equivalent to exactly one reduced characteristic function, given by (27:2), (27:4).
(27:7): for reduced $\bar v$ and every $p$ -element $S$ , $-p\gamma \leqq \bar v(S) \leqq (n-p)\gamma$ , with equality in the stated boundary cases.
(27:B): inessential iff $\sum_j v((j)) = 0$ ; essential iff $\sum_j v((j)) < 0$ .
(27:C) and (27:D): inessential iff $v$ is additive, $v(S) \equiv \sum_{k \in S} \alpha^0_k$ , equivalently iff (25:3:c) always holds with equality.

Significance

The characterization makes the three conditions (25:3:a)–(25:3:c) the complete axiomatics of zero-sum characteristic functions. Every later result in the book that is stated "for a characteristic function" (the solutions of the three-person game in §32, the simple games of Chapter X, the decomposition theory of Chapter IX) is thereby a result about zero-sum games, and conversely no further constraint on $v$ is hidden in the game model. The reduced form of §27 cuts the parameter space of characteristic functions by $n$ and turns essentiality into a sign condition, which is used throughout the rest of the book.

These results are proved in the book. As far as a search of the Prove2Me catalog shows (queries on characteristic function, coalition, strategic equivalence, inessential, superadditive), none of them is formalized there; the existing cooperative-game definitions on the platform use other normalizations ( $v(\emptyset) = 0$ only, no complementarity condition) and are not this object. The mission produces a machine-checked link between the non-cooperative model of an $n$ -person game and the cooperative set function, including the book's explicit game construction behind 26.1.1.

Difficulty

The "only if" direction requires comparing values of different two-person games: (25:3:c) asks that the coalition $S \cup T$ can guarantee as much as $S$ and $T$ separately, which rests on the coalition mixing jointly, and (25:3:b) needs the minimax theorem, since $v(-S)$ is a Max-Min for the opposite side. The "if" direction is an existence claim: from an abstract $v$ one must produce one finite game whose characteristic function matches $v$ on all $2^n$ coalitions at once. Producing, for each $S$ separately, a game with the right value $v_\Gamma(S)$ is easy and proves nothing. The §27 results are finite linear algebra over set functions, but the uniqueness in (27:A) and the boundary equalities in (27:7) depend on using all three conditions.

Formalization scope

Players are Fin n (the book's $1, \dots, n$ are $0, \dots, n-1$ ), coalitions are Finset (Fin n), $-S$ is the complement Sᶜ, and set functions are Finset (Fin n) → ℝ. A game is a structure ZeroSumGame n with strategy sets Fin (β k), a field β k > 0 (finitely many and at least one pure strategy per player), real payoffs H τ k, and the zero-sum condition (25:1) as a field. An aggregate $\tau^S$ is a dependent function on the members of $S$ ; mixed strategies are elements of Mathlib's stdSimplex, and the coalition's $\xi$ is a single distribution on aggregates, as in 25.1.3. The Max and Min in $v(S)$ are written as ⨆/⨅ over the simplices; these are nonempty and the bilinear form is bounded on them, so no junk value arises. No lower bound on $n$ is imposed: the book's statements remain true for $n = 0$ and $n = 1$ , so dropping the implicit $n \geqq 1$ is a harmless strengthening.

Standing hypotheses instantiated in the statements: finiteness of the strategy sets and (25:1) (25.1.3) are part of ZeroSumGame; the §27 results carry (25:3:a)–(25:3:c) as a hypothesis, the book's standing assumption from 26.2 on ("characteristic function"); (27:7) carries reducedness (27:3) and the definition (27:5) of $\gamma$ ; strategic equivalence includes (27:1). The reduced form is the explicit function of (27:2), (27:4), with $\frac1n$ as a real division that only matters for $n \geqq 1$ .

A trivializing reading of the goal, "for every $S$ there is a game with $v_\Gamma(S) = v(S)$ ", is excluded: the statement asks for one game $\Gamma$ with $v_\Gamma = v$ as functions. The coalition value is not the value under independent mixtures of the members, which is smaller in general and for which (25:3:c) can fail.

A complete development needs the minimax theorem for finite matrix games (the platform's AGT.zero_sum_minimax covers it for matrices indexed by Fin (m+1), and can be transported to the aggregate types), bookkeeping for splitting and joining strategy profiles along $S$ and $-S$ , and the construction of 26.1 with its zero-sum check. The profile-splitting lemmas and the value facts for coalition games are reusable for the book's Chapter XI (general games) and for any work on coalitional values of strategic games. Contributions welcome: the §27 milestones, which are self-contained, and the two directions of the goal.

Selected references

J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd edition, 1953), §§25–27, pp. 238–254. https://doi.org/10.1515/9781400829460
J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320 (the minimax theorem used for $v(S)$ ). https://doi.org/10.1007/BF01448847
M. Maschler, E. Solan and S. Zamir, Game Theory, Cambridge University Press, 2013, Ch. 16 (coalitional games with transferable utility). https://doi.org/10.1017/CBO9780511794216

13 thms4 active usersReviewed

Completed

Algorithmic Game Theory Convex Optimization Linear Optimization·Captain: mikedeng1

Theory of Games and Economic Behavior III: Mixed Strategies, the Minimax Theorem and Good StrategiesTextbook

Motivation

A zero-sum two-person game in normalized form is a real matrix $\mathcal H(\tau_1, \tau_2)$ : player 1 chooses a row $\tau_1$ , player 2 simultaneously chooses a column $\tau_2$ , and player 2 pays player 1 the amount $\mathcal H(\tau_1, \tau_2)$ . Matrix games are the base case of non-cooperative game theory, the prototype of every minimax statement in optimization, statistics (Wald's decision theory) and online learning, and, through their equivalence with linear programming, a standard tool of operations research.

Chapter III of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; third edition 1953) gives the book's complete solution of these games. Timeline:

1928. J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Math. Annalen 100, proves that every matrix game has a value in mixed strategies (the minimax theorem), by a topological argument. https://doi.org/10.1007/BF01448847
1937. von Neumann's growth-model paper gives a second proof via a fixed-point argument, later generalized by Kakutani (1941).
1938. J. Ville gives the first elementary proof, based on convexity.
1944. The Theory of Games presents Ville's route: a theorem of the alternative for matrices (§16) yields the minimax theorem (17:6), from which §17 derives the structure of the sets of good strategies.
1951. Gale, Kuhn and Tucker, and Dantzig, relate matrix games to linear-programming duality.

Setting

Player 1 has $\beta_1 \ge 1$ pure strategies $\tau_1$ , player 2 has $\beta_2 \ge 1$ pure strategies $\tau_2$ , and $\mathcal H$ is an arbitrary real $\beta_1 \times \beta_2$ matrix (14.1.1). A mixed strategy of player 1 is a probability vector $\xi$ in the simplex

S_{\beta_1} = \Big\{ \xi \in \mathbb R^{\beta_1} : \xi_{\tau_1} \ge 0,\ \sum_{\tau_1} \xi_{\tau_1} = 1 \Big\},

and similarly $\eta \in S_{\beta_2}$ for player 2. The pure strategy $\tau$ is the coordinate vector $\delta^{\tau}$ . The expected payoff is the bilinear form (17:2)

K(\xi, \eta) = \sum_{\tau_1=1}^{\beta_1} \sum_{\tau_2=1}^{\beta_2} \mathcal H(\tau_1, \tau_2)\, \xi_{\tau_1} \eta_{\tau_2}.

The good strategies of player 1 form the set $\bar A$ of those $\xi \in S_{\beta_1}$ at which $\operatorname{Min}_\eta K(\xi, \eta)$ assumes its maximum; those of player 2 form the set $\bar B$ of those $\eta \in S_{\beta_2}$ at which $\operatorname{Max}_\xi K(\xi, \eta)$ assumes its minimum ((17:B:a), (17:B:b)). A saddle point of $K$ is a pair with $K(\xi', \eta) \le K(\xi, \eta) \le K(\xi, \eta')$ for all $\xi', \eta'$ . With pure strategies alone one has $v_1 = \operatorname{Max}_{\tau_1}\operatorname{Min}_{\tau_2}\mathcal H$ and $v_2 = \operatorname{Min}_{\tau_2}\operatorname{Max}_{\tau_1}\mathcal H$ ; the game is specially strictly determined when $v_1 = v_2$ .

For a general real function $\phi(x, y)$ (§13) the same notions are $\operatorname{Max}_x \operatorname{Min}_y \phi$ , $\operatorname{Min}_y \operatorname{Max}_x \phi$ , saddle points, and the sets $A^\phi$ (maximizers of $\operatorname{Min}_y \phi$ ) and $B^\phi$ (minimizers of $\operatorname{Max}_x \phi$ ), always under the book's standing hypothesis that these maxima and minima exist.

Formalization targets

Goal: (17:D), good strategies characterized by their supports

For all $\xi \in S_{\beta_1}$ and $\eta \in S_{\beta_2}$ : $\xi \in \bar A$ and $\eta \in \bar B$ if and only if

\xi_{\tau_1} = 0 \text{ whenever } \sum_{\tau_2} \mathcal H(\tau_1, \tau_2)\eta_{\tau_2} < \max_{\tau_1'} \sum_{\tau_2} \mathcal H(\tau_1', \tau_2)\eta_{\tau_2},

\eta_{\tau_2} = 0 \text{ whenever } \sum_{\tau_1} \mathcal H(\tau_1, \tau_2)\xi_{\tau_1} > \min_{\tau_2'} \sum_{\tau_1} \mathcal H(\tau_1, \tau_2')\xi_{\tau_1}.

The statement fixes no value and no constant; it says which pairs of mixed strategies are optimal.

Milestones, in attack order

(13:A*) $\operatorname{Max}_x \operatorname{Min}_y \phi \le \operatorname{Min}_y \operatorname{Max}_x \phi$ .
(13:D*) If $\operatorname{Max}\operatorname{Min} = \operatorname{Min}\operatorname{Max}$ , the saddle points of $\phi$ are exactly $A^\phi \times B^\phi$ .
(17:A) $\operatorname{Min}_\eta K(\xi, \eta) = \operatorname{Min}_{\tau_2} \sum_{\tau_1} \mathcal H(\tau_1, \tau_2)\xi_{\tau_1}$ , and dually for $\operatorname{Max}_\xi$ .
(16:C) For every matrix $a(i, j)$ exactly one of: some $x \in S_m$ with $\sum_j a(i,j)x_j \le 0$ for all $i$ ; some $w \in S_n$ with $\sum_i a(i,j)w_i > 0$ for all $j$ .
(16:F) The weak form with $\ge 0$ in place of $> 0$ .
(17:6) The minimax theorem: a saddle point of $K$ exists (already on the platform as AGT.zero_sum_minimax, proved).
(17:C:f) $\xi \in \bar A$ and $\eta \in \bar B$ iff $\xi, \eta$ is a saddle point of $K$ .

After the goal: (17:E) the game is specially strictly determined iff each player has a pure good strategy.

Significance

(17:D) is the complementary-slackness description of the optimal strategy pairs of a matrix game: a good strategy puts weight only on pure strategies that are best replies to the opponent's good strategy, and conversely any pair of mutually supported best replies is optimal. It is the basis of support-enumeration methods for matrix games, of the equalizing arguments used to solve small games by hand (the book's Chapter IV applies it to Matching Pennies, Stone–Paper–Scissors and Poker), and of the rectangular structure $\bar A \times \bar B$ of the set of optimal pairs. (17:E) connects the mixed-strategy solution to the pure-strategy theory of §14 and to the perfect-information games of §15.

The results are classical and proved in the book. The minimax theorem itself is already machine-checked on the platform (AGT.zero_sum_minimax), and Mathlib contains Sion's minimax theorem and the basic saddle-point lemmas for extended-real functions on sets. This mission adds the book's own chain: the §13 saddle-point calculus under its standing attainment hypothesis, the theorems of the alternative (16:C) and (16:F) in the simplex-normalized form the book uses, the reduction (17:A) to pure strategies, and the characterizations (17:C:f), (17:D), (17:E) of good strategies, which are not on the platform in any form.

Difficulty

The "if" direction of (17:D) cannot be proved from the support conditions alone by local reasoning: that a pair of mutual best replies consists of good strategies uses that the value $\operatorname{Max}_\xi \operatorname{Min}_\eta K$ equals $\operatorname{Min}_\eta \operatorname{Max}_\xi K$ , i.e. the minimax theorem. Without that equality the "if" direction of (13:D*) fails (points of $A^\phi \times B^\phi$ exist but are not saddle points), so the calculus of §13 alone does not suffice. Likewise (16:C) is not a direct instance of the Farkas lemma forms on the platform: its alternatives are normalized to the simplex and the second one is strict, and both the existence and the mutual exclusion must be shown.

Formalization scope

Lean conventions, fixed throughout:

Pure strategies are Fin β₁, Fin β₂ (numbered from $0$ ), the matrix is H : Fin β₁ → Fin β₂ → ℝ, and $S_\beta$ is Mathlib's stdSimplex ℝ (Fin β).
Nonempty strategy sets ( $\beta \ge 1$ , from "τ = 1, …, β" in 14.1.1): every theorem assumes 0 < β₁, 0 < β₂, or mixed strategies $\xi \in S_{\beta_1}$ , $\eta \in S_{\beta_2}$ , which force it. The theorems of the alternative assume $n, m \ge 1$ (a matrix with rows and columns).
Standing hypothesis of 13.2.1 ("we are restricting our considerations to such functions, for which Max and Min exist"): the §13 results (13:A*), (13:D*) are stated for an arbitrary $\phi : X \times Y \to \mathbb R$ under the predicate MaxMinAttained φ, which says that $\operatorname{Min}_y \phi(x, y)$ , $\operatorname{Max}_x \phi(x, y)$ , $\operatorname{Max}_x \operatorname{Min}_y \phi$ and $\operatorname{Min}_y \operatorname{Max}_x \phi$ are attained. (13:D*) also carries the hypothesis of 13.5.2 that saddle points exist, stated as $\operatorname{Max}_x \operatorname{Min}_y \phi = \operatorname{Min}_y \operatorname{Max}_x \phi$ .
$\operatorname{Max}$ and $\operatorname{Min}$ are the real ⨆, ⨅; they are the book's attained values under the hypotheses above (compactness of the simplex and continuity of $K$ for the mixed game). (17:A) asserts attainment explicitly (IsLeast, IsGreatest). "Does not assume its maximum at $\tau_1$ " in the goal is written without any Max operator.
$\bar A$ , $\bar B$ are defined as maximizers and minimizers directly from $K$ , not through an assumed value $v'$ .

A trivializing formalization is ruled out: $\bar A$ and $\bar B$ are not taken as hypotheses or defined through the support conditions, strategy sets cannot be empty, and no Max over an empty or unbounded set occurs.

Contributions welcome: proofs of the milestones, especially (16:C) (from Mathlib's convex separation or from a platform Farkas lemma) and the bridge from AGT.zero_sum_minimax to (17:C:f). The §13 lemmas and the (17:A) reduction are reusable by any mission about matrix games or bilinear saddle points.

Selected references

J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd edition, 1953), §§13, 16, 17. https://doi.org/10.1515/9781400829460
J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320. https://doi.org/10.1007/BF01448847
J. Ville, "Sur la théorie générale des jeux où intervient l'habileté des joueurs", in É. Borel, Traité du calcul des probabilités et de ses applications, IV.2, Gauthier-Villars, 1938, 105–113.
S. Kakutani, "A generalization of Brouwer's fixed point theorem", Duke Mathematical Journal 8 (1941), 457–459. https://doi.org/10.1215/S0012-7094-41-00838-4
D. Gale, H. W. Kuhn and A. W. Tucker, "Linear programming and the theory of games", in Activity Analysis of Production and Allocation, Wiley, 1951, 317–329.

11 thms4 active usersReviewed

Completed

Algorithmic Game Theory·Captain: mikedeng1

Theory of Games and Economic Behavior I: Numerical Utility from the Axioms of Preference and MixtureTextbook

Motivation

Game theory as von Neumann and Morgenstern built it measures every outcome by a single number, the utility a player attaches to it, and combines those numbers linearly when an outcome is uncertain: a lottery that yields $u$ with probability $\alpha$ and $v$ with probability $1-\alpha$ is worth $\alpha\,\mathrm v(u) + (1-\alpha)\,\mathrm v(v)$ . Every later chapter of Theory of Games and Economic Behavior uses this without comment, from the value of a zero-sum game to the characteristic function of a coalition. Section 3 of the book justifies it: it states axioms on preferences and on the combination of alternatives with probabilities, and claims that they force utility to be a number, unique up to the choice of a zero and a unit. The proof, announced in 3.6.1 as "somewhat lengthy", was added as the Appendix The Axiomatic Treatment of Utility in the second edition (1947).

The result, the expected utility theorem, is the foundation of decision theory under risk and of expected-payoff reasoning in game theory, statistics and operations research. The axiomatics were later recast by Marschak (1950), Herstein and Milnor (1953) in the language of mixture spaces (Herstein–Milnor). This mission formalizes the original statement and its original proof structure.

Setting

A system of utilities (3.6.1) is an abstract set $U$ of entities $u, v, w, \dots$ , together with

a relation $u > v$ (" $u$ is preferable to $v$ "); write $u < v$ for $v > u$ ;
for every number $\alpha$ with $0 < \alpha < 1$ , an operation producing an element written $\alpha u + (1-\alpha) v$ of $U$ from $u, v \in U$ .

The axioms are:

(3:A) $>$ is a complete ordering: (3:A:a) for any $u, v$ exactly one of $u = v$ , $u > v$ , $u < v$ holds; (3:A:b) $u > v$ , $v > w$ imply $u > w$ .
(3:B) Ordering and combining: (3:B:a) $u < v$ implies $u < \alpha u + (1-\alpha)v$ ; (3:B:b) $u > v$ implies $u > \alpha u + (1-\alpha)v$ ; (3:B:c) $u < w < v$ implies $\alpha u + (1-\alpha)v < w$ for some $\alpha$ ; (3:B:d) $u > w > v$ implies $\alpha u + (1-\alpha)v > w$ for some $\alpha$ .
(3:C) Algebra of combining: (3:C:a) $\alpha u + (1-\alpha)v = (1-\alpha)v + \alpha u$ ; (3:C:b) $\alpha(\beta u + (1-\beta)v) + (1-\alpha)v = \gamma u + (1-\gamma)v$ with $\gamma = \alpha\beta$ .

All weights lie strictly between $0$ and $1$ , and $=$ is identity. The expression $\alpha u + (1-\alpha)v$ is notation for an abstract operation: $U$ carries no linear structure. The Appendix mostly writes the operation as $(1-\gamma)u + \gamma v$ , and writes $u \leqq v$ for " $u = v$ or $u < v$ ". In the Lean development the system is the structure UtilitySystem U with fields gt and mix; S.cmb γ u v is $(1-\gamma)u + \gamma v$ .

A numerical utility (3.5.1) is a map $\mathrm v : U \to \mathbb R$ with

\text{(i)}\quad u > v \implies \mathrm v(u) > \mathrm v(v), \qquad \text{(ii)}\quad \mathrm v\big((1-\gamma)u + \gamma v\big) = (1-\gamma)\mathrm v(u) + \gamma\,\mathrm v(v) \quad (0<\gamma<1).

Formalization targets

Goal: (A:V) and (A:W), p. 627

For every system of utilities satisfying (3:A)–(3:C):

\exists\, \mathrm v : U \to \mathbb R \ \text{with (i), (ii)}, \qquad\text{and}\qquad \forall\, \mathrm v, \mathrm v' \text{ with (i), (ii)}:\ \exists\, \omega_0 > 0,\ \omega_1,\ \forall w,\ \ \mathrm v'(w) = \omega_0\,\mathrm v(w) + \omega_1 .

The constants $\omega_0, \omega_1$ are chosen before $w$ . No assumption on the size of $U$ is made.

Milestones

The milestones follow the Appendix's own chain:

(A:A) if $u < v$ and $\alpha < \beta$ then $(1-\alpha)u + \alpha v < (1-\beta)u + \beta v$ ;
(A:B), (A:C) for $u_0 < v_0$ , the map $\alpha \mapsto (1-\alpha)u_0 + \alpha v_0$ is a one-to-one, monotone map of $(0,1)$ onto the utility interval $u_0 < w < v_0$ ;
(A:E), (A:F) the interval function $f_{u_0,v_0}$ of (A:D) (value $0$ at $u_0$ , $1$ at $v_0$ , and the weight $\alpha$ in between) is monotone and linear toward each endpoint, and is characterized by these properties;
(A:R), (A:S) for fixed $u^* < v^*$ , the normalized mapping $h$ with $h(u^*) = 0$ , $h(v^*) = 1$ , monotone, and linear on combinations of $u < v$ , exists and is unique;
(A:T) $(1-\gamma)u + \gamma u = u$ always;
(A:U) $h$ is linear on all combinations, without the restriction $u < v$ .

Significance

The theorem turns an ordinal preference over uncertain prospects into a cardinal scale on which expectation is meaningful. It is what licenses replacing a player's preferences by numerical payoffs whose mixtures are averaged, which the rest of the book, and most of game theory and stochastic optimization after it, assumes. The uniqueness part (A:W) states exactly how much freedom the scale has: a positive linear transformation, i.e. zero and unit may be fixed at will and nothing else.

The theorem has been proved many times since 1947, in textbooks and in the mixture-space literature, but the book's axiom system differs from the later ones (it uses a strict order with identity, strict monotony, and the two algebraic axioms (3:C) only). As far as the curators know, neither this axiom system nor the Appendix's derivation has a machine-checked proof, and Mathlib has no mixture-space or expected-utility module. The mission produces a checked proof of the original theorem under its original hypotheses and a reusable abstract mixture-space layer.

Difficulty

The obvious argument treats $U$ as a convex set and $\alpha u + (1-\alpha)v$ as a convex combination, then reads the utility off the segment between two reference points. None of that is available. The operation is formal, so identities that hold in a vector space, idempotence $(1-\gamma)u + \gamma u = u$ included, must be derived from (3:B) and (3:C) alone; only one associativity rule (3:C:b), for a repeated right argument, is given. The correspondence between a utility interval and a numerical interval requires the continuity axioms (3:B:c), (3:B:d) and the completeness of the reals. The local scales on different intervals have to be fitted into one global function, and the linearity for pairs $u > v$ and $u = v$ has to be recovered from the case $u < v$ .

Formalization scope

$U$ is an arbitrary type (Type*); the relation is gt : U → U → Prop and the operation mix : OpenUnit → U → U → U, where OpenUnit is the subtype $(0,1)$ of $\mathbb R$ . mix α u v stands for $\alpha u + (1-\alpha)v$ . The operation is not defined at $\alpha = 0, 1$ (3.6.1, footnote 4) and is not extended there.
Axiom (3:A:a) is stated literally ("exactly one of the three relations"), so the order is a strict total order and indifference is identity (A.1.2). The weak-order generalization of §66 is not this theorem.
Numbers are real numbers. Monotony is strict, as in (3:1:a).
Standing hypotheses: every item assumes (3:A)–(3:C), bundled in UtilitySystem. The items from (A:E) on assume fixed $u_0 < v_0$ or $u^* < v^*$ as explicit hypotheses, as the book does "from now on until we get to (A:V) and (A:W)"; the goal does not, since (A:V), (A:W) hold for every $U$ .
The interval function $f_{u_0,v_0}$ is a total Lean function; its value outside $u_0 \leqq w \leqq v_0$ is a placeholder that no statement uses.
A formalization in which $U$ is a convex subset of a vector space, or a space of probability measures, assumes more than the book and makes (A:T) free; it does not count. Neither does a weak monotony, under which constant maps satisfy (A:V) and (A:W) fails.

A complete development needs only order theory and the completeness of the reals from Mathlib. The mixture-space layer (the structure, (A:A)–(A:C), (A:T)) is reusable for any later work on expected utility, including the generalization in §66 and 67 of the book. Proofs of any milestone, alternative routes to the goal (for instance through the Herstein–Milnor axioms, once shown to follow from (3:A)–(3:C)), and statements of the omitted intermediate results (A:G)–(A:Q) are all welcome.

Selected references

J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd edition, 1953), §3 and Appendix. https://doi.org/10.1515/9781400829460
I. N. Herstein, J. Milnor, An axiomatic approach to measurable utility, Econometrica 21 (1953), 291–297. https://doi.org/10.2307/1905540
J. Marschak, Rational behavior, uncertain prospects, and measurable utility, Econometrica 18 (1950), 111–141. https://doi.org/10.2307/1907264

12 thms4 active usersReviewed

Convex Optimization Optimization Probability·Captain: mikedeng1

Numerical Techniques for Stochastic Optimization II: Logarithmic Concavity of Probabilistic ConstraintsTextbook

Motivation

Many engineering and economic planning problems must meet random requirements with a prescribed reliability: a reservoir must satisfy demand with probability at least $0.95$ , a power system must cover load except on rare days, an inventory must avoid shortage with high probability. Probabilistic constrained programming (also called chance-constrained programming) models this by requiring that a system of random inequalities hold jointly with probability at least $p$ .

The first obstacle to solving such problems is structural. The probability that random constraints are satisfied is, in general, neither concave nor convex in the decision, so the feasible set need not be convex and local search can stall. Prékopa's theory of logarithmically concave measures (1971–1973) removed that obstacle for a large class of distributions, and it is the basis of the numerical methods of Chapter 5 of Ermoliev and Wets, Numerical Techniques for Stochastic Optimization (Springer 1988). This mission formalizes the structural theorems of that chapter.

Timeline:

1959: Charnes and Cooper, individual chance constraints.
1971: Prékopa, logarithmic concave measures with application to stochastic programming (Acta Sci. Math. Szeged 32).
1973: Prékopa, logarithmic concave measures and functions (Acta Sci. Math. Szeged 34), containing the marginal theorem: marginals of log-concave functions are log-concave.
1970s–1980s: nonlinear programming methods for (5.1) (SUMT with logarithmic penalty, supporting hyperplanes, reduced gradients) combined with Monte Carlo evaluation of $h_0$ ; the chapter surveys them.

Setting

Let $\xi$ be a random vector in $\mathbb R^q$ on a probability space $(\Omega, \mathcal F, P)$ and let $g_1, \dots, g_r : \mathbb R^n \times \mathbb R^q \to \mathbb R$ . The chapter studies problem (5.1):

\min h(x) \quad \text{s.t.} \quad h_0(x) = P\bigl(g_1(x,\xi) \ge 0, \dots, g_r(x,\xi) \ge 0\bigr) \ge p, \quad h_1(x) \ge p_1, \dots, h_m(x) \ge p_m .

The function $h_0$ is the probability function (chanceProb in Lean). In the special case $g_i(x,y) = T_i x - y_i$ it equals $F(Tx)$ , where $F$ is the joint distribution function of $\xi$ .

A function $f \ge 0$ is logarithmically concave on a convex set $S$ if

f(\lambda u + (1-\lambda) v) \ge f(u)^{\lambda} f(v)^{1-\lambda}, \qquad u, v \in S,\ 0 < \lambda < 1 .

Where $f > 0$ this is concavity of $\log f$ ; the power form also makes sense where $f = 0$ . Nondegenerate normal densities, uniform densities on convex bodies and exponential densities are log-concave.

Section 5.7 introduces the polynomial distribution (5.19) on the cube $0 < z_j \le 1$ :

F(z_1, \dots, z_n) = \frac{1}{\sum_{i=1}^{N} c_i z_1^{\alpha_{i1}} \cdots z_n^{\alpha_{in}}}, \qquad c_i > 0,\ \alpha_{ij} \le 0,\ \textstyle\sum_j \alpha_{ij} < 0

(polyDistF in Lean).

Formalization targets

Goal: Theorem 5.1

If $g_1, \dots, g_r$ are jointly concave on $\mathbb R^{n+q}$ and $\xi$ has a log-concave density $f$ on $\mathbb R^q$ , then

h_0 \text{ is logarithmically concave on } \mathbb R^n .

Its immediate consequence is that the feasible set $\{x : h_0(x) \ge p\}$ is convex for every $p$ .

Milestones

Theorem 5.2.1: if $h$ is log-concave on the convex set $H = \{h \ge p\}$ , $0 < p < 1$ , then $h - p$ is log-concave on $H$ . This makes the logarithmic penalty function (5.5) of the SUMT method convex.
Theorem 5.2.2: under the standing assumptions of §5.2, every interior point $z$ of the feasible set of (5.1) satisfies $h_i(z) > p_i$ , $i = 0, \dots, m$ .
Theorem 5.7.1 (proved content, (5.21)): for $n = 2$ and oppositely ordered exponents, $\partial^2 F / \partial z_1 \partial z_2 \ge 0$ on $(0,1)^2$ .
Theorem 5.7.2: the polynomial distribution function is log-concave on $(0,1]^n$ .

The platform theorem ConvexOptimization.prekopa_marginal_log_concave (Prékopa's marginal theorem, proved) is included as a reference item.

Significance

Theorem 5.1 turns a probabilistic constraint into a convex constraint after taking logarithms. This is what makes convergence proofs for nonlinear programming methods (SUMT with logarithmic penalty, supporting hyperplanes, reduced gradients) applicable to (5.1) and to the reliability maximization problem (5.4); without it, those methods have no guarantee of finding a global optimum. Theorems 5.2.1 and 5.2.2 are the two facts that make the SUMT method of §5.2 well defined and convex on the interior of the feasible set. Theorem 5.7.2 shows that probabilistic constraints under the polynomial distribution define convex sets, so they can be added to geometric programmes.

On status: Theorem 5.1 is a classical result, proved in Prékopa's papers (the chapter itself refers to Prékopa's survey for the proof). Prékopa's marginal theorem and the Prékopa–Leindler inequality are already machine-checked on this platform; Theorem 5.1 and the §5.2 and §5.7 theorems are, as far as a search of the platform shows, not formalized. The work is formalizing known proofs, in the log-concavity predicate the platform already uses.

Difficulty

The obvious argument for Theorem 5.1, "the constraint set is convex and the density is log-concave, so the probability is log-concave", hides the real content: log-concavity of a probability as a function of a parameter is a statement about integrals, and it does not follow from pointwise properties of the integrand without a Prékopa–Leindler-type inequality. Concavity of each $g_i$ separately in $x$ and in $y$ is not enough; joint concavity in $(x, y)$ is used essentially. The probability function vanishes on large regions in typical examples, so any argument that takes logarithms pointwise fails at the boundary of its support.

For Theorem 5.2.2 the naive argument fails at the index $i = 0$ : nothing about $h_0$ is assumed directly, and log-concavity of $h_0$ is exactly Theorem 5.1. For Theorem 5.7.1 the difficulty is a sign condition on a covariance; without the ordering hypothesis the mixed derivative can be negative.

Formalization scope

$\mathbb R^n$ and $\mathbb R^q$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin q); the constraint functions take pairs $(x, y)$ in the product, and concavity is ConcaveOn ℝ Set.univ on that product (joint concavity). A "continuous probability distribution with density $f$ " is stated as P.map ξ = volume.withDensity (ENNReal.ofReal ∘ f) with $\xi$ and $f$ measurable and $P$ a probability measure. Log-concavity is the platform definition ConvexOptimization.LogConcaveOn (nonnegativity plus the power inequality), imported as a reference item; concavity of Real.log ∘ h₀ would be a different, wrong property because Lean's Real.log 0 = 0. Indices are 0-based (Fin r, Fin m, Fin N, Fin n); the probabilistic constraint $i = 0$ of Theorem 5.2.2 is stated separately from $h_1, \dots, h_m$ . The polynomial distribution is a formula on Fin n → ℝ with real powers, used only on the cube.

No constant of the book is replaced by an explicit value: every result of this chapter is qualitative.

Corrections of the printed text, recorded in each item's Formalization Note:

Theorem 5.1 states the density condition "for every $x_1, x_2 \in \mathbb R^n$ "; the density lives on $\mathbb R^q$ and the condition is imposed there.
(5.19) prints the first factor as $z_i^{\alpha_{i1}}$ and the domain index as $i = 1, \dots, N$ ; they are read as $z_1^{\alpha_{i1}}$ and $j = 1, \dots, n$ .
Theorem 5.7.1 prints its ordering hypothesis with transposed indices ( $\alpha_{11} \le \alpha_{12} \le \dots \le \alpha_{1n}$ ); following the proof, it is read as: across the $N$ terms the $z_1$ -exponents increase and the $z_2$ -exponents decrease.
Theorem 5.7.1 claims "is a probability distribution function"; the book proves only (5.21), and normalization would need $\sum_i c_i = 1$ , which is not assumed. The formal statement is (5.21), the mixed derivative as an iterated deriv.

Theorem 5.2.2 carries all six assumptions of §5.2, including compactness of the feasible set and the Slater point; it does not assume log-concavity of $h_0$ , which must be derived from the density and concavity hypotheses. A trivializing formalization, such as one with a density hypothesis that no probability law satisfies or a log-concavity predicate that holds for every function vanishing somewhere, is ruled out: the density hypotheses are satisfiable (checked locally) and LogConcaveOn is the multiplicative inequality at every pair of points.

Needed infrastructure: Prékopa's marginal theorem (available), log-concavity of indicators of convex sets and of products, measurability of the constraint set, and Artin's theorem that a sum of log-convex functions is log-convex (for Theorem 5.7.2). Artin's theorem and closure properties of LogConcaveOn are reusable beyond this mission, and contributions of them are welcome.

Selected references

A. Prékopa, "Numerical Solution of Probabilistic Constrained Programming Problems", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 5, pp. 123–139. https://doi.org/10.1007/978-3-642-61370-8
A. Prékopa, "Logarithmic concave measures with application to stochastic programming", Acta Sci. Math. (Szeged) 32 (1971), 301–316.
A. Prékopa, "On logarithmic concave measures and functions", Acta Sci. Math. (Szeged) 34 (1973), 335–343.
A. Charnes and W. W. Cooper, "Chance-constrained programming", Management Science 6 (1959), 73–79. https://doi.org/10.1287/mnsc.6.1.73
B. L. Miller and H. M. Wagner, "Chance constrained programming with joint constraints", Operations Research 13 (1965), 930–945. https://doi.org/10.1287/opre.13.6.930
A. Prékopa, Stochastic Programming, Kluwer 1995. https://doi.org/10.1007/978-94-017-3087-7

9 thms4 active usersReviewed

Completed

Convex Optimization Linear Optimization Optimization+1·Captain: mikedeng1

Numerical Techniques for Stochastic Optimization I: Edmundson–Madansky Bounds for Independent Random Data and Simple RecourseTextbook

Motivation

In a two-stage stochastic linear program a decision $x$ is taken before random data $\xi$ are observed, and a corrective recourse decision $y$ is taken afterwards at a cost. The objective contains the expectation of an optimal value of a linear program, $\int Q(x,\xi(\omega))\,P(d\omega)$ , and for continuous or high-dimensional $\xi$ that integral cannot be evaluated exactly. Practical methods therefore replace $\xi$ by a discrete random vector and control the error by computable lower and upper bounds on the expected recourse cost. Chapter 2 of Ermoliev and Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), by P. Kall, A. Ruszczyński and K. Frauendorfer, surveys these bounds as they were used in the codes of the time: Jensen's inequality from below, the Edmundson–Madansky inequality from above, and the special structure of simple recourse, where the expected cost is available in closed form.

Timeline. Jensen's inequality (1906) gives the lower bound for a convex integrand. A. Madansky, "Bounds on the expectation of a convex function of a multivariate random variable", Ann. Math. Statist. 30 (1959), and H. P. Edmundson (RAND report, 1956) gave the upper bound by the two-point law on the endpoints of an interval, and its product version for independent components. Kall and Stoyan (1982), Huang, Ziemba and Ben-Tal (1977), Frauendorfer and Kall (1988) developed partition refinement of both bounds, the scheme this chapter describes; Frauendorfer (1988) extended the upper bound to dependent data on boxes.

Setting

The two-stage problem (2.11) is: minimize $\psi(x)=c^Tx+\int_\Omega Q(x,\xi(\omega))\,P(d\omega)$ subject to $Ax=b$ , $x\ge 0$ . The recourse cost $Q(x,\xi)$ is the optimal value of the second-stage problem (2.12),

Q(x,\xi)=\min\{q^Ty : Wy=h-Tx,\ y\ge 0\},\qquad \xi=(q,h,T),

with a deterministic $m_2\times n_2$ matrix $W$ (fixed recourse), and $Q=+\infty$ when (2.12) is infeasible. Throughout the chapter the book assumes complete recourse, $\{Wy:y\ge0\}=\mathbb R^{m_2}$ , and dual feasibility: for every realization of $q$ some $u$ satisfies $W^Tu\le q$ . Under these assumptions $Q$ is finite. The expected recourse function is $\mathcal Q(x)=\int Q(x,\xi(\omega))\,P(d\omega)$ .

The Edmundson–Madansky law of an interval $[a,b]$ , $a<b$ , with mean $\xi^0$ puts mass $p_1=(b-\xi^0)/(b-a)$ at $a$ and $p_2=(\xi^0-a)/(b-a)$ at $b$ (2.32). For a box $\Xi=\times_{j=1}^m[a_j,b_j]$ and means $\xi^0_j$ , the vector $\hat\xi$ with independent components of these two-point laws sits at the vertex $v$ with probability $\prod_j p_j(v_j)$ .

Simple recourse is the case $W=[I,-I]$ , $q=[q^+,q^-]$ with $q^+_j+q^-_j\ge0$ , deterministic $T$ and random $h$ only. With $\chi=Tx$ the recourse cost splits into one-row costs $Q_j(\chi_j,h_j)=q^+_j(h_j-\chi_j)$ if $h_j\ge\chi_j$ , and $q^-_j(\chi_j-h_j)$ otherwise.

Formalization targets

Goal: the Edmundson–Madansky bound for independent components (p. 46)

If $\xi$ has independent components $\xi_j\in[a_j,b_j]$ with means $\xi^0_j$ , and $\varphi$ is convex on $\Xi=\times_j[a_j,b_j]$ , then

E\varphi(\xi)\le\sum_{v\in\mathrm{vert}\,\Xi}\Big(\prod_{j=1}^m p_j(v_j)\Big)\varphi(v).

The book applies it to $\varphi=Q(x,\cdot)$ ; the goal is stated for every convex $\varphi$ , with the explicit weights of (2.32).

Milestones

Properties (b), (d), (e) of p. 40: $Q(x,\cdot)$ is piecewise linear and convex in $(h,T)$ ; $Q(\cdot,\xi)$ is convex piecewise linear in $x$ ; the expected recourse function is finite and convex under finite second moments.
The Jensen lower bound (2.26)–(2.27) on a partition (a published, proved theorem, reused).
The dual-multiplier lower bound (2.30)–(2.31).
The one-dimensional Edmundson–Madansky inequality (2.32)–(2.34).
For simple recourse: separability (2.46)–(2.49), the closed form (2.51) of $EQ_j$ , and the bounds (2.55)–(2.56) from the one-block problem.

Significance

The upper bound is the half of the bounding scheme that is not automatic. Jensen's inequality needs only a mean; an upper bound on the expectation of a convex function needs a bounded support and, in the product form, independence. Together they give a certified interval for the optimal value of a two-stage problem, and repeated partitioning of the support shrinks that interval; this is the basis of the sequential approximation methods of §2.2.4 and of later codes. The dual-multiplier bound and the simple-recourse formulas are the pieces that make those intervals cheap to compute.

The results are classical and proved in the literature cited on the page. The one-dimensional Edmundson–Madansky inequality and the general extreme-point form of the upper bound (a measure on the extreme points reproducing the barycentre) are already formalized on Prove2Me in the Introduction to Stochastic Programming series, as is the partition Jensen bound. The product form for independent components is not: deriving it from the extreme-point form requires constructing the product kernel, which is the content of this mission. The recourse properties (b), (d), (e) for a general distribution with finite second moments, the dual-multiplier bound and the simple-recourse formulas are not formalized anywhere known to this mission.

Difficulty

The obvious argument inducts on the dimension, applying the one-dimensional inequality in one coordinate while the others are held fixed. That step needs the conditional law of the remaining coordinates given the first to be their unconditional law, i.e. independence expressed as a product decomposition of the joint law, and it needs $\varphi$ with one coordinate replaced by an endpoint to remain convex on the lower-dimensional box and integrable. For dependent components the inequality is false with these weights: on $[0,1]^2$ with means $(\tfrac12,\tfrac12)$ and $\varphi(x,y)=(x-y)^2$ , the product law gives $\tfrac12$ while mass $\tfrac12$ at $(1,0)$ and at $(0,1)$ gives $1$ . The book's remark that the product law is extremal among all laws on $\Xi$ with the given mean fails for this reason when $m\ge2$ , and is not part of this mission.

For the recourse properties the difficulty is bookkeeping: $Q$ is an extended-real optimal value, and finiteness, measurability in $\omega$ and integrability must be derived from complete recourse, dual feasibility and the moment hypothesis rather than assumed.

Formalization scope

Vectors are functions from finite index types to $\mathbb R$ (ι → ℝ), matrices are Mathlib Matrix, and random data live on a probability space (Ω, P). The recourse cost is an EReal infimum over the feasible set, so infeasibility gives $+\infty$ and unboundedness $-\infty$ exactly as on p. 39; theorems that integrate it carry complete recourse and dual feasibility, which make it finite. The expected recourse function integrates the real part of the recourse cost. Independence of the components is ProbabilityTheory.iIndepFun; the box is Set.pi univ (fun j => Icc (a j) (b j)), with $a_j<b_j$ , and values in the box are required almost surely. The upper bound is the explicit sum over Boolean vertex labels of products of the weights (2.32); no abstract extremal measure is used.

Conventions fixed where the page is silent or ambiguous:

Properties (b), (d), (e) are stated on all of $\mathbb R^{n_1}$ : under the standing complete-recourse assumption $K_2=\mathbb R^{n_1}$ . "Convex piecewise linear" is rendered as a maximum of finitely many affine functions.
The book's hypothesis of finite second moments in (e) is kept as stated, componentwise.
The book writes $Q$ for both $Q(x,\xi)$ and $\mathcal Q(x)$ , and reuses $\tilde Q$ , $\tilde\psi$ for different functions in (2.27) and (2.30)–(2.31); the Lean names are recourseCost, expectedRecourse and dualLowerBound.
In (2.51) a conditional mean on a null event is $0$ in Lean; it always appears multiplied by that event's probability, so the formula is unchanged.
In (2.56) the minimum is a real infimum over the nonempty first-stage feasible set; attainment is not claimed.
No constant of the chapter is hidden behind $O(\cdot)$ ; all bounds are explicit.

A goal stated for affine $\varphi$ (where it is an equality), or with $\hat\xi$ allowed to be any discrete law with the right mean, would be trivial or a different theorem; the weights are the products of (2.32), and independence of the components is a hypothesis.

A complete development needs: finite-dimensional LP duality with extended-real values (reusable across all recourse missions), measurability and integrability of optimal-value functions, the conditional-independence step for product measures, and the one-dimensional chord inequality. The partitioned upper bound (2.37) and the discrete reformulation (2.21), (2.28) are natural follow-up statements on the same definitions.

Selected references

P. Kall, A. Ruszczyński, K. Frauendorfer, "Approximation Techniques in Stochastic Programming", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 2, pp. 33–64. https://doi.org/10.1007/978-3-642-61370-8
A. Madansky, "Bounds on the expectation of a convex function of a multivariate random variable", Annals of Mathematical Statistics 30 (1959), 743–746. https://doi.org/10.1214/aoms/1177706203
P. Kall, Stochastic Linear Programming, Springer 1976. https://doi.org/10.1007/978-3-642-66252-2
R. J-B Wets, "Stochastic programs with fixed recourse: the equivalent deterministic program", SIAM Review 16 (1974), 309–339. https://doi.org/10.1137/1016053
K. Frauendorfer, "Solving SLP recourse problems with arbitrary multivariate distributions — the dependent case", Mathematics of Operations Research 13 (1988), 377–394. https://doi.org/10.1287/moor.13.3.377
J. R. Birge, F. Louveaux, Introduction to Stochastic Programming, Springer 1997, Ch. 8. https://doi.org/10.1007/b97617

13 thms4 active usersReviewed

Convex Optimization Optimization Probability·Captain: mikedeng1

Introduction to the Scenario Approach I: The Violation Distribution of the Scenario SolutionTextbook

Motivation

Many design problems in control, finance and operations research are convex programs with uncertain constraints: a decision $\theta$ must satisfy $\theta\in\Theta_\delta$ for a parameter $\delta$ that is not known in advance. Enforcing the constraint for every possible $\delta$ (robust optimization) is often intractable or too conservative, and a chance-constrained formulation needs the distribution of $\delta$ , which in practice is rarely known. The scenario approach replaces the uncertain constraint by the constraints of $N$ observed samples $\delta_1,\dots,\delta_N$ and solves the resulting ordinary convex program. The question it answers is how much of the unseen uncertainty the resulting decision still violates.

The answer, the generalization theorem of the scenario approach, is distribution-free: the probability that the scenario solution violates more than a fraction $\varepsilon$ of the uncertainty is bounded by a binomial tail that depends only on $N$ and on the number $d$ of decision variables. This mission formalizes that theorem as it is presented in Chapters 3 and 5 of Campi and Garatti's textbook Introduction to the Scenario Approach (SIAM/MOS 2018), the first mission of a series on the book.

Timeline. Calafiore and Campi introduced scenario programs and bounded the violation of their solutions through the count of support constraints (Math. Program. 2005; IEEE TAC 2006). Campi and Garatti proved in 2008 that the binomial-tail bound of Theorem 3.7 holds for every convex scenario program under existence and uniqueness of the solution, and that it is attained with equality by fully supported problems (SIAM J. Optim. 2008), which settled the tightness question. The textbook (DOI 10.1137/1.9781611975444) presents the theorem with a complete proof for fully supported problems in the plane.

Setting

Fix a cost vector $c\in\mathbb R^d$ , a domain $\Theta\subseteq\mathbb R^d$ , a measurable space $\Delta$ of uncertainty instances with a probability $\mathbb P$ , and a constraint set $\Theta_\delta\subseteq\mathbb R^d$ for each $\delta\in\Delta$ .

The violation of a decision $\theta$ (Definition 3.1) is $V(\theta)=\mathbb P\{\delta\in\Delta:\theta\notin\Theta_\delta\}$ , the probability that $\theta$ fails the constraint of a fresh instance.
For a sample $(\delta_1,\dots,\delta_m)$ , the scenario program is

\min_{\theta\in\Theta}c^T\theta\quad\text{subject to}\quad\theta\in\bigcap_{i=1}^{m}\Theta_{\delta_i}.

A solution is a feasible point of least cost. With $m=N$ i.i.d. samples its solution is denoted $\theta^*$ ; it is a random vector, a function of the sample, and $V(\theta^*)$ is a random variable in $[0,1]$ .

Assumption 3.4 (convexity): $\Theta$ and every $\Theta_\delta$ are convex and closed. Assumption 3.6 (existence and uniqueness): for every $m$ and every sample, the program with $m$ constraints has exactly one solution.
A constraint is a support constraint (Definition 5.1) if its removal improves the solution. A problem is fully supported (Definition 5.4) if for every $m\ge d$ the program with $m$ constraints has, with probability 1, exactly $d$ support constraints.

Formalization targets

Goal: Theorem 3.7

For $1\le d\le N$ and every $\varepsilon\in[0,1]$ , under Assumptions 3.4 and 3.6,

\mathbb P^N\{V(\theta^*)>\varepsilon\}\le\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}.

The right-hand side is the upper tail of a Beta $(d,N-d+1)$ distribution. The statement leaves $\mathbb P$ , $\Theta$ and the constraint family completely unspecified beyond the two assumptions.

Milestones

Helly's lemma (Lemma 5.3), referenced from the platform in its $d$ -dimensional form.
Theorem 5.2: for every $m$ and every sample, a convex scenario program has at most $d$ support constraints.
Eq. (5.3): for a fully supported problem with $d=N=2$ , $\mathbb P^2\{V(\theta^*)>\varepsilon\}=1-\varepsilon^2$ .
Eq. (5.2): for fully supported problems, Theorem 3.7 holds with equality.
Eqs. (3.5)–(3.6): the bound is the Beta $(d,N-d+1)$ distribution function (a published incomplete-beta identity).
Eq. (3.9): $\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}\le 2^{d-1}(1-\varepsilon/2)^N\le2^{d-1}e^{-\varepsilon N/2}$ .
Theorem 3.8: $\mathbb E[V(\theta^*)]\le d/(N+1)$ .
Theorem 1.3: if $N\ge\frac2\varepsilon(\ln\frac1\beta+d-1)$ , then $V(\theta^*)\le\varepsilon$ with probability at least $1-\beta$ .

Significance

Theorem 3.7 is what makes the scenario approach usable as a design method: it certifies the reliability of a decision computed from data without any knowledge of the data-generating distribution, requiring only independence of the samples. Theorems 3.8 and 1.3 are its two most used consequences, an expected-violation bound and an explicit sample size, and later chapters of the book (constraint removal, the FAST algorithm, empirical-cost results) build on the same statement. Equality for fully supported problems shows that the bound cannot be improved for any $d$ and $N$ .

The theorem is proved in the literature; it has no machine-checked proof. A formalization produces, beyond the result itself, a reusable library of scenario programs, violation probabilities and support constraints on which the rest of the series (constraint removal, nonconvex support sets) can be stated, and it checks the measure-theoretic content that the book deliberately leaves aside ("measurability issues are glossed over throughout", p. 33).

Difficulty

The deterministic part, at most $d$ support constraints, is a short consequence of Helly's theorem. The probabilistic part is where the obvious approach fails. A uniform-convergence argument over all $\theta$ (Vapnik–Chervonenkis theory, footnote 11 of the book) gives bounds of the wrong order and can be vacuous, because it ignores that only the solution matters. The sharp bound is an exact statement about the law of $V(\theta^*)$ , not a union bound, and problems with fewer than $d$ support constraints, or with degenerate configurations of constraints, must be shown to be no worse than fully supported ones; the book treats the general case only in the plane and refers to Campi & Garatti 2008 for general $d$ . Handling the null sets and the exchangeability of the samples under the product measure is a substantial part of the work.

Formalization scope

Decisions live in EuclideanSpace ℝ (Fin d); the cost is inner ℝ c θ. A sample of size $m$ is ω : Fin m → Δ with law Measure.pi (fun _ : Fin m => P), and P is a probability measure.
The violation is the real number (P {δ | θ ∉ Θδ δ}).toReal; probabilities of events over the sample are compared in $[0,\infty]$ through ENNReal.ofReal.
The solution $\theta^*$ is a function θstar : (Fin N → Δ) → EuclideanSpace ℝ (Fin d) together with the hypothesis that θstar ω solves the program for every sample; it is never an arbitrary map.
Assumption 3.6 is stated for every $m$ including $m=0$ (a unique minimizer on $\Theta$ itself) and for every sample, as on the page.
Hypotheses the page leaves implicit are explicit: the constraint relation $\{(\theta,\delta):\theta\in\Theta_\delta\}$ is jointly measurable and θstar is measurable (the book's p. 33 convention); $\varepsilon\in[0,1]$ ; $d\ge1$ .
A support constraint is one whose removal leaves a feasible point of strictly smaller cost than the solution; the count is a Finset.card over Fin m.
Theorem 3.8 asserts integrability of $V(\theta^*)$ together with the bound, so it cannot hold through the convention that a non-integrable function integrates to $0$ . Theorem 1.3's own sentence omits the assumptions; they are added as in §3.2.1, where it is derived from Theorem 3.7.

A statement in which $\theta^*$ is any feasible point of the program, or merely a measurable function of the sample, is false and does not count as a formalization of Theorem 3.7; nor does one in which Assumption 3.6 is weakened to almost every sample. Contributions of general infrastructure are welcome: exchangeability arguments for product measures, the binomial–beta identity, and Helly-type counting lemmas are reusable well beyond this mission.

Selected references

M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM/MOS, 2018. https://doi.org/10.1137/1.9781611975444
M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19(3), 2008. https://doi.org/10.1137/07069821X
G. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Mathematical Programming 102, 2005. https://doi.org/10.1007/s10107-003-0499-y
G. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51(5), 2006. https://doi.org/10.1109/TAC.2006.875041
E. Helly, Über Mengen konvexer Körper mit gemeinschaftlichen Punkten, Jahresbericht der DMV 32, 1923.

12 thms4 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Optimization·Captain: mikedeng1

Algorithmic Mechanism Design I: MinWork Is a Strongly Truthful n-Approximation Mechanism for Task Scheduling on Unrelated MachinesResearch Paper

Motivation

Algorithmic mechanism design asks for algorithms whose inputs are held by self-interested parties. Each party reports its private data, the algorithm computes an outcome, and payments are arranged so that no party gains by misreporting. Nisan and Ronen introduced the field in Algorithmic Mechanism Design (Games Econ. Behav. 35, 2001). Their running example is task scheduling on unrelated machines: $k$ tasks are distributed among $n$ machines owned by different agents, each agent knows only its own processing times, and the designer wants to minimize the make-span.

Without incentives the problem is classical: minimizing make-span on unrelated machines is NP-hard and admits a polynomial 2-approximation (Lenstra, Shmoys, Tardos, 1990). With selfish agents the question changes: which approximation ratios can a truthful mechanism guarantee? This mission formalizes the paper's upper bound, the MinWork mechanism, which is the benchmark every later lower bound for truthful scheduling is compared with.

Timeline.

1961: Vickrey introduces the second-price auction (J. Finance 16).
1971–1973: Clarke and Groves generalize it to the VCG family of truthful mechanisms for utilitarian objectives (Groves, Econometrica 41, 1973).
1999/2001: Nisan and Ronen show MinWork is a strongly truthful $n$ -approximation, and that no truthful mechanism beats ratio 2.
2007: Christodoulou, Koutsoupias and Vidali raise the deterministic lower bound to $1+\sqrt2$ for $n \ge 3$ ; Koutsoupias and Vidali later raise it to $1+\varphi \approx 2.618$ .
2023: Christodoulou, Koutsoupias and Kovács prove the Nisan–Ronen conjecture: no deterministic truthful mechanism achieves a ratio below $n$ (STOC 2023, arXiv:2301.11905), so MinWork is optimal among deterministic truthful mechanisms.

Setting

There are $n$ agents and $k$ tasks. Agent $i$ 's type is the vector $t^i = (t^i_1,\dots,t^i_k)$ of positive times, $t^i_j > 0$ being the time agent $i$ needs to perform task $j$ . A type vector is $t = (t^1,\dots,t^n)$ . An allocation $x$ sends each task $j$ to one agent; $x^i$ is the set of tasks agent $i$ receives. The make-span of $x$ is

g(x,t) = \max_{i} \sum_{j \in x^i} t^i_j ,

and agent $i$ 's valuation is $v^i(x,t^i) = -\sum_{j \in x^i} t^i_j$ .

A direct mechanism asks every agent to declare a type, computes an allocation $x(d)$ from the declared vector $d$ , and hands agent $i$ a payment $p^i(d)$ . Agent $i$ 's utility is $p^i(d) + v^i(x(d), t^i)$ , with $t^i$ its true type. The mechanism is truthful if declaring $t^i$ maximizes agent $i$ 's utility for every declaration of the others, and strongly truthful if truth-telling is the only such dominant strategy. An allocation rule is a $c$ -approximation if $g(x(t),t) \le c \cdot g(y,t)$ for every type vector $t$ and every allocation $y$ .

The MinWork mechanism allocates each task to an agent with minimal declared time for it, breaking ties arbitrarily. For each task it wins, an agent receives the second-best declared time $\min_{i' \ne i} d^{i'}_j$ :

p^i(d) = \sum_{j \in x^i(d)} \min_{i' \neq i} d^{i'}_j .

The Lean development uses the same names: load, makespan, IsTruthful, IsStronglyTruthful, IsApprox, IsMinWorkAlloc, secondBest, minTime, minWorkPay.

Formalization targets

Goal: Theorem 4.1

For $n \ge 2$ and every MinWork allocation rule $x$ with payments $p$ as above,

(x,p)\ \text{is strongly truthful} \quad\text{and}\quad g(x(t),t) \le n \cdot g(y,t)\ \ \text{for all positive } t \text{ and all allocations } y .

Milestones

Theorem 3.1 (Groves): a VGC mechanism is truthful. This is an existing platform theorem, used as a reference.
MinWork belongs to the VGC family. Its allocation maximizes $\sum_i v^i(t^i,x)$ , and its payment is $\sum_{i'\ne i} v^{i'}(t^{i'},x(t)) + h^{-i}$ with $h^{-i} = \sum_j \min_{i'\ne i} t^{i'}_j$ .
Claim 4.2: MinWork is strongly truthful.
$g(x(t),t) \le \sum_{j} \min_i t^i_j$ .
$g(y,t) \ge \frac1n \sum_j \min_i t^i_j$ for every allocation $y$ .
Claim 4.3: MinWork is an $n$ -approximation.

Significance

The theorem gives the first positive result for truthful scheduling: a mechanism that is truthful in the strongest sense and is within a factor $n$ of optimal, whatever the tie-breaking rule. Every lower bound in the paper (Theorems 4.6, 4.10 and 4.12) and in the later literature measures itself against this ratio. Since the 2023 resolution of the Nisan–Ronen conjecture, the ratio $n$ is known to be tight for deterministic truthful mechanisms.

The result is proved in the paper; it is not known to be formalized in any proof assistant. The platform already has Groves' theorem in an abstract form (AGT.vcg_incentive_compatible). This mission connects that abstract statement to a concrete combinatorial mechanism, and it adds the strict part of strong truthfulness for any number of tasks and agents, which the paper proves only for one task and two agents. The vocabulary (make-span over unrelated machines, direct scheduling mechanisms, strong truthfulness) is shared with the seven later missions of this series.

Difficulty

Truthfulness follows from Groves' theorem once MinWork is identified as a VGC mechanism. The identification requires the payment identity at every declared vector and under every tie-breaking rule, including ties at the winning time. The main difficulty is the strict part of strong truthfulness. A misreport that differs from the truth only on one task must still be shown to lose strictly for some declarations of the others. Those declarations must stay positive, and on every other task they must leave the outcome unchanged. The paper's proof covers only one task and two agents and leaves the general case as "similar". Its printed inequality also has the two utilities in the wrong order (see below), so it cannot be transcribed directly.

Formalization scope

Agents are Fin n and tasks are Fin k. An allocation is a function Fin k → Fin n, and an agent may receive no task. Types are positive reals, and every truthfulness and approximation quantifier ranges over positive true types, positive misreports and positive declarations of the others.
Payments are handed to the agent, so utility is the payment minus the true time spent. Payments are computed from the declared vector, never from true types.
The allocation rule is a parameter satisfying the MinWork specification (IsMinWorkAlloc). Every result holds for every tie-breaking rule, including rules that depend on the whole declared vector. No particular argmin is fixed.
$n \ge 2$ is a hypothesis of the goal and of the truthfulness items: with a single agent the paper's second-best minimum is undefined. The approximation items need only $n \ge 1$ . There is no hypothesis on $k$ .
The make-span and both minima are Finset.sup' / Finset.inf' over nonempty finite sets, so they are true maxima and minima with no default values.
Strong truthfulness is formalized as truthfulness plus: every misreport $d^i \ne t^i$ is strictly worse than the truth for some positive declarations of the others. Given truthfulness this is equivalent to Definition 5. A formalization that states only that truth-telling is dominant, or proves strictness only for single-task instances, does not meet the goal. Neither does an existential ratio in place of $n$ .
Printed slip: in the proof of Claim 4.2 (p. 177) the case $d^i > t^i$ reads "the utility for agent $i$ is $t^i - d^i < 0$ , instead of 0 in the case of truth-telling". With the Definition 11 payments the misreporting agent loses the task (utility 0), and the truthful agent wins it with utility $d^{3-i} - t^i > 0$ . The milestone text keeps the paper's words; the Lean statements assert what the argument establishes.
Out of scope: running time ("polynomial time"), and the paper's general revelation-principle framework (Proposition 2.1).
Welcome contributions: proofs of the milestones, and a reusable lemma connecting the local VGC milestone to AGT.vcg_incentive_compatible.

Selected references

N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
T. Groves, Incentives in Teams, Econometrica 41 (1973) 617–631. https://doi.org/10.2307/1914085
W. Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16 (1961) 8–37. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
G. Christodoulou, E. Koutsoupias, A. Kovács, A Proof of the Nisan-Ronen Conjecture, STOC 2023. https://arxiv.org/abs/2301.11905

9 thms4 active usersReviewed

Completed

Linear Optimization Optimization·Captain: mikedeng1

Selected Topics in Column Generation III: Ryan–Foster Branching — a Fractional Basic Set-Partitioning Solution Covers Some Row Pair FractionallyResearch Paper

Motivation

Column generation solves linear programs with far too many variables to list: one works with a small subset $J' \subseteq J$ of the columns, the restricted master problem (RMP), and adds columns of negative reduced cost as a pricing problem finds them (Lübbecke and Desrosiers 2005, §2.1). Many integer programs from vehicle routing, crew scheduling and crew pairing are reformulated so that the master problem is a set-partitioning problem: every row (a customer, a flight leg, a task) must be covered by exactly one selected column (a route, a pairing, a schedule). The linear relaxation of such a master is solved by column generation, and an integer solution is then sought by branch-and-price, branch-and-bound with column generation at every node.

Branching in branch-and-price is not free. Fixing a master variable $\lambda_j$ to $0$ does not stop the pricing problem from regenerating the same column, and handling that complicates the pricing problem. The rule that avoids this for set partitioning goes back to Ryan and Foster (1981): branch on a pair of rows, requiring them to be covered either by the same column or by two different columns. Both requirements are constraints the pricing problem can respect directly. Lübbecke and Desrosiers call it "the most common scheme in conjunction with column generation" (§7.3, p. 1020) and state the proposition that makes it well defined as their Proposition 3.

Timeline:

1981: Ryan and Foster introduce the pair-of-rows branching rule for set partitioning in crew scheduling.
1998: the branch-and-price survey of Barnhart et al. (1998) presents the rule as the branching scheme for set-partitioning masters.
2005: Lübbecke and Desrosiers state it as Proposition 3 of their survey, attributing it to Ryan and Foster without proof.

Setting

Rows are indexed by $\{1, \dots, m\}$ and columns by a finite set $J'$ . A matrix $A = (a_{rj}) \in \{0,1\}^{m \times |J'|}$ has every entry equal to $0$ or $1$ ; column $j$ covers row $r$ when $a_{rj} = 1$ . The set-partitioning system of the RMP's linear relaxation is

A\lambda = \mathbf 1, \qquad \lambda \ge \mathbf 0, \qquad \lambda \in \mathbb R^{J'} .

A vector $\lambda$ is a basic feasible solution of this system when it satisfies all its constraints and, among the constraints active at $\lambda$ (the $m$ equality rows, and the constraints $\lambda_j \ge 0$ with $\lambda_j = 0$ ), there are $|J'|$ linearly independent ones. Equivalently, $\lambda$ is feasible and the columns of $A$ in the support of $\lambda$ are linearly independent. A solution is fractional when it is not a $0/1$ vector, $\lambda \notin \{0,1\}^{|J'|}$ .

For two rows $r, s$ the Ryan–Foster quantity is $\sum_{j \in J'} a_{rj} a_{sj} \lambda_j$ , written pairCover A lam r s in Lean: the total weight on the columns that cover both rows. For $r = s$ it is the row sum, equal to $1$ on every feasible $\lambda$ .

Formalization targets

Goal: Proposition 3 (p. 1020)

For every $0/1$ matrix $A$ and every fractional basic feasible solution $\lambda$ of $A\lambda = \mathbf 1$ , $\lambda \ge \mathbf 0$ ,

\exists\, r, s \in \{1, \dots, m\}: \qquad 0 < \sum_{j \in J'} a_{rj}\, a_{sj}\, \lambda_j < 1 .

The two rows are automatically distinct. The statement concerns every fractional basic solution, not only an optimal one, and no cost vector enters it.

Milestone: the branches keep every integer solution (§7.3, p. 1020)

For every $0/1$ solution $\lambda \in \{0,1\}^{|J'|}$ of $A\lambda = \mathbf 1$ and every pair of rows $r, s$ ,

\sum_{j \in J'} a_{rj}\, a_{sj}\, \lambda_j \in \{0, 1\} .

This is the paper's requirement that "integer solutions remain intact" (p. 1019), specialised to the two branches " $= 1$ " and " $= 0$ " of the paragraph after Proposition 3.

Significance

Proposition 3 is what makes Ryan–Foster branching a valid branching scheme in the sense of §7.3: the current fractional solution violates both branches for the chosen pair, so it is excluded from both children, while by the milestone every integer solution survives in one of them. The same pair-of-rows idea underlies branching in bin packing, graph colouring, vehicle routing and crew scheduling codes, where it is used because both branches translate into constraints on the pricing problem rather than on individual master variables.

The paper states the result and refers its proof to Ryan and Foster (1981); no machine-checked version of the proposition is known. This mission produces a formal statement tied to a standard, representation-aware definition of basic solutions (Bertsimas–Tsitsiklis Definition 2.9, already on the platform) and, once proved, a verified lemma that any formal development of branch-and-price for set partitioning can cite.

Difficulty

An argument that uses only feasibility and a fractional coordinate cannot work. Without basicness the claim is false: with one row and two identical columns, $A = [1\ 1]$ , the vector $\lambda = (\tfrac12, \tfrac12)$ is feasible and fractional, yet the only pair of rows is $r = s$ , whose quantity is $1$ . The difficulty is to turn basicness, a linear-algebra condition, into a combinatorial statement about which rows the fractional columns cover. A set-partitioning matrix need not have full row rank, so the familiar description of basic solutions through an invertible basis matrix is not available in general.

Formalization scope

Rows are Fin m and columns Fin n, so $J'$ is identified with $\{0, \dots, n-1\}$ . $A$ is a real matrix Matrix (Fin m) (Fin n) ℝ with the hypothesis IsZeroOneMatrix A (every entry $0$ or $1$ ); $\lambda$ is lam : Fin n → ℝ, since λ is a Lean keyword. Columns are $0/1$ vectors; the equivalent reading as subsets of the rows is only prose.
"Basic solution" is not defined in the paper. It is read as Bertsimas–Tsitsiklis Definition 2.9 for the standard-form constraint family: LinearOptimization.IsBasicFeasibleSolution (LinearOptimization.stdFormSystem A (fun _ => 1)) lam, from the platform definitions BasicSolution and ActiveConstraints. This definition needs no full-row-rank assumption, which a set-partitioning matrix need not satisfy, and it is not replaced by an ad hoc support condition.
Typo correction. The paper writes "i.e., $\lambda \notin \{0,1\}^m$ ". Since $\lambda$ has one coordinate per column, the statement reads it as $\lambda \notin \{0,1\}^{|J'|}$ : ¬ IsZeroOneVector lam.
The rows $r, s$ range over all of $\{1, \dots, m\}$ , including $r = s$ , as on the page; no distinctness is assumed or required.
"Fractional basic solution" is any such solution, not the RMP optimum; no costs or optimality hypothesis enter.
The milestone reads the paragraph after Proposition 3, together with the validity requirement "integer solutions remain intact" (p. 1019), as the dichotomy for all $0/1$ solutions of $A\lambda = \mathbf 1$ . The sentence about transferring the branching information to the pricing problem is not formalized.
Edge cases: for $m = 0$ basicness forces $\lambda = 0$ , and for $n = 0$ the vector is empty; in both cases no fractional basic solution exists and the goal is vacuous, as on the page.
A trivializing formalization is ruled out: dropping basicness makes the goal false (the $[1\ 1]$ example above), dropping the $0/1$ hypothesis on $A$ changes the meaning of the quantity, and replacing "fractional basic" by an unsatisfiable hypothesis would make it empty; the hypotheses are satisfied, for instance, by three rows, the columns $\{1,2\}, \{2,3\}, \{1,3\}$ and $\lambda = (\tfrac12, \tfrac12, \tfrac12)$ .

A complete development needs linear-algebra facts about basic solutions of standard-form systems without a rank assumption (support columns linearly independent), which are reusable beyond this mission. Contributions welcome: that characterization as a lemma, and proofs of the milestone and of the goal.

Selected references

M. E. Lübbecke and J. Desrosiers, Selected Topics in Column Generation, Operations Research 53(6):1007–1023, 2005. https://doi.org/10.1287/opre.1050.0234
D. M. Ryan and B. A. Foster, An integer programming approach to scheduling, in A. Wren (ed.), Computer Scheduling of Public Transport, North-Holland, 1981, pp. 269–280.
C. Barnhart, E. L. Johnson, G. L. Nemhauser, M. W. P. Savelsbergh and P. H. Vance, Branch-and-Price: Column Generation for Solving Huge Integer Programs, Operations Research 46(3):316–329, 1998. https://doi.org/10.1287/opre.46.3.316
D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Definition 2.9.

5 thms4 active usersReviewed

Completed

Convex Optimization Optimization Probability·Captain: mikedeng1

Random Gradient-Free Minimization of Convex Functions III: Accelerated Random SearchResearch Paper

Motivation

Many optimization problems in engineering, simulation-based design and machine learning give access only to function values: the objective is the output of a simulator or a black-box program, and its gradient is unavailable or too expensive. Derivative-free (or zeroth-order) methods address this setting. Nesterov and Spokoiny (Found. Comput. Math. 17 (2017)) showed that a very simple oracle, the finite difference of $f$ along a random Gaussian direction, can replace the gradient in standard first-order schemes at the price of a factor depending only on the dimension. Their analysis became the reference point for later work on zeroth-order stochastic optimization and on gradient-free methods in reinforcement learning and adversarial attacks.

This mission covers Section 6 of the paper: the accelerated random method $\mathcal{FG}_\mu$ and its rate, Theorem 9. It is the third mission of a series; the first covers random search for nonsmooth problems (Theorem 6), the second the random gradient method for smooth problems (Theorem 8).

Setting

Let $E$ be a real inner product space of dimension $n \ge 2$ with norm $\|\cdot\|$ (the paper's space with operator $B$ is $E$ with the inner product $\langle Bx, y\rangle$ ). Let $u$ be a standard Gaussian vector in $E$ , and write $\mathbb E_u$ for expectation over $u$ .

The objective $f : E \to \mathbb R$ is differentiable with Lipschitz gradient, $\|\nabla f(x) - \nabla f(y)\| \le L_1\|x - y\|$ with $L_1 > 0$ , and strongly convex with parameter $\tau \ge 0$ :

f(y) \ge f(x) + \langle\nabla f(x), y - x\rangle + \tfrac{\tau}{2}\|y - x\|^2 .

The value $\tau = 0$ is allowed (plain convexity). The condition number is $\kappa = \tau/L_1$ . The problem $f^* = \min_{x \in E} f(x)$ is assumed solvable, with minimizer $x^*$ .

For $\mu \ge 0$ the Gaussian approximation is $f_\mu(x) = \mathbb E_u f(x + \mu u)$ , and the random gradient-free oracle is

B^{-1}g_\mu(x) = \frac{f(x + \mu u) - f(x)}{\mu}\,u \quad (\mu > 0), \qquad B^{-1}g_0(x) = \langle\nabla f(x), u\rangle\,u .

The paper (p. 548) sets $\theta_n = 1/(16(n+1)^2L_1(f))$ and $h_n = 1/(4(n+4)L_1(f))$ . This mission uses $\theta_n = 1/(16(n+4)^2L_1)$ ; the reason is given under Formalization scope. Method $\mathcal{FG}_\mu$ (Eq. (60)) chooses $x_0 \in E$ , $v_0 = x_0$ and $\gamma_0 > 0$ with $\gamma_0 \ge \tau$ , and at every iteration $k \ge 0$ :

computes $\alpha_k > 0$ with $\theta_n^{-1}\alpha_k^2 = (1 - \alpha_k)\gamma_k + \alpha_k\tau \equiv \gamma_{k+1}$ ;
sets $\lambda_k = \alpha_k\tau/\gamma_{k+1}$ , $\beta_k = \alpha_k\gamma_k/(\gamma_k + \alpha_k\tau)$ and $y_k = (1-\beta_k)x_k + \beta_k v_k$ ;
draws a fresh Gaussian direction $u_k$ , independent of the past, and computes $g_\mu(y_k)$ ;
sets $x_{k+1} = y_k - h_n B^{-1}g_\mu(y_k)$ and $v_{k+1} = (1-\lambda_k)v_k + \lambda_k y_k - (\theta_n/\alpha_k)B^{-1}g_\mu(y_k)$ .

Write $\phi_k = \mathbb E f(x_k)$ (expectation over $u_0, \dots, u_{k-1}$ ), $\psi_k = \prod_{i=0}^{k-1}(1-\alpha_i)$ and $C_k = 1 + \sum_{i=1}^{k-1}\prod_{j=k-i}^{k-1}(1-\alpha_j)$ for $k \ge 1$ , with $\psi_0 = 1$ and $C_0 = 0$ (p. 550).

Formalization targets

Goal: Theorem 9 (p. 549)

For all $k \ge 0$ ,

\phi_k - f^* \le \psi_k\Big[f(x_0) - f(x^*) + \frac{\gamma_0}{2}\|x_0 - x^*\|^2\Big] + \mu^2 L_1\Big(n + \frac{3(n+8)}{16}C_k\Big), \tag{62}

where

\psi_k \le \min\Big\{\Big(1 - \frac{\kappa^{1/2}}{4(n+4)}\Big)^k,\ \Big(1 + \frac{k}{8(n+4)}\sqrt{\frac{\gamma_0}{L_1}}\Big)^{-2}\Big\}, \qquad C_k \le \min\Big\{k,\ \frac{4(n+4)}{\kappa^{1/2}}\Big\}.

The two regimes are a rate $O(n^2/k^2)$ for convex $f$ and a linear rate with ratio $1 - \kappa^{1/2}/(4(n+4))$ for strongly convex $f$ , both up to a bias proportional to $\mu^2$ .

Milestones

In attack order: Lemma 1 (Gaussian moments, (16)–(17)); Theorem 3.1 (the bound (32) on the second moment of $g_0$ ); Theorem 1's (19), $|f_\mu - f| \le \frac{\mu^2}{2}L_1 n$ ; Eq. (12), $L_1(f_\mu) \le L_1(f)$ ; Lemma 5, the bound (37) on $\mathbb E_u\|g_\mu(x)\|_*^2$ in terms of $\nabla f_\mu(x)$ ; Eq. (21), $\nabla f_\mu = \mathbb E_u g_\mu$ ; and Eq. (11), $f_\mu \ge f$ for convex $f$ .

Significance

Theorem 9 shows that the $n$ -fold slowdown of gradient-free methods relative to their gradient counterparts survives acceleration: $\mathcal{FG}_\mu$ reaches accuracy $\epsilon$ in $O(n L_1^{1/2}R/\epsilon^{1/2})$ iterations for convex $f$ , against $O(nL_1R^2/\epsilon)$ for the non-accelerated random gradient method. The analysis also quantifies how small the finite-difference step $\mu$ must be for this to hold. The result is used as the baseline accelerated zeroth-order rate in later work.

The theorem is proved in the paper. As far as is known it has not been machine-checked, and Mathlib has no Gaussian smoothing, no random gradient-free oracle and no analysis of an accelerated method driven by random directions. A formal proof also settles the constant question raised by the printed $\theta_n$ (see below).

Difficulty

The deterministic fast gradient method is analysed by an estimate-sequence argument in which the gradient step is exact. Here the step uses $g_\mu(y_k)$ , which is an unbiased estimate of $\nabla f_\mu(y_k)$ and not of $\nabla f(y_k)$ , and whose second moment is of order $n\|\nabla f_\mu\|^2$ plus a bias term. The step size and the coupling parameter $\theta_n$ must absorb this second moment, and the argument must be run for $f_\mu$ rather than $f$ . The estimate sequence then has to be passed through expectations over the history $u_0, \dots, u_{k-1}$ , which requires the independence of $u_k$ from $x_k, v_k, y_k$ and integrability of every quantity involved. Transporting the result from $f_\mu$ back to $f$ uses (11) and (19), and requires that $f_\mu$ inherits strong convexity with the same parameter $\tau$ , a fact the paper uses without stating it.

Formalization scope

$E$ is an arbitrary finite-dimensional real inner product space (InnerProductSpace ℝ E, FiniteDimensional ℝ E, Borel measurable), $n$ is Module.finrank ℝ E, and the Gaussian is Mathlib's stdGaussian E. The operator $B$ is absorbed into the inner product, so $\nabla f$ is gradient f and $B^{-1}g_\mu$ is $\frac{f(x+\mu u)-f(x)}{\mu}u$ . This is not a restriction to $B = I$ on $\mathbb R^n$ . All expectations are Bochner integrals; under the hypotheses every integrand is integrable, so no integrability hypothesis is added.

The run is a structure over a probability space $(\Omega, \mathbb P)$ : directions $u_k$ that are measurable, mutually independent (iIndepFun) and standard Gaussian; deterministic sequences $\gamma, \alpha$ satisfying step a) as equations; and random points $x_k, v_k$ satisfying steps b)–d) for every outcome. The smoothing parameter satisfies $\mu \ge 0$ , and at $\mu = 0$ the oracle is $g_0$ . The goal pins $\theta = 1/(16(n+4)^2L_1)$ and $h = 1/(4(n+4)L_1)$ . $\psi_k$ and $C_k$ are definitions computed from $\alpha$ .

The constant $\theta_n$ . The paper prints $\theta_n = \frac{1}{16(n+1)^2L_1(f)}$ . The proof (pp. 549–550) needs $\frac{h_n}{4(n+4)} - \frac{h_n^2L_1}{2} = \frac{1}{32(n+4)^2L_1} = \frac{\theta_n}{2}$ , $\alpha_k \ge [\tau\theta_n]^{1/2} = \frac{\kappa^{1/2}}{4(n+4)}$ and $\theta_n^{1/2} = \frac{1}{4(n+4)L_1^{1/2}}$ , which hold only with $(n+4)$ . With the printed value $\theta_n$ is larger than the first inequality allows, and the argument does not go through. The mission therefore states Theorem 9 with $\theta_n = \frac{1}{16(n+4)^2L_1}$ ; all other constants are as printed.

Two trivializing formalizations are ruled out. First, the bound $C_k \le 4(n+4)/\kappa^{1/2}$ carries the hypothesis $\tau > 0$ : at $\tau = 0$ the paper's value is $+\infty$ , while Lean's division by zero would turn it into $C_k \le 0$ , which is false. $\psi_k$ and $C_k$ are definitions from the run, not free variables that only satisfy the bounds. Second, the oracle is the random finite difference along i.i.d. standard Gaussian directions, not the exact gradient (which would give Nesterov's deterministic method) and not an arbitrary direction sequence.

A complete development needs Gaussian integration by parts in an inner product space, moment bounds for $\|u\|$ , differentiation under the integral sign for $f_\mu$ , and conditional expectation along an i.i.d. sequence. The smoothing layer (Lemma 1, (11), (12), (19), (21), (32), (37)) is reusable for any zeroth-order method, and contributions of these components as separate lemmas are welcome.

Selected references

Yu. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17(2):527–566, 2017. https://doi.org/10.1007/s10208-015-9296-2
Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004 (Lemma 2.2.4 and Section 2.2.1, the estimate-sequence analysis the proof of Theorem 9 follows). https://doi.org/10.1007/978-1-4419-8853-9

14 thms4 active usersReviewed

Completed

Convex Optimization Optimization Probability·Captain: mikedeng1

Random Gradient-Free Minimization of Convex Functions II: Random Gradient Descent for Smooth and Strongly Convex ProblemsResearch Paper

Motivation

Many optimization problems in engineering, simulation-based design and machine learning give access to the objective only through its values: the function is computed by a black-box code, and derivatives are unavailable or too expensive to program. Zeroth-order (derivative-free) methods address this setting. Classical derivative-free methods (pattern search, Nelder–Mead, model-based trust regions) come with weak or no global complexity guarantees for convex problems.

Nesterov and Spokoiny (Found. Comput. Math. 17 (2017) 527–566) showed that replacing the gradient by a finite difference along a random Gaussian direction yields methods whose expected complexity is that of the corresponding gradient method multiplied by a factor proportional to the dimension. Their paper is a standard reference for zeroth-order convex optimization and for Gaussian smoothing, and its oracle and analysis are reused in bandit convex optimization, zeroth-order stochastic optimization (e.g. Ghadimi–Lan 2013) and derivative-free reinforcement learning.

This mission concerns Section 5 of the paper: the random gradient method $\mathcal{RG}_\mu$ for smooth convex functions and its linear rate for strongly convex ones.

Setting

Let $E$ be a real inner product space of finite dimension $n$ , with norm $\|\cdot\|$ . (The paper works with a space carrying an operator $B = B^* \succ 0$ and norm $\|x\| = \langle Bx, x\rangle^{1/2}$ ; choosing $\langle B\cdot,\cdot\rangle$ as the inner product gives exactly this setting, and the dual norm $\|\cdot\|_*$ becomes the norm of the Riesz representative.)

A function $f : E \to \mathbb R$ belongs to $C^{1,1}(E)$ with constant $L_1$ if it is differentiable and $\|\nabla f(x) - \nabla f(y)\| \le L_1\|x - y\|$ for all $x, y$ . It is strongly convex with parameter $\tau > 0$ if $f(y) \ge f(x) + \langle \nabla f(x), y - x\rangle + \frac{\tau}{2}\|y-x\|^2$ for all $x, y$ .

Let $u$ be a standard Gaussian vector of $E$ (coordinates in any orthonormal basis are independent $N(0,1)$ ). The Gaussian approximation of $f$ with parameter $\mu \ge 0$ is $f_\mu(x) = \mathbb E_u f(x + \mu u)$ , and the moments are $M_p = \mathbb E_u\|u\|^p$ . The random gradient-free oracle returns, for a sampled direction $u$ ,

B^{-1}g_\mu(x) = \frac{f(x+\mu u) - f(x)}{\mu}\, u \quad (\mu > 0), \qquad B^{-1}g_0(x) = f'(x,u)\, u,

and the symmetric oracle is $B^{-1}\hat g_\mu(x) = \frac{f(x+\mu u) - f(x - \mu u)}{2\mu}u$ .

Consider $f^* = \min_{x\in E} f(x)$ for a convex $f \in C^{1,1}(E)$ , assumed solvable with a minimizer $x^*$ , and $n \ge 2$ . The random gradient method $\mathcal{RG}_\mu$ (Eq. (54), p. 546) is:

Method $\mathcal{RG}_\mu$ : Choose $x_0 \in E$ . Iteration $k \ge 0$ . a). Generate $u_k$ and corresponding $g_\mu(x_k)$ . b). Compute $x_{k+1} = x_k - hB^{-1}g_\mu(x_k)$ .

The directions $u_0, u_1, \dots$ are independent standard Gaussian vectors, and $\phi_k = \mathbb E f(x_k)$ (with $\phi_0 = f(x_0)$ ).

Formalization targets

Goal: Theorem 8 (p. 546)

With step size $h = \frac{1}{4(n+4)L_1}$ and any $\mu \ge 0$ , for every $N \ge 0$ ,

\frac{1}{N+1}\sum_{k=0}^{N}(\phi_k - f^*) \le \frac{4(n+4)L_1\|x_0-x^*\|^2}{N+1} + \frac{9\mu^2(n+4)^2L_1}{25},

and, if $f$ is strongly convex with parameter $\tau > 0$ , then with $\delta_\mu = \frac{18\mu^2(n+4)^2}{25\tau}L_1$ ,

\phi_N - f^* \le \frac12 L_1\left[\delta_\mu + \left(1 - \frac{\tau}{8(n+4)L_1}\right)^{N}\big(\|x_0-x^*\|^2 - \delta_\mu\big)\right].

Both bounds are one theorem with one proof in the paper, so the goal states their conjunction, with every constant as printed.

Milestones

The milestones are the results the paper's proof of Theorem 8 rests on, in attack order:

Lemma 1 (p. 534): $M_p \le n^{p/2}$ for $p \in [0,2]$ and $n^{p/2} \le M_p \le (p+n)^{p/2}$ for $p \ge 2$ .
Theorem 3.1, (32) (p. 537): $\mathbb E_u\|g_0(x)\|_*^2 \le (n+4)\|\nabla f(x)\|_*^2$ at a point of differentiability.
Theorem 4.2, (35) (p. 538): $\mathbb E_u\|g_\mu(x)\|_*^2 \le \frac{\mu^2}{2}L_1^2(n+6)^3 + 2(n+4)\|\nabla f(x)\|_*^2$ , and the same with $\frac{\mu^2}{8}$ for $\hat g_\mu$ .
Eq. (21) (pp. 534–535): for $\mu > 0$ , $f_\mu$ is differentiable with $\nabla f_\mu(x) = \mathbb E_u B^{-1}g_\mu(x)$ .
Eq. (25) (p. 535): $\mathbb E_u \langle\nabla f(x), u\rangle u = \nabla f(x)$ , the $\mu = 0$ counterpart.
Convexity of $f_\mu$ (p. 533) and Eq. (11): $f \le f_\mu$ for convex $f$ .
Theorem 1, (19) (p. 534): $|f_\mu(x) - f(x)| \le \frac{\mu^2}{2}L_1 n$ .

Significance

The result. Theorem 8 shows that a method using two function values per iteration reaches accuracy $\epsilon$ on a smooth convex problem in $O(\frac{n}{\epsilon}L_1\|x_0 - x^*\|^2)$ iterations, and in $O(\frac{nL_1}{\tau}\ln\frac{L_1\|x_0-x^*\|^2}{\epsilon})$ iterations under strong convexity, provided $\mu$ is small enough. This is $n$ times the complexity of the deterministic gradient method, which is the natural price for replacing an $n$ -dimensional gradient by one directional estimate. The strongly convex bound makes explicit the bias floor $\frac12 L_1\delta_\mu$ caused by the finite-difference step, and shows that it vanishes for the limiting method $\mathcal{RG}_0$ .

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of it has a machine-checked proof. A formalization produces a reusable Gaussian-smoothing layer on Mathlib's stdGaussian (moments of the Gaussian norm, differentiation of $f_\mu$ under the integral, variance bounds of random oracles) and a complete expected-complexity proof of a randomized first-order method, in which the probabilistic structure (independent directions, iterates depending only on past directions, tower property) has to be handled explicitly.

Difficulty

The deterministic part of the argument is the textbook analysis of gradient descent. The difficulty is in the Gaussian facts it uses. The obvious bound on the oracle's second moment, $\mathbb E\langle\nabla f(x),u\rangle^2\|u\|^2 \le \|\nabla f(x)\|^2 M_4 \le (n+4)^2\|\nabla f(x)\|^2$ , loses a factor of $n$ and would give a quadratic dependence on dimension; the $(n+4)$ of (32) needs a sharper computation. The moment bounds of Lemma 1 for non-integer $p$ and the differentiation under the integral in (21) are measure-theoretic steps that Mathlib does not package. Finally, the step from per-iteration inequalities to bounds on $\phi_k$ requires conditioning on the past directions, which must be set up on a probability space carrying the whole sequence $u_0, u_1, \dots$ .

Formalization scope

$E$ is an arbitrary finite-dimensional real inner product space with MeasurableSpace and BorelSpace, $n$ is Module.finrank ℝ E, and $\nabla f$ is Mathlib's gradient. Expectations over $u$ are Bochner integrals against ProbabilityTheory.stdGaussian E. A run of $\mathcal{RG}_\mu$ lives on a probability space $(\Omega, P)$ : measurable directions $u_k$ , jointly independent (iIndepFun) with law stdGaussian E, iterates with $x_0$ deterministic and the update holding for every $k$ and outcome. $\phi_k$ is ∫ ω, f (x k ω) ∂P. The oracle is defined by cases, with $f'(x,u)u$ at $\mu = 0$ ( $f'(x,u)$ the one-sided directional derivative of Eq. (23), a Filter.limUnder, which equals fderiv ℝ f x u for differentiable $f$ ), so the goal covers every $\mu \ge 0$ as the paper claims. $L_1$ and $\tau$ are any constants satisfying the defining inequalities. The standing assumptions of Section 5 (convexity, a global minimizer $x^*$ , $n \ge 2$ ) and $L_1 > 0$ are explicit hypotheses; $n \ge 2$ is needed for the constant $9/25$ .

A trivializing formalization is ruled out: the oracle is the random finite difference along i.i.d. standard Gaussian directions, not the true gradient (which would be deterministic gradient descent), and every expectation in the statements is of a quantity that is integrable under the stated hypotheses, so no bound holds through a junk value of a non-integrable integral.

A complete development needs Gaussian moment computations in finite dimension, differentiation under the integral sign for $f_\mu$ , the variance bounds of the oracles, and a conditional-expectation argument for the iteration. The smoothing layer is reusable for the companion missions on random search for nonsmooth problems and on the accelerated random method, and for other zeroth-order methods. Contributions of any of the milestones, of general Gaussian-integrability lemmas, or of alternative proofs are welcome.

Selected references

Yu. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17(2):527–566, 2017. https://doi.org/10.1007/s10208-015-9296-2
S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4):2341–2368, 2013. https://doi.org/10.1137/120880811
Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

14 thms4 active usersReviewed

Completed

Convex Optimization Optimization Probability·Captain: mikedeng1

Random Gradient-Free Minimization of Convex Functions I: Random Search for Nonsmooth Convex ProblemsResearch Paper

Motivation

Many optimization problems in engineering, simulation-based design and machine learning give access to the values of an objective function but not to its gradient: the function is computed by a black-box program, by a simulator, or by a model whose derivatives are unavailable or too expensive. Zeroth-order (or derivative-free) methods use only function values. Classical direct-search methods of this kind usually come without complexity bounds.

Nesterov and Spokoiny (Found. Comput. Math. 17 (2017) 527–566) showed that a very simple randomized scheme has explicit, dimension-dependent worst-case complexity bounds. The idea is to replace the gradient by a finite difference of $f$ along a random Gaussian direction. The resulting oracle is an unbiased estimate of the gradient of a smoothed version of $f$ . Their analysis is the reference point for the later literature on zeroth-order stochastic optimization, bandit convex optimization and gradient-free training.

This mission covers the paper's result for nonsmooth convex problems over a closed convex set: the projected random search method $\mathcal{RS}_\mu$ and its convergence bound, Theorem 6.

Setting

Let $E$ be a real inner product space of finite dimension $n$ , with norm $\|\cdot\|$ . (The paper works with a space carrying a positive definite operator $B$ and the norm $\langle Bx, x\rangle^{1/2}$ . This is the same thing as an arbitrary finite-dimensional inner product space, with $B$ encoding the inner product, and the development is written in that generality.)

A function $f : E \to \mathbb R$ is Lipschitz continuous with constant $L_0 \ge 0$ if $|f(x) - f(y)| \le L_0 \|x - y\|$ for all $x, y$ . The paper calls this class $C^{0,0}(E)$ and writes $L_0(f)$ for the constant.

Let $u$ be a standard Gaussian vector in $E$ : its coordinates in any orthonormal basis are independent $N(0,1)$ variables. For $\mu \ge 0$ the Gaussian smoothing of $f$ is

f_\mu(x) = \mathbb E_u\, f(x + \mu u),

and the Gaussian moments are $M_p = \mathbb E_u \|u\|^p$ .

For $\mu > 0$ the random gradient-free oracle at $x$ draws $u$ and returns the vector

g_\mu(x) = \frac{f(x+\mu u) - f(x)}{\mu}\, u .

It costs two function values.

The problem is

f^* = \min_{x \in Q} f(x),

where $Q \subseteq E$ is closed and convex, $f$ is convex and Lipschitz, and $x^* \in Q$ is a minimizer. With $\pi_Q$ the Euclidean projection onto $Q$ , positive steps $h_0, h_1, \ldots$ and a starting point $x_0 \in Q$ , the random search method $\mathcal{RS}_\mu$ iterates

x_{k+1} = \pi_Q\big(x_k - h_k\, g_\mu(x_k)\big),

drawing a fresh independent Gaussian direction $u_k$ at every iteration. The iterates are random. Write $\phi_k = \mathbb E f(x_k)$ and $S_N = \sum_{k=0}^N h_k$ .

Formalization targets

Goal: Theorem 6

For every $N \ge 0$ ,

\frac{1}{S_N}\sum_{k=0}^{N} h_k(\phi_k - f^*) \le \mu L_0\, n^{1/2} + \frac{1}{S_N}\left[\frac12\|x_0 - x^*\|^2 + \frac{(n+4)^2}{2} L_0^2 \sum_{k=0}^{N} h_k^2\right].

The step sizes, the smoothing parameter and the horizon are left free, so every step-size rule in the paper follows from this one inequality. The constants are the paper's.

Milestones

The facts about smoothing and the oracle on which the goal rests, in the paper's order:

Lemma 1: $M_p \le n^{p/2}$ for $p \in [0,2]$ and $n^{p/2} \le M_p \le (p+n)^{p/2}$ for $p \ge 2$ .
Theorem 1 (18): $|f_\mu(x) - f(x)| \le \mu L_0 n^{1/2}$ .
Convexity of $f_\mu$ for convex $f$ .
Eq. (11): $f_\mu \ge f$ for convex $f$ .
Eq. (21): $\nabla f_\mu(x) = \mathbb E_u\, g_\mu(x)$ for $\mu > 0$ .
Theorem 4.1 (34): $\mathbb E_u \|g_\mu(x)\|^2 \le L_0^2 (n+4)^2$ .
Theorem 2 ( $\mu \ge 0$ ): $f(y) \ge f(x) - \mu L_0 n^{1/2} + \langle \nabla f_\mu(x), y - x\rangle$ for all $y$ , where at $\mu = 0$ the vector is the limiting $\nabla f_0(x) = \mathbb E_u[f'(x,u)\,u]$ of Eq. (24).

Significance

Theorem 6 shows that a method using only function values, with no subgradient, solves nonsmooth convex problems with the classical projected-subgradient guarantee. Two things change: $L_0^2$ is multiplied by $(n+4)^2$ , and a bias $\mu L_0 n^{1/2}$ appears, which can be made as small as desired. With suitable $\mu$ , $h_k$ and $N$ an $\epsilon$ -accurate expected value is reached in $O(n^2 L_0^2 R^2/\epsilon^2)$ oracle calls. The factor $n^2$ quantifies the cost of not having gradients. The same analysis carries over to stochastic objectives (the paper's Theorem 7).

The results are proved in the paper. As far as is known, none of them has a machine-checked proof. The mission produces a Lean development of Gaussian smoothing on an arbitrary finite-dimensional inner product space: the moment bounds, the approximation, convexity and gradient identities, and the oracle variance bound. On top of it sits the full convergence theorem for a randomized projected method, stated for the actual random process rather than for an idealized expectation recursion. The smoothing layer is reusable: the same facts underlie the smooth and accelerated random methods of the same paper and most Gaussian-smoothing analyses in zeroth-order optimization.

Difficulty

A plain subgradient analysis does not apply. The vector $g_\mu(x_k)$ is not a subgradient of $f$ , nor an unbiased estimate of one. It is an unbiased estimate of the gradient of a different function, $f_\mu$ , and its second moment grows with the dimension. The argument therefore has to move between $f$ and $f_\mu$ at exactly the right places, using properties of $f_\mu$ that hold for every nonsmooth Lipschitz $f$ .

Those properties are genuinely analytic. Differentiating $f_\mu$ requires differentiating a Gaussian integral of a function that need not be differentiable. The moment bounds need estimates of $\mathbb E\|u\|^p$ for real $p$ . In the probabilistic part, $x_k$ depends on $u_0, \ldots, u_{k-1}$ , and each one-step estimate has to be integrated using the independence of $u_k$ from the past. Mathlib provides the standard Gaussian measure and independence, but no Gaussian smoothing, no projection onto convex sets and no conditional-expectation argument for this kind of recursion.

Formalization scope

The space is E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E], and $n$ is Module.finrank ℝ E. No lower bound on $n$ is assumed. The Gaussian is ProbabilityTheory.stdGaussian E, and expectations are Bochner integrals against it. $f_\mu$ is the definition smoothing, $M_p$ is moment (with real exponent Real.rpow), and $g_\mu$ is oracle.

The projection is the relation IsMetricProjection Q y z ( $z \in Q$ and $z$ is a nearest point of $Q$ to $y$ ). The run is the predicate IsRandomSearchRun: directions $u_k : \Omega \to E$ on a probability space $(\Omega, P)$ , measurable, mutually independent (iIndepFun) and each with law stdGaussian E; a deterministic $x_0 \in Q$ ; and the update above for every $k$ and every outcome.

$\phi_k$ is $\int f(x_k)\,dP$ . The Lipschitz constant $L_0 \ge 0$ is any constant satisfying the Lipschitz inequality. It is an explicit hypothesis, because the paper's bound uses $L_0(f)$ , which presupposes $f \in C^{0,0}(E)$ . The smoothing parameter satisfies $\mu > 0$ and every step satisfies $h_k > 0$ .

Two trivializing formalizations are ruled out. First, an expectation of a non-integrable function would be $0$ as a Bochner integral; Lipschitz continuity of $f$ makes every expectation in the mission integrable, and no statement relies on the junk value. Second, a run whose directions are not independent standard Gaussians, or whose update uses a subgradient instead of the finite difference, is a different theorem (the projected subgradient method). The run predicate fixes the paper's process exactly. A run exists for every closed $Q$ containing $x_0$ (on the countable product of Gaussians), so the goal is not vacuous.

A complete development needs:

Gaussian integration by parts, or differentiation under the integral, for Lipschitz integrands;
moment estimates for the standard Gaussian norm;
existence and nonexpansiveness of projections onto closed convex sets;
an expectation argument for the random recursion.

The smoothing lemmas, the moment bounds and the projection facts are reusable beyond this mission. Contributions are welcome at every level: proofs of the milestones, general lemmas about stdGaussian and projections, and alternative proofs of Lemma 1 (for example through the chi distribution).

Selected references

Yu. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17(2):527–566, 2017. https://doi.org/10.1007/s10208-015-9296-2
Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
A. D. Flaxman, A. T. Kalai, H. B. McMahan, Online convex optimization in the bandit setting: gradient descent without a gradient, SODA 2005. https://arxiv.org/abs/cs/0408007
J. C. Duchi, M. I. Jordan, M. J. Wainwright, A. Wibisono, Optimal rates for zero-order convex optimization: the power of two function evaluations, IEEE Trans. Inf. Theory 61(5):2788–2806, 2015. https://arxiv.org/abs/1312.2139

14 thms4 active usersReviewed

Completed

Combinatorics Optimization Probability·Captain: mikedeng1

The Distributionally Robust Chance-Constrained Vehicle Routing Problem I: With a Subadditive Demand Estimator the Two-Index Vehicle Flow Formulation Is ExactResearch Paper

Motivation

The capacitated vehicle routing problem (CVRP) asks for delivery routes of minimum cost. Each route starts and ends at a depot, every customer is visited exactly once, and the demand served on a route does not exceed the vehicle capacity. The problem is central in logistics and one of the most studied problems in combinatorial optimization. Its standard exact methods are branch-and-cut algorithms built on the two-index vehicle flow formulation, a 0/1 program over arcs whose capacity constraints are the rounded capacity inequalities (RCIs); see Laporte, Nobert and Desrochers (1985) and Semet, Toth and Vigo (2014).

In practice customer demands are uncertain. A chance-constrained CVRP requires each route to respect its capacity with probability at least $1-\epsilon$ under a known distribution. That distribution is rarely known. Most solution methods also need independent demands. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) study the distributionally robust chance-constrained CVRP. There the chance constraint must hold for every distribution in an ambiguity set $\mathcal P$ of plausible distributions. The ambiguity set may contain dependent distributions and uncountably many of them, so it is not clear a priori that the problem can be solved by the usual branch-and-cut machinery. This mission formalizes the paper's answer to that question: its Theorem 1 and the counterexample that precedes it.

Setting

The graph is complete and directed. Its nodes are $V=\{0,\dots,n\}$ and its arcs are $A=\{(i,j)\in V\times V:i\neq j\}$ . Node $0$ is the depot and $V_C=\{1,\dots,n\}$ are the customers. There are $m$ vehicles, indexed by $K=\{1,\dots,m\}$ , each of capacity $Q>0$ . Traversing the arc $(i,j)$ costs $c(i,j)\ge 0$ ; costs may be asymmetric.

A route $\mathbf R_k=(R_{k,1},\dots,R_{k,n_k})$ is an ordered list of customers, with $R_{k,0}=R_{k,n_k+1}=0$ . A route set $\mathbf R=(\mathbf R_1,\dots,\mathbf R_m)\in\mathfrak P(V_C,m)$ partitions $V_C$ into $m$ nonempty ordered routes. Its cost is $c(\mathbf R)=\sum_{k}\sum_{l=0}^{n_k}c(R_{k,l},R_{k,l+1})$ .

The demand vector $\tilde{\boldsymbol q}\in\mathbb R^n$ is random. The ambiguity set $\mathcal P$ is a set of probability distributions of $\tilde{\boldsymbol q}$ and $\epsilon\in(0,1)$ is the risk level. The problem RVRP( $\mathcal P$ ) minimizes $c(\mathbf R)$ over route sets such that

\mathbb P\Big[\textstyle\sum_{i\in\mathbf R_k}\tilde q_i\le Q\Big]\ge 1-\epsilon\qquad\forall\,\mathbb P\in\mathcal P,\ \forall\,k\in K .

With $\mathbb Q\text{-VaR}_{1-\epsilon}[\tilde X]=\inf\{x:\mathbb Q[\tilde X\le x]\ge1-\epsilon\}$ , the demand estimator of the paper's Eq. (2) is

d_{\mathcal P}(S)=\max\left\{\left\lceil\frac1Q\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]\right\rceil,1\right\}\quad(S\neq\emptyset),\qquad d_{\mathcal P}(\emptyset)=0 .

The problem 2VF( $\mathcal P$ ) minimizes $\sum_{(i,j)\in A}c(i,j)x_{ij}$ over $x\in\{0,1\}^A$ with in- and out-degree $1$ at every customer and $m$ at the depot, and with the RCIs

\sum_{i\in V\setminus S}\sum_{j\in S}x_{ij}\ge d_{\mathcal P}(S)\qquad\forall\,S\subseteq V_C,\ S\neq\emptyset .

A route set induces the arc vector with $x_{ij}=1$ exactly when $(i,j)=(R_{k,l},R_{k,l+1})$ for some $k,l$ (the paper's Eq. (3)). The estimator satisfies the subadditivity condition (S) if $d_{\mathcal P}(S\cup T)\le d_{\mathcal P}(S)+d_{\mathcal P}(T)$ for all $S,T\subseteq V_C$ .

Formalization targets

Goal: Theorem 1

Assume $\tilde{\boldsymbol q}\ge\mathbf 0$ $\mathbb P$ -a.s. for all $\mathbb P\in\mathcal P$ , and assume $d_{\mathcal P}$ is real valued and satisfies (S). Then:

\begin{aligned} &\text{(i)}\ \ \mathbf R \text{ feasible in RVRP}(\mathcal P)\ \Longrightarrow\ x(\mathbf R)\text{ feasible in 2VF}(\mathcal P),\ \ c(x(\mathbf R))=c(\mathbf R);\\ &\text{(ii)}\ \ x\text{ feasible in 2VF}(\mathcal P)\ \Longrightarrow\ x=x(\mathbf R)\text{ for an RVRP}(\mathcal P)\text{-feasible }\mathbf R,\text{ unique up to reordering routes},\ c(x)=c(\mathbf R). \end{aligned}

Milestones

The chance constraint $\mathbb Q[\tilde X\le\tau]\ge1-\epsilon$ is equivalent to $\mathbb Q\text{-VaR}_{1-\epsilon}[\tilde X]\le\tau$ (p. 720).
Eq. (1): a route satisfies its robust chance constraint if and only if the worst-case VaR of its cumulative demand is at most $Q$ .
Example 1: an instance with two customers where a route set is RVRP( $\mathcal P$ )-feasible, yet its induced flow violates the RCI for $S=\{1,2\}$ , since $d_{\mathcal P}(\{1,2\})\ge3$ .
Example 1 (continued): on that instance $d_{\mathcal P}$ violates (S).
Theorem 1 (i) and 6. Theorem 1 (ii), stated separately.

Significance

Theorem 1 separates the modeling question from the algorithmic one. Whenever the ambiguity set yields a subadditive estimator, the distributionally robust CVRP is solved exactly by a two-index flow branch-and-cut. The only change from the deterministic case is the right-hand side $d_{\mathcal P}(S)$ of the RCIs, however many distributions $\mathcal P$ contains. The companion missions of this series show that (S) holds for every moment ambiguity set (Theorem 2 of the paper) and compute $d_{\mathcal P}$ for several classes of such sets. Example 1 shows that the hypothesis cannot be dropped: ambiguity sets that pin down each customer's marginal distribution break the equivalence.

The paper's proofs are in its online supplement; no machine-checked version of these statements exists. Formalizing them produces a checked reduction between a stochastic routing model and an integer program. It also produces reusable definitions of route sets, induced arc flows and RCIs over directed graphs with a depot.

Difficulty

Direction (ii) is a graph decomposition. A 0/1 vector with the prescribed degrees splits into $m$ depot cycles plus possibly depot-free subtours. The RCIs, through the $\max\{\cdot,1\}$ in $d_{\mathcal P}$ , must exclude the subtours, and the RCI on the customers of a single route must enforce that route's chance constraint. Uniqueness up to reordering requires that directed routes are recovered from arcs.

Direction (i) is where (S) enters. The naive argument bounds the number of vehicles entering $S$ by $d_{\mathcal P}(S)$ directly from the chance constraints. It fails because the chance constraints control each route separately, while $d_{\mathcal P}(S)$ looks at the joint worst case of the demands in $S$ ; Example 1 is exactly this failure. A set $S$ is typically visited by several routes, each covering only part of it. Relating the per-route guarantees to the joint quantity $d_{\mathcal P}(S)$ needs both hypotheses of the theorem: nonnegative demands and (S).

Formalization scope

Customers are Fin n (0-based; the paper's customer $i$ is i - 1). Nodes are Fin (n+1) with the depot 0 and customer i at i.succ, and vehicles are Fin m. A route set is R : Fin m → List (Fin n): every route is nonempty and the concatenated routes are a permutation of all customers. Arc vectors are ℕ-valued functions on ordered node pairs, with values in $\{0,1\}$ and the non-arcs $(i,i)$ fixed to $0$ .

Distributions are measures on Fin n → ℝ, and the ambiguity set is a set of probability measures. Chance constraints are written ENNReal.ofReal (1 - ε) ≤ P {q | …}. Value-at-risk is the published MultistageStochastic.valueAtRisk at level 1 - ε. The worst-case VaR is a real sSup and $d_{\mathcal P}$ is integer valued.

Two conventions implicit on the page are explicit hypotheses:

$Q>0$ , because (2) divides by $Q$ ;
boundedness of the VaR values for every customer set, which encodes the paper's declaration $d_{\mathcal P}:2^{V_C}\to\mathbb R_+$ .

A real sSup of an unbounded set is $0$ in Lean. Without the boundedness hypothesis every such estimator would silently equal $1$ and (ii) would fail. For an empty ambiguity set the Lean estimator equals $1$ on nonempty sets, as the paper's does.

The RCIs range over all nonempty customer sets with the depot on the outside. The estimator keeps the ceiling and the $\max\{\cdot,1\}$ . 2VF feasibility mentions neither routes nor chance constraints. RVRP feasibility does not mention $d_{\mathcal P}$ . A formalization in which either side refers to the other, or in which $d_{\mathcal P}$ drops the $\max\{\cdot,1\}$ , is not this theorem.

Useful contributions include lemmas on the decomposition of degree-constrained 0/1 arc vectors into depot cycles, monotonicity of VaR under almost-sure ordering, and the CDF right-continuity behind milestone 1.

Related platform work: SupplyChainTheory_vrp formalizes a different, symmetric, unit-demand VRP and is not reused.

Selected references

S. Ghosal, W. Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Operations Research 68(3):716–732, 2020. https://doi.org/10.1287/opre.2019.1924
G. Laporte, Y. Nobert, M. Desrochers, Optimal routing under capacity and distance restrictions, Operations Research 33(5):1050–1073, 1985. https://doi.org/10.1287/opre.33.5.1050
F. Semet, P. Toth, D. Vigo, Classical exact algorithms for the capacitated vehicle routing problem, in P. Toth, D. Vigo (eds.), Vehicle Routing: Problems, Methods, and Applications, 2nd ed., SIAM, 2014, 37–57. https://doi.org/10.1137/1.9781611973594.ch2
J. Lysgaard, A. N. Letchford, R. W. Eglese, A new branch-and-cut algorithm for the capacitated vehicle routing problem, Mathematical Programming 100(2):423–445, 2004. https://doi.org/10.1007/s10107-003-0481-8

12 thms4 active usersReviewed

Completed

Bandit Algorithms Machine Learning Probability+1·Captain: mikedeng1

Optimal Best Arm Identification with Fixed Confidence III: δ-PAC Guarantee of Chernoff's Stopping Rule for Bernoulli BanditsResearch Paper

Motivation

In best arm identification with fixed confidence, a learner samples $K$ unknown distributions ("arms") one at a time, and must eventually stop and name the arm with the largest mean, with an error probability at most a prescribed risk $\delta$ , while using as few samples as possible. The problem goes back to the sequential design of experiments (Chernoff, 1959; Even-Dar, Mannor and Mansour, 2006) and underlies adaptive A/B testing, clinical trial design and hyperparameter selection.

Any fixed-confidence strategy consists of three parts: a sampling rule, a stopping rule and a decision rule. Garivier and Kaufmann (arXiv:1602.04589, COLT 2016) proposed the Track-and-Stop strategy, the first shown to match the asymptotic lower bound on the expected sample complexity. Its stopping rule is a generalized likelihood ratio (GLR) test, Chernoff's stopping rule. Its correctness, the guarantee that the recommended arm is wrong with probability at most $\delta$ , must hold whatever the sampling rule, which is what allows the sampling rule to be tuned freely for efficiency. This mission formalizes that guarantee for Bernoulli arms, Theorem 10 of the paper, with its explicit threshold $\beta(t,\delta) = \log(2t(K-1)/\delta)$ .

Setting

The arms are $\mathcal A = \{1,\dots,K\}$ . A Bernoulli bandit model is a mean vector $\boldsymbol\mu = (\mu_1,\dots,\mu_K) \in [0,1]^K$ : pulling arm $a$ returns reward $1$ with probability $\mu_a$ and $0$ otherwise, independently of the past. The class $\mathcal S$ contains the models with a unique optimal arm $a^*(\boldsymbol\mu)$ , i.e. $\mu_{a^*} > \mu_i$ for all $i \ne a^*$ .

At round $t$ the learner chooses an arm $A_t$ as a (possibly randomized) function of the past observations and observes a reward $X_t$ . Write $N_a(t)$ for the number of pulls of arm $a$ among the first $t$ rounds, $s_a(t)$ for the number of those pulls that returned $1$ , and $\hat\mu_a(t) = N_a(t)^{-1}\sum_{s \le t} X_s \mathbb 1\{A_s = a\}$ for the empirical mean. The likelihood of arm $a$ 's observations under mean $u$ is $p_u(\underline X^a_{N_a(t)}) = u^{s_a(t)}(1-u)^{N_a(t)-s_a(t)}$ .

The GLR statistic for "arm $a$ is at least as good as arm $b$ " is

Z_{a,b}(t) = \log \frac{\max_{\mu'_a \ge \mu'_b} p_{\mu'_a}(\underline X^a_{N_a(t)})\, p_{\mu'_b}(\underline X^b_{N_b(t)})}{\max_{\mu'_a \le \mu'_b} p_{\mu'_a}(\underline X^a_{N_a(t)})\, p_{\mu'_b}(\underline X^b_{N_b(t)})}.

Chernoff's stopping rule with exploration rate $\beta(t,\delta)$ is

\tau_\delta = \inf\{t \ge 1 : \exists a \in \mathcal A,\ \forall b \ne a,\ Z_{a,b}(t) > \beta(t,\delta)\},

and the decision rule recommends $\hat a_{\tau_\delta} \in \operatorname{argmax}_a \hat\mu_a(\tau_\delta)$ .

The Krichevsky–Trofimov (KT) distribution on binary sequences $x \in \{0,1\}^n$ is $\mathrm{kt}(x) = \int_0^1 \big(\pi\sqrt{u(1-u)}\big)^{-1} p_u(x)\,\mathrm du$ , the Bernoulli likelihood mixed over the Beta $(1/2,1/2)$ prior.

Formalization targets

Goal: Theorem 10

For every $\delta \in (0,1)$ , every sampling strategy, and the threshold $\beta(t,\delta) = \log\big(2t(K-1)/\delta\big)$ ,

\forall \boldsymbol\mu \in \mathcal S,\qquad \mathbb P_{\boldsymbol\mu}\big(\tau_\delta < \infty,\ \hat a_{\tau_\delta} \ne a^*\big) \le \delta .

Milestone: Lemma 11 (Willems, Shtarkov and Tjalkens, 1995)

$\mathrm{kt}$ is a probability law on $\{0,1\}^n$ , and for $n \ge 1$ ,

\sup_{x\in\{0,1\}^n}\ \sup_{u\in[0,1]} \frac{p_u(x)}{\mathrm{kt}(x)} \le 2\sqrt n .

Milestone: the pairwise crossing bound of Appendix C.1

With $T_{a,b} = \inf\{t : Z_{a,b}(t) > \beta(t,\delta)\}$ , for all arms with $\mu_a < \mu_b$ ,

\mathbb P_{\boldsymbol\mu}(T_{a,b} < \infty) \le \frac{\delta}{K-1}.

Significance

Theorem 10 decouples correctness from efficiency. Because the guarantee holds for every sampling strategy, any sampling rule, including the C-Tracking and D-Tracking rules of Track-and-Stop, the uniform rule, or a heuristic, inherits $\delta$ -correctness as soon as it is paired with Chernoff's stopping rule at this threshold. The asymptotic optimality result of the paper (Theorem 14) then only has to control the sample complexity. The threshold is explicit, with no unspecified constant, in contrast to the deviational threshold of Proposition 12.

The result is proved in the paper, in Appendix C.1, and rests on Lemma 11, which the paper quotes from the universal coding literature without proof. As far as the platform's catalog shows, none of these results is formalized. The platform holds a machine-checkable statement of the analogous result for Gaussian arms with the Lattimore–Szepesvári threshold (BanditAlgorithm.chernoff_stopping_rule_sound, Lemma 33.7 of Bandit Algorithms), which is a different model and a different threshold. Formalizing Theorem 10 adds a proof of Lemma 11 (the KT regret bound, reusable in information theory and universal prediction), the Bernoulli GLR statistic, and a change of measure from the true bandit law to a Bayesian mixture law on the trajectory space.

Difficulty

The obvious approach bounds, for each fixed $t$ , the probability that $Z_{a,b}(t)$ exceeds $\beta(t,\delta)$ by a concentration inequality and sums over $t$ . This fails: the sampling strategy is arbitrary and adaptive, so $N_a(t)$ and $N_b(t)$ are random and depend on the past rewards, and a fixed-sample-size deviation bound does not apply; a union bound over the possible values of the counts loses more than the threshold allows. The maximum likelihood in the numerator of $Z_{a,b}$ is also not a probability density, so the likelihood ratio cannot directly be read as a change of measure. The argument must control the whole trajectory law under an arbitrary randomized policy, and must handle empty samples (an arm never pulled contributes likelihood $1$ ) and the boundary means $0$ and $1$ .

Formalization scope

The formalization is in Lean 4 with Mathlib and reuses the platform's canonical bandit model: StochasticBandit, BanditPolicy (a Markov kernel per round from the observed history to the next arm, so randomized strategies are included), banditTrajMeasure (the law of the infinite trajectory, where coordinate $s$ is round $s+1$ ) and IsSoundBAI from BanditTrajectory; bernoulliBandit from bernoulliRelativeEntropy; and only the pull counts trajPullCount and empirical means trajEmpiricalMean from TrackAndStop. The Gaussian GLR and threshold of TrackAndStop are not used.

Conventions committed to:

Arms are Fin K. Bernoulli means range over $[0,1]$ , degenerate laws included; the paper's exponential-family mean space is $(0,1)$ , so the $[0,1]$ statement implies the paper's.
$Z_{a,b}(t)$ is defined as the ratio of the two maxima over $[0,1]^2$ , not by the closed form (7), which holds only when $\hat\mu_a(t) \ge \hat\mu_b(t)$ . Both maxima are attained and positive.
The stopping rule ranges over $t \ge 1$ ; at $t = 0$ there is no observation and the paper's $\beta(0,\delta) = \log 0$ is undefined. $\tau_\delta = \infty$ when the rule never fires.
The decision rule is quantified: the goal holds for every recommendation that maximizes the empirical mean at $\tau_\delta$ , whatever the tie-breaking.
Probabilities of events are outer measures under the trajectory law; no measurability is assumed.
$K \ge 1$ only. For $K = 1$ the statement is trivially true (no suboptimal arm).

Disclosed deviations from the page: Lemma 11's ratio bound is stated for $n \ge 1$ , since at $n = 0$ the printed bound reads $1 \le 0$ ; the use of the lemma in Appendix C.1 is unaffected. Appendix C.1 calls the result "Proposition 10" (a slip for Theorem 10) and prints the KT density as $1/\sqrt{\pi u(1-u)}$ (a slip for $1/(\pi\sqrt{u(1-u)})$ of Lemma 11, which is the normalized one); the formalization follows Lemma 11.

A trivializing formalization is ruled out: stating the result for Gaussian arms or with the Lattimore–Szepesvári threshold is the platform's existing Lemma 33.7 and is not Theorem 10, and a free decision rule without the argmax hypothesis would make the claim false rather than faithful.

Contributions welcome: a proof of Lemma 11; a change-of-measure lemma for banditTrajMeasure under a mixture of environments; and the union-bound reduction from the goal to the pairwise claim.

Selected references

A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016 (JMLR W&CP 49), arXiv:1602.04589v2, 2016. https://arxiv.org/abs/1602.04589
F. M. J. Willems, Y. M. Shtarkov, T. J. Tjalkens, The context-tree weighting method: basic properties, IEEE Transactions on Information Theory 41(3), 1995. https://doi.org/10.1109/18.382012
R. Krichevsky, V. Trofimov, The performance of universal encoding, IEEE Transactions on Information Theory 27(2), 1981. https://doi.org/10.1109/TIT.1981.1056331
H. Chernoff, Sequential design of experiments, Annals of Mathematical Statistics 30(3), 1959. https://doi.org/10.1214/aoms/1177706205
T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 33. https://doi.org/10.1017/9781108571401

10 thms4 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Optimization·Captain: mikedeng1

Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders IV: A Truthful Value-Query Mechanism for Subadditive BiddersResearch Paper

Motivation

In a combinatorial auction a seller offers several indivisible items at once, and bidders value bundles of items rather than items one at a time. Allocating the items to maximize total value is the central optimization problem of the area, and it arises in spectrum licensing, procurement and transport contracting (Cramton, Shoham and Steinberg, Combinatorial Auctions, MIT Press, 2006). Two obstacles meet. Computationally, a valuation has $2^m$ numbers, so an algorithm can only query it, and even then optimization is hard. Strategically, the valuations are private: a bidder reports whatever maximizes its own utility, so an algorithm that is a good approximation on true inputs may be useless on reported ones.

The classical answer to the strategic obstacle is the VCG payment scheme, which makes truthful reporting a dominant strategy but requires the exact optimum. Nisan and Ronen (2007) showed that an approximation algorithm becomes truthful under VCG payments essentially only when it is maximal in range: it fixes a restricted set of allocations in advance and optimizes exactly over that set. Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010, §5) give such an algorithm for complement-free (subadditive) bidders that uses only value queries and loses a factor of order $\sqrt m$ . For general valuations in the value-query model the paper cites a lower bound of order $m/\log m$ (Dobzinski and Schapira, working paper 2005; Blumrosen and Nisan, Hebrew University Discussion Paper 381, 2005; see the paper's references [7] and [2]), and the same paper (Theorem 6.1) shows that even XOS bidders cannot be approximated within $m^{1/2-\epsilon}$ with polynomially many value queries.

Setting

A set $M=\{1,\dots,m\}$ of items is sold to $n$ bidders. Bidder $i$ has a valuation $v_i$ that assigns a real number $v_i(S)$ to every bundle $S\subseteq M$ . Throughout, valuations are normalized, $v_i(\emptyset)=0$ , and monotone, $S\subseteq T\Rightarrow v_i(S)\le v_i(T)$ . A valuation is complement free (CF) if $v(S\cup T)\le v(S)+v(T)$ for all bundles $S,T$ . An allocation $A=(A_1,\dots,A_n)$ gives the bidders pairwise disjoint bundles (items may stay unallocated), and its social welfare is $\sum_i v_i(A_i)$ .

The mechanism receives reports $b=(b_1,\dots,b_n)$ and runs the following algorithm $\mathrm{ALG}$ :

query $b_i(M)$ and $b_i(\{j\})$ for every bidder $i$ and item $j$ ;
compute a maximum-weight matching $P$ in the complete bipartite graph between items and bidders, where the edge between item $j$ and bidder $i$ costs $b_i(\{j\})$ ;
if the bidder $t$ maximizing $b_i(M)$ has $b_t(M)$ strictly larger than the weight $|P|$ , give all items to $t$ ; otherwise give every item matched by $P$ to its matched bidder.

Its range $R$ is the set of allocations that give all of $M$ to one bidder, together with the allocations in which every bidder receives at most one item. Under VCG payments bidder $i$ receives $\sum_{k\ne i}b_k(\mathrm{ALG}(b)_k)$ , so its utility is $v_i(\mathrm{ALG}(b)_i)+\sum_{k\ne i}b_k(\mathrm{ALG}(b)_k)$ . The mechanism is incentive compatible on a class of valuations if no bidder can raise its utility by misreporting within that class, whatever the others report.

Formalization targets

Goal: Theorem 5.1 (p. 11)

For every choice of the maximum-weight matching and of the top bidder as functions of the reports, for every profile $v$ of normalized, monotone, CF valuations and every allocation $O$ ,

\sum_{i=1}^n v_i(O_i)\;\le\;2\sqrt m\,\sum_{i=1}^n v_i\big(\mathrm{ALG}(v)_i\big),

and the mechanism $(\mathrm{ALG},\text{VCG payments})$ is incentive compatible on the CF valuations.

Milestones, in attack order

§5.1, VCG. Welfare maximization with Groves payments is incentive compatible (a published platform theorem, AGT.vcg_incentive_compatible).
§5.1, maximal in range. Any allocation rule that optimizes reported welfare exactly over a fixed range is incentive compatible under VCG payments on the same domain.
ALG is maximal in range with range $R$ on normalized reports.
The CF single-item bound. For a CF valuation and $c\in T$ maximizing $v(\{j\})$ over $T$ : $v(T)\le\sum_{j\in T}v(\{j\})\le|T|\,v(\{c\})$ .
First case. If bidders with $|O_i|\ge\sqrt m$ carry at least half the welfare of $O$ , then $\sum_i v_i(O_i)\le 2\sqrt m\,v_t(M)$ for the top bidder $t$ .
Second case. Otherwise some allocation in which every bidder gets at most one item has welfare at least $\sum_i v_i(O_i)/(2\sqrt m)$ .

Significance

The theorem shows that, for subadditive bidders, the $\sqrt m$ barrier known for general valuations can be matched by a truthful mechanism that asks each bidder only $m+1$ value queries. It is one of the early examples of maximal-in-range mechanism design, a template later used for many truthful approximation mechanisms in combinatorial auctions, and it sits against Theorem 6.1 of the same paper, which shows that for XOS bidders no value-query algorithm with polynomially many queries does better than $m^{1/2-\epsilon}$ .

The result is proved in the paper. What this mission adds is a machine-checked proof: a formal model of VCG-based mechanisms over a restricted range, a proof that the §5.2 algorithm is maximal in range for every tie-breaking of its two optimization steps, and the explicit constant $2$ in the $O(\sqrt m)$ bound. To our knowledge neither half of Theorem 5.1 is formalized elsewhere; the general VCG theorem exists on the platform in the setting of arbitrary outcome sets.

Difficulty

The approximation argument partitions the bidders of a reference allocation by whether their bundles have at least $\sqrt m$ items, and the two cases need different facts: disjointness bounds the number of large bundles by $\sqrt m$ , and subadditivity bounds each small bundle by its size times its best item. A naive transcription breaks at degenerate inputs: the page divides by $|T_i|$ and writes strict inequalities, both of which fail when a bundle is empty or all values are zero, so the formal statement must be organized around non-strict bounds.

Incentive compatibility has a different obstacle. It holds only if the allocation rule depends on the reports alone and optimizes exactly over its range, including at ties between the grand bundle and the matching. The matching and the top bidder are not unique, so the proof must work for an arbitrary but fixed tie-breaking, and the welfare of the matching allocation must be identified with the matching weight, which uses normalization of every bidder who receives nothing.

Formalization scope

Bidders are Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. Normalization and monotonicity (the paper's standing assumptions, p. 1) and complement freedom are hypotheses; IsCFValuation bundles all three. An allocation is a family of pairwise disjoint bundles; unallocated items are allowed. A matching is a partial map Fin m → Option (Fin n) with no bidder matched twice.

Conventions the formalization commits to:

Explicit constant. The paper writes $O(\sqrt m)$ ; its proof yields $2\sqrt m$ (both cases end with $|OPT|/(2\sqrt m)$ ), and the goal states $2\sqrt m$ with Real.sqrt m.
Oracles and ties. The maximum-weight matching and the top bidder enter as functions mat, top of the report profile, each with a specification hypothesis; the goal is stated for every such pair. The algorithm reads only the reports; the tie between $b_t(M)$ and $|P|$ goes to the matching, as on the page.
Payments. The mechanism pays each bidder $\sum_{k\ne i}b_k(\cdot)$ , the paper's convention (footnote 2, p. 11); incentive compatibility is stated on the CF domain, the paper's. The local definition mirrors AGT.MechIncentiveCompatible on outcomes $a\mapsto v_i(a_i)$ .
Reference allocation. The approximation is stated against every allocation $O$ , not only an optimal one; this is equivalent and avoids a junk maximum.
Printed slips. The strict inequalities and the division by $|T_i|$ in the second case are replaced by non-strict, multiplied forms; the first case concludes for a bidder maximizing $v_i(M)$ rather than $v_i(O_i)$ .
Degenerate sizes. At $m=0$ everything is zero and the bound holds trivially; with $n=0$ no top-bidder rule exists.
Out of scope. "In polynomial time" is a running-time claim and is not modelled.

A trivializing formalization is ruled out: the ratio is the explicit $2\sqrt m$ rather than an existential constant, incentive compatibility is over the full CF domain (not additive reports only) for a rule that cannot see true valuations, and the rules mat, top are satisfiable (a maximum over the finitely many matchings exists; a top bidder exists when $n\ge1$ ).

Useful infrastructure: finite maximum-weight matchings on complete bipartite graphs, subadditivity bounds over Finset sums, and a reusable lemma that maximal-in-range rules with VCG payments are truthful. Contributions of any milestone are welcome; milestones 2 and 4 are self-contained.

Selected references

S. Dobzinski, N. Nisan, M. Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Mathematics of Operations Research 35(1):1–13, 2010. https://doi.org/10.1287/moor.1090.0436
N. Nisan, A. Ronen, Computationally Feasible VCG Mechanisms, Journal of Artificial Intelligence Research 29:19–47, 2007. https://doi.org/10.1613/jair.2046
S. Dobzinski, M. Schapira, Optimal Upper and Lower Approximation Bounds for k-Duplicates Combinatorial Auctions, working paper, The Hebrew University of Jerusalem, 2005 (reference [7] of the paper).
L. Blumrosen, N. Nisan, On the Computational Power of Iterative Auctions I: Demand Queries, Discussion Paper 381, Center for the Study of Rationality, The Hebrew University of Jerusalem, 2005 (reference [2] of the paper).
N. Nisan, Introduction to Mechanism Design (for Computer Scientists), in N. Nisan, T. Roughgarden, E. Tardos, V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, pp. 209–242.
P. Cramton, Y. Shoham, R. Steinberg (eds.), Combinatorial Auctions, MIT Press, 2006.

8 thms4 active usersReviewed

Completed

Control Theory Dynamic Programming Optimization·Captain: mikedeng1

Robust Control of Markov Decision Processes with Uncertain Transition Matrices 2: The Robust Bellman Recursion for Discounted Infinite-Horizon MDPsResearch Paper

Motivation

A Markov decision process (MDP) is solved by dynamic programming only when its transition probabilities are known. In practice they are estimated from data, and the optimal policy of the estimated model can perform badly on the true one. Nilim and El Ghaoui (Oper. Res. 53(5), 2005) showed that, when the uncertainty on the transition matrices has a product ("rectangular") structure, the robust problem, in which the controller minimises the worst expected cost over all admissible transition matrices, keeps the structure of dynamic programming. The robust Bellman operator replaces the expectation of the next-stage value by a support function of the uncertainty set. That operator is the basis of later work on robust MDPs and robust reinforcement learning.

Timeline:

Bagnell, Ng and Schneider (2001) considered the max–min value $\psi_\infty(\Pi, \mathcal T)$ and stated without proof that it is computed by the recursion below.
Iyengar (Math. Oper. Res. 30(2), 2005; technical report 2003) independently proved the robust Bellman recursion for the discounted infinite-horizon case.
Nilim and El Ghaoui (2005), Theorem 3, prove the recursion and perfect duality of the stationary discounted game. This mission formalizes that theorem.

Setting

The state space is $\mathcal X = \{1,\dots,n\}$ and the action set $\mathcal A$ is finite and nonempty. Each state–action pair has a cost $c(i,a) \ge 0$ , and costs are discounted by a factor $\nu \in [0,1)$ : the cost at stage $t$ is $\nu^t c(i,a)$ .

Write $\Delta_n = \{p \in \mathbb R^n_+ : p^T\mathbf 1 = 1\}$ for the probability simplex. For each action $a$ and state $i$ a nonempty set $\mathcal P_i^a \subseteq \Delta_n$ is given. It is the set of distributions of the next state that nature may use from state $i$ under action $a$ . No convexity or closedness is assumed. Uncertainty is rectangular: the admissible transition matrices for action $a$ form the product $\mathcal P^a = \mathcal P_1^a \times \cdots \times \mathcal P_n^a$ , so every row is chosen independently.

A stationary control policy $\pi = (\mathbf a, \mathbf a, \dots)$ applies one decision rule $\mathbf a : \mathcal X \to \mathcal A$ at every stage; $\Pi_s$ is the set of them. A stationary policy of nature $\tau \in \mathcal T_s$ fixes one matrix $P^a \in \mathcal P^a$ for each action and uses it forever. Nature chooses after the controller.

From an initial state $i_0$ , the state distribution evolves as $\mu_0 = e_{i_0}$ , $\mu_{t+1}(j) = \sum_i \mu_t(i) P^{\mathbf a(i)}(i,j)$ . The discounted cost is

C_\infty(\pi,\tau) = \sum_{t\ge 0} \nu^t \sum_i \mu_t(i)\, c(i,\mathbf a(i)).

The support function of a set $\mathcal P$ is $\sigma_{\mathcal P}(v) = \sup\{p^T v : p \in \mathcal P\}$ . The robust Bellman operator $g$ and, for a stationary policy $\pi$ , the robust evaluation operator $g_\pi$ act on $v \in \mathbb R^n$ by

g(v)_i = \min_{a\in\mathcal A}\big(c(i,a) + \nu\,\sigma_{\mathcal P_i^a}(v)\big), \qquad g_\pi(v)_i = c(i,\mathbf a(i)) + \nu\,\sigma_{\mathcal P_i^{\mathbf a(i)}}(v).

The two values of the game are

\phi_\infty(\Pi_s,\mathcal T_s) = \min_{\pi\in\Pi_s}\sup_{\tau\in\mathcal T_s} C_\infty(\pi,\tau), \qquad \psi_\infty(\Pi_s,\mathcal T_s) = \sup_{\tau\in\mathcal T_s}\min_{\pi\in\Pi_s} C_\infty(\pi,\tau).

Formalization targets

Goal: Theorem 3 (Robust Bellman Recursion)

There is a unique $v \in \mathbb R^n$ with $v = g(v)$ , i.e.

v(i) = \min_{a\in\mathcal A}\big(c(i,a) + \nu\,\sigma_{\mathcal P_i^a}(v)\big), \quad i \in \mathcal X, \tag{19}

value iteration $v_{k+1} = g(v_k)$ converges to $v$ from every starting vector (20), and

\phi_\infty(\Pi_s,\mathcal T_s) = v(i_0) = \psi_\infty(\Pi_s,\mathcal T_s).

In addition, every policy that picks a minimising action in (19) is optimal (21), every nature policy whose rows attain $\sigma_{\mathcal P_i^a}(v)$ is optimal for nature (22), and for each stationary $\pi$ the worst-case cost $\sup_\tau C_\infty(\pi,\tau)$ is $v^\pi(i_0)$ , where $v^\pi$ is the unique fixed point of $g_\pi$ (23).

Milestones

Lemma 2 (corrected): for a nondecreasing sup-norm contraction $g$ and $q \ge 0$ , the program $\max q^T v$ s.t. $v \le g(v)$ has value $q^T v_\infty$ at the fixed point $v_\infty$ , every feasible $v$ satisfies $v \le v_\infty$ , and $v_\infty$ is the unique optimizer when $q > 0$ .
The operators $g$ of (29) and $g_\pi$ of (30) are nondecreasing and $\nu$ -Lipschitz in $\|\cdot\|_\infty$ .
(26): $C_\infty(\pi,\tau) = \max\{v(i_0) : v(i) \le c(i,\mathbf a(i)) + \nu \sum_j P^{\mathbf a(i)}(i,j) v(j)\}$ .
(28) ⇒ (23): $\sup_{\tau\in\mathcal T_s} C_\infty(\pi,\tau) = v^\pi(i_0)$ .
(27) ⇒ (19): $\psi_\infty(\Pi_s,\mathcal T_s) = v(i_0)$ .

Significance

The theorem makes the robust discounted problem as tractable as the nominal one. The optimal robust policy is stationary, deterministic and computed by value iteration. Each iteration evaluates one support function per state–action pair, and the paper computes these efficiently for likelihood and entropy uncertainty sets (§§5–6). Perfect duality means that the order of play does not change the value: announcing the policy to an adversarial nature costs nothing. The sequel in this series (Theorem 4) uses Theorem 3 to show that restricting to stationary policies loses nothing.

The result is proved in the paper and, independently, by Iyengar (2005). No machine-checked proof of it is known to exist. Mathlib provides the Banach fixed-point theorem, but it has no MDP library, no discounted cost along a Markov chain and no robust Bellman operator. The mission produces that layer.

Difficulty

The fixed-point half is a direct application of the Banach fixed-point theorem once the $\nu$ -contraction is established. The substance is the link between the fixed point and the probabilistic cost, and the duality.

$C_\infty(\pi,\tau)$ is an infinite series along a Markov chain. Identifying it with the solution of a linear system requires summing a matrix geometric series.
Nature's sets are neither closed nor convex, so its maxima are suprema that need not be attained. The worst case over $\mathcal T_s$ must be approached by rows that nearly attain the support function, with an error controlled through the contraction.
The min–max and max–min values are taken over different information structures. Equality has to come from the fixed point, not from a minimax theorem: the policy set is finite and discrete and nature's set is not convex, so no convexity argument applies.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ, with the componentwise order and Mathlib's sup metric, which is $\|\cdot\|_\infty$ .
The model (RobustMDP.Discounted.Model) carries the costs, the discount $\nu \in [0,1)$ (the range printed in Theorem 3; §4 prints $(0,1)$ ) and the row sets. The row sets are assumed nonempty and contained in $\Delta_n$ and nothing else. Nonemptiness is implicit in the paper.
$\Pi_s$ is Fin n → A. $\mathcal T_s$ is the subtype of A → Fin n → Fin n → ℝ whose rows lie in the row sets, which encodes rectangularity.
$C_\infty$ is a tsum of the discounted stage costs along the forward state distribution. The terms are nonnegative and at most $\nu^t\max c$ , so the series is summable and the tsum is the limit of the $N$ -stage costs, the paper's definition.
$\sigma_{\mathcal P}$ is a real sSup. It is the genuine supremum because every set it is applied to is nonempty and inside $\Delta_n$ .
Every "max" over nature is a supremum: IsLUB, or ⨆ inside $\min_\pi\sup_\tau$ , whose inner sets are shown bounded by conclusion (23). Minima over the finite $\Pi_s$ and over $\mathcal A$ are ⨅ and Finset.inf'. The argmax rows of (22) appear only as a hypothesis on a given nature policy that attains them.
Corrected statements:
- Lemma 2 is false as printed for $q$ with zero entries, so uniqueness of the optimizer is stated only for $q > 0$ .
- In (30), $\sigma(v^\pi)$ is read as $\sigma(v)$ .
- The proof's references to "Lemma 1", "(15) and (16)" and "(14)" are read as Lemma 2, (27)–(28) and (26).
Defining $C_\infty(\pi,\tau)$ as the fixed point of $w = c_\pi + \nu P_\pi w$ would make milestone (26) a tautology and conclusion (23) nearly so. The cost here is the probabilistic series, and the fixed-point characterizations must be proved.
Welcome contributions include a reusable library of discounted Markov chain costs on finite state spaces (the geometric-series identity behind (26)) and support-function lemmas on the simplex (monotonicity, the bound $\sigma_{\mathcal P}(u) - \sigma_{\mathcal P}(v) \le \|u-v\|_\infty$ ). Both are needed by the other missions of this series.

Selected references

A. Nilim, L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
J. A. Bagnell, A. Y. Ng, J. Schneider, Solving Uncertain Markov Decision Processes, Technical Report CMU-RI-TR-01-25, Carnegie Mellon University, 2001. https://www.ri.cmu.edu/publications/solving-uncertain-markov-decision-processes/
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

10 thms4 active usersReviewed

Combinatorics Convex Optimization Discrete Geometry+1·Captain: Shuze Chen

Discrete Convex Analysis XXII: Convex Extensibility of M-Convex FunctionsTextbook

Motivation

A discrete function defined only on the integer lattice cannot, by itself, be minimized by the tools of continuous optimization — gradients and convexity in the classical sense simply do not apply. Murota's theory of M-convex functions closes this gap by showing that the exchange axiom alone, a purely combinatorial condition, is enough to guarantee that a discrete function behaves exactly like a convex one: its minimizers form a well-structured (M-convex) set, it can be extended to a genuine convex function on real space without gaining any new local minima, and its behavior under a change of price vector (in the economic interpretation where the function is a cost and its argument a bundle of goods) satisfies the same gross substitutes law economists have studied since Kelso and Crawford's matching-market models. This mission develops the second half of that connection: from local optimality (established in the companion mission) to the full structural picture — minimizer sets, price-substitution laws, and the extension of M-convex functions to genuine convex functions in real variables.

Companion mission 06-mconvex-functions-i (Discrete Convex Analysis V) and sibling mission 22-ch06b-mconvexfunctions (Discrete Convex Analysis XXI) cover this chapter's optimality theory (the M-optimality criterion, the exchange axiom as sequential improvement) and its algebraic toolkit (domain operations, worked examples). This mission builds the vocabulary those results also need (redeclared here, since sibling drafts cannot yet import one another) and proves the results on minimizer structure, gross substitutability, and convex extension that this chapter's remaining sections develop: the M-convexity of minimizer sets, the gross substitutes and stepwise gross substitutes properties and their characterizing role, a minimizer-cut theorem with scaling, integral convexity of M♮-convex functions, and — this mission's goal — the theorem characterizing M-convexity entirely through the polyhedral structure of a function's convex extension.

Setting

Fix a finite ground set $V$ . For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain, write $f[p](x) = f(x) - \langle p,x \rangle$ for the linear reweighting by $p \in \mathbb R^V$ , and $\arg\min g = \{x : g(x) \le g(y)\ \forall y\}$ for the minimizer set of any function $g$ . The convex closure $\bar f(x)$ of $f$ at a real point $x$ is the infimum, over finite convex combinations of points of $\operatorname{dom} f$ representing $x$ , of the corresponding combination of function values; $f$ is convex extensible if $\bar f$ agrees with $f$ on $\mathbb Z^V$ , and integrally convex if $\bar f(x)$ can always be computed using only points from $x$ 's own integral neighborhood $N(x)$ (the integer vectors within one unit of $x$ in every coordinate). A polyhedral convex function $g : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ is (polyhedral) M-convex if it satisfies the real-variable exchange axiom (M-EXC[R]): for $x,y \in \operatorname{dom}_{\mathbb R} g$ and $u \in \operatorname{supp}^+(x-y)$ , some $v \in \operatorname{supp}^-(x-y)$ and $\alpha_0 > 0$ make the exchange inequality hold for every $\alpha \in [0,\alpha_0]$ .

Formalization targets

Goal: convex extensibility characterizes M-convexity

For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain,

f \text{ is M-convex} \iff \bigl(f \text{ is convex extensible}\bigr) \wedge \bigl(\forall p \in \mathbb R^V,\ \arg\min \bar f[-p] \text{ is an M-convex polyhedron, if nonempty}\bigr),

with the M♮-analogue using M♮-convex polyhedra (Theorem 6.43). This is the weakest stable form: it characterizes M-convexity purely by properties of the (unique) convex closure, without reference to any specific algorithm for computing it or any bound on the polyhedron's complexity.

Supporting structural targets

Ten further results build the toolkit this goal draws on and the picture it completes: the M-convexity of minimizer sets (Proposition 6.29), the gross substitutes and stepwise gross substitutes properties and the theorems showing they characterize M-convexity and M♮-convexity among convex-extensible functions (Propositions 6.32-6.33, 6.35, Theorems 6.34, 6.36), a minimizer-cut theorem with scaling used algorithmically in Chapter 10 (Theorem 6.39), integral convexity of M♮-convex functions (Theorem 6.42), a shared-coefficient convex-combination theorem for pairs of M♮-convex functions used in Chapter 8's separation theorem (Theorem 6.44), and the polyhedral-M-convexity of an M-convex function's convex extension together with the correspondence between polyhedral M♮-convexity and the real exchange axiom (Theorems 6.45, 6.47).

Significance

Theorem 6.43 is what makes the whole edifice of M-convex function theory a genuine extension of M-convex set theory (chapters 4-5) rather than a separate parallel development: it says that knowing a function's convex extension is polyhedral, with every price-weighted minimizer set an M-convex polyhedron, is not merely a consequence of M-convexity but an exact characterization of it. This is the theorem that lets later results (the discrete conjugacy theorem of Chapter 8, the separation theorems for M♮-convex functions) move freely between the discrete and continuous pictures. The gross substitutes property (Propositions 6.32-6.36) is independently significant outside this book: it is the exact condition, discovered independently in mathematical economics (Kelso-Crawford, Gul-Stacchetti), under which competitive equilibria with indivisible goods are guaranteed to exist — Murota's theorem that gross substitutability characterizes M-convexity (among convex-extensible functions) is what unifies the economic and combinatorial literatures on this question, taken up again in Chapter 11.

None of these results are open — they are Murota's systematic account of a theory with roots in matroid theory, submodular optimization, and mathematical economics. What this mission contributes is a faithful, machine-checked formal statement of each, extending the shared Lean vocabulary (MExchangeAxiom, ConvexClosureVal, ArgMinOn) the Discrete Convex Analysis series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The forward direction of Theorem 6.43 (M-convex $\implies$ convex extensible with polyhedral minimizers) is comparatively direct given Theorem 6.42 and Proposition 6.29. The converse is substantial: it must show that a function whose weighted minimizer sets are all M-convex polyhedra — a purely global, polyhedral condition — satisfies the local exchange axiom (M-EXCloc[Z]), and the book's proof does this by an edge-direction argument on the polyhedron $B = \arg\min f$ : every edge of an M-convex polyhedron must be parallel to some $\chi_u - \chi_v$ , a fact borrowed from the combinatorial structure of chapter 4's base polyhedra applied to a carefully perturbed weight vector. No shortcut through convex analysis alone succeeds, because ordinary polyhedral theory says nothing about which combinatorial directions a polyhedron's edges must follow — that content comes entirely from the M-convexity of the minimizer sets, not from convexity of the closure by itself.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; functions are (V→ℤ)→WithTop ℝ (integer domain) or (V→ℝ)→WithTop ℝ (real domain, for the polyhedral theorems). The convex closure is built directly from finite convex-combination representations rather than an abstract closure operator, and integral convexity compares it against the same construction restricted to each point's integral neighborhood (Fintype.piFinset of per-coordinate Finset.Icc). Real M-convex/M♮-convex polyhedra are defined as convex hulls of M-convex/M♮-convex integer sets, reusing chapters 4-5's own characterization. The real-variable exchange axioms (Theorems 6.45, 6.47) are formalized from the book's primal (interval-of- $\alpha$ ) definition, not the directional-derivative reformulation (M-EXC'[R]); Theorem 6.47's own three-way equivalence is correspondingly stated with only its first two legs (see Difficulty and MODERATION_NOTES.md/HARD.md — this is a documented scope choice, not a trivializing omission, since the six results using the primal axiom already exercise the chapter's real- variable machinery in full). No numeric constants are hard-coded anywhere in this mission beyond the book's own literal coefficients in Theorem 6.39's cut bound ((n-1)(α-1)). This mission's definitions are redeclared from chunks 06-mconvex-functions-i and 22-ch06b-mconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the twelve sorrys are welcome; the goal's converse direction and Theorem 6.44's shared-coefficient construction carry the most independent proof content.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
A. S. Kelso Jr. and V. P. Crawford, "Job matching, coalition formation, and gross substitutes," Econometrica, 50 (1982), pp. 1483-1504.
F. Gul and E. Stacchetti, "Walrasian equilibrium with gross substitutes," Journal of Economic Theory, 87 (1999), pp. 95-124.

47 thms4 active usersReviewed

Completed

Discrete Geometry Linear Optimization Optimization·Captain: mikedeng1

Elementare Theorie der konvexen Polyeder II: Finitely Many Linear Inequalities Define a Convex Polytope Iff Their Normals Positively Span and the Region Has an Interior PointResearch Paper

Motivation

A convex polytope has two standard descriptions: as the convex hull of finitely many points, and as the intersection of finitely many half-spaces. Linear programming uses both at once. The feasible region of a linear program is given by inequalities, while the simplex method and the theory of basic solutions work with its vertices. That the two descriptions define the same class of sets is the Minkowski–Weyl theorem.

Hermann Weyl's 1935 paper Elementare Theorie der konvexen Polyeder (Comment. Math. Helv., 1935, pp. 290–306) gave an elementary, self-contained proof of this equivalence. An English translation appeared in Contributions to the Theory of Games I (Annals of Mathematics Studies 24, 1950), where it served as the polyhedral foundation for the minimax theorem and linear inequality theory in early game theory and linear programming.

Timeline:

Minkowski (1896, 1910): convex bodies, supporting planes and polyhedra in Geometrie der Zahlen, the setting Weyl's paper takes up.
Farkas (1902): the lemma on homogeneous linear inequalities that is Weyl's Satz 3.
Weyl (1935): the finite-basis theorem for cones (Hauptsatz, Satz 1), the duality between a cone and its extreme supports (§3), and the two descriptions of a convex polyhedron (§4). The paper states explicit conditions under which a finite system of inequalities defines a polytope.
Motzkin (1936), Gale, Kuhn, Tucker (1951): systematic treatments of linear inequalities built on this foundation.

Setting

Write $(a x) = a_1 x_1 + \dots + a_n x_n$ for vectors of $\mathbb{R}^n$ . A point system is a finite set $S \subseteq \mathbb{R}^n$ . It is non-degenerate if no $\alpha \neq 0$ has $(\alpha s) = 0$ for all $s \in S$ . A vector $\alpha \neq 0$ is a support of $S$ if $(\alpha s) \ge 0$ for all $s \in S$ . A support is an extreme support if equality holds at $n-1$ linearly independent points of $S$ . A point $x$ is representable by $S$ if $x = \sum_{s \in S} c_s s$ with all $c_s \ge 0$ .

Read as inequalities $(a \xi) \ge 0$ , $a \in S$ , the same $S$ defines the cone $(S)$ of solutions. An extreme solution is a nonzero $\xi \in (S)$ at which $n-1$ linearly independent inequalities of $S$ are tight. The dual system $\Sigma$ consists of the inequalities $(\alpha x) \ge 0$ , one for each extreme solution $\alpha$ , and $(\Sigma)$ is the cone it defines.

For polytopes, Weyl passes to the hyperplane $x_n = -1$ , identified with $\mathbb{R}^m$ , $m = n-1$ . A convex polyhedron is $\operatorname{conv} S$ for a finite $S \subseteq \mathbb{R}^m$ whose affine span is all of $\mathbb{R}^m$ . Given a finite index set $J$ , normals $A_j \in \mathbb{R}^m$ and constants $b_j \in \mathbb{R}$ , the inequalities $A_j \cdot x - b_j \ge 0$ cut out a region

H = \{x \in \mathbb{R}^m : A_j \cdot x - b_j \ge 0 \ \text{for all } j \in J\}.

In Weyl's notation, row $j$ is $(\alpha x) \equiv \alpha_1 x_1 + \dots + \alpha_{n-1}x_{n-1} - \alpha_n \ge 0$ , with $A_j = (\alpha_1,\dots,\alpha_{n-1})$ and $b_j = \alpha_n$ .

Formalization targets

Goal: §4 II (pp. 302–303)

Assume no row is identically zero ( $A_j \ne 0$ or $b_j \ne 0$ ). Then

H \text{ is a convex polyhedron} \iff \Big(\forall \pi' \in \mathbb{R}^m\ \exists \nu \ge 0:\ \pi' = \sum_j \nu_j A_j\Big) \ \wedge\ \Big(\exists c:\ A_j \cdot c - b_j > 0 \ \forall j\Big).

In words, the normals must positively span $\mathbb{R}^m$ and $H$ must contain an inner point. The goal is the equivalence, not either half alone.

Milestones, in the order the proof of §4 II uses them

Satz 1 (Hauptsatz), p. 291: for a non-degenerate $S$ , every $x$ with $(\alpha x) \ge 0$ for all extreme supports $\alpha$ is representable by $S$ .
Zusatz, pp. 294–295: a non-degenerate $S$ has no extreme support iff $0 = \sum_s c_s s$ with all $c_s > 0$ .
Satz 3, p. 296 (Farkas): if $(p\xi) \ge 0$ on all of $(S)$ , then $p$ is a nonnegative combination of $S$ . This milestone is the published platform theorem LinearOptimization.farkas_cone_corollary.
Satz 6, p. 297: for non-degenerate $S$ , $p \in (\Sigma)$ iff $(p\xi) \ge 0$ for all $\xi \in (S)$ .
§3 II, p. 298: for non-degenerate $S$ , every $\pi \in (S)$ is a nonnegative combination of finitely many extreme solutions.
Satz 9, p. 299: if $S$ is non-degenerate and $(S)$ has an inner point, then $\Sigma$ is non-degenerate.
§4 I, p. 301: a convex polyhedron $\operatorname{conv} S$ has an extreme support and equals the set cut out by its extreme supports.

Significance

The result. §4 II gives both directions of the Minkowski–Weyl theorem for full-dimensional polytopes, together with a test on the data $(A, b)$ : positive spanning of the normals is equivalent to boundedness, and a strictly feasible point is equivalent to full dimension. Several parts of LP theory start from this equivalence: finiteness of the vertex set of a bounded feasible region, the existence of an optimal vertex, and the passage between the primal (inequality) and dual (generator) descriptions used in polyhedral combinatorics.

Formalizing it. The theorem has been proved since 1935; the work here is formalization. Mathlib has convex hulls, extreme points, and pointed cones with their duals, but no Minkowski–Weyl theorem for polytopes or for cones. On this platform, Farkas-type lemmas (LinearOptimization.farkas_cone_corollary) and the statement that a nonempty bounded polyhedron is the hull of its extreme points (Bertsimas–Tsitsiklis Thm 2.9) are published. Neither gives the "only if" direction, the positive-spanning criterion, or full-dimensionality.

Difficulty

The "only if" direction and the reduction from a strictly feasible bounded region to cones are routine. The hard step is the finiteness statement: why a finite set of inequalities has only finitely many generators, and why these generate the whole region. Mathlib's compactness results give "a compact convex set is the closed hull of its extreme points" (Krein–Milman). That result does not show that the extreme points are finite in number, nor that there are finitely many of them in a form that can be computed from the inequalities. Weyl's route avoids topology. It goes through the Hauptsatz, proved by induction on dimension, and the duality between $S$ and $\Sigma$ . Each step of that duality needs non-degeneracy, and keeping that hypothesis alive through the dualization (Satz 9) is where care is needed.

Formalization scope

The homogeneous space is Fin n → ℝ, with dot product ⬝ᵥ. Point systems are Finsets; the zero vector is allowed in them. "Representable" is an explicit nonnegative sum over the Finset.
Non-degeneracy is the literal condition " $(\alpha s)=0$ for all $s \in S$ implies $\alpha = 0$ ", not span = ⊤.
Extreme supports and extreme solutions quantify over all vectors with the property. Positive multiples are not identified, and no representatives are chosen.
Extreme solutions are required to be nonzero and to lie in $(S)$ . This is implicit in the paper.
§4 is stated in affine form on Fin m → ℝ, a point $x$ standing for Weyl's $(x,-1)$ . Linear independence of $n-1$ homogenized points becomes affine independence of $m$ points, and non-degeneracy becomes affineSpan ℝ S = ⊤.
A "convex polyhedron" is the hull of a finite set with full affine span. Dropping full-dimensionality would make the "only if" false, since a segment in $\mathbb{R}^2$ has no inner point.
Added hypotheses: no zero row in the goal (Weyl's half-spaces have nonzero normal $(\alpha_1,\dots,\alpha_n)$ , p. 291). Non-degeneracy of $S$ in Satz 6 and in the p. 298 representation, where it is inherited from Satz 4.
Condition (i) of the goal is positive spanning, i.e. nonnegative coefficients. Linear spanning of $\mathbb{R}^m$ would be strictly weaker and would make the statement false.
A trivializing formalization is ruled out: the goal is an equivalence, "convex polyhedron" is an existential over finite point sets with full affine span, and no hypothesis restricts $J$ , $m$ or the data beyond the nonzero rows. For $m = 0$ the statement is true and non-vacuous.
Useful infrastructure, reusable beyond this mission: a Minkowski–Weyl theorem for polyhedral cones in Fin n → ℝ, extreme rays of pointed polyhedral cones, and the homogenization dictionary between cones in $\mathbb{R}^{m+1}$ and polytopes in $\mathbb{R}^m$ . Proofs of any milestone, and alternative routes to the goal (e.g. via Fourier–Motzkin elimination), are welcome.

Selected references

H. Weyl, Elementare Theorie der konvexen Polyeder, Commentarii Mathematici Helvetici (1935), 290–306. https://doi.org/10.1007/bf01292722
H. Weyl, The elementary theory of convex polyhedra, in: H. W. Kuhn, A. W. Tucker (eds.), Contributions to the Theory of Games I, Annals of Mathematics Studies 24, Princeton University Press, 1950.
J. Farkas, Theorie der einfachen Ungleichungen, Journal für die reine und angewandte Mathematik 124 (1902), 1–27. https://doi.org/10.1515/crll.1902.124.1
H. Minkowski, Geometrie der Zahlen, Teubner, Leipzig, 1896/1910.
A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, §7.2 (Minkowski–Weyl).

13 thms4 active usersReviewed

Completed

Analysis Optimization·Captain: mikedeng1

A Nonsmooth Version of Newton's Method III: Semismoothness of the Augmented Lagrangian GradientResearch Paper

Motivation

The augmented Lagrangian method (method of multipliers) of Hestenes, Powell and Rockafellar solves a constrained nonlinear program by repeatedly minimizing an unconstrained merit function in the primal variables and then updating the multipliers. For inequality constraints, the augmented Lagrangian in the form the paper takes from Rockafellar (Rockafellar 1981) is continuously differentiable but not twice differentiable, even when all problem data are smooth: its Hessian jumps across the surfaces where a constraint switches between the "active" and "inactive" formula. Newton's method for the inner minimization therefore has no classical Hessian to work with on those surfaces.

Qi and Sun (Math. Programming 58, 1993) extended Newton's method to equations $F(x) = 0$ with $F$ locally Lipschitz, replacing the Jacobian by an element of Clarke's generalized Jacobian, and proved local superlinear convergence when $F$ is semismooth. Section 4 of the paper, an example suggested by Rockafellar, shows that the gradient of the augmented Lagrangian of a $C^2$ program is semismooth, so the nonsmooth Newton method applies to the stationarity equation $\nabla L_r = 0$ . This mission formalizes that result, Theorem 4.1.

Setting

Let $f_0, f_1, \dots, f_m : \mathbb{R}^n \to \mathbb{R}$ be of class $C^2$ and consider

\text{(NLP)}\quad \min f_0(x)\ \text{ s.t. }\ f_i(x) = 0,\ i = 1,\dots,p,\qquad f_i(x) \le 0,\ i = p+1,\dots,m. \tag{4.1}

Fix $r > 0$ . For a constraint value $a$ and a multiplier $y$ put

\phi(r, a, y) = \begin{cases} y a + \tfrac12 r a^2, & y + r a \ge 0,\\ -\tfrac{1}{2r} y^2, & y + r a \le 0,\end{cases}

(the two cases agree when $y + ra = 0$ ). The augmented Lagrangian is the function of $(x, y) \in \mathbb{R}^n \times \mathbb{R}^m$

L_r(x, y) = f_0(x) + \sum_{i=1}^{p}\Big(y_i f_i(x) + \tfrac12 r f_i(x)^2\Big) + \sum_{i=p+1}^{m} \phi\big(r, f_i(x), y_i\big).

For a locally Lipschitz map $F$ between finite-dimensional spaces, let $D_F$ be the set where $F$ is differentiable. Clarke's generalized Jacobian is $\partial F(x) = \mathrm{co}\{\lim JF(x_i) : x_i \to x,\ x_i \in D_F\}$ . $F$ is semismooth at $x$ if it is locally Lipschitz near $x$ and, for every direction $h$ , the limit of $V h'$ over $V \in \partial F(x + t h')$ , $h' \to h$ , $t \downarrow 0$ , exists.

For a single constraint function $g$ the proof works with $\eta(x, s) = \phi(r, g(x), s)$ on $\mathbb{R}^n \times \mathbb{R}$ , and with the surface $s + r g(x) = 0$ on which the two formulas for $\phi$ meet.

Formalization targets

Goal: Theorem 4.1

For $r > 0$ and $f_0, \dots, f_m \in C^2$ :

L_r \in C^1, \qquad \nabla L_r \text{ semismooth at } (x,y) \text{ whenever } \exists\, i > p:\ y_i + r f_i(x) = 0,

\nabla L_r \in C^1 \text{ near } (x, y) \text{ whenever } y_i + r f_i(x) \neq 0 \text{ for all } i > p.

All three clauses are the theorem; the last two together cover every point.

Milestones

$\eta \in C^1$ , with $\nabla\eta(x,s) = \big((s + r g(x))\nabla g(x),\ g(x)\big)$ if $s + r g(x) \ge 0$ and $(0, -s/r)$ if $s + r g(x) \le 0$ , and $\nabla \eta$ is locally Lipschitz.
Eq. (4.2): the Hessian of $\eta$ on each side of the surface, and $\nabla\eta \in C^1$ near every point off it.
Eq. (4.7): if $\bar s + r g(\bar x) = 0$ and $\bar s + t_j\alpha_j + r g(\bar x + t_j h_j) = 0$ with $h_j \to h$ , $\alpha_j \to \alpha$ , $t_j \downarrow 0$ , then $\alpha + r\nabla g(\bar x)^{\mathsf T} h = 0$ .
$\nabla\eta$ is semismooth, jointly in $(x, s)$ , at every point of the surface.

Significance

The result places the inner problem of the augmented Lagrangian method inside the scope of the paper's convergence theory: with $F = \nabla L_r$ , the generalized-Jacobian Newton iteration converges locally superlinearly at a root where every element of $\partial F$ is nonsingular. Its practical content is that second-order methods can be run on $L_r$ even though $L_r$ is only $C^{1}$ , with the elements of $\partial \nabla L_r$ playing the role of Hessians. The same pattern (a $C^1$ merit function with semismooth gradient) recurs in extended linear-quadratic programming and in semismooth Newton methods for complementarity problems.

The theorem is proved in the paper by direct computation. As far as a search of the platform showed, none of the objects involved (Clarke's generalized Jacobian, semismoothness, Rockafellar's augmented Lagrangian) has a published formalization there, and Mathlib has none of them. The mission produces a machine-checked version of the computation and, as a by-product, reusable statements about $C^1$ functions obtained by gluing two $C^2$ pieces along a hypersurface.

Difficulty

Clauses 1 and 3 are calculus with a case split: one has to check that the two formulas for $\phi$ and for its gradient match on the surface. Clause 2 is where the argument is not routine. On the surface, $\nabla\eta$ is not differentiable, and the generalized Jacobian $\partial\nabla\eta$ there contains convex combinations of the two one-sided Hessians of (4.2). Semismoothness asks that $V(h', \alpha')$ have a single limit over all such $V$ , for all approaches $(h', \alpha') \to (h, \alpha)$ , $t \downarrow 0$ , including approaches that cross the surface infinitely often. The two one-sided Hessians are different matrices, so no single derivative describes $\nabla\eta$ near the surface, and the existence of the limit must be shown for approaches that alternate between the two sides and for the convex combinations that $\partial\nabla\eta$ contains on the surface itself. General theorems that piecewise-smooth maps are semismooth appear in later literature but are not available in Mathlib, so they cannot be invoked as a shortcut. A second obstacle is infrastructure: Mathlib has no generalized Jacobian, so every fact about $\partial\nabla\eta$ (which limits of derivatives occur near the surface) must be derived from the definition.

Formalization scope

$\mathbb{R}^n$ and $\mathbb{R}^m$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); $L_r$ is a function on their product, and $\eta$ on EuclideanSpace ℝ (Fin n) × ℝ.
The constraint index $i \in \{1,\dots,m\}$ is i : Fin m with paper index i.val + 1; equality constraints are i.val < p, inequality constraints p ≤ i.val. The paper's implicit $p \le m$ is not assumed (for $p > m$ there are no inequality constraints).
The paper's first sum prints $h(r_i, f_i(x), y_i)$ ; the single $r$ is used, as in the paper's definition of $h$ .
$\phi$ uses the first branch when $y + ra \ge 0$ ; the branches agree on the boundary. Every statement assumes $r > 0$ .
$C^2$ is ContDiff ℝ 2 on all of $\mathbb{R}^n$ ; "smooth" is the paper's continuously differentiable, ContDiffAt ℝ 1 of the gradient at the point.
$\nabla L_r$ and $\nabla\eta$ are Fréchet derivatives, valued in continuous linear functionals; semismoothness is invariant under the Riesz isometry to gradient vectors and under equivalent norms on the domain (Mathlib's product has the sup norm).
The Jacobian in Clarke's definition is fderiv, limits are along sequences, and no closure is taken in the convex hull. Semismoothness is the explicit $\varepsilon$ – $\delta$ form of the paper's limit, uniform over $V \in \partial F(x + th')$ .
Hessians in (4.2) are stated as the Fréchet derivative of the gradient map applied to a direction.

A formalization that states only $L_r \in C^1$ , or only the semismoothness of one term $\eta$ , is not Theorem 4.1; the goal contains all three clauses for the full $L_r$ . The combination step from the terms $\eta$ to $L_r$ uses that sums of semismooth maps and $C^1$ maps with locally Lipschitz derivative are semismooth; the paper cites this without proof, and a solver will need to prove it.

Contributions welcome: the lemmas above; general facts about clarkeJac (it contains fderiv at points of strict differentiability; it is a singleton for $C^1$ maps; behaviour under sums and linear maps); and the semismoothness of sums.

Selected references

L. Qi, J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58 (1993) 353–367. https://doi.org/10.1007/BF01581275
R. T. Rockafellar, Proximal subgradients, marginal values, and augmented Lagrangians in nonconvex optimization, Mathematics of Operations Research 6 (1981) 427–437. https://doi.org/10.1287/moor.6.3.427
F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983 (reprinted SIAM Classics in Applied Mathematics 5, 1990). https://doi.org/10.1137/1.9781611971309
R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM J. Control Optim. 15 (1977) 959–972. https://doi.org/10.1137/0315061

8 thms4 active usersReviewed

Completed

Optimization Probability·Captain: mikedeng1

Robust Mean-Covariance Solutions for Stochastic Optimization III: Concave Utilities with a Monotone Second Derivative Have a Closed-Form Robust ObjectiveResearch Paper

Motivation

A decision maker who chooses a portfolio $x\in\mathbb R^n$ of risky assets with random return vector $R$ receives the scalar return $x'R$ and evaluates it by an expected utility $E[u(x'R)]$ . In practice the law of $R$ is not known; what can be estimated with some confidence are its mean $\mu$ and covariance $\Sigma$ . The robust mean-covariance objective replaces the unknown law by the worst law consistent with these two moments:

U(x)=\inf\{E[u(x'R)] : R \text{ has mean } \mu \text{ and covariance } \Sigma\}.

Ioana Popescu (Operations Research 55(1), 2007) showed that $U(x)$ depends on $x$ only through $\mu_x=x'\mu$ and $\sigma_x^2=x'\Sigma x$ , and that for large classes of utilities it has a closed form or reduces to a one-dimensional search. This turns a robust stochastic program into a parametric mean-variance program, which is the practical point of the paper. This mission formalizes the closed form for concave utilities with a monotone second derivative (Proposition 7), a class that contains the exponential utility $1-e^{-ay}$ and all concave quadratics. The reduction to $(\mu_x,\sigma_x)$ is the subject of the companion mission Robust Mean-Covariance Solutions for Stochastic Optimization I; the two-point case is mission II.

The underlying univariate question is a moment problem in the tradition of Chebyshev-type bounds: the extremal value of $E[u(r)]$ over all laws with prescribed mean and variance. Scarf (1958) solved an instance for a piecewise-linear inventory cost, and Birge and Dulá (1991) treated two-point extremal laws on bounded domains.

Setting

Fix $m\in\mathbb R$ and $s\ge 0$ . The mean-variance class $\mathbb M_{(m,s^2)}$ is the set of Borel probability measures $\nu$ on $\mathbb R$ with $\int r^2\,d\nu<\infty$ , $\int r\,d\nu=m$ and $\int (r-m)^2\,d\nu=s^2$ (Lean: MeanVarClass m (s ^ 2)). For a utility $u:\mathbb R\to\mathbb R$ the robust objective is

U(m,s)=\inf\Big\{\int u\,d\nu : \nu\in\mathbb M_{(m,s^2)}\Big\},

with $\min$ read, as in the paper, "in the wide sense of $\inf$ ", so the value $-\infty$ is allowed. The paper's $U(x)$ is $U(\mu_x,\sigma_x)$ .

For $p\in(0,1)$ the two-point law $r_p$ puts mass $p$ on $b=m+\sqrt{(1-p)/p}\,s$ and mass $1-p$ on $a=m-\sqrt{p/(1-p)}\,s$ ; these are exactly the two-point laws of $\mathbb M_{(m,s^2)}$ . Its expected utility is the two-point objective (8),

U(p)=p\,u(b)+(1-p)\,u(a)\qquad(\texttt{twoPointValue u m s p}).

A supporting quadratic of $u$ is $q(y)=Ay^2+By+C$ with $q\le u$ on $\mathbb R$ ; the set of their coefficients is $\mathcal Q$ . Since every $r\sim(m,s^2)$ has $E[q(r)]=A(m^2+s^2)+Bm+C$ , each element of $\mathcal Q$ gives a lower bound on $U(m,s)$ (Proposition 3). The function $u$ has the one-point support property with respect to $(m,s^2)$ (Definition 3, OnePointSupportWrt u m s) if some supporting quadratic touches $u$ at $m$ and $E[u(r_p)]\to E[q(r_p)]$ as $p\to0^+$ or as $p\to1^-$ ; it has one-point support (OnePointSupport u) if this holds for every $m$ and every $s\ge0$ .

Formalization targets

Goal: Proposition 7

Let $u$ be concave and twice differentiable with monotone $u''$ .

(a) If $u'$ is convex, then

U(m,s)=u(m)+\lim_{y\to-\infty}u''(y)\,\frac{s^2}{2}\qquad\text{for all } m,\ s.

(b) If $u'$ is concave, the same holds with $\lim_{y\to+\infty}u''(y)$ .

In each part the limit $L$ of $u''$ exists in $[-\infty,0]$ . When $L$ is finite the goal asserts that $u$ is integrable under every law of every class, that $u(m)+Ls^2/2$ is the greatest lower bound of the expected utilities, and that $u$ has one-point support. When $L=-\infty$ and $s>0$ it asserts $U(m,s)=-\infty$ .

Milestones

Display (9): $\partial U/\partial p=u(b)-u(a)-(b-a)\,\frac{u'(b)+u'(a)}{2}$ .
For convex $u'$ and $s>0$ , $U(p)$ is nonincreasing on $(0,1)$ .
Appendix (4): $\lim_{p\to1^-}U(p)=u(m)+\frac{s^2}{2}\lim_{y\to-\infty}u''(y)$ , including the value $-\infty$ .
Proposition 3: every $E[u(r)]$ dominates every $A(m^2+s^2)+Bm+C$ with $(A,B,C)\in\mathcal Q$ .
The function $d(y)=\frac{u(y)-u(m)}{(y-m)^2}-\frac{u'(m)}{y-m}$ is nondecreasing on $\{y \neq m\}$ when $u'$ is convex.
Appendix (5): $q(y)=\tfrac12u''(-\infty)(y-m)^2+u'(m)(y-m)+u(m)$ supports $u$ , and $\inf_{y\ne m}d(y)=\lim_{y\to-\infty}d(y)=\tfrac12u''(-\infty)$ .

An additional item states Proposition 8: a monotone convex $u$ has one-point support and $U(m,s)=u(m)$ .

Significance

Proposition 7 turns the worst-case expected utility into a mean-variance criterion with an explicit risk weight: a prudent investor ( $u'$ convex) is penalized by $\tfrac12\lim_{y\to-\infty}u''(y)$ per unit of variance, an imprudent one by the limit at $+\infty$ . With Proposition 1, the robust portfolio problem becomes $\max_x\ u(\mu_x)+\tfrac12 L\,\sigma_x^2$ , a concave mean-variance program. For exponential utility the weight is $-\infty$ (Example 3 of the paper), so the robust investor must eliminate variance entirely; this is a qualitative statement about robustness that follows only from the $-\infty$ case of the theorem.

The result is published with a proof in the appendix of the paper. It has, to the best of our search, no machine-checked version, and the platform currently holds no statement of Propositions 3, 7 or 8 or Definition 3. A formal proof would also check two points where the printed argument is incomplete: the proof's step " $\lim_{y\to-\infty}u'(y)=\infty$ " fails for affine $u$ , where the theorem nevertheless holds, and the claim that $u$ "has one-point support" fails when $\lim u''=-\infty$ (see the scope section). Related platform work on worst-case expectations over ambiguity sets is the mission Wasserstein Distributionally Robust Optimization II, which uses a different ambiguity set.

Difficulty

The infimum ranges over all laws with two prescribed moments, an infinite-dimensional set with no compactness, and in the relevant cases it is not attained. The natural first idea, restricting to two-point laws and minimizing over $p$ , gives only an upper bound (display (7)), and here the minimizing $p$ runs off to the boundary: the extremal law puts vanishing mass on a point escaping to $-\infty$ . Identifying the limiting value requires controlling $u(m-sq)/(1+q^2)$ as $q\to\infty$ , a second-order asymptotic statement about $u$ at $-\infty$ . The matching lower bound requires a supporting quadratic whose curvature is exactly $\tfrac12\lim u''$ ; showing that it lies below $u$ everywhere, not only near $m$ , is a global statement that uses the convexity of $u'$ on the whole line. The finite-limit and infinite-limit cases also behave differently: in the second, no supporting quadratic exists at all.

Formalization scope

Laws are Measure ℝ with IsProbabilityMeasure, finite second moment is MemLp id 2, and the class is parameterized by mean $m$ and variance $s^2$ with $s\ge0$ . The statements are univariate: $U(x)$ of the paper is the univariate objective at $(\mu_x,\sigma_x)$ by Proposition 1 of the paper (mission I). Derivatives are deriv u and deriv (deriv u); "twice differentiable" is differentiability of $u$ and of $u'$ . Limits of $u''$ are explicit hypotheses (Tendsto … atBot (𝓝 L) or Tendsto … atBot atBot), never limUnder. Limits in $p$ are one-sided inside $(0,1)$ . Expectations under two-point laws are written by the explicit formula (8).

"Min" is never a real ⨅, which Lean evaluates to $0$ on sets unbounded below. The finite case uses IsGLB together with integrability of $u$ under every law of the class; the infinite case asserts that integrable laws with arbitrarily small expected utility exist; Proposition 3 is stated as "every value $\ge$ every value". Proposition 3 assumes $u$ integrable under the law; Proposition 8 takes the infimum over laws under which $u$ is integrable, which for convex $u$ loses nothing.

One correction to the printed statement: Proposition 7 opens with "then $u$ has one-point support", which is false when $\lim u''=-\infty$ , since no quadratic lies below $1-e^{-ay}$ on $\mathbb R$ . The formalization asserts one-point support only in the finite-limit case and the value $-\infty$ in the other. A formalization that took $\min$ as a real infimum, dropped the integrability conjunct, or asserted one-point support unconditionally would be either trivially satisfiable or false; none of these is used.

A complete development needs: moments of two-point laws, a second-order l'Hôpital or Taylor argument at $-\infty$ , the trapezoid inequality for convex functions, and Jensen-type integration of quadratic lower bounds. The mean-variance class, the two-point objective and the supporting-quadratic lemmas are reusable for mission II and for other moment-problem bounds. Proofs of any milestone, and of part (b), are welcome.

Selected references

I. Popescu, Robust Mean-Covariance Solutions for Stochastic Optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
H. Scarf, A min-max solution of an inventory problem, in Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
J. R. Birge, J. H. Dulá, Bounding separable recourse functions with limited distribution information, Annals of Operations Research 30, 1991.
S. Karlin, W. J. Studden, Tchebycheff Systems: With Applications in Analysis and Statistics, Interscience, 1966.

11 thms4 active usersReviewed

Completed

Convex Optimization Graph Theory Linear algebra+1·Captain: mikedeng1

Lifts of Convex Sets and Cone Factorizations III: Stable Set Polytopes Have No Small Semidefinite LiftsResearch Paper

Motivation

Many polytopes of combinatorial optimization have exponentially many facets, yet linear optimization over them is tractable because they are projections of simpler convex sets: affine slices of a nonnegative orthant (linear programming) or of the cone of positive semidefinite matrices (semidefinite programming). The size of such a representation, the number of variables of the extended formulation, is the natural measure of how compactly a polytope can be optimized over. Yannakakis (Expressing combinatorial optimization problems by linear programs, JCSS 1991) characterized polyhedral representations through nonnegative factorizations of the slack matrix. Gouveia, Parrilo and Thomas (arXiv:1111.3164, Mathematics of Operations Research 2013) extended the characterization to lifts into arbitrary closed convex cones, in particular to cones of positive semidefinite matrices.

The stable set polytope of a graph is the standard test case. For a perfect graph on $n$ vertices it is a linear image of an affine slice of the cone of $(n+1)\times(n+1)$ positive semidefinite matrices (Lovász's theta body construction, stated in the paper as Theorem 5.1 with a citation to Lovász & Schrijver, SIAM J. Optim. 1991); this is the reason the maximum weight stable set problem is solvable in polynomial time on perfect graphs. The question addressed by this mission is whether a smaller matrix size could suffice. Theorem 5.2 of Gouveia–Parrilo–Thomas answers it: for every graph on $n$ vertices, matrices of size $n$ do not suffice.

Setting

Let $G$ be a graph with vertex set $V = \{1,\dots,n\}$ . A set $S \subseteq V$ is stable if no edge joins two of its elements, and its incidence vector $\chi_S \in \{0,1\}^n$ has $(\chi_S)_i = 1$ exactly when $i \in S$ . The stable set polytope is

\mathrm{STAB}(G) = \mathrm{conv}\{\chi_S : S \text{ stable}\} \subseteq \mathbb R^n .

Let $\mathcal S^k_+$ be the cone of $k \times k$ real symmetric positive semidefinite matrices, with the trace inner product $\langle A, B\rangle = \mathrm{tr}(AB)$ , under which it is self-dual. For a closed convex cone $K$ , a set $C$ has a $K$ -lift if $C = \pi(K \cap L)$ for an affine subspace $L$ and a linear map $\pi$ ; the lift is proper if $L$ meets the interior of $K$ .

For a polytope $P$ with vertices $p_1,\dots,p_v$ and facet inequalities $h_1(x) \ge 0, \dots, h_f(x) \ge 0$ , the slack matrix is the nonnegative $v\times f$ matrix $(h_j(p_i))$ . A $K$ -factorization of a nonnegative matrix $M$ assigns $a^i \in K$ to each row and $b^j \in K^*$ to each column with $\langle a^i, b^j\rangle = M_{ij}$ . In Lean the objects are stab, HasPSDLift, HasConeLift, HasProperConeLift, IsSlackMatrix, HasConeFactorization and HasPSDFactorization in the namespace ConeLifts.StableSet.

Formalization targets

Goal: Theorem 5.2

For every $n \ge 1$ and every graph $G$ on $n$ vertices,

\neg\ \exists\, L,\ \pi:\quad \mathrm{STAB}(G) = \pi(\mathcal S^n_+ \cap L).

The statement excludes all lifts, proper or not, and holds for every graph, perfect or not.

Milestones

Theorem 3.3 (first sentence). If a full-dimensional polytope $P$ with the origin in its interior has a proper $K$ -lift, then every slack matrix of $P$ admits a $K$ -factorization.
Rows of the submatrix. The origin and $e_1,\dots,e_n$ are vertices of $\mathrm{STAB}(G)$ .
Columns of the submatrix. For $n \ge 1$ , each $\{x \in \mathrm{STAB}(G) : x_i = 0\}$ is a facet, and some facet does not contain the origin.
The core lemma. For every $s \in \mathbb R^n$ the block matrix

S' = \begin{pmatrix} 1 & 0_n \\ s & I_n\end{pmatrix}

has no $\mathcal S^n_+$ -factorization.

Significance

Theorem 5.2 shows that the semidefinite representation of $\mathrm{STAB}(G)$ for perfect graphs has the smallest possible matrix size: $n+1$ cannot be lowered to $n$ . As Remark 5.3 of the paper notes, the same argument shows that no polytope in $\mathbb R^n$ with a vertex at which it locally looks like the nonnegative orthant has an $\mathcal S^n_+$ -lift. It is also an instance of the factorization method: a statement about all possible semidefinite representations is reduced to a finite obstruction on a small submatrix of the slack matrix.

The theorem is proved in the paper. To the best of our knowledge no machine-checked proof of it, of the factorization theorem for cone lifts, or of any positive semidefinite lower bound for a polytope exists in Mathlib or on this platform. A formalization produces reusable statements about positive semidefinite factorizations, slack matrices and lifts, and a verified instance of the general lower-bound technique.

Difficulty

The step from lifts to factorizations is where the direct argument fails. Theorem 3.3 applies only to proper lifts and only to polytopes with the origin in their interior, while the goal concerns all lifts of a polytope that has the origin as a vertex. Applying Theorem 3.3 to $\mathrm{STAB}(G)$ and an arbitrary lift therefore does not match its hypotheses, and the printed proof does not spell out how the two gaps are closed (see Formalization scope). Theorem 3.3 itself is a consequence of the general factorization theorem of the paper (Theorem 2.4), whose proof rests on conic duality. The core lemma about $S'$ is a statement about every family of $2(n+1)$ positive semidefinite matrices, so it cannot be settled by any finite search.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); vertex $i+1$ of the paper is i : Fin n; graphs are SimpleGraph (Fin n) and stability is SimpleGraph.IsIndepSet. Vertices of a polytope are Set.extremePoints ℝ. $\mathcal S^k_+$ is the set of real $k\times k$ matrices satisfying Matrix.PosSemidef (which includes symmetry), and the ambient space of a positive semidefinite lift is all $k \times k$ matrices; this does not change which sets have lifts, because a lift in the symmetric matrices extends linearly and a lift in all matrices restricts to them. Positive semidefinite factorizations require both factor families to be positive semidefinite and use $\mathrm{tr}(A_iB_j)$ .

Reading decisions: the goal assumes $n \ge 1$ , the paper's meaning of "a graph with $n$ vertices", since for $n = 0$ the polytope $\{0\}$ is the image of $\mathcal S^0_+$ and the printed statement fails. Milestone 3 also assumes $n \ge 1$ , and so does Milestone 1 (Theorem 3.3): in $\mathbb R^0$ the point $\{0\}$ has a proper lift to the whole space $\mathbb R^m$ , whose dual cone $\{0\}$ cannot factor the slack matrix $(1)$ . In Milestone 4 the column $*_n$ is an arbitrary real vector. The slack matrices of Theorem 3.3 are encoded through the identification on p. 9 of the paper: rows are vertices of $P$ , columns are extreme points $y$ of the polar $P^\circ = \{y : \langle x, y \rangle \le 1\ \forall x \in P\}$ , the canonical entry is $1 - \langle p, y\rangle$ , and every slack matrix is the canonical one with positively scaled columns. Facets in Milestone 3 are nonempty proper exposed faces of dimension one less than the polytope.

The goal must not be weakened to proper lifts, and lifts must use equality $\mathrm{STAB}(G) = \pi(\mathcal S^n_+ \cap L)$ with $\pi$ linear and $L$ affine; with inclusion, or with arbitrary maps, the statement becomes trivial or false. The core lemma is meaningful only with both factor families positive semidefinite; without that requirement $S'$ factors trivially.

Beyond the milestones, a complete proof of the goal needs two facts the paper uses without stating them as claims of this proof: (a) an $\mathcal S^n_+$ -lift that is not proper is a proper lift to a face of $\mathcal S^n_+$ (p. 5), every face of $\mathcal S^n_+$ is isomorphic to some $\mathcal S^r_+$ with $r \le n$ (Example 4.2, p. 12), and an $\mathcal S^r_+$ -factorization yields an $\mathcal S^n_+$ -factorization; (b) lifts are preserved by affine maps (Proposition 2.9, pp. 6–7), and translating a polytope changes its slack matrices only by positive column scalings, which is how Theorem 3.3 applies to $\mathrm{STAB}(G)$ , whose origin is a vertex rather than an interior point. Stating (a) and (b) as separate lemmas is welcome.

Needed infrastructure: positive semidefinite matrices and the trace pairing, the face structure of $\mathcal S^n_+$ , invariance of lifts under affine maps, and conic duality for Theorem 3.3. All of these are reusable beyond this mission. Contributions welcome: proofs of the milestones, the bridging facts (a) and (b), and alternative routes to the goal.

Selected references

J. Gouveia, P. A. Parrilo, R. R. Thomas, Lifts of Convex Sets and Cone Factorizations, Mathematics of Operations Research 38(2):248–264, 2013. arXiv:1111.3164v2. https://arxiv.org/abs/1111.3164
M. Yannakakis, Expressing combinatorial optimization problems by linear programs, Journal of Computer and System Sciences 43(3):441–466, 1991. https://doi.org/10.1016/0022-0000(91)90024-Y
L. Lovász, A. Schrijver, Cones of matrices and set-functions and 0-1 optimization, SIAM Journal on Optimization 1(2):166–190, 1991. https://doi.org/10.1137/0801013

14 thms4 active usersReviewed

Completed

Combinatorics Discrete Geometry Optimization·Captain: Shuze Chen

Discrete Convex Analysis I: Valuated MatroidsTextbook

Motivation

Matroids abstract the combinatorial content of linear independence: which sets of columns of a matrix are independent, which are maximal (bases), and how bases relate to each other. This abstraction, isolated independently by Whitney (1935) and van der Waerden's school, turned out to be exactly the right level of generality for a large family of greedy and augmenting-path algorithms — a base of a matroid can always be reached from another by a sequence of single-element swaps, and this exchange property is what makes local search on bases correct and efficient.

A natural question, raised in the 1980s once matroid-based combinatorial optimization was mature, is what happens when bases are not merely present or absent but carry real-valued weights that must interact well with the exchange structure. Dress and Wenzel answered this with the notion of a valuated matroid: a real-valued function on the bases of a matroid satisfying a weighted strengthening of the exchange axiom. Their motivation was explicitly algorithmic — valuated matroids are exactly the structures for which a greedy algorithm computes an optimal basis under linear objectives, and more generally under the family of "tilted" objectives obtained by adding an arbitrary linear functional. Independently, valuated matroids arise from the classical Grassmann–Plücker relation applied to matrices over a field with a valuation (hence the name), connecting them to tropical geometry.

This mission formalizes the two theorems of Murota's Discrete Convex Analysis (2003, §2.4) that make this story precise: the classical correspondence between a matroid's base family and its rank function (Theorem 2.29), and the characterization of valuations by a perturbation-robustness property (Theorem 2.32). Theorem 2.32 is also historically the entry point of the book's central theme — it is the special case, for the two-valued lattice $\{0,1\}^V$ , of the general local-exchange criterion for M-convex functions that occupies chapters 6 and 7.

Setting

Let $V$ be a finite set (the ground set). A matroid on $V$ is a pair $(V, \mathcal B)$ where $\mathcal B$ , the base family, is a nonempty family of subsets of $V$ satisfying the simultaneous exchange axiom (B): for every $J, J' \in \mathcal B$ and every $i \in J \setminus J'$ , there exists $j \in J' \setminus J$ such that both

J - i + j := (J \setminus \{i\}) \cup \{j\} \in \mathcal B \quad\text{and}\quad J' + i - j := (J' \setminus \{j\}) \cup \{i\} \in \mathcal B.

Equivalently (Theorem 2.29 below), a matroid can be described by its rank function $\rho : 2^V \to \mathbb Z$ , a set function satisfying:

(R1) $0 \le \rho(X) \le |X|$ for every $X \subseteq V$ ;
(R2) monotonicity: $X \subseteq Y \implies \rho(X) \le \rho(Y)$ ;
(R3) submodularity: $\rho(X) + \rho(Y) \ge \rho(X \cup Y) + \rho(X \cap Y)$ .

A valuation of a base family $\mathcal B$ is a function $\omega : \mathcal B \to \mathbb R$ satisfying the axiom (VM): for every $J, J' \in \mathcal B$ and $i \in J \setminus J'$ , there is $j \in J' \setminus J$ with $J - i + j, J' + i - j \in \mathcal B$ and

\omega(J) + \omega(J') \le \omega(J - i + j) + \omega(J' + i - j).

The pair $(V, \omega)$ is then a valuated matroid. For $p : V \to \mathbb R$ , the perturbation of $\omega$ by $p$ is

\omega[-p](J) = \omega(J) - \sum_{j \in J} p(j).

Formalization targets

Goal: Theorem 2.32 (the valuated matroid characterization)

\omega \text{ is a valuation of } \mathcal B \iff \forall\, p : V \to \mathbb R,\ \{J \in \mathcal B : \omega[-p](J') \le \omega[-p](J)\ \forall J' \in \mathcal B\} \text{ is a nonempty family satisfying (B)}.

The right-hand side says: for every linear perturbation $p$ , the set of $\omega[-p]$ -maximal bases is again the base family of a matroid. The universal quantifier over $p$ is not optional — a version of this statement quantified over a single fixed $p$ is either vacuous or false, and does not capture what makes valuated matroids useful.

Milestone: Theorem 2.29 (the base-family / rank-function correspondence)

The maps

\rho(X) = \max\{|X \cap J| : J \in \mathcal B\}, \qquad \mathcal B = \{J \subseteq V : \rho(J) = |J| = \rho(V)\}

are mutually inverse bijections between nonempty families satisfying (B) and set functions satisfying (R1)-(R3). This is weaker groundwork than the goal, stated first because it fixes the exact axiomatic vocabulary — (B) and (R) — that Theorem 2.32 is built on.

Significance

The result itself. Theorem 2.32 is the reason valuated matroids are the right object for weighted combinatorial optimization on matroids: it says a function on bases behaves correctly under every linear re-weighting of the ground set exactly when it satisfies the local exchange inequality (VM). This is what guarantees, for instance, that a greedy algorithm which is correct for the unweighted matroid extends correctly to families of tilted objectives, and it is the germ of the general local-optimality criterion for M-convex functions (chapters 6–7), which underlies most of the algorithmic content of the rest of the book. Theorem 2.29 is the classical result — due jointly to the development of matroid theory from the 1930s onward — that the base-exchange and rank-submodularity axiomatizations of a matroid carry the same information; it is the finite, unweighted precursor of Theorem 2.32.

Formalizing it. Neither theorem has a machine-checked proof on the platform prior to this mission (see Formalization scope for the prior-art check). Theorem 2.29's own proof is elementary but has two independent halves (each map preserves its target axiom class, and the two maps compose to the identity in both directions) that must all be established; Theorem 2.32's proof, as given in the source, defers entirely to a later, more general chapter-6 theorem, so a solver working only from this mission must either reconstruct a direct combinatorial argument for this special case or await chunk 06 (DiscreteConvex.MConvexFunctions, a separate mission) and specialize its main theorem.

Difficulty

The obvious approach to Theorem 2.32 — fix an optimal basis $J$ for $\omega[-p]$ and try to show the exchange condition on maximizers directly from (VM) — proves one direction (VM implies the maximizer property) in a few lines, since perturbing does not change which exchange moves are available. The converse is the substantial direction: from "the maximizer set is always a matroid, for every $p$ ," one must recover the single global inequality (VM) that must hold for all pairs $J, J' \in \mathcal B$ , not just optimal ones. The standard argument constructs, for a given non-optimal pair, a perturbation $p$ under which that specific pair becomes simultaneously optimal, and this construction is exactly the step the book skips by citing chapter 6's general theorem. A formalization attempting to bypass this by only checking the maximizer property for a finite or generic sample of perturbations would trivialize the statement to something false or vacuous — a pitfall the goal's explicit ∀ p is designed to prevent.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; $2^V$ is represented as Finset (Finset V), and $V \to \mathbb R$ as a plain function type. The rank function is $\mathbb Z$ -valued (matching the book's own convention for matroid rank, as opposed to the $\mathbb R$ -valued conventions used from chapter 6 onward for general M-convex functions); RankOfFamily is implemented with Finset.sup over $\mathbb N$ rather than a partial max', so that it is a total function — its junk value at the empty family is never invoked, since every hypothesis in this mission supplies nonemptiness explicitly, matching the book's own phrasing.

A trivializing formalization of the goal is one that quantifies over a single fixed $p$ , or allows $\mathcal B$ to be empty; both are explicitly excluded by keeping $\mathcal B.\text{Nonempty}$ a hypothesis and $p$ universally quantified inside the theorem statement itself.

Checked against Mathlib (commit 0df444a360eaa60ab8c11dca51a86af692955474): Mathlib's Matroid structure is axiomatized via the single-element (asymmetric) exchange property, classically but not definitionally equivalent to Murota's simultaneous axiom (B) used throughout this book, and Mathlib provides no constructor recovering a base family or a Matroid from a bare rank function satisfying (R1)-(R3). Theorem 2.29 is therefore genuine, reusable infrastructure, not a restatement of existing Mathlib API. No reference item was found on the platform for either theorem (GET /theorems?q=matroid, q=valuated matroid return only unrelated tropical-geometry and k-server results). Contributions to a shared DiscreteConvex.Combinatorial definitions layer (the exchange and rank axioms) are welcome from later chunks of this series that build on matroid or base-polyhedron structure.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
H. Whitney, "On the abstract properties of linear dependence," American Journal of Mathematics, 57(3), 1935, pp. 509–533.
A. W. M. Dress, W. Wenzel, "Valuated matroids," Advances in Mathematics, 93(2), 1992, pp. 214–250.
R. A. Brualdi, "Comments on bases in dependence structures," Bulletin of the Australian Mathematical Society, 1(2), 1969, pp. 161–167.

13 thms4 active usersReviewed

Completed

Machine Learning Optimization Probability+1·Captain: mikedeng1

A Distributional Interpretation of Robust Optimization II: Box-Robust Sample Average Optimization Is ConsistentResearch Paper

Why robustify a sampled stochastic program

Many decision problems under uncertainty take the form of a stochastic program: choose a decision $v$ from a feasible set $\mathcal F$ to maximise the expected utility $\mathbb E_{x\sim\mu}[f(v,x)]$ , where the distribution $\mu$ of the uncertain parameter $x\in\mathbb R^m$ is known only through i.i.d. samples $x_1,\dots,x_n$ . The standard remedy, sample average approximation, maximises $\frac1n\sum_i f(v,x_i)$ instead. Its consistency (convergence of the optimal expected utility of its solutions to the true optimum) is classical, but it needs regularity assumptions of its own, for example those of King and Wets (Stochastics and Stochastic Reports, 1991), cited on p. 98 of the paper; the paper presents its construction as a route to consistency under weaker conditions.

Robust optimization (RO) takes a different route: it protects each sample by an uncertainty set and optimises against the worst point in it. Xu, Caramanis and Mannor (Math. Oper. Res. 2012) show that RO over several overlapping uncertainty sets is equivalent to a distributionally robust stochastic program (their Theorem 2.1, the subject of mission I of this series). Section 3 of the paper uses that equivalence to show that a specific robustification of the sampled problem, with $\ell_\infty$ boxes of shrinking radius around each sample, is consistent under only boundedness and equicontinuity of $f$ . This mission formalizes that result, Theorem 3.1.

Setting

Equip $\mathbb R^m$ with the sup norm $\|z\|_\infty=\max_k|z_k|$ , its Borel $\sigma$ -algebra and Lebesgue measure $dx$ . The data are:

a set of decisions $V$ and a nonempty feasible set $\mathcal F\subseteq V$ ;
a utility $f:V\times\mathbb R^m\to\mathbb R$ , Borel measurable in $x$ for each $v$ ;
a true density $h^*$ on $\mathbb R^m$ (nonnegative, $\int h^*\,dx=1$ ) and i.i.d. samples $x_1,x_2,\dots$ with distribution $h^*(x)\,dx$ ;
radii $\epsilon(n)>0$ .

For a sample $x_1,\dots,x_n$ the boxes are $\mathcal Z_i=\{x_i+\delta\mid\|\delta\|_\infty\le\epsilon(n)\}$ , and the box-robust sample objective is

J_n(v)=\frac1n\sum_{i=1}^n\ \inf_{\|\delta_i\|_\infty\le\epsilon(n)}f(v,x_i+\delta_i)=\sum_{i=1}^n\frac1n\inf_{x_i'\in\mathcal Z_i}f(v,x_i').

The RO solution $v(n)$ is a maximiser of $J_n$ over $\mathcal F$ . The equicontinuity modulus of $f$ is

d(\epsilon)=\sup_{v,\,x,\ \|\delta\|_\infty\le\epsilon}|f(v,x)-f(v,x+\delta)|.

The proof works with the distribution set $\mathcal P_n$ of probability measures $\mu$ with $\mu(\bigcup_{i\in S}\mathcal Z_i)\ge|S|/n$ for every $S\subseteq\{1,\dots,n\}$ , and with the uniform box kernel density estimator

h_n(x)=(n\epsilon(n)^m)^{-1}\sum_{i=1}^nK\Big(\frac{x-x_i}{\epsilon(n)}\Big),\qquad K(z)=\frac{\mathbf 1(\|z\|_\infty\le1)}{2^m}.

Formalization targets

Goal: Theorem 3.1 (p. 98)

Assume $|f(v,x)|\le C$ for all $v,x$ ; $d(\epsilon)\to0$ as $\epsilon\downarrow0$ ; $\epsilon(n)\downarrow0$ and $n\epsilon(n)^m\uparrow\infty$ . Then for every choice of maximisers $v(n)$ , with probability one,

\lim_{n\to\infty}\int_{\mathbb R^m}f(v(n),x)\,h^*(x)\,dx=\sup_{v\in\mathcal F}\int_{\mathbb R^m}f(v,x)\,h^*(x)\,dx .

Milestones (proof of Theorem 3.1, p. 99)

$h_n$ is the density of a probability measure in $\mathcal P_n$ .
$J_n(v)\le\int f(v,x)\,h_n(x)\,dx$ for every $v$ .
Oscillation over a box: $\sup_{\mathcal Z_i}f(v,\cdot)-\inf_{\mathcal Z_i}f(v,\cdot)\le d(2\epsilon(n))$ .
Eq. (7): with $M_n=C\int|h_n-h^*|\,dx$ , for every $v$ ,

J_n(v)-M_n\le\int f(v,x)h^*(x)\,dx\le J_n(v)+M_n+d(2\epsilon(n)).

Strong $L^1$ consistency of the box kernel density estimator: if $\epsilon(n)\to0$ and $n\epsilon(n)^m\to\infty$ , then $\int|h_n-h^*|\,dx\to0$ almost surely.

Milestones 1–4 are deterministic statements about a fixed sample; milestone 5 is the only probabilistic input.

Significance

Theorem 3.1 gives consistency of a tractable robust reformulation of a sampled stochastic program under conditions the paper notes are weaker than those of King and Wets for sampled stochastic programs: $f$ need only be bounded and equicontinuous in $x$ , uniformly in $v$ , and the true distribution need only have a density. It also gives an explicit schedule for the size of the uncertainty set, $\epsilon(n)\to0$ with $n\epsilon(n)^m\to\infty$ , the bandwidth condition of kernel density estimation. Section 4 of the paper applies the same distributional interpretation to regularised learning methods such as the support vector machine and the Lasso.

The result is proved in the paper, with the $L^1$ consistency of kernel density estimators (Devroye 1983; Devroye and Györfi 1985) cited rather than proved. No part of it is formalized in Lean or on this platform as far as a search of the platform found. A complete development would produce, besides Theorem 3.1, a machine-checked strong $L^1$ consistency theorem for kernel density estimators, which is a basic result of nonparametric statistics in its own right.

Difficulty

The deterministic part (milestones 1–4) is measure-theoretic bookkeeping: the kernel integrates to one only because the box is a sup-norm ball of volume $(2\epsilon)^m$ , and every infimum and supremum must be handled with care, since $f$ need not attain them.

The obstacle is milestone 5. Almost-sure $L^1$ convergence of $h_n$ to an arbitrary density $h^*$ , with no continuity or support assumption, does not follow from the strong law of large numbers applied pointwise: $h_n(x)$ is an average of $n$ terms whose law changes with $n$ through $\epsilon(n)$ , and almost-sure convergence at each fixed $x$ does not give convergence of the integral along a single sample path. The theorem needs both a bias estimate valid for every integrable density and a concentration estimate for the random $L^1$ error. Mathlib has Lebesgue differentiation and the strong law, but no kernel density estimator and no such concentration result.

Formalization scope

$\mathbb R^m$ is Fin m → ℝ, whose Mathlib norm is the sup norm; boxes are Metric.closedBall. The integrals $\int f(v,x)h^*(x)\,dx$ are Bochner integrals against Lebesgue measure of integrable integrands.
The samples are a sequence X : ℕ → Ω → Fin m → ℝ on a probability space, independent (iIndepFun) and each with law volume.withDensity h*; $x_1,x_2,\dots$ become X 0, X 1, …, and the $n$ -th problem uses the first $n$ . "With probability one" is ∀ᵐ ω ∂P.
The goal quantifies over every selection $v(n)$ of maximisers, with no measurability assumed; a version with one chosen maximiser would be weaker and is ruled out.
Readings and corrections of the printed text:
- the kernel argument printed $(x-x_i)/\epsilon$ on p. 98 is read as $(x-x_i)/\epsilon(n)$ , as the proof on p. 99 writes it;
- " $\max_{v,x}|f(v,x)|\le C$ " is read as the uniform bound $|f|\le C$ and the "max" in $d(\epsilon)$ as a supremum;
- " $d(\epsilon)\downarrow0$ " is read as $d(\epsilon)\to0$ as $\epsilon\downarrow0$ ;
- implicit hypotheses made explicit: $\mathcal F\ne\emptyset$ , $\epsilon(n)>0$ , measurability of $f(v,\cdot)$ , $h^*$ a Lebesgue density;
- the monotonicity in " $\epsilon(n)\downarrow0$ , $n\epsilon(n)^m\uparrow\infty$ " is kept in the goal; milestone 5 uses the limits only, as the paper states it;
- the paper's $M_n$ ("there exists $\{M_n\}\to0$ ") is made explicit as $M_n=C\int|h_n-h^*|$ , so Eq. (7) is stated for every sample.
Remark 3.2 and Appendix B (an integrable envelope in place of boundedness) are not part of this mission.
Every real infimum and supremum ranges over a nonempty set of values bounded by $C$ in absolute value, so no statement holds through a junk value; a formalization in which the supremum over $\mathcal F$ or the box infimum could be vacuous is excluded.
The definitions (boxes, $\mathcal P_n$ , the kernel, the estimator, $J_n$ , $d$ ) live in one definition file. $\mathcal P_n$ duplicates, with weights $1/n$ , the distribution set of mission I; the duplication is deliberate because draft missions cannot import each other.
Welcome contributions: the kernel density estimator and its strong $L^1$ consistency as reusable infrastructure, and any of the deterministic milestones.

Selected references

H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
L. Devroye, The equivalence of weak, strong and complete convergence in $L_1$ for kernel density estimates, Annals of Statistics 11(3):896–904, 1983.
L. Devroye, L. Györfi, Nonparametric Density Estimation: The $L_1$ View, Wiley, 1985.
A. J. King, R. J.-B. Wets, Epi-consistency of convex stochastic programs, Stochastics and Stochastic Reports 34(1), 1991 (reference [22] of the paper).

7 thms4 active usersReviewed

Completed

Linear Optimization Optimization Probability·Captain: mikedeng1

Robust solutions of Linear Programming problems contaminated with uncertain data: A Violation-Probability Bound for the Robust CounterpartResearch Paper

Motivation

Linear programs solved in practice carry data that are measured, estimated or rounded. Ben-Tal and Nemirovski (Math. Program. 88, 2000) examined the NETLIB collection of real-world LPs and found that in 13 of them a relative perturbation of only 0.01% in the "ugly" coefficients of the inequality constraints can make the nominal optimal solution more than 50% infeasible (§2.3). Their remedy is the robust counterpart methodology: replace the nominal problem by a deterministic problem whose feasible solutions remain nearly feasible for every, or for all but a small probability of, data realizations.

The paper made the approach concrete for entry-wise uncertainty and gave the probabilistic guarantee that became a standard tool of robust and chance-constrained optimization. The main steps of the history are:

1973, A. L. Soyster: the interval (worst-case, "box") counterpart, here called (IRC).
1998–1999, Ben-Tal and Nemirovski (Math. Oper. Res. 23; Oper. Res. Lett. 25), and independently El Ghaoui and co-authors: robust optimization with ellipsoidal uncertainty sets.
2000, this paper: the ellipsoid-plus-box counterpart (RC[ε, δ, Ω]) and Proposition 1, which bounds each constraint's violation probability by $\exp\{-\Omega^2/2\}$ under independent symmetric perturbations.
2004, Bertsimas and Sim (Oper. Res. 52): the budgeted counterpart, with an analogous probability bound.

Setting

An uncertain linear program is

\text{minimize } c^Tx\quad\text{s.t.}\quad Ex=e,\qquad Ax\le b,\qquad \ell\le x\le u,\tag{LP}

with $x\in\mathbb{R}^n$ , $E\in\mathbb{R}^{p\times n}$ , $A=(a_{ij})\in\mathbb{R}^{m\times n}$ , and bounds $\ell_j\in\mathbb{R}\cup\{-\infty\}$ , $u_j\in\mathbb{R}\cup\{+\infty\}$ . For each inequality row $i$ a set $J_i\subseteq\{1,\dots,n\}$ lists the uncertain entries $a_{ij}$ , $j\in J_i$ . Only these entries are uncertain; $E,e,b,\ell,u,c$ are exact.

Given an uncertainty level $\epsilon>0$ and a feasibility tolerance $\delta>0$ , write $b_i^+=b_i+\delta\max[1,|b_i|]$ .

$x$ is reliable if it is feasible for (LP) and $\sum_{j\notin J_i}a_{ij}x_j+\sum_{j\in J_i}\tilde a_{ij}x_j\le b_i^+$ for every $i$ and every choice of $\tilde a_{ij}$ with $|\tilde a_{ij}-a_{ij}|\le\epsilon|a_{ij}|$ .
In the random symmetric uncertainty model, the true coefficients are $\tilde a_{ij}=(1+\epsilon\xi_{ij})a_{ij}$ , where $\xi_{ij}=0$ for $j\notin J_i$ and, for each row $i$ , $\{\xi_{ij}\}_{j\in J_i}$ are independent random variables, each symmetrically distributed in $[-1,1]$ .
$x$ is almost reliable with level $\kappa$ if it is feasible for (LP) and $\Pr\{\sum_j\tilde a_{ij}x_j>b_i^+\}\le\kappa$ for every $i$ .

The robust counterpart (RC[ε, δ, Ω]), with a safety parameter $\Omega>0$ , has variables $x_j$ , $y_{ij}$ , $z_{ij}$ and constraints $Ex=e$ , $Ax\le b$ , $\ell\le x\le u$ , $-y_{ij}\le x_j-z_{ij}\le y_{ij}$ for all $i,j$ , and

\sum_j a_{ij}x_j+\epsilon\Big[\sum_{j\in J_i}|a_{ij}|y_{ij}+\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2z_{ij}^2}\Big]\le b_i^+\qquad\forall i.

The interval robust counterpart (IRC[ε, δ]) has variables $x_j,y_j$ and the constraint $\sum_ja_{ij}x_j+\epsilon\sum_{j\in J_i}|a_{ij}|y_j\le b_i^+$ with $-y_j\le x_j\le y_j$ , besides the nominal ones. Problem (∗) is the same with $y_j$ replaced by $|x_j|$ .

Formalization targets

Goal: Proposition 1 (pp. 418–419)

If $x$ extends to a feasible solution $(x,y,z)$ of (RC[ε, δ, Ω]), then $x$ is feasible for (LP) and, for every $i$ ,

\Pr\Big\{\sum_j(1+\epsilon\xi_{ij})a_{ij}x_j>b_i+\delta\max[1,|b_i|]\Big\}\le\exp\{-\Omega^2/2\}.

Milestones

The reduction in the proof of Proposition 1 (p. 419), in corrected pointwise form: a violation of row $i$ forces $\sum_{j\in J_i}\xi_{ij}a_{ij}z_{ij}>\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2z_{ij}^2}$ .
Eq. (1), p. 419: for independent symmetric $\eta_j\in[-1,1]$ and reals $p_j$ ,

\Pr\Big\{\sum_j\eta_jp_j>\Omega\sqrt{\textstyle\sum_jp_j^2}\Big\}\le\exp\{-\Omega^2/2\}.

$x$ is reliable iff it is feasible for (∗) (p. 417).
(∗) is equivalent to (IRC[ε, δ]) (pp. 417–418).
Every feasible solution of (IRC) yields one of (RC) with $y_{ij}=y_j$ , $z_{ij}=0$ (p. 420).
Feasibility for (LP) together with $\sum_ja_{ij}x_j+\epsilon\beta_i(x)\le b_i^+$ , $\beta_i(x)=\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2x_j^2}$ , suffices to extend $x$ to (RC) (p. 420).
The ratio $\alpha_i(x)/\beta_i(x)$ , $\alpha_i(x)=\sum_{j\in J_i}|a_{ij}||x_j|$ , is at most $\sqrt{\mathrm{card}(J_i)}/\Omega$ , with equality attained (p. 420, corrected).

Significance

Proposition 1 turns a probabilistic requirement, which is hard to handle directly, into a single convex (second-order-cone) program. The bound $\exp\{-\Omega^2/2\}$ does not depend on the dimension, on the number of uncertain entries, or on which symmetric distributions the perturbations follow, so $\Omega$ can be chosen from the desired reliability level alone. Together with milestones 3–6, the mission certifies the whole chain: the worst-case notion of reliability is exactly Soyster's linear program (IRC), and (RC) is never more conservative than (IRC), with an advantage that can reach the factor $\sqrt{\mathrm{card}(J_i)}/\Omega$ .

The results are proved in the paper; to our knowledge none of them is machine-checked. A formal development produces a reusable model of entry-wise uncertain LPs, the counterparts (∗), (IRC) and (RC) as Lean predicates, and a Hoeffding-type bound for weighted sums of symmetric bounded variables in the exact form (1). The platform's HighDimProb.Concentration.hoeffding_rademacher covers the Rademacher special case only.

Difficulty

The deterministic parts (milestones 1, 3–7) are elementary: worst cases of interval perturbations, and the Cauchy–Schwarz inequality. The obstacle lies in the probabilistic step. The printed proof passes from $\xi_{ij}a_{ij}$ to $\xi_{ij}|a_{ij}|$ with an equality that holds only in distribution, and contains index misprints, so it cannot be transcribed line by line; the reduction has to be restated pointwise. Eq. (1) is a tail bound for general symmetric variables in $[-1,1]$ , not only for random signs; the step (c) of the printed proof of (1) is written as an equality that holds only for random signs, so that proof too needs repair. The degenerate case $\sum_jp_j^2=0$ must be handled rather than assumed away.

Formalization scope

Data are a structure UncertainLP n p m over Fin indices (0-based), with A : Matrix (Fin m) (Fin n) ℝ, J : Fin m → Finset (Fin n) arbitrary, and EReal bounds so that infinite bounds are expressible. The objective $c$ is omitted: no statement involves it.
The probability space is $(S,\mathbb P)$ with IsProbabilityMeasure; the name $S$ avoids a clash with the safety parameter $\Omega$ . Symmetry is equality of the laws of $\xi_{ij}$ and $-\xi_{ij}$ ; values lie in $[-1,1]$ at every outcome; independence is required within each row only, with no identical distribution (§3.1 says only "independent", which is weaker than the "iid" of §2.2). Probabilities are P.real.
The hypotheses $\epsilon>0$ , $\delta>0$ , $\Omega>0$ are the paper's standing assumptions and are carried by every theorem that mentions the parameter.
Corrections of the printed text: $a_{ij}x_i\to a_{ij}x_j$ in (IRC); $\sum_{j\in J}\to\sum_{j\in J_i}$ in (RC); the reduction of milestone 1 is stated with $a_{ij}$ and $z_{ij}$ in place of the printed $|a_{ij}|$ , $x_i-y_{ij}$ and $y_j$ , $y_{ij}$ ; and the ratio of milestone 7 carries the factor $1/\Omega$ that the printed " $\sqrt{\mathrm{card}(J_i)}$ " omits.
Ruling out trivializations: the violation event uses the signed multiplicative model $(1+\epsilon\xi_{ij})a_{ij}$ , never $|a_{ij}|$ or an additive perturbation; the goal concludes both nominal feasibility (i) and the probability bound (ii′) for every row; no hypothesis excludes the degenerate case $\sum_{j\in J_i}a_{ij}^2z_{ij}^2=0$ ; and the probability model is satisfiable (e.g. by $\xi\equiv0$ or by Rademacher signs), so the goal is not vacuous.
The numerical remarks of the paper (0.92, 5.24, $10^{-6}$ , "at least 30") and the NETLIB case study are not formalized.
Reusable beyond this mission: the uncertain-LP model and the three counterparts, and the tail bound (1). Contributions of general lemmas about symmetric bounded random variables are welcome.

Selected references

A. Ben-Tal, A. Nemirovski, Robust solutions of Linear Programming problems contaminated with uncertain data, Math. Program. Ser. A 88 (2000) 411–424. https://doi.org/10.1007/s101070000163
A. L. Soyster, Convex programming with set-inclusive constraints and applications to inexact linear programming, Oper. Res. 21 (1973) 1154–1157. https://doi.org/10.1287/opre.21.5.1154
A. Ben-Tal, A. Nemirovski, Robust convex optimization, Math. Oper. Res. 23 (1998) 769–805. https://doi.org/10.1287/moor.23.4.769
A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Oper. Res. Lett. 25 (1999) 1–13. https://doi.org/10.1016/S0167-6377(99)00016-4
D. Bertsimas, M. Sim, The price of robustness, Oper. Res. 52 (2004) 35–53. https://doi.org/10.1287/opre.1030.0065
W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

12 thms4 active usersReviewed

Completed

Algorithmic Game Theory Linear Optimization·Captain: mikedeng1

The Assignment Game I: The Core 2: The High-Price and Low-Price Corners of the CoreResearch Paper

Motivation

A two-sided market in which each seller owns one indivisible good (a house, in the paper's example) and each buyer wants at most one is the simplest model in which prices emerge from bargaining between individuals rather than from a supply curve. Shapley and Shubik, The Assignment Game I: The Core (Int. J. Game Theory 1 (1971)), treat this market as a cooperative game with transferable utility and describe its core, the set of payoff divisions that no group of traders can improve upon by trading among themselves. The paper is the foundation of the literature on assignment markets, auctions of heterogeneous items, and two-sided matching with money.

This mission formalizes the paper's structural result on the shape of the core, Theorem 3 (p. 121): among all core outcomes there is a high-price corner in which every seller simultaneously receives the highest payoff available in the core and every buyer the lowest, and a low-price corner with the roles reversed; these two corners are the farthest-apart pair of core points. The authors note (p. 121, footnote 2) that a similar theorem for markets without money is proved by Gale and Shapley (1962), where it becomes the existence of seller-optimal and buyer-optimal stable matchings.

Setting

Let $M$ be a finite set of sellers and $N$ a finite set of buyers, with $m = |M|$ and $n = |N|$ not necessarily equal. For each seller $i$ and buyer $j$ a number $a_{ij} \ge 0$ is given: the gain the pair can realize by trading (Eq. (2.5), p. 114; Sec. 2.3, p. 116).

A coalition $S \subseteq M \cup N$ is described by its seller part $A = S \cap M$ and buyer part $B = S \cap N$ . A matching inside $(A, B)$ is a set $P \subseteq A \times B$ of seller–buyer pairs in which no player occurs twice. The characteristic function (Eq. (2.6), p. 115) gives the coalition the best total gain it can realize by pairing its members:

\operatorname{worth}(A, B) = \max_{P \text{ matching in } (A,B)} \sum_{(i,j) \in P} a_{ij}.

A matching of the whole market attaining $\operatorname{worth}(M, N)$ is an optimal assignment.

A payoff vector is a pair $(u, v)$ with $u \in \mathbb{R}^M$ (sellers' payoffs) and $v \in \mathbb{R}^N$ (buyers' payoffs). The core (p. 118) consists of the payoff vectors with

\sum_{i \in M} u_i + \sum_{j \in N} v_j = \operatorname{worth}(M, N) \quad (3.5), \qquad \sum_{i \in A} u_i + \sum_{j \in B} v_j \ge \operatorname{worth}(A, B) \ \text{ for all } A \subseteq M,\ B \subseteq N \quad (3.6).

Singleton coalitions have worth $0$ , so core vectors are nonnegative; the paper calls them "imputations in the core".

For a seller $i$ , write $u^*_i$ and $u_{*i}$ for the highest and lowest value of $u_i$ over the core; for a buyer $j$ , write $v^*_j$ and $v_{*j}$ likewise.

Formalization targets

Goal: Theorem 3 (p. 121)

The low-price corner $(u_*, v^*)$ and the high-price corner $(u^*, v_*)$ are in the core, and for all core vectors $(u', v')$ , $(u'', v'')$ ,

\sum_{i \in M} (u'_i - u''_i)^2 + \sum_{j \in N} (v'_j - v''_j)^2 \le \sum_{i \in M} (u_{*i} - u^*_i)^2 + \sum_{j \in N} (v^*_j - v_{*j})^2 .

Milestones, in attack order

Sec. 3.2, p. 118 — the core is nonempty.
Sec. 3.3, p. 120 — the core is closed, convex and bounded (a polytope).
Sec. 3.3, proof of the Lemma, p. 121 — on an optimal assignment $P$ , every core vector has $u_i + v_j = a_{ij}$ for $(i, j) \in P$ and pays $0$ to players $P$ leaves unassigned.
Lemma, p. 121 — for core vectors $(u', v')$ , $(u'', v'')$ , the vectors $(\min(u', u''), \max(v', v''))$ and $(\max(u', u''), \min(v', v''))$ (coordinatewise) are in the core.
Sec. 3.3, p. 122 — any two core vectors satisfy $|u'_i - u''_i| \le u^*_i - u_{*i}$ and $|v'_j - v''_j| \le v^*_j - v_{*j}$ for every $i$ and $j$ .

Milestone 5 is the strongest form of the distance clause of the goal: it gives the same conclusion for every distance that depends only on the absolute values of the coordinate differences, as the paper remarks on p. 122.

Significance

The result. Theorem 3 says that the core of an assignment market is elongated along the direction of market-wide price movements: "intergroup allocations are relatively indeterminate, intragroup allocations are relatively precise" (p. 121). The high-price corner is the outcome most favourable to all sellers at once, and the low-price corner the one most favourable to all buyers; that such simultaneous optima exist is a property of this game, not of cores in general. The low-price corner, the buyers' optimum, is the outcome reached by the ascending multi-item auction of Demange, Gale and Sotomayor (J. Polit. Econ. 94 (1986)), and the lattice structure underlies the incentive analysis of assignment mechanisms.

Formalizing it. The theorem is classical and fully proved in the paper; Prove2Me has no formalization of it, and nothing on the platform treats transferable-utility assignment games (the platform's stable-matching material concerns the non-transferable-utility model). The mission produces a reusable definition of the assignment game and its core, the lattice property of the core, and the extremal-corner theorem, stated with the core's extrema defined intrinsically rather than as parameters.

Difficulty

The proof in the paper takes a finite family of core vectors realizing all the extremal values and applies the Lemma repeatedly (p. 122). That argument presupposes that each extremum $u^*_i$ , $u_{*i}$ , $v^*_j$ , $v_{*j}$ is attained by some core vector, which the paper takes from the core being a nonempty polytope without stating it separately. Nonemptiness is itself the substantive result of the paper's linear-programming analysis (Theorem 2, via the duality theorem and the integrality of the assignment polytope), and it is not available here as a black box. The other nontrivial point is the Lemma's efficiency claim: that the coordinatewise min/max vectors still distribute exactly $\operatorname{worth}(M, N)$ , which depends on the structure of an optimal assignment and fails for the naive combination $(\max(u', u''), \max(v', v''))$ .

Formalization scope

Players and matrix. $M$ and $N$ are arbitrary finite types (Fintype); either may be empty and $m \ne n$ is allowed. The matrix is a : M → N → ℝ, and every theorem carries the paper's standing assumption $a_{ij} \ge 0$ as a hypothesis. No other hypothesis is added.
Coalitions are pairs (A, B) : Finset M × Finset N. Matchings are finsets of pairs with injective projections. The paper maximizes over exactly $k = \min(|S \cap M|, |S \cap N|)$ disjoint pairs; the formalization maximizes over matchings of every size, which gives the same value because $a_{ij} \ge 0$ .
Naming. The characteristic function is worth, since v denotes buyers' payoffs.
Core is a Set ((M → ℝ) × (N → ℝ)) defined by (3.5) and (3.6) over all coalitions, with no separate nonnegativity clause (it follows from singleton coalitions).
Extremal payoffs uHi, uLo, vHi, vLo are sSup/sInf in ℝ of the image of the core under a coordinate. On an empty or unbounded set these return $0$ ; the goal does not assume the core nonempty or bounded, so it is not vacuous and does not hide milestones 1–2 as hypotheses. The goal's membership clauses imply attainment of the extrema.
Distance. The goal uses the Euclidean distance on $\mathbb{R}^M \times \mathbb{R}^N$ through sums of squared coordinate differences. Lean's default dist on a product of function types is the sup-distance and is not used.
Ruled out. A formalization in which $u^*, u_*, v^*, v_*$ are free parameters constrained only by the conclusion, or in which the goal assumes a nonempty bounded core, would trivialize or weaken Theorem 3; the extrema here are computed from the core.
Not formalized. The dimension statements of p. 120 ("typically equal to min(m,n)") are informal. The LP characterization of the core (Theorem 2) is the subject of the companion mission of this series and is not restated.
Welcome contributions. Lemmas about matchings inside coalitions (injectivity, sums over images), the implication "dual feasible $\Rightarrow$ coalitionally rational", and general facts about sSup/sInf of compact coordinate images are reusable for any assignment-market or TU-matching development.

Selected references

L. S. Shapley and M. Shubik, The Assignment Game I: The Core, International Journal of Game Theory 1 (1971), 111–130. https://doi.org/10.1007/BF01753437
D. Gale and L. S. Shapley, College Admissions and the Stability of Marriage, American Mathematical Monthly 69 (1962), 9–15. https://doi.org/10.2307/2312726
G. Demange, D. Gale and M. Sotomayor, Multi-Item Auctions, Journal of Political Economy 94 (1986), 863–872. https://doi.org/10.1086/261393
G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963. https://doi.org/10.1515/9781400884179

7 thms4 active usersReviewed

Completed

Control Theory Dynamic Programming Optimization·Captain: mikedeng1

Robust Control of Markov Decision Processes with Uncertain Transition Matrices 1: Perfect Duality and the Robust Dynamic Programming Recursion for Finite-Horizon MDPsResearch Paper

Motivation

A Markov decision process (MDP) is solved by dynamic programming once its transition probabilities are known. In practice they are estimated from data, and the optimal policy of an MDP can be sensitive to estimation error: a policy computed from point estimates may perform much worse under the true transition matrices. Nilim and El Ghaoui (Oper. Res. 53(5), 2005) study the robust version of the problem, in which the controller minimises the worst-case expected cost when the transition matrices are only known to lie in given uncertainty sets, and motivate it with aircraft routing under uncertain weather.

Earlier work on MDPs with uncertain transition probabilities includes Satia and Lave (1973) and White and Eldeib (1994), which treat interval and set-valued transition models, and Givan, Leach and Dean (1997) on bounded-parameter MDPs. The robust Bellman recursion under a rectangularity assumption was obtained independently by Iyengar (Columbia technical report 2002, published as Robust dynamic programming, Math. Oper. Res. 30(2), 2005). This mission targets the finite-horizon result of Nilim and El Ghaoui: Theorem 1, which shows that the robust problem is solved by a recursion of the same shape as the nominal one and that the associated min–max game has a value.

Setting

The states form a finite set $\mathcal X=\{1,\dots,n\}$ , the decision horizon is $T=\{0,1,\dots,N-1\}$ , and the action set $\mathcal A$ is finite, nonempty and the same in every state. Costs are $c_t(i,a)\ge0$ for $t\in T$ , and there is a terminal cost $c_N(i)$ . The system starts in a given state $i_0$ .

Write $\Delta_n=\{p\in\mathbb R^n_+ : p^{\mathsf T}\mathbf 1=1\}$ for the probability simplex. For every action $a$ and state $i$ , a nonempty set $\mathcal P_i^a\subseteq\Delta_n$ describes the possible $i$ -th rows of the transition matrix under $a$ . No convexity or closedness is assumed. The rectangular uncertainty property says the uncertainty set of the matrix $P^a$ is the product $\mathcal P^a=\mathcal P_1^a\times\cdots\times\mathcal P_n^a$ .

A controller policy $\pi=(\mathbf a_0,\dots,\mathbf a_{N-1})$ consists of maps $\mathbf a_t:\mathcal X\to\mathcal A$ , and $\Pi=\mathcal A^{nN}$ is the set of such policies. A policy of nature $\tau=(P_t^a)_{a\in\mathcal A,t\in T}$ picks, for every stage, action and state, a row $p_i^a(t)\in\mathcal P_i^a$ . The admissible set is $\mathcal T=(\bigotimes_a\mathcal P^a)^N$ , so nature may change the matrices from stage to stage. The expected total cost is

C_N(\pi,\tau)=\mathbf E\Big(\sum_{t=0}^{N-1}c_t(i_t,\mathbf a_t(i_t))+c_N(i_N)\Big),

where the state $i_t$ evolves as a Markov chain with transition matrix $P_t^{\mathbf a_t(i)}$ from state $i$ . The support function of a set $\mathcal P$ is $\sigma_{\mathcal P}(v)=\sup\{p^{\mathsf T}v : p\in\mathcal P\}$ . The robust recursion (7) starts from $v_N=c_N$ and sets

v_t(i)=\min_{a\in\mathcal A}\big(c_t(i,a)+\sigma_{\mathcal P_i^a}(v_{t+1})\big),

and for a fixed $\pi$ the evaluation recursion (10) starts from $v_N^\pi=c_N$ and sets $v_t^\pi(i)=c_t(i,\mathbf a_t(i))+\sigma_{\mathcal P_i^{\mathbf a_t(i)}}(v_{t+1}^\pi)$ .

Formalization targets

Goal: Theorem 1 (Robust Dynamic Programming)

\min_{\pi\in\Pi}\sup_{\tau\in\mathcal T}C_N(\pi,\tau)=v_0(i_0)=\sup_{\tau\in\mathcal T}\min_{\pi\in\Pi}C_N(\pi,\tau),

together with three further statements. First, $\sup_{\tau}C_N(\pi,\tau)=v_0^\pi(i_0)$ for every $\pi$ . Second, every policy that chooses actions attaining the minimum in (7) (rule (8)) achieves $v_0(i_0)$ in the worst case. Third, every nature policy whose rows attain the suprema $\sigma_{\mathcal P_i^a}(v_{t+1})$ (rule (9)) forces the value $v_0(i_0)$ on every controller.

Milestones

Lemma 1: a problem $\max q^{\mathsf T}v_0$ subject to $v_t\le g_t(v_{t+1})$ with monotone $g_t$ and $q\ge0$ is solved by the recursion $v_t=g_t(v_{t+1})$ .
Support functions of nonempty subsets of $\Delta_n$ are componentwise nondecreasing.
The constraint maps of problems (15) and (16) are componentwise nondecreasing.
Eq. (14): for fixed $\pi$ and fixed matrices, $C_N(\pi,\tau)$ is the value of a linear program.
Eq. (16): $\sup_{\tau\in\mathcal T}C_N(\pi,\tau)=v_0^\pi(i_0)$ .
Eq. (15): $\sup_{\tau\in\mathcal T}\min_{\pi}C_N(\pi,\tau)=v_0(i_0)$ .

Significance

Theorem 1 shows that, under rectangular uncertainty, robustness costs one inner optimisation per state and action: the expected continuation cost $p^{\mathsf T}v_{t+1}$ of nominal dynamic programming is replaced by the support function $\sigma_{\mathcal P_i^a}(v_{t+1})$ . The equality of the min–max and max–min values says that it does not matter whether nature commits before or after the controller. The optimal controller policy remains deterministic and Markov. The later sections of the paper build on this recursion. They cover the discounted infinite-horizon case, the gap between stationary and time-varying uncertainty, and the computation of $\sigma$ for likelihood and entropy models, which the other missions of this series formalize.

The result is proved in the paper, and independently by Iyengar. It has no machine-checked proof that this mission is aware of. A formal proof yields a reusable development: a finite-horizon MDP with a forward-defined expected cost, the link between that expectation and backward linear programs, and the finite-horizon robust Bellman equation for arbitrary nonempty uncertainty sets.

Difficulty

The nominal Bellman recursion is standard. The robust statement is harder than "apply the nominal recursion under the worst matrix", because no single worst matrix need exist. The sets $\mathcal P_i^a$ are neither closed nor convex, so the suprema in $\sigma$ need not be attained, and $\mathcal T$ is not compact. Minimax theorems for convex–concave or compact games therefore do not apply. The expected cost is defined forward, as an expectation over a Markov chain, while the recursions run backward, and connecting the two is part of the work. The max–min side needs nature policies that come within any tolerance of the value simultaneously at every stage, state and action.

Formalization scope

States are Fin n and stages Fin N. Values $v_0,\dots,v_N$ are indexed by natural numbers, and only $t\le N$ is meaningful. Vectors are Fin n → ℝ with the componentwise order.
The model is a structure holding the costs ( $c_t\ge0$ ), the terminal cost (no sign assumed), and the row sets. Every row set must be nonempty and contained in stdSimplex ℝ (Fin n). Nonemptiness is implicit in the paper: without it $\mathcal T$ is empty, and a real supremum over an empty index is $0$ .
Rectangularity is built in: a nature policy is a function $\tau(t,a,i)$ with $\tau(t,a,i)\in\mathcal P_i^a$ . Nature does not observe the realised trajectory, and stationary nature ( $\mathcal T_s$ ) is not the set used here.
$C_N$ is defined by the forward state distribution, not by a backward recursion. Defining it backward would make the evaluation statements hold by definition, which is the trivializing formalization this choice rules out.
$\sigma_{\mathcal P}$ is the real sSup of $\{p^{\mathsf T}v\}$ . This is the true supremum because the set is nonempty and bounded above by $\max_j v_j$ .
Maxima over nature are suprema: ⨆ τ in the goal and IsLUB in the milestones, because the row sets need not be closed. Minima over the finite nonempty $\Pi$ and over $\mathcal A$ are ⨅. The argmax rule (9) is stated only for nature policies attaining the row suprema. The argmin rule (8) is stated for every attaining policy.
The terminal value $v_N=c_N$ is not printed in Theorem 1. It is taken from the proof and from Step 1 of the paper's algorithm (p. 785). The composition $g_1\circ\cdots\circ g_N$ in Lemma 1 is read as $g_0\circ\cdots\circ g_{N-1}$ .
Not included: Corollary 1 (the sequential game) and the accuracy part of Theorem 2. Contributions of either as additional theorems on these definitions are welcome.

Selected references

A. Nilim, L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
J. K. Satia, R. E. Lave, Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
C. C. White, H. K. Eldeib, Markov Decision Processes with Imprecise Transition Probabilities, Operations Research 42(4):739–749, 1994. https://doi.org/10.1287/opre.42.4.739
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

11 thms4 active usersReviewed

Operations Research

Missions

Theory of Games and Economic Behavior IV: The Characteristic Function of a Zero-Sum n-Person GameTextbook

Motivation

Setting

Formalization targets

Goal: the characterization of characteristic functions (26.2)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Theory of Games and Economic Behavior III: Mixed Strategies, the Minimax Theorem and Good StrategiesTextbook

Motivation

Setting

Formalization targets

Goal: (17:D), good strategies characterized by their supports

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Theory of Games and Economic Behavior I: Numerical Utility from the Axioms of Preference and MixtureTextbook

Motivation

Setting

Formalization targets

Goal: (A:V) and (A:W), p. 627

Milestones

Significance

Difficulty

Formalization scope

Selected references

Numerical Techniques for Stochastic Optimization II: Logarithmic Concavity of Probabilistic ConstraintsTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 5.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Numerical Techniques for Stochastic Optimization I: Edmundson–Madansky Bounds for Independent Random Data and Simple RecourseTextbook

Motivation

Setting

Formalization targets

Goal: the Edmundson–Madansky bound for independent components (p. 46)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Introduction to the Scenario Approach I: The Violation Distribution of the Scenario SolutionTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 3.7

Milestones

Significance

Difficulty

Formalization scope

Selected references

Algorithmic Mechanism Design I: MinWork Is a Strongly Truthful n-Approximation Mechanism for Task Scheduling on Unrelated MachinesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Selected Topics in Column Generation III: Ryan–Foster Branching — a Fractional Basic Set-Partitioning Solution Covers Some Row Pair FractionallyResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3 (p. 1020)

Milestone: the branches keep every integer solution (§7.3, p. 1020)

Significance

Difficulty