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.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
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?
Many convex problems met in practice — least squares with a rank-deficient matrix, dual problems of linearly constrained programs, with a strongly convex and a wide matrix — are not strongly convex: their optimal set is a whole affine piece rather than a point. The classical linear-rate theory of first order methods assumes strong convexity, yet these methods are observed to converge linearly on such problems as well.
Necoara, Nesterov and Glineur (arXiv:1504.06298v4, 2016; Math. Program. 175, 2019) introduce a hierarchy of relaxations of strong convexity, all measured relative to the projection onto the optimal set, and prove linear convergence of the projected gradient method, the fast gradient method and feasible descent methods under them. This mission formalizes the result on the fast gradient method (FGM) for the first and strongest relaxation, quasi-strong convexity: an accelerated linear rate, with in place of , under the condition that all extrapolated points share one projection onto the optimal set.
Nesterov's estimate-sequence technique (Nesterov, Introductory Lectures on Convex Optimization, 2004, §2.2) gives the rate for strongly convex functions. The paper shows that the same argument survives when strong convexity is replaced by the quasi-strong inequality at the projection, provided the projections of the points do not move.
Work in with the Euclidean inner product and norm . Problem (P) is
with closed and convex and convex and differentiable with -Lipschitz gradient: . The optimal set is assumed nonempty. For a closed set , denotes a nearest point of in .
is quasi-strongly convex with constant (Definition 1, inequality (10)) if, with ,
The condition number is .
The fast gradient method (FGM) starts from and iterates, for ,
The gradient mapping at is with .
The analysis uses the estimate functions of Lemma 1: for , , , and
If all iterates of (FGM) have the same nearest point in , then
The theorem gives the accelerated linear rate for a class strictly larger than the strongly convex functions. By Remark 1 (p. 27), on an unconstrained problem (FGM) keeps in , so the projection onto never moves; with Theorem 8 of the paper (quasi-strong convexity of for strongly convex smooth ) this covers such problems, and Section 6.1 applies it to consistent linear systems , where is not strongly convex when has a nontrivial kernel.
The result is proved in the paper; nothing here is open mathematically. It has no machine-checked proof: the Nesterov-method items already on the platform concern strongly convex or sublinear settings and do not cover quasi-strong convexity or the same-projection condition. A complete development produces a reusable formal estimate-sequence argument, the gradient-mapping inequality (29) for points outside the feasible set, and the quadratic-growth consequence of (10).
The estimate-sequence argument needs a quadratic lower model of at the point where it is evaluated. Under strong convexity this lower model holds between any two points; under quasi-strong convexity it holds only between a point and its projection onto . Lemma 1 evaluates at a single point for every , so it needs the projections of all to coincide; the obvious attempt to run the strongly convex proof with changing from step to step fails at the induction step (57). This is why the same-projection hypothesis is part of the theorem rather than an artifact.
The second difficulty is bookkeeping: condition (58) concerns the minimum of the recursively defined quadratics , which has no closed form in the statement, and it must be matched against the momentum step of (FGM); this is the only place where the specific value of enters.
EuclideanSpace ℝ (Fin n). The projection is the predicate IsNearest S u p ( minimises ), never a choice function; FGM runs are sequences satisfying this predicate at every step, with and 0-based indices (the page's "for " is a slip).QuasiStrongEverywhere). For , the case of Remark 1, these are exactly the paper's hypotheses.Many planning problems are solved in stages. A decision is taken, uncertainty is revealed, and the next decision reacts to it. Facility location, capacity expansion and network design all fit this pattern. In a growing class of such problems, the distribution of the uncertainty depends on the decision: opening a facility changes the demand it attracts, and a maintenance decision changes the failure rates that follow. Stochastic programs with decision-dependent uncertainty go back to Jonsbråten, Wets and Woodruff (1998) and Goel and Grossmann (2006).
When the distribution is not known exactly, distributionally robust optimization (DRO) optimizes against the worst distribution in an ambiguity set of plausible ones. Moment-based ambiguity sets, which are defined by constraints on the mean and covariance, are one of the standard choices (Delage and Ye, 2010). Luo and Mehrotra (2020) studied single-stage DRO in which such moment sets depend on the decision. Yu and Shen (2020) carry this into the multistage mixed-integer setting. Their goal is to rewrite each stage's min–max Bellman equation as one minimization, so that the stagewise decomposition algorithm SDDiP (Zou, Ahmed and Sun, 2019) applies.
This mission formalizes their reformulation for the Type 2 ambiguity set, which matches a decision-dependent mean and covariance exactly.
Fix a stage . The decision at stage is a pair : a binary state , passed to the next stage, and a stage variable . The pair must lie in a stage feasible set and costs .
The next-stage random vector takes one of finitely many values . This support is fixed (Assumption 3), and only the probabilities are uncertain. The value of being in state when scenario occurs is .
The decision determines a mean and a covariance matrix . The Type 2 ambiguity set is the set of probability vectors that match them exactly:
The Bellman equation (2) of stage is
Throughout, is the Frobenius inner product.
If is nonempty for every feasible , then
The left side is a minimum exactly when the right side is, and the two values agree.
The theorem turns a min–max problem into a single minimization. Under the paper's affine model (12) for and , and with McCormick envelopes for the products of binary states and continuous duals, that minimization becomes a mixed-integer linear program. SDDiP can then solve the multistage model stage by stage, with valid cuts. The Type 2 set is the paper's middle case. It captures correlations between the components of , which the separate moment bounds of the Type 1 set (Theorem 1) cannot, and it still has an LP dual. The Type 3 set of Theorem 3 instead leads to a semidefinite program.
The result is proved in the paper: Appendix C gives a short argument by linear-programming duality. It has not been formalized. A formal proof pins down details the printed proof leaves implicit:
It also yields a reusable, machine-checked instance of LP duality for moment-matching problems on a finite support.
There are two steps. The first is linear-programming strong duality for the inner problem in matrix-valued form. Its constraints are a scalar equation, a vector equation in and a matrix equation in , so the dual variables are a scalar, a vector and a matrix, paired through dot and Frobenius products. Turning this into a standard-form LP to which a library duality theorem applies takes bookkeeping. The second step is the exchange of the outer minimum with the dual minimum. Here attainment matters: the inner maximum must be attained at every feasible , and the stated equality must hold both when the outer minimum exists and when it does not. Weak duality alone gives only one inequality. The naive argument "dualize and combine" also hides the fact that, without , the dual constraints would have to be equalities.
Fin I → ℝ, stage variables are Fin I → Fin J → ℝ, the support is ξ : Fin K → Fin J → ℝ, and the next-stage values are an arbitrary function Qn x k. The theorem uses nothing about the recursion that defines . The covariance map is named Sig.IsLeast, IsGreatest), never sInf/sSup. The goal states that is the least stage value if and only if is the least value of (11). An empty stage set, or an empty ambiguity set, cannot make the statement hold by default values. The ambiguity set is never empty at a feasible state, because that is the theorem's hypothesis, and an empty stage set makes both sides false.First order methods (projected gradient, fast gradient) converge only sublinearly on general smooth convex problems, at rates and in function value. Linear convergence is classically proved under strong convexity, which fails for many problems arising in practice: least squares with a rank-deficient matrix, dual problems of linearly constrained programs, and compositions of a strongly convex with a singular linear map. For such problems the optimal set is not a single point, yet projected gradient methods are still observed to converge linearly.
Necoara, Nesterov and Glineur (arXiv:1504.06298, later Math. Program. 175 (2019)) introduce a hierarchy of relaxations of strong convexity, each obtained by evaluating a strong convexity inequality only at the projection of a point onto the optimal set, and show that first order methods converge linearly on each class. Two of these relaxations are the subject of this mission: quadratic functional growth and the global error bound stated with the gradient mapping. Error bounds of this kind go back to Luo and Tseng (Ann. Oper. Res. 46 (1993)) and Tseng's analysis of feasible descent methods; quadratic growth conditions appear in Anitescu and in Drusvyatskiy–Lewis (Math. Oper. Res. 43 (2018)).
Work in with the Euclidean inner product and norm . Problem (P) is
with closed and convex and convex on , differentiable on , with Lipschitz continuous gradient of constant on : for all . The optimal set is assumed nonempty.
For a set and a point , denotes a point of nearest to ; for nonempty closed convex it exists and is unique. Write . The projected gradient step from is , and the gradient mapping is
When , .
The condition number is . In Lean these are QuadFunGrowth X f κ and ErrorBound X f Lf κ, with written Lf • (x - xp).
Quadratic functional growth with constant implies the global error bound with constant :
In class notation, .
The converse direction, also included as a draft theorem: the error bound with implies quadratic functional growth with constant .
Theorems 6 and 7 together show that, for convex functions with Lipschitz gradient on a closed convex set, quadratic functional growth and the gradient-mapping error bound define the same class of functions up to a change of constant depending only on . A linear convergence proof for projected gradient methods under one condition therefore transfers to the other, and the paper uses this to place the error-bound class inside its hierarchy of relaxations of strong convexity. The explicit constant matters downstream: rates of the form inherit it.
The results are proved in the paper. No machine-checked proof of Theorems 6–7 is known to exist. Related statements formalized elsewhere on the platform concern the unconstrained case (Karimi–Nutini–Schmidt, where replaces ) or the proximal-gradient error bound on sublevel sets (Drusvyatskiy–Lewis), with different constants. A complete development here yields a reusable library of projected-gradient facts on a general closed convex set: the descent inequality, the gradient-mapping inequality and the existence and characterization of projections.
The obvious approach applies (22) at and tries to bound by , as in the unconstrained case where and convexity gives . On a constrained set this fails: is not a subgradient of at , and the available inequality for the gradient mapping, (29), controls only through the value at a different point. Relating the distance to at that point to the distance at , without losing the exact constant , is the central difficulty.
At the Lean level, the descent inequality (2) has to be derived on a convex set from a Lipschitz condition assumed only on , and the variational characterization of the Euclidean projection has to be connected to the nearest-point predicate.
EuclideanSpace ℝ (Fin n). is a real function on all of , convex on (ConvexOn ℝ X f), differentiable at every point of , with = gradient f; its values off never enter.IsNearest), not choice functions; is the predicate IsPGStep. Every statement quantifies over all points satisfying them. Nearest points in nonempty closed convex sets exist, so these quantifiers are not vacuous.A trivializing formalization is ruled out: the error bound uses the gradient mapping and not , the projections are not defined by choice, is nonempty, and no junk gradient value off the differentiability set is used.
Needed infrastructure: the descent lemma on a convex set, the obtuse-angle characterization of the projection onto a closed convex set, existence of nearest points (Mathlib's exists_norm_eq_iInf_of_complete_convex), and closedness and convexity of . These are reusable well beyond this mission; proofs of the milestones and of Theorem 6 are welcome independently.
Linear convergence of gradient-type methods is classically proved under strong convexity. Many problems that arise in practice are not strongly convex: dual formulations of linearly constrained convex problems, least-squares and logistic-type regression with rank-deficient data matrices, convex quadratic programs, and routing problems in data networks all have objectives of the form , where is strongly convex and smooth but the matrix has a nontrivial kernel. Such an is constant along , so it is not strongly convex, and its set of minimizers need not be a single point.
Necoara, Nesterov and Glineur (arXiv:1504.06298v4, published in Math. Program. 175 (2019)) introduce a chain of relaxations of strong convexity: quasi-strong convexity, quadratic gradient growth and quadratic functional growth. They show that projected and fast gradient methods still converge linearly under them. Section 4 of the paper supplies the main examples: compositions , possibly with a linear term and polyhedral constraints. This mission formalizes those examples. The tool behind them is the error bound of Hoffman (1952) for systems of linear inequalities; its use for linear convergence goes back to Luo and Tseng (1993) and Wang and Lin (2014).
Work in with the Euclidean inner product and norm . For a set and a function , the optimal set is and is the optimal value. A nearest point of a set to is a point of minimizing over .
The data are:
The objective is , or in the extensions. The function has Lipschitz gradient with constant on if for . It is quasi-strongly convex with constant if, for every and ,
The class collects the convex functions with -Lipschitz gradient on satisfying this inequality with . The classes (quadratic gradient growth, ) and (quadratic functional growth, ) are defined the same way.
A Hoffman constant for the polyhedron is a number with
where is the componentwise positive part.
If is optimal for and is a Hoffman constant for , then
Theorem 8 makes the linear convergence results of the paper apply to the whole family over polyhedra. That family covers the duals of linearly constrained strongly convex problems and regression with arbitrary design matrices. The rate is explicit in , , and the Hoffman constant. Theorems 9 and 10 extend the picture to a linear term, at the cost of moving to weaker classes. Example 1 shows that the sublevel restriction in Theorem 10 is needed.
All of these results are proved in the paper. None of them has a machine-checked proof that this mission is aware of. A formal development would produce a Lean proof of the class membership, a formal chain-rule computation of the gradient of , and the strict-convexity argument that is constant on the optimal set. These pieces are reusable wherever a composite objective with a rank-deficient linear map appears.
The obvious route, strong convexity of , fails as soon as . Two separate facts have to replace it. The first is that the minimizers of a strongly convex function composed with share the image point , so the optimal set is itself a polyhedron. The second is that the distance to that polyhedron is controlled linearly by the residual on feasible points, which is exactly a Hoffman error bound. Neither follows from local information at a single minimizer. In Theorem 10 the linear term destroys the first fact's simplicity: the value must also be controlled, and that is possible only on bounded sublevel sets.
is EuclideanSpace ℝ (Fin n). and are continuous linear maps, so is the operator norm, which is the spectral norm of the page; it is never the Frobenius norm. Strong convexity is Mathlib's StrongConvexOn Set.univ σg g, which is (5) on all of . The page's "-Lipschitz gradient on " is read on , the domain of . The gradient of the composition is always gradient (fun z => g (A z)), and the identity is a proof step, not part of any statement. is the value at a nearest point of , which is exact because that point is optimal.
Standing assumptions of p. 3: the feasible set is closed and convex (automatic for a polyhedron), the optimal set is nonempty (a named optimal point is a hypothesis), and has Lipschitz gradient (a conclusion here). The "simple" set and "closed" function add no mathematical content and are dropped. The Hoffman constant is a hypothesis, because the page cites its existence (Hoffman 1952) rather than proving it. The hypothesis is the Hoffman inequality for the specific polyhedron , not for every right-hand side.
Trivializing formalizations are ruled out. The projection is a predicate (IsNearest), never a choice function. The optimal set is nonempty by hypothesis. is differentiable everywhere, so no gradient takes a junk value. A sorry-free sanity file shows that the hypotheses of Theorems 8–10 are jointly satisfiable ( on , , ).
A complete development needs the chain rule for gradients through a continuous linear map and its adjoint, first-order characterizations of strong convexity, and optimality conditions for convex differentiable functions on convex sets. Contributions of these as reusable lemmas are welcome, as are proofs of the companion theorems.
Strategic planning of an open pit mine decides, over a horizon of 20 to 50 years, which parts of an ore body are excavated, when, and where the excavated material is sent. A deposit is discretized into blocks, often millions of them, and the decisions are constrained by wall-slope precedences between blocks, by mining and processing capacities, and by blending and other operational rules. The resulting mixed-integer programs are far beyond the reach of general-purpose solvers, so practitioners and researchers rely heavily on preprocessing: rules that provably remove variables before the model is solved.
The oldest such rule is the ultimate pit limit. Lerchs and Grossmann (1965) showed that the most profitable pit, ignoring time and capacities, is a maximum-weight closure of the precedence graph and can be computed by a graph algorithm. Caccetta and Hill (2003) used this limit to eliminate blocks in the capacitated pit problem (C-PIT), where each block has a predefined destination. Rivera Letelier, Espinoza, Goycoolea, Moreno and Muñoz (Operations Research, 2020) extend that result to the general precedence-constrained production scheduling problem with clusters (PCPSP-C) of Bienstock and Zuckerberg (2009): multiple destinations per block, clusters of blocks extracted together, arbitrary nonnegative side constraints, and either full or partial integrality. This mission formalizes that extension, Theorem 1 of the article, together with the surrounding claims of §2 and §4. The source is the published Operations Research article; all page numbers are journal pages.
A PCPSP-C instance consists of a finite set of blocks , destinations , and periods . Sending block to destination is worth (possibly negative); in period it is worth for a discount rate . A relation means that must be extracted no later than . The blocks are partitioned into clusters , with the cluster of ; clusters inherit precedence ( if some block of precedes some block of ), this relation is assumed to be a partial order, and is the set of immediate precedences: when immediately precedes . Blocks have weights , and a matrix inequality collects all side constraints (capacities and others).
The variables are , the fraction of cluster extracted in period , and , the fraction of block sent to in period . The PCPSP-C maximizes subject to
and to an integrality condition: full () or partial (once a cluster has started, each of its immediate predecessors must be completely extracted). An optimal solution is minimal if no other optimal solution lies componentwise below it.
With , the ultimate pit limit problem U-PIT is the linear program
The pit limit of a vector is ; for a PCPSP-C solution it is the pit limit of .
If and , then for either integrality condition, every minimal optimal solution of the PCPSP-C and the minimal optimal solution of U-PIT satisfy
Theorem 1 turns an expensive mixed-integer program into a smaller one using a single maximum-closure computation that ignores time and resources: every cluster outside can be deleted from the instance. In the article's computational study this preprocessing is part of the pipeline that solves industrial instances to near-optimality. The result covers the partial-integrality models used in commercial mine-planning software, not only the full-integrality model of the earlier literature.
The article's proof of Theorem 1 is in an online e-companion; the companion claims of §2 and §4 are stated in the text with brief or cited justifications (claim (b) is attributed to the maximum closure literature, Hochbaum 2008). None of these results has a machine-checked proof. The mission produces a formal model of the PCPSP-C that the sibling missions of this series (clique, variable-right-hand-side and hourglass cuts) share, and a verified justification of a preprocessing step in practical use.
The obvious argument, "a cluster outside the ultimate pit has nonpositive value, so drop it", fails on two counts. First, value is not additive over clusters: U-PIT optimality only says that the clusters outside that can be added to it as a closed set have nonpositive total value, not that each cluster outside it does. Second, the PCPSP-C is a multi-period problem in which a cluster may be extracted in fractions over several periods with different discount factors, and with side constraints that may forbid extracting it at all. The statement therefore depends on the discount factors being decreasing in time, on the side constraints being monotone (), and on minimality of the PCPSP-C solution, without which an optimal solution may also extract clusters of zero value outside the limit.
Everything lives in the namespace OpenPitMIP.UltPit. An instance is a structure over finite types of blocks, destinations and clusters, with periods Fin T (index is period , so the discount factor is ). Block precedence is primitive; cluster precedence and the arc set (the transitive reduction) are derived from it, and the precedence rows (4) and (13) range over only. The standing assumptions of §2.1 are bundled in one hypothesis: the clusters partition the blocks (every cluster is nonempty), cluster precedence is a strict partial order, , and . The integrality condition is a parameter ranging over {full, partial}, and Theorem 1 is stated for both. Optimality and minimality are taken over the whole feasible set, with the componentwise order on the pair . At least one destination is assumed, so that exists. U-PIT is the linear program over , not a binary closure problem.
The theorem is not trivialized: no minimal optimal solution is assumed to exist beyond what the hypotheses give, the discounting is part of the model (with arbitrary period values the theorem is false), and the hypotheses are jointly satisfiable (one block, one cluster, one period, , with the zero solution minimal optimal in both problems).
Contributions welcome: proofs of the milestones, a proof of Theorem 1, and reusable lemmas on closure polytopes (lattice structure, binary minimal optima), which are of interest beyond mining.
A chance-constrained program minimizes a cost over a closed set subject to a constraint that must hold with high probability rather than surely:
where is a random vector, collects the uncertain constraints, and is the tolerated risk. Such models are used in power-system dispatch, portfolio selection, and supply-chain and process design, wherever a constraint may be violated in rare scenarios at a controlled rate.
The probability is rarely computable, so in practice it is replaced by an estimate from an i.i.d. sample . The empirical frequency is a step function of and yields a mixed-integer program. Peña-Ordieres, Luedtke and Wächter (arXiv:1905.07377v2; SIAM J. Optim. 30(3), 2020) replace the indicator by a smooth approximation, which turns the sample problem into a smooth nonlinear program that standard solvers can handle. The question this mission addresses is whether a point accepted by the smoothed sample problem is actually feasible for the true chance constraint, and with what probability.
Timeline. Luedtke and Ahmed (SIAM J. Optim. 19 (2008)) proved finite-sample feasibility guarantees for the empirical (non-smooth) sample approximation, first for finite and then, under a Lipschitz condition on , for bounded (their Theorem 10). Peña-Ordieres, Luedtke and Wächter (2020) extended these guarantees to the smoothed approximation (Theorems 3.8, 3.11 and 3.13 of the preprint).
Let and let be admissible: strictly decreasing, symmetric in the sense , and such that the smoothed indicator
is differentiable on . The paper's concrete choice is a quartic-kernel polynomial (its (2.6)).
For a decision and a level , define
The true feasible set is , and the shifted sample feasible set with shift and sample risk level is
Throughout, has a continuous distribution for each (Assumption 3.1). The margin of a point is ; Assumption 3.7 asks that and .
Suppose is bounded with sup-norm diameter , that for all with probability one (Assumption 3.12), and that Assumption 3.7 holds with and . Then for every ,
The result. Theorem 3.13 gives an explicit, non-asymptotic sample size under which every point accepted by the smoothed sample problem (with a small shift and a slightly tightened risk level ) is feasible for the original chance constraint, uniformly over an infinite decision set. Solving the smooth approximation therefore yields certifiably feasible solutions with a quantified failure probability, the bound depending on the dimension only through the covering number . Corollary 3.9 adds that, under a monotone density near zero, the unshifted smoothed approximation is conservative.
Formalizing it. The results are proved in the paper; none is formalized anywhere to our knowledge. A formal development would produce a machine-checked one-sided Hoeffding bound for averages of bounded functions of an i.i.d. sample, a union bound over a finite candidate set, and a sup-norm covering lemma, assembled into a uniform feasibility guarantee. These ingredients are reused across the sample-average-approximation literature.
The obvious argument is a union bound over , which fails for infinite : the event involves uncountably many points, and is not even obviously measurable. Discretizing by a sup-norm grid is not enough on its own either: a grid point may be infeasible while nearby points are feasible, and the true cdf need not be continuous in . The paper's device is to discretize simultaneously in and in the value of , which requires covering each level slice separately and then transferring sample feasibility from a point to its representative, at the price of the shift and the level change . Keeping the constants exactly as printed, with slices and points per slice, is part of the task.
Fin n → ℝ, whose Mathlib norm is the sup norm used in Assumption 3.12 and Theorem 3.13. is closed (the paper's standing hypothesis).ProbabilityTheory.measure_sum_ge_le_of_iIndepFun with hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero); and Corollary 3.10, whose printed exponent does not follow from its proof.Contributions welcome: proofs of any milestone, in particular the sup-norm covering lemma and the Hoeffding step, which are reusable beyond this mission.
First-order methods (projected gradient, fast gradient, feasible descent) converge linearly on smooth strongly convex problems, but many problems met in practice are not strongly convex: least squares with a rank-deficient matrix, the dual of a linearly constrained problem, or with strongly convex and singular. Such problems have a whole set of minimisers, and strong convexity, which forces a unique minimiser, fails. Necoara, Nesterov and Glineur (arXiv:1504.06298; Math. Program. 175 (2019)) introduce a family of conditions that relax strong convexity by testing it only against the projection onto the optimal set, and prove that the classical first-order methods still converge linearly under them.
Related unconstrained conditions predate the paper: restricted strong convexity for (Zhang and Cheng, Optim. Lett. 2015, the paper's reference [16]), and the error bounds of Luo and Tseng (1993). Karimi, Nutini and Schmidt (arXiv:1608.04636, 2016) compared similar unconstrained conditions with the Polyak–Łojasiewicz inequality. The constrained hierarchy treated here, with one constant along the whole chain, is the first section of the Necoara–Nesterov–Glineur paper and the basis of its convergence results.
This mission formalizes that hierarchy: Theorem 4 of the paper (arXiv v4, p. 9) and the results it is assembled from.
Let be a closed convex set, with the Euclidean inner product and norm . Let be a convex function on , differentiable at every point of , with gradient Lipschitz on with constant :
The optimal set is assumed nonempty, and is the optimal value. For , denotes the projection of onto : the point of nearest to .
For a constant the paper considers five inequalities, for all :
The classes , , , , are the convex functions satisfying (1) and, respectively, (7), (10), (17), (13), (22). In Lean these are the predicates StrongIneq, QuasiStrong, QuadGradGrowth, QuadUnder and QuadFunGrowth of NecoaraNG.Chain.Setting, over optSet X f and the nearest-point predicate IsNearest.
With the same constant at every step,
that is
The goal is the conjunction of the four implications under the standing assumptions.
A companion item states the remark on p. 7: for convex , (10) alone or (13) alone gives (17) with constant .
The chain gives the hierarchy that the paper's convergence theorems are stated for: the projected gradient method converges linearly on and, in distance to , exactly on ; the fast gradient method keeps its accelerated rate on ; and with strongly convex is in on a polyhedron. Each such result transfers down the chain once the inclusions are known, and the fact that one survives every link is what keeps the rates' constants explicit.
All the statements are proved in the paper. None of them is formalized: the platform has unconstrained analogues (the Karimi–Nutini–Schmidt chain, with an existential constant and no feasible set), but no constrained statement and no statement with a fixed constant. A formal proof would also check the projection-invariance step that the paper uses without comment.
The links and are one-line substitutions. The substance is in Theorems 1 and 3, and specifically in the constant: combining (10) or (13) with the convexity inequality at a single pair of points gives (17) only with constant (the companion item), and the same loss of a factor 2 appears in a direct derivation of (13) from (10). Keeping the full constant is what makes (23) a chain of inclusions with one index, and it is where the geometry of the optimal set enters: the conditions are tested only against the projection , which moves with . Convexity of cannot be dropped: (10) alone does not even imply convexity (p. 5).
EuclideanSpace ℝ (Fin n); is Mathlib's gradient f. The function is defined on all of , with differentiability assumed at every point of ; "continuously differentiable" on follows from (1).ConvexOn ℝ X f), (1) with , a minimiser , . "Simple" (cheap projection) and "closed" for carry no mathematical content here and are dropped.IsNearest (optSet X f) x xbar; each condition is required for every nearest point. is written , which is exact because .StrongConvexOn.The column-subset selection problem (CSSP) asks for columns of a real matrix whose span approximates all of as well as possible in squared Frobenius norm. It is a basic primitive of low-rank approximation, feature selection and numerical linear algebra, studied both for its exact complexity and for approximation algorithms (see Boutsidis, Drineas and Magdon-Ismail, doi:10.1137/12086755X, cited as [2] in the source paper).
Sviridenko, Vondrák and Ward study submodular maximization and supermodular minimization when the objective has bounded total curvature, a parameter introduced by Conforti and Cornuéjols that measures how far a monotone set function is from being linear. Their guarantees improve as decreases. Section 8 of the paper applies this to CSSP: it bounds the curvature of the CSSP objective in terms of the condition number of , so that a well-conditioned matrix has small curvature. This mission formalizes that bound (Lemma 8.2) and the steps of its proof.
Let be a real matrix with columns , so that for , and let be the Euclidean norm. For write for the orthogonal projection of onto , the point of that subspace nearest to (). The CSSP objective is
the squared Frobenius distance from to the nearest matrix whose columns lie in the span of the selected columns.
For a set function on a finite set , the marginal value of at is . The function is monotone decreasing if every . Following (1.1) of the paper, a monotone decreasing has total curvature at most when, for every ,
i.e. the last marginal of is at least a fraction of its first marginal in absolute value.
When the columns of are linearly independent, the condition number is
For with linearly independent columns,
Items 1–7 hold for arbitrary columns; only item 8 and the goal assume independence.
Lemma 8.2 turns a spectral quantity into a combinatorial one. With it, any curvature-dependent guarantee for monotone decreasing set functions can be stated for CSSP in terms of . The paper's Lemma 8.3 shows the bound is asymptotically tight, so is the right order of the curvature.
There is a caveat that the formalization makes explicit. The paper deduces from Lemma 8.1 that is supermodular, and on that basis quotes its supermodular-minimization algorithm for CSSP with factor (p. 12). Both the submodularity half of Lemma 8.1 and the supermodularity of are false as printed. With , and in , the function has . With columns , . A small perturbation gives a counterexample with independent columns. This is the "suppressor variable" phenomenon of regression. The curvature bound itself does not depend on supermodularity and is true, so it is the goal here. The approximation factor for CSSP is not posed, because it rests on the false claim and is stated with .
As far as is known, none of these statements has a machine-checked proof. The results are proved on paper, except the two false claims above. The mission adds a formal proof of the curvature–conditioning bound, and makes explicit which parts of §8 survive.
The individual steps are short linear algebra, but they rest on infrastructure that has to be assembled: orthogonal projections onto spans of finite column families, the Pythagorean identities that relate to projections, and the variational characterization of and of over the unit sphere.
The paper's own route to the large unit vector (milestone 5) does not work as printed. It sets and uses , which is false when , so the signs of the inner products have to be accounted for. In the final step, the ratio is a quotient of two negative numbers. Comparing it with requires the supremum to be finite and the infimum to be strictly positive, which is exactly what independence of the columns provides.
c : Fin n → EuclideanSpace ℝ (Fin m), and is ∑ j, x j • c j. Subsets of are Finset (Fin n). is Finset.univ.erase i and is insert i S.Submodule.starProjection onto Submodule.span ℝ (c '' S), which is finite-dimensional, so the argmin of the page exists and is unique.⨆ and ⨅ of over the unit-sphere subtype of . It is used only under LinearIndependent ℝ c, the page's "non-singular", where both are finite and positive. The page's for dependent columns is not encoded.Useful infrastructure that would be reusable beyond this mission includes Pythagoras for starProjection, monotonicity of projection norms under inclusion of subspaces, and extremal characterizations of and . Contributions of any of the milestones, or of these general lemmas, are welcome.
Strategic open pit mine planning decides which parts of an ore body are excavated, in which period, and to which destination (a processing plant, a stockpile, a waste dump) each block of material is sent. Rivera Letelier, Espinoza, Goycoolea, Moreno and Muñoz (Operations Research 68(5), 2020) model this as a mixed-integer program, the precedence-constrained production scheduling problem with clusters (PCPSP-C), which extends the PCPSP of Bienstock and Zuckerberg (2010) by grouping blocks into clusters that are extracted together. The integer versions of the model have weak linear relaxations on production scheduling instances, so the authors derive cutting planes. Their production cuts (§5.2) exploit the capacity of a single destination together with the precedence structure. This mission concerns the second family of production cuts, the hourglass cuts: they bound how much material must be sent away from a capacitated destination once a cluster is started, using both the predecessors and the successors of that cluster.
Valid inequalities for precedence-constrained knapsack problems have been studied since Boyd (1993) (cited on p. 1433); the paper's contribution is the extension to several destinations, several periods, clusters and partial integrality, the condition used in commercial mine planning software.
All page references are journal pages of the published Operations Research article.
An instance has finite sets of blocks, of destinations and of clusters, the latter a partition of , and periods . Block lies in cluster and has weight . A precedence relation on blocks induces one on clusters ( if some block of precedes some block of ), assumed to be a strict partial order. The arc set is its transitive reduction: when is an immediate predecessor of . The closure is and the reverse closure ; is the set of blocks of a set of clusters, and is the total weight of a set of blocks.
Variables give the fraction of cluster extracted in period and the fraction of block sent to destination in period . The constraints (2)–(7) of p. 1427 are
with an integrality condition: full integrality (10), , defines the PCPSP-F, and partial integrality (11), " implies for ", defines the PCPSP-P. The rows include the destination capacity rows (9), . The cuts are written in the cumulative variables (17).
The simplified setting of §5.2.1 is the mode-knapsack set MK (p. 1433): for a directed acyclic graph , weights and a capacity , the triples with , , , and for every arc . Here is processing and is waste.
Let , , , and let be a set of blocks with . With , the inequality
is valid for the PCPSP-C, that is, for both the PCPSP-F and the PCPSP-P.
In the computational study of §8 (Table 5, p. 1440; discussion on p. 1442) the authors add early start, lifted clique, VRHS and hourglass cuts to the LP relaxation and drop one class at a time; they observe that all classes improve the bound and that the hourglass cuts have the most significant impact. Display (38) makes the separation of the most violated hourglass cut a single pass over the blocks for each cluster, destination and period window. The cuts are valid under partial integrality, the weaker condition that mine planning software imposes, so they strengthen the relaxation of the model actually solved in practice.
Theorem 8 is proved in the paper by a direct calculation; no machine-checked proof exists. A formal proof would certify the inequality in exactly the generality of the model (clusters, several destinations, several periods, both integrality conditions), and the formal model of the PCPSP-C built for it is shared with the other missions of this series.
The inequality is false for the LP relaxation: a fractional start of need not force its predecessors to be complete. Every proof therefore has to use integrality, and the two integrality conditions behave differently. Under partial integrality (11) the implication "started implies predecessors complete" is stated only along the arcs of the transitive reduction , and has to be propagated along chains of immediate predecessors to reach every predecessor of . The capacity step needs that the strict predecessors, itself and its strict successors are pairwise disjoint block sets, which is where the strict partial order is used. The terms are cumulative from period 1 while the terms are summed from ; the two must not be aligned.
Periods are Fin T, so index denotes period . Cluster precedence is derived from the block relation, and is its covering relation. The standing assumptions of §2.1 (clusters partition the blocks, a strict partial order on clusters, discount rate , weights ) are a single hypothesis on the instance. "Valid for the PCPSP-C" is stated as: for each integrality condition, at every feasible whose destination capacity rows (9) hold, which is the page's assumption that (9) is among the rows . The destination , unbound on the page, is a fixed arbitrary destination. In Theorem 8 is a set of blocks and is the weight of together with the blocks of . In MK an arc means precedes , and is reachability in .
Reading "valid" as "valid for the LP relaxation" would make the goal false, while dropping the condition , or the capacity rows, would make it a different statement; neither is the target. In (38) the maximum is taken over all as on the page, without the side condition , which need not satisfy.
A complete development needs only finite sums, finsets and the transitive closure of a relation from Mathlib. Proofs of the milestones, of the MK results and of the goal are all welcome; the lemma that partial integrality propagates along chains of arcs is reusable across all production cuts of the paper.
Unit commitment (UC) is the daily scheduling problem of electricity system operators: decide which generators are switched on in each hour of the next day, and how much each produces, so that supply meets the net load at minimum cost while respecting generation limits, ramping limits and transmission limits. With growing shares of wind and solar power, the net load is uncertain at the time the commitment is fixed. Adaptive robust UC protects the schedule against every net-load trajectory in an uncertainty set.
Lorca, Sun, Litvinov and Zheng (Oper. Res., 2016) argue that the dispatch must be nonanticipative (the output at hour may depend only on loads observed up to ) and propose a multistage robust UC model. To make it computable they restrict the dispatch to affine policies of the observed loads, in the spirit of Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 99, 2004). The paper solves the model on the IEEE 118-bus test case and on the 2718-bus Polish system. The two results of this mission are what makes the simplest such policy cheap to solve: under it, the semi-infinite robust constraints on generation, ramping and energy balance collapse to finitely many deterministic constraints.
There are generators , load nodes and periods . A net-load trajectory is , and its total load in period is . The budget uncertainty set (3) is
with nominal loads , deviations and a conservativeness parameter .
The -policy (10) sets the output of generator in period to an affine function of the current total load,
and the -policy (9) is the special case in which does not depend on . Given commitments , output limits and ramp rates , the robust constraints of the affine model (8) require, for all : generation limits (8c); ramping limits ((8d), (8e)); and energy balance (8g).
The extreme total-load scenarios are a trajectory whose total load is maximal over in every period (19), a trajectory whose total load is minimal in every period (20), and the mixed scenarios
of (21), (22).
Under the -policy (or the -policy), for every generator and period :
For a full-dimensional uncertainty set, the robust energy balance (8g) holds if and only if and for all ((15)); for the -policy, and ((14)).
Proposition 6 removes the constraints (8c)–(8e) from the constraint-generation loop of the affine robust UC: they can be imposed before the algorithm starts, through two scenarios per generation constraint and four per ramping constraint, leaving only the worst-case cost constraint and the transmission constraints to be separated. Proposition 4 turns the semi-infinite energy balance into linear equalities. Together they are the reason the -policy scales to the 2718-bus system in the paper's experiments.
Both results are proved in the paper, and the proofs are short. No machine-checked version is known. The formalization fixes the exact handling of the first period (the initial dispatch ), the exact definition of the mixed scenarios, and the dependence of part (ii) on the product structure of , all of which the paper leaves implicit or states loosely.
Part (i) needs only that the constraint is affine in the scalar total load of one period. Part (ii) is where the obvious argument fails: the ramping constraint couples two periods, and a set that is not a product over periods may not contain a trajectory that is simultaneously maximal in period and minimal in period . The separability of is exactly what puts and in . The labels the paper attaches to (25a) and (25d) are swapped relative to (21)–(22); following them literally sends the argument to the wrong scenario.
Fin Ng, Fin Nd, Fin T; trajectories are Fin T → Fin Nd → ℝ. Periods are 0-based: Lean period t is the paper's period , so "periods " in (21)–(22) are the Lean periods s < t.EReal, under the standing assumptions , that make every nonempty and bounded.The development needs only finite sums, products of sets, and order facts about affine functions; it reuses nothing beyond Mathlib. Proofs of the milestones, the goal and Proposition 4 are welcome.
A basic test of any model of learning in games is whether it respects strict dominance: a strategy that does worse than another against every behaviour of the opponents should eventually be abandoned, and, after it is gone, so should every strategy that becomes dominated in what remains. For the replicator dynamics of evolutionary game theory this is classical: elimination of dominated and iteratively dominated strategies goes back to Akin (1980), Nachbar (1990) and Samuelson and Zhang (1992), whose notion of extinction of a mixed strategy is the one used here; Weibull (1995) gives the textbook account, including a conditional result for weakly dominated strategies.
The replicator dynamics are the continuous-time limit of exponential weights (the logit choice rule), one member of a large family of learning schemes in which every player accumulates the payoffs of their strategies into a score and turns scores into mixed strategies by a regularized best response. Different regularizers give different dynamics: the Gibbs entropy gives the replicator dynamics, the Euclidean square gives the projection dynamics, and many others are used in online optimization. Mertikopoulos and Sandholm (arXiv:1407.6267, Mathematics of Operations Research 41(4), 2016) analyse this whole family in a single framework. In particular they do not assume that the regularizer is steep, so play can reach the boundary of the simplex in finite time and the induced dynamics on the simplex can fail to be well-posed. Their first rationality result is that every iteratively dominated strategy becomes extinct under every scheme of the family.
A finite game has a finite set of players , a finite set of pure strategies for each player , and payoffs . A mixed strategy of player is a point of the simplex , and is the expected payoff (2.1) at a mixed profile . The payoff vector of player is , where is the payoff of the pure strategy against .
A penalty function on a simplex (Definition 2.1) is a function that is continuous, smooth on the relative interior of every face of , and strongly convex with some constant :
Its choice map is (Definition 2.2). Each player has a penalty function and choice map . The reinforcement learning dynamics are
so that is the cumulative payoff of player 's pure strategies and is the resulting play. Strategy is dominated by , written , if for all (4.1). Removing dominated strategies and repeating gives the iteratively dominated strategies. A mixed strategy becomes extinct along if .
The analysis runs through the Fenchel coupling , where , and the Bregman divergence , defined with the one-sided directional derivative so that it makes sense at boundary points where has no gradient.
For every orbit of (RL), every player , and every mixed strategy that is dominated, possibly only after some rounds of elimination,
The penalty functions are arbitrary in the sense of Definition 2.1, including non-steep ones, and may differ across players.
Two companion statements extend the goal: Proposition 4.2, the rate under the rescaled dynamics (RLγ) with decomposable penalties, which gives extinction in finite time when the kernel is not steep at ; and Proposition 4.3, a conditional extinction result for weakly dominated strategies.
The theorem shows that elimination of iteratively dominated strategies is a property of the whole class of regularized reinforcement learning schemes, not only of exponential weights. It is also unilateral: a player who follows (RL) stops playing dominated strategies whatever the other players do (Remark 4.2). The proof does not use the dynamics induced on the simplex, which need not be well-posed for non-steep regularizers; it works with the scores in the dual space. Proposition 4.2 then shows that the regularizer sets the speed of elimination: exponential for the entropy, finite time for the Euclidean square.
The result is proved in the paper; nothing here is open. No part of it is formalized. The mission produces the paper's convex-analytic toolkit for penalty functions on a simplex (Fenchel coupling, the one-sided Bregman divergence, their comparison with the Euclidean distance) and a machine-checked proof of the elimination theorem on top of it. The same toolkit is used by the paper's results on strict equilibria and zero-sum games.
The familiar argument for the replicator dynamics shows that the Kullback–Leibler divergence diverges. For a general penalty function the analogous Bregman divergence uses , which does not exist at boundary points, and non-steep dynamics spend time on the boundary. The proof therefore tracks the Fenchel coupling , whose growth is easy to bound, and must convert its divergence into extinction. That conversion (Propositions C.2–C.4) needs continuity of the one-sided Bregman divergence on , including at points of lower-dimensional faces, and a compactness argument that turns "no limit point in " into a statement about every time sequence. The iterated case adds an induction in which the payoff gap is only positive on the surviving profiles, so the trajectory's distance to those profiles must be controlled.
Lean conventions:
Fintype ι; strategies are Fintype (A k); payoffs are u : ι → (∀ k, A k) → ℝ. Mixed strategies, mixed profiles and expected payoffs are those of the published agt_games definition.IsPenalty h K: continuity on the simplex, along smooth curves in the relative interior of a face (footnote 5), and (2.5) with the Euclidean norm. Steepness is not assumed.IsChoice h y x ( maximizes on the simplex), never a chosen maximizer.Trivializing formalizations are ruled out. Orbits are not vacuous: a sorry-free check exhibits an explicit orbit of a game with a strictly dominated action, under the quadratic penalty. The choice map is not a junk argmax. Steepness, which would keep play interior, is not added. Extinction is not weakened to a .
Needed infrastructure: properties of strongly convex functions on a simplex, the conjugate and its maximizers, one-sided derivatives of convex functions along segments, and compactness of the product of simplices. Most of this is reusable beyond the mission. Contributions are welcome on the Appendix-C lemmas, which are independent of the game, as well as on the goal.
In decentralized consensus optimization, agents connected by a communication network cooperatively solve
where agent privately holds the convex function and may only exchange vectors with its neighbours. The model covers distributed estimation and learning over sensor networks, multi-agent control and decentralized machine learning, where no agent may collect all the data. The classical method, decentralized gradient descent (DGD), lets every agent average its neighbours' iterates and take a local gradient step. With a fixed step size DGD stalls at a neighbourhood of the solution whose size is proportional to the step, so exact convergence requires diminishing steps and is slow.
Shi, Ling, Wu and Yin (arXiv:1404.6264; SIAM J. Optim. 25 (2015)) introduced EXTRA, an "exact first-order algorithm" that keeps a fixed step size and still converges to the exact solution. This mission formalizes the second main result of that paper: under restricted strong convexity, EXTRA converges linearly. The companion mission of the series covers the sublinear rates for general convex objectives.
Agent keeps a local copy ; the stacked variable has these copies as rows, with Frobenius inner product . Write , let be the matrix with rows , and for a symmetric matrix let .
Two symmetric mixing matrices satisfy Assumption 1: their off-diagonal entries vanish between non-neighbours of a connected graph; and ; and , . Each is convex with -Lipschitz gradient (Assumption 2), and the problem has a solution (Assumption 3). With step size , EXTRA is
Each agent uses only its own gradient and its neighbours' iterates.
The analysis uses , the auxiliary sequence , an optimal pair with , , , and the stacked pair , measured in .
A gradient map is restricted strongly convex with respect to with constant if for all . The condition is imposed on the penalized function
If is restricted strongly convex with respect to with constant and , then there is such that for all
and consequently . The goal asserts the existence of a contraction factor, not a particular value of , so it survives any improvement of the constants.
A companion item states Proposition 3.6: is restricted strongly convex at if and only if is at .
Theorem 3.7 is what separates EXTRA from DGD: a fixed step size gives linear convergence to the exact solution, with the strong convexity requirement placed on , not on the individual (Remark 1). By Proposition 3.6 this is the same as restricted strong convexity of the global objective , so agents with merely convex local losses still converge linearly. EXTRA is an early member of the family of exact decentralized methods (gradient tracking, NIDS, exact diffusion), whose linear-rate analyses use Lyapunov functions of the same primal–dual type.
The result is proved in the paper. Neither it nor any other decentralized optimization rate is formalized in Mathlib or on the platform. A formal development would produce a reusable layer for stacked variables, Frobenius geometry, matrix-weighted norms and mixing-matrix assumptions, on which other decentralized algorithms could be stated.
The obvious Lyapunov function does not contract: EXTRA is a primal–dual method in disguise, and the primal error alone can increase. The contraction holds only for the joint quantity , and the descent inequality (3.29) controls only the primal part of . The dual error must be bounded separately. That bound (3.35) works only because lies in the range of , where is invertible with smallest nonzero eigenvalue . Restricted strong convexity of also gives curvature only toward the single point , not between arbitrary pairs.
Stacked variables are Fin n → EuclideanSpace ℝ (Fin p). The sup norm Lean puts on this type is never used: Frobenius quantities go through an explicit inner product frob, and is the quadratic form frob x (mix M x), also for indefinite as in (3.29). , , and are pinned by their characterisations (an eigenvalue that is extreme among all eigenvalues). is any symmetric positive semidefinite matrix with . Assumptions 1–3 are standing hypotheses of every item except Proposition 3.6, which assumes only Assumptions 1 and 2, as printed. Assumption 2 uses one common Lipschitz constant . The step-size conditions are multiplied out (), so that is not turned into by Lean's . The gradients of and are written as explicit formulas.
The goal does not mention , , the minimum (3.38) or (3.30). A version assuming those intermediate inequalities would be trivial, and so would one with a free allowed to depend on . The printed "In addition" sentence of Proposition 3.6 () is false; the companion item states the direction proved in Appendix A.
The infrastructure needed is: Frobenius inner products of stacked variables, quadratic-form bounds by extreme eigenvalues, the range/nullspace argument for symmetric positive semidefinite matrices, and the elementary inequality . Proofs of any milestone, and reusable lemmas on matrix-weighted norms, are welcome.
In decentralized optimization a group of agents minimizes a sum of functions without a central coordinator: agent knows only its own function and can exchange vectors only with its neighbours in a communication network. The setting covers sensor networks, multi-robot coordination and data-parallel learning in which the data cannot be pooled. The basic algorithm is decentralized gradient descent (DGD), in which every agent averages its neighbours' iterates and takes a local gradient step. It goes back to Nedić and Ozdaglar's distributed subgradient method (IEEE TAC 2009), which used diminishing stepsizes.
Practitioners often run DGD with a fixed stepsize, and with a fixed stepsize DGD does not reach consensus at an optimum: the local gradient term keeps pushing the agents apart. Yuan, Ling and Yin (arXiv:1310.7063v3; SIAM J. Optim. 26(3), 2016) quantify what a fixed stepsize achieves. They show that bounded gradients follow from a stepsize condition rather than being assumed, that the agents stay within of their mean, and that under (restricted) strong convexity every agent converges geometrically to an neighbourhood of the solution set. This mission formalizes that linear-rate result, Corollary 1 of the paper (p. 14). A companion mission covers the sublinear rate of the convex case (Theorem 2).
There are agents and a decision space . Agent holds , and the agents solve
with solution set , assumed nonempty. The network is a graph on the agents, and the mixing matrix has only if or are neighbours. Starting from , DGD with stepsize updates all agents at once:
If is symmetric, its eigenvalues are real and sorted with multiplicity as . The network enters through the second largest eigenvalue magnitude
Assumption 1 (p. 4): (a) each is convex, differentiable and bounded below, and is Lipschitz with constant ; (b) the network is connected, and is symmetric and doubly stochastic with .
Write , , and
The mean iterate is , and has gradient Lipschitz constant . The function is strongly convex with modulus if for all . It is restricted strongly convex with modulus if the same holds with only (7). The solution error is with . Lemma 3 (p. 12) supplies constants : in the strongly convex case and ; in the restricted case and with . Here and .
Under Assumption 1, if is strongly or restricted strongly convex with , and , then for every and every agent
where and at .
ConvexOptAlg.StrongGD.lemma_3_11.The result separates the two error sources of fixed-step DGD. The geometric term comes from the optimization, at a rate governed by . The floor is and comes from the network. Halving the stepsize halves the floor but slows the rate, and a poorly connected network ( close to ) inflates the floor. This trade-off motivated exact decentralized methods such as EXTRA and gradient tracking, which remove the floor. Corollary 1 is the baseline they are compared against.
The paper's proofs are short and have not been machine-checked. Formalizing them yields reusable Lean infrastructure for decentralized methods: stacked iterates in with the Euclidean norm, mixing matrices and their spectral gap, the consensus bound of Lemma 1, and the inexact-gradient view (15) of the mean iterate. Lemma 3 (a) is already formalized on the platform (Bubeck, Lemma 3.11, Proved).
The algebra of Theorem 3 is routine once Lemmas 1–3 are available. The work lies elsewhere. Theorem 1 must derive bounded gradients from the stepsize condition alone, with no a priori bound on the iterates and with possibly negative. Lemma 1 requires the operator norm of , tensored with the identity on , to equal , which needs the spectral theorem for symmetric matrices and the fact that makes the eigenvalue simple. Bounding directly by summing gradient steps fails, because the bound grows with : the consensus estimate has to go through the deviation from the mean. Lemma 3 (b) holds only at the projection onto , not at an arbitrary solution, which constrains how it can be applied.
is EuclideanSpace ℝ (Fin p), and stacked vectors live in PiLp 2 over the agents, so is the Euclidean norm of , not a maximum norm. DGD is a recursively defined sequence from , not an arbitrary sequence with stated properties. and are entries of Mathlib's eigenvalues of a Hermitian matrix sorted nonincreasingly with multiplicity. The definitions return off the symmetric case, which Assumption 1 excludes. Gradients are Mathlib's gradient, is the infimum of , and projections are nearest-point predicates. The Lemma 3 constants are a disjunction of the two cases, so the goal covers both.
Additions relative to the page, each disclosed in the items: , so that exists; ; , which the page needs for ; , which is standing on p. 2; and the bound (10) at , which Lemma 1's proof uses. Theorem 1's convergence sentence is not stated. It fails at the boundary stepsize , and only the bound (10) is used downstream. A trivializing formalization is excluded: the iterates are those of (4), the stack norm is Euclidean, uses the sorted spectrum, and a two-agent instance with and satisfies every hypothesis of the goal. Contributions of proofs of any milestone are welcome. The spectral bound inside Lemma 1 and the descent argument for Theorem 1 are reusable beyond this mission.
A forward–backward stochastic differential equation (FBSDE) couples a forward diffusion with a backward equation for a pair whose terminal value depends on . FBSDEs are the probabilistic form of quasilinear parabolic PDEs and appear in stochastic control (the stochastic maximum principle), in mathematical finance (hedging with large investors, stochastic differential utility) and in mean-field games. Their solvability over an arbitrary horizon is delicate: the coupling can make a solution exist only on short time intervals.
Ma, Wu, Zhang and Zhang (arXiv:1110.4658v2, Ann. Appl. Probab. 25 (2015)) reduce well-posedness of a general one-dimensional FBSDE to the behaviour of two scalar dominating ODEs: when these have solutions that stay bounded on , the FBSDE has a regular decoupling field and a unique solution. Section 5.1 of the paper tests this programme on the simplest class, the linear FBSDE with constant coefficients, and obtains necessary and sufficient conditions. The authors describe these as setting the "limits" for the solvability of general FBSDEs.
Earlier approaches each covered part of the picture: the method of contraction mappings for small time (Antonelli 1993, MR1233625), the four-step scheme for Markovian FBSDEs with regular coefficients (Ma, Protter, Yong 1994, MR1262970), and the method of continuation under monotonicity conditions (Hu, Peng 1995, MR1355060; Peng, Wu 1999, MR1675098; later Yong 1997, MR1440146). The unified approach of the paper contains these as special cases.
Let be real numbers and consider the linear FBSDE (4.1)
in Case 1, . Then the two dominating ODEs coincide and become the scalar backward equation
with the cubic
In the Appendix's notation (A.3), with , , .
A solution on of is a function such that, for every , is integrable on and the equation holds at . A bounded solution additionally has . In Lean the coefficients form the structure UnifiedFBSDE.Cubic.Coeffs, is Coeffs.F, and the predicates are IsSolution and IsBoundedSolution.
For a fixed horizon : (i) or ; (ii) , , ; (iii) , , , with small. Each guarantees a bounded solution on .
Theorem 5.3 turns the existence of a global bounded solution of the dominating ODE into a finite check on a cubic polynomial: the sign of , the location of a real root, and two coefficient identities. Through the paper's main construction, a bounded solution yields a uniformly Lipschitz decoupling field, and hence well-posedness of the linear FBSDE on any horizon. When none of (i)–(iii) holds, the dominating ODE explodes in finite time. This is the sense in which the paper says the constant-coefficient results "more or less set the 'limits'" for the solvability of general FBSDEs: the conditions it later imposes on random coefficients (§5.2, §7) are modelled on the cases (i)–(iii).
The result is proved in the paper: sufficiency on p. 21, necessity in the Appendix (pp. 46–47). To our knowledge none of it is machine-checked. A formalization produces a reusable comparison theorem for scalar backward integral equations with Lipschitz-on-a-band nonlinearities (Lemma 5.1), explicit finite-time blow-up criteria for polynomial ODEs, and a complete, checked classification of global solvability for the cubic Riccati-type equation (5.3).
Sufficiency rests on Lemma 5.1, which requires Carathéodory existence and uniqueness for an equation that is only Lipschitz on a time-dependent band, followed by an integrating-factor comparison argument. Mathlib's Picard–Lindelöf and Gronwall tools are stated for forward equations with continuous right-hand sides, so they need adaptation.
Necessity is a case analysis whose obvious version fails at two points. First, one cannot simply bound below by using the smallest real root: the intermediate inequality (A.5) as printed points the wrong way for some root orderings, and the correct bound uses the largest root or an infimum over . Second, the blow-up step compares a solution of (5.3) with an explicit exploding solution. This needs the solution to stay above for the whole interval, which in turn needs continuity of the right-hand side. For a discontinuous right-hand side the comparison fails.
Time is real, with and . Solutions are functions whose values outside are irrelevant. The integral is Mathlib's interval integral. "For arbitrary " is , with the universal quantifier outside. "A zero point in " is .
Pinned readings, all disclosed in the items:
Trivializing formalizations are ruled out. The solution predicate carries integrability of the integrand, so Lean's junk value for a non-integrable integral cannot make an arbitrary with a solution. The goal assumes neither a zero of nor a blow-up: both are proved in the milestones. Lemma 5.1's uniqueness is over solutions in the band.
The needed infrastructure is scalar ODE theory on Mathlib: existence for Lipschitz Carathéodory equations, differentiation of , comparison of sub- and super-solutions, and elementary real-root facts for cubics. The comparison lemma and the blow-up lemma are reusable beyond this mission. Contributions of either the sufficiency or the necessity chain are welcome independently.
Many planning problems are made in two stages: a first decision is fixed before an uncertain parameter is observed, and a second, corrective decision is made afterwards. When the second-stage decisions are binary (which route, which facility, which crew), the resulting two-stage robust binary programs are notoriously hard: the second-stage decision is a function of the uncertain parameter, and no general finite reformulation is known.
Bertsimas and Caramanis (IEEE Trans. Automatic Control, 2010) proposed the K-adaptability approximation: instead of a full second-stage policy, the decision maker commits here-and-now to candidate second-stage decisions and implements the best of them once the parameter is known. Besides being computable, this matches practice in vehicle routing, production scheduling and emergency planning, where a small number of contingency plans is preferred to re-optimizing after every observation. The basic question is how many candidates are needed before nothing is lost. Hanasusanto, Kuhn and Wiesemann (Oper. Res. 63(4), 2015) answer it when the uncertainty affects only the objective function; this mission formalizes that answer, Theorem 1 of their paper.
The data are matrices , , , , a vector , a set of first-stage decisions , a set of binary second-stage decisions , and an uncertainty set
a nonempty bounded polyhedron. (The paper writes both for the number of uncertain parameters and for the cost matrix; in Lean the dimension is nQ and the matrix Q.)
The two-stage robust binary program with objective uncertainty is
For and , the K-adaptability problem is
The affine dimension is the dimension of the smallest affine subspace containing , and is the rank of the cost matrix .
For every number of policies ,
with the unit simplex in . 4. (EC.1) = (EC.2) (p. ec2): the randomized problem with policies has the same optimal value as the one with policies; and, for the case , as the one with policies. 5. (EC.2) is the -adaptability problem (p. ec2): for every , the randomized problem with policies has the optimal value of .
The set may contain exponentially many binary vectors, so a priori full adaptability could require exponentially many policies. Theorem 1 says that under objective uncertainty at most policies are ever needed, a number linear in the problem size. It justifies solving for small as an exact method rather than a heuristic whenever or is small, and it is the reason the paper's mixed-integer linear reformulation of (Theorem 2) solves itself for such . It also contrasts with the constraint-uncertainty case, where the same paper shows that every can leave a strict gap.
Theorem 1 is proved in the paper's e-companion. As far as is known, neither the theorem nor any step of its proof has a machine-checked proof; this mission produces one, together with reusable Lean statements of the problems , and their randomized relaxations in the extended reals.
The obvious argument lists all feasible second-stage decisions as policies, which needs of them. Reducing this number is not a matter of discarding unused policies: for different different policies are optimal, and which subset of policies suffices is not determined by any single . The reduction to policies holds only for the optimal value, not decision by decision, and it passes through a relaxation in which the policies are mixed with weights; exchanging the maximum over with the minimum over the weights requires compactness and convexity of , and in Lean the exchange has to be carried out for extended-real values. The bound must also hold for every above the threshold, so monotonicity in the number of policies is part of the statement.
Problem N M L nQ R; its fields include the standing assumptions: , every point of is a 0/1 vector ( is a Finset), and is nonempty and bounded. is an arbitrary set (the paper allows mixed binary first-stage decisions).EReal. Maxima and minima are suprema and infima, as in the paper's notation: a first-stage decision without a feasible second-stage decision has objective , and an infeasible problem has optimal value .Fin K and need not be distinct; every policy must satisfy , as in problem of Observation 1.Module.finrank ℝ (vectorSpan ℝ 𝒴) (so in Lean; both optimal values are then ), and is Matrix.rank.Sion.minimax in Mathlib), Carathéodory's theorem (convexHull_eq_union), compactness of bounded polyhedra and extended-real iSup/iInf manipulation. Lemmas on suprema of linear functions over compact polyhedra and on min-max exchange in EReal are reusable beyond this mission. Proofs of any milestone, and alternative routes to the goal, are welcome.Two-stage robust optimization models decisions taken in two steps around an uncertain parameter: a here-and-now decision is fixed before the parameter is revealed, and a wait-and-see decision adapts to it, and the decision maker guards against the worst in an uncertainty set . When the second-stage decisions are binary, as in routing, scheduling and network design, the exact two-stage problem is computationally out of reach. Bertsimas and Caramanis (IEEE TAC, 2010) proposed the K-adaptability approximation: choose second-stage policies here and now, and once is revealed implement the best of those that are feasible. Hanasusanto, Kuhn and Wiesemann (Oper. Res., 2015; preprint Optimization Online 2014/03/4294) study this problem in depth. When the uncertain parameter enters the second-stage constraints, the K-adaptability problem is in general neither convex nor continuous, and to obtain a solvable reformulation the authors first approximate it by a family of problems with closed uncertainty sets. This mission formalizes the statement that this approximation is asymptotically exact.
The data are matrices , , , , , a nonempty bounded polyhedron , a first-stage set (the standing assumption of §3 of the paper) and a second-stage set . A decision is with . Policy is feasible for if . The K-adaptability problem minimizes over decisions
which is when some leaves no feasible policy.
Let . For , the set collects the for which every policy with is feasible and every policy with violates constraint strictly: . Problem (6) minimizes
The sets are not closed. For the closed inner approximations replace the strict inequality by , and problem has objective , defined like with . The effective domains and are the decisions at which , respectively , is not .
(i) There is such that
(ii) For every there is such that for all and every decision in , both objective values are finite and
Proposition 2 is the justification for the computational part of §3 of the paper: Theorem 5 reformulates , not (6), as a mixed-integer bilinear program, and Proposition 2 says that solving that program for small recovers the K-adaptability problem's feasible decisions exactly and its objective values to arbitrary accuracy, uniformly over all decisions. Without it the bilinear reformulation would approximate an unrelated problem. Together with Proposition 1 it connects the original K-adaptability problem to a family of problems with closed, polyhedral uncertainty sets. The same exhaustion of a non-closed polyhedral set by closed inner approximations appears whenever strict inequalities are replaced by -margins.
The results are proved in the paper's e-companion. To our knowledge none of them has a machine-checked proof. The mission produces a Lean model of the K-adaptability problem with constraint uncertainty and its decision-dependent uncertainty sets, which other formalizations of the paper's Theorem 5 or of related K-adaptability work can reuse.
Pointwise, the claim is easy: each belongs to once is below its own constraint slack. That slack can be arbitrarily close to on , because is not closed, so no single works for all . Uniformity in needs a compactness argument on the bounded set . Uniformity over decisions needs finiteness of , which is where enters. With a continuous first stage the threshold in (i) could depend on . A second difficulty is bookkeeping: and are extended-real suprema of infima over index sets that may be empty, and the comparison in (ii) must first show that both values are finite.
EuclideanSpace ℝ (Fin nQ), so every norm and distance is Euclidean, as in the paper's use of Cauchy–Schwarz. Decisions are pairs (x, y) with y : Fin K → Fin M → ℝ. is a Finset of 0/1 vectors and a set of 0/1 vectors.Fin K → Fin (L+1). The paper's row is i.succ for i : Fin L.EReal. The paper's max and min are read as sup and inf, an infimum over no admissible policy is , and a supremum over an empty set is . "Finite (do not evaluate to )" in the definition of the effective domains is read as . Part (ii) asserts that both values are real numbers before comparing them, so the truncation EReal.toReal ⊤ = 0 plays no role.Metric.hausdorffEDist. The real-valued Metric.hausdorffDist is when one set is empty, so a statement with it would drop the nonemptiness of that the lemma contains.EReal suprema. Proofs of the milestones, alternative arguments, and variants with continuous under additional hypotheses are welcome.Many planning problems are decided in two stages. A here-and-now decision is taken before an uncertain parameter vector is observed, and a wait-and-see decision is taken afterwards. When the wait-and-see decision is binary (which route to drive, which facility to open, which machine to schedule), the resulting two-stage robust binary program has no known tractable reformulation, even when ranges over a polyhedron.
Bertsimas and Caramanis (2010) proposed the K-adaptability approximation. Here candidate second-stage policies are fixed here and now, together with , and the best of them is selected once is known. Operationally this matches settings where a few contingency plans are preferred to an arbitrary re-optimization, such as production scheduling or emergency response. Bertsimas and Caramanis gave a bilinear reformulation for . Hanasusanto, Kuhn and Wiesemann (2015) proved that, when enters only the objective, the K-adaptability problem for any is equivalent to a single mixed-integer linear program (MILP) whose size is polynomial in the input data. That equivalence, Theorem 2 of their paper, is the subject of this mission.
The data are matrices , , , , a vector , and an uncertainty set
assumed nonempty and bounded. Inequalities between vectors are componentwise. The letter names both the number of uncertain parameters and a matrix. The first-stage feasible set is , and the second-stage feasible set is .
Fix and write . The K-adaptability problem with objective uncertainty is
The decision consists of and the policies . The adversary chooses , and the decision maker then uses the cheapest policy. Following the paper, max and min denote sup and inf when they are not attained.
With the all-ones vector, the MILP (5) is
Problem is equivalent to the MILP (5). Formally:
and the minimum on the right is attained; 3. the optimal values of and (5) coincide.
Parts 1 and 2 are the per-decision correspondence; part 3 is the equality of optimal values. Together they are what "equivalent" means on p. 13.
and the minimum is attained.
The result. Theorem 2 makes the K-adaptability problem with objective uncertainty solvable by off-the-shelf MILP solvers, and the size of (5) grows polynomially in the size of the input data (p. 13). Together with Theorem 1 of the same paper, which shows that policies already recover the full two-stage problem, it yields an exact finite MILP formulation of two-stage robust binary programs with objective uncertainty. The paper's numerical experiments on supply chain design and route planning (§4.1–4.2), which are instances of , use this formulation.
Formalizing it. The theorem is proved in the paper, in a short argument in its electronic companion. No machine-checked version exists. A formal proof certifies the exact form of (5), including every sign and every inequality of the linearization, against the original min–max–min problem. It also exercises LP strong duality in a form with attainment, for a polyhedron given by with free variables. The same pattern (dualize an inner LP, then linearize products of a continuous and a binary variable) recurs across robust and bilevel optimization, so a reusable development of it is valuable beyond this paper.
The obvious route is to swap the max over with the min over policies, and that fails. The function is concave, not linear, so is not a min–max of a bilinear function in the policies. The inner maximization must be kept as an optimization problem and replaced by an equivalent minimization, which needs LP strong duality with attainment of the dual optimum. Its preconditions (primal feasibility from , boundedness from bounded and ) have to be discharged. The dualized problem contains products of continuous and binary variables. Replacing them by linear constraints is exact only because is binary and ; with fractional the three inequalities do not force (Remark 4, p. 14). The remaining effort is bookkeeping in extended reals: optimal values are infima and suprema, and the correspondence of feasible points must be exact in both directions.
Vectors are Fin n → ℝ, matrices are Matrix (Fin a) (Fin b) ℝ, products are Matrix.mulVec and dotProduct, and ≤ on vectors is componentwise. The paper's dimension is nQ. The data, with the standing assumptions of §1 (Ξ nonempty and bounded, , points of binary), form one structure KAdaptability.ObjMILP.Problem. is an arbitrary set of nonnegative vectors, and an arbitrary set of 0/1 vectors. Policies are indexed by Fin K with the hypothesis 0 < K. The all-ones vector is 1.
Every objective and optimal value is an EReal. The objective of is a supremum over of plus an infimum over . The optimal values of , of (5) and of the dual LP are infima, equal to when infeasible. The epigraph LP's value is a supremum. Part 3 of the goal is an equality of infima, since the optimum over need not be attained when is not closed.
The goal does not assert merely that the two optimal values coincide, nor an inequality. It states the per-decision identity with attainment and the correspondence of feasible decisions. The program (5) appears with exactly its constraints, including , so it cannot be replaced by some other MILP.
A complete development needs LP strong duality with dual attainment for . The platform's LinearOptimization.lp_strong_duality and SmaleNinth.lp_strong_duality are possible tools, in their own encodings. It also needs elementary facts about EReal suprema and infima. Contributions of a general "LP value equals dual LP value" lemma in the Matrix.mulVec encoding are welcome and reusable.
Two-stage robust optimization models decisions taken in two steps around an uncertain parameter : a here-and-now decision is fixed before is revealed, and a wait-and-see (recourse) decision is chosen afterwards, against the worst case of in an uncertainty set . When the recourse is binary — routing, scheduling, facility opening, emergency response — the fully adaptive problem is intractable in general, and practitioners also often prefer a short list of contingency plans to an arbitrary decision rule.
The K-adaptability approach, introduced by Bertsimas and Caramanis (IEEE TAC 2010), fixes candidate recourse decisions here-and-now and implements the best feasible one once is known. Hanasusanto, Kuhn and Wiesemann (Oper. Res. 2015; preprint Optimization Online 2014/03/4294) study how many candidates are needed. Their Theorem 1 shows that if enters only the objective, candidates recover the fully adaptive optimum. Their Theorem 4, the subject of this mission, shows that this fails completely once enters the constraints.
The generic two-stage robust binary program has data , , , , , a first-stage set , a second-stage set , and a nonempty bounded polyhedral uncertainty set . Its optimal value is
The K-adaptability problem instead chooses and policies in advance:
If no policy is feasible for some , the inner infimum is over the empty set and the objective is . Affine dependence of the right-hand side on is written with an extra parameter constrained to equal .
The paper's instance (EC.4) has no first-stage decision, , zero objective, and constraints , () over . Its K-adaptability problem is (EC.5).
For every and every , the instance (EC.4) satisfies
One instance per serves every at once.
The result. Theorem 4 separates the two regimes of the paper. Under objective uncertainty a number of policies linear in the dimension suffices (Theorem 1); under constraint uncertainty no number short of , which is exponential in , can be guaranteed. This justifies the paper's turn in §3 to approximations of whose quality depends on rather than to exact recovery of , and it marks a structural limit for any method that approximates two-stage problems by finitely many contingency plans.
Formalizing it. The result is proved in the paper; no machine-checked version exists. The mission produces general Lean definitions of and with the conventions made explicit, reusable by later missions on this paper (the ε-approximations of §3.1 and the bilinear reformulation are stated for the same problems), and a checked instance showing that the convention "infeasible means " is what drives the gap.
The mathematics of the instance is elementary; the content lies in stating it against the general problems. The step that fails for any obvious formalization shortcut is the treatment of infeasibility: the gap between and exists only because an empty inner infimum is and the outer supremum ranges over a nonempty set. A formalization in which a missing feasible policy contributes (the Lean default for a real-valued infimum of the empty set) would make and agree on this instance, and the theorem false. A second subtlety is the affine right-hand side , which the general model with linear admits only through the auxiliary coordinate .
Fin n → ℝ, matrices Matrix (Fin a) (Fin b) ℝ, inequalities between vectors are componentwise.EReal; max and min are read as sup and inf; an empty infimum is , an infeasible problem has value .Finset of 0/1 vectors and a set of 0/1 vectors (the standing assumption of §3). Nonemptiness and boundedness of are part of the data, so the instance proves them.Fin K and may repeat; and are allowed.Fin Q → Bool, with proved in the definition file.A trivializing formalization is ruled out: the goal is stated about the general optimal values optP and optPK evaluated at the instance, not about a hard-coded formula for (EC.4) or (EC.5); a statement whose problems are written out for the instance alone would reduce to a computation and is not the paper's theorem.
Welcome contributions: proofs of the three milestones and the goal; lemmas computing for general data (monotonicity in , the conservative-approximation inequality , equality at ), which are reusable across the series.
Tensor decompositions are a standard tool in signal processing, chemometrics, telecommunications and blind source separation. The canonical polyadic decomposition (CPD) writes a tensor as a sum of rank-one tensors; the rank- block term decomposition (BTD) replaces each rank-one term by the outer product of a rank- matrix and a vector. Sorber, Van Barel and De Lathauwer (SIAM J. Optim. 23(2), 2013) introduced a common generalization, the (rank- rank-1) BTD, and derived optimization algorithms that compute all three decompositions of complex tensors. Their quasi-Newton and nonlinear conjugate gradient methods are built on complex Taylor models in and (Sorber, Van Barel and De Lathauwer, SIAM J. Optim. 22(3), 2012), and each iteration needs the complex cogradient of the least-squares objective. This mission formalizes the closed form of that cogradient, Theorem 4.4 of the paper. The algorithms were released in the MATLAB toolbox Tensorlab.
Let be a tensor of order . Fix block sizes and put . The unknowns are complex matrices for and for , collected in the vector
Let be the block-diagonal matrix of row vectors of ones. The (rank- rank-1) BTD is read as a structured CPD with factor matrices
Its residual tensor is , and the objective is the nonlinear least-squares function
with the Frobenius norm induced by .
For a set of modes, is the Khatri–Rao product (column-wise Kronecker product) of the factor matrices outside , and is the Hadamard product of their Gramians. The mode- unfolding arranges the mode- fibres of as columns, ordered like the rows of .
The objective is real-valued, hence not holomorphic in . The cogradient is the vector of Wirtinger derivatives
the derivative with respect to with held constant. Overbars denote entrywise complex conjugation.
For every tensor and every , for and ,
The identity (4.4), which assembles from these blocks, holds by construction in the formalization.
Theorem 4.4 gives the gradient information every first-order and quasi-Newton method for the CPD, the rank- BTD and their generalization needs. It replaces derivatives through the large Khatri–Rao product by small Hadamard products of Gramians, and leaves one tensor–Khatri–Rao product per mode as the dominant cost. Table 4.1 of the paper specializes it to third-order CPDs and BTDs, and the same structure underlies the alternating least squares updates of §4.1.
The paper proves the result. As far as a search of the Prove2Me catalogue and Mathlib shows, it has not been machine-checked. Mathlib has the Kronecker product and Matrix.vec, but no Khatri–Rao product, tensor unfoldings or Wirtinger calculus on matrix-valued unknowns. A formal proof would supply a checked derivation of the gradient formula used in tensor software, together with reusable lemmas about Khatri–Rao products and Wirtinger derivatives of real quadratic forms.
Each step is elementary, but the bookkeeping is easy to get wrong. The cogradient of a real function is not a complex derivative. Conjugates appear exactly where the conventions put them: with instead of , or with the inner product conjugated on the other argument, every overbar in (4.5) moves. The proof also differentiates with respect to , which is not an unknown. That step is justified only by treating the structured CPD as an unstructured one and pulling back through with a chain rule for Wirtinger derivatives, which needs real differentiability of the outer function. Finally, the Khatri–Rao identity requires reindexing a product over a permuted list of modes into a product over all modes.
Modes are Fin P ⊕ Fin Q. The paper's mode is Sum.inl (p-1) and its mode is Sum.inr (q-1). The columns are Σ r : Fin R, Fin (L r) in lexicographic order, which is the order of (3.5), and all indices are 0-based. vec is column-major (Mathlib's Matrix.vec). The rows of and the columns of are indexed by tuples of the remaining indices rather than by integers; both use the same order, so the products in (4.5) are unchanged. The residual is defined entrywise and is a real number cast to . The cogradient is defined coordinatewise from Mathlib's real deriv along the directions and . The functions differentiated in the goal are real polynomials in the real and imaginary parts, so deriv is a genuine derivative there; a junk value of would make (4.5) false, not vacuous. Milestones 3–5 are stated for the unstructured CPD, in which every mode, including , has a free factor matrix. Proposition 4.1's chain rule assumes the outer function is real-differentiable at the point. That is the only hypothesis in the mission.
The paper's qualifiers " nonzero" (3.1) and "rank-" (3.5) describe what a decomposition is, and §4 never uses them. They are not imposed: the statements hold for arbitrary complex factor matrices and tensors, and , , , , may be . The goal must not be replaced by its (4.4) part alone, which holds by construction, nor by a version with or with the Hermitian transpose in place of the entrywise conjugate .
A complete development needs Khatri–Rao Gramian identities, derivatives of real-valued polynomial maps along real lines in , and the Wirtinger chain rule for a -linear inner map. All of these can be reused outside this mission. Contributions are welcome on any milestone, and on general Wirtinger-calculus lemmas (linearity, products, conjugation, chain rule).
For a -regular graph on vertices, the Expander Mixing Lemma (Alon–Chung 1988; see the survey of Hoory, Linial and Wigderson 2006) says that for any vertex sets , the number of edges between them is close to its expected value: , where is the largest absolute value of a nontrivial eigenvalue of . The deviation, called the discrepancy of and , measures how random-like the graph is. It is one of the basic tools of spectral graph theory and of the theory of expanders.
Higher-dimensional expansion asks the same questions for simplicial complexes, where the role of edges is played by -dimensional cells. Parzanchevski, Rosenthal and Tessler (Combinatorica 35, 2015) prove, for complexes with a complete skeleton, a Cheeger inequality and a Mixing Lemma: the number of -cells with one vertex in each of disjoint vertex sets is controlled by the spectrum of the upper Laplacian. The Mixing Lemma is the result of this mission. In the same paper it yields a lower bound on Gromov's geometric overlap (Gromov 2010) of complexes with a small spectral spread.
Let and . A -dimensional complex with a complete skeleton contains every set of at most vertices as a cell, together with a set of -cells, each a set of vertices. Cells are oriented by the increasing order of their vertices.
A -form is a real function on the -element subsets of ; the space carries the inner product . Similarly consists of functions on -subsets ( when ) and of functions on -cells. Writing for the -th vertex of , the co-boundary operators are (for only on ), and the boundary operators are , the sum over vertices with a cell, where is the oriented cell .
The upper, lower and full Laplacians on are
The -cycles are , and the exact forms are ; they are orthogonal complements in . Write and for the orthogonal projections. For vertex sets , is the set of -cells with exactly one vertex in each .
For the operator preserves , and
For every and any pairwise disjoint vertex sets (not necessarily a partition),
The parameter is free; the introduction's Theorem 1.4 (p. 4) is the case , the average degree of a -cell, and is included as a companion item.
The milestones follow the proof of §4.3 and the facts of §§2–3 that it uses:
For the theorem is the Expander Mixing Lemma of graphs. For it shows that a complex whose upper Laplacian has its nontrivial spectrum concentrated near distributes its -cells evenly across any disjoint vertex sets, with a bound that depends on the set sizes only through . The paper uses it to bound the geometric overlap of such complexes from below (Corollary 1.6), and to show that random Linial–Meshulam complexes (Linial–Meshulam 2006) have small discrepancy.
The result is proved in the paper. To the knowledge of this mission, neither it nor the underlying signed simplicial Laplacians with their Hodge decomposition on a complete skeleton has been formalized. The formalization produces the boundary and co-boundary operators, the three Laplacians, the identity for the complement complex, and the projection formula for , all of which are standard in the spectral theory of complexes and reusable well beyond this result.
Each step of the proof is a finite computation, but the steps are sign-sensitive. The count (4.6) relies on the orientation conventions: replaces only the first block of , and the off-diagonal terms of carry the signs that make on neighbouring cells. Proposition 3.2 (1) and (3) are identities between explicit matrices indexed by -subsets that hold only because the skeleton is complete. The spectral step needs the orthogonal decomposition , invariance of under , and the spectral theorem for the restriction. A direct transcription of the graph argument does not apply: the operators act on -forms rather than on functions on vertices, and the expected count is not visible from of alone.
Vertices are Fin n. A complex is the structure Complex n d holding its -cells, so the complete skeleton is built in; forms are EuclideanSpace ℝ over the subtype of -element subsets of Fin n, oriented by the order of Fin n. All boundary and co-boundary operators are defined by their formulas, not as adjoints of one another. The standing assumption is added to every statement. The disjoint sets form an arbitrary pairwise-disjoint family, some possibly empty; no partition and no bound is assumed. The exponent is a real power of a nonnegative real.
is not defined as a maximum or supremum: the goal is stated for every real that bounds for all eigenvalues of on , which is equivalent to the statement for . Trivializing formalizations are ruled out by construction: forms cannot be supported outside -subsets (such a form would be a spurious cycle), an empty eigenvalue set cannot be read through a default sSup value, the boundary operators carry orientation signs, and disjoint families are not confused with partitions.
Contributions are welcome at every milestone, in particular a general library for signed boundary operators on finite complexes, the identity , and the Hodge-type decomposition of forms, which are reusable for the Cheeger inequality of the companion mission and for other work on high-dimensional expanders.
First-order methods (gradient descent, Nesterov's accelerated method, the Heavy-ball method) are the workhorses of large-scale convex optimization, and their worst-case convergence rates on smooth strongly convex functions are classical objects of study. Lessard, Recht and Packard (arXiv:1408.3595v7, SIAM J. Optim. 26(1), 2016, doi:10.1137/15M1009597) recast a first-order method as a linear dynamical system in feedback with the gradient map, and replace the unknown gradient by integral quadratic constraints (IQCs): quadratic inequalities that every gradient of a function in a given class must satisfy along every input sequence. Any rate certified this way holds for the whole function class, and finding the certificate is a small semidefinite program.
The analysis is only as good as the IQCs it is fed. The constraints in Section 3.3 of the paper are what turn the general framework into statements about convex optimization. The weighted off-by-one IQC (Lemma 10) is the one the paper uses for its rate results for the Gradient method, Nesterov's method and the Heavy-ball method on strongly convex functions (Sections 4–5).
Timeline. IQCs were introduced for robust control in continuous time by Megretski and Rantzer (IEEE TAC 42(6), 1997, doi:10.1109/9.587335); the multipliers behind Lemma 9 go back to Zames and Falb (SIAM J. Control 6(1), 1968, doi:10.1137/0306007). Lessard, Recht and Packard (arXiv 2014, journal 2016) adapted the framework to discrete-time optimization algorithms, with exponentially weighted ("ρ-hard") constraints to certify linear rates.
Write and for the Euclidean inner product and norm on . For , the class consists of the functions that are continuously differentiable, strongly convex with parameter ,
and have an -Lipschitz gradient, .
The gradient acts on sequences: for an input sequence in the output is . A reference is a pair with ; it need not be a minimizer. The shifted signals are
Two scalar quantities recur: the sector term and the off-by-one term
Given a rate , a constraint is -hard when its partial sums, weighted by , are nonnegative for every .
For , every reference , every with , every sequence and every ,
Lemma 9 (Zames–Falb IQC, (3.19)), which contains Lemma 8 as the multiplier , and the rate claim of Section 4.4: gradient descent with step on satisfies .
The goal leaves free in : gives Lemma 8 and a weighted sector constraint, so the goal contains both earlier IQCs.
The result. Lemma 10 is the constraint that, combined with the paper's main theorem (Theorem 4), yields the certified linear rates for first-order methods on , including the numerically computed rates for Nesterov's method in Section 4.5 and the robustness analyses of Section 5. The sector IQC alone is too weak for accelerated methods; the off-by-one term carries the extra information about convexity (not just about the gradient's sector) that makes tight certificates possible. The parameter is an additional degree of freedom in the semidefinite program (Remark 11).
Formalizing it. The lemmas are proved on the page, and no machine-checked version is known to exist. A formal proof supplies the reusable inequality layer for IQC-based algorithm analysis: co-coercivity for convex functions with Lipschitz gradient, the sector inequality, and the telescoping bounds (3.16)–(3.18). It also settles a gap in the printed proof: the proof of Lemma 8 uses and , which hold only when , while Lemmas 8 and 10 are stated for every reference. The lemmas remain true for every reference, and the goal is stated in that generality.
The proofs are short but not routine to formalize. Co-coercivity (3.13c) for a convex function with Lipschitz gradient needs a descent lemma and a minimization argument over an auxiliary function; Mathlib has the ingredients but not the statement. The auxiliary function must be shown convex with -Lipschitz gradient, which is not a consequence of the Lipschitz bound on by the triangle inequality alone. The printed proof of Lemma 8 needs , so the general-reference statements need an argument the page does not give. Finally, the passage from -hardness to -hardness reweights partial sums whose individual terms may be negative, and at the weights used on the page are undefined.
EuclideanSpace ℝ (Fin d), so norms are 2-norms; gradients are Mathlib's gradient. is the structure InSmL f m L with fields , , ContDiff ℝ 1 f, StrongConvexOn Set.univ m f, and the Lipschitz bound on gradient f.Proofs of any milestone are welcome independently; (3.13c) and the Abel-summation remark are reusable beyond this mission.
Polynomial optimization problems invariant under permutation of the variables appear throughout global optimization, and their semidefinite (SDP) relaxations, the moment–sum-of-squares hierarchy of Lasserre (2001), grow quickly with the number of variables . Riener, Theobald, Jansson Andrén and Lasserre (arXiv:1103.0486v3, Math. Oper. Res. 2013) show how symmetry reduces the size of these relaxations. Their last section treats a model family in which the reduction is extreme: minimizing one power sum subject to fixed values of the lower power sums.
For this family the paper gives two bounds. A lower bound (Theorem 6.6, the subject of a companion mission) comes from an SDP over an Hankel matrix. The present mission concerns the complementary upper bound, Theorem 6.7, which comes from an SDP in a single real variable whose matrix has size , the number of constraints plus one, independently of . The idea behind it, that candidate optima have at most non-zero coordinates, is the same phenomenon studied in the degree principle for symmetric polynomials of Timofte (2003) and Riener (2012).
Fix and real numbers . For write for the power sum of order . Problem (6.4) is
with standing assumptions and , and optimal value (an infimum, possibly if the constraints are inconsistent, or ).
For a sequence the Hankel matrix of order is . For a monic real polynomial
with complex roots (with multiplicity), the Newton sums are , so . Newton's identities express the through the coefficients and back; in particular determine , so that, once for is imposed, the only free coefficient is , and every later Newton sum is a known polynomial , . For the paper defines
where , for , and for . The constraint is equivalent to the real-rootedness of (Hermite's criterion).
For and ,
and if has an optimal solution with at most non-zero entries, then
Both halves are part of the goal; the equality is what makes (6.7) an exact convex reformulation of (6.4) in the sparse case.
In attack order:
The result. Theorem 6.7 bounds a nonconvex polynomial optimization problem in variables from above by a semidefinite program in one variable with an matrix. Combined with Theorem 6.6 it brackets between two SDP values, and when an -sparse optimum exists, it identifies the optimal value exactly by a problem whose size does not grow with . The milestones are classical facts about univariate polynomials (Newton's identities, Hermite's criterion) that are used far beyond this paper, in real algebraic geometry, the theory of hyperbolic and real-rooted polynomials, and moment problems.
Formalizing it. The inequality has a short printed proof; the equality case has none, so the formalization supplies a complete argument for a stated but unproved claim. Hermite's real-root criterion is, as far as the platform's library search shows, not available in Mathlib, and a formal proof of it is a reusable contribution in its own right. Newton's identities exist in Mathlib for multivariate symmetric polynomials; their form for the coefficients and roots of a monic univariate polynomial, as printed here, is a separate statement. No part of Theorem 6.7 is known to have a machine-checked proof.
The obvious argument for the inequality, sending a feasible to the vector of roots of , needs the roots to be real, and real-rootedness is encoded only through positive semidefiniteness of a Hankel matrix of Newton sums. The step "psd Hankel matrix implies real roots" is Hermite's criterion, a nontrivial classical theorem with no library support. The equality half needs the converse direction of the same criterion together with a construction that the text does not give. Finally, the printed proof starts from "an optimal solution of the SDP (6.7)", which need not exist; the formal statement is about infima and must be proved without assuming attainment.
Points are Fin n → ℝ; is a sequence ℕ → ℝ of which only are read. Both and are infima in EReal over their feasible sets, so an infeasible problem has value and no optimizer is assumed. The Hankel matrix is indexed from : entry is , , which is the paper's . Newton sums of a real polynomial are the real part of over its complex roots with multiplicity (Polynomial.aroots), which is real for real polynomials.
The feasible set of (6.7) is parametrized by the monic polynomial itself rather than by : monic of degree , for , and . Milestone 2 shows that this is a bijective change of coordinates , and for is the paper's by definition. The hypothesis in the goal is the standing assumption of (6.4); with it forces . In milestone 5, is needed because the padding zeros contribute .
Several formalizations would trivialize or falsify the targets and are ruled out: values are never real infima (which are on empty or unbounded sets); is defined by (6.7) with tied to , not by the relaxation (6.6) in which those entries are free and which can have a strictly smaller value; and the equality half is stated in full, not weakened to an inequality.
The needed infrastructure is Vieta's formulas and Newton's identities over Polynomial, Hermite's quadratic form and its signature, and the passage between root multisets and coordinate vectors. All of it is reusable outside this mission; contributions of Hermite's criterion in particular are welcome.
The Heavy-ball method of Polyak, , adds a momentum term to gradient descent. On strongly convex quadratics with curvature between and , a classical eigenvalue analysis gives the step size and momentum that minimise the worst-case linear rate, and with , and the resulting rate matches the lower bound for first-order methods. Practitioners and theorists alike have long asked whether this tuning carries over from quadratics to all smooth strongly convex functions.
Lessard, Recht and Packard (SIAM J. Optim. 2016) built a framework, based on integral quadratic constraints (IQCs) from robust control, that certifies convergence rates of first-order methods by solving small semidefinite programs. Applied to the Heavy-ball method, the certificates degrade sharply once exceeds about 18. Section 4.6 of the paper shows that this is not a weakness of the certificates: the method itself fails. It exhibits a one-dimensional function with , on which the Heavy-ball method with the quadratic-optimal tuning settles into a cycle of period 3 instead of converging to the minimiser. Appendix B proves this for the initial point .
The example is a standard reference point for why momentum methods need an analysis beyond quadratics.
For , the class consists of the continuously differentiable functions that are strongly convex with parameter and whose gradient is Lipschitz with constant . Here .
The counterexample is the function (unique up to an additive constant) with the piecewise-linear derivative (4.11):
Its minimiser is .
The Heavy-ball run with step size , momentum and starting point is the sequence with and the initialization , so . With , the tuning of Proposition 1 gives , , and the run satisfies (B.1): .
The limit cycle (B.3) is , , ; the sequence cycles through . The perturbation of a sequence is ; the matrix governs it near the cycle; and is the distance from the cycle to the nearest transition point of .
In Lean everything lives in the namespace IQCAlg.HeavyBall: gradF is (4.11), hbRun g α β x0 the Heavy-ball run, hbAlpha L m, hbBeta L m the tuning, cyc the cycle, eps x k the perturbation, Pm the matrix , epsBar the margin , and InSmL1 f m L the class on .
With the Heavy-ball run on (4.11) with Proposition 1's tuning for , , from :
In particular the iterates do not converge to the minimiser .
The result itself. The goal shows that tuning a momentum method on quadratics does not transfer to the class it is usually advertised for: a function with condition ratio 25 defeats the Heavy-ball method (the paper reports a cycle for numerically; only is proved). It explains the failure of IQC certificates for Heavy-ball at large and separates Heavy-ball from Nesterov's method, whose accelerated rate holds on all of .
Formalizing it. The paper's proof is complete but terse: the linear system, eleven exact rational iterates, a matrix-power norm bound and an induction keeping all later iterates on the right linear pieces are all left to "one can easily verify". A machine-checked version settles each of these and gives a reusable, fully explicit counterexample for momentum methods.
Every step is elementary, and the difficulty is in making the global argument airtight. The naive argument, that forces perturbations to decay, does not suffice: a perturbation can grow transiently, push an iterate across a transition point or of , and then the linear recursion no longer applies. The proof replaces the spectral radius by the induced norm of , which requires a bound on the largest singular value of an explicit matrix with entries over , and combines it with an induction over blocks of eight indices whose invariant is that the iterates stay on the cycle's pieces. The remaining work is exact rational arithmetic on eleven iterates of a piecewise-defined recursion.
All objects are on ; no measure theory or probability is involved. The conventions:
StrongConvexOn, ContDiff ℝ 1 and an -Lipschitz deriv f; this is the paper's class in dimension one.Real.sqrt, not replaced by and , so the goal is explicitly about the quadratic-optimal tuning; milestone 2 reduces it.Matrix.Norms.L2Operator), the page's induced 2-norm.The goal has no hypotheses: it is a statement about one explicit sequence, so it cannot hold vacuously, and it pins the three limits exactly, which rules out a formalization that only asserts non-convergence or the existence of some cycle. The fixed starting point is exact; floating point never enters.
Contributions are welcome at every milestone. The matrix-norm bound and the exact-arithmetic computation of iterates are independent of each other and of the induction, and can be attacked in parallel. A general lemma converting an eight-step contraction into convergence of a perturbed linear recursion would be reusable beyond this mission.
A chance constraint asks that a decision satisfy uncertain inequalities with high probability. In the setting of Zymler, Kuhn and Rustem (Math. Program. 137, 2013), affine inequalities , whose coefficients depend affinely on , must hold jointly with probability at least . Joint chance constraints appear wherever several safety conditions must hold at once: portfolio and network design, water reservoir operation, production planning under uncertain demand. They are hard for two reasons. Checking feasibility of a fixed requires a multi-dimensional integral, and the feasible set is typically nonconvex (Prékopa 1995). Moreover the distribution of is rarely known; often only its mean and covariance can be estimated.
The distributionally robust version requires the constraint for every distribution consistent with the known first and second moments. A standard tractable inner approximation replaces the probability by a worst-case Conditional Value-at-Risk (CVaR) of a single loss. For a joint constraint this needs the inequalities aggregated into one loss, and the choice of aggregation decides how much is lost.
Timeline. Charnes and Cooper (1959) and Miller and Wagner (1965) introduced chance constraints; Prékopa proved convexity of joint constraints with log-concave right-hand sides. Nemirovski and Shapiro (2006) studied convex (CVaR-type) approximations. El Ghaoui, Oks and Oustry (2003) and Calafiore and El Ghaoui (2006) gave exact SDP and SOCP reformulations of individual robust chance constraints under moment information. Chen, Sim, Sun and Teo (2010) introduced scaling parameters and an SOCP approximation of joint constraints. Zymler, Kuhn and Rustem (2013) showed that the worst-case CVaR of the scaled max-loss admits an exact LMI representation and that, with the scaling parameters free, it is essentially exact.
Let be a random vector in . Fix and a positive definite , and let be the set of all probability measures on with finite second moments, mean and covariance . The second-order moment matrix is
For a measurable loss , a probability measure and , the CVaR is
and the worst-case CVaR is its supremum over .
The data are vectors and scalars for , , with and . The sets of interest are:
The goal makes no regularity assumption on the constraint functions; it holds for all data, all , all , all and all .
The result. The worst-case CVaR approximation is an LMI-representable inner approximation of the robust joint chance constraint for each fixed (Theorem 3.3). Theorem 3.6 says that optimizing over loses at most the boundary between the strict and the non-strict constraint: no tractable family based on the scaled max-loss can be uniformly better. Remark 3.2 of the paper observes that, for well-specified constraints, and differ by a Lebesgue-null set. Together with the inclusions of §3.3, it places the approximation at least as tight as the Bonferroni and Chen–Sim–Sun–Teo approximations and as close to as the strict constraint allows; it is the reason to treat as a decision variable.
Formalizing it. The theorem is proved in the paper; nothing here is open mathematically. None of it is machine-checked. A formal proof requires moment-problem duality for the full moment set (Lemmas A.1 and A.2, which the paper sketches by citing Isii and Calafiore–El Ghaoui), a minimax interchange over a non-compact set of distributions, and the S-lemma, which is available on the platform. Each milestone is reusable: Lemmas A.1 and A.2 are the generalized Chebyshev bounds behind most of moment-based distributionally robust optimization.
The second inclusion is the conservativeness of CVaR, a Markov-type argument. The first inclusion is where the content lies. It requires the worst-case probability of a union of half-spaces to be an attained semidefinite program value, and an S-lemma certificate for each row. The obvious proof applies the S-lemma to every row, but the S-lemma's converse needs a strictly feasible point, which a row with lacks; such rows must be treated separately. Similarly, the SDP representations are stated as existence of a feasible point, so the infima must be shown to be attained. The interchange of the supremum over and the infimum over in (31) cannot cite weak compactness: is not weakly compact, since mass can escape to infinity while the second moments stay fixed.
Fin k → ℝ; matrices in are indexed by Fin k ⊕ Unit with the extra coordinate last; is Matrix.PosSemidef (which includes symmetry); .MomentDRO.Conf definitions), so moments are genuine integrals.Distributionally robust optimization asks a decision to perform well against every probability distribution in an ambiguity set , a family of distributions consistent with partial information about an uncertain parameter . Which kinds of information an ambiguity set can encode decides which models a solver can handle. Wiesemann, Kuhn and Sim (Optimization Online 3757, 2013; Operations Research 62(6), 2014, doi:10.1287/opre.2014.1314) introduce a standardized ambiguity set: distributions of described by one linear expectation constraint and by probability bounds on conic confidence sets. A linear expectation constraint can only fix means. Section 3 of the paper shows that it covers much more, through the Lifting Theorem (Theorem 5): a conic bound on a nonlinear moment is equivalent to a linear constraint on an auxiliary random vector together with an almost-sure conic constraint coupling and . With this result the paper recognizes mean, variance, mean absolute deviation and Huber-loss bounds as special cases of its standardized set.
This mission formalizes assertion (i) of the Lifting Theorem and two of its instances.
A proper cone is a closed convex cone that is pointed () and has nonempty interior; means . Fix a measurable map , a vector , measurable sets and bounds for in a finite index set .
The moment set (momentSet) contains the probability distributions on under which exists, , and for all .
The lifted set (liftedSet) contains the probability distributions on of a pair such that , , and for all .
For a set of joint distributions, the marginal (marginal) is the set of -marginals of its members.
The goal is the set identity for arbitrary measurable , any proper cone and any finite family of measurable confidence sets.
The result. Theorem 5 is what lets the paper's tractable reformulation (Theorem 1, a finite conic system equivalent to a worst-case expectation constraint) apply to ambiguity sets with nonlinear moment information. Without it, the standardized set would describe only first moments and confidence-set probabilities; with it, any moment function whose -epigraph is conic representable can be bounded, including covariance bounds through the semidefinite cone and robust-statistics bounds such as mean absolute deviation. The identity is exact, so worst-case expectations of functions of over and over coincide.
Formalizing it. The theorem is proved in the paper (Appendix A, p. 40), in a few lines that pass silently over measure-theoretic points: existence of expectations, the measurability of the lift, and the transfer of expectations to the marginal. No machine-checked version exists. The formal statement makes the integrability conditions explicit and shows which of them are needed (see below). The same encoding serves the other lifted ambiguity sets of the paper (Examples 2–6, Propositions 2 and 3).
The informal proof is short; the difficulty is in the bookkeeping. The construction direction needs the pushforward of under to be a probability measure with the right expectations and marginal, which requires measurability of and integrability of . The projection direction needs an integral of a vector-valued function to stay in a closed convex cone when the integrand does so almost surely, and needs expectations of functions of to coincide under the joint law and under its marginal. The natural first attempt, reading and as enough to control , fails: can be very negative along the cone and need not have an expectation at all.
Vectors are Fin n → ℝ, distributions are MeasureTheory.Measure with IsProbabilityMeasure, expectations are Bochner integrals, probabilities are μ.real, and is the image under Measure.map Prod.fst. The index set is Fin nI (0-based). The proper cone is a local predicate IsProperCone (closed, contains , closed under addition and nonnegative scaling, pointed, nonempty interior), and is y - x ∈ K.
Committed conventions and deviations from the page:
Integrable clauses; without them Lean's integral of a non-integrable map is , and the moment set would contain every distribution with whose has no expectation, a trivializing formalization that these clauses rule out.A sanity file (not part of the proposal) proves milestone 2 and exhibits Dirac members of both sets, so the hypotheses are satisfiable.
Contributions welcome: proofs of the milestones and goal, and general lemmas on pushforward lifts and conic expectation bounds, which are reusable for the other lifted ambiguity sets of the series.