Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Quantum Max-Cut

Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph $G$ with nonnegative rational edge weights, write

H_G=\sum_{i<j}w_{ij}(I-\mathrm{SWAP}_{ij}),\qquad\mathrm{OPT}(G)=\lambda_{\max}(H_G).

This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed $G$ , let $R$ be the algorithm's internal fair random bits, and let $v(G,R)$ be its nonnegative rational output. A ratio $\alpha$ requires

0\le v(G,R)\le\mathrm{OPT}(G)\quad\text{for every random outcome }R,

\mathbb E_R[v(G,R)]\ge\alpha\,\mathrm{OPT}(G).

The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.

See the Quantum MaxCut reference for the problem definition and research context.

≥ 0.5Formalized record≥ 0.526Open frontier

3 provers on it3 of 8 missions formalized

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.13981Formalized record≥ 2.15Open frontier

11 provers on it22 of 23 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 2Formalized record

19 provers on it9 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 4Formalized record≤ 2Open frontier

8 provers on it17 of 18 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 19Formalized record≤ 5Open frontier

42 provers on it17 of 19 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns

See all campaigns →

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Quantum Max-Cut

Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph $G$ with nonnegative rational edge weights, write

H_G=\sum_{i<j}w_{ij}(I-\mathrm{SWAP}_{ij}),\qquad\mathrm{OPT}(G)=\lambda_{\max}(H_G).

0\le v(G,R)\le\mathrm{OPT}(G)\quad\text{for every random outcome }R,

\mathbb E_R[v(G,R)]\ge\alpha\,\mathrm{OPT}(G).

The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.

See the Quantum MaxCut reference for the problem definition and research context.

≥ 0.5Formalized record≥ 0.526Open frontier

3 provers on it3 of 8 missions formalized

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.13981Formalized record≥ 2.15Open frontier

11 provers on it22 of 23 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 2Formalized record

19 provers on it9 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 4Formalized record≤ 2Open frontier

8 provers on it17 of 18 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 19Formalized record≤ 5Open frontier

42 provers on it17 of 19 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Algorithmic Game Theory Operations Research Optimization+1·Captain: mikedeng1

A Supply Chain Theory of Factoring and Reverse Factoring 1: The Supplier's Equilibrium Choice Among Recourse, Non-Recourse and Reverse FactoringResearch Paper

Motivation

Small and medium-sized suppliers that sell to large retailers typically ship first and are paid weeks or months later. Until the invoice is paid, the supplier's cash is trapped in accounts receivable, while production has to be financed up front. Factoring (selling or pledging the receivable to a financial intermediary for immediate cash) and reverse factoring (a buyer-initiated program in which the retailer approves the invoice and the supplier is paid early by the retailer's bank) are the standard remedies, and reverse factoring programs of large buyers are often coupled with an extension of payment terms. Which of these instruments a supplier should use, and how the answer depends on the credit ratings of the two firms, is the question addressed by Kouvelis and Xu, "A Supply Chain Theory of Factoring and Reverse Factoring", Management Science 67(10):6071–6088, 2021 (doi:10.1287/mnsc.2020.3788). The paper embeds each financing scheme in the pull wholesale-price game of Cachon (2004) and compares the resulting equilibria.

Setting

A retailer (the Stackelberg leader) offers a wholesale price $w$ to a capital-constrained supplier (the follower), who then chooses a production quantity $q \ge 0$ and carries the inventory; the retail price $p$ is fixed, and $0 < c < p$ is the unit production cost. Demand $D \ge 0$ has density $f$ , complementary distribution function $\bar F$ , finite mean, $f > 0$ on $[0, \mathbb Z]$ ( $\mathbb Z \le +\infty$ ), and a strictly increasing failure rate $z = f/\bar F$ (strict IFR). Expected sales are $S(q) = \int_0^q \bar F(\xi)\,d\xi$ , and $k(q) = S(q)/\bar F(q)$ .

Each firm $j \in \{s, r\}$ has a credit rating $C_j \in (C_{\min}, C_{\max})$ . The default probability $\rho_j = \rho(C_j) \in [0,1]$ is strictly decreasing in the rating, and the interest-rate premium $\eta_j = \eta(C_j) > 0$ is decreasing. Production takes a lead time $t_1$ , payment follows after a term $t_2$ , and the supplier faces a Poisson liquidity shock of rate $\lambda_s$ during production (the retailer, rate $\lambda_r$ ). Under a scheme $i \in \{\mathcal F, \mathcal N, \mathcal R\}$ (recourse, non-recourse, reverse factoring, the last with a payment extension $\tau \ge 0$ ), the supplier's expected profit is

\pi_i(q; w) = (1-\rho_s)\big(\Lambda_i e^{-\lambda_s t_1} w S(q) - c q e^{\eta_s t_1}\big),

with coefficients $\Lambda_{\mathcal F} = (1-\rho_r) + (1-\rho_s) - e^{\eta_s t_2}$ , $\Lambda_{\mathcal N} = e^{-\eta_r t_2}(1-\rho_r)$ , $\Lambda_{\mathcal R} = e^{-\eta_r(t_2+\tau)}$ , and effective unit cost $c_i = c\,e^{(\eta_s+\lambda_s)t_1}/\Lambda_i$ . The retailer's profit is $e^{-\lambda_s t_1}(1-\rho_r)(p-w)S(q)$ under factoring and carries the extra factor $2 - e^{-\lambda_r \tau}$ under reverse factoring.

Formalization targets

Goal: Proposition 5

For a given $\tau \ge 0$ , let $\mathbb C_3$ be the unique supplier rating with $\Lambda_{\mathcal F} = \Lambda_{\mathcal R}$ , $\mathbb C_1$ the one with $\Lambda_{\mathcal F} = \Lambda_{\mathcal N}$ , and $\mathbb C_{\mathcal F}, \mathbb C_{\mathcal N}, \mathbb C_{\mathcal R}$ the feasibility thresholds ( $c_i = p$ ). With all three schemes available,

e^{-\eta_r\tau} < 1-\rho_r:\quad \mathcal F \text{ adopted} \iff C_s > \mathbb C_{\mathcal F}\vee\mathbb C_1,\qquad \mathcal N \text{ adopted} \iff \mathbb C_{\mathcal N} < C_s \le \mathbb C_1;

1-\rho_r \le e^{-\eta_r\tau}:\quad \mathcal F \text{ adopted} \iff C_s > \mathbb C_{\mathcal F}\vee\mathbb C_3,\qquad \mathcal R \text{ adopted} \iff \mathbb C_{\mathcal R} < C_s \le \mathbb C_3.

Milestones

Proposition 2 (p. 6078): recourse factoring is feasible iff $C_s > \mathbb C_{\mathcal F}$ , and then the unique equilibrium solves $p\bar F(q) = c_{\mathcal F}[1+z(q)k(q)]$ , $w = c_{\mathcal F}/\bar F(q)$ .
Proposition 3 (p. 6079): the same for non-recourse factoring with $c_{\mathcal N}$ .
§5.2 (p. 6082, Proposition EC.2): the same for reverse factoring with $c_{\mathcal R}(\tau)$ .
§4.4 (p. 6080, Lemma EC.2): between feasible schemes, the supplier's equilibrium profits are ordered as the $\Lambda_i$ .
Proposition 4 (p. 6080): the choice between $\mathcal F$ and $\mathcal N$ alone.

A follow-on item states Corollary 1(i) (p. 6081): when the retailer's rating is at least the supplier's, non-recourse factoring strictly dominates recourse factoring whenever the latter is feasible.

Significance

Proposition 5 is the paper's main prediction: non-recourse factoring is the choice of medium-rated suppliers, recourse factoring of highly rated ones, and reverse factoring with a fixed payment extension is chosen only by low-to-medium-rated suppliers and only if the retailer's rating is not too high relative to the extension. The paper uses it to explain the documented reluctance of suppliers to join reverse-factoring programs that come with extended payment terms (Wuttke, Rosenzweig and Heese 2019; Corsten 2010, a teaching case), and it is the starting point of the paper's Proposition 6 on the retailer's optimal payment extension, which is the subject of the second mission of this series.

The results are proved in the paper's Online Appendix B. To the best of available knowledge none of them, and no model of supply chain finance, has a machine-checked proof. A formal development would also supply a reusable treatment of the pull wholesale-price game under a strictly IFR demand with an arbitrary effective unit cost, of which Propositions 2, 3 and EC.2 are three instances.

Difficulty

The case analysis of Proposition 5 is short once the milestones are available; the substance lies in them. Proposition 2 requires solving a bilevel problem: the follower's best response has to be identified for every wholesale price, including prices at which the supplier produces nothing, and the leader's objective has to be shown to have a single maximizer. The natural route through the first-order condition needs the IFR property to exclude multiple stationary points, and it has to cope with a support end $\mathbb Z$ that may be finite (where $\bar F$ vanishes and $k$ , $z$ lose meaning) or infinite. Lemma EC.2 requires the equilibrium supplier profit as an explicit function of the effective cost and a monotonicity argument for it; comparing the $\Lambda_i$ directly, without the equilibrium, does not prove it. The proofs themselves are not in the main text.

Formalization scope

Demand is a probability measure μ on ℝ with a density f, the support end Z : EReal, and the complementary distribution function Fbar μ x = μ((x, ∞)). The model data, the coefficients coef, the effective costs cF, cN, cR, the two profit functions, best responses, equilibria, feasibility and adoption are definitions; all theorems are for arbitrary data satisfying Params.Valid and DemandModel. Readings fixed by the formalization:

"Feasible": some wholesale price $w \ge 0$ with a supplier best response gives the retailer strictly positive profit. It is not defined as $c_i < p$ , which is what Propositions 2 and 3 prove.
"Adopted" / "should be adopted": the scheme is feasible and its equilibrium supplier profit is best among the feasible available schemes, with ties resolved $\mathcal R \succ \mathcal N \succ \mathcal F$ , the order forced by the paper's boundaries ( $C_s = \mathbb C_1$ , $C_s = \mathbb C_3$ , $C_r = \mathbb C_2$ ). Profits are compared, not the $\Lambda_i$ .
"The unique value of $C_s$ that satisfies …": a point of $(C_{\min}, C_{\max})$ satisfying the equation and the only such point. The equation $c_{\mathcal F} = p$ is cross-multiplied, $c\,e^{(\eta_s+\lambda_s)t_1} = p\Lambda_{\mathcal F}$ , since $\Lambda_{\mathcal F}$ may be $\le 0$ .
" $C_r > \mathbb C_2$ " is read through the paper's equivalence $\tau > -\eta_r^{-1}\ln(1-\rho_r)$ , i.e. $e^{-\eta_r\tau} < 1-\rho_r$ : the stated assumptions give no single crossing in $C_r$ .
"The unique equilibrium can be derived from …": the equilibrium exists and is unique, and it is exactly the solution of the system with $q \in (0, \mathbb Z)$ ; this part is stated under feasibility.
"Increasing/decreasing" is weak unless stated (p. 6075); $\rho$ is strictly decreasing, $\eta$ weakly.
Continuity of $f$ is read on $[0,\mathbb Z]$ , and $\mathbb Z$ as the upper end of the support.
Additions: wholesale prices are nonnegative; the retailer's reverse-factoring profit is the last line of the p. 6082 display (the middle line has a stray factor $w$ ).
Corollary 1(i): "higher credit rating" is read as $C_r \ge C_s$ , "dominates" as a strictly larger equilibrium supplier profit whenever recourse is feasible.

A formalization in which feasibility or adoption is defined by the inequalities being proved ( $c_i < p$ , largest $\Lambda_i$ ) makes the propositions trivial and is ruled out by the definitions above. The profit functions (7), (10) and the p. 6082 display are taken as the model; the derivation from bank and factor pricing (Eqs. (1), (5), (6), Lemma 1) is not formalized, and the unstated assumptions of Table EC.2 are not included. Contributions of reusable lemmas on $S$ , $k$ and $z$ under strict IFR are welcome.

Selected references

P. Kouvelis and F. Xu, A Supply Chain Theory of Factoring and Reverse Factoring, Management Science 67(10):6071–6088, 2021. https://doi.org/10.1287/mnsc.2020.3788
G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0189
D. A. Wuttke, E. Rosenzweig, H. S. Heese, An Empirical Analysis of Supply Chain Finance Adoption, Journal of Operations Management 65(3):242–261, 2019.
P. Kouvelis and W. Zhao, Who Should Finance the Supply Chain? Impact of Credit Ratings on Supply Chain Decisions, Manufacturing & Service Operations Management 20(1):19–35, 2018.

8 thms2 active usersReviewed

Completed

Control Theory Convex Optimization Operations Research+1·Captain: mikedeng1

Robust Solutions to Uncertain Semidefinite Programs II: An SDP Inner Approximation of the Robust Feasible Set under Structured PerturbationsResearch Paper

Motivation

A semidefinite program (SDP) minimizes a linear objective $c^Tx$ subject to a linear matrix inequality $F(x) = F_0 + \sum_{i=1}^m x_i F_i \succeq 0$ . In engineering applications the coefficient matrices are rarely known exactly: they come from measurements, from a model of a physical plant, or from a finite-precision implementation. El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) asked for solutions that remain feasible for every admissible value of the uncertain data, and showed how to compute such robust solutions by semidefinite programming. The paper appeared alongside Ben-Tal and Nemirovski's robust convex programming (Math. Oper. Res. 23(4), 1998) and is one of the two founding treatments of robust SDP.

When the uncertainty has structure (a block-diagonal perturbation, repeated scalar parameters, a symmetric matrix), the exact robust problem is NP-hard (El Ghaoui and Lebret, SIAM J. Matrix Anal. Appl. 18, 1997). This is the same obstacle that robust control meets in computing the structured singular value, and the remedy the paper uses, scaling matrices that commute with the perturbation structure, goes back to that literature (Doyle, IEE Proc. D 129, 1982; Fan, Tits and Doyle, IEEE Trans. Automat. Control 36, 1991). This mission formalizes the resulting tractable conservative approximation, Theorem 3.2 of the paper, together with the lemma it rests on and an application to integer feasibility problems.

Setting

Fix natural numbers $m, n, p, q$ . The decision variable is $x \in \mathbb{R}^m$ . The nominal data are affine maps

F(x) = F_0 + \sum_{i=1}^m x_i F_i \in \mathbb{R}^{n\times n}, \qquad R(x) = R_0 + \sum_{i=1}^m x_i R_i \in \mathbb{R}^{q\times n},

with every $F_i$ symmetric, and fixed matrices $L \in \mathbb{R}^{n\times p}$ , $D \in \mathbb{R}^{q\times p}$ . A perturbation is a matrix $\Delta \in \mathbb{R}^{p\times q}$ , and the perturbed constraint matrix is the linear-fractional representation (LFR)

\mathbf{F}(x,\Delta) = F(x) + L\Delta(I - D\Delta)^{-1}R(x) + R(x)^T(I - \Delta^TD^T)^{-1}\Delta^TL^T,

which is defined when $\det(I - D\Delta) \neq 0$ . The perturbation ranges over a linear subspace $\mathcal{D} \subseteq \mathbb{R}^{p\times q}$ , which encodes the structure, and is bounded by a level $\rho > 0$ in the spectral norm $\|\Delta\|$ (the largest singular value). The robust feasible set is

\mathcal{X}_\rho = \{x : \text{for every } \Delta \in \mathcal{D} \text{ with } \|\Delta\| \le \rho,\ \det(I - D\Delta) \neq 0 \text{ and } \mathbf{F}(x,\Delta) \succeq 0\},

and the robust SDP (RSDP) is to minimize $c^Tx$ over $\mathcal{X}_\rho$ .

The scaling set of $\mathcal{D}$ is the linear subspace

\mathcal{B} = \{(S,T,G) \in \mathbb{R}^{p\times p}\times\mathbb{R}^{q\times q}\times\mathbb{R}^{p\times q} : S\Delta = \Delta T,\ G\Delta^T = -\Delta G^T \text{ for every } \Delta \in \mathcal{D}\}.

Formalization targets

Goal: Theorem 3.2 (p. 37), as an inclusion of feasible sets

For every $x$ : if some $(S,T,G) \in \mathcal{B}$ has $S \succ 0$ , $T \succ 0$ and

\begin{bmatrix} F(x) - LSL^T & R(x)^T - LSD^T + LG \\ R(x) - DSL^T + G^TL^T & \rho^{-2}T - DSD^T + DG + G^TD^T\end{bmatrix} \succ 0,

then $x \in \mathcal{X}_\rho$ , and in fact $\mathbf{F}(x,\Delta) \succ 0$ for every $\Delta \in \mathcal{D}$ with $\|\Delta\| \le \rho$ . A companion item states the consequence for optimal values: the SDP value is an upper bound on the RSDP value, with both infima taken in the extended reals.

Milestones

Lemma 3.2 (p. 37): the same implication for constant $F$ , $R$ and $\rho = 1$ , with the matrix (13).
The full-perturbation case (p. 37): for $\mathcal{D} = \mathbb{R}^{p\times q}$ and $p, q \ge 1$ , $\mathcal{B}$ consists exactly of the triples $(\tau I_p, \tau I_q, 0)$ , with $\tau \ge 0$ when $S \succeq 0$ .
Theorem 5.6 (p. 48): if $F_i = 2L_iR_i$ with $r_i = \operatorname{rank} F_i$ , and $x_{\mathrm{feas}}$ satisfies, for some $\lambda \ge 0$ and block-diagonal $S = S^T$ , $G = -G^T$ ,

\begin{bmatrix} F(x_{\mathrm{feas}}) - \lambda I - LSL^T & \tfrac12R^T + LG \\ \tfrac12R - GL^T & S\end{bmatrix} \succ 0,

then every integer vector closest to $x_{\mathrm{feas}}$ in the maximum norm satisfies $F(z) \succeq 0$ .

Significance

The result. Theorem 3.2 replaces an NP-hard semi-infinite constraint, one matrix inequality for each admissible perturbation, by a single linear matrix inequality in the enlarged variable $(x, S, T, G)$ . Every point it certifies is robustly feasible, so its optimal value is a certified upper bound on the robust optimum and its optimizer is a usable robust solution. In the full case the scalings collapse to one multiplier $\tau$ (milestone 2), which connects the bound to the exact reformulation of Section 3.1 of the paper. Theorem 5.6 shows the same machinery at work on a combinatorial problem: robustness against perturbations of size $1/2$ in each coordinate of $x$ turns an SDP-feasible point into an integer solution by rounding.

Formalizing it. The results are proved in the paper (Lemma 3.2 with the proof deferred to [16]); none of them has a machine-checked proof that this mission is aware of, and the platform has no linear-fractional or structured-perturbation results. The formalization also settles the exact form of the certificate: as printed, the matrix (13) and the LMI of Theorem 3.2 contain products that are dimensionally undefined, and this mission states the condition the proof actually yields (see the scope section).

Difficulty

The inequality to be proved is a statement about infinitely many perturbations, and $\mathbf{F}(x,\Delta)$ depends on $\Delta$ through a matrix inverse. The natural first step, eliminating $\Delta$ by an exact S-procedure as in the full case, is not available: with a structured $\mathcal{D}$ the set of pairs of vectors linked by some $\Delta \in \mathcal{D}$ is not described by one quadratic inequality, and losslessness fails. The scalings in $\mathcal{B}$ give several valid quadratic inequalities instead, and one must show that their combination controls every $\Delta$ in the norm ball, including the well-posedness claim $\det(I - D\Delta) \neq 0$ , which is part of the conclusion rather than an assumption. The commutation condition $S\Delta = \Delta T$ must be turned into an inequality for $\|\Delta\| \le 1$ , which requires more than the definition of the spectral norm. For Theorem 5.6 the block-diagonal perturbation family and the rescaling between $\rho = 1/2$ and the stated matrix must be matched to the general lemma.

Formalization scope

Matrices are Matrix (Fin a) (Fin b) ℝ; $\succ 0$ and $\succeq 0$ are Matrix.PosDef and Matrix.PosSemidef (both include symmetry); block matrices are Matrix.fromBlocks on Fin n ⊕ Fin q. The norm of a perturbation is the $\ell^2$ operator norm (open scoped Matrix.Norms.L2Operator), i.e. the largest singular value; the maximum norm in Theorem 5.6 is Mathlib's sup norm on Fin m → ℝ. $\mathcal{D}$ is a Submodule. Affine maps are given by coefficient families indexed by Fin (m+1). Mathlib's matrix inverse is $0$ at a singular matrix, so every statement pairs the LFR with $\det(I - D\Delta) \neq 0$ . The standing assumption $\rho > 0$ of Section 3 is a hypothesis.

Readings and corrections of the printed statements:

(13) as printed is dimensionally inconsistent; we state the condition the proof yields, which coincides with the printed one when $G$ is square and skew-symmetric and $\mathcal{D}$ consists of symmetric matrices. Concretely, (11) prints $G \in \mathbb{R}^{q\times p}$ with $G\Delta = -\Delta^TG^T$ and (13) prints the blocks $R - DSL - GL^T$ and $T - GD^T + DG - DSD^T$ ; the mission uses $G \in \mathbb{R}^{p\times q}$ with $G\Delta^T = -\Delta G^T$ and the blocks $R - DSL^T + G^TL^T$ and $T - DSD^T + DG + G^TD^T$ . The same correction applies to the LMI of Theorem 3.2 (with $\rho^{-2}T$ ). Theorem 5.6 is stated as printed.
"An upper bound on the RSDP (4) and a corresponding solution $x$ can be computed by solving the SDP" is read as the inclusion of the SDP's feasible projection in $\mathcal{X}_\rho$ , for every $x$ ; the goal states it with the strict conclusion $\mathbf{F}(x,\Delta) \succ 0$ as well. The value form is a separate item.
In the full-perturbation remark, "for some $\tau \ge 0$ " is stated under $S \succeq 0$ , and "We then recover the exact results of section 3.1" is not formalized.
In Theorem 5.6, $\mathcal{S}$ 's index range " $i = 1,\dots,n$ " is read as $i = 1,\dots,m$ ; the hypothesis $r_i = \operatorname{rank}F_i$ is kept.

Trivializing formalizations are ruled out: $(0,0,0) \in \mathcal{B}$ always, so the hypotheses $S \succ 0$ and $T \succ 0$ are kept outside $\mathcal{B}$ ; $\mathcal{D}$ is a subspace, not an arbitrary set; and the norm is the spectral norm, not Mathlib's default entrywise norm.

A complete development needs the square root of a positive definite matrix and its commutation with $S$ and $T$ , the spectral-norm characterization $\Delta\Delta^T \preceq \|\Delta\|^2 I$ , Schur-complement and congruence facts for block matrices, and a linear-fractional identity relating $(I - D\Delta)^{-1}$ to an auxiliary vector. These are reusable well beyond this mission; contributions of any of them, and of the value and rounding corollaries, are welcome.

Selected references

L. El Ghaoui, F. Oustry, H. Lebret, Robust Solutions to Uncertain Semidefinite Programs, SIAM J. Optim. 9(1):33–52, 1998. https://doi.org/10.1137/S1052623496305717
L. El Ghaoui, H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM J. Matrix Anal. Appl. 18:1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
M. K. H. Fan, A. L. Tits, J. C. Doyle, Robustness in the presence of mixed parametric uncertainty and unmodeled dynamics, IEEE Trans. Automat. Control 36:25–38, 1991. https://doi.org/10.1109/9.62265
J. C. Doyle, Analysis of feedback systems with structured uncertainties, IEE Proc. D 129(6):242–250, 1982. https://doi.org/10.1049/ip-d.1982.0053
A. Ben-Tal, A. Nemirovski, Robust convex optimization, Math. Oper. Res. 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777

5 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Integrating Replenishment Decisions with Advance Demand Information II: With Zero Set-up Cost the Myopic Base-Stock Policy Is Optimal When Myopic Levels Are NondecreasingResearch Paper

Motivation

Many firms learn about demand before it has to be served: customers place orders days or weeks ahead of the date they want delivery. Gallego and Özer (Management Science 47(10), 2001) model this advance demand information in a periodic-review inventory system and ask how the optimal replenishment policy should use it. Classical inventory theory (Arrow, Harris and Marschak 1951; Scarf 1959; Veinott 1965, 1966; Iglehart 1963) assumes that nothing about future demand is known when an order is placed. With advance orders the state of the system is no longer a single number, and it is not a priori clear whether the familiar policy structures survive.

This mission covers the paper's zero set-up cost case (Section 5). The companion mission Integrating Replenishment Decisions with Advance Demand Information I covers the positive set-up cost case and its $(s, S)$ policies.

Setting

Time is divided into periods $t = 1, \dots, T$ . The supply lead time is an integer $L \ge 0$ , and the information horizon is $N$ . In period $t$ customers place orders $D_t = (D_{t,t}, \dots, D_{t,t+N})$ , where $D_{t,s} \ge 0$ is demand placed in period $t$ for delivery in period $s$ . Throughout, $N > L + 1$ ; write $M = N - L - 1 \ge 1$ .

At the start of period $t$ the decision maker knows two things. The first is the modified inventory position $x_t$ : on-hand stock plus outstanding orders minus backorders, net of the demand already observed for the protection period $t, \dots, t+L$ . The second is the vector

o_t = (o_{t,t+L+1}, \dots, o_{t,t+N-1}) \in \mathbb{R}^M

of demands already observed for periods beyond the protection period. The decision maker raises the position to $y \ge x_t$ at zero fixed cost, the demand vector $D_t$ is realised, and the state moves to

x_{t+1} = y - \sum_{k=0}^{L+1} D_{t,t+k} - o_{t,t+L+1}, \qquad o_{t+1,s} = o_{t,s} + D_{t,s}\ (s = t+L+2, \dots, t+N),

with $o_{t,t+N} = 0$ .

Costs enter through a single-period cost $G_t : \mathbb{R} \to \mathbb{R}$ (holding, backorder and linear ordering cost, charged against the demand over the protection period) and one-period discount factors $\alpha_{t+1} > 0$ . The optimal cost-to-go $J_t$ and the cost $V_t$ of ordering up to $y$ satisfy

J_t(x, o) = \min_{y \ge x} V_t(y, o), \qquad V_t(y, o) = G_t(y) + \alpha_{t+1}\,\mathbb{E}\,J_{t+1}(x_{t+1}, o_{t+1}), \qquad J_{T+1} \equiv 0,

where the expectation is over $D_t$ . The base-stock level in period $t$ is the smallest minimizer

y_t(o) = \min\{y : V_t(y, o) = \min_x V_t(x, o)\},

and the myopic level is the smallest minimizer of the single-period cost,

y^m_t = \min\{y : G_t(y) = \min_x G_t(x)\}.

A function $f(x, \theta)$ has decreasing differences if $f(x_1, \theta) - f(x_2, \theta) \le f(x_1, \theta') - f(x_2, \theta')$ whenever $x_1 \ge x_2$ and $\theta \ge \theta'$ componentwise.

Formalization targets

Goal: Theorem 5 (p. 1352)

If $t \mapsto y^m_t$ is nondecreasing on $\{1, \dots, T\}$ , then for every period $t$ and every observed-demand vector $o \ge 0$ ,

y_t(o) = y^m_t .

The optimal order-up-to level then ignores all advance information beyond the protection period. A second item states the paper's stationary special case: if $G_t = G$ for all $t$ , the smallest minimizer $y^m$ of $G$ is the optimal base-stock level in every period.

Milestones: Theorem 4 (p. 1351)

For every period $t$ and every fixed $o_t$ :

$V_t(\cdot, o_t)$ is convex and $V_t(x, o_t) \to \infty$ as $|x| \to \infty$ ;
$y_t(o_t)$ exists and $J_t(x, o_t) = V_t(\max(y_t(o_t), x), o_t)$ : a state-dependent base-stock policy is optimal;
$J_t(\cdot, o_t)$ is nondecreasing and convex;
$V_t(x, o)$ has decreasing differences in $(x, o)$ ;
$J_t(x, o)$ has decreasing differences in $(x, o)$ ;
$y_t(o)$ is nondecreasing in $o$ .

Parts 1–3 are what the goal's proof uses. Parts 4–6 are the paper's second zero set-up result, monotonicity of the base-stock level in observed demand.

Significance

The theorem identifies when advance demand information beyond the protection period can be ignored. When the myopic levels do not decrease over time, which includes stationary costs and ramping-up demand, the $(1 + M)$ -dimensional dynamic program collapses to a sequence of one-dimensional newsvendor-type problems. That is both a computational simplification and a managerial statement: information about demand after the protection period does not change the order. Theorem 4, Part 5 gives the complementary monotone comparative statics. When the myopic condition fails, more observed demand never lowers the order-up-to level.

The results are proved in the paper, with the proofs in Appendix B. No machine-checked version exists. This mission produces a formal account of the finite-horizon recursion with a multi-dimensional information state, and checks the base-stock and myopic-optimality arguments against it.

Difficulty

The obvious induction carries convexity of $J_{t+1}$ backward, but here the future cost is evaluated at a random next state $(x_{t+1}, o_{t+1})$ whose first coordinate depends on the current observed demand $o_{t,t+L+1}$ . Showing that the base-stock level does not depend on $o_t$ therefore needs more than convexity. It needs to know where $J_{t+1}(\cdot, o_{t+1})$ is flat, uniformly in the random $o_{t+1}$ , and that the next position cannot exceed the current order-up-to level. The latter holds only on the reachable states, where observed demands are nonnegative. For a sufficiently negative $o_{t,t+L+1}$ the next period starts above its myopic level whatever is ordered now, and the conclusion fails. On the analytic side, every infimum and expectation in the recursion must be shown to be finite and attained before the order-theoretic argument can start.

Formalization scope

The model is parametrised by $L$ and $M \ge 1$ , with $N = L + M + 1$ . The demand vector is a function on $\{0, \dots, N\}$ and $o$ a function on $\{0, \dots, M-1\}$ , ordered componentwise. $J_t$ is defined by backward recursion with $J_t \equiv 0$ for $t > T$ . The minimum over $y \ge x$ is a real infimum and the expectation a Bochner integral against the law $\mu_t$ of $D_t$ . Attainment and finiteness are consequences proved in the theorems, not assumptions. Base-stock and myopic levels are characterised as smallest minimizers (IsLeast), never through sInf.

The single-period cost $G_t$ is a primitive rather than being assembled from $c_t$ , $g_t$ and the lead-time demand; the paper's $G_t$ has the assumed properties, so the theorems cover the paper's model. Hypotheses the paper uses without stating, all placed on primitives and labelled in the statements:

