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.
Track exact exponent savings κ for integer multiplication in time, where . Higher κ is better. Every entry uses the same public IntMul.KappaBound definition: one deterministic machine, a fixed finite alphabet and tape count, exact multiplication for every positive input length, and an eventual worst-case time bound.
Avi’s Harvey–van der Hoeven mission supplies the shared foundation. Its main goal uses the natural-logarithm formulation of the 2021 bound, so it serves as the foundation rather than a numeric entry. Avi’s positive-κ mission targets Jain’s round-six value 0.00003666565558019; it is a historical checkpoint. The reviewed community PR #62 checkpoint targets 0.000051016920170078. Open entries record goals to prove, not established records. The full multiplication theorem remains Open even when finite numerical certificates have been verified.
Community checkpoint and credits · Original framework · Harvey–van der Hoeven
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?
Nesterov's accelerated gradient method minimizes a smooth convex function at the rate in the number of iterations , against for plain gradient descent. Su, Boyd and Candès (arXiv:1503.01243) observed that, as the step size tends to zero, Nesterov's scheme becomes the second-order differential equation
with , a heavy-ball system whose friction coefficient vanishes as (asymptotic vanishing damping). Studying (1) in continuous time gives Lyapunov arguments that are then discretized into new algorithms.
Attouch, Chbani, Peypouquet and Redont (Math. Program. 168 (2018), DOI 10.1007/s10107-016-0992-8) analyse (1) for general . This mission formalizes their result for strongly convex , where the rate of convergence of (1) depends on and improves without bound as grows.
Timeline.
Let be a real Hilbert space with inner product and norm , and let be continuously differentiable with gradient . Fix and . A solution of (1) is a twice differentiable trajectory with velocity satisfying (1) at every .
is strongly convex with constant if
Such a has exactly one minimizer , and .
For , the anchored energy is
a sum of nonnegative terms. The proof of the main theorem fixes
For strongly convex and , every solution of (1) converges strongly to the unique minimizer , and
as . The goal states the asymptotic form; the explicit constants are milestones.
The theorem shows that the rate of (1) on strongly convex functions is not capped at or : the exponent grows linearly in , and it already exceeds for every . It extends [44, Theorem 4.2], which needs and gives . The same parametrized energy is the template for the discrete analyses of Nesterov-type algorithms with parameter , so its derivative identity (10) is reusable beyond this mission.
The result is proved on paper. To the best of current knowledge none of it is formalized: Mathlib has no theory of inertial dynamics, and the platform's strongly convex rates concern discrete methods. A completed mission gives a machine-checked Lyapunov analysis of a non-autonomous second-order ODE in a Hilbert space, with the explicit constants of the paper.
The derivative identity (10) is a computation, but it must be carried out with one-sided derivatives at , real powers , and the chain rule for in an infinite-dimensional space. The obvious argument, that is nonincreasing, fails: even with the best choice of and the bound on its derivative keeps a term of no fixed sign, and only for is the quadratic term in nonpositive. Passing from the differential inequality to (26) therefore needs integration on for functions known only through one-sided derivatives. The velocity bound then combines (26), (27) and (28) through square roots, and the goal additionally requires the existence of the minimizer in an infinite-dimensional space, which is a compactness argument (weak lower semicontinuity) and not an algebraic one.
InnerProductSpace ℝ H, CompleteSpace H), not . is ContDiff ℝ 1 and is Mathlib's gradient.Asymptotics.IsBigO along atTop; strong convergence is norm convergence. The existence and uniqueness of are conclusions of the goal, not hypotheses, so the goal cannot be satisfied vacuously by an empty argmin; the strong-convexity hypothesis is satisfiable (e.g. with , and solves (1)).Useful infrastructure: the derivative of via gradient, integration of differential inequalities on , and existence of minimizers of strongly convex continuous functions on Hilbert spaces. Proofs of any milestone, and of the goal from the milestones, are welcome.
In classical optimal transport, a transport plan that minimizes the total cost is characterized through its support: an optimal plan is -cyclically monotone, meaning that no finite collection of its transported particles can be re-paired more cheaply (Villani, Optimal Transport, Old and New, 2009, Ch. 4–5). This pointwise criterion is how most structural results in optimal transport are proved: it is what turns a global minimization over measures into a statement about finitely many points.
The martingale transport problem adds a constraint motivated by mathematical finance: the plan must be the law of a one-step martingale with given marginals , . Its value gives model-independent bounds on the price of an exotic option whose payoff is the cost function, given the prices of all vanilla options at two dates (Beiglböck, Henry-Labordère, Penkner, Model-independent bounds for option prices, Finance Stoch. 2013). Because the martingale constraint ties together all points with the same first coordinate, the classical re-pairing argument does not carry over: swapping two destinations generally destroys the martingale property.
M. Beiglböck and N. Juillet (On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 2016; arXiv:1208.1509v2) prove a martingale replacement for -cyclical monotonicity, the variational lemma (Lemma 1.11). It is the tool from which they derive the left-monotone structure of optimal plans, the uniqueness of the left-curtain coupling as optimizer for costs with strictly convex, and the support bounds for optimizers. This mission is the first of a series formalizing that paper.
All measures live on or with their Borel -algebras. Two probability measures on with finite first moment are in convex order, , if for every convex .
A transport plan is a measure on with first marginal and second marginal . It is a martingale transport plan, , if under the conditional mean of given equals ; equivalently,
A cost is a Borel function satisfying the sufficient integrability condition with , ; then the cost of a plan, , is well defined in . A plan is optimal if for every , and it leads to finite costs if .
A measure on is a competitor of (Definition 1.10) if it has the same two marginals as and the same conditional barycentres: for almost every , where , are disintegrations with respect to the first marginal. A competitor redistributes the mass of in a way that a martingale plan could absorb: replacing a piece of a martingale plan by keeps both marginals and the martingale property.
Let be probability measures, a Borel cost satisfying the sufficient integrability condition, and optimal with . Then there is a Borel set with such that
The set is chosen once, before ; the quantifier order is the content.
The milestones are the steps of the paper's proof (§3, pp. 16–19), in attack order:
The result. The variational lemma converts optimality of a martingale plan, a property of a measure, into a condition on finite configurations of points in its support. In the paper it is applied, together with a lemma on accumulation points of sections (Lemma 3.2), to show that optimizers for costs with strictly convex are left-monotone, which by the paper's Theorem 1.5 identifies them as the left-curtain coupling; it also yields the bound of Theorem 7.1 and the two-graph structure of the optimizers for . Later missions of this series use it as a milestone. Its converse, under continuity assumptions, is the separate Lemma A.2 of the paper's appendix.
Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization needs a usable form of Kellerer's duality for multi-marginal problems, which is not in Mathlib, and the bookkeeping that finite rearrangements of a martingale plan stay in . Both are reusable well beyond this paper: Kellerer's theorem underlies the analogous results for classical, multi-marginal and martingale transport.
The classical proof of -cyclical monotonicity perturbs an optimal plan by moving a small amount of mass around a finite cycle of its support points. For martingale plans this fails: the perturbation must preserve the conditional barycentre of every , and mass sitting at isolated points of a non-atomic plan cannot be moved without moving mass at uncountably many other points. The proof therefore cannot argue point by point. It works with whole families of bad configurations at once, which requires the measure-theoretic duality of Kellerer (resting on Choquet's capacitability theorem) and a measurable choice of an optimal competitor for each configuration. Proving that the set of bad configurations is Borel, and that a positive-mass family of them can be glued into a cheaper competitor of a piece , is the technical core.
The Lean development uses Mathlib's Measure ℝ and Measure (ℝ × ℝ). Costs and integrals that may be infinite take values in EReal, through the published definition ModelRiskOT.Duality.extIntegral (, with ); no Bochner integral of a possibly non-integrable function is compared. Martingale plans and competitors are encoded through test functions (the paper's characterization (4), p. 10) instead of disintegrations. A finitely supported finite measure is written with a finite set and weights ; this covers every such measure, and masses are taken finite. is Fin n → ℝ × ℝ.
Committed conventions and disclosed additions:
A formalization in which is empty or -null, or in which is allowed to depend on , is trivial and is ruled out by the statement: and . The competitor ranges over all measures, not only finitely supported ones.
Welcome contributions: a general form of Kellerer's duality theorem (milestone 1), the Borel-measurability of the bad set, and the gluing step of milestone 6.
Proximal gradient methods are used to minimize an objective with one smooth part and one convex part whose proximal map can be evaluated. A small proximal gradient step is a practical stopping signal, but it indicates proximity to an optimizer only when the objective has an appropriate error bound. Section 4 of Drusvyatskiy and Lewis gives conditions for that bound in the structured problem : the conditions concern the dual problem and the growth of the two component functions, rather than requiring strong convexity of their sum. This matters for problems with a nontrivial solution set and for penalties that are not strongly convex. The paper places this result after its §3 comparison of quadratic growth and proximal gradient error bounds (pp. 9–11).
Let and , with their Euclidean inner products and norms. Let be linear, be continuously differentiable and convex, and be proper, lower semicontinuous, and convex. The primal objective and its minimizer set are
The mission assumes is nonempty and bounded. Its minimum is finite. For an extended-real function , its Fenchel conjugate is . The dual objective is , and denotes a dual minimizer. The effective domain is ; denotes relative interior. The paper assumes dual nondegeneracy, , and dual strict complementarity, (p. 10).
A closed convex function is firmly convex relative to when its tilt grows at least quadratically away from its minimizers on each compact set. The positive coefficient may depend on the compact set. Theorem 4.2 assumes this property for at and for at (Definition 4.1, p. 11).
For , a proximal gradient step is , and its residual is . The error bound asks whether the distance from to is controlled by whenever lies below a prescribed objective threshold (Definition 3.1, p. 5).
The milestone path records the Kuhn–Tucker description of , the relative-interior identity (4.3), the compact-set distance estimate (4.4), the two component inequalities (4.5), and the resulting quadratic growth of on every sublevel set. In particular, for each there is such that
These are the claims stated in §4 and in the proof of Theorem 4.2, pp. 10–11. The milestone for (4.5) retains the paper's printed in its quotation, while the Lean statement uses positive constants, as Definition 4.1 requires for nontrivial quadratic growth.
The goal is Theorem 4.2: under the conditions above, for every there exist such that
The formal statement makes explicit that has a Lipschitz constant. This is part of the §3 setting used by the paper's Corollary 3.6 to reach the displayed error bound. A companion statement, Theorem 4.5, pp. 12–13, says that the Moreau envelope of a firmly convex function retains firm convexity relative to the same vector.
The conclusion converts dual geometric information and component growth into an error bound expressed through a proximal gradient step. The residual is available when running the method, whereas the distance to is generally not. Combined with the paper's §3 results, the error bound yields local convergence guarantees for the proximal gradient method in structured convex problems (Corollary 3.6 and Theorem 4.2). The statement covers settings in which component functions have local quadratic growth after a tilt while the composite objective need not be strongly convex.
The research result is proved in the paper. The work of this mission is to formalize its exact assumptions and claims, including the convex dual and the relative-interior statements, then supply machine-checked proofs. The resulting Euclidean conjugate, firm-convexity, and structured-objective definitions can also support other convex optimization formalizations. The statements in this proposal are proof obligations; compiling the statements alone does not establish the theorems.
Component growth concerns distance to separate subdifferential inverse images. The desired error bound concerns distance to their intersection, which is the primal solution set. Two small component distances do not automatically control distance to an intersection: the sets can meet at a poor angle. The dual interior hypotheses supply the regularity needed in (4.4). The argument also changes the quantity being controlled from objective growth to a proximal gradient residual. Those two changes are the substantive steps a proof must justify; treating either as an unrestricted distance identity would change the theorem.
The Lean spaces are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); dimensions zero are permitted. The linear map is continuous, and is its adjoint. Extended-real values use EReal; properness excludes values, and lower semicontinuity encodes closedness. Conjugates take suprema in EReal, and the dual objective follows (4.2). Relative interior is intrinsicInterior ℝ. The published convex subdifferential, proper-convex predicate, and proximal-point predicate are imported as reference items because their meanings match the paper's objects. The paper's Euclidean conjugate is defined locally because the available published conjugate has a strong-dual codomain.
The minimum value is real and is pinned to the nonempty primal minimizer set. The dual point is pinned as a minimizer of . Proximal steps are expressed as argmin predicates, so no default result is chosen for a failed minimization. The firm-convexity predicate requires a nonempty minimizer set of the tilted function: otherwise Lean's real distance to the empty set would be zero while the source uses an infinite distance. The growth constant of Definition 4.1 and the constants of (4.5) are strictly positive: the page leaves the sign implicit or prints , but with a zero constant every convex function would be firmly convex, contradicting the page's own example , and the growth statements would be empty. The error bound is restricted to the stated sublevel set, and all of its constants are positive. The goal includes a nonnegative Lipschitz constant for , disclosed because the source's §3 bridge to the error bound assumes one; the component-growth milestones do not assume it.
Contributions should establish the Euclidean convex-duality identities, the compact-set regularity estimate, the component and composite growth claims, and the proximal gradient conclusion. The Moreau-envelope preservation theorem is a separate companion target. None of the dual interior conditions or the firm-convexity assumptions may be replaced by a vacuous condition: the goal concerns their effect on the actual solution set of .
Peaceman–Rachford splitting and its relaxed forms solve the problem of minimizing a sum by evaluating the two proximal maps separately. This is useful when minimizing either function by itself is simple while minimizing their sum directly is not. Douglas–Rachford splitting is the half-relaxed case. Davis and Yin study which properties of and turn the basic convergence of this iteration into quantitative rates. Their Theorem 2.1 supplies the regularity estimates used throughout their later objective and fixed-point analyses (Davis and Yin, arXiv:1407.5210v3, §§1–2).
The theorem measures progress using a term that can respond to strong convexity, a Lipschitz gradient, or both. Its conclusions distinguish three observations of the same run: the best iterate found so far, a weighted average of the auxiliary points, and the current iterate. This distinction matters because a rate for a best iterate need not hold for every iterate; the authors explicitly leave open whether their best-iterate conclusion can be improved in that way (Davis and Yin, p. 9).
Let be a real Hilbert space. The functions are closed, proper, and convex. For a positive step size , the proximal map of sends to the unique minimizer of . Define the reflection and likewise . The Peaceman–Rachford map is . Given relaxation parameters , Algorithm 1 generates
At , set and . These points may differ, so the theorem tracks them separately. Their selected proximal subgradients are and . The tilde means a particular member of a subdifferential when the function is not differentiable (Lemma 1.1, p. 7).
Suppose is a fixed point of and put . Each function has a nonnegative strong-convexity parameter and a nonnegative smoothness parameter . If , the function is differentiable and its gradient is -Lipschitz; a zero parameter imposes no such property. For the selected subgradients at and , define the regularity term
The partial relaxation weight is . All of these conventions are from the paper's notation, Algorithm 1, and equations (1.13)–(1.14) (Davis and Yin, pp. 3–8).
The goal first asserts the exact one-step inequality (2.1):
It also asserts that converges and that eight times times this sum is at most . These are Theorem 2.1's common quantitative bounds (p. 8).
If the are bounded below by a positive constant, the minimum through of each regularity term is . The weighted averages of and , together with the matching weighted averages of their selected subgradients, have regularity terms whose sum is at most . Finally, if the products have a positive lower bound, the sum of the two current regularity terms is (Theorem 2.1, p. 9).
Strong convexity makes the regularity term control squared distance to ; a positive smoothness parameter makes it control the difference between selected gradients. Theorem 2.1 therefore connects properties of the objectives to rates for quantities produced by Algorithm 1. The one-step bound is also the stated input to later linear-convergence arguments in the same paper (§4, pp. 13–16). Without this result, those applications lack their common quantitative estimate.
The paper proves Theorem 2.1. This mission asks for a machine-checked proof of its precise statement and supporting claims, not for a new asymptotic rate. The proximal-map and subdifferential definitions already exist as published formal objects; the reusable remaining work includes their quantitative inequalities and the summable-sequence rate facts. The draft goal and milestones are theorem statements with proof holes and do not yet constitute verified proofs.
The obvious inference from a finite sum of nonnegative regularity terms gives a bound on cumulative error, but it does not directly give little- rates for the current term. The theorem also separates a best-iterate conclusion from a last-iterate conclusion: the regularity terms need not be monotone, and the stronger condition on is required for the latter. The ergodic conclusion concerns weighted averages of both points and subgradients, so bounding only the average of pointwise regularity terms does not by itself state the result (Theorem 2.1 and its discussion, pp. 8–9).
Lean uses EReal for the objectives, a complete real inner-product space for , and published predicates for closed proper convex functions, proximal maps, and subgradients. A proximal map is supplied as a function satisfying the minimization property; uniqueness under the stated assumptions makes it the paper's map. Selected subgradients are fixed difference quotients from Lemma 1.1. The parameters are nonnegative, and positive requires a real-valued differentiable function with -Lipschitz gradient. A fixed point states the solution-existence assumption in the form used by Theorem 2.1. No hypothesis asserts any conclusion of the theorem.
The finite minimum uses the nonempty index range ; little- uses Mathlib's asymptotic relation at infinity. The denominators , , and are positive under the stated bounds. In supporting objective inequalities, conversion from EReal to real numbers occurs only at proximal outputs and points with subgradients, where function values are finite. The printed unweighted, repeated- subgradient sum in the ergodic clause is corrected to the -weighted average consistent with the page's definition of and with the result it states. Contributions proving the exact goal, any milestone, or reusable proximal and sequence lemmas are in scope.
Many quantities in stochastic analysis and mathematical finance depend on the whole past of a process, not only on its current value: running maxima, averages, integrals against the quadratic variation, payoffs of path-dependent options, conditional expectations of path functionals. The classical Itô formula describes the evolution of for a smooth function of the current state; it says nothing directly about a process that depends on the path .
In 2009 Dupire proposed two pathwise derivatives for such functionals, a horizontal (time) derivative obtained by freezing the path and a vertical (space) derivative obtained by bumping its endpoint, and a change-of-variable formula built on them (Dupire 2009). Cont and Fournié gave this calculus a rigorous framework and proved the functional Itô formula for continuous semimartingales (Cont and Fournié, Ann. Probab. 2013; preprint arXiv:1002.2446v5). The companion paper (Cont and Fournié, J. Funct. Anal. 2010) gives a pathwise version in the spirit of Föllmer. The formula underlies the martingale representation results of the same paper and the later theory of path-dependent PDEs.
Fix a horizon . A path is a cadlag function on ; denotes the -valued ones and the paths with values in the positive semidefinite matrices. For a path :
A nonanticipative functional assigns a real number to each pair , measurably for the -algebra generated by the evaluations of the paths (Definition 2.1). Paths at different times are compared with the distance (9),
is left-continuous (, Definition 2.4) if is close to whenever is -close to ; it is boundedness preserving (, Definition 2.5) if it is bounded on sets of paths with values in a compact set. The horizontal derivative is
and the vertical derivative is the gradient at of ; is the vertical derivative of . (Definition 3.6) is the class of left-continuous with continuous at fixed times, left-continuous, and .
On a filtered probability space satisfying the usual hypotheses, is a continuous -valued semimartingale and its quadratic covariation has a density, (3), with cadlag, adapted, -valued. has predictable dependence on when (10).
For every verifying (10) and every , almost surely,
Theorem 4.1 shows that a path-dependent process is a semimartingale whose decomposition is computed from the jet along the path of . It contains the classical Itô formula () and covers functionals such as , and . Downstream it yields the identification of the martingale part of , the intrinsic character of the vertical derivative of an adapted process (Corollary 4.4), and the representation of smooth martingales (Theorem 5.2), which is the subject of the second mission of this series.
The result is proved in the paper. No machine-checked proof of it exists; the classical multidimensional Itô formula itself is an open goal on this platform (EthierKurtz.ito_formula). This mission produces a formal definition layer for functional Itô calculus (stopped paths, the metric , the regularity classes, pathwise derivatives) and a formal statement of the formula with its supporting lemmas.
The obvious argument fails at its first step: a path functional cannot be differentiated along the path of . The horizontal derivative freezes the path and the vertical derivative bumps only its endpoint; neither is a perturbation of in the direction of its own increments, so the chain rule behind the classical Itô formula has nothing to act on. A second obstruction is regularity: is only cadlag, the derivatives of are only left-continuous or continuous at fixed times for , and the paths at which they must be evaluated live on intervals of different lengths. Any limit procedure therefore needs uniform control of cadlag paths in the sup norm, which fails across their jumps, together with convergence theorems for stochastic integrals whose integrands are only locally bounded. Finally, the classical Itô formula, which is a special case, is itself not yet formalized.
Time is with horizon , and every statement concerns . Paths are functions on ; a path on is represented by its stopped version , which also serves as the horizontal extension. Functionals are defined on all path pairs and are required to be nonanticipative (); every continuity, boundedness and differentiability condition quantifies only over pairs cadlag on with positive semidefinite , as in the paper. The norm on pairs (vector, matrix) is the largest absolute value of the entries; "" is an explicit bound, so unbounded suprema never count. The derivatives are witnesses tied to by one-sided and Fréchet derivative statements, which makes them unique; free derivative witnesses, a functional that is not nonanticipative, and conditions over non-cadlag paths are each excluded. Definition 2.1's measurability is part of the class: without it Theorem 2.7 fails.
The semimartingale is with continuous, adapted, of bounded variation, and a continuous local martingale componentwise (the published EthierKurtz.IsSourceLocalMartingale); (3) uses the published EthierKurtz.HasCrossVariation. The Itô integral in (30) is the limit in probability of dyadic left Riemann sums (the published EthierKurtz.itoStepSum): the goal states that these sums converge to the remaining terms of (30). This is the a.s. identity, not a weakening, because limits in probability are unique; it is not a junk limit, because the integrand is left-continuous up to a -null set, adapted and locally bounded. The -integrals have bounded integrands by , so the Bochner integrals are genuine.
A complete development needs: cadlag path lemmas (A.1–A.3), stopping times of jumps, the predictable -algebra (in Mathlib), the classical Itô formula, and dominated convergence for stochastic integrals. The cadlag lemmas and the path-space layer are reusable beyond this mission. Proofs of any milestone, of the classical Itô formula, and of the stochastic-integral convergence theorems are welcome.
The Kalman filter estimates the hidden state of a linear system from noisy observations. At every step it solves a minimum mean square error (MMSE) estimation problem: given a joint normal distribution of a signal and an observation , find the estimator minimizing . The answer, the conditional mean, is optimal only if the model distribution is correct, and in practice the system matrices and noise covariances are estimated and misspecified.
Shafieezadeh-Abadeh, Nguyen, Kuhn and Mohajerin Esfahani (arXiv:1809.08830, NeurIPS 2018) replace the single model by a set of plausible models: all normal distributions within type-2 Wasserstein distance of a nominal normal distribution. The estimator is then chosen to minimize the worst-case mean square error over this set. Their Theorem 2.5 shows that this robust estimation problem, although posed over an infinite-dimensional space of estimators and a nonconvex set of distributions, has the same value as a finite convex program over covariance matrices, and that the robust estimator is affine. Applied at every time step, this yields the Wasserstein distributionally robust Kalman filter of the paper's §4.
This mission formalizes Theorem 2.5 together with the minimax theorem (Theorem 2.3) and the lemmas of its proof.
Let and . A point of is with signal and observation . A symmetric matrix is partitioned as . () denotes the positive semidefinite (definite) matrices, means , , and is the positive semidefinite square root of .
Normal distributions. is the normal distribution on with mean and covariance ; singular is allowed. is the set of all of them.
Wasserstein distance. For distributions on ,
the infimum ranging over all distributions on with marginals and .
Ambiguity set. Fix , , the nominal distribution and a radius . The Wasserstein ambiguity set is
Robust estimation. Let be the set of all measurable functions . The distributionally robust MMSE problem is
and a distributionally robust MMSE estimator is a attaining the outer infimum. Nature's problem exchanges the two optimizations; a attaining its outer supremum is a least favorable prior.
The finite program. With , program (5) maximizes over (with , ) subject to
is a distributionally robust MMSE estimator. 3. For the same , lies in and is a least favorable prior.
Existence and uniqueness of an optimal are not part of the statement.
The result. Theorem 2.5 gives the robust estimator in closed form from one optimal covariance matrix, and identifies the least favorable distribution as a normal distribution with the nominal mean. Together with Theorem 2.3 it shows that the pair is a saddle point: the robust estimator is the Bayesian estimator for the least favorable prior. For the program has the single feasible point and the estimator reduces to the classical conditional mean, so the theorem contains the Kalman update as a special case. The finite program is what makes the robust filter of §4 computable; the paper's §3 (formalized in the companion mission of this series) solves it with a Frank–Wolfe method.
Formalizing it. The result is proved in the paper; nothing here is open. No part of it is machine-checked yet. The Gelbrich formula for normal distributions (Proposition 2.2) is cited from the literature and has no formal proof in Mathlib; neither does Lemma A.1, cited from earlier work of the same authors. A closely related statement for a Wasserstein ball over all distributions around an elliptical nominal (Kuhn et al. 2019, Theorem 25) is posed on the platform as WassersteinDRO.Shrinkage.distributionally_robust_mmse_estimator; it is a different theorem, since the ambiguity set there is convex and contains non-normal distributions.
The ambiguity set is not convex, because a mixture of normal distributions is generally not normal. The standard route to a minimax equality, Sion's theorem, needs convexity on nature's side and therefore does not apply to (2) directly; the obvious attempt to interchange the infimum and the supremum fails at this step. The space of measurable estimators is infinite-dimensional, and the Wasserstein constraint is an infimum over couplings, so a proof must pass to finite-dimensional descriptions on both sides (means and covariances for , affine maps for ) and justify each passage. The matrix-analytic parts involve the nonlinear map , for which Mathlib has square roots but little calculus.
EuclideanSpace ℝ (Fin n ⊕ Fin m); the Sum.inl coordinates are , the Sum.inr coordinates are , and the blocks of a matrix are toBlocks₁₁, toBlocks₁₂, toBlocks₂₁, toBlocks₂₂.multivariateGaussian c S with S.PosSemidef; only the nominal is required to be positive definite.WassersteinDRO.Shrinkage.wassersteinDistance 2 in . The ambiguity set is defined through it, not through the Gelbrich formula; the formula is Proposition 2.2, a milestone.sdpValue in EReal, and the two are compared through the coercion.A complete development needs the Gelbrich formula for (possibly degenerate) normal distributions, conditional means of jointly normal vectors, a minimax theorem for convex–concave functions on compact sets, Lagrangian duality for a convex semidefinite program, and calculus of the positive semidefinite square root. The first three are reusable well beyond this mission, and contributions of any of them as separate results are welcome.
A Kalman filter estimates the hidden state of a linear system from observations , assuming the joint law of is a known Gaussian. When that law is only approximately known, Shafieezadeh-Abadeh, Nguyen, Kuhn and Mohajerin Esfahani (arXiv:1809.08830v3, NeurIPS 2018) replace it by the worst Gaussian within a 2-Wasserstein ball of radius around a nominal Gaussian with covariance . Their Theorem 2.5 shows that the resulting minimax estimation problem is equivalent to a finite nonlinear semidefinite program, program (5), whose objective is .
Each step of the robust filter solves program (5), so the filter is only practical if (5) can be solved quickly. The paper solves it with a Frank–Wolfe method (Algorithm 2), which avoids projections by replacing the objective with its linearization at the current iterate and maximizing that linear function over the original feasible set. That inner problem, the direction-finding subproblem, is again a nonlinear SDP. The paper's Algorithm 1 solves it by a one-dimensional bisection, and Theorem 3.2 states that this bisection returns a feasible solution whose objective value is within a prescribed tolerance of the optimum. This mission formalizes that guarantee.
Fix dimensions (state) and (observation), , and index coordinates so that the first belong to . Let and denote the positive semidefinite and positive definite matrices, and the trace inner product. The data are a nominal covariance with smallest eigenvalue , a radius , a tolerance , and the current Frank–Wolfe iterate , written in blocks .
The gradient matrix is
which is positive semidefinite and nonzero. The direction-finding subproblem (7b) is
its constraint says that the Gaussian with covariance lies within Wasserstein distance of the nominal Gaussian, and denotes its feasible set. For with the paper defines
Algorithm 1 takes the largest eigenvalue of and a unit eigenvector , and starts from the bracket with
Each pass sets and , replaces by if and by otherwise, and the loop exits with output as soon as and .
For all inputs as above:
The termination hypothesis is a correction: the printed theorem asserts that the algorithm outputs a solution, but if a trial point (or ) coincides exactly with the root of , the upper end of the bracket becomes that root, all later trial points have , and the loop never exits. Soundness holds unconditionally. The normalization is also added; the page says only "an eigenvector", and is not a lower bound for a rescaled one.
Theorem 3.2 is what makes Algorithm 1 a valid linear-maximization oracle for the Frank–Wolfe method on program (5): the convergence analysis of Frank–Wolfe with inexact oracles requires exactly a feasible point whose linearized objective is within a known tolerance of the optimum. It also shows that the inner problem, a semidefinite program with a matrix square root in the constraint, reduces to a scalar root-finding problem once is diagonalized, which is why the robust filter runs at a cost comparable to an eigendecomposition per step.
The result is proved in the paper; no machine-checked version exists. The formal version adds what the paper leaves implicit: the termination edge case, the normalization of , and the requirement (here ). The milestone statements on Lagrangian weak duality for the Wasserstein–Gaussian trust region and on the location of the multiplier are reusable for other covariance-robust programs of the same shape, such as Wasserstein shrinkage estimation.
The algorithm is elementary; the analysis is not. Feasibility of requires computing the matrix square root in closed form and comparing eigenvalues of non-commuting products to obtain . The dual bound is a semidefinite Lagrangian duality statement over a constraint involving a matrix square root, whose inner supremum (Lemma A.1, cited from earlier work) must be evaluated in closed form. Termination needs monotonicity and continuity of on and a careful account of which side of the root each bisection update lands on; the obvious invariant "the root stays strictly inside the bracket" fails precisely in the excluded dyadic case.
Matrices are indexed by Fin n ⊕ Fin m with blocks toBlocks₁₁ (), toBlocks₁₂ (), toBlocks₂₂ (). The feasible set is the published definition WassersteinDRO.Shrinkage.sdpFeasibleSet ρ Σ σ, which uses the published positive semidefinite square root psdSqrt. Mathlib's matrix inverse returns on singular matrices; every statement involving , or assumes or works at trial points that lie above , and is allowed to be this junk value because the theorem admits any (then ). The constants and are passed as reals together with hypotheses that pin them to the smallest eigenvalue of and the largest eigenvalue of . The algorithm is modelled as its sequence of passes, not as a function returning an output, so a non-terminating run cannot silently produce a value.
A formalization that defines the output with a fuel bound or a default value, that states only optimality of at the exact root, or that assumes termination as a hypothesis would not be Theorem 3.2; -suboptimality is stated against every feasible point, not against a supremum that could be a junk value.
A complete development needs the spectral theorem for symmetric matrices, uniqueness of the positive semidefinite square root, and semidefinite Lagrangian duality; Mathlib supplies the first two. Proofs of the milestones are welcome contributions.
An online retailer does not show its catalogue at once. Products are arranged on a sequence of pages, and a consumer looks at the first few pages and then chooses among what she has seen, or leaves. Where a product is placed therefore decides whether it is considered at all. Gallego, Li, Truong and Wang (Operations Research, 2020) call the placement decision product framing. They show that the optimal framing problem is NP-hard even with two pages and a multinomial logit choice model, and give polynomial-time framing algorithms with constant performance guarantees.
The paper builds on the assortment optimization literature, where a seller chooses one set of products to offer under a choice model, and on work in which consideration sets depend on how products are presented. Davis, Topaloglu and Williamson (2015) studied a sequential assortment problem in which products are added over time. Two of their results, on how per-product revenue behaves when products are removed, are the structural inputs of this mission. Aouad and Segev (2016) studied a variant with one product per page under the MNL model, in which every product must be displayed.
There are products , and product earns unit revenue . The products are placed on pages, each holding at most products, and a product may be left undisplayed. A consumer views the first pages, where is random with law and tail , independent of the framing. Her consideration set is the set of products on pages .
A choice model gives, for each consideration set , purchase probabilities with for and . The expected revenue of is . The optimal framing value is
the maximum over all placements with at most products per page (problem (1)). The cardinality-constrained assortment problem is (problem (2)), and is the best revenue from a consumer who sees pages.
The analysis rests on three assumptions:
The algorithm NEST(), for , first takes an optimal solution of (2) with bound . Then, for down to , it chooses of size whose per-product revenue is at least that of . Page displays , and pages after stay blank. is the expected revenue of this framing, and .
The goal holds under A1, A2 with and A3, for every run of NEST(), . Here .
The milestones are the numbered results the proof of Theorem 3 uses, in the order it uses them:
taken over NBUE tails and functions that are increasing with decreasing and . Proposition 3 states . 7. Lemma 7 and Corollaries 5–6, comparing NBUE with an exponential variable of the same mean. 8. The evaluation for exponential with mean . 9. The bound .
Theorem 3 gives a constant-factor guarantee for a problem that is NP-hard under the same assumptions. The constant does not depend on the choice model beyond A1, on the number of pages, or on the page capacity, and the paper shows it is tight relative to the upper bound (Proposition 4, in the geometric limit). NEST needs only a cardinality-constrained assortment oracle, which exists in polynomial time for the MNL and nested logit models. The same bound-revealing program, problem (5), is reused in the paper for joint framing and pricing (Theorem 7).
The paper proves the result in full. No part of it has been machine-checked. The mission formalizes the model and states the guarantee and every intermediate result. The proofs combine finite combinatorics (Lemmas 1 and 2, Proposition 1) with a comparison of a discrete NBUE law against the exponential distribution, and that comparison is reusable for other approximation analyses with the same structure. The equality of the exponential integral with connects to Mathlib's hasSum_zeta_two.
The upper bound (Theorem 2) and the lower bound (Proposition 1) are each elementary. The difficulty is to compare them uniformly over all choice models and all NBUE page-count laws. The ratio of to depends on the whole function and the whole law of , and the worst case cannot be read off from any single instance. Replacing the instance by the program (5) removes the choice model. Bounding the program still requires an optimization over distributions, and its value is attained only in a limit (Proposition 4).
The comparison with the exponential law goes through the increasing convex order. Here is a discrete law on and the comparison variable is continuous. The function to which Lemma 7 is applied is increasing and convex only on , so a formal argument has to track the domain.
Theorem numbers and pages are those of the authors' accepted manuscript (49 pp.), which differ from the journal typesetting. The conventions are:
Fin n. Pages are the naturals , kept 1-based, with .Fin n → ℕ: page means "not displayed", and each page holds at most products. is the maximum over the finite, nonempty set of feasible framings.expMeasure with rate . The independence in Corollary 6 is encoded by iterated integrals.NEST makes arbitrary choices, so a run is a predicate on its output. Theorem 3 is stated for every family of runs, and a separate milestone shows that runs exist. The value is the expected revenue of the framing the run actually displays, not the closed form , whose equality with it is part of the proof of Proposition 1. A formalization that quantified over some run, that defined by that closed form, or that assumed Lemma 2 for would not be Theorem 3.
Program (5) is stated with its tail variable and law , . The page's typos are corrected in the statements and recorded in the notes: "" in (5), and the right-hand side of Corollary 5. Proposition 2 is formalized in its existential reading: some optimal solution of (5) has constant .
A complete development needs:
The exponential comparison and the integral are reusable beyond this mission. Proofs of any milestone are welcome, including alternative proofs of Lemmas 1 and 2 from A1.
Nesterov's accelerated gradient method and its proximal variant FISTA minimize a smooth convex function with a value gap of order after iterations, against for plain gradient descent. They are among the most widely used first-order methods in large-scale optimization, signal processing and machine learning. Su, Boyd and Candès (JMLR 2016) observed that, for , the second-order differential equation
is a continuous-time limit of Nesterov's scheme, and proved for . A rate on the values says nothing about the trajectory itself: whether (or the iterates ) converges at all was a long-standing question. The paper of Attouch, Chbani, Peypouquet and Redont answers it for : every trajectory of (1) converges weakly to a minimizer of .
Timeline:
Let be a real Hilbert space with inner product and norm , and let be a continuously differentiable convex function with gradient . Fix a damping parameter and an initial time . A solution of (1) on is a pair of maps from the time axis to such that, at every , has derivative and has derivative . So , and satisfies (1). The damping coefficient is singular at and vanishes as ; this is why the time origin is positive.
Three functions of time measure the progress of a solution:
converges weakly to as if for every . A weak limit point of is the weak limit of a sequence with . is the set of minimizers of .
If and , then for every solution of (1) there is with
The goal asserts only the qualitative conclusion; no rate or constant enters it.
The result. Theorem 2.16 is the first proof that the trajectories of the continuous Nesterov model converge, not only their values. The paper's discrete analysis parallels the continuous one and yields weak convergence of the iterates of Nesterov-type forward–backward algorithms for (Theorem 5.3, a companion mission). The minimizing property (Theorem 2.3) holds for every , with no minimizer assumed, and shows that a bounded trajectory exists only if has a minimizer. Strong convergence results under further geometric assumptions (Theorems 3.1–3.3) build directly on Theorem 2.16.
Formalizing it. All statements are proved on paper. None of them, nor the differential equation (1), is formalized on Prove2Me or in Mathlib; the discrete analogue (weak convergence of the unperturbed accelerated forward–backward iterates) exists on the platform as a separate result. A formal development provides: a reusable encoding of solutions of a non-autonomous second-order ODE in a Hilbert space; Lyapunov arguments with one-sided derivatives on a half-line; a continuous-time Opial lemma, which is the standard tool for weak convergence of evolution equations and of semigroups; and the scalar differential-inequality lemma A.4.
Lyapunov functions such as or give rates on the values but not convergence of : a decreasing energy says nothing about where the trajectory goes, and the minimizer set may be a continuum. The natural first idea, showing that is eventually monotone as for the gradient flow, fails: the inertial term makes oscillate, and (7) controls only , a second-order quantity. Making it usable requires integrability of on , which is not available from the Su–Boyd–Candès energy and holds only for ; the borderline is open. In infinite dimension, convergence is genuinely weak: bounded sets are not compact, so the argument must identify weak limit points through weak lower semicontinuity of and conclude through Opial's lemma.
InnerProductSpace ℝ H, CompleteSpace H); no finite dimension is assumed, since in finite dimension weak and norm convergence coincide.ConvexOn ℝ Set.univ Φ and ContDiff ℝ 1 Φ; is Mathlib's gradient. Minimizers are points with for all ; is written for such a point.EReal, as an EReal infimum. Improper integrals carry an explicit integrability conjunct; integrals over are interval integrals of continuous functions.deriv), and the solution predicate is non-vacuous: the constant trajectory for and the explicit solution of Example 2.5 satisfy it.Contributions of reusable infrastructure are welcome, in particular a continuous-time Opial lemma, weak lower semicontinuity of continuous convex functions on a Hilbert space along weakly convergent sequences, and integration-by-parts lemmas for one-sided derivatives on a half-line.
Adam (Kingma and Ba, 2015, arXiv:1412.6980) is the default optimizer for training deep neural networks. At each step it keeps exponential moving averages and of the stochastic gradients and of their coordinatewise squares, corrects both for their initialization at zero (the bias-correction or debiasing step , ), and moves the iterate by . Despite its use, its convergence theory for nonconvex objectives was thin; the original convergence argument was later shown to be flawed (Reddi, Kale and Kumar, 2018, arXiv:1904.09237).
Barakat and Bianchi (arXiv:1810.02263v4, SIAM J. Math. Data Sci. 3(1), 2021, doi:10.1137/19M1263443) study Adam through the ODE method: when the stepsize tends to zero and the averaging constants satisfy , , the interpolated iterates follow a deterministic non-autonomous differential equation, the continuous-time Adam ODE. Everything else in the paper (convergence of the trajectory, rates under a Łojasiewicz condition, tracking by the constant-step iterates, almost-sure convergence of a decreasing-step variant) presupposes that this ODE is well posed from Adam's initialization. This mission formalizes that well-posedness result, Theorem 3.1 of the paper.
Let and , with points ; set , and . The data are reals , a function (the objective) and a map (in the paper, and , the mean squared gradient). All vector operations are coordinatewise. The Adam vector field is, for ,
and (ODE) is . The factors and are the continuous-time debiasing. A global solution with initial condition is a continuous map , continuously differentiable on , satisfying (ODE) for every , with .
The proof works with the regularized equations : for , and for , where . The fields are extended to by replacing with , and denotes the set of solutions on , . The Lyapunov function is with , and its limit is . The debiasing map is .
The hypotheses are those of §7 of the paper: is with locally Lipschitz gradient (Assumption 7.1) and coercive (Assumption 2.3); is locally Lipschitz (Assumption 7.2) with coordinatewise (Assumption 2.4); and (Assumption 2.5).
For every there is a global solution of (ODE) with initial condition such that
and any two global solutions with initial condition coincide on .
Theorem 3.1 makes the continuous-time Adam trajectory a well-defined object. The paper's convergence theorem for this trajectory (Theorem 3.2), its rate under a Łojasiewicz condition (Theorem 3.4) and the tracking result for the constant-step iterates (Theorem 4.3) are all stated about "the" solution, and the semiflow used for the asymptotic pseudotrajectory argument rests on the same uniqueness. The bound of Proposition 7.6 also gives the cost decrease , which the authors read as evidence that the bias correction makes early Adam steps safe.
The result is proved in the paper, and as far as is known nothing here has been formalized; no statement about this ODE exists on the platform. The mission formalizes the statement and the numbered lemmas of its proof. A complete development would also be a worked example of existence for an ODE whose field is neither continuous in time at nor Lipschitz in space, by regularization, compactness and passage to the limit.
Off-the-shelf theory does not apply. Cauchy–Lipschitz fails because contains , which is not Lipschitz at , and the initial condition has . Cauchy–Peano fails because blows up as : the factor behaves like . The obvious remedy, shifting time by , gives solutions , but passing to the limit needs bounds uniform in , both on the trajectory and on how far stays from zero. Uniqueness then has to be proved by a Grönwall argument whose coefficient is not integrable at , so the initial behaviour of solutions must be controlled to second order. Solutions from initial conditions with , need not exist at all (p. 5), so the special initialization is essential, not cosmetic.
Vectors are EuclideanSpace ℝ (Fin d) and states are triples; Lean's norm on the product is the maximum of the three Euclidean norms, which changes no boundedness, compactness or continuity statement. and are abstract functions satisfying Assumptions 7.1, 7.2, 2.3 and 2.4, as in §7 of the paper. Under Assumption 2.2 the expectation-defined and of (2.2) satisfy these, so the goal implies the theorem as printed. Coercivity is Tendsto F (cocompact _) atTop. Solutions are maps constrained only on : uniqueness is agreement on , never ∃! over all functions. The field is evaluated only at , where Lean's (1 - exp 0)⁻¹ = 0 cannot interfere. ranges over WithTop ℝ≥0 ( is and selects ), and over WithTop ℝ. The solution sets are -valued with the extension, as on p. 12, so positivity of is a theorem (Lemma 7.4), not an assumption.
A notion of solution without the differential equation, with it only away from on a set like , or with a derivative not tied to would make existence trivial. The definitions here require at every , continuity at and the exact initial value.
Mathlib provides Picard–Lindelöf, Grönwall-type bounds and Arzelà–Ascoli, but no Cauchy–Peano theorem; a reusable Peano existence theorem with maximal-interval extension would be a valuable contribution beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of the goal.
A McKean–Vlasov or mean-field stochastic differential equation is an SDE whose coefficients depend on the law of the solution itself. Such equations describe the limit of large systems of weakly interacting particles (Kac's kinetic models, McKean's propagation of chaos) and are the state dynamics of mean-field games and mean-field control. For a classical diffusion the expectation of a terminal payoff is a function of time and state and solves a linear parabolic PDE (the Feynman–Kac connection). For a mean-field diffusion the same expectation depends on time, on the state and on the current law of the population, so the associated PDE lives on , an infinite-dimensional space of probability measures. Buckdahn, Li, Peng and Rainer (arXiv:1407.1215, Ann. Probab. 2017) prove that this value function is the unique classical solution of its PDE, using the derivative with respect to measures introduced by P.-L. Lions in his Collège de France lectures.
Timeline. McKean (1966) introduced the equations; Sznitman (1991) gave the propagation-of-chaos theory. Buckdahn, Djehiche, Li and Peng (2009) and Buckdahn, Li and Peng (2009) studied mean-field backward SDEs and the associated PDEs in a form where the law enters only through the coefficients. Lions (2007–2012 lectures, notes by Cardaliaguet 2013) introduced differentiation on through lifts to . Carmona and Delarue (arXiv:1303.5835, 2013; arXiv:1404.4694, 2014) developed the Itô formula on the Wasserstein space and the master equation for mean-field games. The present paper (2014) proves the classical-solution result for the decoupled forward equation under second-order regularity of the coefficients in .
Let be a complete probability space carrying a -dimensional Brownian motion , let , and let be a sub--field independent of that is rich: every is the law of some . Here is the set of probability measures with finite second moment, with the 2-Wasserstein distance , the infimum over couplings of and . The filtration is .
Given Lipschitz coefficients , , a time , and , the processes and solve on
The second process depends on only through , so for the value function is a function on .
A function has Lions derivative if its lift on is Fréchet differentiable with derivative . The classes and ask for one or two such derivatives (together with derivatives in and in the extra variable ), all bounded and Lipschitz. Hypothesis (H.2) asks that and be bounded and that every component be in .
Under (H.2) and , belongs to and is the unique solution in that class of
The goal also records that does not depend on the choice of with a given law.
In the order the proof uses them: the second-order expansion on (Lemma 2.1); symmetry of mixed derivatives (Lemma 4.1); the substitution identity and flow property (3.4)–(3.5); the stability estimate (Lemma 3.1) and its consequence that depends only on (Remark 3.1); first- and second-order regularity of in (Lemmas 5.1, 5.2) and in (Lemma 6.1); the mean-field Itô formulas (Proposition 6.1, Theorem 6.1); the martingale identity (6.15); and uniqueness (6.19)–(6.20). A companion theorem states the existence and pathwise uniqueness of solutions of both SDEs under Lipschitz coefficients.
The result is a Feynman–Kac representation on the Wasserstein space: it identifies the expectation functional of a McKean–Vlasov diffusion with the unique classical solution of a second-order PDE in , of the type that appears as the master equation of mean-field games and as the dynamic-programming equation of mean-field control. It gives a mean-field Itô formula for functions of the state and of the law, which is the basic tool for verification arguments in these problems.
All results of the mission are proved in the paper, which takes the well-posedness of the SDEs from Carmona and Delarue. None is formalized: the platform has the Itô integral as an definition, but no Itô isometry, no Burkholder–Davis–Gundy inequality, no SDE existence theorem and no Itô formula (the classical Itô formula is posed separately as an open goal). Formalizing the mission produces a calculus on in Lean, together with existence, stability and flow results for McKean–Vlasov equations.
The obvious route, differentiating in by the chain rule, fails because is not a map between finite-dimensional spaces: the measure derivative of requires Fréchet differentiability of in , the identification of the derivative through a family of auxiliary linear SDEs indexed by a point , and estimates uniform in . A second difficulty is that the second-order expansion on has remainder of order , not , so the Itô formula is not a direct Taylor argument in and needs a partition argument with control of each increment. A third is regularity in time: is differentiable in only after the Itô formula has been applied to , and the time derivative must again be bounded and Hölder. The paper writes its proofs for and and leaves some estimates to the reader, so a solver must supply them.
Time is ℝ≥0, is EuclideanSpace ℝ (Fin d), measures are Measure (E d), and every condition on a measure argument is quantified over only. is the real value of the published WassersteinDRO.Duality.wassersteinDistance 2, finite on . Brownian motion, the Brownian filtration and the Itô integral are the published Peng1990.SMP objects, and the null sets are ReflectedBSDE.Existence.nullSigma. The standing assumptions of §3 are hypotheses of every statement: completeness, , independence of and , richness of , and the Lipschitz condition (stated even where (H.2) implies it). Matrices carry the Frobenius norm.
Solutions of (3.1) and (3.2) are processes in satisfying the integral equation at every almost surely, with for Itô integrals of . Statements about take solution families as hypotheses; the companion well-posedness theorem states that such families exist, and a sanity file shows that zero coefficients with constant solutions and satisfy every hypothesis. The decoupled equation takes a random initial value, so (3.4) needs no measurable selection in .
Derivatives in , and are genuine (HasGradientAt; HasDerivWithinAt on , one-sided at the ends). Derivatives in are witness functions with the Fréchet property of the lift, the lift being taken on the paper's own rich space; this rules out the trivializing reading in which every function is differentiable because the underlying space carries only Dirac laws. The subscript bounds the derivatives, not the function, except that (H.1)/(H.2) also require and themselves to be bounded on : this is the of (H.1) ii), read uniformly in as the paper's proofs use it, and without it the bounded time derivative of fails (e.g. ). The class additionally requires the derivatives entering the Itô formula to be jointly continuous in for ; this is the reading of the letter , and satisfies it. over an independent copy is the integral against the corresponding law. Where the page writes or without , the bounded classes the paper defines are used. The uniqueness statement ranges over every function of the class with its own derivatives.
A complete development needs the Itô isometry and BDG inequality for the published integral, Gronwall's inequality, strong existence for McKean–Vlasov SDEs, -differentiability of SDE solutions with respect to the initial condition, and a classical multidimensional Itô formula. The Lions-derivative calculus and the Wasserstein estimates are reusable for any mean-field mission. Contributions to any of these pieces are welcome.
First-order methods use function gradients to minimize an objective without solving a second-order subproblem at each iteration. Inertial methods also use the previous iterate, which can improve the convergence rate but complicates the choice of momentum and step size. Attouch, Chbani, Fadili, and Riahi study a family of such methods derived from continuous dynamical systems with Hessian driven damping. Their explicit strongly convex scheme, IGAHD-SC, uses a difference of consecutive gradients in addition to momentum and the current gradient. The difference represents the damping contribution without evaluating a Hessian matrix. Attouch et al., §5.2, pp. 28–29.
The question in this mission is quantitative. If the objective has strong curvature and a Lipschitz gradient, do the iterates, objective values, and a discounted sum of squared gradients decrease at the geometric rates claimed in Theorem 11? This is the final independent convergence theorem of the paper's series of discrete algorithms. Attouch et al., Theorem 11, p. 29.
Let be a real Hilbert space and a continuously differentiable objective. For , the paper calls -strongly convex when is convex. Let be a minimizer of . The paper assumes that the gradient is -Lipschitz for a positive constant : for every . Strong convexity makes the minimizer unique. Attouch et al., Definition 1, p. 19; Theorem 11, p. 29.
Choose parameters and , and write . Starting from arbitrary , IGAHD-SC determines for by
The two differences have different roles: is the inertial part, and is the Hessian damping term in this explicit discretization. The algorithm is exactly the displayed scheme on p. 28, with its two starting points free. Attouch et al., (25) and (IGAHD-SC), p. 28.
Theorem 11 assumes and the two smoothness bounds in (26). Define
Both constants lie strictly between zero and one. The mission's goal is the paper's three-part conclusion:
and
The milestones record the auxiliary vector and energy from the proof, their velocity and strong-convexity estimates, the gradient majorization, the one-step energy inequality, and the geometric energy bound. These are claims displayed by the authors on pp. 30–32, in the order in which they lead to the goal. Attouch et al., proof of Theorem 11, pp. 30–32.
The first two bounds give geometric decay of distance to the optimizer and of objective error for the specified parameter regime. The third controls a discounted accumulation of squared gradients. Together they describe more than convergence of the objective alone: the same run has explicit asymptotic rates for its points and gradient behavior. The rate constants depend on the strong-convexity parameter, step size, and allowed damping range. Attouch et al., Theorem 11, p. 29.
This result is proved in the cited paper; the open work here is its Lean formalization. A completed development would include a reusable representation of the explicit inertial run, a precise strong-convexity interface matching Definition 1, and the energy estimates that support the theorem. The formal statements in this proposal are proof targets, not claims that already have machine-checked proofs. The two comparison methods mentioned in Remark 10 use different discretizations or hypotheses, so their rate theorems cannot replace this target. Attouch et al., Remark 10, p. 29.
Ordinary smooth gradient descent is controlled by the current gradient and one step difference. Here the recurrence also contains the preceding gradient and the preceding step. A direct estimate of does not isolate a contracting quantity. The paper therefore tracks an auxiliary vector and an energy involving both the objective gap and that vector; the precise coefficients in the two bounds of (26) are needed for the final one-step inequality. The proof's intermediate display on p. 31 also changes a gradient index between lines, so each formalized displayed claim needs scrutiny against the recurrence and the final p. 32 inequality. Attouch et al., proof of Theorem 11, pp. 30–32.
Lean represents as a complete real inner-product space, by Mathlib's gradient, and the run as a predicate on a sequence obeying (IGAHD-SC) for every . The source's arbitrary initial pair is preserved. A witness and the hypothesis that it minimizes express the nonempty argmin assumption without taking an infimum of real values. The strong-convexity definition is exactly Definition 1. Positive , , and make every square root and step-size denominator meaningful. The first bound in (26) is written , which retains the paper's intended case; the paper later uses explicitly, so it is included. Attouch et al., pp. 19, 28–32.
The rates use =O[Filter.atTop]. Lean writes as , and the sum through as Finset.range (k - 1). For the finite range is empty; the asymptotic claim concerns large . The source prints in the sum limit and in its summand; both are read as . The goal itself mentions the iterates, objective values, and gradients, without assuming an energy decay bound. A complete proof can contribute reusable inequalities for strongly convex functions with Lipschitz gradients and geometric recurrences, alongside the paper-specific run and energy lemmas.
A cap in an affine or projective space over a finite field is a set of points no three of which are collinear; a cap is complete when it is maximal with respect to inclusion, so that every point outside it lies on a line through two of its points. Caps are closely connected with error-correcting codes: projective caps can serve as parity-check columns for linear codes with minimum distance at least 4. Constructing small complete caps explicitly is a long-standing question in finite geometry; Giulietti's survey collects the known families.
Counting the lines through pairs of points gives the trivial lower bound
for the size of a complete cap in a Galois space of dimension and order . A short timeline:
Let and let be the field with elements. The affine space has as points the vectors ; three points are collinear when they lie on a common affine line over .
For an additive subgroup of , is the set of points whose coordinate vectors lie in . A translation cap is a cap of the form . By Giulietti, Proposition 2.5, for a translation cap has at most points; one attaining this bound is a maximal translation cap.
On the projective side, let , so that . An -subspace of (an additive subgroup) of -dimension , the rank, defines the -linear set . It is scattered when every point meets in exactly , i.e. has weight one. A scattered linear set has rank at most (Blokhuis–Lavrauw); one of rank in the plane is called maximum.
For , even, and even, there is a complete cap in with
The exponent is an integer because is even.
Theorem 1.3 shows that the trivial bound (1) is sharp up to the factor in even dimension for every even square , extending to even dimension what the constructions of Segre and Pambianco–Storme give in odd dimension. The construction supplies caps near the elementary size lower bound in a parameter range where the paper reports no comparably small infinite family. Remark 4.8 of the paper extends the construction to complete caps of comparable size in . The proof also establishes Proposition 4.3, a dictionary between scattered -linear sets and translation caps, so that any new maximum scattered linear set yields new small complete caps.
The result is proved on paper; no machine-checked proof of it or of the cited results of [6] (Lemmas 4.5, 4.6 and the bound of Prop. 2.5, whose proofs are not in this paper) is known to exist. The mission produces a formal statement of Theorem 1.3, the cap–linear set correspondence, and formal statements of the three results the paper imports from [6].
Assembling Proposition 4.7 from the milestones is short. The difficulty lies in the inputs. The doubling construction requires showing that every point of outside lies on a secant, which uses the maximality in a counting argument; it is cited from [6], not proved in the paper. The existence of a maximum scattered linear set in is the deep input: Lemma 2.8 needs a bound on the value set of a non-permutation polynomial (Turnwald) and a point count on a plane curve over . A tempting shortcut, taking any maximal cap obtained by greedy extension, gives a complete cap of unknown and generally much larger size; the content of the theorem is the exact size.
Fin r → K for a finite field with ; collinearity is Mathlib's affine Collinear K, over itself. A complete cap is quantified against every point of .Set.ncard. The goal's size is written with natural-number division, exact because is even; maximality of a translation cap is the squared form , and the [6] bound is .Welcome contributions: a general library of caps and translation caps in ; the scattered-linear-set/translation-cap dictionary; a formalization of the doubling construction of [6]; transport of the -model of Theorem 2.10 to coordinates . The linear-set definitions mirror those of the companion mission on scattered linear sets and are reusable there.
The alternating direction method of multipliers (ADMM) solves linearly constrained problems whose objective splits into separately treatable blocks. For two blocks, , it alternates one minimisation of the augmented Lagrangian in each block with a multiplier update. Its convergence for closed convex has been known since the work of Glowinski–Marrocco (1975) and Gabay–Mercier (1976), and the survey of Boyd, Parikh, Chu, Peleato and Eckstein (2011) made it a standard tool in statistics, imaging and machine learning.
Many applications have three or more blocks: robust principal component analysis with noisy and incomplete data, latent-variable graphical model selection, image alignment. Practitioners therefore apply the direct extension of ADMM, which simply cycles through all blocks in Gauss–Seidel order before updating the multiplier. Whether this extension converges for convex problems remained open for years: convergence was known under extra assumptions (strong convexity with a restricted penalty, Han–Yuan 2012; orthogonality of coefficient matrices, Section 2 of the source paper), and modified schemes with correction steps were proposed precisely because no proof was available.
Chen, He, Ye and Yuan (Math. Program., 2014) settled the question negatively by an explicit three-block example. This mission formalizes that example and the paper's main theorem.
Problem (1.1). Given , , closed convex sets and convex functions , with a nonempty solution set,
Augmented Lagrangian (1.6). For a penalty and multiplier ,
Direct extension of ADMM (1.5). From : minimises over ; minimises over ; minimises over ; and . A sequence satisfying these four conditions for every is a run (IsRun15).
The example. System (3.1) is with columns , scalar unknowns, zero objective, and ; its unique solution is when is nonsingular. The paper takes
the instance example310. With the scaled multiplier , the state is (stateVec). The matrices (3.6) and (3.7) are built from the inner products and the columns, and (3.9).
For the instance (3.10), which satisfies the standing assumptions of (1.1), there are a three-dimensional subspace and a nonzero linear functional on such that for every and every starting point with
a run of (1.5) from exists and no such run converges.
The theorem shows that convexity alone does not make the cyclic three-block ADMM convergent, and the failure is robust: it holds for every penalty parameter and for an open half of a three-dimensional subspace of starting points, on a problem as simple as a nonsingular homogeneous linear system with zero objective. It explains why later convergent variants add assumptions (strong convexity, orthogonality, small step sizes, randomised block order) or modify the scheme, and it is the standard reference for that fact in the operator-splitting literature.
The result is proved in the paper; no machine-checked version is known. A formal version produces a certified negative example for the most widely used multi-block splitting heuristic, a reusable formal model of the extended ADMM (Problem, augLag, IsRun15) on which convergent variants can later be stated, and a worked instance of turning a numerically presented spectral argument (the paper prints its eigen-decomposition to four digits) into exact statements.
The first step, that the iteration on (3.1) is linear in and independent of , is elementary but requires extracting minimisers of convex quadratics from the minimiser conditions of the run. The main difficulty is exact spectral information about a specific rational matrix whose characteristic polynomial is times an irreducible quartic over with two pairs of complex roots of moduli about and . The paper's evidence is a floating-point eigen-decomposition; a proof must instead locate the roots exactly, for example by certified bounds, and must show that the divergent component is present for a whole real subspace of starting points rather than for one numerically chosen vector. Finally, unboundedness of the scaled state has to be transferred back to the original sequence for every .
Vectors are Fin n → ℝ, matrices Matrix (Fin p) (Fin n) ℝ, and in (1.6) is the dot product . Each is real-valued and convex on all of ; "closed" is automatic for such functions and is not stated separately. "Argmin" is read as "a minimiser": the run predicate does not select a minimiser, and the goal asserts that a run exists, so the non-convergence claim is not vacuous. The paper's blocks and multiplier components are 1-based, the Lean components 0-based. Convergence of the sequence is convergence of in the product topology; is never read by (1.5). "Divergent" means "not convergent". The "continuously dense half space of dimension 3" is for a three-dimensional subspace and nonzero linear , expressed in the coordinates ; and are chosen before , as in the paper. Requiring and rules out the trivial choices or . Eigenvalues are complex roots of the characteristic polynomial; a statement using only real eigenvalues would be wrong, since the only real eigenvalue of is . Norms enter only through "", where the choice of norm on is irrelevant. The rounded numbers of (3.11) are not used anywhere.
Every object is defined in ExtADMM.Diverge.Setting. The general definitions (problem, augmented Lagrangian, run) are written for arbitrary dimensions and are intended for reuse by later missions on multi-block splitting. Contributions welcome: proofs of the milestones, exact root localisation for the quartic factor of the characteristic polynomial, and general lemmas such as "a real matrix with an eigenvalue of modulus above one has unbounded orbits on a real subspace".
A decision maker wants to choose in a compact set to minimize an expected cost , but the distribution of is unknown; only independent samples are available. The standard remedy, minimizing the cost under the empirical distribution, is known to produce decisions whose realized cost exceeds the in-sample estimate: the "optimizer's curse" of decision analysis (Smith and Winkler, 2006) and overfitting in statistics. Distributionally robust optimization (DRO) replaces the empirical distribution by a worst case over a set of nearby distributions. Many such sets have been proposed, and the question of which one is best has no answer unless "best" is made precise.
Van Parys, Mohajerin Esfahani and Kuhn (arXiv:1704.04118v3, published in Management Science 67(6), 2021) give such a precise meaning. They ask for the least conservative data-driven decision rule whose out-of-sample disappointment decays exponentially at a prescribed rate under every possible data-generating distribution, and they prove that DRO over a relative-entropy ball of radius is that rule. This mission formalizes the prescription half of the result (Theorem 7 of the paper), in which decisions, not only cost estimates, are optimized. The prediction half (Theorem 4) is the subject of mission 1 of this series, and the extension to continuous state spaces (Theorem 10) is mission 3. All page and result numbers below refer to the arXiv version v3 (22 Dec 2019).
The random parameter takes values in a finite set . The model class is the probability simplex with the topology inherited from . The cost is continuous in for each , and . From a sample path the decision maker forms the empirical distribution . When the samples are drawn independently from , the probability of an event about is written .
A data-driven predictor is a continuous function ; estimates . A function is quasi-continuous if for every , every and every neighbourhood of there is a non-empty open on which (the set need not contain ). A data-driven prescriptor induced by is a quasi-continuous with for every . The family consists of all such pairs .
The prescription disappointment of a pair under a model is
the probability that the true cost of the prescribed decision exceeds its in-sample estimate. Pairs are ordered by their in-sample optimal values: iff for all . Problem (6) of the paper is the vector optimization problem
and a pair is strongly optimal if it is feasible and every feasible pair.
The relative entropy is , with and . The distributionally robust predictor and prescriptor are
with quasi-continuous (Definition 7). The estimator realization is the first argument of , the reverse of the usual Kullback–Leibler ball.
The proof of Theorem 7 also uses results posed as milestones of mission 1 of this series: the large deviation bounds of Theorem 1, (7a) and (7b) (p. 12); the continuity of (Proposition 3, p. 16); the inclusion of the disappointment set in from the proof of Theorem 3 (pp. 16–17); and the construction of a perturbed model with from the proof of Theorem 4 ((14)–(16), pp. 17–18). They are not posed again here.
Theorem 7 says that no decision rule whose prescriptions disappoint with probability decaying at rate can report a smaller in-sample optimal value than relative-entropy DRO, at any realization of the data. It turns a modelling choice (which ambiguity set to use) into a consequence of a statistical requirement, and it identifies the radius of the ball with the decay rate of the out-of-sample disappointment. Theorem 8 complements this with a finite-sample bound that holds before any data are observed.
The theorem is proved in the paper, and its proof is short given the earlier results; there is no machine-checked version. A complete formalization adds a finite-alphabet Sanov theorem with the infinity convention of the relative entropy, an elementary theory of quasi-continuous functions on the simplex (density of continuity points, selection of quasi-continuous minimizers from an upper semicontinuous arg-min map), and Berge's maximum theorem in the form used here. The paper itself only sketches several steps (the construction of "exactly as in the proof of Theorem 4", and the proof of Theorem 8 is omitted).
Theorem 7 does not follow from the predictor result (Theorem 4). The order compares only the in-sample optimal values, so a competing pair may use a predictor that lies below away from its own minimizers, and the pointwise comparison of predictors that settles Theorem 4 says nothing about such a pair. What the data can detect is governed by the large deviations of , which only see sets with non-empty interior in , while the competitor's prescriptor need not be continuous. Without quasi-continuity of the argument breaks: a selector that jumps to a cheaper decision only on a set with empty interior is invisible to the data, and the theorem is not claimed for such selectors. The existence half (Proposition 4) rests on a selection theorem for upper semicontinuous set-valued maps on Baire spaces (Matejdes 1987, Corollary 4), for which there is no Mathlib counterpart.
Lean conventions:
Fin d, and is the subtype of stdSimplex ℝ (Fin d) with its subspace topology.EuclideanSpace ℝ (Fin n), with decisions in the subtype ↥X and the Euclidean distance; is continuous in for each . These are the standing assumptions of §2 (p. 5).EReal, equal to unless .Ruled out:
Real.log would treat a probability that vanishes as having rate .Each of these makes the statement different from the paper's, and none is used.
Reusable infrastructure includes quasi-continuity (with the Bledsoe density theorem), Berge's maximum theorem for the minimum value, and finite-alphabet large deviations for empirical distributions. Contributions of any of these, or of the mission 1 milestones, are welcome.
Adam (Kingma and Ba, 2015) is the default optimizer for training neural networks. At step it keeps an exponential moving average of stochastic gradients and an exponential moving average of their squared coordinates, corrects both for their initialization at zero (the bias correction or debiasing step), and moves the iterate by coordinatewise. Despite its use, its convergence on nonconvex objectives was poorly understood when Barakat and Bianchi wrote their paper: Reddi, Kale and Kumar (2018) exhibited convex online problems on which constant-parameter Adam fails to converge, and earlier analyses either dropped the bias correction or replaced Adam by a modified algorithm.
Barakat and Bianchi (arXiv:1810.02263v4, SIAM J. Math. Data Sci. 2021) study Adam through the ODE method: as the step size with and , the interpolated iterates follow a non-autonomous ordinary differential equation, the continuous-time version of Adam. This mission formalizes their convergence theorem for that ODE (Theorem 3.2): trajectories started as Adam is started, with zero moment estimates, approach the critical points of the objective.
Let be continuously differentiable with locally Lipschitz gradient , and let be locally Lipschitz. In the paper is the objective and the coordinatewise second moment of the stochastic gradient; §7 only uses the two properties above. Assume is coercive ( as ) and coordinatewise for every . Fix constants with .
The state is , and is the part where . All vector operations are coordinatewise. The Adam field (3.3) is, for ,
and (ODE) is . The factors and are the continuous-time bias corrections; they blow up as . A global solution with initial condition is a continuous , continuously differentiable on , satisfying (ODE) for every , with . The critical set is .
The proof passes through the autonomous field , its semiflow on , and the notions of equilibrium point, strict Lyapunov function and asymptotic pseudotrajectory (APT) of a semiflow.
Assume in addition that has empty interior in . For every global solution with initial condition , the set is non-empty and
The theorem does not claim that converges; convergence to a single critical point needs a Łojasiewicz condition (Theorem 3.4, a separate mission).
The milestones are the numbered results of §7.1–7.3 used in the proof, in the order the proof uses them: positivity of along solutions (Lemma 7.4); decrease of along (Lemma 7.5, autonomous part); compactness of trajectories (Propositions 7.6, 7.7) and lower bounds on (Lemma 7.8); well-posedness of the autonomous system and its semiflow (Proposition 7.13); the abstract limit-set theorem for APTs (Proposition 7.14, quoted from Benaïm); the strict Lyapunov function (Proposition 7.15); and the APT property of the (ODE) solution (Proposition 7.17).
Theorem 3.2 is the deterministic core of the paper's analysis of Adam. Combined with the paper's tracking result (constant-step Adam converges in probability to the ODE solution as , Theorem 4.3) it says that for small steps Adam's iterates spend their time near critical points of ; it is also the input of the decreasing-step almost-sure convergence theorem (Theorem 5.2) and of the convergence-rate theorem (Theorem 3.4), which both rely on the same Lyapunov function and limit-set argument. The condition under which the Lyapunov function decreases is satisfied by the default parameters , .
The result is proved in the paper; to the best of current knowledge it has not been machine-checked. The mission produces a formal proof of the theorem, and reusable formal statements about semiflows on metric spaces: strict Lyapunov functions, and the limit set of a relatively compact asymptotic pseudotrajectory.
The obvious route is to show that decreases and apply LaSalle's invariance principle. This fails on two counts. First, (ODE) is non-autonomous, and LaSalle's principle is a statement about autonomous systems: the derivative of along the flow vanishes only on a set that depends on . Second, the field is singular: blows up at and is not Lipschitz near , because of , so neither existence and uniqueness nor continuous dependence on initial data come from standard theorems. The energy of the autonomous limit is a Lyapunov function but not a strict one: it is constant along some non-equilibrium orbits, so non-increase of an energy alone does not identify the limit points.
Each block lives in EuclideanSpace ℝ (Fin d) and is their product; Mathlib's norm on the product is the maximum of the three Euclidean norms, which is equivalent to the Euclidean norm of and changes no statement. and are abstract, with the hypotheses of the paper's §7 (Assumptions 7.1, 7.2, 2.3, 2.4); this generality implies the printed theorem for the , of (2.2). Solutions are maps constrained only on (or ), and the equation is required at only. The field is extended off by , as on p. 12 of the paper. A semiflow is Mathlib's Flow ℝ≥0 M, on the subtype or on a compact subset of it. The semiflow in the milestones is always assumed to be the flow of , never an arbitrary flow. The APT and limit-set definitions are the published StochApproxDyn.LimitSet ones.
The goal is stated for every global solution of the specific field (3.3), and keeps " is non-empty" in the conclusion. A statement about some solution of an unspecified field, or with " has empty interior" strengthened to " is finite", is a different theorem and does not count.
A complete development needs: Grönwall-type comparison and chain-rule arguments along trajectories; well-posedness of the autonomous system on and continuity of its flow; and the limit-set theory of asymptotic pseudotrajectories (Benaïm 1999), adapted to strict Lyapunov functions in the paper's sense. The last part is independent of Adam and reusable in stochastic approximation. Contributions to any milestone are welcome; Propositions 7.13 and 7.14 are the largest pieces of infrastructure.
In ordinary statistical learning, a hypothesis is chosen from training data drawn from a distribution and judged by its risk under that same . In practice the test distribution often differs from the training one: covariate shift, domain drift, adversarial perturbation of inputs. Distributionally robust learning replaces the risk at by the worst risk over a neighbourhood of . When the neighbourhood is a ball in a Wasserstein distance, the perturbed distributions may move mass to nearby points of the instance space rather than only reweight the observed ones, which makes the model a natural description of small domain drifts and adversarial perturbations (Esfahani–Kuhn 2018, Gao–Kleywegt 2016, Sinha–Namkoong–Duchi 2018).
Lee and Raginsky (NeurIPS 2018) asked whether minimising the empirical version of this worst-case risk learns: does the empirical minimiser come close, in worst-case risk, to the best hypothesis of the class, at the usual rate? Their §3.2 answers yes when every hypothesis is uniformly Lipschitz. Their §3.3, the subject of this mission, removes that assumption: one hypothesis with controlled growth is enough.
The instance space is a Polish metric space with metric and Borel -algebra; fix . For Borel probability measures on , the -Wasserstein distance is
the infimum over couplings of and . For a radius , is the Wasserstein ball around .
A hypothesis is a function , read as a loss; a hypothesis class is a set of them. The risk of under is . The local worst-case risk and the local minimax risk are
Given i.i.d. samples with empirical distribution , the local minimax ERM is
The standing assumptions are:
The complexity of is measured by the entropy integral , where is the covering number of in the uniform norm.
Under Assumptions 1, 2 and 4, for every , with probability at least ,
The goal carries the paper's constants. The mission does not ask for sharper constants; a proof of the stated bound closes it.
The result. Theorem 3 is a generalisation guarantee for Wasserstein distributionally robust ERM that needs no uniform smoothness of the class. The uniformly Lipschitz assumption of the companion Theorem 2 fails for most classes of interest when : a function with is constant (p. 6). Assumption 4 holds, for example, for regression with quadratic loss whenever the predictor class contains the zero predictor (p. 6). The second term of (11) decreases as grows, which quantifies how a larger ambiguity set screens out non-smooth hypotheses (Remark 4).
Formalizing it. The theorem has a published pen-and-paper proof (Appendix C.5 of the arXiv version); it has no machine-checked proof. A formalization produces machine-checked statements of the dual characterisation of Wasserstein worst-case risk on a bounded Polish space, of a symmetrization-plus-McDiarmid uniform deviation bound for a parametrised class, and of a Dudley-entropy bound on a product class. The proof (C.5) on p. 16 starts from an achiever of , which need not exist; the goal is stated without that assumption, so a complete proof also handles the infimum.
The obvious argument decomposes the excess risk through and bounds by a uniform deviation over . That step fails: is a supremum over a ball of measures, not an expectation, so it is not an empirical process in . Passing to the dual makes it one, but the dual multiplier depends on the sample and has no a priori bound, so the class over all is too large. Without uniform smoothness of there is no obvious a priori bound on , and the entropy of the resulting two-parameter class must still be controlled at rate . Strong duality itself (Proposition 4) needs the existence of optimal couplings and a measurable-selection argument on a Polish space; it is not in Mathlib.
MetricSpace with BorelSpace and PolishSpace instances; Assumption 1 is Bornology.IsBounded (Set.univ : Set 𝒵), and is Metric.diam Set.univ. Throughout, and (the paper's standing choice, p. 3).WassersteinLinOpt.Ball.wassersteinDist and wassersteinBall, which range over all Borel probability measures; on a bounded space this equals the paper's ball.The following formalizations would trivialize the goal and are ruled out: a bound for each fixed in place of ; an defined by Classical.choose of an unproved existence; a supremum over all measures instead of over the ball; and the real conversion of an infinite .
The infrastructure is reusable beyond this mission: Wasserstein strong duality on Polish spaces (Proposition 4 specialises the general optimal-transport duality of Blanchet–Murthy 2019, whose transport-plan form is a proved theorem on the platform as ModelRiskOT.Duality.theorem_1); Dudley's entropy bound for sub-Gaussian processes indexed by infinite classes; and McDiarmid's inequality for suprema of empirical processes. Contributions of these general tools, as separate theorems, are welcome. Source: the arXiv v2 preprint, which is the NeurIPS 2018 camera-ready text followed by the supplementary appendices.
A decision based on observed data can change when the data law differs from the one used to choose it. Distributionally robust optimization addresses this by evaluating each decision against a family of nearby probability laws. Optimal transport gives one way to define “nearby”: a candidate law is admissible when probability mass can be moved from the baseline law at a bounded expected cost. For a linear decision rule, the resulting worst-case expectation is usually harder to optimize than an ordinary sample-average loss. Blanchet, Murthy, and Zhang identify a dual objective whose variables are the decision vector and a scalar transport multiplier, then study its curvature near the multipliers that actually minimize it (Blanchet–Murthy–Zhang, 2022).
The paper proves that this dual objective is jointly strongly convex on a specified region for sufficiently small transport radius. This matters because ordinary convexity allows flat directions in the joint decision–multiplier space. The joint lower Hessian bound gives local curvature in every direction with one positive modulus that remains independent of the radius apart from the paper's explicit factor (Theorem 4, p. 11).
Let have a baseline probability law , and let a decision be a vector in a nonempty compact convex set . The loss of a possible outcome is for a convex function . A state-dependent positive-definite matrix sets the cost of moving mass from to :
Assumption 1 requires this cost to be lower semicontinuous and the eigenvalues of to lie between positive constants and for -almost every . Assumption 2 requires at most quadratic growth of and a finite fourth moment of . The ambiguity radius is positive (Assumptions 1–2, pp. 9–10).
The paper's dual objective is an expectation under the known law . Write . For a scalar and an auxiliary scalar , set
This value may be . Under the paper's duality conditions, minimizing over gives the worst-case loss at (Theorem 1 and (7), p. 10).
Assumption 3 bounds above by and excludes an almost surely zero for each . Assumption 4 makes compact. Lemma 6 supplies positive constants bounding uniformly over . With , the constants are those of (28), and
Theorem 3 first gives a bounded Hessian on and a positive lower bound on its block when , with the explicit from p. 36. The goal, Theorem 4, adds Assumption 5: is locally strongly convex and, at each , the loss derivative and the linear score are simultaneously separated from zero with positive probability. It asserts the joint bound
The order of the quantifiers is part of the target: works for every sufficiently small (Theorems 3–4, p. 11).
The Hessian bound makes the joint dual parameters locally identifiable by curvature on a region that contains every dual optimizer. In the paper, this structure also underlies the analysis of algorithms and of how the optimizer changes with the transport radius (Proposition 1, p. 11; §3 and §5.4). Theorem 4 is already proved in the paper; this mission asks for its machine-checked formalization, together with the stated bounds on multipliers, the maximizing scalar, and the intermediate curvature results. The general optimal-transport integral used here already has a published Prove2Me definition from Blanchet and Murthy's earlier model-risk work. The new definitions specify this paper's Mahalanobis model, regions, and smoothness assumptions.
Convexity alone gives only a nonnegative Hessian; it cannot produce a strictly positive joint lower bound. Even curvature of does not by itself control directions that combine a change in with a change in . The inner supremum over can become infinite outside its effective domain, while at its maximizer ceases to be unique. The theorem therefore needs a region where the dual objective is finite and differentiable and a probabilistic condition that prevents the relevant score and derivative from vanishing together. The target keeps the actual scale instead of settling for a radius-dependent positive constant (§2.2.2 and Remark 4, pp. 10–12, 39).
Lean uses EuclideanSpace ℝ (Fin d) for , a Borel probability measure for , and EReal for and the inner supremum. The reused extended-real integral records the and cases; the Hessian is taken only where is finite on a neighborhood and its real representative is differentiable there. Quadratic Hessian forms use , since Lean's product norm is not the paper's Euclidean norm. The compact set is explicitly nonempty, and the positive ambiguity radius is quantified inside the goal so that and are uniform in . Theorem 3 additionally assumes for the proof's explicit formula for : nonempty compact would make that formula zero. Assumption 5 already gives in the goal.
The goal retains Assumption 5's per-decision quantifiers. That assumption itself excludes : its strict score event is empty at . Intermediate statements where the printed wording includes but the claim fails there state explicitly. Lemma 5 also states the differentiability and positive-multiplier conditions needed for its derivative and division. Proposition 9(b)'s printed strict curvature-margin inequality is corrected to the nonstrict inequality derived in its proof; its original wording is preserved in the milestone quotation. The claims are about the expectation , with independent of , rather than a pointwise or merely convex substitute.
A complete development needs measurable extended-real integration, the matrix quadratic form and its inverse, almost-everywhere spectral bounds, differentiability under an expectation, and Hessian estimates for an optimized scalar. The transport integral, the assumptions and constants, and the multiplier bounds are intended as reusable interfaces for the companion missions. Contributions that close the listed lemmas or add the paper's omitted second-order kernel formula are within scope.
A linear two-stage stochastic program chooses a first-stage decision before an uncertain parameter is revealed, and pays the optimal value of a second-stage linear program once the realization is known. Such programs are the basic model of planning under uncertainty in operations research, and their computational complexity determines which solution methods can be expected to work. In 2006, Dyer and Stougie argued that linear two-stage stochastic programs with fixed recourse are #P-hard even when the random data follow independent uniform distributions. Hanasusanto, Kuhn and Wiesemann showed that this proof is not correct and gave a corrected one, which also covers approximate evaluation to sufficiently high accuracy; their note also shows that, when the second-stage constraint matrix itself depends on (random recourse), even finding an approximately optimal decision is strongly NP-hard.
This mission formalizes that last result, Theorem 4 of the note. The previous missions of the series treat the hardness of evaluating the expected recourse with fixed and with random recourse.
The Integer Feasibility Problem. An instance is an integer matrix and an integer vector such that the polytope lies in the unit cube . The question is whether some binary vector satisfies . This problem is strongly NP-hard (Garey and Johnson).
The second-stage problem. For a decision and a realization , write for the all-ones vector and consider
The coefficient of in each constraint depends on , which is what makes the recourse random.
Problem (11). With uniformly distributed on ,
The second stage is not feasible for every (the problem lacks relatively complete recourse), so a decision is feasible only if the second stage is feasible for every . Let be the infimum of the objective over feasible decisions. A feasible is -optimal if
The constant . Lemma 4 fixes with and for every row .
For an instance with nonempty polytope, , as above, , and any -optimal decision of (11),
This is the mathematical content of "determining an -optimal decision is strongly NP-hard whenever ": a single comparison of any approximate decision with a threshold answers the NP-hard question.
The result. Theorem 4 implies that, unless the problems in NP admit an efficient solution scheme, there is no fully polynomial-time approximation scheme for two-stage stochastic programs with random recourse, even with a one-dimensional first stage and a uniform distribution. Together with the #P-hardness results of the same note, it delimits what algorithms such as sample average approximation can guarantee once relatively complete recourse and fixed recourse are dropped.
Formalizing it. The theorem has a short published proof, but that proof leaves several conventions implicit: the index set of the constraint block, the meaning of first-stage feasibility, and the condition on when has a zero row. A machine-checked version fixes each of them and verifies that the claimed formula for is correct under the chosen reading. To our knowledge none of these statements has been formalized before. The objects are elementary (finite-dimensional linear programs, a set integral on the unit cube), and the second-stage solution and rounding lemma are reusable for related reductions from integer feasibility.
The individual steps are short; the difficulty is bookkeeping across three layers. The second stage is an optimisation over whose feasibility depends on the sign pattern of ; the first stage requires a supremum over a polytope to be attained (compactness), and the expected recourse to be the same integral for all feasible decisions (integrability of a piecewise-defined value function over the cube). The tempting shortcut, reading off feasibility from the value of , fails: an infeasible linear program has no meaningful value, and treating it as cost would make every decision look optimal. Similarly, an almost-sure notion of feasibility looks natural for a stochastic program but invalidates the formula for whenever the polytope has measure zero, as it typically does for integer feasibility instances written with equalities.
All objects live in SPHardness.IntFeas. Vectors are functions on Fin n and Fin m; and are integer and are cast to , and integrality is kept because Lemma 4 depends on it. The uniform law on is Lebesgue measure restricted to the cube (volume ); expectations are set integrals. The recourse value, and are sInf/sSup in , and second-stage feasibility, first-stage feasibility and -optimality are separate predicates, so no statement depends on the junk value of an empty infimum.
Pinned readings and added conventions:
Strong NP-hardness, the FPTAS consequence, running times and encoding lengths are not formalized; the goal is the correctness of the reduction. A statement in which ranges over arbitrary reals satisfying a hypothesised identity, rather than over -optimal decisions of the program (11) built from , would be trivial and is ruled out: every object in the goal is defined from the instance.
Contributions welcome: proofs of the milestones, in particular measurability and integrability of the recourse function on the cube and attainment of , which are reusable for other piecewise-linear recourse functions.
The alternating direction method of multipliers (ADMM) is one of the standard splitting methods for problems of the form , in which a nonsmooth term acts on a linear image of the variable. It is used in signal and image processing, statistical learning and matrix completion, and in many of these applications or is nonconvex: sparsity penalties such as or with , rank constraints, or indicator functions of nonconvex sets. For convex problems the convergence theory of ADMM is classical; for nonconvex problems the questions of whether, and how fast, the iterates converge were open until the last decade.
R. I. Boţ and D.-K. Nguyen (arXiv:1801.01994v2, Math. Oper. Res. 45(2), 2020, DOI) analyse a proximal ADMM with variable metrics and its linearized variant in the nonconvex setting. Their first main result (Theorem 14, the subject of the companion mission of this series) shows that bounded iterates converge to a KKT point when a regularization of the augmented Lagrangian has the Kurdyka–Łojasiewicz property. This mission formalizes their second main result, Theorem 20: when that function has the Łojasiewicz property with exponent , the iterates converge in finitely many steps, linearly, or sublinearly, according to the value of .
Timeline. Łojasiewicz (1963) proved his gradient inequality for real-analytic functions; Attouch and Bolte (Math. Program. 2009) derived from its nonsmooth version the rates / / for the proximal point algorithm; Bolte, Sabach and Teboulle (Math. Program. 2014) gave a general KL-based convergence scheme (PALM); Li and Pong (SIAM J. Optim. 2015) proved convergence of a proximal ADMM under KL assumptions; Boţ and Nguyen (2018/2020) treated variable metrics, relaxation parameters , and the linearized variant, with explicit rates.
Let be proper and lower semicontinuous, differentiable with -Lipschitz gradient, and linear. The augmented Lagrangian with parameter is
Given positive semidefinite matrices , and , Algorithm 1 produces from any starting point by: minimizes ; minimizes ; and . Algorithm 2 replaces in the -step by .
Assumption 2 requires and to be bounded below, to be surjective with (), , , , and for all , where and are explicit functions of .
The analysis runs on the regularized augmented Lagrangian of Section 3
with explicit constants , . Along a run, . If the run converges to , put , and . has the Łojasiewicz property at with constant and exponent if
for all near , where is the limiting subdifferential.
Under Assumption 2, for a bounded run converging to at which has the Łojasiewicz property with exponent :
All constants are existential and independent of ; the goal fixes only the shape of each rate.
Theorem 20 is the quantitative half of the paper: it converts a local growth condition on one explicit function into convergence rates for the iterates of two practical nonconvex splitting methods. Since semi-algebraic functions satisfy the Łojasiewicz property with some exponent, the theorem applies to most of the sparsity- and rank-type models for which ADMM is used, and it explains when finite termination or linear convergence is to be expected. The intermediate results (Lemma 15 in particular) are the standard route from a Łojasiewicz inequality to rates and recur in the analysis of many first-order methods.
The result is proved in the paper; to our knowledge no part of it has a machine-checked proof. The mission produces a formal statement and proof of the rates, with every constant of the paper defined explicitly, and records where the paper's constants need recomputing: the constants and of Lemma 9 are reused on p. 26 for a regularization whose gradient is twice as large.
Lemma 15 is elementary but delicate: the recurrence has a lag and, for , a nonlinearity that a direct induction does not control, and the index bookkeeping determines the exponent. The rates for require a bound on an explicit subgradient of , whose limiting subdifferential involves the nonsmooth , so the calculus of limiting subgradients for a sum of a lower semicontinuous and a smooth function on a product space is needed. Transferring rates from to the iterates needs a finite-length estimate with explicit constants, uniform in the tail. A tempting shortcut, applying the Łojasiewicz inequality directly to , fails: does not decrease along the iterates; only the regularized does.
Vectors live in EuclideanSpace ℝ (Fin n); takes values in EReal and is proper and lower semicontinuous; and take values in EReal. Points of form a nested WithLp 2 product, so the norm and the inner product are the Euclidean ones of the paper. The limiting subdifferential is the published NonconvexSplitting.Shared.LimitingSubdiff. The two algorithms are the constructors of an inductive type; a run is a relation (any minimizer may be taken), and every statement holds for both. and are replaced by arbitrary valid bounds. is , which the paper shows equals .
The Łojasiewicz hypothesis requires the inequality for every subgradient, so that , and only at points with , the convention ; with Lean's the hypothesis would be unsatisfiable at , and a Łojasiewicz hypothesis that no function satisfies, an Assumption 2 that no data satisfy, or a rate whose constant depends on would each make the targets trivial. Assumption 2 together with the run predicate is satisfiable (checked on a one-dimensional instance), and all constants are quantified before .
Labelled corrections: uses as displayed on p. 25 (not ); and are recomputed for the Section 3 ; Lemma 17 asks for ; Lemma 19 assumes , since for the paper's is .
Needed infrastructure: calculus of the limiting subdifferential for the sum of a lower semicontinuous function and a function on a product space, the descent lemma, and real-power estimates for sequences. Lemma 15 is independent of ADMM and reusable. Proofs of individual milestones are welcome in any order.
Many first-order optimization methods are discretizations of second-order differential equations. In the continuous system the velocity carries the momentum, and the damping terms decide how fast the trajectory settles at a minimizer. Attouch, Chbani, Fadili and Riahi study inertial systems with Hessian driven damping: a friction term proportional to , which damps the oscillations that plain heavy-ball and Nesterov-type dynamics show. Because is the time derivative of , a discretization can use differences of gradients and never evaluate a Hessian. Attouch et al., §1, pp. 1–3.
For a -strongly convex objective, the paper shows that the dynamic
makes decay like (Theorem 7, p. 19). Section 5.1 asks whether that rate survives an implicit (proximal) discretization. The answer is Theorem 9: the algorithm converges linearly, and the gradients also go to zero at a geometric rate. The authors remark that they know of no earlier result of this kind for such a proximal algorithm. Attouch et al., Theorem 9 and Remark 9, p. 23.
Let be a real Hilbert space with inner product and norm , and let be convex and continuously differentiable, with gradient . For , is -strongly convex when is convex (Definition 1, p. 19). Such an has at most one minimizer; write for it.
For and , the proximal point is the minimizer of .
Fix and a step (the paper writes with the step size). Starting from arbitrary , the inertial proximal algorithm with Hessian damping for strongly convex functions, (IPAHD-SC), produces for
The first line is an extrapolation with momentum and an explicit gradient correction; the second is one implicit (proximal) step. Attouch et al., (IPAHD-SC), p. 23.
The rates are
both in , and the constant of the theorem is
Assume and . Then every sequence generated by (IPAHD-SC) satisfies, for every ,
and
The milestone targets are the paper's displayed intermediate claims, in order:
Theorem 9 gives linear convergence of a proximal algorithm for a smooth strongly convex objective with no Lipschitz assumption on and no upper bound on the step in terms of a smoothness constant: the step condition involves only the strong convexity modulus. It also gives a geometric rate for a weighted sum of squared gradients, which the authors present as new for proximal algorithms of this type. In §5.1.2 the same estimate, applied to the Moreau envelope, gives linear convergence for nonsmooth strongly convex objectives (Theorem 10), and §5.2 shows the explicit gradient counterpart (Theorem 11).
The result is proved in the paper. A formal development would certify the exact constants (, , and the factor in (24)) and the index bookkeeping of the gradient sums, where the printed proof contains small slips. It would also provide reusable proximal optimality and strong convexity results for later formalizations.
The continuous-time estimate of Theorem 7 does not transfer term by term to the discrete energy . Its difference contains cross terms such as and , whose signs are not automatic. The upper bound on and the lower bound on must both survive the resulting estimates. The gradient conclusion introduces a separate weighted sum, with different index ranges in Theorem 9 and the final displayed line of its proof. The algorithm begins at and uses two free initial points, and .
The Lean development works on a real Hilbert space H (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace), with Mathlib's gradient f. Conventions:
ConvexOn ℝ Set.univ f and ContDiff ℝ 1 f, and -strongly convex in the literal sense of Definition 1 (HessianDamping.DINSC.IsStronglyConvex, convexity of ), with . The standing assumption is a point with for every , so is . The step is positive, as the page implies (, ). The parameter hypotheses are and , as printed.GoldenRatioVI.Shared.IsProxPoint: minimizes . No proximal function is defined. A run imposes the step for every ; and are free.Real.sqrt (μ * s). is an integer power. is a sum over Finset.range (k - 1). is =O[Filter.atTop] with the constant allowed to depend on all the data. The side claims and are a conjunct of the goal.Infrastructure needed: the first-order optimality condition of a proximal step for a differentiable function, and the first-order characterization of strong convexity, , from Definition 1. Both are reusable well beyond this mission, as is the iteration of linear recursive inequalities . Contributions of either kind, and proofs of the individual milestones, are welcome.
The alternating direction method of multipliers (ADMM) solves a constrained optimization problem by minimizing an augmented Lagrangian over one block of variables at a time and then updating a multiplier. Its two-block version had established convergence results. Applying the same cycle to three or more blocks was natural in models whose objective separates into several terms, but its convergence was unresolved when Chen, He, Ye and Yuan wrote this paper. Their analysis gives both a sufficient condition for convergence and, elsewhere in the paper, a counterexample to unrestricted convergence. This mission concerns the sufficient condition: the first and third constraint matrices are orthogonal in the sense . Chen, He, Ye and Yuan (2014)
The condition matters because the third block is separated from the first in the quadratic part of the augmented Lagrangian, while the middle block still participates in both updates. The result therefore covers a genuine three-block algorithm. It identifies what the direct cyclic extension can guarantee under this structure. The companion result gives an ergodic rate for averages of auxiliary iterates, from any starting point.
The three-block problem has variables , matrices , and a vector :
Each is closed and convex, each is convex, and the primal solution set is nonempty. For , write . The augmented Lagrangian is . The minus sign in front of fixes the sign of the multiplier step of (2.4c).
The paper analyzes a reordered cycle, numbered (2.4): minimize in , minimize in , update , then minimize in . The input state is ; is an intermediate variable. Each minimization may choose any minimizer. The reordered cycle is the cyclic direct extension with shifted by one index. A run is any sequence satisfying all four update conditions. Chen et al., pp. 4–5
Let , , and . The affine map has blocks . The variational inequality solution set consists of for which for every . Such points are the KKT points used in this mission. The paper employs and without defining them; these definitions fix their intended meaning.
Let , and let be the corresponding projection of . With the positive semidefinite block matrix in equation (2.11), the main target is Theorem 2.4:
If and have full column rank and , the entire sequence converges to a point of . The milestone list follows the paper's affine monotonicity statement, Lemmas 2.1–2.3, the displayed contraction, the summability and vanishing correction terms, and the cluster-point variational inequality. Chen et al., pp. 5–9
Theorem 2.5 bounds a gap at the average , where is the auxiliary point of (2.13). For every , the target is
This companion is stated, as on the page, for an arbitrary starting point. Chen et al., p. 9
The contraction gives a quantitative decrease relative to any variational inequality solution, even though is only semidefinite. Combined with the rank assumptions, it yields convergence of all primal blocks and the multiplier to a KKT point. The auxiliary average gives a finite-iteration gap bound with an explicit coefficient. These statements locate a useful structural regime inside a method that the same paper shows can diverge without additional conditions.
The formal development records the whole update cycle, the variational inequality, and the two block operators and . It leaves the named theorems as proof targets; compiling their statements does not claim a machine-checked proof. The definitions and intermediate inequalities can be reused when formalizing other cyclic splitting schemes or comparing this one with two-block ADMM.
The familiar two-block ADMM convergence argument cannot simply be applied to a three-block cycle: the middle iterate is updated between the first and third blocks, and the multiplier update sits before the next first-block minimization. The resulting one-step inequality contains a correction involving the previous and next essential states. Even after that correction is controlled, is semidefinite, so contraction in its quadratic form alone does not imply convergence of every coordinate. The full column rank conditions provide the additional control demanded by the paper's conclusion.
Vectors are functions on Fin n; matrices are Mathlib matrices. Every occurrence of a squared Euclidean norm in the paper is represented by a dot product or the expanded quadratic form. Mathlib's default norm on a function vector is a sup norm, so it is not used for those squares. The topology in the final convergence statement is the product topology on the four vector blocks. The block labels in the paper correspond to separate fields in Lean. The initial is unused by the run predicate. A zero-dimensional block is allowed when the stated conditions still make sense.
There are disclosed repairs to the printed text. Lemma 2.3 and the contraction are restricted to : their derivation uses the preceding optimality condition, which an arbitrary initial point need not satisfy. The convergence part additionally assumes , since the paper assumes a primal optimizer but supplies no constraint qualification guaranteeing a KKT point. Lemma 2.2's displayed uses , while its inequality and the run use ; Lean uses the latter. Theorem 2.5's verbal assertion that is represented as the indexed average .
The convex objectives are real valued on all of , as on p. 1. Such a convex function is continuous, so the paper's word “closed” adds no extra condition here. Runs quantify over actual minimizers and are not constructed by a default-valued argmin; this prevents an empty subproblem from creating a fictitious iterate. A complete proof can contribute the convex first-order conditions, matrix identities, summability argument and finite-dimensional convergence steps. The reusable interfaces are the three-block problem, run, variational inequality and block quadratic forms.
The ℓ1-regularized least squares problem (the Lasso, or basis pursuit denoising) is the model problem of compressed sensing and sparse inverse problems: given a matrix , data and a weight , one seeks a vector that fits while having few nonzero entries. The standard first-order method for it is the iterative shrinkage thresholding algorithm (ISTA), a forward-backward splitting scheme whose backward step is componentwise soft thresholding. Each iteration costs two matrix–vector products, which is why ISTA and its variants are used on problems far too large for interior-point methods.
The classical complexity guarantee for ISTA is , the rate of the proximal gradient method on any convex composite problem (Beck–Teboulle 2009). ISTA itself goes back to Daubechies–Defrise–De Mol 2004, and its link with forward-backward splitting to Combettes–Wajs 2005. An asymptotic linear rate was known, with an explanation through partial smoothness (Liang–Fadili–Peyré), but there was no global, explicit, non-asymptotic bound. Bolte, Nguyen, Peypouquet and Suter (arXiv:1510.08234v3, Math. Program. 2017) derive such a bound from two ingredients: an error bound for the Lasso objective on balls, with a constant written through a Hoffman constant, and their general theory turning a Kurdyka–Łojasiewicz (KL) inequality into complexity bounds for descent methods.
Write with the Euclidean norm , and . For a matrix , is its spectral norm, the operator norm from to with Euclidean norms. The objective is
with and . Put and . Then is convex with gradient , Lipschitz with constant .
Given stepsizes with and any , ISTA is
where is the minimizer of . More generally, in a real Hilbert space with proper, lower semicontinuous and convex and convex with -Lipschitz gradient, the forward-backward method takes to be a minimizer of .
A sequence is a subgradient descent sequence for a convex with constants if and, for every ,
With , has the KL property on a set with desingularizing function if for every such and every .
A number is a Hoffman constant for a pair of matrices if, for every right-hand side with and intersecting, for all .
Put and , and . Let be such that whenever . Then ISTA converges to some and
The result. The theorem replaces the sublinear guarantee of ISTA by a global linear rate with explicit constants depending only on , , , the stepsizes, and a Hoffman constant. It also bounds the distance of the iterates to the limit, not only the objective gap, and needs no uniqueness of the minimizer. Through , it shows that conditioning of the objective near its minimizers, rather than strong convexity, governs the complexity of the method. The general machinery behind it (Theorem 16 of the paper, a separate mission of this series) applies to any method producing subgradient descent sequences.
Formalizing it. The result is proved on paper, and no machine-checked proof of it or of its ingredients is known. A formalization would give a verified linear-rate certificate for a widely deployed algorithm. It would also yield reusable lemmas: the descent and relative-error properties of the forward-backward method in a Hilbert space, and quadratic growth for the Lasso on balls. Lemma 10 rests on an external result (Beck–Shtern, Lemma 2.5) that a complete development must also formalize.
The Lasso objective is not strongly convex when has a nontrivial kernel, and its minimizer need not be unique. The textbook argument for linear convergence of proximal gradient methods, which uses strong convexity, therefore does not apply. Quadratic growth is the substitute, but it holds only on bounded sets, with a constant degrading in the radius. The analysis must therefore show that the iterates stay in a fixed ball and keep track of how the growth constant enters the rate. Deriving the explicit requires recasting the problem as a quadratic program over a polyhedron with facets and invoking a Hoffman-type error bound for it.
Citations refer to the arXiv preprint arXiv:1510.08234v3 (20 July 2016), with its numbering and pages; the journal version is not used. is EuclideanSpace ℝ (Fin n) and matrices act through Matrix.toEuclideanLin. Spectral norms are operator norms of the associated continuous linear maps, never Mathlib's default entrywise matrix norm. The data vector, called in §3.2.1 of the paper and in §5.3, is throughout; is the constant of (H2).
Functions with values in are EReal-valued. The convex subdifferential, Γ₀, , the prox predicate and the class of desingularizing functions are reused from published platform definitions. The stepsize condition is written , so that (where ) is covered. is the infimum of , and is a real power.
In the goal, is any positive constant satisfying the error bound on the ball of radius ; it is not fixed to the value (10) and not existentially quantified. The constants are fixed formulas, never existentials. A statement with an unspecified constant, with chosen after the sequence, or with the stepsize hypothesis written as (unsatisfiable or vacuous at ) would trivialize the goal and is ruled out.
The subgradient-descent and KL notions duplicate, in the sub-namespace ErrBoundCplx.ISTA, those of the series' first mission, because draft items cannot import each other. Proofs of any milestone are welcome, in particular Proposition 13 and the KL consequence of Lemma 10, which are self-contained. A formalization of Hoffman's error bound and of Beck–Shtern's Lemma 2.5 is the main infrastructure Lemma 10 needs.
Linear sets are the main tool for building point sets with few intersection sizes in finite projective spaces: sets meeting every hyperplane, two-intersection sets, translation ovoids, and the geometric side of finite semifields and rank-metric codes (Polverino, 2010). Among them, scattered linear sets are those whose points all carry the smallest possible weight, and a scattered linear set of the largest possible rank is called maximum scattered. By Blokhuis and Lavrauw (2000), a maximum scattered linear set of of rank is a two-intersection set with respect to hyperplanes, so each one yields a two-weight code and a strongly regular graph.
Timeline.
Let be a prime power, , and let be an -dimensional vector space over ; has as points the spans of nonzero . An -subspace is a subset closed under addition and under multiplication by . It defines the -linear set
whose rank is . A linear set comes paired with , so every statement here is about . The weight of a point is , and is scattered when every point of has weight ; equivalently, for every nonzero ,
The plane construction (§2). Fix and the field with its subfields and . As an -space has dimension , so . For and an -linear the paper studies
with a monomial or a binomial . The relative norms enter the hypotheses.
For even and , in each of the cases (a) , ; (b) ; (c) , ,
Theorem 1.2 gives maximum scattered linear sets, and hence two-intersection sets, two-weight codes and strongly regular graphs, for infinitely many with odd, a regime where earlier existence results covered only a few values of . The case feeds the paper's second main result: scattered -linear sets of of rank are translation caps, from which complete caps of size in are built.
All statements are proved in the preprint; none has a machine-checked proof. Formalizing them requires a usable theory of subfields of a finite field as Frobenius fixed fields, relative norms and their images, linearized polynomials and their trace adjoints, and the passage between -dimension, cardinality and weight. Each of these is reusable for later work on linear sets, MRD codes and semifields.
The criterion of Proposition 2.2 reduces scatteredness to a polynomial system, but the system has to be solved for a specific . For the monomials this rests on the solvability of in , a norm condition interacting with the gcd hypotheses. For the binomial with , the existence of a suitable (Lemma 2.8) needs a value-set bound for non-permutation polynomials (Turnwald, 1995) and a point count on a plane curve. The higher-dimensional statement then needs the elementary bound for scattered to obtain the rank equivalence in Theorem 3.1. A tempting shortcut, taking or any small subspace, is scattered but has the wrong rank; the content is in the rank .
Fin r → K; the plane of §2 on itself.Data-driven decision making estimates the cost of a decision from training data and then optimizes that estimate. The optimized estimate is biased downwards: the decision that looks best on the training data tends to disappoint on fresh data. Distributionally robust optimization counters this by optimizing the worst case of the estimate over all distributions within a radius of the empirical distribution, measured by a chosen distance function . Many distance functions are in use (φ-divergences, Wasserstein distances, moment sets), and the choice is usually justified by tractability.
Bertsimas and Van Parys, Bootstrap robust prescriptive analytics (arXiv:1711.09974v2), measure disappointment on bootstrap data: resamples drawn with replacement from the training data. Their Theorem 6 shows that with the entropic bootstrap distance the bootstrap disappointment decays exponentially in the sample size at rate at least . Proposition 1, the subject of this mission, is the converse: is the smallest distance function with this guarantee. Any distance that is strictly larger than near some distribution admits a nominal formulation whose disappointment decays strictly slower than . The result is in the spirit of Van Parys, Esfahani and Kuhn (arXiv:1704.04118), where the relative entropy is shown to be the optimal ambiguity set for i.i.d. data.
The distinct training points form a finite set , written in Lean. A distribution on it is a vector with nonnegative entries summing to one; the simplex of all such vectors is . The training data have the empirical distribution , which gives positive weight to every point of .
The bootstrap distance (Definition 6, Eq. (27)) is the relative entropy
with and if some .
A distribution distance function (Definition 4) is a map that is nonnegative, vanishes exactly on the diagonal ( iff ), and is convex in its first argument. is one.
A bootstrap sample of size is independent draws from (Eq. (14)); its law is the product , and its empirical distribution is , the frequency of each point of among the draws.
A nominal formulation here is a loss with cost estimator . Its robust counterpart (Eq. (24)) replaces the estimate by , and its disappointment set is
the bootstrap distributions on which the realized cost exceeds the robust budget.
Let be a distribution distance function, with , and a neighbourhood of , open in , on which . Then there is a loss whose disappointment set satisfies
stated in Lean in the equivalent form: for some , eventually .
Proposition 1 turns Theorem 6 from a sufficient condition into a characterization. Theorem 6 says the bootstrap distance guarantees disappointment rate ; Proposition 1 says no distance function that is larger than on an open set does, for some nominal formulation. A practitioner who wants the bootstrap guarantee with the least conservative ambiguity set therefore has no better choice than in this sense. The result is one instance of a pattern in data-driven optimization, where large-deviation rate functions appear as the optimal ambiguity sets.
The paper's proof is a short combination of three standard facts: strict separation of convex sets, Sanov's theorem, and convexity of relative entropy. None of the three is available on the platform in the form needed. Sanov's theorem for empirical distributions on a finite alphabet has no machine-checked proof in Mathlib or on the platform; the lower bound (31) is a self-contained, reusable result of independent interest. The separation step needs strict separation inside the affine hull of the simplex, which Mathlib provides only in the ambient vector space. The result is proved on paper; none of it is formalized.
The separation and convexity steps are routine once the relative topology of the simplex is handled. The central difficulty is the lower bound (31), a large-deviation lower bound for the empirical distribution of i.i.d. draws. The bootstrap probability of an event is a sum of multinomial probabilities over the empirical distributions with denominator that fall in the event, and the bound must hold for every point of the relative interior, including points on the boundary of the simplex, where some coordinates vanish and the distance is not differentiable. An argument that only treats distributions of full support, or only open sets of , does not cover these points.
A second difficulty is bookkeeping between the three topologies in play: the ambient space , the simplex , and the affine hull in which separation takes place.
stdSimplex ℝ ι. Covariates, responses, neighbourhood weights and the decision are abstracted away: the nominal formulation is the estimator (the estimator (18) with and unit weights), so the robust prescription plays no role.EReal-valued; convexity of is written out in EReal. The supremum defining is an EReal supremum. It is never empty, because lies in the -ball, so cannot collapse to all of .Measure.pi of , with fixed while .A complete development needs the method of types on a finite alphabet, strict separation in an affine subspace, and the convexity of relative entropy. The method-of-types lower bound is reusable well beyond this mission (hypothesis testing, large deviations of empirical measures). Proofs of any milestone, and alternative proofs of (31), are welcome.