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?
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.
Two-stage stochastic linear programs model decisions taken in two steps: a first-stage decision is fixed before an uncertain parameter is observed, and a second-stage (recourse) decision adapts to afterwards. They underlie capacity planning, inventory and network design. In practice the distribution of is known only through samples . Distributionally robust optimization replaces the unknown distribution by the worst case over an ambiguity set; a popular choice is a Wasserstein ball around the empirical distribution, because it contains the true distribution with high probability and yields out-of-sample guarantees (Mohajerin Esfahani and Kuhn, 2018).
Hanasusanto and Kuhn (arXiv:1609.07505, Operations Research 66(3), 2018) study when the resulting two-stage problem can be solved exactly. Section 3 of their paper gives a copositive reformulation for the 2-Wasserstein ball (the subject of a companion mission). Section 4, the subject of this mission, shows that when the uncertainty enters only the constraints of the recourse problem and the ball is a 1-Wasserstein ball with a polyhedral reference distance, the whole problem is a linear program.
Let and be the first-stage cost and feasible set, the second-stage cost, the recourse matrix, and , affine functions of . The recourse value at is
The uncertainty affects only the constraints (in the paper's notation, ), and there is no support constraint: . The problem has sufficiently expensive recourse if some satisfies .
For scaling parameters the reference distance is with
Moving a unit of mass in the positive direction of coordinate costs , in the negative direction . The 1-Wasserstein ball consists of the probability measures on whose optimal transport cost to under is at most . The worst-case expectation and the two-stage problem (1) are
The dual norm of (31) is .
For and every , equals the optimal value of the linear program
and consequently problem (1) has the optimal value of (32) minimized jointly over and the other variables with added to the objective.
Theorem 6 shows that the two-stage distributionally robust linear program over a 1-Wasserstein ball, which is a priori an optimization over infinitely many distributions, has a linear-programming reformulation with blocks of variables and constraints. It covers distributionally robust least-absolute-deviation regression (Example 2 of the paper), where the reformulation becomes the empirical loss plus a dual-norm regularizer, and it contrasts with the paper's Theorem 7, which shows that for -norm reference distances with the same problem is NP-hard.
The result is proved in the paper; there is no machine-checked proof. A formalization adds a verified chain from the measure-theoretic worst-case expectation to a finite linear program, including the conventions the paper leaves implicit: the extended-real values ( may be , and (32) may then be infeasible), the restriction , and the first-stage cost in the objective.
Each step of the proof is classical, but the chain crosses several regimes. Theorem 1 is a Wasserstein strong duality result, and here it is applied to a loss that is convex, possibly on part of , and not upper semicontinuous, with a cost that is not symmetric; the standard published duality theorems assume an upper semicontinuous real-valued loss or a metric. The passage to (33) interchanges a supremum over with an infimum over the dual-norm ball and must handle the case where the dual recourse polyhedron is unbounded. Finally, every equivalence must hold in the extended reals: an argument that tacitly assumes finiteness proves a statement that fails exactly when the dual polyhedron has a recession direction.
Vectors are Fin n → ℝ, samples are ξhat : Fin I → (Fin K → ℝ) with , and carries its product (Borel) σ-algebra. and are affine maps. The transport cost is the platform definition RWPI.SqrtLasso.transportCost (couplings with first marginal , second ), the empirical distribution is WassersteinDRO.Duality.empiricalDistribution, and expectations of the extended-real recourse value use WassersteinDRO.Duality.erealExpectation (value whenever the positive part has infinite integral). Every optimal value is an extended-real infimum or supremum over its feasible set; no Bochner integral and no real-valued sInf/sSup is used.
Conventions made explicit, with reasons:
A formalization in which is defined by (6), (33) or (32), in which the gauge is secretly symmetric, or in which expectations are Bochner integrals (zero for non-integrable functions) would make the goal trivial or different; the definitions here exclude each of these.
A complete development needs Wasserstein strong duality for a lower semicontinuous loss and cost (with a disintegration of couplings to pass to the moment problem (5)), LP strong duality and Farkas' lemma in the extended-real form, and a minimax interchange over a compact dual-norm ball. Wasserstein duality for general costs and extended-real LP duality are reusable well beyond this mission; contributions of either 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.
Stochastic gradient descent (SGD) minimizes an objective that is an expectation, , by stepping along the gradient of one randomly drawn component at a time. It is the workhorse of large-scale machine learning, where is an average loss over training examples, and it also contains the randomized Kaczmarz method for linear systems, where each component is a single squared residual (Strohmer & Vershynin 2009).
For smooth, strongly convex objectives, the question is how fast a fixed step size drives the iterates to the minimizer , and how the rate depends on the smoothness constants of the components. Bach & Moulines (2011) showed that an iteration count scaling with the squared conditioning suffices. Needell, Srebro and Ward (arXiv:1310.5715v5, Theorem 2.1) replaced this by a dependence that is linear in the uniform conditioning . Their theorem is the base of the rest of the paper: Corollary 2.2 (choice of step size), the importance-sampling results of Section 3 (weighting components by ), and the Kaczmarz rates of Section 5 are all derived from it.
Timeline:
Let be a probability distribution, the source distribution, on an arbitrary measurable index space . Let be a real Hilbert space (for example with the Euclidean norm ), and let , , be a family of functions. The objective is
and is a minimizer of . The paper assumes:
The number is an almost-sure upper bound on , and the residual is
which vanishes exactly when is a stationary point of every component (the realizable case).
The SGD iterates with fixed step size start at and follow (2.2):
where are drawn independently from . The iterate is a random point that depends on . In Lean these objects are objective D f, residual D f xstar, iidLaw D (the law of the index sequence) and sgdIter f γ x0 k ω in the namespace SGDKaczmarz.SGD.
If , then for every
where the expectation is over the sampling of . The constants are the paper's; nothing is left unfixed.
In the order of the paper's proof (Appendix A):
The bound has two terms: a contraction at rate and a floor proportional to . Choosing to balance them (Corollary 2.2) gives an iteration count of order , linear rather than quadratic in the conditioning. In the realizable case it is a pure linear rate. Reweighting the distribution by turns into the average (Section 3), and specializing to least squares yields convergence rates for randomized Kaczmarz with uniform, weighted and hybrid row selection (Section 5). These consequences are stated in terms of Theorem 2.1, so a formal version of the theorem is the prerequisite for formalizing any of them.
The result is proved on paper (Appendix A.2). The work here is to formalize that proof: co-coercivity in a Hilbert space, differentiation of under the expectation, and the passage from a conditional one-step bound to the unconditional bound over an i.i.d. sequence. To our knowledge no machine-checked proof of Theorem 2.1 exists. The platform has formal results on projected SGD with decaying steps and on the finite-sum Kaczmarz iteration, which state different results.
The one-step algebra is routine once co-coercivity is available. What is hard is making the expectation rigorous. On the page, "" in the recursion is an expectation over the index alone, with held fixed. Iterating it requires that be a measurable function of , that be independent of it, and that expectations of possibly non-integrable nonnegative quantities be handled without junk values. The unbiasedness step is a differentiation under the integral sign in a possibly infinite-dimensional space, and it needs a dominating bound that comes from the almost-sure bound on together with the finiteness of . A tempting shortcut, assuming for every , gives only the realizable special case and is not the theorem.
gradient. Assumption (1) is LipschitzWith (L i) (gradient (f i)) with L i : ℝ≥0, together with Differentiable ℝ (f i) and ConvexOn ℝ Set.univ (f i) for every .gradient (objective D f). Differentiability of is not assumed separately: it follows whenever (milestone "unbiasedness").γ * supL < 1 (and as γ * supL ≤ 1), with and .Measure.infinitePi of the index sequence, the second over . A non-integrable iterate therefore cannot satisfy the bound vacuously, and makes the right side , which is the paper's meaning.Infrastructure that a complete development needs, and that is reusable beyond this mission:
Measure.infinitePi.Contributions of any of these as separate lemmas are welcome.
Many polynomial optimization problems are invariant under permuting the variables: the objective and the constraints are symmetric polynomials. Lasserre's moment–sum-of-squares hierarchy solves such problems by a sequence of semidefinite programs whose size grows quickly with the number of variables and the degree, and symmetry is the main tool for shrinking them. Riener, Theobald, Jansson Andrén and Lasserre (arXiv:1103.0486, Math. Oper. Res. 38(1), 2013, doi:10.1287/moor.1120.0558) develop symmetry reductions of the hierarchy and, in their Section 6, a second route: instead of reducing the moment matrices, describe the orbit space of the symmetry group directly by polynomial inequalities, following Procesi and Schwarz, and optimize over it.
For the symmetric group the orbit space is described by a single Hankel matrix of power sums. This mission formalizes the lower bound that results for a basic family of symmetric problems: minimize one power sum subject to prescribed values of the lower power sums.
Fix and a point . The power sum of order is ; note .
The problem (6.4). Given with , , and prescribed reals , minimize over all with for . Its optimal value is written .
The Hankel matrix. For a real sequence and , .
The matrix (6.1). For a finite group acting on with fundamental invariants , the matrix has -invariant entries . For the symmetric group with , is the Hankel matrix of power sums.
The SDP (6.5). For and ,
The variable is the sequence ; the constraint is a single linear matrix inequality of size .
For and :
(a)
(b) If , put , and . If , then
The goal is the conjunction of (a) and (b).
Part (a) bounds a nonconvex polynomial problem of degree in variables by a semidefinite program with one matrix variable, whose size does not depend on . Part (b) evaluates the bound in closed form in the even case , where the SDP reduces to a single scalar constraint on the free moment . Together with the upper bound of Theorem 6.7 (a separate mission of this series), it brackets the optimal value of power-sum problems, which appear in moment problems, in the analysis of symmetric inequalities, and as test cases for symmetry-adapted relaxations.
The paper's proof is a few lines, citing the Procesi–Schwarz theorem and Schur's complement. A formal development makes each step explicit: the positive semidefiniteness of the Hankel matrix of power sums of a real point, the principal-submatrix argument, and the Schur complement for a Hankel block. It also fixes a misprint: the bound of (b) is printed as without the inverse, which is false (for , , the minimum is but the printed bound is ). No machine-checked version of this result is known to exist.
The individual steps are classical, and the difficulty is in the bookkeeping. The paper reaches (a) through the Procesi–Schwarz description of the orbit space, a deep result stated for general finite groups; the formal route needs only the positive semidefiniteness of the Hankel matrix of power sums of every real point, which the page leaves implicit. The identity requires computing partial derivatives of power sums with the right index shifts. In (b), must be identified with a block matrix whose top-left block is with , which needs the prescribed values and a reindexing of as . The extended-real values must be handled: the problem can be infeasible (value ), and for odd unbounded below.
Lean namespace SymPolyOpt.PowerSumLB. Conventions:
x : Fin n → ℝ; is powerSum x j, so powerSum x 0 = n.γ : ℕ → ℝ of which only are read. The page's "" in (6.4) is read as .EReal: for an infeasible problem, possibly . They are compared only by ≤.s : ℕ → ℝ; its entries past are unconstrained and irrelevant since .MvPolynomial.psum and pderiv.Disclosed changes relative to the page:
Trivializing formalizations are ruled out: real-valued infima (which return on empty or unbounded sets) are not used; is an SDP over arbitrary sequences, not over power-sum vectors of points, so (a) is not definitional; the constraint is kept; Lean's junk inverse of a singular matrix is excluded by the positive-definiteness hypothesis; and the printed false bound is not stated.
Needed infrastructure: Mathlib's Matrix.PosSemidef, Matrix.PosDef, PosSemidef.submatrix and the Schur-complement lemmas for block matrices (fromBlocks). A reusable lemma that Hankel matrices of power sums (and, more generally, of moments of a finitely supported measure) are positive semidefinite would serve other moment-problem missions. Contributions to any milestone are welcome.
Linear-quadratic (LQ) control is the setting in which stochastic optimal control has a closed-form answer: the optimal control is a linear feedback of the state, and the feedback gain comes from a Riccati differential equation. In the mean-field version, the expectation of the state and of the control appear in the dynamics and in the cost. Mean-field SDEs go back to Kac (1956) and McKean (1966) as models of interacting particle systems. A cost containing can penalize the variance of the state, which is what is wanted when the optimal state should not be too sensitive to the noise (mean–variance portfolio selection is the standard example). With such a cost the problem is no longer a classical LQ problem: the weights on may be negative definite, and the cost is not an expectation of a function of the state path, so the classical Riccati theory does not apply as it stands.
J. Yong (SIAM J. Control Optim. 51(4), 2013, pp. 2809–2838) solved the problem with deterministic coefficients. He derives the optimality system, a linear mean-field forward–backward SDE, and decouples it with two Riccati equations. One governs the deviation , the other the mean . The optimal control is then an explicit state feedback.
Timeline:
Let be a complete probability space carrying a one-dimensional standard Brownian motion , and let be the natural filtration of augmented by the -null sets. Fix a horizon . An admissible control is an -progressively measurable with ; the set of them is . For the state solves
with deterministic matrix-valued coefficients. The cost is
Problem (MF-LQ): minimize over . The assumptions are:
The weights themselves need not be semidefinite.
With and , the two Riccati equations are
with . Write and .
Under (H1)–(H2), (4.8) and (4.9) have unique solutions and on . The closed-loop system obtained by substituting
into the state equation has a unique solution . With and the explicit , the 4-tuple solves the optimality system, and is optimal. Moreover
The Woodbury identity used on p. 2826 is already proved on the platform (FamousTheorems.woodbury_identity) and is referenced.
The result. Theorem 4.1 reduces a mean-field stochastic control problem, whose state law enters the dynamics, to two matrix ODEs. The optimal control is computable offline: integrate and backward, then feed back the state and its mean. The value is explicit, so cost comparisons between the mean-field problem and its classical counterpart become comparisons between Riccati solutions; §5 of the paper does exactly this for variance-penalized costs. When all barred coefficients vanish, and the classical stochastic LQ feedback is recovered.
Formalizing it. The result is proved, not open; this mission formalizes the known proof. No continuous-time stochastic LQ theorem exists on the platform. The mission builds on the published stochastic calculus of Peng1990.SMP.Stochastic (Itô integrals, SDE and BSDE solutions, ) and adds a reusable mean-field LQ setting, matrix Riccati equations in integral form, and a verification theorem. None of the statements has a machine-checked proof yet.
The Riccati equations are nonlinear matrix ODEs with only coefficients. Local existence is routine, but global existence on needs an a priori bound, which a local fixed-point argument does not give. The bound comes from the control interpretation of the equation, and it requires semidefiniteness of . The second equation contains , and its quadratic term is only controlled when , which in turn needs . Its "state weight" is semidefinite only through the identity of milestone 7, even though itself may be negative definite. On the stochastic side, the verification step (milestone 9) and the duality arguments of Theorems 3.1–3.2 apply Itô's product rule to and to for processes driven by the same Brownian motion, with an absolutely continuous (not differentiable) . Itô's formula is not yet available on the platform: it is the open goal EthierKurtz.ito_formula. Existence in Proposition 2.8 needs a minimizer of a coercive continuous quadratic functional on the Hilbert space .
States are Fin n → ℝ, controls Fin m → ℝ, time is ℝ≥0, and the horizon satisfies . The probability space is complete. is Peng1990.SMP.IsStdBrownian with one coordinate, and is ReflectedBSDE.Existence.augmentedFiltration. is the Bochner integral of the solution itself. Every mean-field term is a closure over the process being solved for, never a free deterministic input. Solutions of the forward and backward equations are the published SolvesSDE/SolvesBSDE notions: progressive, square-integrable, with the integral identity at each almost surely. Controls and -components are identified up to -null sets.
Other conventions:
Matrix.inv is a true inverse. For (4.9), follows from (H2) once .A formalization in which the mean is an independent input, or in which a Riccati "solution" may use the junk value of a singular inverse, would trivialize the problem. Both are ruled out by the definitions above. A sorry-free sanity file shows that (H1)–(H2) hold for data with negative definite, and that the Riccati class is non-empty.
Contributions are welcome on all of the following:
An online learner repeatedly chooses a point, observes a loss, and is judged by the difference between its accumulated loss and that of a fixed competitor. In practice, an available learner may operate on a broad feasible set , while the application permits decisions only in a smaller set . Replacing each output by a feasible point changes the learner's losses, so its existing regret guarantee no longer directly applies. Chapter 12 of Orabona's text develops reductions that use the learner as a black box: they change the feedback sent to it and recover a guarantee for the constrained predictions.
The chapter treats Euclidean and other norms, Bregman projections, sleeping experts, and the separation of magnitude from direction. This mission focuses on its first general construction, Theorem 12.5. It is useful when the internal update of the learner is unavailable or when a solver wants to reuse one unconstrained algorithm across several constraint sets. The theorem gives four explicit surrogate losses and an explicit bound on their subgradient norms. Orabona, Chapter 12 also explains how its distance based construction relates to regret matching on the simplex.
Work in a finite-dimensional real vector space with an arbitrary norm . Its continuous dual consists of real-valued linear functionals; is the pairing and is the dual norm. Let , with nonempty, closed, and convex. The distance to and the generalized projection are
The minimum exists under these assumptions. A projection need not be unique for an arbitrary norm; the construction accepts any . In round , an underlying learner outputs , the reduction predicts , and the environment reveals a real-valued loss . Choose a subgradient of at that satisfies the subgradient inequality for competitors in . Choose any full-space subgradient . For a fixed , the constrained regret is
The surrogate losses are functions passed back to the learner. Their four formulas are the distance-penalized linear loss, its linear form using , a distance penalty activated only when , and that activated penalty's linear form. Each is defined on the ambient space, then used on . The projection rule and the selected subgradients are the only information the reduction needs from a run.
For each of the four choices in Theorem 12.5 and every , the goal is
The theorem is pathwise: it applies to any sequence of predictions that the underlying learner could produce. No particular learner or regret rate is built into the target. Equation (12.2) isolates the linearized regret term that each surrogate must cover. The four clauses of Lemma 12.2 establish convexity, the exact Lipschitz constant, the zero subgradient on , and the subdifferential characterization outside .
The companion clause of Theorem 12.5 says that every full-space subgradient of a surrogate at a point of satisfies
The factor is part of the printed result. It applies to all four choices, including the branches at which the activation term vanishes.
The result transfers a regret guarantee from an algorithm working on to feasible decisions in through a loss transformation. The norm bound makes this transfer quantitative for algorithms whose guarantees depend on subgradient magnitudes: the new losses have controlled scale. Lemma 12.2 is reusable apart from online learning, because it describes distance and subgradients for a closed convex set in any finite-dimensional normed geometry.
Orabona presents these as established mathematical results in Theorem 12.5 and Lemma 12.2. The work here is to give them auditable Lean statements and, subsequently, machine-checked proofs. The chapter's Bregman projection, sleeping-experts, and magnitude/direction reductions are separate results; this proposal leaves them for later missions or additions. A proof of the present goal would make the first black-box reduction reusable without depending on a specific unconstrained learner's implementation.
Simply projecting into leaves an extra term in the linearized regret: the old learner was evaluated at while the actual loss was incurred at . An arbitrary correction to the feedback can cover that term while destroying convexity or greatly enlarging gradients. The four formulas balance both requirements, and the two activated formulas must also handle the boundary case , where a normalized direction would otherwise divide by zero. Generalized projections create another issue: an argument cannot silently assume one canonical nearest point when the norm is not Euclidean.
Lean uses a finite-dimensional real normed space and represents dual vectors as continuous linear functionals. Their operator norm is the book's dual norm. The distance is Metric.infDist; nonemptiness keeps its value meaningful, and closedness plus finite dimensionality supplies an attained minimum. Projection is a relation, so all valid choices are covered. Sequences start at index ; index is unused, and the horizon is explicitly at least one. The original losses are real-valued on the ambient space, with the subgradient inequality required only for comparators in . The distance and surrogate subgradients use the full-space inequality. This matters when has empty interior: a relative subgradient on can have an arbitrary normal component and would make the printed norm bound false.
The underlying algorithm is abstracted by its sequence ; its surrogate regret is exactly the sum on the right of the goal. is allowed to be strictly larger than , so the statement retains the constraint-reduction content. The normalized direction in the third and fourth surrogates appears only in the branch with , which implies . Contributions toward the distance-function lemmas, the surrogate inequalities, and the gradient bound all support the goal. The same geometric definitions can also support later reductions based on other projections.
In online learning, a learner chooses a point before seeing each round's loss. Ordinary regret compares the learner with one fixed point chosen after all rounds. That comparison can be too coarse when a useful action changes over time. A portfolio allocation, a prediction rule, or an operating point may need to move after the environment shifts. Dynamic regret compares the learner with a specified sequence of feasible points, one for each round. The sequence is allowed to move, but its movement appears explicitly in the bound. Chapter 14 of Orabona's Online Learning: A Modern Introduction Using Convex Optimization develops this comparison, then studies strongly adaptive and tracking regret. This mission isolates its first capstone, Theorem 14.2.
The result extends the book's earlier analysis of online mirror descent to changing comparators. As the chapter explains, a moving comparator can achieve a smaller cumulative loss than any single fixed point, so a dynamic bound answers a stricter performance question. The bound also makes its own limit clear: frequent or large comparator changes cost more. The chapter relates this framework to earlier work on drift in online learning; the formal target here is the precise statement in the pinned arXiv version, with its explicit constants and final Bregman term. Source, Chapter 14, pp. 227–229.
Let be a finite-dimensional real normed space, , and a nonempty closed convex feasible set. On round , the learner plays , receives a real-valued loss , and selects a subgradient at . A comparison sequence consists of arbitrary points in . The dynamic regret is
The path length of the comparison sequence is the total distance between successive points:
It is zero for a constant sequence. The path starts at round two, so neither nor an artificial first movement enters the claim. The norm on is arbitrary. Its dual norm on continuous linear functionals is written .
Online mirror descent uses a differentiable regularizer and its Bregman divergence
At each round, the next point minimizes over , with one constant step size . The regularizer is closed and -strongly convex, with , on the stated domain. Its derivative must be evaluated at interior points of . For a horizon , the theorem measures the range of the gradients seen along the run by the finite maximum
The maximum includes , at which the difference is zero, and stops at . These conventions are the ones in Definition 14.1 and Theorem 14.2.
The first milestone is the inequality part of Lemma 6.10. For each feasible comparator, one OMD update controls the loss difference by a decrease in Bregman divergence plus a quadratic dual-norm term. The milestone records the book's whole inequality chain, including the intermediate term that exposes the change in the iterate. It is the local estimate used at every round of Theorem 14.2. Lemma 6.10, p. 67.
The second milestone is the display in the proof of Theorem 14.2 immediately before the final choice . It keeps that additional comparator free and shows the gradient-difference sum explicitly. This intermediate statement is useful for inspecting the sign and time index of each comparator shift. Proof of Theorem 14.2, pp. 228–229.
The goal is the full bound of Theorem 14.2:
It applies to every feasible comparator sequence, including a constant one. The negative terminal divergence is part of the target. Retaining it makes the statement match the source and preserves information for later use. Theorem 14.2, p. 228.
The theorem quantifies how much a comparator may move before its performance becomes hard to match. The cost of movement is linear in the path length and scaled by the regularizer-gradient range . With a bounded dual norm for the observed subgradients and a suitable constant step size, the chapter derives a square-root dependence on the horizon for slowly moving sequences. A static comparator has path length zero and recovers the familiar mirror-descent setting. The bound also applies to arbitrary norms and regularizers, so it is not limited to Euclidean projection. Discussion after Theorem 14.2, p. 229.
The mathematical result is proved in the book. The remaining task is to give its exact assumptions, update rule, intermediate inequality, and final inequality machine-checked proofs. The already published Bregman definition supplies a reusable representation of ; the new run, path-length, and gradient-maximum definitions supply the chapter's missing interface. Those definitions can support later formalizations of tracking regret and other moving-comparator results. No proof of the present chapter result is claimed by these draft statements.
For a fixed comparator, the Bregman terms from successive rounds line up directly. With changing, they do not: each transition changes the first argument of . The resulting correction depends on differences of regularizer gradients, and its time index must agree with the path-length sum. A simple replacement of the static comparator by in a static regret theorem therefore leaves an unaccounted term. The terminal point is also essential to the full telescoping statement. The mission asks for the book's exact constant and terminal term rather than only an asymptotic rate.
The Lean model uses a finite-dimensional real normed space. Losses and the regularizer are real-valued on their evaluated domains; the feasible-set and domain predicates represent the book's extended-real convention outside those domains. Closedness of the regularizer is represented by a closed epigraph over . Subgradients are continuous linear functionals, so their operator norm is the dual norm. The run predicate represents every admissible subgradient and argmin choice for Algorithm 6.1; it also carries the required membership of in . The run is a predicate on sequences, not a selected canonical sequence.
The book's round labels start at one. Index zero is unused. The horizon is at least one, and are positive. These conditions keep the finite maximum nonempty and every denominator meaningful. The subgradient condition is relative to , which is sufficient for the theorem's comparisons and slightly weaker than the book's full-space subgradient convention. This choice is disclosed in the item statements. The comparator sequence is universally quantified through its feasibility condition; it is never restricted to a constant sequence or assumed to satisfy the conclusion. The definitions and theorem statements invite proofs of the one-step inequality, the summed estimate, and the final bound, as well as reusable results about Bregman divergence on arbitrary normed spaces.
Many operational decisions are linear programs whose cost vector is uncertain but predictable from side information: routing with travel times that depend on weather and time of day, procurement with prices that depend on market signals, assignment with costs that depend on observed features. Contextual linear optimization (CLO) formalizes this: observe features , choose a decision in a polytope , pay for an unobserved random cost vector .
Two families of data-driven methods compete. Estimate-then-optimize (ETO) fits a regression and then solves the linear program with the estimated costs. Integrated methods (for example the SPO+ approach of Elmachtoub and Grigas, 2022) choose a decision rule by minimizing the empirical decision cost directly over a policy class, on the argument that a regression fit ignores how its errors affect decisions. Hu, Kallus and Mao (arXiv:2011.03030v3, Management Science 2022) show that, under a margin condition on the problem, the comparison goes the other way: ETO attains faster regret rates than any method that only uses a policy class.
This mission formalizes their ETO upper bound, Theorem 8. It is the third of a three-mission series on the paper; the first formalizes the upper bound for empirical risk minimization over a policy class (Theorem 6) and the second the matching lower bound for policy-class methods (Theorem 7).
Write for Euclidean space with inner product and norm .
the extra cost of the best suboptimal vertex; otherwise .
It always holds with ; larger means less mass near dual degeneracy.
In Lean the polytope is FastCLO.ETO.Polytope, the distribution is FastCLO.ETO.Instance (the law of and the conditional law of given ), and optVal, Zstar, gap, NoiseCond, IsPlugIn and regret are the objects above.
Fix and . There is a constant depending only on these such that, for every instance satisfying the noise condition, every , every and every estimator with
the plug-in policy satisfies
The constant is existential, as on the page; the proof gives an explicit value, but the goal does not commit to it.
The milestones are the displayed steps of the paper's proof (Appendix A.5, p. 30), in order:
For well-specified least squares regression, is of order up to a logarithmic factor (Corollary 4 of the paper), and Theorem 8 gives regret of order up to logarithms. Theorem 7 of the same paper shows that no algorithm that only uses a policy class of Natarajan dimension can beat in the worst case over such instances. Since for every , the two results separate ETO from integrated methods when the regression model is well specified. This runs against the common intuition behind end-to-end learning. The noise condition is the CLO analogue of the Tsybakov margin condition in classification (Tsybakov, 2004): the gap plays the role of the distance of the regression function from the decision boundary.
The result is proved in the paper; as far as is known it has not been machine-checked. Formalizing it fixes the exact hypotheses (which quantifiers the tail condition carries, what "universal" means for , and the measurability the regret integral needs) and yields reusable pieces: the extreme-point argument behind the implication display and the peeling bound in .
The obvious argument bounds regret by , which gives only the rate and ignores the noise condition (this is Theorem 4 of the paper). The faster rate needs two things the naive bound does not use. First, a wrong decision at is possible only where the gap is positive and at most a multiple of the estimation error. This uses that plug-in decisions are extreme points, so a strictly suboptimal decision is at least worse than optimal; it requires finiteness of , which must be proved for an H-polytope. Second, the error must be controlled pointwise in , with sub-Gaussian tails over the data, and combined with the noise condition shell by shell, through a Fubini exchange between the data and the feature.
EuclideanSpace ℝ (Fin k). The polytope bundles , , , nonemptiness and the bound . The distribution is a probability measure on features and a Markov kernel with ; , and the data law is the -fold product of .Nesterov's accelerated gradient method minimizes a convex function with -Lipschitz gradient at the rate , which is optimal among first-order methods. For a -strongly convex the method with the generic momentum coefficient does not exploit the strong convexity: Su, Boyd and Candès show in §4.2 of arXiv:1503.01243 that its rate stays polynomial. Linear convergence is available with the momentum , but this requires knowing , which is rarely available in practice.
Restarting is the practical remedy. O'Donoghue and Candès (2013) proposed gradient restarting: reset the momentum whenever the objective increases. It is observed to recover linear convergence, but no rate was proved for it. Section 5 of Su, Boyd and Candès proposes a variant, speed restarting, which resets the momentum when the speed of the iterates stops increasing, and proves a linear rate for its continuous-time limit. This mission formalizes that result, Theorem 10 of the paper, and the lemmas it rests on.
Write with the Euclidean norm. A function is in if it is convex and continuously differentiable with . It is in if it is continuously differentiable and is convex. The class with is the standing assumption of the whole mission. A minimizer is written and ; the ratio is the condition number.
The Nesterov ODE is
the continuous-time limit of Nesterov's scheme with step size tending to zero. The paper's Theorem 1 shows it has a unique solution in . In Lean a solution is a pair with (IsSolution f 3 x₀ X V).
The speed restarting time of the solution from is
the first time at which the speed decreases (restartTime; the set is restartSet).
The speed restarted ODE (29) replaces by , where is the time since the latest restart . Its solution starts at , follows (3) from for time , then follows (3) from for time , and so on. If a restart point is a minimizer the trajectory stays there. In Lean this is the predicate IsSpeedRestarted f x₀ Xsr.
There are positive constants , depending only on , such that for every , every and every ,
The constants are left unspecified, so the goal survives improvements of them.
For one unrestarted solution of (3), with :
Theorem 10 is a linear convergence guarantee for a momentum method that does not need : the restart rule only watches the speed. The paper presents it as a new result; gradient restarting has no comparable theorem. It also gives a framework for analyzing restart rules: each restart decreases the gap by a factor depending on (Lemma 12), and restarts happen at a rate bounded below (Lemmas 13 and 25). Section 5.3 of the paper reports that the discrete analogue of the scheme (Algorithm 1) converges linearly in experiments.
The results are proved in the paper, but not formalized anywhere to our knowledge; the platform has no statement about restarting the Nesterov ODE. The formal work is the full proof, in particular the analysis of (3) near its singular point . Sharper constants are of interest: the paper conjectures that for a large class of , which would improve , and the generalization to friction with mentioned after Theorem 10 is a natural further target.
The ODE (3) is singular at , so the standard Picard–Lindelöf theory does not apply there, and the small-time estimates (Lemma 11, (30), Lemma 25) must control the solution uniformly up to , where the friction coefficient is unbounded. Lemma 11 bounds a supremum by a quantity that involves the same supremum; this argument needs a separate proof that the supremum is finite.
The speed restarting time is defined as a supremum, and neither nor follows from the definition. The restarted trajectory is assembled from infinitely many segments, and the number of restarts before time needs a lower bound. The obvious route through the rate of the unrestarted ODE gives only a polynomial rate, because it does not use strong convexity in a way that survives the restarts.
is EuclideanSpace ℝ (Fin n), is Mathlib's gradient, is an NNReal, and is the paper's literal definition. The classes , and the solution predicate of (3) come from the series' shared definitions (NesterovODE.WellPosed.Setting, NesterovODE.StrongCvx.Setting); the speed restarting time and the restarted trajectory sit in this mission's Setting definition, namespace NesterovODE.Restart.
Conventions the formalization commits to:
sSup is on an empty or unbounded set. Lemma 25 is stated as membership of in the set defining , and Lemma 13 as a bound on every element of that set, so neither can hold through this junk value.A complete development needs the analysis of (3) at (also the subject of mission I of this series), monotonicity arguments from derivative signs, and properties of strongly convex functions with Lipschitz gradient. The last two are reusable beyond this mission. Proofs of any milestone, and statements with explicit constants, are welcome.
Phase recovery (also called phase retrieval) asks to reconstruct a complex signal from the magnitudes of linear measurements of it, the phases being lost. It arises wherever detectors record intensities only: X-ray crystallography, diffraction imaging, astronomy and optics, where a sensor measures and not . The classical algorithms are alternating projections of Gerchberg–Saxton type (Gerchberg and Saxton, 1972; Fienup, 1982), which are fast but non-convex and can stall at stationary points that are not solutions.
Two convex relaxations change this picture. PhaseLift (Chai, Moscoso and Papanicolaou, 2011; Candès, Strohmer and Voroninski, 2013) lifts the signal to the rank-one matrix and relaxes the rank constraint to a trace minimization; for random Gaussian measurements it provably recovers with high probability (Candès and Li, 2014). Waldspurger, d'Aspremont and Mallat (arXiv:1206.0102v3, Math. Programming 2015) instead separate amplitude and phase and obtain PhaseCut, a semidefinite program with the structure of the Goemans–Williamson MaxCut relaxation, for which MaxCut algorithms (block coordinate descent, rounding) apply. The question this mission formalizes is how the two relaxations compare in the noiseless case.
Timeline. An earlier version of the paper showed that PhaseLift tightness implies PhaseCut tightness; Voroninski (2012, working paper, cited in arXiv:1206.0102v3, §4.3) reversed the argument under additional assumptions. Version 3 of the paper (2013) introduces the refined program PhaseCutMod and proves that, for injective , PhaseCutMod is tight whenever PhaseLift is (Corollary 4.3).
Fix a measurement matrix with rows , and a vector of amplitudes . The phase recovery problem (1) is
i.e. for every . Write for the Hermitian matrices and for positive semidefiniteness. When is injective, is invertible and the pseudoinverse is ; is the orthogonal projector onto the range of . With the diagonal matrix of the , set
The three programs are
PhaseCutMod selects, among the optimal points of PhaseCut (which in the noiseless case are exactly its points with ), one of minimal . A relaxation is tight when it has a unique optimal solution and that solution has rank one. The two lifted programs are linked by the map
In Lean these objects are PhaseCut.Tight.pinv, Mmat, Bmat, Phi, IsSolvable, phaseLiftFeasible/phaseLiftOptimal, phaseCutFeasible/phaseCutOptimal, phaseCutModFeasible/phaseCutModOptimal and IsTight.
If is injective, for all , and (1) has an exact solution, then
The statement fixes no constants and no probabilistic model: it is a deterministic comparison of two programs, valid for every and meeting the three hypotheses.
The result. Corollary 4.3 says that the MaxCut-type relaxation, once refined to PhaseCutMod, is never worse than PhaseLift at exact recovery: every recovery guarantee proved for PhaseLift (for instance the Gaussian-measurement results of Candès–Strohmer–Voroninski and Candès–Li) transfers to PhaseCutMod. Since PhaseCutMod can be approached by solving PhaseCut with replaced by for small , the algorithms designed for PhaseCut (greedy and block-coordinate SDP solvers) inherit those guarantees. The bijection of Proposition 4.2 also gives a precise dictionary between the lifted signal space and the phase space .
Formalizing it. The result is proved in the paper; to the best of current knowledge none of it has a machine-checked proof. The mission produces a formal statement of the three programs over complex Hermitian matrices, of the pseudoinverse identities for injective matrices, and of the trace and rank transport under the congruence , which are reusable for other lifting arguments in phase retrieval and low-rank SDP.
The corollary itself is short once Proposition 4.2 and the two transport identities are available; the substance lies in Proposition 4.2. The natural first attempt is to check that maps feasible points to feasible points, which is direct. Surjectivity is the step that requires an argument: a PhaseCutMod-feasible satisfies only the scalar constraint , and one must first upgrade it to the matrix equation (using positive semidefiniteness of both factors) and then to a range condition on before a preimage can be written down. In Lean, an additional cost is the absence of a pseudoinverse and of trace-zero-product lemmas for complex Hermitian matrices in the form needed, and the bookkeeping between complex traces and real objectives.
Matrices are Matrix (Fin n) (Fin p) ℂ and Matrix (Fin m) (Fin m) ℂ; is Mathlib's Matrix.PosSemidef (Hermitian included); rank is Matrix.rank. Conventions committed to:
Function.Injective A.mulVec. is encoded as (Aᴴ * A)⁻¹ * Aᴴ, Mathlib's inverse returning on singular matrices; it is the pseudoinverse only for injective , so every statement mentioning , or assumes injectivity. This adds injectivity, not present on the page, to the claim (p. 4) and to the companion claim on p. 12.Set.BijOn Φ (PhaseLift feasible) (PhaseCutMod feasible).Infrastructure that a complete development needs, and that is reusable beyond this mission: the pseudoinverse identities and for injective complex , the fact that is a Hermitian idempotent, the lemma for complex positive semidefinite matrices, and rank invariance under congruence by injective matrices. Proofs of any milestone are welcome, as are general Mathlib-style lemmas on these points.
In D-optimal design, a statistician chooses weights for a collection of candidate observations. The weights determine an information matrix, and maximizing its determinant favors a design that estimates several parameters jointly with a small confidence region. The same determinant objective appears in the minimum-volume enclosing ellipsoid problem. These links, and the earlier methods developed specifically for this objective, are described by Lu, Freund and Nesterov (2018), §2.2. A convergence theorem matters because a numerical design is useful only when its objective value can be related to the best possible value.
The paper applies a general relative smoothness framework to this problem. The usual first-order analysis asks for a uniform Lipschitz bound on the gradient of the objective. The logarithmic determinant has curvature that grows near singular information matrices, so a Euclidean smoothness constant on the whole design region is unsuitable. A logarithmic reference function gives a scale adapted to the coordinate boundary. The mission isolates the matrix result that provides this scale and the resulting explicit iteration bound for the primal gradient scheme. Both results are proved in the paper; their Lean statements are targets for formal proof.
Fix an real matrix with row rank and . A design weight is a vector with nonnegative coordinates and . This set is the simplex . Write and . On the points where is positive definite, the optimization problem is
The optimum may occur on the boundary of . At a singular point has no finite real value in the paper's model. Accordingly, the formal optimum is an attained point for which x^*, minimal among all such points.
For the algorithm, the positive simplex is . The reference function and its Bregman distance are
h(x)=-\sum_{j=1}^n\log x_j, \qquad D_h(y,x)=h(y)-h(x)-\nabla h(x)\cdot$y-x$.A primal gradient run starts at . At each iteration , it chooses to minimize
The coefficient of is exactly one. Proposition 2.2 of Lu, Freund and Nesterov (2018) establishes this relative smoothness constant on the positive orthant. The displayed update represents the minimization condition; no tie-breaking rule is fixed.
For all positive vectors , Proposition 2.2 asserts
f(y)\le f(x)+\nabla f(x)\cdot$y-x$+D_h(y,x).Its source-stated matrix claims form the first part of the milestone list. If , the paper identifies , , and . Equation (17) then records the full comparison with . Proposition 1.1 connects this Hessian comparison to relative smoothness. These statements fix the constant used by the algorithm.
The mission goal is Theorem 4.1 of Lu, Freund and Nesterov (2018). For , it states
The remaining milestones are the instance of the paper's primal gradient rate used here, the interior comparison point bound (40), and the logarithmic Bregman estimate (41)–(42). They follow the objects and constants named in the proof of Theorem 4.1.
The theorem gives a concrete stopping threshold expressed in the number of design weights, the requested objective gap, and the gap at the uniform start. It applies the same primal gradient method analyzed for general relatively smooth functions to a determinant objective whose gradient becomes steep near the boundary. The rate is an iteration count; it does not claim a superior arithmetic-operation count to specialized Frank–Wolfe methods. The paper compares those costs in its Table 1, noting that dense primal gradient iterations require a matrix inverse computation Lu, Freund and Nesterov (2018), §4.
A machine-checked development would connect finite-dimensional matrix inequalities, determinant derivatives, relative smoothness, and the algorithmic rate in one formal model. The matrix and logarithmic derivative results can be reused for other determinant objectives and barrier-based methods. The article proves Theorem 4.1; the mission asks solvers to formalize that known proof or another proof of the same precise statement. None of the draft theorem items is represented as already machine-checked.
The determinant objective is well behaved on positive definite information matrices but is undefined at a singular design. A first attempt to apply a smoothness bound over the entire closed simplex encounters unbounded curvature near that boundary. A second issue is that an optimal design can have zero weights, while the logarithmic reference function and the algorithm use positive weights. The rate statement must therefore compare an interior run with an optimum that may lie on the boundary. The milestone list exposes the matrix curvature estimate and the boundary comparison as separate claims rather than hiding either in the goal's assumptions.
Vectors are functions , with explicit finite sums; matrices have the corresponding finite index types. The Bregman pairing y-x$$ is Lean's real Fréchet derivative applied to . Iterates are zero-based. A Loewner inequality means that is positive semidefinite. Rank and are the standing data of problem (16). The reference function is used on the positive orthant, and Algorithm 1 minimizes over , matching the positive subproblem minimizer described on p. 341.
The paper treats as infinite when the information matrix is singular and as infinite at a zero coordinate. Lean's real logarithm has a total value there, so every theorem restricts its meaningful objective evaluations to positive vectors or positive definite information matrices. The goal represents by an attained on that domain. It states because the source's iteration formula divides by and takes a logarithm of a ratio involving it. The interior point in (40) is constructed from ; it is not an unconstrained input. These conditions rule out a vacuous interior, a junk logarithm, or division by zero as a formalization of the paper's conclusion.
The development needs matrix rank and positive definiteness, determinant and logarithm differentiation, positive semidefinite matrix order and the Schur product property, finite-sum calculus, and convex analysis of the positive simplex. The finite-dimensional matrix estimates and the relative smoothness criterion are natural reusable contributions. A proof may establish the listed milestones in another order, provided it keeps the same statements and constants.
Online learning studies repeated decisions made before their losses are known. A learner chooses a point, observes a loss function, and then uses that observation to choose the next point. The natural performance measure is regret: the learner's cumulative loss minus the cumulative loss of one fixed competitor chosen after the sequence is known. A regret bound makes a claim for every loss sequence, including a sequence adapted to the learner's earlier decisions. Orabona's Chapter 6 develops online mirror descent as a way to obtain such bounds in geometries other than Euclidean distance Orabona, Chapter 6.
The geometry matters because the decision set and its loss gradients can have very different scales under different norms. On a simplex, for example, a Euclidean description treats coordinate changes differently from an entropy-based description. Theorem 6.11 expresses the guarantee in a primal norm chosen for the regularizer and the corresponding dual norm for the observed subgradients. It is the chapter's general regret statement for the basic mirror-descent algorithm Orabona, Theorem 6.11, p. 67.
Let be a finite-dimensional real normed space, representing the book's with a chosen norm . The learner chooses from a nonempty closed convex set . A regularizer has domain ; it is strictly convex on and differentiable on the interior of . Its Bregman divergence is
defined when and . It need not be symmetric or satisfy the triangle inequality. The regularizer is -strongly convex on with respect to the chosen norm, where . The norm of a gradient , written , is the norm dual to . These are the conventions of Definition 6.4 and Lemma 6.10 Orabona, pp. 63–67.
At round , beginning with , the learner has , then observes a loss and a selected subgradient at . With step size , Algorithm 6.1 chooses any minimizer
The book gives two ways to keep each update in the interior of . The statements assume either of them, (6.5) or (6.6), , so every iterate is a valid reference point for the next Bregman divergence Orabona, Algorithm 6.1 and (6.6), p. 65. Regret is measured against one fixed :
For and nonincreasing positive step sizes, Theorem 6.11 gives the chapter's general bound
When every step equals the same , it also gives the more specific bound
The decreasing-step bound is the goal; the constant-step conclusion is a companion theorem. The milestone list records the book's three-point identity (Lemma 6.7), the unique-minimizer theorem for a closed strongly convex function (Theorem 6.9), and the existence and full three-part inequality of the one-step mirror-descent lemma (Lemma 6.10). Theorem 6.11 follows these results in the source Orabona, pp. 64–67.
The first bound makes the cost of the update explicit: one term measures the divergence from the competitor to the iterates, and the other accumulates squared dual norms of the selected subgradients. The constant-step form depends only on the initial divergence, which can be substantially easier to estimate. These forms let a later analysis choose a regularizer and norm pair suited to its feasible set and gradients, as the chapter does in its subsequent examples Orabona, §§6.6–6.7.
The theorem and its proof are known mathematically from the textbook. The work here is to express the algorithm, its admissible oracle choices, and the exact bounds as Lean statements and then prove them. A formal proof of the one-step inequality would also be reusable for later dynamic-regret and optimistic mirror-descent results. The published Bregman-divergence definition is reused, but the statements in this mission remain proof targets; a related published three-point identity assumes continuous differentiability, stronger than the book's hypothesis.
The usual squared Euclidean distance has a symmetric algebraic expansion. Bregman divergence is asymmetric and its second argument must lie where the regularizer is differentiable. Thus a direct replacement of squared distance by does not by itself establish that every update is defined or that the terms in a regret sum have the right orientation. Theorem 6.11 also allows changing step sizes, so the divergence terms carry different denominators from one round to the next. The one-step lemma packages the exact inequality needed to make those issues precise Orabona, Lemma 6.10 and Theorem 6.11, p. 67.
The Lean development uses an arbitrary finite-dimensional real normed space; continuous linear functionals represent subgradients, and their operator norm is . The regularizer is a total real-valued Lean function, but only its values on represent the book's function. Closedness is expressed by the closed epigraph of the extension equal to outside . Bregman divergence uses the published definition with the derivative at the second argument. The run predicate records the initial point, a selected subgradient, and a minimizer over on each round; it imposes no tie-breaking rule. The loss functions are real valued on , and subgradient inequalities are stated relative to , the only points compared in the regret result.
All sums use rounds ; index zero carries no data. The maximum is a finite maximum with the explicit condition . Positive and protect every division in the displayed bounds. Every drafted statement assumes the book's "(6.5) or (6.6)", with (6.5) read as a one-sided limit . The update is required to minimize over itself, and ranges over ; allowing points outside that set would change the theorem. The minimizer result, the full one-step chain, and both regret bounds are welcome proof targets. The domain-restricted closed-function representation and the finite-round run predicate can be reused in related online convex optimization developments.