nonnegative demands, $D_{t,s} \ge 0$ almost surely;
coercivity of $G_t$ (the paper states it for $\tilde G_t$ only);
$\alpha_{t+1} > 0$ ;
finiteness of the expectation in (9), guaranteed by linear growth of $G_t$ and finite first moments of $D_t$ . This covers piecewise-linear holding and backorder costs with any finite-mean demand (including the paper's Poisson example), but excludes superlinear costs;
in the goal, $o \ge 0$ , the set of reachable states.

The goal cannot be trivialised: the hypotheses are satisfied by concrete instances (for example $G_t(y) = |y|$ with any finite-mean nonnegative demand), and the conclusion identifies the base-stock level exactly rather than asserting that some minimizer exists.

Out of scope: the reduction of the control problem to the functional equation (Appendix A, Özer 2000), the infinite-horizon Theorem 6, and Lemma 5, whose proof argues on the integers and whose real-valued form with a unit forward difference is unverified. Contributions of general lemmas are welcome: convexity and attainment for $\inf_{y \ge x}$ of a convex coercive function, and preservation of convexity and decreasing differences under expectation. All of them are reusable in other inventory models.

Selected references

G. Gallego, Ö. Özer, Integrating Replenishment Decisions with Advance Demand Information, Management Science 47(10):1344–1360, 2001. https://doi.org/10.1287/mnsc.47.10.1344.10261
A. F. Veinott, Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

9 thms2 active usersReviewed

Completed

Convex Optimization Linear Optimization Operations Research+1·Captain: mikedeng1

Validation of Subgradient Optimization I: The Core Problem Built from the Subgradient Iterates Solves the Dual Linear ProgramResearch Paper

Motivation

Subgradient optimization maximizes a concave function that is not differentiable by stepping along an arbitrary subgradient with a prescribed sequence of step sizes. It became a standard tool of integer programming after Held and Karp used it to compute the Lagrangian 1-tree bound for the traveling-salesman problem (Held & Karp 1971). Held, Wolfe and Crowder then tested it on the assignment problem, a traveling-salesman relaxation and a multicommodity flow problem (Held, Wolfe & Crowder 1974).

The method has one practical defect that the paper names at the start of its Section 6: it contains no test of optimality. The value $w(\pi^j)$ approaches the maximum, but at no finite step does the method say that the maximum has been reached, or what the maximum is. Section 6 of the paper supplies such a test for the case where $w$ is a minimum of finitely many affine functions. The finitely many subgradients produced by the iterates define a small linear program, the core problem, and from some iteration on this linear program already solves the full dual linear program. Its optimal value is therefore the exact maximum of $w$ , obtained from quantities the method computes anyway. This is how the authors certified the optimal values reported in their experiments.

Timeline:

1967–1969: Poljak proves that the subgradient iterates satisfy $w(\pi^j)\to\max w$ when the step sizes tend to zero and have divergent sum (Poljak 1967; Poljak 1969).
1971: Held and Karp apply the method to the 1-tree bound (Held & Karp 1971).
1974: Held, Wolfe and Crowder prove that the core problem $P(J,J^*)$ solves the dual linear program (Theorem 6.3) and give a sufficient condition for bounded iterates (Theorem 6.1).
1996–1999: primal recovery from subgradient iterates is developed further, by convex combinations of the subgradients with weights derived from the step sizes (Sherali & Choi 1996; Larsson, Patriksson & Strömberg 1999).

Setting

Fix $n\ge0$ and write $E^n=\mathbb R^n$ with the Euclidean inner product $\pi\cdot v$ . The data are $K\ge1$ scalars $c_k$ and vectors $v_k\in E^n$ , and

w(\pi)=\min\{c_k+\pi\cdot v_k : k=1,\dots,K\}.\qquad(2.2)

The function $w$ is assumed bounded above, the paper's standing assumption. An index $k$ attains the minimum at $\pi$ if $c_k+\pi\cdot v_k=w(\pi)$ .

A run of the subgradient algorithm consists of a starting point $\pi^0\in E^n$ , step sizes $t_j>0$ and indices $k(j)$ such that $k(j)$ attains the minimum at $\pi^j$ , and

\pi^{j+1}=\pi^j+t_j\,v_{k(j)}\qquad(j=0,1,\dots).\qquad(2.6)

No rule for choosing among several minimizing indices is imposed. Write $v^j=v_{k(j)}$ and $c^j=c_{k(j)}$ . The step-size conditions are

t_j\to0,\qquad \sum_{j=0}^\infty t_j=\infty.\qquad(2.7)

The dual linear program of $\max w$ is

\min\Big\{\sum_k c_ky_k : y_k\ge0,\ \sum_ky_k=1,\ \sum_ky_kv_k=0\Big\}.\qquad(6.1)

For integers $J<J^*$ the core problem $P(J,J^*)$ has one variable $y_j$ for each iteration $j\in[J,J^*]$ :

\min\Big\{\sum_{j=J}^{J^*}c^jy_j : y_j\ge0,\ \sum_{j=J}^{J^*}y_j=1,\ \sum_{j=J}^{J^*}y_jv^j=0\Big\}.

An index chosen at several iterations contributes several identical columns. A point $y$ of $P(J,J^*)$ is sent to the point $\bar y_k=\sum\{y_j : J\le j\le J^*,\ k(j)=k\}$ of (6.1). This aggregation preserves feasibility and objective value.

Formalization targets

Goal: Theorem 6.3 (p. 82)

Assume $w$ is bounded above, $(t_j,\pi^j,k(j))$ is a run satisfying (2.7), and $\{\pi^j\}$ is bounded. Then

\forall J\ \exists J^*>J:\quad P(J,J^*)\text{ has a solution, and every solution of }P(J,J^*)\text{ aggregates to a solution of (6.1)}.

The goal states existence of $J^*$ , which is what the paper claims. The paper's argument in fact gives the conclusion for every sufficiently large $J^*$ . That stronger form is not the goal. Feasibility of $P(J,J^*)$ (Lemma 6.2) or the inequality $\mathrm{Value}[P(J,J^*)]\ge\mathrm{Value}[(6.1)]$ , which holds for every feasible $P(J,J^*)$ , is not a formalization of the goal. The content is optimality in (6.1).

Milestones

Eq. (2.10): if $\pi^*$ maximizes $w$ and $k$ attains the minimum at $\pi$ , then $w^*-w(\pi)\le v_k\cdot(\pi^*-\pi)$ .
§6, p. 80 (display): under (2.6), (2.7) and $w$ bounded above, $\lim_j w(\pi^j)=\max w=w(\pi^*)$ for some $\pi^*$ . The iterates are not assumed bounded.
Theorem 6.1: if every $\pi\ne0$ has some $\pi\cdot v_k<0$ , every run satisfying (2.7) is bounded.
Eq. (6.1): (6.1) has a solution, and its optimal value equals $\max w$ .
Lemma 6.2: for any $J$ there is $J^*>J$ with $P(J,J^*)$ feasible, for bounded runs.

Significance

Theorem 6.3 turns an asymptotic method into one that returns an exact answer. Solving $P(J,J^*)$ for growing $J^*$ produces a linear program of bounded size whose optimum is eventually the optimum of (6.1), and hence $\max w$ . In the Lagrangian applications, where (6.1) is the linear relaxation of a combinatorial problem, this yields both the bound and a primal solution of the relaxation. The theorem is the ancestor of the primal-recovery results listed in the timeline.

The mission produces a machine-checked version of the paper's Section 6, together with the input the paper takes on citation: Poljak's convergence theorem for divergent-series step sizes, specialized to piecewise-linear concave functions. Neither Poljak's theorem nor Theorem 6.3 is in Mathlib. The pieces are reusable: the convergence theorem applies to every Lagrangian dual solved by subgradient steps, and the duality between $\max w$ and (6.1) is linear-programming duality for a minimum of affine functions.

Difficulty

The inequality $\operatorname{Value}P(J,J^*)\ge\operatorname{Value}(6.1)$ is immediate, since aggregation maps feasible points to feasible points with the same objective. All of the content lies in the reverse inequality. That inequality ties a finite linear program to the limit of an infinite sequence, and it must hold for an arbitrary choice among tied minimizing indices. The iterates themselves need not converge, and under (2.7) the values $w(\pi^j)$ are not monotone. So an argument that inspects a single iterate, or assumes that the method settles on one face of $w$ , fails. The convergence statement of milestone 2 is not proved in the paper and is the heaviest single step. Feasibility of $P(J,J^*)$ also needs its own argument, and it fails without the boundedness hypothesis.

Formalization scope

$E^n$ is EuclideanSpace ℝ (Fin n), the index set is a finite nonempty type ι, and $w$ is the finite minimum Finset.univ.inf'. A run is the predicate IsSubgradientRun c v t π k: positive steps, a minimizing index at every step, and update (2.6). It is not a function of $\pi^0$ , so every tie-breaking rule is covered. (2.7) is StepSizeCond t: t → 0, and the partial sums tend to $+\infty$ . Iterates are indexed from $j=0$ . Boundedness is Bornology.IsBounded (Set.range π). The variables of $P(J,J^*)$ are a function on $\mathbb N$ of which only the values at $J\le j\le J^*$ enter. Optimality of $y$ in either linear program means feasibility plus an objective no larger than that of every feasible point. Suprema are never taken over unbounded sets: every maximum of $w$ is stated as attained at an explicit $\pi^*$ .

A statement that only asserts feasibility of $P(J,J^*)$ , or only $\operatorname{Value}P\ge\operatorname{Value}(6.1)$ , is not the theorem. The goal requires that the solutions of $P(J,J^*)$ be optimal for (6.1).

Theorem 6.1 is printed for the step rule (2.8), but its proof uses $w(\pi^j)\to w^*$ , the consequence of (2.7). The mission states it for (2.7), and its milestone title says so.

A complete development needs:

linear-programming duality for (6.1), including attainment;
the convergence theorem for divergent-series step sizes;
existence of a maximizer of a bounded-above minimum of finitely many affine functions;
basic facts on convex hulls of finitely many vectors in $E^n$ .

The first three are reusable well beyond this mission. Contributions of any of them, as standalone theorems, are welcome.

Selected references

M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974) 62–88. https://doi.org/10.1007/BF01580223
M. Held, R. M. Karp, The traveling-salesman problem and minimum spanning trees: Part II, Mathematical Programming 1 (1971) 6–25. https://doi.org/10.1007/BF01584070
B. T. Poljak, A general method of solving extremum problems, Soviet Mathematics Doklady 8 (1967) 593–597.
B. T. Poljak, Minimization of unsmooth functionals, USSR Computational Mathematics and Mathematical Physics 9 (1969) 14–29. https://doi.org/10.1016/0041-5553(69)90061-5
H. D. Sherali, G. Choi, Recovery of primal solutions when using subgradient optimization methods to solve Lagrangian duals of linear programs, Operations Research Letters 19 (1996) 105–113. https://doi.org/10.1016/0167-6377(96)00019-3
T. Larsson, M. Patriksson, A.-B. Strömberg, Ergodic, primal convergence in dual subgradient schemes for convex programming, Mathematical Programming 86 (1999) 283–312. https://doi.org/10.1007/s101070050090

7 thms2 active usersReviewed

Completed

Convex Optimization Linear algebra Numerical Analysis+2·Captain: mikedeng1

Robust Solutions to Least-Squares Problems with Uncertain Data II: Robust Least Squares as Tikhonov RegularizationResearch Paper

Motivation

Least squares fits a linear model $Ax \simeq b$ by minimizing $\|Ax - b\|$ , and its solution can be extremely sensitive to errors in the data $(A, b)$ when $A$ is ill-conditioned. The standard remedy is Tikhonov regularization (ridge regression): minimize $\|Ax - b\|^2 + \mu\|x\|^2$ , whose solution $x = (A^\top A + \mu I)^{-1}A^\top b$ is stable but depends on a parameter $\mu > 0$ that must be chosen by some external rule.

El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed instead to take the uncertainty in $(A, b)$ seriously: the robust least-squares (RLS) solution minimizes the worst-case residual over all perturbations $[\Delta A\ \Delta b]$ of Frobenius norm at most $\rho$ . Their Theorem 3.1 shows that for $\rho = 1$ this worst-case residual equals $\|Ax - b\| + \sqrt{\|x\|^2 + 1}$ and that its minimization is the second-order cone program (15). Theorem 3.2, the subject of this mission, reads off the optimal solution: it is a Tikhonov-regularized solution, and the regularization parameter is not a free choice but is fixed by the data. This gives a principled answer to the question of how to choose $\mu$ , and it is the reason the paper describes RLS as "a Tikhonov regularization procedure" with "a rigorous way to compute the regularization parameter" (abstract, p. 1035).

A closely related model for least squares with bounded data uncertainty was developed at the same time by Chandrasekaran, Golub, Gu and Sayed; the paper notes that their preliminary draft (its reference [5]) gives a solution to the unstructured RLS problem similar to that of §3.2 (pp. 1036–1037).

Setting

Throughout, $A \in \mathbb R^{n\times m}$ , $b \in \mathbb R^n$ , $x \in \mathbb R^m$ , and every vector norm is Euclidean, $\|v\| = \sqrt{\sum_i v_i^2}$ . For $x \in \mathbb R^m$ , $[x; 1] \in \mathbb R^{m+1}$ is $x$ with a coordinate $1$ appended, so $\|[x;1]\| = \sqrt{\|x\|^2 + 1}$ .

The SOCP (15) is the problem, in the variables $x \in \mathbb R^m$ and $\lambda, \tau \in \mathbb R$ ,

\text{minimize } \lambda \quad\text{subject to}\quad \|Ax - b\| \le \lambda - \tau,\qquad \|[x;1]\| \le \tau.

A triple $(x, \lambda, \tau)$ is optimal for (15) if it is feasible and $\lambda \le \lambda'$ for every feasible $(x', \lambda', \tau')$ . Its dual, derived in the paper from the general second-order cone duality of §2.1, is the problem in $z \in \mathbb R^n$ , $u \in \mathbb R^m$ , $v \in \mathbb R$

\text{maximize } b^\top z - v \quad\text{subject to}\quad A^\top z + u = 0,\quad \|z\| \le 1,\quad \|[u; v]\| \le 1.

The minimum-norm solution of $Ax = b$ is a solution $x$ with $\|x\| \le \|y\|$ for every other solution $y$ ; when $Ax = b$ is consistent it is $A^\dagger b$ , with $A^\dagger$ the Moore–Penrose pseudoinverse.

In the Lean development these objects are IsSOCPFeasible, IsSOCPOptimal, IsDualFeasible, dualObjective, IsDualOptimal and IsMinNormSolution, in the namespace RobustLS.Tikhonov, with the Euclidean norm eucNorm.

Formalization targets

Goal: Theorem 3.2 with the identity for $\mu$

Let $(x, \lambda, \tau)$ be optimal for (15) and set $\mu = (\lambda - \tau)/\tau$ . Then

x = \begin{cases} (\mu I + A^\top A)^{-1}A^\top b & \text{if } \mu > 0,\\ A^\dagger b & \text{else,}\end{cases}\qquad\text{and}\qquad \mu = \frac{\|Ax - b\|}{\sqrt{\|x\|^2 + 1}}.

By Theorem 3.1 (the subject of the companion mission I of this series), the $x$ -part of an optimal point of (15) is the RLS solution for $\rho = 1$ , so this is formula (17) of the paper. The identity for $\mu$ is the final display of the paper's proof and is the claim in the mission's title.

