Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
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.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
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.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic 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 -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
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.
The sharp Hlawka inequality for Schatten -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 . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Large combinatorial structures are often best understood through their limits. For dense graphs, Lovász and Szegedy (2006) showed that every sequence of graphs whose subgraph densities converge has a limit object, a graphon, and that every graphon arises this way. Borgs, Chayes, Lovász, Sós and Vesztergombi (2008) related this convergence to the cut distance. These results turned questions of extremal combinatorics and property testing into analysis on a compact space.
Hoppen, Kohayakawa, Moreira, Ráth and Sampaio (arXiv:1103.5844; J. Combin. Theory Ser. B, 2013) carried this programme over to permutations. Their limit objects, called limit permutations here and now usually called permutons (as a probability measure on the square), underlie later work on quasirandom permutations, pattern densities, and property testing of permutations (Hoppen et al., 2011). This mission formalizes the paper's main result, Theorem 1.6: convergent permutation sequences have limits, and every limit is attained.
Timeline:
For , is the set of permutations of , and for . For and , the number of occurrences counts the increasing -tuples in with . The subpermutation density is for and for . A permutation sequence is convergent if converges for every fixed .
A function is a cdf if it is non-decreasing and right-continuous with and . A limit permutation is a Lebesgue measurable such that is a cdf for every , and for every . The set of limit permutations is .
With one associates a random point : , and given , has cdf . Draw independent copies . The -random permutation records the relative order of the read in increasing order of the . The density of in is . A sequence with converges to , written , if for every .
For , the step limit permutation spreads the permutation matrix of uniformly over its grid cells. The rectangular distance is the largest difference, over axis-parallel rectangles, between the probabilities the two associated random points assign to the rectangle.
The two parts together identify with the set of limits of permutation sequences.
In the order the proof uses them:
Theorem 1.6 makes , modulo null sets, the completion of the set of finite permutations under density convergence. Asymptotic statements about pattern densities, such as quasirandomness criteria, extremal pattern-density problems and the testability of permutation properties, can then be stated and proved on a compact space of measures rather than along sequences. Lemma 4.2 is the quantitative sampling statement behind testability, and Theorem 1.7 says that a limit, viewed as a measure on the square, is unique.
The results are proved in the paper and have been used for over a decade. To the best of current knowledge they are not formalized in any proof assistant. The mission produces a machine-checked account of the permuton correspondence: the definitions of subpermutation density, limit permutation and -random permutation, and the equivalences between the three natural convergences on . Alternative proofs are welcome, for instance of (ii) through Lemma 4.2 and the Borel–Cantelli lemma rather than the paper's strong law for U-statistics.
The obvious route to (i) is compactness: the laws of the random points attached to have a weakly convergent subsequence. The weak limit is only a measure, however. Turning it into a function that is a cdf in for every , with exact uniform integrals for every , requires a regular conditional distribution (Lemma 2.2). One then has to show that weak convergence carries the pattern densities along. That fails for general measures on the square, because the events defining have boundaries on which ties occur. Uniform marginals are what rule the ties out. The limit must also be independent of the subsequence, which needs the uniqueness statement Lemma 5.1. For (ii), the natural random sequence converges only almost surely, so an almost-sure limit theorem or a quantitative concentration bound is unavoidable.
unitInterval with Lebesgue measure. A limit permutation is a curried real function Z : I → I → ℝ. Measurability is almost-everywhere measurability for the product measure, which is Lebesgue measurability. The cdf and integral conditions hold for every and every .Equiv.Perm (Fin n) (0-based), and a permutation sequence is ℕ → Σ n, Equiv.Perm (Fin n). Patterns of every length, including the trivial length , are quantified over; the length- clause always holds.Needed infrastructure includes Prokhorov compactness of probability measures on a compact space, the Portmanteau theorem, conditional cdfs (ProbabilityTheory.condCDF), Hoeffding's inequality and Borel–Cantelli, all largely in Mathlib. The permutation-density and permuton layer is reusable for quasirandomness and testing results. Mission II of this series, on the rectangular-distance characterization, uses the same model.
A semidefinite program (SDP) minimizes a linear objective subject to a linear matrix inequality . 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.
Fix natural numbers . The decision variable is . The nominal data are affine maps
with every symmetric, and fixed matrices , . A perturbation is a matrix , and the perturbed constraint matrix is the linear-fractional representation (LFR)
which is defined when . The perturbation ranges over a linear subspace , which encodes the structure, and is bounded by a level in the spectral norm (the largest singular value). The robust feasible set is
and the robust SDP (RSDP) is to minimize over .
The scaling set of is the linear subspace
For every : if some has , and
then , and in fact for every with . 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.
then every integer vector closest to in the maximum norm satisfies .
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 . 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 (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 in each coordinate of 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).
The inequality to be proved is a statement about infinitely many perturbations, and depends on through a matrix inverse. The natural first step, eliminating by an exact S-procedure as in the full case, is not available: with a structured the set of pairs of vectors linked by some is not described by one quadratic inequality, and losslessness fails. The scalings in give several valid quadratic inequalities instead, and one must show that their combination controls every in the norm ball, including the well-posedness claim , which is part of the conclusion rather than an assumption. The commutation condition must be turned into an inequality for , which requires more than the definition of the spectral norm. For Theorem 5.6 the block-diagonal perturbation family and the rescaling between and the stated matrix must be matched to the general lemma.
Matrices are Matrix (Fin a) (Fin b) ℝ; and 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 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 → ℝ. is a Submodule. Affine maps are given by coefficient families indexed by Fin (m+1). Mathlib's matrix inverse is at a singular matrix, so every statement pairs the LFR with . The standing assumption of Section 3 is a hypothesis.
Readings and corrections of the printed statements:
Trivializing formalizations are ruled out: always, so the hypotheses and are kept outside ; 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 and , the spectral-norm characterization , Schur-complement and congruence facts for block matrices, and a linear-fractional identity relating 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.
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 policies.
Time is divided into periods . The supply lead time is an integer , and the information horizon is . In period customers place orders , where is demand placed in period for delivery in period . Throughout, ; write .
At the start of period the decision maker knows two things. The first is the modified inventory position : on-hand stock plus outstanding orders minus backorders, net of the demand already observed for the protection period . The second is the vector
of demands already observed for periods beyond the protection period. The decision maker raises the position to at zero fixed cost, the demand vector is realised, and the state moves to
with .
Costs enter through a single-period cost (holding, backorder and linear ordering cost, charged against the demand over the protection period) and one-period discount factors . The optimal cost-to-go and the cost of ordering up to satisfy
where the expectation is over . The base-stock level in period is the smallest minimizer
and the myopic level is the smallest minimizer of the single-period cost,
A function has decreasing differences if whenever and componentwise.
If is nondecreasing on , then for every period and every observed-demand vector ,
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 for all , the smallest minimizer of is the optimal base-stock level in every period.
For every period and every fixed :
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.
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 -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.
The obvious induction carries convexity of backward, but here the future cost is evaluated at a random next state whose first coordinate depends on the current observed demand . Showing that the base-stock level does not depend on therefore needs more than convexity. It needs to know where is flat, uniformly in the random , 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 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.
The model is parametrised by and , with . The demand vector is a function on and a function on , ordered componentwise. is defined by backward recursion with for . The minimum over is a real infimum and the expectation a Bochner integral against the law of . 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 is a primitive rather than being assembled from , and the lead-time demand; the paper's 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:
The goal cannot be trivialised: the hypotheses are satisfied by concrete instances (for example 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 of a convex coercive function, and preservation of convexity and decreasing differences under expectation. All of them are reusable in other inventory models.
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 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 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 , obtained from quantities the method computes anyway. This is how the authors certified the optimal values reported in their experiments.
Timeline:
Fix and write with the Euclidean inner product . The data are scalars and vectors , and
The function is assumed bounded above, the paper's standing assumption. An index attains the minimum at if .
A run of the subgradient algorithm consists of a starting point , step sizes and indices such that attains the minimum at , and
No rule for choosing among several minimizing indices is imposed. Write and . The step-size conditions are
The dual linear program of is
For integers the core problem has one variable for each iteration :
An index chosen at several iterations contributes several identical columns. A point of is sent to the point of (6.1). This aggregation preserves feasibility and objective value.
Assume is bounded above, is a run satisfying (2.7), and is bounded. Then
The goal states existence of , which is what the paper claims. The paper's argument in fact gives the conclusion for every sufficiently large . That stronger form is not the goal. Feasibility of (Lemma 6.2) or the inequality , which holds for every feasible , is not a formalization of the goal. The content is optimality in (6.1).
Theorem 6.3 turns an asymptotic method into one that returns an exact answer. Solving for growing produces a linear program of bounded size whose optimum is eventually the optimum of (6.1), and hence . 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 and (6.1) is linear-programming duality for a minimum of affine functions.
The inequality 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 are not monotone. So an argument that inspects a single iterate, or assumes that the method settles on one face of , fails. The convergence statement of milestone 2 is not proved in the paper and is the heaviest single step. Feasibility of also needs its own argument, and it fails without the boundedness hypothesis.
is EuclideanSpace ℝ (Fin n), the index set is a finite nonempty type ι, and 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 , so every tie-breaking rule is covered. (2.7) is StepSizeCond t: t → 0, and the partial sums tend to . Iterates are indexed from . Boundedness is Bornology.IsBounded (Set.range π). The variables of are a function on of which only the values at enter. Optimality of 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 is stated as attained at an explicit .
A statement that only asserts feasibility of , or only , is not the theorem. The goal requires that the solutions of be optimal for (6.1).
Theorem 6.1 is printed for the step rule (2.8), but its proof uses , the consequence of (2.7). The mission states it for (2.7), and its milestone title says so.
A complete development needs:
The first three are reusable well beyond this mission. Contributions of any of them, as standalone theorems, are welcome.
Least-squares fitting is a standard tool in estimation, identification and data analysis, and its data , are rarely known exactly. El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed to choose to minimize the worst-case residual over a set of admissible data perturbations. Earlier missions of this series treat unstructured perturbations of and perturbations affine in a parameter vector. §5 of the paper covers a more general model, taken from robust identification (Doyle et al.): the perturbed data depend on an uncertain matrix through a linear-fractional transformation. This form covers rational dependence of the data on uncertain parameters, max-norm bounds on independent parameters, and data matrices with some columns known exactly (pp. 1046–1047).
In this generality, deciding whether the worst-case residual is finite is NP-complete, and computing it is NP-hard even when the dependence is affine (§5.3, Lemma 5.1). Theorem 5.2 gives the tractable replacement: a semidefinite program whose value bounds the worst-case residual from above, and equals it when the perturbation is unstructured. The main tool is a structured form of the S-procedure. Robust control uses the same tool, with the scalings and below, to bound the real structured singular value (Fan, Tits and Doyle, 1991).
Vectors carry the Euclidean norm . For a matrix , is its largest singular value (operator norm between Euclidean spaces). Let be a linear subspace of (the perturbation structure), and fix , , , , , . For with the perturbed data are
With the normalization (the paper's, with no loss of generality), the worst-case residual of is
if for every such , and otherwise (35). The commutant scalings are and (37). The SDP constraint is
For all and :
Part (a) says the value of the SDP (40) is an upper bound on . Part (b) says this upper bound is exact for full perturbations, including the case , where (40) is infeasible.
The worst-case residual under linear-fractional uncertainty cannot be computed efficiently unless P = NP. Theorem 5.2 gives an SDP-computable upper bound with an explicit certificate . Since enters (38) linearly, the same constraint can also be optimized over (Theorem 5.3, not part of this mission). For the bound is exact, which covers the model and, as a special case, the unstructured problem of §3.
The results are proved in the paper (the proof of Theorem 5.2 is only indicated, through Appendix C). No machine-checked version of these statements, of Lemma 2.2 or of the structured S-procedure with commutant scalings is known. The formalization also fixes the statements. As printed, Lemma 2.2's "only if", Lemma 2.3 and the upper bound of Theorem 5.2 are each false in a boundary or structural case (see Formalization scope). The corrected forms stated here are the ones the paper's proofs support.
Part (a) reduces to robust positivity of a linear-fractional matrix function, and the difficulty is the inverse . The certificate is one LMI in which does not appear, while the conclusion is about a rational function of over a whole structured ball. The certificate also has to guarantee that is invertible everywhere on that ball, and not only that the residual is small where it is defined. Evaluating at a single point does not show this. Part (b) needs a lossless S-procedure in its strict form. The standard (non-strict) S-lemma gives only , and the gap between strict and non-strict inequalities is exactly where the printed statements fail. The degenerate case is not covered by the S-lemma's regularity condition and has to be handled separately.
Fin n, Fin m, Fin N; is a Submodule ℝ (Matrix (Fin N) (Fin N) ℝ), with as ⊤. The Euclidean norm is written out, because ‖·‖ on Fin n → ℝ is the sup norm. is the operator norm of Matrix.toEuclideanLin Δ, the largest singular value.ResidualBelow: every with has and residual . It is false for every when . No real-valued supremum is used, so the branch of (35) cannot turn into a default . Matrix inverses are Mathlib's Matrix.inv, and every use carries the determinant condition.ConvexOptimization.s_procedure, in a different sign convention), square roots of positive definite matrices that commute with , and compactness of the structured unit ball. The S-procedure lemmas are reusable in robust control and trust-region analysis. Proofs of the milestones in any order are welcome.Least squares fits a linear model by minimizing , and its solution can be extremely sensitive to errors in the data when is ill-conditioned. The standard remedy is Tikhonov regularization (ridge regression): minimize , whose solution is stable but depends on a parameter 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 seriously: the robust least-squares (RLS) solution minimizes the worst-case residual over all perturbations of Frobenius norm at most . Their Theorem 3.1 shows that for this worst-case residual equals 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 , 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).
Throughout, , , , and every vector norm is Euclidean, . For , is with a coordinate appended, so .
The SOCP (15) is the problem, in the variables and ,
A triple is optimal for (15) if it is feasible and for every feasible . Its dual, derived in the paper from the general second-order cone duality of §2.1, is the problem in , ,
The minimum-norm solution of is a solution with for every other solution ; when is consistent it is , with 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.
Let be optimal for (15) and set . Then
By Theorem 3.1 (the subject of the companion mission I of this series), the -part of an optimal point of (15) is the RLS solution for , so this is formula (17) of the paper. The identity for is the final display of the paper's proof and is the claim in the mission's title.
A further item states Remark 3.1: for , is the unique minimizer of the weighted residual with and .
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 or at its endpoint , and it identifies the point on the path through a fixed-point equation relating to the residual and the size of the solution. The paper builds on this in §3.3 (a one-dimensional search for 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 , all in terms of explicit Euclidean norms on Fin k → ℝ.
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 also needs care: there , 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 , or that assumes the matrix invertible without deriving it from , misses part of the theorem.
Fin k → ℝ; the Euclidean norm is the explicit eucNorm v = √(∑ vᵢ²) (Mathlib's ‖·‖ on Fin k → ℝ is the sup norm). Stacked vectors and are indexed by Fin m ⊕ Unit.Matrix.inv; it is used only where , where the matrix is positive definite. at every feasible point, so is well defined without an extra hypothesis.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.
In 1965 Erdős asked how large a family of -element subsets of an -element set can be if it contains no pairwise disjoint members. The question, now called the Erdős Matching Conjecture (EMC), contains the Erdős–Ko–Rado theorem (the case ) and is one of the central open problems of extremal set theory. Beyond combinatorics it is tied to tail bounds for sums of random variables (generalizations of Markov's inequality, see Alon, Frankl, Huang, Rödl, Ruciński and Sudakov, JCTA 2012, as cited on p. 2 of the paper) and to Dirac-type thresholds for perfect matchings in hypergraphs.
Timeline.
Write and for the set of its -element subsets. For a family , a matching is a subfamily of pairwise disjoint members, and the matching number is the largest size of a matching. The Erdős matching function is
Two families show the conjectured value. The family of all -sets meeting has members; the family of all -subsets of has members. Both have , and the EMC asserts is the larger of the two numbers. For the first is larger.
The proof uses the shifting order: for and , if for all and . A family is initial if it is closed downward under . For , , and denotes the shadow. Families are cross-dependent if no choice is pairwise disjoint, and nested if . A random -matching is a uniformly random ordered -tuple of pairwise disjoint -subsets of , and counts how many of its sets lie in a fixed family of density .
There is an absolute constant such that for all , and
The constant is existential and uniform in and ; no value is fixed, so any improvement of the proof keeps the statement valid.
For every there is such that the same equality holds for all , and . Theorem 1 follows by taking .
Following the paper's proof: Lemma 3 (shifting), Proposition 4, Lemma 5, Proposition 6, Corollary 7 and Lemma 8 (structure of initial families and their shadows); Proposition 11, Theorem 12 and Proposition 13 (concentration of for random matchings); Lemma 18 and Lemma 15 (the weighted bound for cross-dependent nested families); Lemmas 16 and 17 (the induction step at ); Theorem 14.
The theorem extends the range in which the EMC is known from to for large , settling roughly a third of the remaining range. The paper uses it as a black box to derive a universal upper bound on below that range (its Theorem 2) and consequences for Dirac thresholds. The concentration inequality of Theorem 12, a Gaussian tail for the number of members of a fixed family hit by a random matching, is a tool of independent use and has since been applied to rainbow versions of the problem (Kupavskii, arXiv:2104.08083).
The result is proved on paper; this mission formalizes it. No part of the argument has a machine-checked proof: Mathlib has shadows and the Erdős–Ko–Rado theorem, and the platform has Erdős–Ko–Rado for , but there is no formal theory of the matching number, shifted families, Kneser graph spectra, or martingale concentration for random matchings. A complete formalization would make the EMC in this range, and the concentration theorem, available for reuse.
Averaging over a random full partition of into -sets gives only , far from the truth: the expected number of partition classes in says nothing about how that number is distributed. The paper's step is to show the count is concentrated (Theorem 12) and to exploit the deterministic bound of Lemma 18, which penalizes matchings with many classes in . Controlling the regime where the density is small needs the separate comparison of Proposition 13.
The second difficulty is Lemma 17, whose proof in the appendix is a delicate estimate on sums and products of binomial coefficients over all , supported by numerical computations done in Mathematica. A formal proof needs certified numerics for these finite checks and a separate stability argument for . The case is an external base case (Frankl 2017), so the induction on also needs that result or another route.
Sets are finite sets of natural numbers; is Finset.Icc 1 n, so the paper's indices such as and appear unshifted. is a maximum over subfamilies (members are distinct), and is a finite maximum, always attained. Initial families are closed downward among -subsets of only. Random matchings are ordered tuples, and probabilities, expectations and covariances are uniform averages over the finite sample space. The constant is the exact decimal, not . The paper omits integer parts at ; the formalization rounds up. Where the paper leaves hypotheses implicit, they are binders: in Corollary 7, Lemma 8 and Lemma 16, and the induction hypothesis in Lemma 17, in Theorem 12, and (the division ) in Lemma 15.
The goal is the equality ; exhibiting the family of -sets meeting proves only the lower bound and does not close it.
Useful infrastructure, reusable beyond this mission: shifting and the compression argument (Lemma 3), the shadow bounds of Section 2, the expander mixing lemma and the second eigenvalue of Kneser graphs, and the Azuma–Hoeffding inequality for the exposure martingale of a random matching. Contributions of any of these, and of alternative proofs of the milestones, are welcome.
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 time, and the scaling algorithm of Gabow and Tarjan (1991) runs in time on graphs with vertices, edges and integer weights of magnitude at most . Applications such as switch scheduling, graph clustering and sparse linear solvers accept a slightly suboptimal matching in exchange for speed. This motivates -approximate maximum weight matchings: matchings whose weight is at least a 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):
Let be a finite simple graph with integer weights , . A matching is a set of vertex-disjoint edges, with weight ; a vertex is free if no edge of touches it. is a -MWM if for every matching .
A blossom is built recursively: a single vertex is a trivial blossom with ; an odd number of disjoint blossoms joined in a cycle by edges form the blossom with edge set . It is full if . The algorithm keeps a laminar set of full blossoms; a root blossom is a maximal one, and contracts each root blossom to a single vertex.
Dual values and on odd vertex sets give each edge the value
The scaling algorithm (Figure 2 of the paper) has parameters and . It runs scales with granularity and truncated weights . Each scale repeats four steps: augment along a maximal set of vertex-disjoint augmenting paths of the eligible graph , shrink a maximal set of new blossoms, adjust the duals by , and dissolve root blossoms whose -value has reached zero. It stops when the free vertices' -values reach a scale-dependent value, which is at scale . 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 in scales unless it is a blossom edge.
For every with , the algorithm of Figure 2 with Definition 3.10 eligibility has a terminating run, and every terminating run returns a matching with
The result. Theorem 3.12 gives the first algorithm for -approximate maximum weight matching on general graphs that runs in linear time for every fixed ; earlier linear-time algorithms achieved only or . 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.
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 is , and this slack does not shrink as the scales advance. Converting it into a factor 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 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 fraction of , 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 . 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.
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 ; weights are with on edges. Duals, and are real numbers. is a function on all finite vertex sets and sums it over the odd sets that contain the edge, as on the page. and , , are given through their exponents. uses the convention . The paper's standing assumption is used only for running time and is omitted.
The algorithm is a nondeterministic relation. A state holds , with its blossom edge sets, , , a ghost record of the scale in which each edge last entered , 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 -MWM.
The running times of Theorem 3.8 and 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 (Theorem 3.8) and (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 .
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.
A convex risk measure assigns to a bounded financial position (a random net payoff) a number , interpreted as the capital that must be added to 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 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 . 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 with continuity from above. Detlefsen–Scandolo (2005): the conditional version, Theorem 3.2 of the paper formalized here.
Fix a probability space and a sub--algebra describing the available information. is the space of essentially bounded random variables and its -measurable part; every (in)equality between random variables holds -almost surely.
A map is a conditional convex risk measure if and, for :
The admissible models are
For a family of -valued random variables, the essential supremum is the -a.s. smallest random variable that dominates every member -a.s.; it replaces the pointwise supremum, which is not meaningful for uncountable families of equivalence classes.
A map is representable if there is a penalty with
The minimal penalty is . is continuous from above if -a.s. implies -a.s.
For a conditional convex risk measure , the following are equivalent:
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 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 . The last of these is the standard representation theorem of the theory of convex risk measures and is useful well beyond this paper.
The obvious route, applying the unconditional representation pathwise or by , fails: is not a risk measure of anything, and conditional expectations are only defined up to null sets that depend on , 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 , which is not available off the shelf.
MemLp X ⊤ P; is a map constrained only on . Because it acts on functions, is required to respect -a.s. equality, and is required to be -strongly measurable and essentially bounded; the paper's acts on classes, so this adds nothing in substance. is a MeasurableSpace m with m ≤ mΩ.Q[X | m]; it is -measurable, hence determined -a.s. for .EReal; penalties are ENNReal-valued and coerced, so only (real) occurs, never .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 -measurable -valued essential supremum of is a penalty for .⨆ over the family, or via Mathlib's essSup of a single function, and an index set equal to all or to the equivalent to ; each of these changes statement (b) or makes it vacuous.The linear-quadratic regulator (LQR) is the basic problem of optimal control: steer a linear system so as to minimize an integrated quadratic cost. When the full state is measured and the gain may be chosen freely, the optimal feedback is given by the algebraic Riccati equation (Kalman, 1960). In many applications only an output is measured, and the controller is restricted to a static feedback . For this output-feedback problem no Riccati-type characterization exists; the design problem is a non-convex optimization over the gain matrix .
Direct optimization of the gain by gradient descent, known in the control literature since Levine and Athans (1970) and revived in reinforcement learning as policy gradient (Fazel, Ge, Kakade and Mesbahi, 2018, arXiv:1801.05039), is therefore of interest both to control engineers and to the learning community. Fatkhullin and Polyak (arXiv:2004.09875, SIAM J. Control Optim. 2021) give a self-contained analysis of the continuous-time problem: the cost is coercive on the set of stabilizing gains, smooth on sublevel sets, and, for state feedback, satisfies a gradient-domination (Łežanski–Polyak–Łojasiewicz) inequality. From these they derive convergence guarantees for the gradient method.
Fix real matrices , , and weights , , and an initial-state covariance . A gain is a matrix , and the closed-loop matrix is . A square matrix is Hurwitz if all its complex eigenvalues have negative real part. The set of stabilizing gains is
For let be the unique solution of the Lyapunov equation
and define the cost , the expected integrated quadratic cost of the closed loop from a random initial state with covariance . With the solution of , the gradient of in the Frobenius inner product is
A known stabilizing gain is given, and is its sublevel set. The standing assumptions are , and . State feedback (SLQR) is the case .
The gradient method with step sizes is
A number is a smoothness constant if for all .
For , an optimal gain , and any smoothness constant :
and there are , with .
In attack order:
The theorem shows that a plain first-order method, started from any stabilizing gain, never destabilizes the closed loop and decreases the cost monotonically, for output feedback as well as state feedback. For state feedback it converges globally and linearly to the optimal gain. The cost is non-convex, and its domain is open, possibly non-convex and unbounded, so this does not follow from convex optimization theory. It is the continuous-time counterpart of the policy-gradient guarantees of Fazel et al. for discrete-time LQR, and it underlies model-free and data-driven variants of gain tuning.
The result is proved in the paper, but it has not been formalized. The formalization adds three things. It makes the invariance argument (the iterates stay in ) explicit, and the paper describes that argument as the non-trivial part. It corrects the statements where the printed text is wrong (see below). It also produces a reusable library of Lyapunov-equation facts. Mathlib has no Lyapunov equation, no LQR cost and no Hurwitz stability theory, and the platform has no continuous-time LQR material. The nearest platform items treat discrete-time Riccati iteration (BertsekasDP.riccati_convergence_stability) and Polyak–Łojasiewicz rates on a whole normed space (ShiOptRates.pl_rate). Neither applies to a function defined only on a non-convex open subset.
The standard descent-lemma argument assumes is defined and -smooth on the whole space. Here is defined only on , and it is not smooth on all of : it blows up at the boundary. A gradient step from a point of could in principle jump out of , where the Lyapunov equation has no meaningful solution. The smoothness bound is available only inside , so the argument must show that the whole segment from to stays in before the descent inequality can be used on it. That requires coercivity, compactness of and an exit-time argument. For the linear rate, gradient domination has to be established on with constants controlled by , and passing from function values to distances to needs that minimizer's structure. Gradient domination fails for output feedback (the paper's Example 3.4 has two disconnected components with different minima), so the linear rate is stated only for .
Matrices are Matrix (Fin p) (Fin q) ℝ. Hurwitz means every element of the complex spectrum has negative real part. , are "the unique solution of the Lyapunov equation, if there is none or several"; this junk value is never used, because every statement evaluates and only at gains proved or assumed to lie in . The iterates' membership in is a conclusion of the goal, never a hypothesis; assuming it would delete the theorem's content. is defined by the formula (3.3), and Lemma 3.11 is the theorem that it is the gradient. is , is the spectral (operator) norm, and are the minimum and maximum eigenvalue of a symmetric matrix. State feedback is the instance , . In (4.6) the Frobenius norm replaces the paper's spectral norm, which is equivalent because is existential. The minimum over requires .
Deviations from the printed text, each recorded in the item's Formalization Note:
Not stated: Theorem 4.3 and Algorithm 4.1, Lemma 3.6, Lemmas 3.12–3.14, Corollary 3.16 and the explicit constant (3.8). Welcome contributions include a Lyapunov-equation library (existence, uniqueness, integral representation, positivity), continuity of the spectrum, and the exit-time argument, which is reusable for any descent method on a sublevel set of an open domain.
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 for a fixed parameter . Section 3.4 of the paper justifies this substitution: as , 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.
Let be natural numbers and the space of real matrices, with the inner product . Three functions of a matrix are used:
Let be constraint functions and the feasible set. The nuclear norm problem is
and, for , the proximal problem is
When the are convex and is nonempty, (3.4) has exactly one solution, written , because is strongly convex. Problem (1.6) may have many solutions. Among them, the paper singles out the minimum Frobenius norm solution
Linear equality constraints, and in particular the matrix completion constraints for sampled entries , are covered by taking pairs of affine functionals.
Assume that the are convex and lower semicontinuous. Then
In the order in which the paper's proof uses them (all on p. 1967):
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 . Theorem 3.1 says what is worth: for large 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 . 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.
The first steps are elementary consequences of the definitions of and : (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.
A tempting shortcut, reading the family as a sequence indexed by integers, proves a weaker statement: the limit in (3.15) is over real .
Matrix (Fin n₁) (Fin n₂) ℝ, abbreviated Mat n₁ n₂, over the reals as in the paper. and .LinearMap.singularValues of Matrix.toEuclideanLin X. It is the genuine sum of singular values, not an abstract norm or the Frobenius norm.f : Fin m → Mat n₁ n₂ → ℝ of real-valued functions. (no constraints) is allowed.ConvexOn ℝ Set.univ (f i) and LowerSemicontinuous (f i) for every . Lower semicontinuity is redundant for real-valued convex functions on a finite-dimensional space, but it is kept because the theorem states it.Xτ : ℝ → Mat n₁ n₂ assumed to solve (3.4) for every , and its values at play no role. is a matrix assumed to satisfy the defining property (3.14): it solves (1.6) and has the least among its solutions. Uniqueness of is a milestone to prove, not an assumption.Filter.atTop on . Convergence of matrices uses Mathlib's entrywise topology, which is the topology of . The goal states (3.15) literally, with the Frobenius norm of the difference tending to .Infrastructure. The needed facts, all reusable beyond this mission:
Contributions of these general lemmas as separate theorems are welcome.
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 , 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.
Let be natural numbers and the real matrices, with the Frobenius inner product and norm . The nuclear norm is the sum of the singular values of . For a fixed the objective is
A matrix is a subgradient of a function at , written , if for all .
Let be convex and put . On , and is the Euclidean norm. The constrained problem is
with Lagrangian for . A pair with is primal-dual optimal if it is a saddle point:
The paper's standing assumption "strong duality holds" is the existence of such a pair.
The iteration (3.5) starts from and, for step sizes , sets for
where has entries . 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 is affine, the minimization is a singular value thresholding step, which gives the algorithm its name.
The analysis of §4.2 assumes is Lipschitz in the sense
for a constant .
If and strong duality holds, then the sequence of (3.5) converges to the unique solution of (3.4):
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 , 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.
The obvious approach is to view (3.5) as projected gradient ascent on the dual function and quote the standard convergence theorem for gradient methods with Lipschitz gradients. That does not apply directly: for general convex the dual function need not be differentiable, is only a supergradient, and the Lipschitz hypothesis (4.2) is on , 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 with nonsmooth , and it needs the strong monotonicity of (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.
Matrices are Matrix (Fin n₁) (Fin n₂) ℝ, vectors in 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 is a real-valued function with ConvexOn ℝ Set.univ. The iteration is a predicate on sequences indexed by ℕ: the paper's step produces X (k+1) and y (k+1) from y k with step size δ (k+1), and y 0 = 0. is required to minimize ; for and convex this minimizer exists and is unique, so the predicate is satisfiable and determines the sequence. The step-size condition is stated as for with and , which avoids the division (evaluated as in Lean when ); for it requires only bounded steps, matching the convention . Strong duality is the hypothesis that a saddle point exists; Slater's condition is not assumed. The paper's standing assumptions (, convex , and (4.2) where 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 ), 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 ; 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.
Matrix completion asks to recover an matrix from a subset of its entries. When has low rank, a standard convex surrogate is to minimize the nuclear norm (the sum of the singular values) subject to agreeing with on ; Candès and Recht showed that this recovers 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 . 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.
All matrices are real. For write and . The nuclear norm is the sum of the singular values of .
For an index set , the sampling projector keeps the entries with indices in and sets the others to zero.
A reduced singular value decomposition of a matrix of rank is with () and () having orthonormal columns and with . For the singular value shrinkage operator is
Fix , a sequence of step sizes and data . The SVT iteration (2.7) starts from and sets, for ,
The proximal problem (2.8) is
More generally, for a linear map with adjoint and spectral norm , and , problem (3.1) is to minimize subject to , and Uzawa's iteration (3.3) starts from and sets , .
If , then (2.8) has a unique solution and the SVT iterates satisfy
If (3.1) is feasible and , then (3.1) has a unique solution and the iterates of (3.3) converge to it.
The theorem certifies that SVT, run with any step sizes in a fixed interval , 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 (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 , the Lagrangian identity, strong monotonicity of , 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.
Nothing in the iteration is a gradient step of a smooth function in : the -update is a nonsmooth proximal map, and the convergence of 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 to the unique solution.
Matrices are Matrix (Fin n₁) (Fin n₂) ℝ; convergence is Mathlib's topology on matrices, which coincides with the Frobenius-norm topology. and are defined entrywise; is the sum of Mathlib's LinearMap.singularValues of viewed as a map . The shrinkage operator is a relation IsShrink τ Y X defined, as in (2.1)–(2.2), through some reduced SVD of ; well-definedness is a milestone. It is not defined as the minimizer of (2.3), which would make Theorem 2.1 definitional. Linear maps are given by matrices with , and a sampling operator by an injective enumeration of . Subgradients are those of (2.4).
Sequences are indexed by : Lean's step is the paper's step , so and are unused. Committed conventions:
A small unprinted helper, 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.
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 augmentations for capacities (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.
A network consists of a finite set of nodes, a source and a sink , and a set of arcs, which are ordered pairs with ; there is at most one arc from a node to another. One arc is the special return arc , and denotes the set of all other arcs. Each has a real capacity .
A flow is a nonnegative function on the arcs of with on and with inflow equal to outflow at every node, the return arc included. The value is the amount sent from to ; a maximum flow maximizes it.
Given a flow , the residual network has the same nodes, and is an arc of when with , or with . An augmenting path is a sequence of distinct nodes whose consecutive pairs are arcs of . Each step carries a number (residual capacity forward, flow backward, or their sum when both and lie in ); , and a step with is a bottleneck arc. Augmenting raises by 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 where is a flow and each arises from by augmenting along a path with fewest arcs. The distance is the least number of arcs of a directed path from to in , or .
For every network on nodes and every run of length with fewest-arc augmentations,
and if no augmenting path exists relative to , then is a maximum flow. The capacities are arbitrary positive reals, and the initial flow is arbitrary.
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.
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.
Nodes form a finite type V with decidable equality and = Fintype.card V counts all nodes, and included. The arc set A is a Finset (V × V) with no loops and without ; 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 " for every flow ", 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 . The explicit constants are stated as printed: in ℕ (the truncated subtraction is harmless since ) and 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 , , which the paper's own description of 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 ) 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 " 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.
Many problems in signal processing, statistics and machine learning minimise a sum of three convex terms: a smooth data-fit term and two nonsmooth regularisers or constraints, each of which is easy to handle on its own (through its proximal map) but not in combination. Examples are constrained sparse regression, matrix completion with a nuclear-norm penalty and box constraints, and support-vector machines with a norm penalty. Davis and Yin (Set-Valued Var. Anal. 25 (2017)) introduced a three-operator splitting scheme that evaluates each proximal map and the gradient of the smooth term once per iteration and reduces to Douglas–Rachford splitting (Lions and Mercier 1979) and forward–backward splitting as special cases. Section 3 of that paper gives the objective-error rates of the scheme on convex problems. This mission formalizes those rates for general convex problems.
Let be a real Hilbert space. The problem is
where are closed, proper, convex functions (lower semicontinuous, never , finite somewhere, with convex epigraph) and is convex and differentiable with -Lipschitz gradient , .
For the proximal map is the unique minimiser of . Algorithm 2 of the paper picks and and iterates, with relaxation ,
Equivalently for the three-operator map
If is a fixed point of , then minimises (3.1). The weighted ergodic iterate is
and is defined the same way from .
Let be a fixed point of , , and suppose is -Lipschitz continuous on the closed ball . Then there is a constant , independent of , with
The goal asserts the order and leaves the constant free, so it is not invalidated by a sharper constant.
The result. Theorem 3.1 gives the last iterate an objective error of . Theorem 3.2 shows that averaging with linearly increasing weights improves this to , the rate of the standard uniform ergodic average, while putting more weight on recent iterates. The paper notes that this matters when the iterates are sparse vectors or low-rank matrices and the average should stay close to them. The rates hold under a local Lipschitz condition on one of the two nonsmooth terms only, so may be the indicator function of a constraint set. They therefore cover the constrained applications of Section 4 of the paper.
Formalizing it. The results are proved in the paper. No machine-checked version of this scheme or its rates exists on the platform or, as far as is known, in Mathlib. A formalization produces a checked proof in an arbitrary real Hilbert space with extended-valued . It also produces infrastructure that Mathlib lacks: proximal maps characterised by minimisation, the prox-subgradient inclusion, Fejér monotonicity of an averaged-operator iteration, and a weighted Jensen inequality for extended-valued convex functions. All of these can be reused by other splitting and proximal-gradient missions. The formalization also checks the constants: the last display of the published proof of Theorem 3.2 drops a factor in front of the Lipschitz term, and the printed ball in both theorems is centred at where the proof needs .
The obvious argument sums the one-step inequality (3.2). That controls the objective at the two different points and , and only appears, never . Moving from one point to the other needs the Lipschitz hypothesis on , and so it needs every iterate, and every weighted average, to stay in the ball on which that hypothesis holds. For the weighted average there is a further obstacle: the cross term does not telescope under the weights . Controlling it requires the summability of the gradient differences (2.7), which is inherited from the averagedness analysis of Section 2 and not from convexity alone. Uniform averaging with the same argument does not give the weighted statement, and the weights must not be replaced.
InnerProductSpace ℝ H, CompleteSpace H), not .EReal. They are proper (never , somewhere ), lower semicontinuous, and have a convex epigraph in . is convex and differentiable, and Mathlib's gradient h is -Lipschitz.Welcome contributions: the prox–subgradient inclusion for EReal-valued convex functions, averagedness and Fejér monotonicity of (the companion mission on Section 2 treats the general operator case), a weighted Jensen inequality in EReal, and proofs of the milestones in the listed order.
Many problems in convex optimization, variational inequalities and signal processing reduce to a monotone inclusion: find a point at which the sum of several monotone operators contains . 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 () and forward–backward splitting () 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.
Let be a real Hilbert space. A set-valued operator is monotone if for all , , and maximal monotone if its graph is not properly contained in the graph of another monotone operator. Its domain is and the zero set of an operator is . A single-valued is -cocoercive () if for all .
Problem (1.1) is: given maximal monotone and -cocoercive , find
For the resolvent is the map with . The Davis–Yin operator (Eq. (1.2)) is
Algorithm 1 starts from and, for relaxation parameters , iterates
so that . A sequence converges weakly, , if for every .
Fix , , and with , where , and . If , there is with and
and if or is uniformly monotone on every nonempty bounded subset of its domain, or is demiregular at every zero of , then and converge strongly to a common point of .
In the order the proof uses them: Lemma 2.1 (the identities for one application of ), Lemma 2.2 (), Lemma 2.3 (inequality (2.1)), Proposition 2.1 ( is -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 ), Corollary 2.1 Part 4 (the residual rates and ), and Eqs. (2.6)–(2.7) (the per-step descent inequality and its summed form).
Theorem 2.1 is the basic convergence guarantee for three-operator splitting: it certifies that the computable sequences , , not only the auxiliary sequence , approach a solution of (1.1). In infinite dimensions this is the delicate part: for Douglas–Rachford splitting () weak convergence of the shadow sequence 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 , 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.
The fixed-point part is standard once is known to be averaged: Krasnosel'skiĭ–Mann theory and Opial's argument give . The obstacle is transferring this to . Resolvents are nonexpansive but not weakly continuous, so does not imply ; the naive argument fails at exactly this step. Identifying the weak cluster points of requires a closedness property of sums of maximal monotone operators under mixed weak and strong convergence, fed by the strong convergence of , 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.
NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace); a finite-dimensional space would identify weak and strong convergence and change the theorems.H → Set H; is single-valued H → H. The resolvents are not constructed: are maps satisfying the resolvent inclusion , which for maximal monotone operators determines them uniquely and exists by Minty's theorem.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.
Many objective functions in optimization are pointwise maxima: the worst case of a loss over an uncertainty set, the value of a minimax problem as a function of the outer variable, a penalty for a system of constraints, or the largest eigenvalue of a symmetric matrix. Such a function
is typically not differentiable even when every piece is smooth, because the maximizing jumps. Descent methods, optimality conditions and sensitivity analysis for these problems all need a substitute for the gradient of and a formula for its directional derivatives.
Danskin's theorem (Danskin 1966) answers this when exists and is continuous in and is compact: has one-sided directional derivatives , where is the set of maximizers. Convex analysis gives the analogue when each is convex (Rockafellar 1970). In Generalized gradients and applications (Clarke 1975) Frank Clarke introduced the generalized gradient of a locally Lipschitz function and proved, as his first application, a single theorem, Theorem (2.1), that contains both cases. The generalized gradient became the standard object of nonsmooth analysis (Clarke 1983), and Theorem (2.1) is the prototype of every "subdifferential of a max function" rule used in minimax optimization.
Work in with the Euclidean norm and inner product . A function is locally Lipschitz if for every bounded set there is with for . By Rademacher's theorem such is differentiable almost everywhere.
and the one-sided directional derivative is when the limit exists.
For the max function, is a nonempty sequentially compact topological space and . Write , , for the objects above applied to at . Let and . The hypotheses of Theorem (2.1) are:
Under (a)–(d):
The result. Theorem (2.1) computes the directional derivatives and the generalized gradient of a max function from those of its active pieces. It yields Danskin's theorem when is continuous, and the convex max rule when each is convex, and it applies to nonsmooth, nonconvex families satisfying (c), a property later called regularity (Clarke 1983, §2.3). In the same paper it is applied to the distance function to compute (Proposition (2.4), Corollary (2.5)), which then drives the characterization of flow-invariant sets in §4. Proposition (1.4) and Corollary (1.10), which the theorem rests on, are the duality between and used throughout nonsmooth optimization: Clarke stationarity, bundle methods and subgradient methods for weakly convex functions all state their results against them.
Formalizing it. The results are classical and proved; none of them, to the platform's knowledge, has a machine-checked proof. Mathlib has Rademacher's theorem, gradients and convex hulls, but no Clarke generalized gradient. This mission builds the first layer of nonsmooth analysis: the definitions of , , and upper semicontinuity of multifunctions, the support-function duality, and the max rule.
The obvious approach reads off a single active piece. It fails because the active set changes as , may be infinite, and need not converge; can be differentiable at points where no individual piece is known to be. Hypothesis (c) cannot be dropped: for a single point and on , has while , so conclusion (3) fails. Limits of maximizers exist only through the sequential compactness of together with (a), and limits of gradients only through the joint closed-graph condition (d) in ; continuity in for each fixed is not enough. Proposition (1.4), on which everything rests, is itself a measure-theoretic statement: it relates the upper limit of difference quotients over all nearby base points to gradients that exist only almost everywhere.
EuclideanSpace ℝ (Fin n), is inner ℝ ζ v, is Mathlib's gradient, and " exists" is DifferentiableAt ℝ f x.LipschitzOnBounded. Hypothesis (b) is ∀ B bounded, ∃ K, ∀ u, LipschitzOnWith K (g · u) B: the constant is uniform in .gradient is where is not differentiable.Filter.limsup in along ; this is a junk value for non-Lipschitz , so every statement using assumes the Lipschitz hypothesis. The one-sided derivative is a Tendsto along .IsGreatest, which asserts attainment. The max function is ⨆ u, g x u; is nonempty ([Nonempty U]) and SeqCompactSpace, and (a) is Mathlib's UpperSemicontinuous on . The paper uses implicitly; with conclusion (4) would be false.UpperHemicontinuous.sSup without attainment would make the statements trivial or false; these are ruled out as above.Contributions welcome: proofs of the milestones, in particular Proposition (1.4) and Corollary (1.10), which are reusable for every later nonsmooth-analysis mission; lemmas that is nonempty and compact; the equivalence of LipschitzOnBounded with Mathlib's LocallyLipschitz.
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 largest of a set of linear forms. Beale's motivation comes from the theory of games: "if the enemy has to choose out of a set of possible actions, and represents his average gain through using the th", then the defender wants to minimize the sum of the largest .
The same objective can be written as a linear program. One introduces a bound and requires every sum of forms to be at most . That formulation has constraints, which is unwieldy once and 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 largest components of a vector, the "top- sum", and times the conditional value-at-risk of an empirical distribution. Beale's paper is an early source for its optimality conditions.
There are real variables , indexed by in a finite set (possibly empty), and . Two linear forms in these variables are given,
together with further forms
For an integer the objective is
The sum of the largest of numbers is the largest total of any of them. Ties do not make it ambiguous.
The feasible region is fixed by a set of indices. The variables with and all the are free, and every other is restricted to . At the origin , all forms are equal to , so the origin is where fails to be differentiable. In Beale's algorithm the origin is the current basic solution: the measure how far the "borderline" forms sit from a chosen critical form, and collects the forms that are certainly among the largest.
Write and .
For , is minimized over the feasible region when all the and vanish if and only if
"Minimized" means a global minimum: at every feasible point.
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- 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:
Necessity, the "only if" direction, is the part the paper calls obvious: each descent rule changes 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 is not differentiable at the origin. Nonnegative derivatives along the coordinate axes do not control mixed directions in which several move by different amounts, which reorders the forms. Which forms are the largest then depends on the point, and the paper settles the configurations in which is among the largest by an informal appeal to the "essential symmetry" between and the other forms. A formal proof cannot leave that appeal informal: the forms are parametrised relative to (each is ), so the symmetry is a change of variables that has to be written down and shown to preserve (4.5).
z : Fin r → ℝ (any r, including ) and u : Fin s → ℝ. The paper's for is Lean's u f for . The coefficients form a structure Forms r s.Fin (s+1) → ℝ, with index for and index f.succ for . The free set is a Finset (Fin r), and is a natural number cast to wherever it multiplies a coefficient.sumLargest τ v is the maximum over -element subsets of (Finset.sup' over powersetCard). It is the junk for larger than the number of entries, a case no statement uses.Needed infrastructure:
sumLargest: its value at a constant family, at a family sorted by a monotone shift, and under adding a common constant;These lemmas are reusable for any top--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.
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.
Points of the plane are , with the inventory level and the logarithm of the price. The limiting process has drift and covariance matrix
so its generator is
Two curves bound the region where the process lives: the rejection boundary (below it, orders are rejected) and the idleness boundary (above it, production stops). For the region is
and its boundary splits into four pieces: , , , . Write for the inward unit normal on and for arc length. A reflection field on gives the direction in which the process is pushed back into . The basic adjoint relation (BAR) of the paper, equation (43), is
and the paper cites Harrison and Williams for the fact that the stationary distribution of the reflected process satisfies it. Proposition 2 introduces the eigen-decomposition ( a rotation whose rows are eigenvectors, diagonal), the whitening map and , and assumes that is normal to . The exponents are
For continuously differentiable with on , , and every function on ,
The boundary integral is written out on the four pieces, with equal to , , and respectively. The normalizing constant is left out because the relation is linear in .
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 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.
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 , 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 , are exactly where the terms in and of the boundary integral come from.
The second trap is the reflection field. The page describes the modification as substituting the inward unit normal for ; with the identity is false as soon as is not a multiple of the identity (on a random instance the residual is of order one). Only the conormal field , which is what the hypothesis of Proposition 2 selects, gives a true statement.
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 . Parameters satisfy , , ; is any real number, and (then ) 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 goal quantifies over every test function; restricting to functions supported inside 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 graphs, which is reusable for any planar PDE statement on such regions. Contributions of that lemma, and of the four milestones, are welcome.
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 , the distance of below its running maximum, is the drawdown of . Its first passage above a level is the time at which a drawdown of size first occurs. Avram, Kyprianou and Pistorius (AKP 2004) computed the joint Laplace transform of this passage time and of the overshoot in closed form, in terms of the scale functions of . 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 for every spectrally negative Lévy process of unbounded variation, or of bounded variation with absolutely continuous Lévy measure.
Let be a spectrally negative Lévy process on : it starts at , has independent and stationary increments, càdlàg paths, no positive jumps, and paths that are not monotone. Its Laplace exponent is , and "" means that is integrable. For such , the tilted exponent is .
The paper assumes throughout that has unbounded variation, or has bounded variation and a Lévy measure with .
For , is the largest root of . The -scale function is the unique function that vanishes on , is continuous on , and satisfies
For it is defined by the series , where and is convolution on . Further, . The functions and are the same objects built from instead of .
Under the process starts at with a prior maximum . Its running maximum is , and the reflected process is , which starts at . For ,
For and with , with and ,
Here may be negative, so may be negative, which is where the series extension of enters.
Items (13)–(22) are stated under the proof's restriction . The goal is not.
The identity gives, for every spectrally negative Lévy process, the law of the first drawdown of size and of its overshoot. With it is the Laplace transform of the drawdown time. With 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.
The natural first idea is to treat like and read off its exit from from the two-sided exit identities of Proposition 1. This works only until first returns to . Up to that time is a copy of . After it, is reflected at , it is not a Lévy process, and no two-sided exit problem of describes it. The whole content of the theorem is the constant of (13), the value of the functional for started at , where the reflection acts at every instant. A second difficulty is the range of . For the integrand is unbounded, because can jump far above . Its finiteness is part of the claim. So is the passage from the region , where every scale function in (12) comes from Definition 2, to all , where can be negative.
Time is (ℝ≥0). is a real process with . is encoded by the path , and by that path together with the prior maximum . Random times take values in WithTop ℝ≥0, with as "never". The functional and discount factors are set to where the time is infinite. Every stated expectation carries its integrability as part of the conclusion.
Readings of the paper's informal words:
The scale functions are defined from the exponent of the given . A formalization in which is an arbitrary function satisfying a Laplace-transform hypothesis is ruled out. So is one in which is defined as , 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.
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.
A seller offers a product during the season ; throughout this mission , so time is measured as a fraction of the season. Customers arrive as a Poisson process with rate . Customer has a base valuation drawn independently from a distribution with tail , and values the product at at time , where is the decline factor. The paper reparametrizes it as , the fraction of the base valuation left at the end of the season.
In the numerical study, is a Gamma law with mean and coefficient of variation (standard deviation over mean): shape and rate . The paper sets . For this is the exponential law with mean one, for .
A contingent two-price policy posts the premium price on , where is fixed, and a discount price from time on. A myopic customer arriving at buys at if his valuation is at least ; otherwise he waits and buys at if his valuation is then at least . Customers arriving at or after buy if their valuation is at least . The numbers of customers in these groups are Poisson with means
With unlimited inventory, the expected revenue of the policy is
and the expected revenue of a single price is (Eq. (9) of the paper). The optimal values are and .
Suppose , and (unlimited inventory), with and . Then
Both maxima are attained. The goal states the two optimal values; it does not fix the optimal prices.
Proposition 3 gives the relative benefit of contingent pricing over a single price, , as a function of the discount time alone. It increases in and is largest at , where it equals . 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 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.
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 inside , 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 is not concave on the region , so a stationary point is not automatically a global maximizer, and the boundary and unbounded directions have to be ruled out. Uniqueness of the maximizer, which the paper asserts, fails at and needs .
All declarations sit in the namespace SeasonalPricing.MyopicExp. Time, prices and rates are real numbers. The season is with and . Integrals are interval integrals. The valuation tail is gammaValuationTail μ c x = 1 - cdf (gammaMeasure (1/c^2) (1/(μ c^2))) x, used at . The hypothesis is decayRatio α 1 = 1 with .
Readings of the paper's informal words:
IsGreatest), not a supremum.The Gamma density printed on p. 349 has the exponent , a misprint for ; at the exponent is either way.
A trivializing formalization would state the goal on the reduced two-variable function, dropping the model: the goal here is about built from and the Gamma tail, and about built from Eq. (9). The platform's BuyingToBundle.monopolyRevenue (definition monopoly_pricing) is a related object, ; with and , equals 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.
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.
A seller holds units over a season split at a fixed time with . On the premium price applies. At time the seller observes the remaining inventory and charges the discount menu price , where for . Customer has a base valuation and valuation at time , with a common decline factor .
A customer arriving at either buys immediately at or waits until , when he requests a unit if the discounted price leaves him a nonnegative surplus. Waiting is uncertain in two ways: the remaining inventory is random, and when fewer units remain than customers request them, units are rationed at random. A belief is a probability mass function of on together with allocation probabilities , , where is the event that the customer is allocated a unit. It is determined by the other customers' strategies, which are arbitrary.
With , the expected surplus of waiting of a customer with current valuation is
The paper's purchase rule (p. 344): buy immediately iff the current surplus is nonnegative and at least .
Assume , and or . For every the equation
has a unique solution ; a customer arriving at buys immediately under the purchase rule if and only if ; and the threshold function is nondecreasing in .
Theorem 1 reduces a customer's strategy, a function of arrival time and valuation, to one threshold function on . The segment sizes 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 ; 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 () or imperfect availability, and the monotonicity of the threshold needs a nonnegative premium price. A formal and threshold are the starting point for formalizing the equilibrium and pricing results of the paper.
The mathematics is one-dimensional. The difficulty is in stating it exactly. is piecewise linear with a kink wherever 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 " is false when 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 rests on increasing in for fixed , which needs ; 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.
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 enters (2). The menu is p2 : ℕ → ℝ with required on only; never matters because . The belief does not depend on the arrival time, as in Eq. (4) of the paper. waitingSurplus is with written Real.exp (-(α * (T - t))); buysNow is the purchase rule, stated on the current valuation .
Readings of the paper's words:
∃!). The paper's "" includes only in the case excluded by the added hypothesis.MonotoneOn), since is constant on an initial interval whenever no menu price is reachable (p. 347).Added hypotheses, both named in the statements: or , the one hypothesis the paper's proof uses without stating it; and , the model's convention that prices are nonnegative. Only the branch of the threshold is stated: for the paper's is the model's rule for late customers. The belief enters through the explicit sum; a formalization with an unspecified monotone , or with 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 for with increments bounded by , , is reusable. Proofs of the milestones and the goal, in any order, are welcome.
In a two-person zero-sum game with objective randomization, whatever one player gains the other loses: the value 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 and player 2 more than 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).
A game has a finite set of players, a finite set of pure strategies for each player, a finite set of outcomes and an outcome function from onto . Player has a utility ; write for .
A randomizing structure consists of a set of states of the world with a -field of events, a sub--field for each player (the events regarding which is informed), and a probability measure on for each player (the subjective probability of ). A strategy of is a map whose level sets lie in . For a profile of strategies, player 's payoff is computed under his own beliefs:
An event is objective if all coincide, and subjective otherwise. It is -secret if and every other player regards as independent of every event in the -field generated by the , . It is public if it lies in every . A measure is non-atomic on a -field if every event of of positive measure contains an event of of strictly smaller positive measure; a roulette is a sub--field of on which every is non-atomic, and a public roulette is a roulette of public events. Throughout, Assumption II holds: every player has a -field of -secret events on which every is non-atomic.
The game is two-person zero-sum if and for all . Its value is player 1's payoff at a Nash equilibrium of the classical mixed extension; by the minimax theorem all such equilibria give the payoff pair .
Let be a two-person zero-sum game with value , and assume
Then there is a pair of strategies with
The pair is not an equilibrium: it is an agreement that each player, by his own beliefs, strictly prefers to playing the game.
a special case of the goal in which the players share both the subjective event and the correlating device.
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 and ) 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.
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 , but the lemma asks for one event with prescribed values under measures and further measures simultaneously; this is the range of a vector measure, not of a scalar one.
0, 1 : Fin 2 (the paper's 1, 2). S 0, S 1, X are finite types and g is surjective.mΩ, an explicit parameter of RandomizingStructure; are σ-fields below it, and each is a probability measure on . Probabilities are ℝ≥0∞-valued; "probability " is ENNReal.ofReal α with .NoAtoms, which would trivialize the roulette hypotheses.IsValue u g v requires for a Nash equilibrium of the mixed extension (AGT.IsMixedNash from the published definition agt_games). A free would make the goal false. The minimax theorem is the published AGT.zero_sum_minimax.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 for strategies with finitely many values. Lyapunov's theorem is reusable far beyond this mission. Contributions of any milestone are welcome.
A sorting network is a sorting procedure whose sequence of comparisons is fixed in advance, independently of the data. Its depth, the number of rounds of simultaneous comparisons on disjoint pairs, is the parallel running time. Sorting networks are used in parallel and hardware sorting, in switching networks, and in cryptography, where a data-independent (oblivious) sequence of operations is required. How small the depth can be as a function of the number of inputs is a basic question of parallel computation.
Timeline:
There are registers holding elements of a linearly ordered set. An elementary step (a comparator) with compares the contents of and and exchanges them if the content of is larger. Afterwards holds the minimum and the maximum of the two, and every other register is unchanged. A parallel step is a set of comparators in which no register occurs twice, so it has at most comparators. A comparator network is a finite sequence of parallel steps, fixed before the input is seen. Its depth is the number of parallel steps and its size the total number of comparators. sorts if for every input the output satisfies .
The construction runs on the tree of finite - sequences, whose levels are ordered lexicographically. A chain on level assigns to every node of that level a set of registers, with the sets pairwise disjoint and of a common size . A ⟨k, ε⟩ expander on ⟨A, B⟩, for disjoint register sets and , is a bipartite graph between and of maximum degree in which every nonempty has more than neighbours, and symmetrically for . The Lean development uses the names ComparatorNetwork, compareExchange, IsChain, chainN, IsExpander, IsLowerSection for these objects.
The constant is absolute and is not fixed. Any explicit value would be invalidated by the next improvement, and the paper gives none.
The result. The AKS theorem settles the asymptotic depth of sorting networks at and their size at . It gives an -time sorting algorithm with processors that performs only data-independent comparisons. It is the standard reference point for oblivious sorting in parallel algorithms, circuit complexity (sorting is in via comparators) and oblivious RAM constructions. Lemma 4, the ε-halver property of expander comparisons, is the component that later constructions (Paterson) reuse.
Formalizing it. The theorem has been proved since 1983. No Lean proof of the AKS theorem is known. Mathlib has no expander graphs in the ⟨k, ε⟩ sense and no sorting networks. The mission asks for a formal proof of the headline theorem by any route (the AKS construction or Paterson's variant), and for formal proofs of the paper's verified lemmas as reusable components. The expander lemma needs either an explicit family (Margulis; Gabber–Galil) or a probabilistic existence argument, both substantial on their own.
Every elementary argument stalls at depth : recursive merging needs merge rounds, and merging two sorted lists by a comparator network needs depth . A depth of therefore cannot come from exact merging. It must come from constant-depth approximate operations (ε-halvers, which require bounded-degree expanders) combined with a mechanism that corrects the errors they leave. In the paper this mechanism is a movement of registers up and down a binary tree, controlled by a family of constants chosen in a fixed order ("", p. 2). The accounting that shows the misplaced elements decay geometrically is the hard part. Several intermediate lemmas of the paper are false as printed, so the paper's text is not a checklist to transcribe.
Conventions committed to in Lean:
Fin n, and contents lie in an arbitrary linearly ordered type. A network is a List of layers, each a List (Fin n × Fin n) of comparators with distinct endpoints, and no register occurs twice in a layer. A comparator puts the minimum into , and both directions and are allowed. Sorts means the output is monotone for every linearly ordered type and every input, not only for permutations.Real.logb 2 n, and the goal is stated for . The constant is quantified before .Fin (2^i), with numeric order equal to lexicographic order. A chain is a Fin (2^i) → Finset R.Trivializing formalizations are ruled out. The goal is not "for every there is a network of depth " with the constant chosen after , which is true for trivial reasons. Layers without the disjointness condition would let a single layer contain a whole insertion sort. A bound on the number of comparisons alone, with unbounded depth, is a different and much older result; the goal states both the depth and the size bound.
The mission states the AKS theorem and the paper's lemmas that are correct as stated. It does not formalize the AKS algorithm itself (, , the operations CH1–CH4, IMP) or its intermediate Lemmas 5–11 and 13–15. Those depend on unspecified constants constrained only by "sufficiently small" chains, and Lemmas 5, 10 and 12(b) are false as printed. A solver may of course define the algorithm, with pinned constants, as part of a proof.
Contributions welcome: a library of comparator networks (composition, the 0-1 principle, depth of Batcher's networks), existence of bounded-degree bipartite expanders, the ε-halver lemma, and any complete proof of the goal. The network and expander definitions are independent of this paper and reusable.
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.
Two gold mines, Anaconda () and Bonanza (), hold amounts and of gold. A single machine can be used in either mine. A use in Anaconda succeeds with probability : it then mines a fraction of the gold currently in Anaconda and the machine stays undamaged. With probability it mines nothing and the machine is destroyed. Bonanza behaves the same way with probability and fraction . 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 : the mine for use number , applied if uses succeeded. With , the numbers of - and -uses among the first , use collects if and if , and does so with probability (, ). The expected return is
and Bellman's (8.1) defines the optimal return
In Lean these are expectedReturn p q r s σ x y and optimalReturn p q r s x y in the namespace BellmanTheoryDP.GoldMining.
Write and for the two branches of (8.2). For and :
The paper prints the rule with and in the denominators:
a. For , choose A, b. For , choose B, c. For , 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, (resp. ), not . As printed the rule is false: with , , , , , the printed indices are , but . The mission's goal is the corrected rule, the one the paper describes in words.
"Using this prescription, may be computed recurrently": the choice sequence generated by applying the corrected rule to the current amounts at every use satisfies .
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.
The equation (8.2) looks immediate, and the paper calls it "easily seen". The informal argument treats as the value of an optimal policy, but 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 and , 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.
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: is the supremum over all sequences.tsum and a real iSup. For the parameter ranges above the terms are nonnegative, the partial sums are bounded by , 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.AllocationIndices.two_discount_index_policy_optimal (Gittins et al., Theorem 3.4) concerns Markov bandits whose rewards are discounted by at global time ; 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.