Milestones (in the order of the paper's proof, p. 1041)

Both (15) and its dual have optimal points.
If $\lambda = \tau$ at the optimum, then $Ax = b$ and $\lambda = \tau = \sqrt{\|x\|^2 + 1}$ .
In that case $x$ is the minimum-norm solution of $Ax = b$ , $x = A^\dagger b$ .
Eq. (18): for $\lambda > \tau$ , primal and dual optimal values coincide,

\|Ax - b\| + \|[x;1]\| = \lambda = b^\top z - v = -(Ax-b)^\top z - [x^\top\ 1]\begin{bmatrix} -A^\top z\\ v\end{bmatrix}.

The dual optimal point is $z = -(Ax - b)/\|Ax - b\|$ , $[u; v] = -[x; 1]/\sqrt{\|x\|^2 + 1}$ .
Substituting into $A^\top z + u = 0$ : $x = (A^\top A + \mu I)^{-1}A^\top b$ with $\mu = (\lambda - \tau)/\tau = \|Ax - b\|/\sqrt{\|x\|^2 + 1}$ .

A further item states Remark 3.1: for $\lambda > \tau$ , $x$ is the unique minimizer of the weighted residual $\big\|[A; I; 0]y - [b; 0; 1]\big\|_\Theta$ with $\Theta = \mathbf{diag}((\lambda-\tau)I, \tau I, \tau)$ and $\|r\|_\Theta = \|\Theta^{-1/2} r\|$ .

Significance

The result. Theorem 3.2 turns a robust optimization problem into a familiar linear-algebra object. It says that the robust solution always lies on the Tikhonov path $\{(A^\top A + \mu I)^{-1}A^\top b : \mu > 0\}$ or at its endpoint $A^\dagger b$ , and it identifies the point on the path through a fixed-point equation relating $\mu$ to the residual and the size of the solution. The paper builds on this in §3.3 (a one-dimensional search for $\mu$ via the SVD) and in §6 (continuity of the RLS solution in the data), and Remark 3.1 is the template for the weighted least-squares interpretation of the structured and linear-fractional problems in §5.

Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal account of second-order cone duality for a concrete program, the characterization of the optimal dual point by equality in the Cauchy–Schwarz inequality, and the minimum-norm characterization of $A^\dagger b$ , all in terms of explicit Euclidean norms on Fin k → ℝ.

Difficulty

The paper's proof rests on strong duality for (15) ("both primal and dual problems are strictly feasible"), which it cites from the SOCP literature rather than proving; Mathlib has no second-order cone duality, so this step is the main gap. The degenerate case $\lambda = \tau$ also needs care: there $\|Ax - b\| = 0$ , the residual term is not differentiable at the optimum, and the conclusion changes from a regularized inverse to a pseudoinverse. A statement that only handles the case $Ax \ne b$ , or that assumes the matrix $A^\top A + \mu I$ invertible without deriving it from $\mu > 0$ , misses part of the theorem.

Formalization scope

Normalization. The paper states Theorem 3.2 for $\rho = 1$ ("we take $\rho = 1$ in what follows", p. 1039) and obtains general $\rho$ by the scaling $\varphi(A, b, \rho) = \rho\,\varphi(A/\rho, b/\rho, 1)$ . Only the $\rho = 1$ statement is formalized.
The RLS solution. The perturbation model is not used here: all statements are about optimal points of (15). That the $x$ -part of such a point is the RLS solution is Theorem 3.1 (mission I), and it is recalled in prose only.
Norms. Vectors are Fin k → ℝ; the Euclidean norm is the explicit eucNorm v = √(∑ vᵢ²) (Mathlib's ‖·‖ on Fin k → ℝ is the sup norm). Stacked vectors $[x;1]$ and $[u;v]$ are indexed by Fin m ⊕ Unit.
Optimality. "Optimal point" means feasible with objective no worse than every feasible point; the minimum and maximum are therefore attained by definition, and milestone 1 guarantees they exist.
Pseudoinverse. Mathlib has no matrix pseudoinverse, so $A^\dagger b$ is stated as the minimum-norm solution of $Ax = b$ , which is how the proof uses it. The branch "else" is $\neg(\mu > 0)$ .
Inverse. $(\mu I + A^\top A)^{-1}$ is Mathlib's Matrix.inv; it is used only where $\mu > 0$ , where the matrix is positive definite. $\tau \ge 1$ at every feasible point, so $\mu$ is well defined without an extra hypothesis.
No trivialization. The goal quantifies over optimal points of (15) over the whole feasible set, not over feasible points, and milestone 1 shows the hypothesis is satisfiable for every $(A, b)$ , including $n = 0$ or $m = 0$ .
Weighted norm. For Remark 3.1, $\|r\|_\Theta$ for the diagonal $\Theta$ is written as $\sqrt{\sum_i r_i^2/\theta_i}$ , which equals $\|\Theta^{-1/2}r\|$ for positive weights.

Contributions welcome: second-order cone (or general conic) weak and strong duality for finite-dimensional programs, the equality case of Cauchy–Schwarz in the explicit-norm form used here, and a Moore–Penrose pseudoinverse for real matrices with its minimum-norm property. The platform's ConvexOptimization.conic_slater_strong_duality may help with the duality step.

Selected references

L. El Ghaoui and H. Lebret, Robust Solutions to Least-Squares Problems with Uncertain Data, SIAM J. Matrix Anal. Appl. 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
S. Chandrasekaran, G. H. Golub, M. Gu and A. H. Sayed, A new linear least-squares type model for parameter estimation in the presence of data uncertainties, cited as submitted to SIAM J. Matrix Anal. Appl. (reference [5] of the paper).
A. N. Tikhonov and V. Y. Arsenin, Solutions of Ill-Posed Problems, Wiley, New York, 1977 (reference [43] of the paper).
Y. Nesterov and A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
M. S. Lobo, L. Vandenberghe, S. Boyd and H. Lebret, Applications of Second-Order Cone Programming, Linear Algebra Appl. 284:193–228, 1998. https://doi.org/10.1016/S0024-3795(98)10032-0

9 thms2 active usersReviewed

Combinatorics Graph Theory Operations Research+2·Captain: mikedeng1

Linear-Time Approximation for Maximum Weight Matching: The Approximation Guarantee of the Scaling AlgorithmResearch Paper

Motivation

The maximum weight matching (MWM) problem asks, for a graph with edge weights, for a set of vertex-disjoint edges of largest total weight. It is a central problem of combinatorial optimization, with applications to transportation, assignment and scheduling, and as a subroutine for shortest paths, planar max cut, Chinese postman tours and metric TSP. Edmonds' blossom algorithm (1965) solves it on general graphs; the fastest implementation, due to Gabow, runs in $O(mn+n^2\log n)$ time, and the scaling algorithm of Gabow and Tarjan (1991) runs in $O(m\sqrt{n\log n}\,\log(nN))$ time on graphs with $n$ vertices, $m$ edges and integer weights of magnitude at most $N$ . Applications such as switch scheduling, graph clustering and sparse linear solvers accept a slightly suboptimal matching in exchange for speed. This motivates $(1-\epsilon)$ -approximate maximum weight matchings: matchings whose weight is at least a $1-\epsilon$ fraction of the optimum.

Timeline of linear and near-linear time approximation for general graphs (Section 1.3 and Table IV of the paper; the entries below are as the paper attributes them):

Folklore: the greedy algorithm, which repeatedly takes the heaviest remaining edge, gives a $\tfrac12$ -MWM in $O(m\log n)$ time.
Preis (STACS 1999): a $\tfrac12$ -MWM in linear time; Drake and Hougardy (2003) gave a simpler one.
Drake and Hougardy (2003; journal version Vinkemeier and Hougardy, ACM Trans. Algorithms 2005): a $(\tfrac23-\epsilon)$ -MWM in $O(m\epsilon^{-1})$ time; Pettie and Sanders (2004) improved this to $O(m\log\epsilon^{-1})$ .
Duan and Pettie (FOCS 2010) and Hanke and Hougardy (2010): a $(\tfrac34-\epsilon)$ -MWM in $O(m\log n\log\epsilon^{-1})$ time.
Duan and Pettie (2014): a $(1-\epsilon)$ -MWM in $O(m\epsilon^{-1}\log\epsilon^{-1})$ time, which is linear for every fixed $\epsilon$ .

Setting

Let $G=(V,E)$ be a finite simple graph with integer weights $w:E\to\{1,\dots,N\}$ , $N=2^L$ . A matching $M$ is a set of vertex-disjoint edges, with weight $w(M)=\sum_{e\in M}w(e)$ ; a vertex is free if no edge of $M$ touches it. $M$ is a $c$ -MWM if $c\cdot w(M')\le w(M)$ for every matching $M'$ .

A blossom is built recursively: a single vertex $\{v\}$ is a trivial blossom with $E_{\{v\}}=\emptyset$ ; an odd number $\ge3$ of disjoint blossoms $A_0,\dots,A_\ell$ joined in a cycle by edges $e_i\in A_i\times A_{i+1}$ form the blossom $B=\bigcup A_i$ with edge set $E_B=\bigcup E_{A_i}\cup\{e_0,\dots,e_\ell\}$ . It is full if $|M\cap E_B|=(|B|-1)/2$ . The algorithm keeps a laminar set $\Omega$ of full blossoms; a root blossom is a maximal one, and $G/\Omega$ contracts each root blossom to a single vertex.

Dual values $y:V\to\mathbb R$ and $z$ on odd vertex sets give each edge the value

yz(u,v)=y(u)+y(v)+\sum_{B\ \text{odd},\ u,v\in B} z(B).

The scaling algorithm (Figure 2 of the paper) has parameters $N$ and $\epsilon'=2^{-g}\le\tfrac14$ . It runs scales $i=0,\dots,L$ with granularity $\delta_i=\epsilon'N/2^i$ and truncated weights $w_i(e)=\delta_i\lfloor w(e)/\delta_i\rfloor$ . Each scale repeats four steps: augment along a maximal set of vertex-disjoint augmenting paths of the eligible graph $G_{\mathrm{elig}}$ , shrink a maximal set of new blossoms, adjust the duals by $\pm\delta_i/2$ , and dissolve root blossoms whose $z$ -value has reached zero. It stops when the free vertices' $y$ -values reach a scale-dependent value, which is $0$ at scale $L$ . Eligibility is given by Definition 3.2; the linear-time variant keeps the algorithm unchanged and uses Definition 3.10, which additionally ignores an edge $e$ in scales $i>\mathrm{scale}(e)+\log\epsilon'^{-1}$ unless it is a blossom edge.

Formalization targets

Goal: Theorem 3.12, approximation half

For every $\epsilon$ with $\epsilon'\le\epsilon/7$ , the algorithm of Figure 2 with Definition 3.10 eligibility has a terminating run, and every terminating run returns a matching $M$ with

w(M)\ \ge\ (1-\epsilon)\,w(M')\qquad\text{for every matching } M' \text{ of } G .

Milestones, in attack order

Lemma 2.3: approximate complementary slackness ( $yz(e)\ge(1-\epsilon_0)w(e)$ everywhere, $yz(e)\le(1+\epsilon_1)w(e)$ on matched and blossom edges, zero free duals) gives a $(1+\epsilon_1)^{-1}(1-\epsilon_0)$ -MWM.
Section 2 rescaling: rounding real weights to $\lfloor w/\gamma_r\rfloor$ , $\gamma_r=\epsilon w_{\max}/n$ , loses at most a factor $1-\epsilon/2$ .
Lemma 3.5: with Definition 3.2 the algorithm preserves Property 3.1, which consists of granularity, active blossoms, near domination $yz(e)\ge w_i(e)-\delta_i$ , near tightness $yz(e)\le w_i(e)+2(\delta_j-\delta_i)$ for type- $j$ edges, and equal free duals.
Lemma 3.6: eligible edges searched up to scale $i$ weigh at least $N/2^{i+1}+\delta_i$ , and matched edges satisfy $yz(e)\le(1+4\epsilon')w(e)$ .
Lemma 3.7: the output under Definition 3.2 is a $(1-5\epsilon')$ -MWM.
Theorem 3.8: the approximation half of Theorem 3.8, with $\epsilon'\le\epsilon/5$ .
Lemma 3.11: the invariants under Definition 3.10, including $yz(e)>(1-\epsilon')w_i(e)$ and $yz(e)<(1+6\epsilon')w_i(e)$ once $i>\mathrm{scale}(e)+\gamma$ .

Significance

The result. Theorem 3.12 gives the first algorithm for $(1-\epsilon)$ -approximate maximum weight matching on general graphs that runs in linear time for every fixed $\epsilon$ ; earlier linear-time algorithms achieved only $\tfrac12$ or $\tfrac23-\epsilon$ . Its analysis is a relaxation of Edmonds' complementary slackness conditions that grows weaker over the scales, but not uniformly, and Lemma 2.3 certifies an approximate matching by approximately feasible duals.

Formalizing it. The result is proved in the paper. Mathlib (at the pinned revision) has matchings, alternating walks and Tutte's theorem, but no blossoms, contracted graphs or weighted matching algorithms. A complete development gives a Lean model of blossoms, contraction and augmenting paths through blossoms, a verified primal–dual invariant for a scaling algorithm, and a checked approximate-slackness certificate for matchings. Each of these can be reused to formalize Edmonds' exact algorithm or the Gabow–Tarjan scaling algorithm.

Difficulty

The two halves of the argument pull against each other. Lemma 2.3 needs near domination and near tightness as multiplicative bounds. The algorithm maintains only additive bounds whose slack for an edge of type $j$ is $2(\delta_j-\delta_i)$ , and this slack does not shrink as the scales advance. Converting it into a factor $1+O(\epsilon')$ requires a lower bound on the weight of every edge that ever became eligible, which in turn depends on the free vertices' duals following an exact schedule across scales.

For Definition 3.10 the obvious argument breaks down: an edge that is ignored after scale $\mathrm{scale}(e)+\gamma$ may violate near domination and near tightness by an amount that grows with every later dual adjustment. The claim is that the accumulated violation stays within an $O(\epsilon')$ fraction of $w_i(e)$ , and establishing this requires tracking every adjustment that can reach an ignored edge.

On the combinatorial side, the Augmentation and Blossom Shrinking steps work in the contracted graph $G/\Omega$ . Their correctness uses the classical facts that augmenting paths lift through full blossoms and that blossoms stay full after augmentation (Lemma 2.1), which have to be formalized from scratch.

Formalization scope

Graphs are SimpleGraph V on a Fintype V with decidable equality; edges are Sym2 V; matchings are Finset (Sym2 V) with pairwise vertex-disjoint edges of $G$ ; weights are $w:\mathrm{Sym2}\,V\to\mathbb N$ with $1\le w(e)\le 2^L$ on edges. Duals, $\delta_i$ and $w_i$ are real numbers. $z$ is a function on all finite vertex sets and $yz$ sums it over the odd sets that contain the edge, as on the page. $N=2^L$ and $\epsilon'=2^{-g}$ , $g\ge2$ , are given through their exponents. $\mathrm{scale}(e)$ uses the convention $\mu_{-1}=+\infty$ . The paper's standing assumption $N\le n^2$ is used only for running time and is omitted.

The algorithm is a nondeterministic relation. A state holds $M$ , $\Omega$ with its blossom edge sets, $y$ , $z$ , a ghost record of the scale in which each edge last entered $M\cup\bigcup_{B\in\Omega}E_B$ , and the common free-vertex dual that drives the loop test. The maximal sets of augmenting paths and of new blossoms and the lifts of paths through blossoms are choices. Invariants are stated for states reachable by a run, and the goal asserts both that a terminating run exists and that every terminating run returns a $(1-\epsilon)$ -MWM.

The running times $O(m\epsilon^{-1}\log N)$ of Theorem 3.8 and $O(m\epsilon^{-1}\log\epsilon^{-1})$ of Theorem 3.12 are not formalized: the paper fixes no cost model, and its bounds rely on a modified depth-first search and on word-RAM table lookups. The explicit constants $\epsilon'\le\epsilon/5$ (Theorem 3.8) and $\epsilon'\le\epsilon/7$ (Theorem 3.12) are the ones the proofs supply.

The following trivializing formalizations are ruled out: a "matching" that may contain non-edges or repeated edges; a goal about a state only assumed to satisfy Property 3.1 rather than reached by the algorithm; a run relation with no terminating run, which the existence conjunct excludes; eligibility or blossoms chosen freely instead of by the page's rules; and comparison only against matchings of the contracted graph instead of all matchings of $G$ .

Welcome contributions include a Lean treatment of blossoms and their contraction (Lemma 2.1, which is not a milestone here), the lift of augmenting paths, Lemmas 3.3 and 3.4 as auxiliary results, and proofs of the milestones in the order listed.

Selected references

R. Duan and S. Pettie, Linear-Time Approximation for Maximum Weight Matching, Journal of the ACM 61(1), Article 1, 2014. https://doi.org/10.1145/2529989
J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B, 125–130, 1965. https://doi.org/10.6028/jres.069B.013
H. N. Gabow and R. E. Tarjan, Faster scaling algorithms for general graph-matching problems, Journal of the ACM 38(4), 815–853, 1991. https://doi.org/10.1145/115234.115366
R. Preis, Linear time 1/2-approximation algorithm for maximum weighted matching in general graphs, STACS 1999, LNCS 1563, 259–269 (cited from the bibliography of Duan and Pettie 2014).
D. E. D. Vinkemeier and S. Hougardy, A linear-time approximation algorithm for weighted matchings in graphs, ACM Transactions on Algorithms 1(1), 107–122, 2005 (cited from the bibliography of Duan and Pettie 2014).
S. Pettie and P. Sanders, A simpler linear time 2/3 − ϵ approximation to maximum weight matching, Information Processing Letters 91(6), 271–276, 2004 (cited from the bibliography of Duan and Pettie 2014).

12 thms2 active usersReviewed

Functional Analysis Operations Research Probability·Captain: mikedeng1

Conditional and Dynamic Convex Risk Measures I: Robust Representation of Conditional Convex Risk MeasuresResearch Paper

Motivation

A convex risk measure assigns to a bounded financial position $X$ (a random net payoff) a number $\rho(X)$ , interpreted as the capital that must be added to $X$ to make it acceptable. The axiomatic theory began with coherent risk measures (Artzner, Delbaen, Eber and Heath, 1999) and was extended to convex ones by Föllmer and Schied (2002) and Frittelli and Rosazza Gianin (2002). Its central structural result is a robust representation: a convex risk measure that is continuous from above equals a worst case of expected losses over a family of probabilistic models, each penalized by how implausible it is.

Regulators and risk managers do not assess positions once and for all; they reassess them as information arrives. Detlefsen and Scandolo (2005) extend the representation to conditional risk measures, whose value $\rho(X)$ is itself a random variable measurable with respect to the information available to the agent. This is the building block of dynamic (time-consistent) risk measurement, studied in later work on dynamic risk measures and backward stochastic differential equations.

Timeline. Artzner et al. (1999): coherent risk measures on finite $\Omega$ . Delbaen (2002): coherent risk measures on general probability spaces, Fatou property. Föllmer–Schied (2002) and Frittelli–Rosazza Gianin (2002): convex risk measures and their robust representation; Föllmer–Schied, Stochastic Finance, Theorem 4.26 (2002 edition) for $L^\infty$ with continuity from above. Detlefsen–Scandolo (2005): the conditional version, Theorem 3.2 of the paper formalized here.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ and a sub- $\sigma$ -algebra $\mathcal G\subseteq\mathcal F$ describing the available information. $L^\infty$ is the space of essentially bounded random variables and $L^\infty_{\mathcal G}$ its $\mathcal G$ -measurable part; every (in)equality between random variables holds $P$ -almost surely.

A map $\rho:L^\infty\to L^\infty_{\mathcal G}$ is a conditional convex risk measure if $\rho(0)=0$ and, for $X,Y\in L^\infty$ :

(conditional translation invariance) $\rho(X+Z)=\rho(X)-Z$ for every $Z\in L^\infty_{\mathcal G}$ ;
(monotonicity) $X\le Y$ implies $\rho(X)\ge\rho(Y)$ ;
(conditional convexity) $\rho(\Lambda X+(1-\Lambda)Y)\le\Lambda\rho(X)+(1-\Lambda)\rho(Y)$ for every $\Lambda\in L^\infty_{\mathcal G}$ with $0\le\Lambda\le1$ .

The admissible models are

\mathcal P_{\mathcal G}=\{Q \text{ probability on }(\Omega,\mathcal F): Q\ll P,\ Q(A)=P(A)\text{ for all }A\in\mathcal G\}.

For a family $\mathcal X$ of $[-\infty,+\infty]$ -valued random variables, the essential supremum $\operatorname{ess.sup}\mathcal X$ is the $P$ -a.s. smallest random variable that dominates every member $P$ -a.s.; it replaces the pointwise supremum, which is not meaningful for uncountable families of equivalence classes.

A map $\rho$ is representable if there is a penalty $\alpha:\mathcal P_{\mathcal G}\to L^0_{\mathcal G}([0,+\infty])$ with

\rho(X)=\operatorname*{ess.sup}_{Q\in\mathcal P_{\mathcal G}}\{-E_Q(X\mid\mathcal G)-\alpha(Q)\},\qquad X\in L^\infty .

The minimal penalty is $\alpha^*(Q)=\operatorname{ess.sup}_{X\in L^\infty}\{-E_Q(X\mid\mathcal G)-\rho(X)\}$ . $\rho$ is continuous from above if $X_n\searrow X$ $P$ -a.s. implies $\rho(X_n)\nearrow\rho(X)$ $P$ -a.s.

Formalization targets

Goal: Theorem 3.2

For a conditional convex risk measure $\rho$ , the following are equivalent:

\text{(a) } \rho \text{ continuous from above}\iff\text{(b) } \rho\text{ representable}\iff\text{(c) } \rho(X)=\operatorname*{ess.sup}_{Q\in\mathcal P_{\mathcal G}}\{-E_Q(X\mid\mathcal G)-\alpha^*(Q)\}.

Milestones

Theorem A.1: existence and a.s. uniqueness of the essential supremum; an increasing sequence converging to it for upward directed families.
Lemma A.2: $E_P(\operatorname{ess.sup}\mathcal X)=\sup_{X\in\mathcal X}E_PX$ for upward directed $\mathcal X$ .
The easy inequality $\rho(X)\ge\operatorname{ess.sup}_{Q}\{-E_Q(X\mid\mathcal G)-\alpha^*(Q)\}$ .
The unconditional representation (Föllmer–Schied, Theorem 4.26) of a convex risk measure $\rho_0:L^\infty\to\mathbb R$ continuous from above: $\rho_0(X)=\sup_{Q\ll P}\{-E_QX-\alpha^*_0(Q)\}$ .
For $\rho_0=E_P[\rho(\cdot)]$ : $\alpha^*_0(Q)<\infty$ forces $Q\in\mathcal P_{\mathcal G}$ .
The family $B_Q=\{-E_Q(X\mid\mathcal G)-\rho(X):X\in L^\infty\}$ is upward directed.
$E_P[\alpha^*(Q)]=\alpha^*_0(Q)$ for $Q\in\mathcal P_{\mathcal G}$ .
Representable implies continuous from above.
Remark 3.3: $\alpha^*\le\alpha$ for every penalty $\alpha$ , and $\alpha^*(Q)=\operatorname{ess.sup}_{X\in\mathcal A_\rho}\{-E_Q(X\mid\mathcal G)\}$ .

Significance

The result. Theorem 3.2 shows that a conditional convex risk measure is determined by a random penalty on the models consistent with the available information, exactly when it satisfies a sequential continuity condition. The representation is the input for the paper's later sections: the conditional entropic risk measure, whose minimal penalty is the conditional relative entropy, and the consistency of dynamic risk measures via Lemma 3.4, which is expressed through the minimal penalty. The restriction to $\mathcal P_{\mathcal G}$ has an interpretation: the more information, the fewer models can enter the worst case.

Formalizing it. The theorem has been proved in the literature since 2005; to our knowledge neither it nor its unconditional counterpart has a machine-checked proof. The mission produces an essential supremum of arbitrary families of extended random variables with its existence theorem, the exchange of expectation and essential supremum for directed families, and the unconditional Föllmer–Schied representation on $L^\infty$ . The last of these is the standard representation theorem of the theory of convex risk measures and is useful well beyond this paper.

Difficulty

The obvious route, applying the unconditional representation pathwise or $\omega$ by $\omega$ , fails: $\rho(X)(\omega)$ is not a risk measure of anything, and conditional expectations are only defined up to null sets that depend on $Q$ , of which there are uncountably many. The essential supremum is what turns an uncountable supremum of classes into a well-defined class, and passing expectations through it requires directedness. The unconditional step itself (continuity from above implies the dual representation) rests on a Krein–Šmulian / weak* closedness argument on $L^\infty$ , which is not available off the shelf.

Formalization scope

Payoffs are real functions $\Omega\to\mathbb R$ with MemLp X ⊤ P; $\rho$ is a map $(\Omega\to\mathbb R)\to(\Omega\to\mathbb R)$ constrained only on $L^\infty$ . Because it acts on functions, $\rho$ is required to respect $P$ -a.s. equality, and $\rho(X)$ is required to be $\mathcal G$ -strongly measurable and essentially bounded; the paper's $\rho$ acts on classes, so this adds nothing in substance. $\mathcal G$ is a MeasurableSpace m with m ≤ mΩ.
Translation invariance and convexity quantify over $\mathcal G$ -measurable $Z$ and $\Lambda$ (not constants). $\mathcal P_{\mathcal G}$ is the subtype of probability measures $Q\ll P$ with $Q(A)=P(A)$ for all $A\in\mathcal G$ — equality on $\mathcal G$ , not mutual absolute continuity.
$E_Q(X\mid\mathcal G)$ is Mathlib's Q[X | m]; it is $\mathcal G$ -measurable, hence determined $P$ -a.s. for $Q\in\mathcal P_{\mathcal G}$ .
Extended values live in EReal; penalties are ENNReal-valued and coerced, so only (real) $-(+\infty)=-\infty$ occurs, never $+\infty-(+\infty)$ .
The essential supremum is a predicate IsEssSup P F Z (a.e. upper bound of every member, a.e. below every a.e.-measurable a.e. upper bound). The minimal penalty is a predicate IsMinimalPenalty on a candidate; statement (c) of the goal asserts that a $\mathcal G$ -measurable $[0,+\infty]$ -valued essential supremum of $B_Q$ is a penalty for $\rho$ .
Continuity from above: $X_n,X\in L^\infty$ , $(X_n)$ a.s. non-increasing and a.s. convergent to $X$ implies $(\rho(X_n))$ a.s. non-decreasing and a.s. convergent to $\rho(X)$ . It is not norm or weak* continuity.
Lemma A.2's "provided the expectations exist" is pinned as: each member has an expectation in $[-\infty,+\infty]$ and some member has integrable negative part (without the latter the lemma is false). Theorem A.1's directed part assumes a nonempty family. The acceptance set of Remark 3.3 is $\{X\in L^\infty:\rho(X)\le0\}$ (the paper's $L^\infty_{\mathcal G}$ on p. 4 is a misprint).
Ruled out: an essential supremum defined as a pointwise ⨆ over the family, or via Mathlib's essSup of a single function, and an index set equal to all $Q\ll P$ or to the $Q$ equivalent to $P$ ; each of these changes statement (b) or makes it vacuous.
Needed infrastructure: essential suprema of families, extended expectations with monotone convergence, conditional expectation under a change of measure agreeing on $\mathcal G$ , and the $L^\infty$ – $L^1$ duality behind Föllmer–Schied 4.26. The essential-supremum layer and the unconditional representation are reusable in any mission on risk measures or robust optimization; contributions to either are welcome.

Selected references

K. Detlefsen, G. Scandolo, Conditional and Dynamic Convex Risk Measures, SFB 649 Discussion Paper 2005-006, Humboldt-Universität zu Berlin, 2005 (the version formalized here; journal version: Finance and Stochastics 9(4), 539–561, 2005, https://doi.org/10.1007/s00780-005-0159-6)
H. Föllmer, A. Schied, Stochastic Finance — An Introduction in Discrete Time, de Gruyter Studies in Mathematics 27, 2002. https://doi.org/10.1515/9783110198065
H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4), 429–447, 2002. https://doi.org/10.1007/s007800200072
M. Frittelli, E. Rosazza Gianin, Putting order in risk measures, Journal of Banking and Finance 26, 1473–1486, 2002. https://doi.org/10.1016/S0378-4266(02)00270-4
P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3), 203–228, 1999. https://doi.org/10.1111/1467-9965.00068
F. Delbaen, Coherent risk measures on general probability spaces, in Advances in Finance and Stochastics, Springer, 2002. https://doi.org/10.1007/978-3-662-04790-3_1

14 thms2 active usersReviewed

Control Theory Operations Research Optimization·Captain: mikedeng1

Optimizing Static Linear Feedback: Gradient Method II: The Gradient Flow Stays in the Sublevel Set and Converges Exponentially under State FeedbackResearch Paper

Motivation

The linear-quadratic regulator (LQR) is the basic problem of optimal control: steer a linear system $\dot x = Ax + Bu$ so as to minimize an integrated quadratic cost of state and input. When the full state is measured, the optimal law is a static linear feedback $u = -Kx$ obtained from an algebraic Riccati equation. When only an output $y = Cx$ is measured, the optimal static output feedback $u = -Ky$ has no closed form, and the problem is nonconvex. In both cases the cost can be written as a function $f(K)$ of the gain alone, which makes it natural to minimize $f$ by gradient methods directly in the space of gains. This view goes back to Levine and Athans (1970) for output feedback and was revived in reinforcement learning by Fazel, Ge, Kakade and Mesbahi (2018), who proved global convergence of policy gradient for discrete-time state-feedback LQR.

Fatkhullin and Polyak (arXiv:2004.09875v2, SIAM J. Control Optim. 2021) carry out this program for the continuous-time problem. They show that $f$ is coercive, that it is $L$ -smooth on every sublevel set, and that under state feedback it satisfies a gradient-domination (Łojasiewicz–Polyak) inequality. From these properties they derive convergence of the continuous gradient flow and of the discrete gradient method. This mission formalizes the continuous part, Theorem 4.1.

Setting

Fix real matrices $A\in\mathbb R^{n\times n}$ , $B\in\mathbb R^{n\times m}$ , $C\in\mathbb R^{r\times n}$ and symmetric positive definite weights $Q\in\mathbb R^{n\times n}$ , $R\in\mathbb R^{m\times m}$ and covariance $\Sigma\in\mathbb R^{n\times n}$ . A gain is $K\in\mathbb R^{m\times r}$ , and the closed-loop matrix is $A_K = A - BKC$ . A square matrix is Hurwitz if all its eigenvalues have negative real part. The stabilizing set is

\mathcal S = \{K : A_K \text{ is Hurwitz}\}.

For $K\in\mathcal S$ , let $X(K)$ and $Y(K)$ be the unique solutions of the Lyapunov equations

A_K^\top X + XA_K + C^\top K^\top RKC + Q = 0,\qquad A_KY + YA_K^\top + \Sigma = 0 .

The LQR cost is $f(K) = \mathrm{Tr}(X(K)\Sigma)$ . It equals the expected infinite-horizon quadratic cost when the initial state has covariance $\Sigma$ . Its gradient with respect to the Frobenius inner product $\langle M,N\rangle = \mathrm{Tr}(M^\top N)$ is

\nabla f(K) = 2\,(RKC - B^\top X(K))\,Y(K)\,C^\top .

Given a known stabilizing gain $K_0\in\mathcal S$ , the sublevel set is $\mathcal S_0 = \{K\in\mathcal S : f(K)\le f(K_0)\}$ . The gradient flow is the ODE

\dot K(t) = -\nabla f(K(t)),\qquad K(0) = K_0 .

State feedback (SLQR) is the case $C = I$ ; there $f$ is written $f_S$ , and $K_*$ denotes a minimizer of $f_S$ on $\mathcal S$ . Norms: $\|\cdot\|_F$ is the Frobenius norm and $\|\cdot\|$ the spectral norm. $\lambda_1(M)$ is the smallest eigenvalue of a symmetric $M$ .

Formalization targets

Goal: Theorem 4.1 for state feedback

For $C=I$ , let $L>0$ be a Lipschitz constant of $\nabla f$ on $\mathcal S_0$ and let $\mu$ be the constant (3.11),

\mu = \frac{\lambda_1(R)\lambda_1^2(\Sigma)\lambda_1(Q)}{8f_S(K_*)\big(\|A\| + \|B\|^2 f_S(K_0)/(\lambda_1(\Sigma)\lambda_1(R))\big)^2}.

Then the flow has a solution on $[0,\infty)$ , and every solution stays in $\mathcal S_0$ , has $f(K_t)$ nonincreasing, has $\nabla f(K_t)\to0$ and $\min_{0\le t\le T}\|\nabla f(K_t)\|_F^2\le f(K_0)/T$ , and

\|K_t - K_*\|_F \le \frac{\sqrt{2L(f(K_0)-f(K_*))}}{\mu}\,e^{-\mu t}\qquad(t\ge0).

Milestones

In attack order:

Existence of a minimizer (Corollary 3.10).
The gradient formula (Lemma 3.11).
Existence of a Lipschitz constant of $\nabla f$ on $\mathcal S_0$ (Theorem 3.15, qualitative).
The gradient-domination inequality $\tfrac12\|\nabla f_S(K)\|_F^2\ge\mu(f_S(K)-f_S(K_*))$ on $\mathcal S_0$ (Theorem 3.17).
The energy identity $\tfrac{d}{dt}f(K_t) = -\|\nabla f(K_t)\|_F^2$ .
The integral bound of Appendix D.1.
The output-feedback part of Theorem 4.1 (general $C$ with $\operatorname{rank} C = r$ ): existence, invariance of $\mathcal S_0$ , monotonicity and (4.2).

Significance

The theorem certifies a simple, model-based procedure: start from any stabilizing gain and follow the negative gradient of the cost. The iterate never loses stability, and it converges exponentially to the optimal gain. The same happens for state feedback even though neither $f$ nor $\mathcal S$ is convex. For output feedback it guarantees convergence to stationarity with an explicit $O(1/T)$ rate. The continuous-time result is the template for the discrete gradient method of the same paper (Theorem 4.2) and for policy-gradient analyses of LQR in learning-based control.

The result is proved in the paper. The paper writes out the proof of (4.2) in Appendix D.1. It describes the whole proof as a replica of Theorems 8 and 9 of Polyak 1963, which treat functions satisfying the Łojasiewicz–Polyak inequality on the whole space. No machine-checked version of any of these statements is known. A formal proof would give the first verified treatment of LQR as an optimization problem over gains. It needs Lyapunov equations, the stabilizing set and the cost, together with the analytic facts on which the policy-gradient literature rests: coercivity, smoothness on sublevel sets, and gradient domination.

Difficulty

The obvious argument is the textbook convergence proof for gradient flows of smooth functions satisfying the Łojasiewicz–Polyak inequality. That proof assumes the function is defined and smooth on the whole space. Here $f$ lives only on the open set $\mathcal S$ , blows up at its boundary, is unbounded on $\mathcal S$ and is not globally $L$ -smooth. The Łojasiewicz–Polyak inequality holds only on $\mathcal S_0$ , with a constant that depends on $K_0$ . The work therefore lies in keeping the trajectory inside $\mathcal S_0$ and showing it exists for all time. This requires compactness of $\mathcal S_0$ (coercivity of $f$ ) and a positive distance from $\mathcal S_0$ to the boundary of $\mathcal S$ . Local ODE existence alone gives neither. The explicit constant $\mu$ additionally requires lower bounds on solutions of Lyapunov equations and an upper bound on $\|K\|_F$ over $\mathcal S_0$ .

Formalization scope

Matrices are Matrix (Fin p) (Fin q) ℝ. Hurwitz means every complex eigenvalue of the complexified matrix has negative real part. $X(K)$ and $Y(K)$ are the unique solutions of their Lyapunov equations. Where the solution is not unique (possible only off $\mathcal S$ ) they take the value $0$ , and no statement uses these off- $\mathcal S$ values. $\nabla f$ is defined by formula (3.3), and Lemma 3.11 states that it is the Fréchet derivative with respect to the Frobenius inner product. A solution of the flow is a curve with $K(0)=K_0$ that stays in $\mathcal S$ for $t\ge0$ . Its entries have the prescribed derivative within $[0,\infty)$ . Global existence and invariance of $\mathcal S_0$ are conclusions, never hypotheses. Assuming a global solution, or a solution confined to $\mathcal S_0$ , would trivialize the theorem, and that encoding is excluded. The case $C=I$ is a matrix argument $C$ with $C=1$ . $\lambda_1$ is the minimum of the (unsorted) eigenvalues, and the spectral norm is $\sqrt{\lambda_{\max}(M^\top M)}$ . "Monotone decreasing" is rendered as nonincreasing. $\min_{0\le t\le T}$ is rendered as the existence of a point of $[0,T]$ where the bound holds.

The standing assumptions of p. 3 are hypotheses wherever they apply: $K_0\in\mathcal S$ , $Q,R,\Sigma\succ0$ , $\operatorname{rank}C=r$ , and $B\ne0$ . Deviations from the printed paper:

The paper's explicit Lipschitz constant (3.8) is false as printed; the planning notes record counterexamples for both output and state feedback. The goal therefore takes $L$ as any Lipschitz constant of $\nabla f$ on $\mathcal S_0$ , which is the paper's own definition of $L$ -smoothness (§3.6). Theorem 3.15 enters only in its qualitative form, as the existence of such an $L$ .
The set-builder for $\mathcal S$ on p. 3 writes $\mathbb R^{m\times n}$ ; gains are $m\times r$ .
The optimal gain $K_*$ is a hypothesis (its existence is Corollary 3.10), and $f(K_*)>0$ is not assumed.

A complete development needs the following: Lyapunov equations and their solution theory (uniqueness, positivity, integral representation), continuity and differentiability of $K\mapsto X(K)$ on $\mathcal S$ , coercivity of $f$ , global existence for ODEs confined to a compact invariant set, and the Łojasiewicz–Polyak argument for flows on a subset. The Lyapunov and stabilizing-set layer is reusable across control missions. Proofs of any milestone, and of auxiliary lemmas such as Lemmas 3.8, A.5, C.1–C.3, are welcome.

Selected references

I. Fatkhullin, B. Polyak, Optimizing Static Linear Feedback: Gradient Method, SIAM J. Control Optim. 59 (2021); preprint arXiv:2004.09875v2. https://arxiv.org/abs/2004.09875
M. Fazel, R. Ge, S. Kakade, M. Mesbahi, Global Convergence of Policy Gradient Methods for the Linear Quadratic Regulator, ICML 2018. https://arxiv.org/abs/1801.05039
W. S. Levine, M. Athans, On the determination of the optimal constant output feedback gains for linear multivariable systems, IEEE Trans. Automat. Control 15 (1970). https://doi.org/10.1109/TAC.1970.1099363
H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak–Łojasiewicz Condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636
B. T. Polyak, Gradient methods for the minimisation of functionals, USSR Comput. Math. Math. Phys. 3 (1963), 864–878. https://doi.org/10.1016/0041-5553(63)90382-3

13 thms2 active usersReviewed

Completed

Convex Optimization Linear algebra Optimization·Captain: mikedeng1

A Singular Value Thresholding Algorithm for Matrix Completion 3: Convergence to the Minimum Nuclear Norm SolutionResearch Paper

Motivation

Nuclear norm minimization is the standard convex surrogate for rank minimization: to recover a low-rank matrix from a few linear measurements, or from a subset of its entries, one minimizes the sum of the singular values subject to the data constraints. For matrix completion, Candès and Recht (Found. Comput. Math. 2009) showed that this convex program recovers a low-rank matrix exactly from sufficiently many random entries. Solving it at scale is another matter: interior-point methods for the equivalent semidefinite program become impractical beyond matrices of a few hundred rows and columns.

Cai, Candès and Shen (SIAM J. Optim. 2010) proposed the singular value thresholding (SVT) algorithm, whose iterates are cheap and typically of low rank. SVT does not solve the nuclear norm problem itself. It solves a proximal problem, in which the nuclear norm is replaced by $\tau\|X\|_* + \tfrac12\|X\|_F^2$ for a fixed parameter $\tau>0$ . Section 3.4 of the paper justifies this substitution: as $\tau\to\infty$ , the solutions of the proximal problem converge to a specific solution of the nuclear norm problem, the one of least Frobenius norm. This mission formalizes that result, Theorem 3.1 of the paper, under general convex constraints.

Setting

Let $n_1, n_2$ be natural numbers and $\mathbb R^{n_1\times n_2}$ the space of real $n_1\times n_2$ matrices, with the inner product $\langle X, Y\rangle = \operatorname{trace}(X^*Y) = \sum_{i,j}X_{ij}Y_{ij}$ . Three functions of a matrix $X$ are used:

the Frobenius norm $\|X\|_F = \sqrt{\langle X, X\rangle}$ ;
the nuclear norm $\|X\|_*$ , the sum of the singular values of $X$ ;
for a parameter $\tau$ , the proximal objective $f_\tau(X) = \tau\|X\|_* + \tfrac12\|X\|_F^2$ .

Let $f_1,\dots,f_m:\mathbb R^{n_1\times n_2}\to\mathbb R$ be constraint functions and $\mathcal C = \{X : f_i(X)\le 0,\ i = 1,\dots,m\}$ the feasible set. The nuclear norm problem is

\text{(1.6)}\qquad \text{minimize } \|X\|_* \quad \text{subject to } f_i(X)\le 0,\ i=1,\dots,m,

and, for $\tau>0$ , the proximal problem is

\text{(3.4)}\qquad \text{minimize } f_\tau(X) \quad \text{subject to } f_i(X)\le 0,\ i=1,\dots,m.

When the $f_i$ are convex and $\mathcal C$ is nonempty, (3.4) has exactly one solution, written $X^\star_\tau$ , because $f_\tau$ is strongly convex. Problem (1.6) may have many solutions. Among them, the paper singles out the minimum Frobenius norm solution

\text{(3.14)}\qquad X_\infty := \arg\min_X\{\|X\|_F^2 : X \text{ is a solution of (1.6)}\}.

Linear equality constraints, and in particular the matrix completion constraints $X_{ij} = M_{ij}$ for sampled entries $(i,j)$ , are covered by taking pairs of affine functionals.

Formalization targets

Goal: Theorem 3.1

Assume that the $f_i$ are convex and lower semicontinuous. Then

\text{(3.15)}\qquad \lim_{\tau\to\infty}\|X^\star_\tau - X_\infty\|_F = 0.

Milestones

In the order in which the paper's proof uses them (all on p. 1967):

Eq. (3.16), for every $\tau>0$ :

\|X^\star_\tau\|_* + \frac{1}{2\tau}\|X^\star_\tau\|_F^2 \le \|X_\infty\|_* + \frac{1}{2\tau}\|X_\infty\|_F^2 \quad\text{and}\quad \|X_\infty\|_*\le\|X^\star_\tau\|_*.

Eq. (3.17), for every $\tau>0$ : $\|X^\star_\tau\|_F^2 \le \|X_\infty\|_F^2$ .
Convergence of the nuclear norms: $\lim_{\tau\to\infty}\|X^\star_\tau\|_* = \|X_\infty\|_*$ .
Uniqueness of $X_\infty$ : two minimum Frobenius norm solutions of (1.6) coincide when the $f_i$ are convex.
Cluster points: if $\tau_k\to\infty$ and $X^\star_{\tau_k}\to X_c$ , then $X_c = X_\infty$ .

Significance

The result itself. Theorem 3.1 is the link between the problem SVT actually solves and the problem one wants solved. The companion missions of this series prove that the SVT iteration, and its variant for general convex constraints, converges to $X^\star_\tau$ . Theorem 3.1 says what $X^\star_\tau$ is worth: for large $\tau$ it is close to a nuclear norm minimizer, and the minimizer it approaches is identified exactly, namely the one of least Frobenius norm. The statement is not specific to matrix completion. It covers every finite family of convex, lower semicontinuous constraints, and hence noisy variants such as the inequality-constrained problems of §3.3 of the paper.

Formalizing it. The theorem is proved in the paper, in about half a page. It has not, to our knowledge, been machine-checked. A formal proof pins down the hypotheses: the argument needs the minimizers to exist, and it uses continuity and convexity of the nuclear norm, closedness of the feasible set, and uniqueness of $X_\infty$ . It also produces a reusable fact about the nuclear norm in Lean, namely that the sum of singular values is a continuous convex function of the matrix.

Difficulty

The first steps are elementary consequences of the definitions of $X^\star_\tau$ and $X_\infty$ : (3.16) compares objective values, and (3.17) and the convergence of the nuclear norms follow by algebra and a squeeze. The difficulty lies elsewhere.

Identifying the limit. Boundedness gives cluster points of $X^\star_\tau$ , not convergence. Each cluster point must be shown to be feasible, to be optimal for (1.6), and to have the least Frobenius norm among the optimal points. Feasibility uses lower semicontinuity of the constraints. Optimality uses continuity of the nuclear norm. Minimality uses (3.17) passed to the limit.
Uniqueness of $X_\infty$ . The last step concludes $X_c = X_\infty$ from $\|X_c\|_F = \|X_\infty\|_F$ , which needs uniqueness of the minimum Frobenius norm solution. That in turn needs convexity of the solution set of (1.6), hence convexity of the nuclear norm, together with strict convexity of $\|\cdot\|_F^2$ .
Nuclear norm in Lean. The nuclear norm is defined from singular values, and its convexity (the triangle inequality for the sum of singular values) and continuity are not currently available as ready-made statements. They are the main groundwork.

A tempting shortcut, reading the family $X^\star_\tau$ as a sequence indexed by integers, proves a weaker statement: the limit in (3.15) is over real $\tau\to\infty$ .

Formalization scope

Matrices. Matrices are Matrix (Fin n₁) (Fin n₂) ℝ, abbreviated Mat n₁ n₂, over the reals as in the paper. $\langle X,Y\rangle = \sum_{i,j}X_{ij}Y_{ij}$ and $\|X\|_F = \sqrt{\langle X,X\rangle}$ .
Nuclear norm. $\|X\|_*$ is the sum of Mathlib's LinearMap.singularValues of Matrix.toEuclideanLin X. It is the genuine sum of singular values, not an abstract norm or the Frobenius norm.
Constraints. The constraints are a family f : Fin m → Mat n₁ n₂ → ℝ of real-valued functions. $m = 0$ (no constraints) is allowed.
Hypotheses of Theorem 3.1. The hypotheses are ConvexOn ℝ Set.univ (f i) and LowerSemicontinuous (f i) for every $i$ . Lower semicontinuity is redundant for real-valued convex functions on a finite-dimensional space, but it is kept because the theorem states it.
$X^\star_\tau$ and $X_\infty$ . $X^\star_\tau$ is a family Xτ : ℝ → Mat n₁ n₂ assumed to solve (3.4) for every $\tau>0$ , and its values at $\tau\le 0$ play no role. $X_\infty$ is a matrix assumed to satisfy the defining property (3.14): it solves (1.6) and has the least $\|\cdot\|_F^2$ among its solutions. Uniqueness of $X_\infty$ is a milestone to prove, not an assumption.
Vacuous case. These hypotheses presuppose, as the paper does, that (1.6) has a solution. They can be met exactly when the feasible set is nonempty. When it is empty the statement is vacuous, which matches the paper, where $X_\infty$ is then undefined.
Limits and topology. Limits in $\tau$ are along Filter.atTop on $\mathbb R$ . Convergence of matrices uses Mathlib's entrywise topology, which is the topology of $\|\cdot\|_F$ . The goal states (3.15) literally, with the Frobenius norm of the difference tending to $0$ .
Excluded shortcuts. A formalization that replaces the nuclear norm by the Frobenius norm or by an arbitrary norm, indexes $\tau$ by $\mathbb N$ , or assumes uniqueness or convergence as a hypothesis would not be Theorem 3.1. It is ruled out.

Infrastructure. The needed facts, all reusable beyond this mission:

nonnegativity, convexity and continuity of the nuclear norm on real matrices;
closedness and convexity of sublevel sets of convex lower semicontinuous functions;
uniqueness of the minimizer of a strictly convex function over a convex set;
a cluster-point argument for bounded families in finite-dimensional spaces.

Contributions of these general lemmas as separate theorems are welcome.

Selected references

J.-F. Cai, E. J. Candès, Z. Shen, A Singular Value Thresholding Algorithm for Matrix Completion, SIAM J. Optim. 20(4):1956–1982, 2010. https://doi.org/10.1137/080738970
E. J. Candès, B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9:717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5
B. Recht, M. Fazel, P. A. Parrilo, Guaranteed Minimum-Rank Solutions of Linear Matrix Equations via Nuclear Norm Minimization, SIAM Rev. 52(3):471–501, 2010. https://doi.org/10.1137/070697835

8 thms2 active usersReviewed

Completed

Convex Optimization Linear algebra Numerical Analysis+1·Captain: mikedeng1

A Singular Value Thresholding Algorithm for Matrix Completion 2: Convergence of the SVT Iteration under General Convex ConstraintsResearch Paper

Motivation

Singular value thresholding (SVT) is a first-order method introduced by Cai, Candès and Shen (SIAM J. Optim. 20 (2010)) for recovering a low-rank matrix from incomplete or indirect information. Its basic form, for matrix completion, alternates a soft-thresholding of singular values with a gradient step on a dual variable, and needs only one sparse singular value decomposition per iteration. That is what made nuclear-norm heuristics usable on matrices with tens of thousands of rows and columns, where interior-point methods for the equivalent semidefinite program do not fit in memory.

Matrix completion is only one constraint set. In applications the data are noisy linear measurements $b = \mathcal A(M) + z$ , and the constraint takes the form of componentwise error bounds or norm balls around the data (§3.3 of the paper). Section 3.2 of the paper extends the method to a general finite family of convex constraints, and §4.2 proves that the extended iteration converges. This mission formalizes that extension and its convergence theorem, Theorem 4.4.

Setting

Let $n_1, n_2, m$ be natural numbers and $\mathbb R^{n_1\times n_2}$ the real $n_1\times n_2$ matrices, with the Frobenius inner product $\langle X, Y\rangle = \sum_{i,j} X_{ij}Y_{ij}$ and norm $\|X\|_F = \sqrt{\langle X, X\rangle}$ . The nuclear norm $\|X\|_*$ is the sum of the singular values of $X$ . For a fixed $\tau > 0$ the objective is

f_\tau(X) = \tau\|X\|_* + \tfrac12\|X\|_F^2 .

A matrix $Z$ is a subgradient of a function $g$ at $X_0$ , written $Z\in\partial g(X_0)$ , if $g(X)\ge g(X_0) + \langle Z, X - X_0\rangle$ for all $X$ .

Let $f_1,\dots,f_m:\mathbb R^{n_1\times n_2}\to\mathbb R$ be convex and put $\mathcal F(X) = (f_1(X),\dots,f_m(X))\in\mathbb R^m$ . On $\mathbb R^m$ , $\langle u, v\rangle = \sum_i u_iv_i$ and $\|v\|$ is the Euclidean norm. The constrained problem is

\text{(3.4)}\qquad \text{minimize } f_\tau(X)\quad\text{subject to } f_i(X)\le 0,\ i=1,\dots,m,

with Lagrangian $\mathcal L(X, y) = f_\tau(X) + \langle y, \mathcal F(X)\rangle$ for $y\ge 0$ . A pair $(X^\star, y^\star)$ with $y^\star\ge0$ is primal-dual optimal if it is a saddle point:

\mathcal L(X^\star, y)\le \mathcal L(X^\star, y^\star)\le \mathcal L(X, y^\star)\qquad\text{for all } y\ge 0,\ X .

The paper's standing assumption "strong duality holds" is the existence of such a pair.

The iteration (3.5) starts from $y^0 = 0$ and, for step sizes $\delta_k$ , sets for $k = 1, 2, \dots$

X^k = \arg\min_X\{f_\tau(X) + \langle y^{k-1}, \mathcal F(X)\rangle\},\qquad y^k = [\,y^{k-1} + \delta_k\mathcal F(X^k)\,]_+ ,

where $x_+$ has entries $\max(x_i, 0)$ . It is Uzawa's method for (3.4): an exact minimization in the primal variable followed by a projected ascent step on the dual. When $\mathcal F(X) = b - \mathcal A(X)$ is affine, the minimization is a singular value thresholding step, which gives the algorithm its name.

The analysis of §4.2 assumes $\mathcal F$ is Lipschitz in the sense

\text{(4.2)}\qquad \|\mathcal F(X) - \mathcal F(Y)\|\le L\,\|X - Y\|_F\quad\text{for all } X, Y,

for a constant $L\ge 0$ .

Formalization targets

Goal: Theorem 4.4 (p. 1969)

If $0 < \inf_k\delta_k\le\sup_k\delta_k < 2/L^2$ and strong duality holds, then the sequence $X^k$ of (3.5) converges to the unique solution of (3.4):

\exists!\,X^\star\ \text{solving (3.4)},\qquad \lim_{k\to\infty} X^k = X^\star .

Milestones, in the order the proof uses them

Lemma 4.1 (p. 1968): $\langle Z - Z', X - X'\rangle\ge\|X - X'\|_F^2$ for $Z\in\partial f_\tau(X)$ , $Z'\in\partial f_\tau(X')$ .
Lemma 4.3 (p. 1969): for a primal-dual optimal pair and each $\delta > 0$ , $y^\star = [y^\star + \delta\mathcal F(X^\star)]_+$ .
Eq. (4.4) (p. 1969): there are $Z^k\in\partial f_\tau(X^k)$ and $Z^\star\in\partial f_\tau(X^\star)$ with $\langle Z^k, X - X^k\rangle + \langle y^{k-1}, \mathcal F(X) - \mathcal F(X^k)\rangle\ge 0$ and $\langle Z^\star, X - X^\star\rangle + \langle y^\star, \mathcal F(X) - \mathcal F(X^\star)\rangle\ge 0$ for all $X$ .
Eq. (4.5) (p. 1969): $\langle y^{k-1} - y^\star, \mathcal F(X^k) - \mathcal F(X^\star)\rangle\le -\|X^k - X^\star\|_F^2$ .
Contraction step (p. 1969): $\|y^k - y^\star\|\le\|y^{k-1} - y^\star + \delta_k(\mathcal F(X^k) - \mathcal F(X^\star))\|$ .
Eq. (4.6) (p. 1970): if $2\delta_k - \delta_k^2L^2\ge\beta > 0$ for $k\ge1$ , then $\|y^k - y^\star\|^2\le\|y^{k-1} - y^\star\|^2 - \beta\|X^k - X^\star\|_F^2$ .

Significance

The result. Theorem 4.4 is the convergence guarantee for SVT beyond matrix completion. The componentwise error bounds of (3.8), whose SVT iteration is (3.9), are finitely many affine constraints and fall under it directly, as does any finite family of Lipschitz convex constraints, for instance a Frobenius-norm ball around the data. The conic variants of §3.3 ((3.11)–(3.13)) project the dual variable onto a cone rather than onto the nonnegative orthant and are not covered by the theorem as stated. Together with Theorem 3.1 of the same paper, which says that the solution of (3.4) tends to the minimum-nuclear-norm solution as $\tau\to\infty$ , it justifies using SVT as a solver for nuclear-norm minimization under general convex constraints.

Formalizing it. The theorem is proved in the paper, with two steps delegated to the literature: Lemma 4.3 cites [31], and the concluding step reads "the conclusion is as before". Its proof is short but relies on convex-analytic facts that are standard on paper and missing, in this form, from Mathlib: subgradients of the nuclear norm, the subdifferential sum rule for finite convex functions, and nonexpansiveness of the projection onto the nonnegative orthant. No machine-checked proof of this theorem or of Uzawa-type convergence for nuclear-norm objectives is known to exist. The mission produces a complete, checked version of the argument, including the omitted closing step.

Difficulty

The obvious approach is to view (3.5) as projected gradient ascent on the dual function $g(y) = \min_X\mathcal L(X, y)$ and quote the standard convergence theorem for gradient methods with Lipschitz gradients. That does not apply directly: for general convex $f_i$ the dual function need not be differentiable, $\mathcal F(X^k)$ is only a supergradient, and the Lipschitz hypothesis (4.2) is on $\mathcal F$ , not on a dual gradient. The proof instead works with the primal-dual pair: it needs first-order optimality conditions (4.4), which require a subdifferential sum rule for $f_\tau + \sum_i y_i f_i$ with nonsmooth $f_i$ , and it needs the strong monotonicity of $\partial f_\tau$ (Lemma 4.1), which depends on the description of subgradients of the nuclear norm. A second subtlety is that the theorem asserts convergence of the whole primal sequence to the unique solution, not to some solution along a subsequence, while nothing is claimed about convergence of the dual sequence.

Formalization scope

Matrices are Matrix (Fin n₁) (Fin n₂) ℝ, vectors in $\mathbb R^m$ are Fin m → ℝ, and convergence of matrices is in Mathlib's product topology, which coincides with the Frobenius topology. The nuclear norm is the sum of Mathlib's LinearMap.singularValues of the matrix viewed as a map between Euclidean spaces. Each $f_i$ is a real-valued function with ConvexOn ℝ Set.univ. The iteration is a predicate on sequences indexed by ℕ: the paper's step $k$ produces X (k+1) and y (k+1) from y k with step size δ (k+1), and y 0 = 0. $X^k$ is required to minimize $\mathcal L(\cdot, y^{k-1})$ ; for $\tau>0$ and convex $f_i$ this minimizer exists and is unique, so the predicate is satisfiable and determines the sequence. The step-size condition is stated as $a\le\delta_k\le C$ for $k\ge1$ with $a>0$ and $C L^2 < 2$ , which avoids the division $2/L^2$ (evaluated as $0$ in Lean when $L=0$ ); for $L=0$ it requires only bounded steps, matching the convention $2/0 = \infty$ . Strong duality is the hypothesis that a saddle point exists; Slater's condition is not assumed. The paper's standing assumptions ( $\tau>0$ , convex $f_i$ , and (4.2) where $L$ enters) appear as explicit hypotheses in every statement.

A formalization that assumes convergence or boundedness of the dual iterates, replaces the primal minimization by a closed-form thresholding step (valid only for affine $\mathcal F$ ), or states only subsequential convergence would not be this theorem; each of these is excluded by the statements above.

A complete development needs: subgradients of the nuclear norm and strong monotonicity of $\partial f_\tau$ ; existence and characterization of minimizers of strongly convex continuous functions on a finite-dimensional space; the subdifferential sum rule for finite convex functions; complementary slackness from the saddle-point inequalities; and nonexpansiveness of the entrywise positive part. These are reusable beyond this mission, especially for other Uzawa and augmented Lagrangian analyses. Contributions of any of these pieces as separate lemmas are welcome.

Selected references

J.-F. Cai, E. J. Candès, Z. Shen, A Singular Value Thresholding Algorithm for Matrix Completion, SIAM J. Optim. 20(4):1956–1982, 2010. https://doi.org/10.1137/080738970
E. J. Candès, B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9:717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5
K. J. Arrow, L. Hurwicz, H. Uzawa, Studies in Linear and Nonlinear Programming, Stanford University Press, 1958.
S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511804441

9 thms2 active usersReviewed

Completed

Convex Optimization Linear algebra Numerical Analysis+1·Captain: mikedeng1

A Singular Value Thresholding Algorithm for Matrix Completion 1: The SVT Iteration Converges to the Unique Solution of the Proximal ProblemResearch Paper

Motivation

Matrix completion asks to recover an $n_1\times n_2$ matrix $M$ from a subset $\Omega$ of its entries. When $M$ has low rank, a standard convex surrogate is to minimize the nuclear norm $\|X\|_*$ (the sum of the singular values) subject to agreeing with $M$ on $\Omega$ ; Candès and Recht showed that this recovers $M$ exactly under incoherence and sampling conditions (Candès–Recht 2009). Generic interior-point solvers for this semidefinite program do not scale beyond matrices of a few hundred rows.

Cai, Candès and Shen (SIAM J. Optim. 2010) proposed the singular value thresholding (SVT) algorithm: a first-order iteration whose only nonlinear step is a soft-thresholding of singular values, and whose other iterate is a sparse matrix supported on $\Omega$ . The algorithm has become a standard baseline in low-rank matrix recovery and a model example of dual (Uzawa-type) methods for nuclear-norm problems. This mission formalizes its convergence theorem.

Setting

All matrices are real. For $X,Y\in\mathbb R^{n_1\times n_2}$ write $\langle X,Y\rangle=\operatorname{trace}(X^*Y)=\sum_{i,j}X_{ij}Y_{ij}$ and $\|X\|_F^2=\langle X,X\rangle$ . The nuclear norm $\|X\|_*$ is the sum of the singular values of $X$ .

For an index set $\Omega$ , the sampling projector $P_\Omega$ keeps the entries with indices in $\Omega$ and sets the others to zero.

A reduced singular value decomposition of a matrix $Y$ of rank $r$ is $Y=U\Sigma V^*$ with $U$ ( $n_1\times r$ ) and $V$ ( $n_2\times r$ ) having orthonormal columns and $\Sigma=\operatorname{diag}(\sigma_1,\dots,\sigma_r)$ with $\sigma_i>0$ . For $\tau\ge0$ the singular value shrinkage operator is

\mathcal D_\tau(Y)=U\operatorname{diag}\big((\sigma_i-\tau)_+\big)V^*,\qquad t_+=\max(0,t).

Fix $\tau>0$ , a sequence of step sizes $\{\delta_k\}_{k\ge1}$ and data $M$ . The SVT iteration (2.7) starts from $Y^0=0$ and sets, for $k=1,2,\dots$ ,

X^k=\mathcal D_\tau(Y^{k-1}),\qquad Y^k=Y^{k-1}+\delta_k P_\Omega(M-X^k).

The proximal problem (2.8) is

\text{minimize}\ \ f_\tau(X)=\tau\|X\|_*+\tfrac12\|X\|_F^2\quad\text{subject to}\ \ P_\Omega(X)=P_\Omega(M).

More generally, for a linear map $\mathcal A:\mathbb R^{n_1\times n_2}\to\mathbb R^m$ with adjoint $\mathcal A^*$ and spectral norm $\|\mathcal A\|=\sup\{\|\mathcal A(X)\|_{\ell_2}:\|X\|_F=1\}$ , and $b\in\mathbb R^m$ , problem (3.1) is to minimize $f_\tau(X)$ subject to $\mathcal A(X)=b$ , and Uzawa's iteration (3.3) starts from $y^0=0$ and sets $X^k=\mathcal D_\tau(\mathcal A^*(y^{k-1}))$ , $y^k=y^{k-1}+\delta_k(b-\mathcal A(X^k))$ .

Formalization targets

Goal: Theorem 4.2, second sentence (p. 1968)

If $0<\inf_k\delta_k\le\sup_k\delta_k<2$ , then (2.8) has a unique solution $X^\star$ and the SVT iterates satisfy

\lim_{k\to\infty}X^k=X^\star .

Theorem 4.2, first sentence (p. 1968)

If (3.1) is feasible and $0<\inf_k\delta_k\le\sup_k\delta_k<2/\|\mathcal A\|^2$ , then (3.1) has a unique solution and the iterates $X^k$ of (3.3) converge to it.

Supporting results (milestones, in attack order)

Well-definedness of $\mathcal D_\tau$ (§2.1, p. 1960): the output does not depend on the chosen SVD.
Theorem 2.1 (p. 1960): $\mathcal D_\tau(Y)=\arg\min_X \tfrac12\|X-Y\|_F^2+\tau\|X\|_*$ .
Sparsity of the iterates (§2.2, p. 1961): since $Y^0=0$ , every $Y^k$ vanishes outside $\Omega$ .
Eq. (2.14) (p. 1964): the minimizers of the Lagrangian $f_\tau(X)+\langle Y,P_\Omega(M-X)\rangle$ are those of $\tau\|X\|_*+\tfrac12\|X-P_\Omega Y\|_F^2$ .
Lemma 4.1 (p. 1968): for $Z\in\partial f_\tau(X)$ , $Z'\in\partial f_\tau(X')$ , $\langle Z-Z',X-X'\rangle\ge\|X-X'\|_F^2$ .
The §3.1 reduction (p. 1964): for a sampling operator, $\mathcal A^*\mathcal A=P_\Omega$ and (3.3) becomes (2.7) under $Y^k=\mathcal A^*(y^k)$ .
Theorem 4.2, first sentence, as above.

Significance

The theorem certifies that SVT, run with any step sizes in a fixed interval $(0,2)$ , computes the unique minimizer of the strongly convex surrogate (2.8). Together with the separate fact that the solution of (2.8) tends to the minimum nuclear norm completion as $\tau\to\infty$ (the paper's Theorem 3.1, a companion mission), this is what justifies using SVT as a solver for nuclear-norm matrix completion. Theorem 2.1, the proximal characterization of singular value soft-thresholding, is used throughout the literature on proximal methods for low-rank problems.

The paper's proof of Theorem 4.2 consists of the reduction to Uzawa's method and a citation of a general convergence theorem for projected gradient methods on the dual. The formalization produces a self-contained, machine-checked chain: the proximal characterization of $\mathcal D_\tau$ , the Lagrangian identity, strong monotonicity of $\partial f_\tau$ , and the convergence argument itself. To our knowledge none of these results has a machine-checked proof; Mathlib at the pinned revision has singular values of linear maps but no SVD structure, no nuclear norm and no subgradient calculus.

Difficulty

Nothing in the iteration is a gradient step of a smooth function in $X$ : the $X$ -update is a nonsmooth proximal map, and the convergence of $X^k$ is not visible from the recursion itself. The paper's argument cites a general theorem on projected gradient methods ([25, Theorem 2.1]) and takes for granted that "strong duality holds" for (2.8) (p. 1963), so the existence of a Lagrange multiplier is part of what must be formalized. Theorem 2.1 depends on the subdifferential of the nuclear norm, which Mathlib does not provide, and therefore on the singular value decomposition and the duality between the nuclear and spectral norms. Convergence of objective values or of a subsequence would not suffice: the target is convergence of the whole sequence $X^k$ to the unique solution.

Formalization scope

Matrices are Matrix (Fin n₁) (Fin n₂) ℝ; convergence is Mathlib's topology on matrices, which coincides with the Frobenius-norm topology. $\langle\cdot,\cdot\rangle$ and $\|\cdot\|_F$ are defined entrywise; $\|X\|_*$ is the sum of Mathlib's LinearMap.singularValues of $X$ viewed as a map $\mathbb R^{n_2}\to\mathbb R^{n_1}$ . The shrinkage operator is a relation IsShrink τ Y X defined, as in (2.1)–(2.2), through some reduced SVD of $Y$ ; well-definedness is a milestone. It is not defined as the minimizer of (2.3), which would make Theorem 2.1 definitional. Linear maps $\mathcal A$ are given by matrices $A_1,\dots,A_m$ with $\mathcal A(X)_i=\langle A_i,X\rangle$ , and a sampling operator by an injective enumeration of $\Omega$ . Subgradients are those of (2.4).

Sequences are indexed by $\mathbb N$ : Lean's step $k+1$ is the paper's step $k$ , so $X^0$ and $\delta_0$ are unused. Committed conventions:

$Y^0=0$ and $y^0=0$ are hypotheses; with a start that is nonzero outside $\Omega$ the iterates converge to a different matrix.
The standing $\tau>0$ is kept, except in Theorem 2.1 and the well-definedness statement, which are printed for $\tau\ge0$ .
The step-size conditions are explicit bounds $a>0$ , $C$ with $a\le\delta_k\le C$ for $k\ge1$ , together with $C<2$ , respectively $C\|\mathcal A\|^2<2$ . The multiplicative form avoids Lean's $x/0=0$ : for $\mathcal A=0$ the condition does not become unsatisfiable.
Feasibility of (3.1) is an added hypothesis of Theorem 4.2's first sentence, since "the unique solution" presupposes it.
"Converges to the unique solution" is stated as existence and uniqueness of the solution together with convergence of the whole sequence to it.

A small unprinted helper, $\|\mathcal A\|\le1$ for sampling operators, is included to pass from the first sentence of Theorem 4.2 to the second; it is not a milestone. The subdifferential formula (2.6) of the nuclear norm and the Fejér-type condition of §5.1.2 are not stated. Reusable infrastructure welcome from solvers: existence and uniqueness properties of the reduced SVD, the nuclear/spectral norm duality, the subdifferential of the nuclear norm, and a general convergence theorem for Uzawa's method with a strongly convex objective.

Selected references

J.-F. Cai, E. J. Candès, Z. Shen, A Singular Value Thresholding Algorithm for Matrix Completion, SIAM J. Optim. 20(4):1956–1982, 2010. https://doi.org/10.1137/080738970
E. J. Candès, B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9:717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5
K. J. Arrow, L. Hurwicz, H. Uzawa, Studies in Linear and Non-Linear Programming, Stanford University Press, 1958.

12 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems 1: The Augmentation Bound for Shortest Augmenting PathsResearch Paper

Why the number of augmentations matters

The maximum flow problem asks how much of a commodity can be sent from a source to a sink through a network whose arcs have capacities. It is a basic model in operations research, underlies bipartite matching, transportation and scheduling problems, and is a standard subroutine inside larger combinatorial algorithms.

The classical method for it is the labeling method of Ford and Fulkerson: starting from some flow, repeatedly find an augmenting path from source to sink along which flow can be increased, push as much as the path allows, and stop when no such path exists. When all capacities are integers, each augmentation raises the flow value by at least one, so the method terminates, but the number of augmentations can be as large as the final flow value, which is exponential in the size of the input. Edmonds and Karp give a four-node example in which the method alternates between two paths and needs $2M$ augmentations for capacities $M$ (Edmonds–Karp 1972, p. 250). With irrational capacities, Ford and Fulkerson showed that the method need not terminate at all and may converge to a non-maximum flow.

Timeline.

1956 — Ford and Fulkerson introduce the labeling method and the max-flow min-cut theorem (Ford–Fulkerson 1956).
1962 — Flows in Networks records the non-termination example for incommensurable capacities.
1970 — Dinic independently obtains a polynomial bound using layered (shortest-path) networks (Dinic 1970).
1972 — Edmonds and Karp prove that choosing each augmenting path with fewest arcs bounds the number of augmentations by $\tfrac14(n^3-n)$ , for arbitrary real capacities (Edmonds–Karp 1972, Theorem 1).

Setting

A network $N$ consists of a finite set of $n$ nodes, a source $s$ and a sink $t \ne s$ , and a set of arcs, which are ordered pairs $(u,v)$ with $u \ne v$ ; there is at most one arc from a node to another. One arc is the special return arc $(t,s)$ , and $A$ denotes the set of all other arcs. Each $(u,v) \in A$ has a real capacity $c(u,v) > 0$ .

A flow is a nonnegative function $f$ on the arcs of $N$ with $f(u,v) \le c(u,v)$ on $A$ and with inflow equal to outflow at every node, the return arc included. The value $f(t,s)$ is the amount sent from $s$ to $t$ ; a maximum flow maximizes it.

Given a flow $f$ , the residual network $N^f$ has the same nodes, and $(u,v)$ is an arc of $N^f$ when $(u,v) \in A$ with $c(u,v) - f(u,v) > 0$ , or $(v,u) \in A$ with $f(v,u) > 0$ . An augmenting path is a sequence of distinct nodes $s = u_1, \dots, u_p = t$ whose consecutive pairs are arcs of $N^f$ . Each step carries a number $\varepsilon_i > 0$ (residual capacity forward, flow backward, or their sum when both $(u_i,u_{i+1})$ and $(u_{i+1},u_i)$ lie in $A$ ); $\varepsilon = \min_i \varepsilon_i$ , and a step with $\varepsilon_i = \varepsilon$ is a bottleneck arc. Augmenting raises $f(t,s)$ by $\varepsilon$ and shifts the flow on the path's arcs accordingly, using the paper's own rule for opposite arcs, which never exceeds a capacity.

A run with fewest-arc augmentations is a sequence $f^0, \dots, f^K$ where $f^0$ is a flow and each $f^{k+1}$ arises from $f^k$ by augmenting along a path $P^k$ with fewest arcs. The distance $\delta^k(u,v)$ is the least number of arcs of a directed path from $u$ to $v$ in $N^k = N^{f^k}$ , or $\infty$ .

Formalization targets

Goal — Theorem 1

For every network on $n$ nodes and every run of length $K$ with fewest-arc augmentations,

K \le \tfrac14\,(n^3 - n),

and if no augmenting path exists relative to $f^K$ , then $f^K$ is a maximum flow. The capacities are arbitrary positive reals, and the initial flow is arbitrary.

Milestones

§1.1: augmentation yields a flow with value $f(t,s) + \varepsilon$ , $\varepsilon > 0$ .
§1.1: a flow is maximum if and only if it admits no augmenting path.
Proposition 1: a bottleneck arc of $P^k$ is not an arc of $N^{k+1}$ .
Proposition 2: $(u,v) \in N^{k+1}$ implies $(u,v) \in N^k$ or $(v,u) \in P^k$ .
Lemma 1: if $(u,v)$ is a bottleneck arc at steps $k < m$ , then $(v,u) \in P^l$ for some $k < l < m$ .
Proposition 3: $\delta^k(s,u) \le \delta^{k+1}(s,u)$ and $\delta^k(u,t) \le \delta^{k+1}(u,t)$ .
Lemma 2: if $k < l$ , $(u,v) \in P^k$ and $(v,u) \in P^l$ , then $\delta^l(s,t) \ge \delta^k(s,t) + 2$ .
Proof of Theorem 1: each pair $\{u,v\}$ occurs as a bottleneck at most $\tfrac12(n+1)$ times.

Significance

The theorem shows that one simple rule for choosing augmenting paths, which a breadth-first labeling process implements, makes the number of augmentations depend on the number of nodes alone, independent of the capacities and of their arithmetic nature. It removes both pathologies of the unrestricted labeling method at once: exponential running time for integer capacities, and non-termination for irrational ones. Together with Dinic's work it is the starting point of the theory of strongly polynomial network-flow algorithms, and the distance-monotonicity argument (Proposition 3, Lemma 2) reappears in blocking-flow and push-relabel analyses.

The result is classical and fully proved in the paper. What this mission adds is a machine-checked version of the complete argument in the paper's own model: return arc, arbitrary real capacities, and the paper's augmentation rule for pairs of opposite arcs, which differs from Ford and Fulkerson's (footnote 1, p. 249). The platform has a max-flow min-cut theorem and an integer termination theorem for the Ford–Fulkerson method in the Bertsimas–Tsitsiklis model (Introduction to Linear Optimization, missions IX–X), but no bound on the number of augmentations. No machine-checked proof of Theorem 1 in Lean is known to exist.

Difficulty

The obvious argument, "each augmentation saturates a bottleneck arc, which then disappears", fails because a saturated arc can reappear after later augmentations push flow back along its reverse. Counting augmentations therefore requires control over how often the same pair of nodes can supply a bottleneck again, and no property of a single augmentation provides it; the bound has to come from an invariant of the whole run that holds for real capacities, where no integrality argument is available. A second trap is that the converse direction of milestone 2 (no augmenting path implies maximality) is a max-flow min-cut statement that the paper cites without proof; it must be proved in the paper's model with the return arc.

Formalization scope

Nodes form a finite type V with decidable equality and $n$ = Fintype.card V counts all nodes, $s$ and $t$ included. The arc set A is a Finset (V × V) with no loops and without $(t,s)$ ; capacities are real and positive on A. A flow is a function V → V → ℝ whose values off the arcs are ignored. A maximum flow is the predicate " $f(t,s) \ge g(t,s)$ for every flow $g$ ", never a real supremum. Paths are lists of distinct nodes with every consecutive pair a residual arc, so the return arc is never on a path. Distances take values in ℕ∞. A run is a pair of ℕ-indexed sequences constrained on indices up to $K$ . The explicit constants are stated as printed: $4K \le n^3 - n$ in ℕ (the truncated subtraction is harmless since $n \le n^3$ ) and $2\,b(u,v) \le n + 1$ for the per-pair count.

Case (b) of the paper's definition of augmenting paths is misprinted (its hypothesis repeats that of Case (c)); the formalization uses the reading $(u_i,u_{i+1}) \notin A$ , $(u_{i+1},u_i) \in A$ , which the paper's own description of $N^f$ on p. 251 confirms.

A trivializing formalization is ruled out: a run predicate that no sequence satisfies (for instance, one that requires paths through the return arc, or computes $\varepsilon = 0$ ) would make the bound vacuous; the step predicate here is satisfiable, and a concrete four-node run has been checked. Replacing the paper's augmentation rule by "increase the forward arc by $\varepsilon$ " would also change the theorem, because that rule can violate capacities.

A complete development needs basic facts on simple paths in finite digraphs, shortest paths and their subpaths, and a max-flow min-cut theorem in the paper's model. These are reusable well beyond this mission, as are the network, residual-network and augmentation definitions. Contributions proving any milestone independently are welcome.

Selected references

J. Edmonds, R. M. Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, Journal of the ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699
L. R. Ford, D. R. Fulkerson, Maximal Flow Through a Network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5
L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962. https://doi.org/10.1515/9781400875184
E. A. Dinic, Algorithm for Solution of a Problem of Maximum Flow in a Network with Power Estimation, Soviet Mathematics Doklady 11:1277–1280, 1970. https://www.cs.bgu.ac.il/~dinitz/D70.pdf
D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 7 (network flow problems; formalized on the platform in missions IX–X).

24 thms2 active usersReviewed

Completed

Convex Optimization Functional Analysis Operations Research+1·Captain: mikedeng1

A Three-Operator Splitting Scheme and its Optimization Applications 1: Weak and Strong Convergence of the Three-Operator Splitting IterationResearch Paper

Motivation

Many problems in convex optimization, variational inequalities and signal processing reduce to a monotone inclusion: find a point $x$ at which the sum of several monotone operators contains $0$ . When the sum has two terms, the classical operator-splitting methods (Douglas–Rachford, forward–backward, forward–backward–forward) solve it by iterating a fixed-point map that uses each operator separately, through its resolvent or through a forward (explicit) step. Problems with three terms, for instance a smooth loss plus two nonsmooth regularizers or constraints, are common in practice, and before 2015 no fixed-point map was known that handled three operators one at a time without a product-space reformulation.

Davis and Yin (Set-Valued Var. Anal. 25 (2017) 829–858; preprint arXiv:1504.01032) introduced such a map, now called Davis–Yin three-operator splitting. It contains Douglas–Rachford splitting ( $C = 0$ ) and forward–backward splitting ( $B = 0$ ) as special cases, and it has become a standard building block of first-order methods for composite optimization. This mission formalizes Section 2 of the paper: the fixed-point encoding, the averagedness of the map, and the weak and strong convergence of the resulting iteration.

Setting

Let $H$ be a real Hilbert space. A set-valued operator $A : H \to 2^H$ is monotone if $\langle x - y, u - v\rangle \ge 0$ for all $u \in Ax$ , $v \in Ay$ , and maximal monotone if its graph is not properly contained in the graph of another monotone operator. Its domain is $\operatorname{dom}(A) = \{x : Ax \ne \emptyset\}$ and the zero set of an operator $M$ is $\operatorname{zer}(M) = \{x : 0 \in Mx\}$ . A single-valued $C : H \to H$ is $\beta$ -cocoercive ( $\beta > 0$ ) if $\beta\|Cx - Cy\|^2 \le \langle Cx - Cy, x - y\rangle$ for all $x, y$ .

Problem (1.1) is: given maximal monotone $A, B$ and $\beta$ -cocoercive $C$ , find

x \in H \quad\text{with}\quad 0 \in Ax + Bx + Cx .

For $\gamma > 0$ the resolvent $J_{\gamma A} = (I + \gamma A)^{-1}$ is the map with $x \in J_{\gamma A}x + \gamma A(J_{\gamma A}x)$ . The Davis–Yin operator (Eq. (1.2)) is

T := J_{\gamma A} \circ (2J_{\gamma B} - I - \gamma C \circ J_{\gamma B}) + I - J_{\gamma B}.

Algorithm 1 starts from $z^0 \in H$ and, for relaxation parameters $\lambda_k > 0$ , iterates

x_B^k = J_{\gamma B}(z^k),\qquad x_A^k = J_{\gamma A}(2x_B^k - z^k - \gamma Cx_B^k),\qquad z^{k+1} = z^k + \lambda_k(x_A^k - x_B^k),

so that $z^{k+1} = (1 - \lambda_k)z^k + \lambda_k Tz^k$ . A sequence converges weakly, $u_k \rightharpoonup u$ , if $\langle u_k, y\rangle \to \langle u, y\rangle$ for every $y \in H$ .

Formalization targets

Goal: Theorem 2.1 (Main convergence theorem)

Fix $\varepsilon \in (0,1)$ , $\gamma \in (0, 2\beta\varepsilon)$ , $\alpha = 1/(2-\varepsilon)$ and $\lambda_k \in (0, 1/\alpha)$ with $\sum_k \tau_k = \infty$ , where $\tau_k = \lambda_k(1-\lambda_k) + \lambda_k(1-\alpha)/\alpha$ , and $\inf_k \lambda_k > 0$ . If $\operatorname{Fix} T \ne \emptyset$ , there is $z^* \in \operatorname{Fix} T$ with $z^k \rightharpoonup z^*$ and

Cx_B^k \to Cx^* \ \ (\forall x^* \in \operatorname{zer}(A+B+C)),\qquad x_B^k \rightharpoonup J_{\gamma B}(z^*) \in \operatorname{zer}(A+B+C),\qquad x_A^k \rightharpoonup J_{\gamma B}(z^*),

and if $A$ or $B$ is uniformly monotone on every nonempty bounded subset of its domain, or $C$ is demiregular at every zero of $A + B + C$ , then $x_B^k$ and $x_A^k$ converge strongly to a common point of $\operatorname{zer}(A + B + C)$ .

Milestones

In the order the proof uses them: Lemma 2.1 (the identities for one application of $T$ ), Lemma 2.2 ( $\operatorname{zer}(A+B+C) = J_{\gamma B}(\operatorname{Fix} T)$ ), Lemma 2.3 (inequality (2.1)), Proposition 2.1 ( $T$ is $2\beta/(4\beta-\gamma)$ -averaged, inequality (2.2)), Remark 2.1 (the strengthened inequality (2.4)), Corollary 2.1 Parts 1–3 (Fejér monotonicity, vanishing residual, weak convergence of $z^k$ ), Corollary 2.1 Part 4 (the residual rates $\|Tz^k - z^k\|^2 \le \|z^0 - z^*\|^2/(\underline\tau(k+1))$ and $o(1/(k+1))$ ), and Eqs. (2.6)–(2.7) (the per-step descent inequality and its summed form).

Significance

Theorem 2.1 is the basic convergence guarantee for three-operator splitting: it certifies that the computable sequences $x_B^k$ , $x_A^k$ , not only the auxiliary sequence $z^k$ , approach a solution of (1.1). In infinite dimensions this is the delicate part: for Douglas–Rachford splitting ( $C = 0$ ) weak convergence of the shadow sequence $J_{\gamma B}(z^k)$ was only established by Svaiter in 2011. The result underlies the convergence of the many algorithms obtained from it by specialization (Douglas–Rachford, forward–backward, and the three-block methods of Section 4 of the paper), and the averagedness coefficient of Proposition 2.1 reduces, for $B = 0$ , to the best known one for forward–backward splitting.

All statements of this mission are proved in the paper, partly by appeal to Bauschke and Combettes' monograph (Krasnosel'skiĭ–Mann convergence, the demiclosedness of maximal monotone graphs). None of them has a machine-checked proof: Mathlib has no maximal monotone operators, resolvents, averaged maps or Krasnosel'skiĭ–Mann theorem. The mission therefore produces both a formal proof of the Davis–Yin theorem and a first body of monotone-operator theory in Lean.

Difficulty

The fixed-point part is standard once $T$ is known to be averaged: Krasnosel'skiĭ–Mann theory and Opial's argument give $z^k \rightharpoonup z^*$ . The obstacle is transferring this to $x_B^k = J_{\gamma B}(z^k)$ . Resolvents are nonexpansive but not weakly continuous, so $z^k \rightharpoonup z^*$ does not imply $J_{\gamma B}(z^k) \rightharpoonup J_{\gamma B}(z^*)$ ; the naive argument fails at exactly this step. Identifying the weak cluster points of $x_B^k$ requires a closedness property of sums of maximal monotone operators under mixed weak and strong convergence, fed by the strong convergence of $Cx_B^k$ , which in turn needs the extra term of (2.4) that (2.2) discards. Strong convergence in Part 2 needs yet another argument for each of the three alternative hypotheses.

Formalization scope

$H$ is an arbitrary real Hilbert space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace); a finite-dimensional space would identify weak and strong convergence and change the theorems.
Operators $A, B$ are H → Set H; $C$ is single-valued H → H. The resolvents are not constructed: $J_A, J_B$ are maps satisfying the resolvent inclusion $\gamma^{-1}(x - Jx) \in A(Jx)$ , which for maximal monotone operators determines them uniquely and exists by Minty's theorem.
Weak convergence is $\langle u_k, y\rangle \to \langle u, y\rangle$ for every $y$ ; strong convergence is norm convergence. Iterates are indexed from $0$ .
The printed hypothesis $\alpha = 1/(2-\varepsilon) < 2\beta/(4\beta-\gamma)$ of Corollary 2.1 and Theorem 2.1 contradicts $\gamma < 2\beta\varepsilon$ (it is a typo for $>$ ) and is not assumed. The printed $\tau_k = (1-\lambda_k/\alpha)\lambda_k/\alpha$ is replaced by the $\tau_k$ of the proof (p. 836), a weaker hypothesis.
Uniform monotonicity uses a nondecreasing $\varphi : [0,\infty) \to [0,+\infty]$ with $\varphi(0) = 0$ that vanishes only at $0$ , as the proof requires; with $\varphi \equiv 0$ allowed, Part 2(a) would be false.
The O-constant of Corollary 2.1 Part 4 is explicit, $\|z^0 - z^*\|^2/\underline\tau$ , and the little- $o$ is stated as $(k+1)\|Tz^k - z^k\|^2 \to 0$ . Eq. (2.7) is stated with a uniform lower bound $\underline\lambda \le \lambda_i$ in place of the printed $\lambda_k$ , with summability part of the conclusion.
A formalization with $T$ an arbitrary averaged map, with resolvents replaced by arbitrary nonexpansive maps, or with the contradictory comparison of $\alpha$ kept as a hypothesis would make the theorem vacuous or different; all three are ruled out.

A complete development needs the basic theory of monotone operators (monotonicity of resolvents' graphs, firm nonexpansiveness of resolvents, weak-to-strong closedness of maximal monotone graphs), Krasnosel'skiĭ–Mann iteration with Opial's lemma, and weak sequential compactness of bounded sets in Hilbert space. All of this is reusable far beyond this mission, and contributions of any of these pieces as separate theorems are welcome.

Selected references

D. Davis and W. Yin, A Three-Operator Splitting Scheme and its Optimization Applications, Set-Valued and Variational Analysis 25 (2017) 829–858. https://doi.org/10.1007/s11228-017-0421-z
H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011. https://doi.org/10.1007/978-1-4419-9467-7
B. F. Svaiter, On weak convergence of the Douglas–Rachford method, SIAM J. Control Optim. 49 (2011) 280–287. https://doi.org/10.1137/100788100
D. Davis and W. Yin, Convergence rate analysis of several splitting schemes, in: Splitting Methods in Communication, Imaging, Science, and Engineering, Springer, 2016. https://arxiv.org/abs/1406.4834

14 thms2 active usersReviewed

Completed

Algorithmic Game Theory Convex Optimization Operations Research+1·Captain: mikedeng1

On Minimizing a Convex Function Subject to Linear Inequalities II: Optimality Conditions for the Sum of the Largest Linear FormsResearch Paper

Motivation

In 1955 E. M. L. Beale showed how Dantzig's simplex method, which was built for linear objectives, can be carried over to certain nonlinear convex objectives that are minimized subject to linear inequalities (Beale 1955). Section 4 of that paper treats one such objective: the sum of the $t$ largest of a set of $g$ linear forms. Beale's motivation comes from the theory of games: "if the enemy has to choose $t$ out of a set of $g$ possible actions, and $L_f$ represents his average gain through using the $f$ th", then the defender wants to minimize the sum of the $t$ largest $L_f$ .

The same objective can be written as a linear program. One introduces a bound $u$ and requires every sum of $t$ forms to be at most $u$ . That formulation has $\binom{g}{t}$ constraints, which is unwieldy once $t>1$ and $g$ is large. Beale's alternative works with the nonlinear objective directly, and he needs a test that tells him when the current basic solution is already optimal. This mission formalizes that test, Theorem 1 of the paper.

The objective reappears in later work under other names: the sum of the $k$ largest components of a vector, the "top- $k$ sum", and $k$ times the conditional value-at-risk of an empirical distribution. Beale's paper is an early source for its optimality conditions.

Setting

There are real variables $z_l$ , indexed by $l$ in a finite set (possibly empty), and $u_1,\dots,u_s$ . Two linear forms in these variables are given,

A=A_0+\sum_l A_l z_l+\sum_{f=1}^{s}\varphi_f u_f,\qquad L_0=c_{00}+\sum_l c_{0l} z_l+\sum_{f=1}^{s}\theta_f u_f,

together with $s$ further forms

L_f=L_0-u_f\qquad(f=1,\dots,s).

For an integer $\tau\ge0$ the objective is

C=A+\bigl(\text{sum of the }\tau\text{ largest of }L_0,L_1,\dots,L_s\bigr).

The sum of the $\tau$ largest of $s+1$ numbers is the largest total of any $\tau$ of them. Ties do not make it ambiguous.

The feasible region is fixed by a set $F$ of indices. The variables $z_l$ with $l\in F$ and all the $u_f$ are free, and every other $z_l$ is restricted to $z_l\ge0$ . At the origin $z=0$ , $u=0$ all $s+1$ forms are equal to $c_{00}$ , so the origin is where $C$ fails to be differentiable. In Beale's algorithm the origin is the current basic solution: the $u_f$ measure how far the "borderline" forms sit from a chosen critical form, and $A$ collects the forms that are certainly among the largest.

Write $a_l=A_l+\tau c_{0l}$ and $w_f=\varphi_f+\tau\theta_f$ .

Formalization targets

Goal: Theorem 1 (a), p. 179

For $\tau\le s$ , $C$ is minimized over the feasible region when all the $z_l$ and $u_f$ vanish if and only if

\begin{aligned} &a_l\ge0\ \text{for all } l, \qquad a_l=0\ \text{for all } l\in F,\\ &0\le w_f\le1\ \text{for all } f,\qquad \tau-1\le\sum_{f=1}^{s}w_f\le\tau . \end{aligned}\tag{4.5}

"Minimized" means a global minimum: $C(0,0)\le C(z,u)$ at every feasible point.

Milestones

Convexity (p. 179). $C$ is a convex function of $(z,u)$ for $\tau\le s+1$ .
Descent rules (second half of Theorem 1 (a), p. 179). When a condition of (4.5) fails, a stated move of one variable, or of all $u_f$ together, lowers $C$ below $C(0,0)$ for every small enough step. There are six moves: $z_l\uparrow$ if $a_l<0$ ; $z_l\downarrow$ if $a_l>0$ and $l\in F$ ; $u_f\uparrow$ if $w_f<0$ ; $u_f\downarrow$ if $w_f>1$ ; all $u_f\uparrow$ if $\sum w_f<\tau-1$ ; all $u_f\downarrow$ if $\sum w_f>\tau$ .
The rearrangement identity (proof of Theorem 1 (a), p. 180). If $1\le\tau\le s$ , $u'_1\le\dots\le u'_s$ and $u'_\tau\le0$ , then

C=A_0+\tau c_{00}+\sum_l a_l z'_l+\sum_{f=1}^{\tau}(w_f-1)(u'_f-u'_\tau)+\sum_{f=\tau+1}^{s}w_f(u'_f-u'_\tau)+\Bigl\{\sum_{f=1}^{s}w_f-\tau\Bigr\}u'_\tau .

Theorem 1 (b) (p. 180). For $\tau=s+1$ , the origin is a minimum if and only if (4.5) holds and $w_f=1$ for every $f$ . Otherwise some value of $u_f$ with the sign opposite to $w_f-1$ lowers $C$ .

Significance

Theorem 1 is the optimality test of Beale's simplex method for the sum-of-largest objective. The algorithm on pp. 178–179 changes nonbasic variables one at a time. When no single change is profitable it applies Theorem 1: either (4.5) holds and the current solution is optimal, or one of the six descent rules names the variable to change next. The test is exact even though the objective is not differentiable at the current point. It is a closed-form description of the subdifferential of a top- $\tau$ sum at a point where all the forms tie. The theorem is also the base case of the multi-group generalization that Beale mentions on p. 181.

The paper proves Theorem 1 by hand. To our knowledge neither the theorem nor the rearrangement identity behind it has been formalized in any proof assistant. The mission produces:

a checked statement and proof of the test, including the degenerate cases $\tau=0$ and $s=0$ , which the paper does not discuss separately;
the boundary case $\tau=s+1$ ;
a reusable Lean definition of the sum of the $\tau$ largest entries of a finite real family, with its convexity.

Difficulty

Necessity, the "only if" direction, is the part the paper calls obvious: each descent rule changes $C$ linearly for small steps. Two features still have to be handled explicitly. The step must be small only in rule-dependent ways, and the ordering of the forms changes along the moves of rules 4 and 6.

Sufficiency is where the work lies. The naive argument, "the directional derivative in every coordinate direction is non-negative, so the origin is a minimum", fails because $C$ is not differentiable at the origin. Nonnegative derivatives along the coordinate axes do not control mixed directions in which several $u_f$ move by different amounts, which reorders the forms. Which $\tau$ forms are the largest then depends on the point, and the paper settles the configurations in which $L_0$ is among the $\tau$ largest by an informal appeal to the "essential symmetry" between $L_0$ and the other forms. A formal proof cannot leave that appeal informal: the forms are parametrised relative to $L_0$ (each $L_f$ is $L_0-u_f$ ), so the symmetry is a change of variables that has to be written down and shown to preserve (4.5).

Formalization scope

Data. The variables are z : Fin r → ℝ (any r, including $0$ ) and u : Fin s → ℝ. The paper's $u_f$ for $f=1,\dots,s$ is Lean's u f for $f=0,\dots,s-1$ . The coefficients $(A_0,A_l,\varphi_f,c_{00},c_{0l},\theta_f)$ form a structure Forms r s.
Forms. The family $L_0,\dots,L_s$ is Fin (s+1) → ℝ, with index $0$ for $L_0$ and index f.succ for $L_0-u_f$ . The free set $F$ is a Finset (Fin r), and $\tau$ is a natural number cast to $\mathbb R$ wherever it multiplies a coefficient.
Sum of the largest. sumLargest τ v is the maximum over $\tau$ -element subsets $S$ of $\sum_{i\in S}v_i$ (Finset.sup' over powersetCard). It is the junk $0$ for $\tau$ larger than the number of entries, a case no statement uses.
Minimality. "Minimized when all variables vanish" is the global statement $C(0,0)\le C(z,u)$ for all $(z,u)$ with $z_l\ge0$ for $l\notin F$ . It is not a local minimum, and the sign constraints on restricted $z_l$ are kept: they are why the first condition of (4.5) is an inequality.
Descent. " $C$ can be decreased by moving $x$ from zero" is a strict decrease for all step sizes in some interval $(0,\varepsilon)$ , with every other variable at zero.
No trivialization. The goal is an equivalence with no hypothesis beyond $\tau\le s$ . Neither direction can be satisfied vacuously, and the cases $\tau=0$ and $s=0$ are included, as on the page.
Added hypotheses. The rearrangement milestone assumes $\tau\ge1$ , because the paper's $u'_\tau$ does not exist at $\tau=0$ . Its second line uses $c_{0l}$ where the page misprints $c_l$ .

Needed infrastructure:

basic lemmas on sumLargest: its value at a constant family, at a family sorted by a monotone shift, and under adding a common constant;
the change of variables behind the paper's symmetry between $L_0$ and the other forms.

These lemmas are reusable for any top- $k$ -sum or empirical-CVaR objective. Contributions are welcome at any level: lemmas about sumLargest, any of the milestones, or an alternative sufficiency proof through convexity and one-sided directional derivatives.

Not in scope: the pivoting rules (4.2)–(4.4), the degeneracy discussion on pp. 180–181, and the multi-group generalization, which the paper says is "cumbersome to state" and does not state.

Selected references

E. M. L. Beale, On Minimizing a Convex Function Subject to Linear Inequalities, Journal of the Royal Statistical Society, Series B 17(2), 173–184, 1955. https://doi.org/10.1111/j.2517-6161.1955.tb00191.x
G. B. Dantzig, A. Orden and P. Wolfe, The generalized simplex method for minimizing a linear form under linear inequality restraints, Pacific Journal of Mathematics 5(2), 183–195, 1955. https://doi.org/10.2140/pjm.1955.5.183
R. T. Rockafellar and S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2(3), 21–41, 2000. https://doi.org/10.21314/JOR.2000.038

7 thms2 active usersReviewed

Completed

Operations Research Partial Differential Equations Probability+1·Captain: mikedeng1

Revenue Management of a Make-to-Stock Queue: Exponential Stationary Density under Normal Reflection (Proposition 2)Research Paper

Motivation

A make-to-stock manufacturer who also sells on a spot market must decide, at every moment, whether to keep producing and whether to accept or reject incoming orders at the prevailing price. Caldentey and Wein (Revenue Management of a Make-to-Stock Queue, Operations Research 54(5), 2006) study this problem in heavy traffic. The limit is a two-dimensional singular control problem for a diffusion: the inventory level and the logarithm of the price move jointly as a correlated Brownian motion, and the controls push the inventory only when it reaches one of two free boundaries. The optimal boundaries are characterized by an elliptic free-boundary problem that the authors could not solve in closed form.

The paper's way forward is an approximation: change the direction of reflection on the boundary so that the stationary distribution of the controlled process becomes an explicit exponential. Proposition 2 states that exponential form, and it turns the free-boundary problem into a calculus-of-variations problem for the two boundary curves. Explicit stationary densities of reflected diffusions in two dimensions are rare; the classical condition for an exponential stationary density of a reflected Brownian motion, and the characterization of the stationary law by a basic adjoint relation, are due to Harrison and Williams, Multidimensional reflected Brownian motions having exponential stationary distributions, Annals of Probability 15, 1987, the reference the paper cites. This mission formalizes the analytic core of Proposition 2: the exponential density satisfies that relation for the reflection field the proposition singles out.

Setting

Points of the plane are $(x,y)$ , with $x$ the inventory level and $y$ the logarithm of the price. The limiting process $(\mathcal X,\mathcal Y)$ has drift $(\theta,0)$ and covariance matrix

\Sigma=\begin{pmatrix}\sigma^2&\sigma\delta\varrho\\ \sigma\delta\varrho&\delta^2\end{pmatrix},\qquad \sigma>0,\ \delta>0,\ -1<\varrho<1,

so its generator is

\Gamma=\theta\frac{\partial}{\partial x}+\frac{\sigma^2}{2}\frac{\partial^2}{\partial x^2}+\sigma\delta\varrho\frac{\partial^2}{\partial x\,\partial y}+\frac{\delta^2}{2}\frac{\partial^2}{\partial y^2}.

Two curves bound the region where the process lives: the rejection boundary $x=\eta(y)$ (below it, orders are rejected) and the idleness boundary $x=\xi(y)$ (above it, production stops). For $y_{\min}<y_{\max}$ the region is

\Omega=\{(x,y):\ y_{\min}<y<y_{\max},\ \eta(y)<x<\xi(y)\},

and its boundary splits into four pieces: $x=\eta(y)$ , $x=\xi(y)$ , $y=y_{\min}$ , $y=y_{\max}$ . Write $\vec n$ for the inward unit normal on $\partial\Omega$ and $dl$ for arc length. A reflection field $\vec v$ on $\partial\Omega$ gives the direction in which the process is pushed back into $\Omega$ . The basic adjoint relation (BAR) of the paper, equation (43), is

\int_\Omega \Gamma f\,\pi_\Omega\,ds+\frac12\int_{\partial\Omega}\vec v\cdot\nabla f\,\pi_\Omega\,dl=0\quad\text{for all test functions } f,

and the paper cites Harrison and Williams for the fact that the stationary distribution $\pi_\Omega$ of the reflected process satisfies it. Proposition 2 introduces the eigen-decomposition $\Sigma=V'EV$ ( $V$ a rotation whose rows are eigenvectors, $E$ diagonal), the whitening map $T=E^{-1/2}V$ and $\Omega^*=T(\Omega)$ , and assumes that $T\vec v$ is normal to $\partial\Omega^*$ . The exponents are

m_x=\frac{2\theta}{\sigma^2(1-\varrho^2)},\qquad m_y=\frac{-2\varrho\theta}{\sigma\delta(1-\varrho^2)}.\tag{47}

Formalization targets

Goal: the exponential density satisfies the BAR under conormal reflection

For $\eta,\xi$ continuously differentiable with $\eta<\xi$ on $[y_{\min},y_{\max}]$ , $\pi(x,y)=e^{m_xx+m_yy}$ , and every $C^2$ function $f$ on $\mathbb R^2$ ,

\int_\Omega \Gamma f\;\pi\,ds+\frac12\int_{\partial\Omega}(\Sigma\vec n)\cdot\nabla f\;\pi\,dl=0 .

The boundary integral is written out on the four pieces, with $\vec n\,dl$ equal to $(1,-\eta'(y))\,dy$ , $(-1,\xi'(y))\,dy$ , $(0,1)\,dx$ and $(0,-1)\,dx$ respectively. The normalizing constant is left out because the relation is linear in $\pi$ .

Milestones

The interior equation: $\Gamma^*\pi=-\theta\pi_x+\frac{\sigma^2}{2}\pi_{xx}+\sigma\delta\varrho\,\pi_{xy}+\frac{\delta^2}{2}\pi_{yy}=0$ everywhere.
The zero-flux identity: $\frac12\Sigma\nabla\pi=(\theta,0)\,\pi$ everywhere.
The meaning of the hypothesis: with $T=E^{-1/2}V$ , $(Tv)\cdot(Tw)=v\cdot\Sigma^{-1}w$ , and for $n\neq0$ , $Tv$ is orthogonal to $T$ of every vector orthogonal to $n$ exactly when $v$ is a multiple of $\Sigma n$ .
The normalizing constant: $\pi$ is integrable on $\Omega$ and a unique $K_\Omega>0$ makes $K_\Omega\pi$ integrate to one.

Significance

For the operations model, Proposition 2 is what makes the problem computable. Once the stationary density is explicit, the long-run average cost of any pair of boundary curves is an explicit integral, and optimizing over $(\eta,\xi)$ becomes a variational problem with Euler–Lagrange equations; the paper's proposed policy and its numerical comparisons all rest on it.

For formalization, the mission produces a machine-checked version of a statement whose proof the paper does not contain (it is in an online companion) and whose hypothesis is stated only in words. The formal statements fix exactly which reflection field makes the claim true, which the prose leaves ambiguous. None of the statements has, to our knowledge, a machine-checked proof anywhere; the result itself is classical in spirit (an integration by parts on a planar region), but no divergence theorem on a region between two graphs with an anisotropic operator is currently available as a ready-made statement.

Difficulty

The interior equation and the zero-flux identity are finite computations with the exponential. The difficulty is the goal: it is an integration-by-parts identity on a curved planar region with an anisotropic second-order operator. The obvious first step, "apply Green's identity", presupposes a divergence theorem on a region bounded by two graphs $x=\eta(y)$ , $x=\xi(y)$ and two horizontal segments, with the boundary integral written in the parametrization of each piece and the orientation of every normal tracked. Mathlib has the divergence theorem on rectangular boxes, not on such regions, and the moving limits $\eta(y)$ , $\xi(y)$ are exactly where the terms in $\eta'$ and $\xi'$ of the boundary integral come from.

The second trap is the reflection field. The page describes the modification as substituting the inward unit normal $\vec n$ for $\vec v$ ; with $\vec v=\vec n$ the identity is false as soon as $\Sigma$ is not a multiple of the identity (on a random instance the residual is of order one). Only the conormal field $\Sigma\vec n$ , which is what the hypothesis of Proposition 2 selects, gives a true statement.

Formalization scope

Everything lives in the namespace MakeToStockRM.ExpDensity. The plane is ℝ × ℝ with the inventory first; partial derivatives are Fréchet derivatives applied to (1, 0) and (0, 1), and the mixed partial is $\partial_x(\partial_y f)$ . Parameters satisfy $\sigma>0$ , $\delta>0$ , $|\varrho|<1$ ; $\theta$ is any real number, and $\theta=0$ (then $\pi\equiv1$ ) is allowed.

This is the analytic, pinned-down content of Proposition 2. The identification "the BAR characterizes the stationary law of the reflected diffusion" (Harrison–Williams 1987) is out of scope: Mathlib has no reflected Brownian motion. Relative to the page, the formalization commits to the following:

The reflection field is $\vec v=\Sigma\vec n$ with $\vec n$ the inward unit normal and $dl$ arc length. The hypothesis " $T\vec v$ is normal to $\partial\Omega^*$ " fixes only the direction of $\vec v$ (milestone 3); the length $\Sigma\vec n$ is the one for which the BAR holds. The page's phrase "substituting the inward unit normal $\vec n$ for $\vec v$ " is inconsistent with the proposition's own hypothesis and is not followed.
The boundary curves are $C^1$ on $\mathbb R$ with $\eta<\xi$ on $[y_{\min},y_{\max}]$ , and $y_{\min}<y_{\max}$ , so $\Omega$ is a nonempty bounded region; the paper assumes this implicitly.
Test functions are all $C^2$ functions on $\mathbb R^2$ , which are bounded with bounded derivatives on the closure of $\Omega$ (the paper's "twice continuous and bounded").
The constant $K_\Omega$ is dropped from the goal and treated in milestone 4.

The goal quantifies over every $C^2$ test function; restricting to functions supported inside $\Omega$ would delete the boundary term and reduce the goal to milestone 1, and that trivialization is ruled out. The second half of Proposition 2 ("(45)–(46) is equivalent to (48)–(49)"), Proposition 1, the heavy-traffic limit, the HJB equation and the proposed policy are not formalized: their normalizations or proofs are only in the online companion.

A complete development needs a divergence theorem on regions between two $C^1$ graphs, which is reusable for any planar PDE statement on such regions. Contributions of that lemma, and of the four milestones, are welcome.

Selected references

R. Caldentey, L. M. Wein, Revenue Management of a Make-to-Stock Queue, Operations Research 54(5):859–875, 2006. https://doi.org/10.1287/opre.1060.0289
J. M. Harrison, R. J. Williams, Multidimensional reflected Brownian motions having exponential stationary distributions, Annals of Probability 15(1):115–137, 1987. https://doi.org/10.1214/aop/1176992259
F. John, Partial Differential Equations, 4th ed., Springer, 1982. https://doi.org/10.1007/978-1-4684-9333-7

10 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Exit Problems for Spectrally Negative Lévy Processes and Applications to (Canadized) Russian Options I: Joint Laplace Transform of the Exit Time and Exit Position of the Reflected ProcessResearch Paper

Motivation

A spectrally negative Lévy process is a process with stationary independent increments whose jumps are all downward: Brownian motion with drift plus a compound Poisson or infinite-activity stream of negative jumps. It is the standard model for a risk reserve that earns premiums continuously and pays claims in lumps, for a storage level or a queue workload seen in reverse, and, in mathematical finance, for a log-price that can crash but not jump up. Exit problems (when and where such a process first leaves an interval) are the basic quantities in ruin theory, in dividend and barrier problems, and in the pricing of path-dependent options.

The reflected process $Y=\overline X-X$ , the distance of $X$ below its running maximum, is the drawdown of $X$ . Its first passage above a level $k$ is the time at which a drawdown of size $k$ first occurs. Avram, Kyprianou and Pistorius (AKP 2004) computed the joint Laplace transform of this passage time and of the overshoot $Y_{\tau_k}$ in closed form, in terms of the scale functions of $X$ . This is the first of three missions on that paper. The two others use this identity for the perpetual Russian option and its Canadized version.

Timeline. Bertoin gave the upward two-sided exit identity for spectrally negative Lévy processes in terms of scale functions (Bertoin 1996, Theorem VII.8) and the downward one (Bertoin 1997, Corollary 1). Avram, Kyprianou and Pistorius (2004) obtained the joint transform of $(\tau_k,Y_{\tau_k})$ for every spectrally negative Lévy process of unbounded variation, or of bounded variation with absolutely continuous Lévy measure.

Setting

Let $X=\{X_t,t\ge0\}$ be a spectrally negative Lévy process on $(\Omega,\mathcal F,\mathbb P)$ : it starts at $0$ , has independent and stationary increments, càdlàg paths, no positive jumps, and paths that are not monotone. Its Laplace exponent is $\psi(\theta)=\log\mathbb E[e^{\theta X_1}]$ , and " $\psi(v)<\infty$ " means that $e^{vX_1}$ is integrable. For such $v$ , the tilted exponent is $\psi_v(\theta)=\psi(\theta+v)-\psi(v)$ .

The paper assumes throughout that $X$ has unbounded variation, or has bounded variation and a Lévy measure $\Lambda$ with $\Lambda(dx)\ll dx$ .

For $q\ge0$ , $\Phi(q)$ is the largest root of $\psi(\theta)=q$ . The $q$ -scale function $W^{(q)}:\mathbb R\to[0,\infty)$ is the unique function that vanishes on $(-\infty,0]$ , is continuous on $(0,\infty)$ , and satisfies

\int_0^\infty e^{-\theta x}W^{(q)}(x)\,dx=\frac1{\psi(\theta)-q},\qquad\theta>\Phi(q).

For $q<0$ it is defined by the series $W^{(q)}=\sum_{k\ge0}q^kW^{\star(k+1)}$ , where $W=W^{(0)}$ and $\star$ is convolution on $[0,\infty)$ . Further, $Z^{(q)}(x)=1+q\int_{-\infty}^xW^{(q)}(z)\,dz$ . The functions $W_v^{(p)}$ and $Z_v^{(p)}$ are the same objects built from $\psi_v$ instead of $\psi$ .

Under $\mathbb P_{s,x}$ the process starts at $x$ with a prior maximum $s\ge x$ . Its running maximum is $\overline X_t=\max\{s,\sup_{0\le u\le t}X_u\}$ , and the reflected process is $Y=\overline X-X$ , which starts at $z=s-x$ . For $k>0$ ,

\tau_k=\inf\{t\ge0:Y_t\notin[0,k)\}.

Formalization targets

Goal: Theorem 1

For $u\ge0$ and $v$ with $\psi(v)<\infty$ , with $z=s-x\ge0$ and $p=u-\psi(v)$ ,

\mathbb E_{s,x}\big[e^{-u\tau_k-vY_{\tau_k}}\big]=e^{-vz}\left(Z_v^{(p)}(k-z)-W_v^{(p)}(k-z)\frac{pW_v^{(p)}(k)+vZ_v^{(p)}(k)}{W_v^{(p)\prime}(k)+vW_v^{(p)}(k)}\right).

Here $v$ may be negative, so $p$ may be negative, which is where the series extension of $W$ enters.

Milestones

(2) $\mathbb E[e^{\theta X_t}]=e^{t\psi(\theta)}$ .
Remark 4: $W^{(u)}(x)=e^{vx}W_v^{(u-\psi(v))}(x)$ for every real $u$ .
Proposition 1, (9) and (10): for $x\in(a,b)$ , the Laplace transforms of the exit time of $X$ from $(a,b)$ on the events of exit above and exit below.
(13): the splitting of the goal's expectation at the first zero of $Y$ .
(14)–(15) and (16): the two expectations of (13).
(22): the value $C$ of the functional for $Y$ started at $0$ .
Remark 6, (23): the stopped process whose martingale property is equivalent to Theorem 1.

Items (13)–(22) are stated under the proof's restriction $u\ge\psi(v)\vee0$ . The goal is not.

Significance

The identity gives, for every spectrally negative Lévy process, the law of the first drawdown of size $k$ and of its overshoot. With $v=0$ it is the Laplace transform of the drawdown time. With $u=0$ it is the transform of the overshoot. The paper uses it, through its Corollary 1, to solve the perpetual Russian option and the Canadized Russian option in closed form. Identities of this form, written in scale functions, are the standard tool for drawdown and reflected-process problems for spectrally negative Lévy processes.

The theorem is proved. As far as the platform and Mathlib show, none of it is formalized: Mathlib has independent increments and cumulant generating functions but no Lévy process, no scale function and no excursion theory. This mission produces a formal statement of the paper's model and of the exit identities. A complete development would also give Mathlib its first fluctuation-theory results for Lévy processes.

Difficulty

The natural first idea is to treat $Y$ like $X$ and read off its exit from $[0,k)$ from the two-sided exit identities of Proposition 1. This works only until $Y$ first returns to $0$ . Up to that time $Y$ is a copy of $-X$ . After it, $Y$ is reflected at $0$ , it is not a Lévy process, and no two-sided exit problem of $X$ describes it. The whole content of the theorem is the constant $C$ of (13), the value of the functional for $Y$ started at $0$ , where the reflection acts at every instant. A second difficulty is the range of $(u,v)$ . For $v<0$ the integrand $e^{-vY_{\tau_k}}$ is unbounded, because $Y$ can jump far above $k$ . Its finiteness is part of the claim. So is the passage from the region $u\ge\psi(v)\vee0$ , where every scale function in (12) comes from Definition 2, to all $u\ge0$ , where $p$ can be negative.

Formalization scope

Time is $[0,\infty)$ (ℝ≥0). $X$ is a real process with $X_0=0$ . $\mathbb P_x$ is encoded by the path $x+X$ , and $\mathbb P_{s,x}$ by that path together with the prior maximum $s$ . Random times take values in WithTop ℝ≥0, with $\infty$ as "never". The functional $e^{-u\tau_k-vY_{\tau_k}}$ and discount factors $e^{-qT}$ are set to $0$ where the time is infinite. Every stated expectation carries its integrability as part of the conclusion.

Readings of the paper's informal words:

"Lévy process": the paths start at $0$ , are càdlàg and have no positive jumps for every $\omega$ , not only almost surely.
"We exclude the case that X has monotone paths": the paths are neither almost surely nondecreasing nor almost surely nonincreasing.
"unbounded variation": not of bounded variation. The standing assumption is "bounded variation implies (AC)".
" $\Lambda(dx)\ll dx$ ": for every Lebesgue-null Borel $A$ , almost surely no nonzero jump in $(0,1]$ lands in $A$ . The Lévy measure is not constructed.
" $\psi(v)<\infty$ ": $e^{vX_1}$ is integrable.
"the largest root": the supremum of the nonnegative roots.
"the unique function": a definite description by choice.
"analytic extension": the series (5) for real negative index. Complex indices are out of scope.
" $W'$ ": the derivative at $k>0$ .
"is a martingale" in (23): a martingale for the natural filtration of $X$ .
Misprint: (23) prints $vZ_v^{(q)}(k)$ , and the statement uses $vZ_v^{(p)}(k)$ .

The scale functions are defined from the exponent $\psi$ of the given $X$ . A formalization in which $W$ is an arbitrary function satisfying a Laplace-transform hypothesis is ruled out. So is one in which $W_v^{(p)}$ is defined as $e^{-vx}W^{(p+\psi(v))}(x)$ , which would make Remark 4 a tautology.

Infrastructure a complete development needs: Lévy processes and their Laplace exponent, the strong Markov property at stopping times, existence and regularity of scale functions (via Laplace inversion), and the Esscher change of measure. No statement of the mission mentions excursion theory. Contributions of reusable infrastructure for Lévy processes are welcome.

Selected references

F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14(1), 215–238, 2004. https://doi.org/10.1214/aoap/1075828052
J. Bertoin, Lévy Processes, Cambridge University Press, 1996. https://www.cambridge.org/core/books/levy-processes/
J. Bertoin, Exponential decay and ergodicity of completely asymmetric Lévy processes in a finite interval, Ann. Appl. Probab. 7(1), 156–169, 1997. https://doi.org/10.1214/aoap/1034625254

16 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers 3: Optimal Contingent-Pricing Revenue with Myopic Customers and Exponential ValuationsResearch Paper

Motivation

Retailers of seasonal goods (fashion, electronics, holiday items) sell a fixed stock over a short season and routinely cut prices toward its end. A markdown of this kind segments the market over time: customers with high valuations buy early at a premium price, and customers with lower valuations are served later at a discount price. Aviv and Pazgal (MSOM 2008) study how much such two-price schemes are worth when customers arrive over time, differ in their valuations, and may or may not anticipate the discount.

To measure the value of price segmentation, the paper compares every two-price scheme with the best fixed-price policy, a single price held for the whole season. Its benchmark is the case of myopic customers, who never delay a purchase strategically. Proposition 3 of the paper computes this benchmark in closed form in the simplest nontrivial setting: exponentially distributed valuations that do not decline over the season, and unlimited inventory. The resulting formula explains the pattern of the paper's Table 1, where the benefit of segmentation grows with the heterogeneity of valuations and with a late discount time.

Setting

A seller offers a product during the season $[0, H]$ ; throughout this mission $H = 1$ , so time is measured as a fraction of the season. Customers arrive as a Poisson process with rate $\lambda > 0$ . Customer $j$ has a base valuation $V_j$ drawn independently from a distribution $F$ with tail $\bar F(x) = 1 - F(x)$ , and values the product at $V_j e^{-\alpha t}$ at time $t$ , where $\alpha \ge 0$ is the decline factor. The paper reparametrizes it as $\rho = e^{-\alpha H}$ , the fraction of the base valuation left at the end of the season.

In the numerical study, $F$ is a Gamma law with mean $\mu$ and coefficient of variation $c$ (standard deviation over mean): shape $1/c^2$ and rate $1/(\mu c^2)$ . The paper sets $\mu = 1$ . For $c = 1$ this is the exponential law with mean one, $\bar F(x) = e^{-x}$ for $x \ge 0$ .

A contingent two-price policy posts the premium price $p_1$ on $[0, T)$ , where $0 < T \le 1$ is fixed, and a discount price $p_2 \le p_1$ from time $T$ on. A myopic customer arriving at $t < T$ buys at $p_1$ if his valuation is at least $p_1$ ; otherwise he waits and buys at $T$ if his valuation is then at least $p_2$ . Customers arriving at or after $T$ buy if their valuation is at least $p_2$ . The numbers of customers in these groups are Poisson with means

\Lambda_I(p_1) = \lambda\int_0^T \bar F(p_1 e^{\alpha t})\,dt, \quad \Lambda_W(p_1,p_2) = \lambda\int_0^T \big[\bar F(\min\{p_1e^{\alpha t}, p_2e^{\alpha T}\}) - \bar F(p_1e^{\alpha t})\big]dt, \quad \Lambda_L(p_2) = \lambda\int_T^H \bar F(p_2e^{\alpha t})\,dt .

With unlimited inventory, the expected revenue of the policy is

R_{C/N}(p_1, p_2) = p_1\Lambda_I(p_1) + p_2\big(\Lambda_W(p_1,p_2) + \Lambda_L(p_2)\big),

and the expected revenue of a single price $p$ is $R_F(p) = p\,\lambda\int_0^H \bar F(p e^{\alpha t})\,dt$ (Eq. (9) of the paper). The optimal values are $\pi^*_{C/N} = \max_{p_2 \le p_1} R_{C/N}(p_1,p_2)$ and $\pi^*_F = \max_p R_F(p)$ .

Formalization targets

Goal: Proposition 3

Suppose $c = 1$ , $\rho = 1$ and $Q/\lambda \to \infty$ (unlimited inventory), with $\mu = 1$ and $H = 1$ . Then

\pi^*_{C/N} = (\lambda e^{-1})\cdot e^{T/e} = \pi^*_F \cdot e^{T/e}.

Both maxima are attained. The goal states the two optimal values; it does not fix the optimal prices.

Milestones from the paper's proof

The reduced problem: for $0 \le p_2 \le p_1$ , $R_{C/N}(p_1,p_2) = p_2\cdot\lambda e^{-p_2} + (p_1-p_2)\cdot\lambda T e^{-p_1}$ .
Its solution: over $p_2 \le p_1$ the maximum is $\lambda e^{-1+T/e}$ , attained exactly at $p_1^* = 2 - T/e \ge 1$ , $p_2^* = p_1^* - 1 \le 1$ .
The fixed-price optimum (a supporting item of the goal, stated in the proof on pp. 358–359): $p^* = \mu = 1$ is the unique optimal single price and $\pi^*_F = \lambda e^{-1}$ .

Significance

Proposition 3 gives the relative benefit of contingent pricing over a single price, $e^{T/e} - 1$ , as a function of the discount time alone. It increases in $T$ and is largest at $T = 1$ , where it equals $e^{1/e} - 1 \approx 44.46\%$ . This is the paper's analytic anchor for its numerical findings: segmentation is most valuable when valuations are heterogeneous and customers are carried to the discount at little cost, and a late discount exposes more customers to the premium price. Under strategic customers the same quantity serves as an upper bound on the benefit of segmentation (§6.1 of the paper).

The result is proved in the paper, in a short appendix argument that states the reduced problem and its solution without the calculus. No machine-checked version exists. Formalizing it produces a reusable Lean encoding of the paper's segment rates $\Lambda_I, \Lambda_W, \Lambda_L$ as integrals of a valuation tail, a Gamma valuation law through Mathlib's gammaMeasure, and a complete verification that the integral model reduces to the two-variable problem and that the stated prices are its unique maximizer.

Difficulty

The obvious route is to write the revenue in closed form and set the gradient to zero. Two steps of that route are not automatic. First, the reduction requires evaluating the three integrals with the piecewise tail of the exponential law, including the $\min$ inside $\Lambda_W$ , and the reduced formula is valid only for nonnegative prices; negative prices must be handled separately in the model itself, where the tail equals one. Second, the reduced objective $p_2\lambda e^{-p_2} + (p_1-p_2)\lambda T e^{-p_1}$ is not concave on the region $p_2 \le p_1$ , so a stationary point is not automatically a global maximizer, and the boundary $p_2 = p_1$ and unbounded directions have to be ruled out. Uniqueness of the maximizer, which the paper asserts, fails at $T = 0$ and needs $T > 0$ .

Formalization scope

All declarations sit in the namespace SeasonalPricing.MyopicExp. Time, prices and rates are real numbers. The season is $[0, 1]$ with $0 < T \le 1$ and $\lambda > 0$ . Integrals are interval integrals. The valuation tail is gammaValuationTail μ c x = 1 - cdf (gammaMeasure (1/c^2) (1/(μ c^2))) x, used at $\mu = c = 1$ . The hypothesis $\rho = 1$ is decayRatio α 1 = 1 with $\alpha \ge 0$ .

Readings of the paper's informal words:

" $Q/\lambda \to \infty$ " is read as unlimited inventory: the truncated Poisson mean $N(q,\Lambda)$ of §4.2 is replaced by $\Lambda$ and stock-outs never occur. This is what the proof computes, what p. 348 writes as $Q = \infty$ , and what §7.1 calls inventory that is "practically unlimited". A limit of finite-inventory optimal revenues is not stated.
"max" is an attained maximum (IsGreatest), not a supremum.
The optimum is taken over all real prices with $p_2 \le p_1$ , as printed; the paper never restricts signs, and negative prices are never optimal in the model.
The seller's discount at $T$ is a best response to $p_1$ in the paper ( $R(q \mid p_1)$ , p. 349). With unlimited inventory it does not depend on the realized sales, and the nested maximum equals the joint maximum over $(p_1, p_2)$ , which is what the goal states.
"The solution … is" (milestone 2) and "the optimal single price is given by $p^* = \mu = 1$ " (the fixed-price item) are read as unique maximizers.

The Gamma density printed on p. 349 has the exponent $1/(sc^2-1)$ , a misprint for $1/c^2 - 1$ ; at $c = 1$ the exponent is $0$ either way.

A trivializing formalization would state the goal on the reduced two-variable function, dropping the model: the goal here is about $R_{C/N}$ built from $\Lambda_I, \Lambda_W, \Lambda_L$ and the Gamma tail, and about $R_F$ built from Eq. (9). The platform's BuyingToBundle.monopolyRevenue (definition monopoly_pricing) is a related object, $\sup_p p\,\nu([p,\infty))$ ; with $\rho = 1$ and $H = 1$ , $\pi^*_F$ equals $\lambda$ times it for the exponential law, but it is a supremum without arrivals or time and is not reused.

Contributions welcome: closed forms of the segment rates for the exponential tail, a general lemma that negative prices are dominated, and the two-variable maximization.

Selected references

Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
D. Besanko and W. L. Winston, Optimal Price Skimming by a Monopolist Facing Rational Consumers, Management Science 36(5):555–567, 1990. https://doi.org/10.1287/mnsc.36.5.555
G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999

6 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization+1·Captain: mikedeng1

Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers 1: Threshold Purchasing Policies under Contingent PricingResearch Paper

Motivation

Retailers of fashion and seasonal goods sell at a premium price early in the season and mark the remaining stock down later. When customers anticipate the markdown, some of them who would buy at the premium price instead wait, trading a lower price against the risk that the item sells out and against the decline of their own valuation over the season. How forward-looking ("strategic") customers respond to a markdown policy is the first question any model of such pricing has to answer, because the seller's optimal prices depend on it.

Aviv and Pazgal (MSOM 2008) model a seller with a fixed inventory, Poisson arrivals of customers with heterogeneous, exponentially declining valuations, and two pricing regimes: contingent pricing, where the discount depends on the inventory left at the markdown time, and announced fixed discounts. The first step of their analysis of contingent pricing is Theorem 1: whatever the other customers do, a customer's best response is a threshold rule on his current valuation, with a threshold that rises as the markdown approaches. Their numerical study of equilibria and of the value of price commitment (§§4.2–7) is built on this reduction.

Setting

A seller holds $Q$ units over a season $[0, H]$ split at a fixed time $T$ with $0 < T \le H$ . On $[0, T)$ the premium price $p_1$ applies. At time $T$ the seller observes the remaining inventory $Q_T \in \{0, 1, \dots, Q\}$ and charges the discount menu price $p_2(Q_T)$ , where $p_2(q) \le p_1$ for $q = 1, \dots, Q$ . Customer $j$ has a base valuation $V_j$ and valuation $V_j(t) = V_j e^{-\alpha t}$ at time $t$ , with a common decline factor $\alpha \ge 0$ .

A customer arriving at $t < T$ either buys immediately at $p_1$ or waits until $T$ , when he requests a unit if the discounted price leaves him a nonnegative surplus. Waiting is uncertain in two ways: the remaining inventory $Q_T$ is random, and when fewer units remain than customers request them, units are rationed at random. A belief is a probability mass function $\pi$ of $Q_T$ on $\{0, \dots, Q\}$ together with allocation probabilities $a(q) = \Pr\{\mathcal A \mid Q_T = q\} \in [0,1]$ , $a(0) = 0$ , where $\mathcal A$ is the event that the customer is allocated a unit. It is determined by the other customers' strategies, which are arbitrary.

With $\delta = e^{-\alpha(T-t)}$ , the expected surplus of waiting of a customer with current valuation $\psi$ is

W_t(\psi) = \mathrm E_{Q_T}\!\left[\max\{\psi\delta - p_2(Q_T), 0\}\cdot \mathbf 1\{\mathcal A \mid Q_T\}\right] = \sum_{q=0}^{Q}\pi(q)\,a(q)\,\max\{\psi\delta - p_2(q), 0\}.

The paper's purchase rule (p. 344): buy immediately iff the current surplus $V(t) - p_1$ is nonnegative and at least $W_t(V(t))$ .

Formalization targets

Goal: Theorem 1 and Corollary 1

Assume $p_1 \ge 0$ , and $\alpha > 0$ or $\sum_q \pi(q)a(q) < 1$ . For every $t \in [0,T)$ the equation

\psi - p_1 = W_t(\psi) \tag{2}

has a unique solution $\psi(t) \ge p_1$ ; a customer arriving at $t$ buys immediately under the purchase rule if and only if $V(t) \ge \psi(t)$ ; and the threshold function $\psi : [0, T) \to [p_1, \infty)$ is nondecreasing in $t$ .

Milestones

The right-hand side of (2) is nonnegative and nondecreasing in $\psi$ , with increments bracketed by $\delta\,\Pr\{\psi\delta \ge p_2(Q_T), \mathcal A\}$ at the two endpoints, and this slope is below one.
Equation (2) has a unique solution $\psi \ge p_1$ .

Significance

Theorem 1 reduces a customer's strategy, a function of arrival time and valuation, to one threshold function $\psi$ on $[0, T)$ . The segment sizes $\Lambda_I, \Lambda_S, \Lambda_W, \Lambda_L$ of §4.2, the seller's menu problem (3), the equilibrium iteration (4) and the closed form of Proposition 2 are all written in terms of $\psi$ ; without Theorem 1 none of them is defined. Corollary 1, that the threshold rises toward the markdown, is what the paper calls "useful in our analyses below"; the customer segments of Figure 1 are drawn with it.

The result is proved in the paper, with a short appendix argument. No machine-checked version exists. The mission produces a formal statement and proof of the reduction for an arbitrary belief, which fixes the exact hypotheses under which it holds: the paper's slope bound needs either valuation decline ( $\alpha > 0$ ) or imperfect availability, and the monotonicity of the threshold needs a nonnegative premium price. A formal $W_t$ and threshold are the starting point for formalizing the equilibrium and pricing results of the paper.

Difficulty

The mathematics is one-dimensional. The difficulty is in stating it exactly. $W_t$ is piecewise linear with a kink wherever $\psi\delta$ crosses a menu price, so the paper's derivative is only a one-sided derivative, and the uniqueness argument has to use increments. The paper's bound "slope $< 1$ " is false when $\alpha = 0$ and a unit is allocated with certainty; then (2) has either no finite solution or a half-line of them. The threshold's monotonicity in $t$ rests on $W_t(\psi)$ increasing in $t$ for fixed $\psi$ , which needs $\psi \ge 0$ ; with a negative premium price the threshold can decrease. The naive reading of "optimal to use a threshold" as an abstract fixed-point fact about any monotone function with slope below one discards the model and is not the goal.

Formalization scope

Lean namespace SeasonalPricing.Contingent. Time, prices and valuations are real numbers. The belief is a pair pmf alloc : ℕ → ℝ restricted to {0, …, Q} (IsInventoryBelief), not a random variable on a probability space; only the law of $(Q_T, \mathbf 1\{\mathcal A\})$ enters (2). The menu is p2 : ℕ → ℝ with $p_2(q) \le p_1$ required on $\{1, \dots, Q\}$ only; $p_2(0)$ never matters because $a(0) = 0$ . The belief does not depend on the arrival time, as in Eq. (4) of the paper. waitingSurplus is $W_t$ with $e^{-\alpha(T-t)}$ written Real.exp (-(α * (T - t))); buysNow is the purchase rule, stated on the current valuation $V(t)$ .

Readings of the paper's words:

"the unique solution" of (2): existence and uniqueness of a real $\psi \ge p_1$ (∃!). The paper's " $\psi \in [p_1, \infty]$ " includes $\infty$ only in the case excluded by the added hypothesis.
"it is optimal to base purchasing decisions on a threshold function": the purchase rule of p. 344 holds exactly when $V(t) \ge \psi(t)$ .
"derivative … $< 1$ ": a two-sided bracket on increments of $W_t$ , with right slope $\delta\Pr\{\psi\delta \ge p_2(Q_T), \mathcal A\}$ , below one.
"increasing" (Corollary 1): nondecreasing (MonotoneOn), since $\psi$ is constant on an initial interval whenever no menu price is reachable (p. 347).

Added hypotheses, both named in the statements: $\alpha > 0$ or $\sum_q \pi(q)a(q) < 1$ , the one hypothesis the paper's proof uses without stating it; and $p_1 \ge 0$ , the model's convention that prices are nonnegative. Only the branch $0 \le t < T$ of the threshold $\theta$ is stated: for $t \ge T$ the paper's $\theta(t) = p_2$ is the model's rule for late customers. The belief enters through the explicit sum; a formalization with an unspecified monotone $W$ , or with $\psi(t)$ defined by choice inside a definition, is not the target.

No new library is needed beyond finite sums, max and Real.exp. A lemma on unique roots of $\psi \mapsto \psi - c - f(\psi)$ for $f$ with increments bounded by $k(\psi' - \psi)$ , $k < 1$ , is reusable. Proofs of the milestones and the goal, in any order, are welcome.

Selected references

Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
X. Su, Intertemporal Pricing with Strategic Customer Behavior, Management Science 53(5):726–741, 2007. https://doi.org/10.1287/mnsc.1060.0667
G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999

5 thms2 active usersReviewed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Subjectivity and Correlation in Randomized Strategies II: Subjective Events Let Both Zero-Sum Players Beat the ValueResearch Paper

Motivation

In a two-person zero-sum game with objective randomization, whatever one player gains the other loses: the value $v$ of the game is the most player 1 can guarantee and the least player 2 can hold him to, and no arrangement between the players can give player 1 more than $v$ and player 2 more than $-v$ at the same time. Aumann's 1974 paper (doi:10.1016/0304-4068(74)90037-8) replaces objective coin flips by ordinary events of the world, about which players may hold different subjective probabilities and may be differently informed. Sect. 6 of the paper shows that this breaks the zero-sum logic: once the players disagree about the probability of events they can observe, a zero-sum game becomes, in expectation as each player computes it, a game in which both can gain.

The phenomenon is the game-theoretic form of betting between people who disagree: two players with different beliefs can each expect to profit from the same wager. Aumann's proposition identifies exactly what information structure makes such an agreement possible inside a given zero-sum game, and shows by an example that informing only one player of a subjective event is not enough. The same paper introduced correlated equilibrium; the companion mission of this series formalizes its two-person result on subjective mixed equilibria (Proposition 5.1).

Setting

A game has a finite set $N=\{1,\dots,n\}$ of players, a finite set $S_i$ of pure strategies for each player, a finite set $X$ of outcomes and an outcome function $g$ from $S=\times_{i\in N}S_i$ onto $X$ . Player $i$ has a utility $u_i:X\to\mathbb R$ ; write $h_i(a)=u_i(g(a))$ for $a\in S$ .

A randomizing structure consists of a set $\Omega$ of states of the world with a $\sigma$ -field $\mathcal B$ of events, a sub- $\sigma$ -field $\mathcal J_i\subseteq\mathcal B$ for each player (the events regarding which $i$ is informed), and a probability measure $p_i$ on $\mathcal B$ for each player (the subjective probability of $i$ ). A strategy of $i$ is a map $s_i:\Omega\to S_i$ whose level sets lie in $\mathcal J_i$ . For a profile $s$ of strategies, player $i$ 's payoff is computed under his own beliefs:

H_i(s)=\int_\Omega h_i\big(s(\omega)\big)\,dp_i(\omega).

An event $A$ is objective if all $p_i(A)$ coincide, and subjective otherwise. It is $i$ -secret if $A\in\mathcal J_i$ and every other player $j$ regards $A$ as independent of every event in the $\sigma$ -field generated by the $\mathcal J_k$ , $k\ne i$ . It is public if it lies in every $\mathcal J_i$ . A measure is non-atomic on a $\sigma$ -field $\mathcal R$ if every event of $\mathcal R$ of positive measure contains an event of $\mathcal R$ of strictly smaller positive measure; a roulette is a sub- $\sigma$ -field of $\mathcal B$ on which every $p_j$ is non-atomic, and a public roulette is a roulette of public events. Throughout, Assumption II holds: every player $i$ has a $\sigma$ -field $\mathcal R_i$ of $i$ -secret events on which every $p_j$ is non-atomic.

The game is two-person zero-sum if $n=2$ and $u_1(x)+u_2(x)=0$ for all $x\in X$ . Its value $v$ is player 1's payoff $F_1(\sigma)=\sum_{a\in S}h_1(a)\sigma_1(a_1)\sigma_2(a_2)$ at a Nash equilibrium $\sigma$ of the classical mixed extension; by the minimax theorem all such equilibria give the payoff pair $(v,-v)$ .

Formalization targets

Goal: Proposition 6.1 (p. 80)

Let $G$ be a two-person zero-sum game with value $v$ , and assume

\exists\,x,y\in X:\ u_1(x)>v>u_1(y),\tag{6.2}

\text{for each } i\in\{1,2\} \text{ there is } B_i\in\mathcal J_i \text{ with } p_1(B_i)\ne p_2(B_i).\tag{6.3}

Then there is a pair $s=(s_1,s_2)$ of strategies with

H_1(s)>v,\qquad H_2(s)>-v.\tag{6.4}

The pair is not an equilibrium: it is an agreement that each player, by his own beliefs, strictly prefers to playing the game.

Milestones

Lemma 7.1 (p. 81): in a roulette $\mathcal R$ there is, for every $\alpha\in[0,1]$ and events $B^1,\dots,B^l$ , an objective event $A\in\mathcal R$ with $p(A)=\alpha$ , independent of each $B^k$ .
Lemma 4.2 (p. 77): for every $i$ , event $B$ and $\alpha\in[0,1]$ there is an objective $i$ -secret event of probability $\alpha$ independent of $B$ .
Lemma 4.4 (p. 77): if there is a public roulette, the same holds with "public" in place of " $i$ -secret".
Remark after Proposition 6.1 (p. 80): the conclusion (6.4) under (6.2) and

\text{there is a public subjective event } B \text{ and there is a public roulette,}\tag{6.5}

a special case of the goal in which the players share both the subjective event and the correlating device.

Significance

The proposition shows that the value of a zero-sum game is a property of objective randomization, not of the game alone. With subjective randomization available to both players, the conflict of a zero-sum game can be resolved by agreement, so the classical prediction (each player receives his security level) is not robust to disagreement about probabilities. The counterexample on p. 81 (the game with matrix rows $(1,1)$ and $(2,0)$ ) shows that hypothesis (6.3) is needed for both players, and the paper notes that in any specific game only one player need use a subjective strategy, though which one depends on the game.

Lemmas 4.2, 4.4 and 7.1 are the model's basic existence results for objective randomization: every probability can be realised by an event that is secret (or public) and independent of finitely many given events. They are used throughout the paper, including in the companion mission.

The paper's proofs are published and accepted; none of these statements has a machine-checked proof. This mission produces the formal statements and invites complete proofs; Lemma 7.1 requires Lyapunov's convexity theorem for finite-dimensional non-atomic vector measures, which is not in Mathlib.

Difficulty

The central difficulty for the goal is that (6.3) gives each player only some subjective event, of unknown size and in his own information field, while (6.4) requires strict gains for both players under two different measures at once. The obvious approach, betting on one subjective event, gives one player a strict gain but, when that event is not known to the other player, the other player cannot condition his choice on it; the example on p. 81 shows that one-sided information genuinely fails. Both inequalities must be arranged simultaneously, and the strategies must remain measurable with respect to each player's own information.

For Lemma 7.1, a non-atomic scalar measure takes every value in $[0,p(\Omega)]$ , but the lemma asks for one event with prescribed values under $n$ measures and $nl$ further measures simultaneously; this is the range of a vector measure, not of a scalar one.

Formalization scope

Players of the zero-sum game are 0, 1 : Fin 2 (the paper's 1, 2). S 0, S 1, X are finite types and g is surjective.
$\mathcal B$ is the σ-field mΩ, an explicit parameter of RandomizingStructure; $\mathcal J_i$ are σ-fields below it, and each $p_i$ is a probability measure on $\mathcal B$ . Probabilities are ℝ≥0∞-valued; "probability $\alpha$ " is ENNReal.ofReal α with $0\le\alpha\le1$ .
Non-atomicity is the standard notion on a sub-σ-field, not Mathlib's NoAtoms, which would trivialize the roulette hypotheses.
$H_i$ is a Bochner integral under $p_i$ ; for strategies with finitely many values it is the finite sum $\sum_a p_i\{s=a\}h_i(a)$ .
The value $v$ is not a free real: IsValue u g v requires $v=F_1(\sigma)$ for a Nash equilibrium $\sigma$ of the mixed extension (AGT.IsMixedNash from the published definition agt_games). A free $v$ would make the goal false. The minimax theorem is the published AGT.zero_sum_minimax.
Assumption II is a hypothesis of every theorem, including those whose proofs do not need it.
The conclusion of the goal and of the Remark asks for strategies, not for an equilibrium point, and does not require the strategies to be independent or objective.

Needed infrastructure: Lyapunov's theorem (or a direct argument for the finite-dimensional case), manipulation of σ-fields generated by families of sub-σ-fields, and computation of $H_i$ for strategies with finitely many values. Lyapunov's theorem is reusable far beyond this mission. Contributions of any milestone are welcome.

Selected references

R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1 (1974) 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
A. Lyapunov, Sur les fonctions-vecteurs complètement additives, Bull. Acad. Sci. URSS Sér. Math. 4 (1940) 465–478.
J. von Neumann, Zur Theorie der Gesellschaftsspiele, Mathematische Annalen 100 (1928) 295–320. https://doi.org/10.1007/BF01448847
J. Nash, Non-cooperative games, Annals of Mathematics 54 (1951) 286–295. https://doi.org/10.2307/1969529

9 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

The Theory of Dynamic Programming: The Index Rule for Bellman's Stochastic Gold-Mining ProblemResearch Paper

Motivation

Richard Bellman's survey The theory of dynamic programming (Bull. Amer. Math. Soc. 60 (1954), 503–515, DOI 10.1090/s0002-9904-1954-09848-8) introduced dynamic programming to a general mathematical audience. It states the principle of optimality (§2, p. 504): "An optimal policy has the property that whatever the initial state and initial decisions are, the remaining decisions must constitute an optimal policy with regard to the state resulting from the first decisions", and derives from it the functional equations of finite and infinite stochastic decision processes, (4.2) and (5.1) (p. 506).

The survey illustrates the method on a small number of worked examples. The second of them, §8 "Stochastic gold mining" (pp. 508–509), is the one with a sharp answer: a two-armed sequential allocation problem with an absorbing failure state, whose optimal policy is a simple index rule. It is an early instance of the allocation-index phenomenon later made general by Gittins and Jones (1974) and Gittins (1979), and the paper itself notes (p. 509) that the rule "is not valid generally in more complicated decision processes", citing a counterexample of Karlin and Shapiro. The full treatment is in Bellman's RAND report R-245 and his 1957 book Dynamic Programming.

Setting

Two gold mines, Anaconda ( $A$ ) and Bonanza ( $B$ ), hold amounts $x \ge 0$ and $y \ge 0$ of gold. A single machine can be used in either mine. A use in Anaconda succeeds with probability $p$ : it then mines a fraction $r$ of the gold currently in Anaconda and the machine stays undamaged. With probability $1-p$ it mines nothing and the machine is destroyed. Bonanza behaves the same way with probability $q$ and fraction $s$ . While the machine works, the operator chooses the next mine; the aim is to maximize the expected amount mined before the machine is destroyed.

The only information the operator ever receives is that the machine still works. A policy is therefore a choice sequence $\sigma = (\sigma_0, \sigma_1, \dots) \in \{A, B\}^{\mathbb N}$ : the mine for use number $n$ , applied if uses $0, \dots, n-1$ succeeded. With $a_n$ , $b_n$ the numbers of $A$ - and $B$ -uses among the first $n$ , use $n$ collects $g_n = r x (1-r)^{a_n}$ if $\sigma_n = A$ and $g_n = s y (1-s)^{b_n}$ if $\sigma_n = B$ , and does so with probability $\prod_{k=0}^{n} \pi_{\sigma_k}$ ( $\pi_A = p$ , $\pi_B = q$ ). The expected return is

J(\sigma; x, y) = \sum_{n \ge 0} \Big(\prod_{k=0}^{n} \pi_{\sigma_k}\Big) g_n ,

and Bellman's (8.1) defines the optimal return

f(x, y) = \sup_\sigma J(\sigma; x, y).

In Lean these are expectedReturn p q r s σ x y and optimalReturn p q r s x y in the namespace BellmanTheoryDP.GoldMining.

Formalization targets

Milestone: the functional equation (8.2), p. 508

f(x, y) = \max\Big\{ p\,[r x + f((1-r)x, y)],\ q\,[s y + f(x, (1-s)y)] \Big\}.

Goal: the decision rule (8.3), p. 509, corrected

Write $V_A = p[rx + f((1-r)x, y)]$ and $V_B = q[sy + f(x, (1-s)y)]$ for the two branches of (8.2). For $0 < p, q, r, s < 1$ and $x, y \ge 0$ :

\frac{prx}{1-p} > \frac{qsy}{1-q} \Rightarrow V_A > V_B, \qquad \frac{prx}{1-p} < \frac{qsy}{1-q} \Rightarrow V_A < V_B, \qquad \frac{prx}{1-p} = \frac{qsy}{1-q} \Rightarrow V_A = V_B .

The paper prints the rule with $(1-r)$ and $(1-s)$ in the denominators:

a. For $prx/(1 - r) > qsy/(1 - s)$ , choose A, b. For $prx/(1 - r) < qsy/(1 - s)$ , choose B, c. For $prx/(1 - r) = qsy/(1 - s)$ , choose either.

and glosses it as "the locus of points where immediate expected gain over immediate expected loss is the same for both choices". The immediate expected loss is the probability of destroying the machine, $1-p$ (resp. $1-q$ ), not $1 - r$ . As printed the rule is false: with $p = 1/2$ , $r = 0.9$ , $q = 0.9$ , $s = 0.1$ , $x = 1$ , $y = 2$ the printed indices are $4.5 > 0.2$ , but $V_A \approx 0.924 < V_B \approx 1.055$ . The mission's goal is the corrected rule, the one the paper describes in words.

Companion: the index policy is optimal, p. 509

"Using this prescription, $f(x, y)$ may be computed recurrently": the choice sequence $\sigma^*$ generated by applying the corrected rule to the current amounts at every use satisfies $J(\sigma^*; x, y) = f(x, y)$ .

Significance

The decision rule reduces an optimization over infinite sequences to comparing two explicit numbers, one per mine, each depending only on that mine's own data. This is the defining property of an index policy, and gold mining is one of the earliest problems where it was observed. The functional equation (8.2) is the concrete form, for this process, of the infinite-horizon equation (5.1) that the paper states formally.

Formalizing the example yields a complete machine-checked instance of the principle of optimality for an infinite-horizon stochastic process whose state space (the amounts left in the two mines) is infinite, where the supremum over policies is not attained trivially and the finite-horizon recursion does not apply directly. It also records, with a checked statement, the correction of the misprint in (8.3). No machine-checked proof of (8.2) or (8.3) is known to exist.

Difficulty

The equation (8.2) looks immediate, and the paper calls it "easily seen". The informal argument treats $f$ as the value of an optimal policy, but $f$ is a supremum over infinite sequences that need not be attained a priori, and the return of a sequence is an infinite series. The finite-horizon recursion (4.2) does not apply as it stands, because the process has no last stage and its state space, the amounts left in the two mines, is infinite.

The rule (8.3) compares the two optimal continuations $f((1-r)x, y)$ and $f(x, (1-s)y)$ , which are themselves unknown. A comparison of the one-step gains alone does not decide it, as the misprinted rule shows. Parts a and b are strict preferences, so it is not enough to show that one choice is at least as good as the other.

Formalization scope

Representation. The mines are a two-element inductive type Mine; a policy is a function ℕ → Mine (ChoiceSeq). All quantities are real numbers. Randomized policies are mixtures of choice sequences and give no larger return, so they are not modelled. No restriction to stationary or Markov policies is made: $f$ is the supremum over all sequences.
Parameter ranges. The paper does not state them. The theorems assume $0 < p, q, r, s < 1$ and $x, y \ge 0$ (zero amounts allowed). $p, q < 1$ keeps the indices $prx/(1-p)$ , $qsy/(1-q)$ well defined.
Series and supremum. $J$ is a real tsum and $f$ a real iSup. For the parameter ranges above the terms are nonnegative, the partial sums are bounded by $x + y$ , and the family is bounded above, so neither Lean default value (0 for a divergent series or an unbounded supremum) arises; this is stated as the auxiliary theorem expectedReturn_le_add.
Survival indexing. The gold of use $n$ is counted only if use $n$ itself succeeds, so the survival product runs over $k \le n$ .
The misprint. The goal and the index policy use $(1-p)$ , $(1-q)$ in place of the printed $(1-r)$ , $(1-s)$ . The printed rule appears only as the quotation above.
No trivializing encoding. $f$ is defined as the supremum of expected returns over all choice sequences, per (8.1); it is not defined as a solution of (8.2), as the value of the index policy, or as a limit of value iteration, any of which would make the milestone or the goal true by definition.
Auxiliary theorems (not from the paper). The bound $0 \le J \le x + y$ with summability, the one-step unrolling $J(\sigma) = p[rx + J(\sigma'; (1-r)x, y)]$ when $\sigma_0 = A$ (and symmetrically), and the single-mine values $f(x, 0) = prx/(1 - p(1-r))$ , $f(0, y) = qsy/(1-q(1-s))$ are included as footholds. They are not milestones.
Related platform content. AllocationIndices.two_discount_index_policy_optimal (Gittins et al., Theorem 3.4) concerns Markov bandits whose rewards are discounted by $a^t$ at global time $t$ ; gold mining multiplies by the success probability of each use of the mine used, so it is a different model and is not reused. BertsekasDP.dp_algorithm_optimality is finite-horizon and does not give (8.2).

Contributions welcome: proofs of the auxiliary theorems, of (8.2), of the decision rule, and of the optimality of the index policy.

Selected references

R. Bellman, The theory of dynamic programming, Bull. Amer. Math. Soc. 60 (1954), no. 6, 503–515. https://doi.org/10.1090/s0002-9904-1954-09848-8
R. Bellman, Dynamic Programming, Princeton University Press, 1957.
J. C. Gittins, Bandit processes and dynamic allocation indices, J. Roy. Statist. Soc. Ser. B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
J. C. Gittins, K. D. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9780470980033

4 thms2 active usersReviewed

Completed

Bandit Algorithms Machine Learning Optimization·Captain: mikedeng1

Taming the Monster: A Fast and Simple Algorithm for Contextual Bandits II: The Iteration Bound of Coordinate DescentResearch Paper

Motivation

In the contextual bandit problem a learner repeatedly observes a context, picks one of $K$ actions, and sees the reward of that action only. Against a finite class $\Pi$ of policies, statistically optimal regret of order $\sqrt{KT\ln|\Pi|}$ has been known since EXP4 (Auer et al., 2002), but EXP4 maintains a weight per policy and costs $\Omega(|\Pi|)$ time per round. For the large policy classes used in practice (linear classifiers, trees), that is prohibitive.

The oracle-efficient line of work accesses $\Pi$ only through a cost-sensitive classification oracle (an arg max oracle, AMO). The RandomizedUCB algorithm of Dudík et al. (2011) obtains optimal regret with polynomially many oracle calls by solving a convex program in each round, but the number of calls is large. Agarwal, Hsu, Kale, Langford, Li and Schapire (2014) replace that solver by a coordinate descent method whose number of iterations, and hence of oracle calls, is bounded independently of $|\Pi|$ . Their algorithm, ILOVETOCONBANDITS, and its practical variant are now standard references for oracle-based exploration.

This mission formalizes the optimization half of that paper: Algorithm 2 solves the per-epoch problem (OP) after at most $4\ln(1/(K\mu))/\mu$ coordinate steps.

Setting

Let $A=\{0,\dots,K-1\}$ be the actions, $X$ any set of contexts, and $\Pi\subseteq A^X$ a finite nonempty set of policies. A history $H_t$ is a sequence of $t\ge1$ records $(x_i,a_i,r_i(a_i),p_i(a_i))$ with $r_i(a_i)\in[0,1]$ the observed reward and $p_i(a_i)\in(0,1]$ the probability with which $a_i$ was chosen. Write $\widehat{\mathbb E}_{x\sim H_t}[f(x)]=\frac1t\sum_i f(x_i)$ .

The inverse propensity scoring estimate (Eq. (1)) is

\widehat{\mathcal R}_t(\pi)=\frac1t\sum_{i=1}^t\frac{r_i(a_i)\,\mathbb 1\{\pi(x_i)=a_i\}}{p_i(a_i)},

the estimated regret is $\widehat{\mathrm{Reg}}_t(\pi)=\max_{\pi'\in\Pi}\widehat{\mathcal R}_t(\pi')-\widehat{\mathcal R}_t(\pi)$ , and for a minimum probability $\mu$ one sets $b_\pi=\widehat{\mathrm{Reg}}_t(\pi)/(\psi\mu)$ with $\psi=100$ .

Weights are vectors $Q\in\mathbb R^\Pi$ ; $\Delta^\Pi$ is the set of nonnegative $Q$ with $\sum_\pi Q(\pi)\le1$ . The smoothed projection of $Q$ is

Q^\mu(a\mid x)=(1-K\mu)\sum_{\pi:\ \pi(x)=a}Q(\pi)+\mu .

The optimization problem (OP) asks for $Q\in\Delta^\Pi$ with

\sum_{\pi\in\Pi}Q(\pi)b_\pi\le2K\quad(2),\qquad \widehat{\mathbb E}_{x\sim H_t}\Bigl[\frac1{Q^\mu(\pi(x)\mid x)}\Bigr]\le2K+b_\pi\ \ \forall\pi\in\Pi\quad(3).

Algorithm 2 starts from $Q_{\mathrm{init}}$ and loops. With $V_\pi(Q)=\widehat{\mathbb E}[1/Q^\mu(\pi(x)\mid x)]$ , $S_\pi(Q)=\widehat{\mathbb E}[1/Q^\mu(\pi(x)\mid x)^2]$ and $D_\pi(Q)=V_\pi(Q)-(2K+b_\pi)$ : if $\sum_\pi Q(\pi)(2K+b_\pi)>2K$ it rescales $Q$ by $c=2K/\sum_\pi Q(\pi)(2K+b_\pi)$ (Eq. (4)); then, if some $\pi$ has $D_\pi(Q)>0$ , it adds

\alpha_\pi(Q)=\frac{V_\pi(Q)+D_\pi(Q)}{2(1-K\mu)S_\pi(Q)}

to $Q(\pi)$ (Step 8) and repeats; otherwise it halts and outputs $Q$ .

The analysis uses the potential (Eq. (6)), with $\tau=t$ and $\mathcal U_A$ uniform on $A$ ,

\Phi_m(Q)=\tau\mu\left(\frac{\widehat{\mathbb E}_x[\mathrm{RE}(\mathcal U_A\,\|\,Q^\mu(\cdot\mid x))]}{1-K\mu}+\frac{\sum_\pi Q(\pi)b_\pi}{2K}\right),\qquad \mathrm{RE}(p\|q)=\sum_a\bigl(p_a\ln\tfrac{p_a}{q_a}+q_a-p_a\bigr).

Formalization targets

Goal: Theorem 3 (p. 6)

For $0<\mu\le1/(2K)$ , Algorithm 2 with $Q_{\mathrm{init}}=\mathbf 0$ satisfies: every run executes Step 8 at most

\frac{4\ln(1/(K\mu))}{\mu}

times, whatever policy each Step 8 chooses among those with $D_\pi>0$ ; and when it halts, its output solves (OP). The bound depends on $K\mu$ only, not on $|\Pi|$ or $t$ .

Milestones

Lemma 5 (p. 10). If Algorithm 2 halts and outputs $Q$ , then $Q$ satisfies (2), (3) and $\sum_\pi Q(\pi)\le1$ .
Lemma 6 (p. 10). If $\sum_\pi Q(\pi)(2K+b_\pi)>2K$ and $c$ is as in Eq. (4), then $\Phi_m(cQ)\le\Phi_m(Q)$ .
Lemma 7 (p. 10). If $D_\pi(Q)>0$ and $Q'$ adds $\alpha_\pi(Q)$ to $Q(\pi)$ , then

\Phi_m(Q)-\Phi_m(Q')\ge\frac{\tau\mu^2}{4(1-K\mu)}.

Significance

The result. Theorem 3 is what makes ILOVETOCONBANDITS computationally efficient: each call of Algorithm 2 is implemented with one AMO call per iteration (Lemma 1 of the paper), so the oracle complexity of an epoch is $O(\ln(1/(K\mu))/\mu)$ . Combined with the epoch schedule and warm start, this gives the paper's total of $\tilde O(\sqrt{KT/\ln(|\Pi|/\delta)})$ oracle calls over $T$ rounds. Theorem 3 also gives a constructive proof that (OP) is feasible for every history, which the regret analysis (a separate mission in this series) assumes.

Formalizing it. The result is proved in the paper, with complete proofs of Lemmas 5–7 in Appendix D. No machine-checked version is known. The formalization would give a checked termination bound for a coordinate descent method on a non-smooth feasibility problem, with a fully explicit constant, and a verified definition of the unnormalized relative entropy potential that is reusable for other smoothed-projection analyses (e.g. RandomizedUCB-type convex programs).

Difficulty

Termination cannot be read off the constraints. Step 8 raises one weight and can push the total weight above 1, after which Step 5 shrinks every coordinate, so no constraint and no single weight moves monotonically along a run. The number of policies that violate (3) can also go up after a step. Bounding the number of iterations therefore needs a global quantity that tracks progress through both kinds of step. The rescaling step is the harder of the two: it lowers every $Q^\mu(a\mid x)$ at once, which pushes the relative-entropy term the wrong way, and it must be offset by the drop in the regret term. Knowing that (OP) is feasible, or that some convex function has a minimizer, bounds nothing about how many steps a particular method takes; that is the obvious approach, and it gives no count.

Formalization scope

Actions are Fin K with $K\ge1$ ; contexts form an arbitrary type (no measure is needed: Theorem 3 is deterministic). $\Pi$ is a nonempty Finset (X → Fin K); weights are real functions on its subtype.
Histories are indexed by Fin t with $t\ge1$ (0-based indices). The paper allows $p_i(a_i)\in[0,1]$ ; the formalization requires $p_i(a_i)\in(0,1]$ , since Eq. (1) divides by it.
$\widehat{\mathrm{Reg}}_t(\pi)$ is written as $\max_{\pi'}\widehat{\mathcal R}_t(\pi')-\widehat{\mathcal R}_t(\pi)$ , which equals $\widehat{\mathcal R}_t(\pi_t)-\widehat{\mathcal R}_t(\pi)$ for any maximizer $\pi_t$ ; $\psi=100$ is hard-wired in $b_\pi$ .
$Q^\mu$ , $V_\pi$ , $S_\pi$ , (OP) and $\Phi_m$ all use the smoothed projection of the unnormalized weights; there is no default policy in this mission.
$\mu$ ranges over $(0,1/(2K)]$ , the range of $\mu_m$ in Algorithm 1 that the printed theorem refers to. $\tau$ in $\Phi_m$ is the history length $t$ .
Algorithm 2 is encoded relationally. A run of length $n$ from $Q_{\mathrm{init}}$ is a sequence $Q^{(0)}=Q_{\mathrm{init}},\dots,Q^{(n)}$ in which each $Q^{(k+1)}$ is Step 8, for some policy with $D_\pi>0$ , applied to the rescaled $Q^{(k)}$ . It halts at $Q^{(n)}$ when no policy has $D_\pi>0$ after rescaling, and it then outputs the rescaled $Q^{(n)}$ . "Iterations" means executions of Step 8. The last pass, which halts at Step 10, is not counted: the paper's proof bounds "the number of times Step 8 is executed". The bound is compared in $\mathbb R$ , without rounding.
Lemmas 5–7 are stated for nonnegative weight vectors without a bound on their sum, because Algorithm 2 rescales vectors whose sum may exceed 1. Lemma 7's " $\alpha=\alpha_\pi(Q)>0$ " is part of its conclusion.
A trivializing formalization is ruled out: the goal quantifies over every run from $\mathbf 0$ and every choice in Step 8, not over some run, and the potential, $b_\pi$ and $D_\pi$ are computed from the history rather than taken as free parameters.
The auxiliary facts $\Phi_m\ge0$ and $\Phi_m(\mathbf 0)\le\tau\mu\ln(1/(K\mu))/(1-K\mu)$ are inline claims in the paper and are not stated separately; contributions stating and proving them are welcome, as are general lemmas on the unnormalized relative entropy.
Out of scope: the regret bound (Theorem 2) and the probabilistic model (mission I of this series), the AMO implementation (Lemma 1), warm start and epoch-level oracle counts (Lemmas 2, 3, 8), and the support lower bound (Theorem 4).

Selected references

A. Agarwal, D. Hsu, S. Kale, J. Langford, L. Li, R. E. Schapire, Taming the Monster: A Fast and Simple Algorithm for Contextual Bandits, ICML 2014; arXiv:1402.0555v2. https://arxiv.org/abs/1402.0555
M. Dudík, D. Hsu, S. Kale, N. Karampatziakis, J. Langford, L. Reyzin, T. Zhang, Efficient Optimal Learning for Contextual Bandits, UAI 2011. https://arxiv.org/abs/1106.2369
P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM J. Comput. 32(1), 2002. https://doi.org/10.1137/S0097539701398375

7 thms2 active usersReviewed

Bandit Algorithms Machine Learning Operations Research+1·Captain: mikedeng1

Online Decision Making with High-Dimensional Covariates: Regret Bound of the LASSO BanditResearch Paper

Motivation

Many sequential decisions are personalised: a physician chooses a drug dose for each arriving patient, a platform chooses which offer to show each arriving user. Each decision is made after observing a vector of covariates describing the individual, and its outcome is observed only for the option chosen. This is the contextual (covariate) bandit problem, studied in operations research and machine learning since Auer (JMLR 2002) and Goldenshluger and Zeevi (Stochastic Systems 2013).

In medical and e-commerce applications the covariate vector is often high-dimensional: the number of covariates $d$ is comparable to or larger than the number of decisions that will ever be made, while the outcome of each option depends on a few of them. Low-dimensional bandit algorithms then incur regret that grows polynomially with $d$ . Bastani and Bayati (Operations Research 2020) proposed the LASSO Bandit, which estimates each option's reward model with the LASSO, and proved a regret bound that grows only logarithmically in $d$ . The paper evaluates the method on warfarin dosing data.

Timeline:

2002–2003: Auer introduces linear-reward contextual bandits with confidence bounds.
2013: Goldenshluger and Zeevi give a forced-sampling algorithm for two arms in low dimension with $O(\log T)$ regret under a margin condition and an arm-optimality condition, and an information-theoretic lower bound of the same order.
2020: Bastani and Bayati extend the forced-sampling scheme to $K$ arms and high-dimensional sparse parameters, with regret $O(s_0^2[\log T+\log d]^2)$ .

Setting

There are $K$ arms with unknown parameters $\beta_1,\dots,\beta_K\in\mathbb R^d$ . At each time $t=1,2,\dots,T$ a covariate vector $X_t\in\mathbb R^d$ arrives; the $X_t$ are i.i.d. with law $\mathcal P_X$ and take values in a fixed set $\mathcal X$ . If arm $i$ is pulled, the reward is $X_t^\top\beta_i+\varepsilon_{i,t}$ , where the noises $\varepsilon_{i,t}$ are independent, $\sigma$ -subgaussian ( $\mathbb E[e^{s\varepsilon}]\le e^{\sigma^2s^2/2}$ for all $s$ ), and independent of the covariates. A policy chooses the arm $\pi_t$ from $X_t$ and the past covariates, arms and observed rewards. Its cumulative expected regret is

R_T=\sum_{t=1}^T\mathbb E\Big[\max_jX_t^\top\beta_j-X_t^\top\beta_{\pi_t}\Big].

The sparsity $s_0$ is the smallest integer $s_0\ge1$ with $\|\beta_i\|_0\le s_0$ for all $i$ .

The four assumptions are: (1) $\|x\|_\infty\le x_{\max}$ on $\mathcal X$ and $\|\beta_i\|_1\le b$ ; (2) a margin condition $\Pr[0<|X^\top(\beta_i-\beta_j)|\le\kappa]\le C_0\kappa$ ; (3) arm optimality: every arm is either suboptimal by a margin $h$ at every covariate, or optimal by margin $h$ on a region $U_i$ of probability at least $p_*$ ; (4) a compatibility condition: the conditional second-moment matrix $\Sigma_i=\mathbb E[XX^\top\mid X\in U_i]$ of each optimal arm lies in the set $\mathcal C(\mathrm{supp}(\beta_i),\phi_0)$ of matrices $M\succeq0$ with $\|v_I\|_1^2\le|I|\,v^\top Mv/\phi_0^2$ whenever $\|v_{I^c}\|_1\le3\|v_I\|_1$ .

The LASSO estimator on $n$ samples is any minimizer of $\|Y-\mathbf X\beta'\|_2^2/n+\lambda\|\beta'\|_1$ . The LASSO Bandit forces arm $i$ at the prescribed times $\mathcal T_i=\{(2^n-1)Kq+j : n\ge0,\ q(i-1)<j\le qi\}$ . At every other time it keeps the arms whose forced-sample estimate $\hat\beta(\mathcal T_{i,t-1},\lambda_1)$ is within $h/2$ of the best. Among them it plays the arm with the largest all-sample estimate $\hat\beta(\mathcal S_{i,t-1},\lambda_{2,t-1})$ , trained on every past pull of the arm, with $\lambda_{2,t}=\lambda_{2,0}\sqrt{(\log t+\log d)/t}$ .

Formalization targets

Goal: Theorem 1 (regret of the LASSO Bandit)

For $q\ge4\lceil q_0\rceil$ , $K\ge2$ , $d>2$ , $T\ge C_5$ , $\lambda_1=\phi_0^2p_*h/(64s_0x_{\max})$ and $\lambda_{2,0}=[\phi_0^2/(2s_0)]\sqrt{1/(p_*C_1)}$ ,

R_T\le C_3(\log T)^2+\big[2Kbx_{\max}(6q+4)+C_3\log d\big]\log T+\big(2bx_{\max}C_5+2Kbx_{\max}+C_4\big),

with the explicit constants $C_1,\dots,C_5$ , $q_0$ of the paper (p. 285).

Milestones

Proposition 1: a LASSO tail inequality for adaptively collected rows with conditionally subgaussian noise.
Lemma 1: a LASSO tail inequality when a constant fraction of the rows is i.i.d. with a compatible second-moment matrix.
Proposition 2: the forced-sample estimator of an optimal arm is within $h/(4x_{\max})$ of $\beta_i$ except with probability $5/t^4$ .
Proposition 3: the all-sample estimator of an optimal arm is within $16\sqrt{(\log t+\log d)/(p_*^3C_1t)}$ of $\beta_i$ except with probability $2/t+2e^{-p_*^2C_2^2t/32}$ .

Significance

The theorem shows that exploiting sparsity makes the regret depend on the ambient dimension only through $\log d$ , while its dependence on the horizon is within one $\log T$ factor of the $\Omega(\log T)$ lower bound known in low dimension. Proposition 1 is a LASSO oracle inequality for adapted designs, where each row may depend on earlier observations. It applies whenever a LASSO is fitted to data gathered by a feedback policy: adaptive experiments, dynamic pricing, sequential treatment assignment.

The results are proved in the paper and its online appendix; none of them has a machine-checked proof. This mission produces a formal model of the covariate bandit with a non-anticipating algorithm, a formal LASSO for adapted designs, and, when complete, a verified regret bound with every constant explicit. Proposition 1 and Lemma 1 are reusable beyond bandits.

Difficulty

The all-sample estimator is trained on the times at which the algorithm chose an arm, and those choices depend on earlier estimates. Its design rows are therefore neither independent nor identically distributed, and the standard LASSO analysis, which starts from i.i.d. rows and a restricted-eigenvalue bound on their population covariance, does not apply. The forced samples are i.i.d. but only $O(\log t)$ in number, too few for the $\sqrt{\log t/t}$ rate the regret bound needs. Controlling the compatibility constant of the adaptively selected sample covariance, and the martingale noise term, is where the naive argument breaks.

Formalization scope

Arms are Fin K (paper arm $i$ is i.val + 1), coordinates Fin d, times are natural numbers from $1$ . The model is a structure IsCovariateNoiseModel on a probability space: i.i.d. measurable covariates in a measurable set $\mathcal X$ , independent subgaussian noises (Mathlib's HasSubgaussianMGF with parameter $\sigma^2$ ), noise independent of covariates. Assumptions 1–4 are separate predicates. $\|x\|_\infty$ is Mathlib's sup norm, logarithms are natural, and $\Sigma_i$ is the uncentred conditional second moment.

The LASSO minimizer and the arg max need not be unique, so the algorithm takes a selection rule and a tie-breaking rule as parameters, and the theorems hold for all of them. Each round reads only the current covariate, the past covariates, the past arms and their observed rewards. The regret theorem and Proposition 3, whose data set $\mathcal S_{i,t}$ is chosen by the algorithm, require both rules to be measurable. Otherwise the trajectory would not be a random variable, and the expectations in $R_T$ could be integrals of non-measurable functions, which Lean evaluates to $0$ and which would make the goal trivially true. For the same reason every assumption constant is required to be positive, and $T\ge C_5$ is imposed on the horizon. Only the explicit inequality of Theorem 1 is stated, not the trailing $O(s_0^2[\log T+\log d]^2)$ or $q_0=O(s_0^2\log d)$ . Proposition 2 is stated for optimal arms (see its note).

A complete development needs matrix concentration for bounded i.i.d. rows, the Azuma–Hoeffding inequality, and the deterministic LASSO basic inequality under a compatibility condition. Contributions of any of these as standalone lemmas are welcome.

Selected references

H. Bastani and M. Bayati, Online Decision Making with High-Dimensional Covariates, Operations Research 68(1):276–294, 2020. https://doi.org/10.1287/opre.2019.1902
A. Goldenshluger and A. Zeevi, A Linear Response Bandit Problem, Stochastic Systems 3(1):230–261, 2013. https://doi.org/10.1287/11-SSY032
P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3:397–422, 2002. https://www.jmlr.org/papers/v3/auer02a.html
P. Bühlmann and S. van de Geer, Statistics for High-Dimensional Data, Springer, 2011. https://doi.org/10.1007/978-3-642-20192-9

9 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

School Choice: A Mechanism Design Approach 2: The Top Trading Cycles Mechanism with Type-Specific Quotas Is Strategy-ProofResearch Paper

Motivation

Many US school districts assign children to public schools centrally. Each family ranks the schools. Each school ranks the children by priority, which is set by state or local law (siblings, walking distance, a lottery). A procedure then turns these rankings into an assignment. Abdulkadiroğlu and Sönmez (Columbia Economics Discussion Paper 0203-18, 2003; published in the American Economic Review 93(3), 2003) cast this as a mechanism design problem. They showed that the mechanisms then in use in Boston, Columbus and Minneapolis gave families reasons to misreport their preferences. They proposed two alternatives: the student-optimal stable mechanism of Gale and Shapley, and a school-choice version of Shapley and Scarf's top trading cycles (TTC) mechanism.

Many districts also operate under controlled choice: court-ordered or voluntary rules that keep the racial or ethnic composition of each school within bounds. In Minneapolis, for instance, a 100-seat school could admit at most 75 majority and at most 55 minority students (paper, Section III). Such rules are implemented as type-specific quotas. Section III.B of the paper modifies TTC to respect these quotas. It proves that the modified mechanism keeps both properties that recommend TTC: it wastes nothing beyond what the quotas force (constrained efficiency, Proposition 6), and truth-telling is a dominant strategy (strategy-proofness, Proposition 7). This mission formalizes those two results.

Setting

There is a finite set $I$ of students and a finite set $S$ of schools. School $s$ has a capacity $q_s$ , and the total number of seats suffices: $|I|\le\sum_s q_s$ . Each student $i$ has a strict preference over all schools, encoded as a ranking $P_i : S\to\{0,\dots,|S|-1\}$ with rank $0$ the favourite. Each school $s$ has a strict priority ranking over all students, with rank $0$ the highest priority. Each student belongs to exactly one type $\tau(i)$ , and school $s$ has a type quota $q_s^t$ for each type $t$ .

An assignment $\nu$ gives each student a school or nothing ( $\varnothing$ , worse than every school). It satisfies the controlled choice constraints if every school $s$ receives at most $q_s$ students, and at most $q_s^t$ students of each type $t$ . An assignment $\mu$ is constrained efficient if no assignment satisfying the constraints makes every student weakly better off and some student strictly better off.

The top trading cycles mechanism with type-specific quotas, $\mathrm{TTC}^q$ , runs in steps. Each school keeps a counter $c_s$ (initially $q_s$ ) and one type counter $c_s^t$ for each type (initially $q_s^t$ ). A school is removed when $c_s$ reaches zero. At each step:

every remaining student points to her favourite remaining school with room for her type, that is, with $c_s>0$ and $c_s^{\tau(i)}>0$ ;
every remaining school points to its highest-priority remaining student, whatever her type;
every student on a cycle of this graph is assigned the school she points to and leaves;
that school's counter and its counter for her type each drop by one.

A direct mechanism is strategy-proof if no student can ever gain by misreporting her preference, whatever the others report.

Formalization targets

Goal: Proposition 7 (p. 23)

For every student $i$ , every profile $P$ of announced preferences and every alternative report $Q_i$ ,

\mathrm{TTC}^q(Q_i,P_{-i})(i)=s' \implies \mathrm{TTC}^q(P)(i)=s \text{ with } P_i(s)\le P_i(s').

This holds for all capacities without shortage, all quotas, all types and all priorities. The priorities are fixed data, not reported.

Milestones

Section III.B, Step 1 (p. 22). At every step there is at least one cycle, after the convention below has removed the students who cannot point.
The Lemma (Appendix, pp. 28–29; declared valid for the modified mechanism on p. 30). Fix the other students' reports, and suppose student $i$ is still present at the beginning of a step under two different reports of hers. Then the two runs have the same remaining students and the same counters at that point.
Proposition 6 (p. 23). $\mathrm{TTC}^q(P)$ satisfies the controlled choice constraints and is constrained efficient with respect to $P$ .

Significance

Strategy-proofness is what lets a district publish a simple instruction: rank the schools in your true order. A strategy-proof mechanism does not reward families who can afford to gather information and game the system. Proposition 7 shows that this guarantee survives the addition of flexible diversity quotas, which many districts are legally bound to impose. Proposition 6 shows that the quotas cost nothing beyond the losses they themselves cause. Both results were proved in 2003 by pen and paper. The published proof of Proposition 7 is a short adaptation of the proof of Proposition 4 (strategy-proofness of plain TTC). It rests on a lemma about how the algorithm's intermediate states depend on one student's report.

To our knowledge neither result has a machine-checked proof. The related platform theorem AGT.ttc_strategyproof concerns the Shapley–Scarf housing market, where every agent owns one house and the mechanism selects the core. It does not cover capacities, priorities or quotas. A formal proof here would check the adaptation that the paper leaves to the reader, and would give a reusable formal model of cycle-clearing allocation algorithms with multiple counters.

Difficulty

The algorithm clears all cycles of a step at once, and a student's report changes the graph at every step she is present. The paper's argument compares two whole runs of the algorithm, under the true report and under a misreport, step by step. That comparison needs precise control of which parts of the state a single student's report can influence, and when. A local argument about one step does not suffice. The student's outcome can depend on cycles that form several steps after the two runs could first have diverged.

With quotas, the pointing graph also depends on the type counters. A school can be present but closed to one type, and a school points to its best remaining student even when it has no room for her type. The comparison must therefore track the type counters as well as the set of remaining schools. Efficiency cannot be read off step by step against unrestricted matchings either: every competing assignment must satisfy both the capacity and the quota constraints.

Formalization scope

Students, schools and types are finite types; no nonemptiness is assumed. Preferences and priorities are bijective rankings onto Fin, so strictness is built in. Rank $0$ is the favourite or the highest priority. The no-shortage condition $|I|\le\sum_s q_s$ appears in every theorem, as the standing assumption of Section I. No relation between $q_s$ and $q_s^t$ is imposed, which generalises the paper.

The algorithm is a concrete, total definition: a state with remaining students, counters, type counters and partial assignments, a step map that clears all cycles simultaneously, and $|I|$ iterations. run … t is the state at the beginning of the paper's Step $t+1$ .

The paper's step is undefined when a remaining student has no remaining school with room for her type. She cannot point, and the promised cycle may not exist. The formalization adopts one convention: at the beginning of each step, such a stuck student is removed unassigned, and her outcome is $\varnothing$ , ranked below every school. Counters only decrease, so a stuck student stays stuck. Whenever nobody gets stuck, the algorithm is exactly the paper's, and when every quota is at least the capacity it is plain TTC. The goal and Proposition 6 are stated for assignments that may leave students unassigned. When everyone is assigned, they coincide with the paper's statements over matchings.

The formalization does not add a hypothesis that the run never gets stuck. Such a hypothesis would restrict the algorithm's own behaviour and could make the theorems vacuous. Nor may strategy-proofness be weakened to comparisons at the truthful profile only: the others' reports and the misreport are arbitrary.

Contributions welcome: invariants of the step map (counters bounded by the initial values, assigned students leave for good), the cycle-existence lemma for functional graphs on finite sets, and the comparison lemma. These pieces are shared with the plain-TTC mission of this series.

Selected references

Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, Columbia University Department of Economics Discussion Paper No. 0203-18, 2003. https://doi.org/10.7916/D8057T27
Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, American Economic Review 93(3), 729–747, 2003. https://doi.org/10.1257/000282803322157061
Lloyd Shapley and Herbert Scarf, On Cores and Indivisibility, Journal of Mathematical Economics 1(1), 23–37, 1974. https://doi.org/10.1016/0304-4068(74)90033-0

6 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

School Choice: A Mechanism Design Approach 1: The Top Trading Cycles Mechanism Is Strategy-ProofResearch Paper

Motivation

Public school districts in many US cities let families rank schools and then assign seats by a centralized procedure. Each school has a limited number of seats, and state or local law gives some students priority at some schools, for example for a sibling already enrolled or for living within walking distance. Abdulkadiroğlu and Sönmez (Columbia Economics Discussion Paper 0203-18, 2003; published in the American Economic Review 93(3), 2003) framed this as a mechanism design problem and showed that the mechanism then used in Boston rewards families who misreport their preferences. They proposed two replacements with written proofs of their properties. This mission covers the second one, the top trading cycles mechanism, and its two properties: every outcome is Pareto efficient, and no student can gain by misreporting.

The paper drew on earlier results for simpler allocation problems:

1974: Shapley and Scarf introduce housing markets and Gale's top trading cycles algorithm, in which each agent owns one house.
1977: Roth and Postlewaite show the algorithm finds the unique core allocation of a housing market.
1982: Roth proves the core mechanism for housing markets is strategy-proof.
1999: Abdulkadiroğlu and Sönmez adapt the algorithm to house allocation with existing tenants and prove strategy-proofness.
2000: Pápai introduces hierarchical exchange rules, a wider class that includes these mechanisms.
2003: the paper formalized here extends the algorithm to schools with capacities and school-specific priorities (Propositions 3 and 4).

Setting

A school choice problem consists of a finite set $I$ of students, a finite set $S$ of schools, a capacity $q_s \in \mathbb N$ for each school, a strict preference $P_i$ of each student over all schools, and a strict priority ordering $\succ_s$ of each school over all students. The standing assumption is that there is no shortage of seats:

|I| \le \sum_{s\in S} q_s .

Preferences are rankings: $P_i(s)\in\{0,\dots,|S|-1\}$ is the rank of $s$ for student $i$ , with rank $0$ the favourite. Priorities are rankings of students in the same way, with rank $0$ the highest priority. A matching is a map $\mu : I\to S$ with $\#\{i:\mu(i)=s\}\le q_s$ for every school $s$ . A matching $\mu$ is Pareto efficient if no other matching $\nu$ gives every student a weakly better school ( $P_i(\nu(i))\le P_i(\mu(i))$ ) and some student a strictly better one.

A direct mechanism maps the reported preference profile, together with the fixed priorities and capacities, to a matching. It is strategy-proof if no student can ever obtain a school she strictly prefers by changing her own report while the others keep theirs.

The top trading cycles algorithm keeps a counter $c_s$ of free seats at each school, starting at $q_s$ . A school is remaining while $c_s>0$ . At each step every remaining student points to her favourite remaining school, and every remaining school points to the remaining student with the highest priority for it. A cycle is a list $(s_1,i_1,\dots,s_k,i_k)$ of distinct schools and students in which $s_1$ points to $i_1$ , $i_1$ points to $s_2$ , and so on, and $i_k$ points to $s_1$ . Every student on a cycle is assigned the school she points to and is removed. Each school on a cycle loses one seat. All cycles present at a step are cleared at that same step. The top trading cycles mechanism $\mathrm{TTC}(q,\succ,P)$ returns the resulting assignment.

Formalization targets

Goal: Proposition 4 (strategy-proofness)

For all capacities with no shortage, all priorities, every profile $P$ , every student $i$ and every alternative report $Q_i$ , student $i$ is assigned schools $s = \mathrm{TTC}(q,\succ,P)(i)$ and $s' = \mathrm{TTC}(q,\succ,(Q_i,P_{-i}))(i)$ , and

P_i(s) \le P_i(s') .

Milestones

At every step at which some student remains, there is a cycle (Section II.B, p. 15).
After $|I|$ steps no student remains, and the outcome is a matching (Section II.B, p. 16).
Lemma (Appendix, pp. 28–29): if student $i$ is still remaining at the beginning of a step under two different reports of her own, the remaining students and the remaining schools at that point are the same under both reports.
Proposition 3 (p. 17): the outcome is a Pareto efficient matching with respect to the reported profile.
When all schools share one priority ordering $\pi$ , the mechanism equals the serial dictatorship induced by $\pi$ (Section II.B, p. 16).

Significance

Strategy-proofness means truthful reporting is a dominant strategy for every student. Families need no information about other families' reports. Under the Boston mechanism, ranking a popular school first can cost a student her priority at her second choice. Proposition 3 separates the top trading cycles mechanism from the Gale–Shapley student-optimal stable mechanism, which is also strategy-proof but can select Pareto dominated matchings.

The results are proved in the paper, in short prose arguments in its Appendix. To the best of our knowledge they have no machine-checked proof. The platform already has the housing-market version, AGT.ttc_strategyproof, but that statement covers one house per agent with the mechanism characterised as the core. Capacities, school priorities and the step-by-step algorithm are absent from it. This mission produces a checked account of the algorithm with capacities and counters, together with its termination and invariance properties.

Difficulty

The paper's argument moves from the step at which student $i$ leaves under one report to the step at which she leaves under another. It relies on the claim that the cycles formed before either step are unaffected by $i$ 's report. Informally, $i$ is not on a cycle yet, so what she points to does not matter. Formally, "the same cycles form" requires comparing two runs of a simultaneous-clearing procedure step by step. At each step one has to show that the set of cycles, and hence the counters and the remaining schools, agree, even though $i$ points to different schools in the two runs. Reasoning about a single cycle at a time does not work, because the algorithm clears all cycles of a step at once. Termination is also not immediate: without the no-shortage condition the algorithm can leave students unassigned. Seats are counted with multiplicity, so a school can stay in the market for several steps.

Formalization scope

Everything lives in the namespace SchoolChoice.TTC. Students and schools are arbitrary finite types with decidable equality; the set of students may be empty. Capacities are q : S → ℕ, and a school of capacity zero is never remaining. A preference is a bijection S ≃ Fin (card S) and a priority is a bijection I ≃ Fin (card I), in both cases with rank 0 the best. Strictness and completeness of both therefore hold by construction, and every school is acceptable. A state of the algorithm consists of the remaining students, the counters and the assignments made so far. run q pri P t is the state after t completed steps, which is the beginning of the paper's Step t + 1. The mechanism ttc q pri P : I → Option S reads off the assignment after card I steps. Every theorem assumes card I ≤ ∑ s, q s.

The algorithm is a concrete, deterministic definition that clears all cycles at every step. The mechanism is not defined as "some Pareto efficient matching" or characterised by properties, since that would make Proposition 3 trivial. The goal asserts that both outcomes exist, so an unassigned outcome cannot satisfy it vacuously. The misreport, the other students' reports and the priorities are all universally quantified.

A complete development needs termination of the algorithm, a combinatorial account of the pointing graph (cycles in a finite functional graph), and the step-by-step invariance argument of the Lemma. The last two are reusable for the type-specific quota variant and for other trading-cycle mechanisms. Contributions of intermediate lemmas are welcome: counter invariants such as "the sum of the counters is at least the number of remaining students", monotonicity of the remaining sets, and the fact that a student on a cycle receives her favourite remaining school.

Selected references

Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, Columbia University Department of Economics Discussion Paper No. 0203-18, 2003. https://doi.org/10.7916/D8057T27
Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, American Economic Review 93(3), 729–747, 2003. https://doi.org/10.1257/000282803322157061
Lloyd Shapley and Herbert Scarf, On Cores and Indivisibility, Journal of Mathematical Economics 1(1), 23–37, 1974. https://doi.org/10.1016/0304-4068(74)90033-0
Alvin E. Roth and Andrew Postlewaite, Weak versus Strong Domination in a Market with Indivisible Goods, Journal of Mathematical Economics 4(2), 131–137, 1977. https://doi.org/10.1016/0304-4068(77)90004-0
Alvin E. Roth, Incentive Compatibility in a Market with Indivisible Goods, Economics Letters 9(2), 127–132, 1982. https://doi.org/10.1016/0165-1765(82)90003-9
Atila Abdulkadiroğlu and Tayfun Sönmez, House Allocation with Existing Tenants, Journal of Economic Theory 88(2), 233–260, 1999. https://doi.org/10.1006/jeth.1999.2553
Szilvia Pápai, Strategyproof Assignment by Hierarchical Exchange, Econometrica 68(6), 1403–1433, 2000. https://doi.org/10.1111/1468-0262.00166

9 thms2 active usersReviewed

Completed

Discrete Geometry Linear Optimization Operations Research+1·Captain: mikedeng1

Elementare Theorie der konvexen Polyeder I: A Point on All Extreme Supports of a Finite Cone Is a Nonnegative Combination of at Most n GeneratorsResearch Paper

Motivation

A polyhedral cone can be described in two ways: as the set of nonnegative combinations of finitely many vectors (a finitely generated cone), or as the intersection of finitely many closed half-spaces through the origin. That the two descriptions give the same class of sets is the Minkowski–Weyl theorem. It is the structural basis of linear programming: the simplex method, LP duality, Farkas' lemma, and the vertex/facet description of polytopes used throughout combinatorial optimization all rest on it.

Hermann Weyl's 1935 paper Elementare Theorie der konvexen Polyeder (Comment. Math. Helv. 7, 290–306) gives an elementary, self-contained proof of both directions. Its first result, which Weyl calls the Hauptsatz (main theorem, Satz 1), is the direction "finitely generated ⇒ finite intersection of half-spaces", in a sharp form: the half-spaces needed are exactly the extreme supports of the generating set, i.e. its facets. Its sharpening, Satz 2, bounds the number of generators needed to represent a point by the dimension $n$ . This mission formalizes §§1–2 of the paper (pp. 290–295): the Hauptsatz, its sharpening, and the steps of Weyl's inductive proof.

Timeline:

1896, H. Minkowski, Geometrie der Zahlen: polytopes as bounded intersections of half-spaces and as convex hulls of finitely many points.
1911, C. Carathéodory: a point in the convex hull of a set in $\mathbb{R}^d$ is a convex combination of at most $d+1$ of its points (Rend. Circ. Mat. Palermo 32).
1935, H. Weyl: the present paper; Satz 1 and Satz 2 for cones, with the dual statements in §3 and the polytope theorem in §4.

Setting

Points of $\mathbb{R}^n$ are $n$ -tuples $x = (x_1, \ldots, x_n)$ , and $\langle \alpha, x \rangle = \alpha_1 x_1 + \cdots + \alpha_n x_n$ . A vector $\alpha \ne 0$ determines the half-space $\{x : \langle\alpha,x\rangle \ge 0\}$ ; positive multiples of $\alpha$ give the same half-space.

A point system $S$ is a finite set of points of $\mathbb{R}^n$ . It is non-degenerate if its points do not all satisfy one equation $\langle\alpha,x\rangle = 0$ with $\alpha \neq 0$ , i.e. the only $\alpha$ orthogonal to every point of $S$ is $0$ .

A half-space $\langle\alpha,x\rangle\ge 0$ ( $\alpha\ne 0$ ) is a support of $S$ if every point of $S$ lies in it. It is an extreme support if, in addition, equality $\langle\alpha,x\rangle = 0$ holds at $n-1$ linearly independent points $x$ of $S$ .

A point $x$ is representable by $S$ if it is a nonnegative combination of the points of $S$ :

x = \sum_{s\in S} c_s\, s, \qquad c_s \ge 0 .

The set of points lying in all extreme supports of $S$ is Weyl's konvexe Pyramide. In the Lean development these objects are Representable, NonDegenerate, IsSupport and IsExtremeSupport in the namespace WeylPolyhedra.Pyramid, with points of type Fin n → ℝ and $\langle\alpha,x\rangle$ written α ⬝ᵥ x.

Formalization targets

Goal: Satz 2 (Verschärfung des Hauptsatzes), p. 295

For a finite non-degenerate $S \subset \mathbb{R}^n$ and a point $x$ with $\langle\alpha,x\rangle\ge 0$ for every extreme support $\alpha$ of $S$ ,

\exists\, T \subseteq S,\quad |T| \le n,\quad x = \sum_{t\in T} c_t\, t,\ \ c_t \ge 0 .

Satz 1 (Hauptsatz), p. 291

Under the same hypotheses, $x$ is representable by $S$ . Satz 2 contains Satz 1.

Steps of the proof (§1–§2)

A finite non-degenerate $S$ has only finitely many extreme supports, up to positive scaling (p. 291).
The reduction step of case a) (p. 292): if $S$ has an extreme support $\beta$ and $p$ satisfies all extreme supports, there are $e \in S$ with $\langle\beta,e\rangle>0$ and $\lambda\ge 0$ such that $q = p-\lambda e$ still satisfies all extreme supports and lies on the plane of one of them.
The lifting step (p. 293): with $x_n \ge 0$ an extreme support of $S$ and $S_0$ the points on $x_n = 0$ , every extreme support $\beta$ of $S_0$ in $\mathbb{R}^{n-1}$ lifts to the extreme support $\beta_1x_1+\cdots+\beta_{n-1}x_{n-1} - \mu x_n \ge 0$ of $S$ (inequality (6)).
Case b) (p. 291, proved pp. 293–294): if $S$ has no extreme support, every point of $\mathbb{R}^n$ is representable by $S$ .

Significance

Satz 1 together with its trivial converse identifies the cone generated by $S$ with the intersection of its extreme-support half-spaces. This is one half of the Minkowski–Weyl theorem for cones, and it names the half-spaces: they are the facets of the cone. Satz 2 adds the conic form of Carathéodory's theorem: every point of a cone generated by a finite spanning set in $\mathbb{R}^n$ is a nonnegative combination of at most $n$ generators. In linear programming this is the statement that a feasible system has a basic feasible solution. The second mission in this series, on §§3–4 of the paper, uses Satz 1 to prove that a bounded region cut out by finitely many inequalities is the convex hull of finitely many points, and conversely.

On formalization status: Mathlib defines finitely generated and dually finitely generated pointed cones (PointedCone, PointedCone.DualFG) and proves Carathéodory's theorem for convex hulls (convexHull_eq_union), but, at the pinned revision, it does not prove the Minkowski–Weyl theorem or the facet description of a finitely generated cone. The results are classical and proved in the paper; this mission produces machine-checked proofs of them, in Weyl's formulation with extreme supports, together with the intermediate steps of his induction.

Difficulty

The hypothesis only controls $x$ against the extreme supports, not against every support. Showing that $x$ lies in the cone generated by $S$ whenever $\langle\alpha,x\rangle\ge 0$ holds for every support is the conic Farkas lemma, which follows from a separating hyperplane argument. Here that argument is not enough: a separating hyperplane is a support, but in general not an extreme one, and the statement is about the finitely many extreme ones. The proof has to produce, for a point outside the cone, a violated extreme support, which requires control over the facet structure of the cone.

The dimension count of Satz 2 is a second difficulty. An induction on the dimension naturally gives $n$ generators in one case and $n+1$ in another (a point of a half-space needs one generator on each side), and Weyl notes that he could not avoid a detour to recover the bound $n$ . The case where $S$ has no extreme support at all must also be handled separately; it is not vacuous, since $S$ can then generate all of $\mathbb{R}^n$ .

Formalization scope

Conventions committed to in Lean:

$\mathbb{R}^n$ is Fin n → ℝ; points and normals share this type (the dual space is identified with $\mathbb{R}^n$ , as in the paper). The pairing is dotProduct, written α ⬝ᵥ x.
A point system is a Finset (Fin n → ℝ). The zero vector is not excluded.
A support normal satisfies α ≠ 0. Extreme supports require a subset T ⊆ S with T.card = n - 1 whose elements are linearly independent in the vector space $\mathbb{R}^n$ .
"All extreme support equations are satisfied" in Satz 1 is read as the inequalities $\langle\alpha,x\rangle\ge0$ for every extreme normal $\alpha$ , as the proof and Satz 2 make explicit. The hypothesis quantifies over all extreme normals, so no representatives are chosen.
"Positive-linear" combinations have nonnegative coefficients (display (3)). In Satz 2 the subset $T$ is not required to be linearly independent.
Finiteness of extreme supports is stated up to positive scaling.
The lifting step is stated in the coordinates Weyl fixes on p. 293: $\mathbb{R}^n$ is Fin (m+1) → ℝ, the extreme support is $x_n \ge 0$ (Fin.last m), $S_0$ is projected by Fin.init, and $\mu$ is given together with hypotheses that it is the attained minimum. The hypothesis $n \ge 2$ is made explicit.

Replacing extreme supports by all supports in the hypothesis of Satz 1 or Satz 2 would turn the goal into a much weaker theorem (the conic Farkas lemma plus Carathéodory) and is not an admissible formalization. Dropping non-degeneracy makes Satz 1 false: for $S = \{e_1\} \subset \mathbb{R}^2$ the extreme supports are $\pm x_2 \ge 0$ , and $x = (-1, 0)$ satisfies both without being a nonnegative multiple of $e_1$ .

A complete development needs basic linear algebra over Fin n → ℝ (hyperplanes through $n-1$ independent points, projection to a coordinate hyperplane) and finite minimisation. The facet description of finitely generated cones, conic Carathéodory and the finiteness of facets are reusable beyond this mission, including for the second mission of the series. Contributions of lemmas on PointedCone that connect Representable with PointedCone.span are welcome.

Selected references

H. Weyl, Elementare Theorie der konvexen Polyeder, Commentarii Mathematici Helvetici 7 (1935), 290–306. https://doi.org/10.1007/BF01292722
C. Carathéodory, Über den Variabilitätsbereich der Fourier'schen Konstanten von positiven harmonischen Funktionen, Rendiconti del Circolo Matematico di Palermo 32 (1911), 193–217. https://doi.org/10.1007/BF03014795
A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, §7.2 (the Farkas–Minkowski–Weyl theorem). ISBN 978-0-471-98232-6
G. M. Ziegler, Lectures on Polytopes, Springer GTM 152, 1995, Lecture 1. https://doi.org/10.1007/978-1-4613-8431-1

9 thms2 active usersReviewed

Campaigns

All missions

Campaigns

All missions

Campaigns

All missions

A Supply Chain Theory of Factoring and Reverse Factoring 1: The Supplier's Equilibrium Choice Among Recourse, Non-Recourse and Reverse FactoringResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 5

Milestones

Significance

Difficulty

Formalization scope

Selected references

Robust Solutions to Uncertain Semidefinite Programs II: An SDP Inner Approximation of the Robust Feasible Set under Structured PerturbationsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2 (p. 37), as an inclusion of feasible sets

Milestones

Significance

Difficulty

Formalization scope

Selected references

Integrating Replenishment Decisions with Advance Demand Information II: With Zero Set-up Cost the Myopic Base-Stock Policy Is Optimal When Myopic Levels Are NondecreasingResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5 (p. 1352)

Milestones: Theorem 4 (p. 1351)

Significance

Difficulty

Formalization scope

Selected references

Validation of Subgradient Optimization I: The Core Problem Built from the Subgradient Iterates Solves the Dual Linear ProgramResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.3 (p. 82)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Robust Solutions to Least-Squares Problems with Uncertain Data II: Robust Least Squares as Tikhonov RegularizationResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2 with the identity for μ\muμ

Milestones (in the order of the paper's proof, p. 1041)

Significance

Difficulty

Formalization scope

Selected references

Linear-Time Approximation for Maximum Weight Matching: The Approximation Guarantee of the Scaling AlgorithmResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.12, approximation half

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Conditional and Dynamic Convex Risk Measures I: Robust Representation of Conditional Convex Risk MeasuresResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimizing Static Linear Feedback: Gradient Method II: The Gradient Flow Stays in the Sublevel Set and Converges Exponentially under State FeedbackResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2 with the identity for $\mu$