Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
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.
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.
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.
The notebooks Ramanujan kept in India record identities, evaluations, transformations and general principles, usually presented without proofs. They preserve a working mathematician's collection rather than a textbook arranged around a sequence of prerequisite theorems. The Tata Institute of Fundamental Research published an unedited facsimile edition in 1957, making the manuscripts available for systematic study.
Bruce C. Berndt's Ramanujan's Notebooks, published by Springer in five parts in 1985, 1989, 1991, 1994 and 1998, supplies that study. The volumes examine the entries individually, proving them, correcting them where necessary, or explaining why they are false or lack a rigorous interpretation. Their subject matter ranges from magic squares and combinatorial identities to hypergeometric series, continued fractions, elliptic functions, modular equations, class invariants and asymptotic expansions.
This mission takes the results established in Berndt's treatment as formalization targets. The published arguments provide mathematical reference proofs. The remaining task is to express the results precisely and construct proofs checked by Lean.
An entry is a source claim identified by its chapter and local entry label in Berndt's series. The collection is organized around one Lean statement per entry that Berndt establishes. Where an entry contains separately identified parts, corollaries or examples, suffixes distinguish the corresponding statements while preserving their common source location. Intermediate steps of a printed proof do not automatically become additional targets.
The mission covers Chapters 1–39. Part I contains Chapters 1–9; Part II, Chapters 10–15; Part III, Chapters 16–21; Part IV, Chapters 22–31; and Part V, Chapters 32–39. The Part IV appendix on the first notebook and the Quarterly Reports treated in Part I also belong to the mission's scope, with their statements incorporated as they are added.
Declarations use the namespace RamanujanNotebooks and names of the form
entry_<chapter>_<entry>, such as RamanujanNotebooks.entry_16_19. Shared definitions fix the
meaning of recurring objects: q-shifted factorials, theta functions, hypergeometric series,
continued-fraction convergents and the special functions used across chapters. Their domains,
normalizations and indexing conventions are documented so that different entries refer to the
same mathematical objects.
The series has no single capstone theorem. Its goal item is therefore a representative entry: Chapter 16, Entry 19, Jacobi's triple product identity in Ramanujan's notation. This is in Part III, whose chapter develops q-series and theta functions.
For complex parameters , Ramanujan's general theta function is
Both exponents are nonnegative integers. Under , the series converges absolutely, and Entry 19 identifies it with an infinite product. Writing , the target is
Equivalently, with the infinite q-Pochhammer symbol
the identity reads
The Lean statement uses ramanujanTheta and qPochInf, with the hypothesis
‖a * b‖ < 1. Proving this goal establishes the representative identity; completion of the
collection is tracked through its member statements, one per entry.
Every entry is a separate statement of this mission, named RamanujanNotebooks.entry_<chapter>_<entry>
(with suffixes for parts, corollaries and examples): 3,863 statements for Parts I–V, the Part IV appendix
on the first notebook and the Quarterly Reports; the AMS Memoir 477 statements are being added. A chapter's
statements are found by searching for its name prefix. The milestone list has one milestone per chapter,
in source order, titled like “Part III · Ch. 16 — q-series and theta-functions”; each links one
representative result and its description names the chapter's main results.
The mathematical reference is what Berndt proves, with the hypotheses his argument requires. A notebook display alone is insufficient when its domain, convergence conditions or branch choices are unstated. Each target identifies its source and records the conditions under which the asserted equality, limit, transformation or asymptotic relation is established.
Corrected statements carry the explicit phrase “Differs from the printed source”. The accompanying note explains the difference and its origin: a correction supplied by Berndt, a restriction required by the proof, or a reading that resolves an ambiguity. A proposed repair supported only by numerical experiments requires further mathematical review before inclusion as a result established by the reference.
Entries that Berndt shows to be false are not stated as theorem targets. Neither are identities treated only formally, without a rigorous version. For example, Chapter 37's Entry 34 manipulates divergent series, while Entries 35–37 are shown false. Chapter 39 also contains formal claims and entries for which the book supplies no definite interpretation. Such omissions preserve the boundary between a proved result and a suggestive manuscript formula.
Numerical checks are recorded in theorem docstrings, including the tested parameters and the kind of comparison performed. They help detect indexing errors, sign errors and unsuitable domains. Agreement at sampled points is evidence about the transcription; it is not a proof of the universally quantified Lean statement.
The mission brings together source-linked statements of known results whose proofs otherwise remain dispersed across Berndt's commentary. Formal proofs can expose exactly which analytic hypotheses an identity needs and make the shared special-function definitions available for later developments. A proof of the triple product, for example, connects the series definition of the general theta function with its product representation, which recurs throughout the theta-function material.
The statements are proof targets. A declaration that type-checks has a meaningful Lean type; that check alone does not establish the proposition. The description makes no claim that the collection already has machine-checked proofs. Progress is measured by proofs of the individual targets with their stated hypotheses.
The entries vary considerably in their prerequisites. Finite algebraic and combinatorial identities can be approached with relatively little analytic infrastructure. Other chapters depend on convergence theory for continued fractions, transformations of theta and elliptic functions, modular forms, or class invariants.
Even a short equality can require substantial work before its expressions have the intended meaning. A divergent series cannot be interpreted as an ordinary sum, and a complex root or logarithm needs an appropriate branch convention. The central challenge is to preserve the object and domain of the reference result while supplying the formal infrastructure needed to prove it.
Statements use real or complex variables according to the reference, with exceptional values, nonvanishing conditions and convergence ranges explicit. Infinite series are expressed with convergence assertions where necessary; continued fractions are represented through their convergents and limits. Integrals carry the hypotheses needed for their intended interpretation. Lean's total definitions of division, infinite sums and infinite products must not turn an undefined or divergent source expression into a trivial theorem.
Contributions should prove the registered statements using their shared definitions. Reusable lemmas about convergence, special functions and transformations are part of that work. Any suspected statement error should be reported with the declaration name, source location and a specific mathematical objection, so that the source relationship can be reviewed before a replacement is prepared.
A fractional program minimizes a ratio over a set . Nonconvex, nonsmooth ratios arise in the scale-invariant sparse signal recovery model over a polyhedron, in robust Sharpe-ratio optimization in finance, and in the Rayleigh quotient over a sphere; with and the problem reduces to composite optimization . The classical method of Dinkelbach (1967) and its proximal-gradient descendants assume a convex numerator and a concave or smooth denominator, which these models do not satisfy.
Boţ, Dao and Li (arXiv:2003.04124, Math. Oper. Res. 2022) propose the extrapolated proximal subgradient algorithm (e-PSG) for problems in which the numerator is the sum of a smooth convex and a nonsmooth nonconvex term and the denominator is only weakly convex, and they prove that its cluster points satisfy a first-order condition. This mission formalizes that subsequential convergence theorem (Theorem 4.5).
Let with the Euclidean inner product, and let be nonempty, closed and convex. The problem is
Assumption 1. , where is continuously differentiable and convex with an -Lipschitz gradient, is proper and lower semicontinuous, , and on .
Assumption 2. is finite and positive on , continuous on an open set containing , and either weakly convex with modulus on an open convex set containing (that is, is convex there), or regular (Fréchet and limiting subdifferentials coincide) and weakly convex with modulus on .
The limiting subdifferential collects limits of Fréchet subgradients along with . A point is a lifted stationary point of (P) if
where is on and off .
The boundedness condition (BC) asks for on . Algorithm 1 (e-PSG) starts from with parameters , () and extrapolation bounds (in explicit ranges depending on under (BC), and otherwise). At step it sets , picks and , forms , with , , and takes
Finally .
If is bounded and , then every cluster point of satisfies
In the formal statement is in addition Lipschitz around every point of ; see Formalization scope.
with the explicit constants (14), and convergence of . 6. Theorem 4.5(ii): is bounded, , and . 7. The limit inequality at a cluster point (proof of Theorem 4.5(iii), p. 13).
Theorem 4.5 is the subsequential convergence result on which the paper's later results rest: with a Kurdyka–Łojasiewicz property of a merit function it upgrades to convergence of the whole sequence and to linear rates (Theorem 5.5), and under strict differentiability of lifted stationarity becomes ordinary stationarity (Corollary 4.6). The merit function with explicit constants is the template for analyzing extrapolated proximal methods on ratio objectives.
The result is proved on paper; no machine-checked version exists. Formalizing it produces a verified descent analysis of an extrapolated proximal method for a nonconvex ratio, a formal subgradient inequality for weakly convex functions with respect to the limiting subdifferential, and a checked passage to the limit through limiting subdifferentials. It also pins down the hypotheses: the formal statement records a missing assumption of the printed theorem (below).
The ratio is not a sum, so the standard sufficient-decrease argument for proximal gradient methods does not apply directly: the subproblem linearizes through a limiting subgradient scaled by the current ratio , and the descent of comes only after dividing by , which ties the step size to and to bounds on . Extrapolation adds a cross term that the merit function must absorb, which is where the explicit ranges of come from. At a cluster point, is only lower semicontinuous, so convergence of to must be extracted from the optimality of the subproblems, and the limits of must be shown to lie in . The naive approach of passing to the limit in the subproblem's optimality condition fails because has no sum rule in this generality.
is EuclideanSpace ℝ (Fin N). Functions into are EReal-valued; properness is the published IsProperFn, and , are the published IsRegularSubgrad and LimitingSubdiff. The denominator is real-valued on all of : only its values and subgradients near enter, where the paper's is finite. Weak convexity "with modulus " means that is a valid constant, not the smallest one. A run of Algorithm 1 is a predicate on the sequences ; the argmin and are selections, never Classical.choose. . Ratios are real numbers (f x).toReal / g x, meaningful because the iterates stay in . The -range of Step 1 is written as , avoiding division by . is an eventual positive lower bound, which is equivalent since . Cluster points are MapClusterPt.
Correction. Under the second alternative of Assumption 2 alone, Theorem 4.5(iii) fails: for , on and , the iterates converge to , where , so is not lifted stationary. The goal and the limit-inequality milestone therefore assume that is Lipschitz around every point of , which holds automatically under the first alternative.
The trivializing formalizations are ruled out: the parameter ranges are inhabited (checked in Lean, including ), the goal quantifies over every cluster point of every run, and lifted stationarity requires actual limiting subgradients rather than an infDist that would be on an empty set.
Contributions welcome: the subgradient inequality for weakly convex functions, the descent lemma's use in (16), the limit arguments for limiting subdifferentials (the platform has the robustness property (3) as NonconvexSplitting.ProxGrad.limitingSubdiff_robust), and Fermat's rule for constrained minimizers of — the last is reusable well beyond this mission.
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.
A two-stage stochastic program chooses a first action before uncertainty is observed and then takes a recourse action after the observation. Evaluating the expected optimal recourse value can be difficult even when the recourse problem for each fixed observation is a small linear program. This mission isolates the example in Section 3 of Hanasusanto, Kuhn and Wiesemann's preprint: the second-stage program has no first-stage decision at all, yet sufficiently accurate expected values determine how many ways a finite partial order can be arranged into a total order.
The counting connection has a specific history. Brightwell and Winkler (1991) established the complexity of counting linear extensions and related their number to an order-polytope volume. Hanasusanto, Kuhn and Wiesemann use that relation in their October 2015 preprint to establish Theorem 3's strong #P-hardness claim for approximate expected recourse with random recourse coefficients. The mission addresses the exact mathematical relation and the error threshold that support that claim. The complexity-class and encoding parts are outside its Lean statement.
Let be a finite partially ordered set with . A linear extension lists its elements in a total order that respects the partial order. The number of these lists is . The unit cube is . Its order polytope is
Write for the Lebesgue volume of . The paper writes and for this polytope; changing the names of the elements does not change either the count or the volume.
For a realization , define as the optimal objective value of the paper's random-recourse program (10). It maximizes a scalar , subject to , nonnegative variables , and
The sum includes reflexive pairs, for which the summand is zero. The expected recourse value is . Lebesgue measure of is one, so this integral is the expectation under the uniform distribution on the cube. The program is feasible for every : and are allowed. Its objective is bounded by one because . These details give the value a genuine finite meaning at every realization.
The first target is the exact value of the second stage for every :
Consequently, the expected recourse value satisfies the displayed identity in the proof of Theorem 3:
The counting target quoted in the proof of Lemma 3 is
Lemma 3's rounding step concerns an approximation of . If and , then . The mission's main goal uses an approximation of , as in Theorem 3. Under the same strict error threshold,
The target leaves no independent dimension parameter or unspecified oracle value: is the cardinality of the very poset used in program (10), and must approximate that program's expected value. The strict half-unit bound makes the unique nearest integer to .
The theorem shows that an accurate numerical answer to the expected-recourse question contains an exact combinatorial count. This explains why a routine second-stage linear optimization problem can lead to a difficult expectation problem: the expectation records the volume of a polytope whose geometry encodes all linear extensions. The page's threshold specifies precisely how much accuracy is needed to recover the count; a coarser estimate does not support the same rounding conclusion. The original paper also explains why its instance yields strong #P-hardness: the coefficients needed for its random-recourse representation are only , , and in the continuation of Theorem 3's proof.
Formalizing the reduction's mathematical claims produces reusable interfaces for order-polytopes, their volumes, and the expectation of this recourse program. It also poses the factorial volume identity as a theorem rather than treating it as a free assumption. The published Prove2Me definition FCP.Order.LinearExtensions already represents the same linear-extension object and is reused here. The five theorem statements in this proposal are open proof obligations; the existence of the published definition is not a claim that these results already have machine-checked proofs. Proofs of the pointwise value, the expectation identity, the volume identity, and the rounding consequences are welcome.
For a fixed realization, the program's variables have no upper bounds. That feature makes its value jump between zero and one according to whether the order inequalities hold. The pointwise characterization does not by itself settle the expectation: the set where the value changes must be represented measurably, and the integral is over the unit cube with its normalized mass. The factorial relation is a separate geometric statement about the order polytope. Simply counting its defining inequalities gives neither its volume nor the number of linear extensions. These are the substantive steps behind the short rounding calculation.
Lean uses a finite type with a PartialOrder in place of the paper's labeled set . The published FCP.Order.LinearExtensions definition counts order-preserving bijections from this type to the positions . It has exactly the paper's meaning of a compatible permutation. The cube and order polytope are sets of real-valued functions on that finite type. Volume is volume converted to a real number; expected recourse is the Lebesgue integral over the cube. The cube has mass one, including when is empty, and the results include that edge case.
The reusable cube, order polytope, volume, and linear-extension count form a separate definition module. The paper's second-stage program imports that module and defines only its own feasible levels, optimal value, and expected recourse.
The second-stage program is encoded through its feasible objective levels and their real supremum. Since zero is feasible and every feasible level is at most one, the supremum cannot use Lean's default value for an empty or unbounded real set. Classical decidability selects the comparable pairs in the finite sum. Accuracy means an absolute-error inequality with a nonnegative and a strict threshold . These choices preserve both the page's feasibility and its rounding margin.
The main goal is the correctness of the reduction in Theorem 3. It does not formalize #P, strong #P-hardness, pseudo-polynomial running time, unary encodings, or bit lengths. A formulation that assumes or in the goal would erase the result's content; those are separate milestone theorems. Reusable work includes the finite-order volume identity and measure-theoretic handling of the indicator on the cube. The preprint's Section 3 supplies every object and convention used here.
Accelerated first-order methods, such as Nesterov's method and FISTA, reach a convergence rate of on the objective values of a smooth convex function, against for plain gradient descent. Since the work of Su, Boyd and Candès (arXiv:1503.01243), these methods are studied through their continuous-time limits, second-order differential equations with a vanishing viscous damping . The trajectories of these equations, and the iterates of the corresponding algorithms, oscillate strongly around the minimizers.
Adding a Hessian-driven damping term to the dynamic damps these oscillations while keeping the fast rate. The idea goes back to Alvarez, Attouch, Bolte and Redont (2002) and was developed for fast convex minimization by Attouch, Peypouquet and Redont (arXiv:1601.07113, J. Differential Equations 2016). Shi, Du, Jordan and Su (arXiv:1810.08907) showed that the gradient-correction term of Nesterov's method is exactly such a Hessian damping, observed in a high-resolution limit. Because is the time derivative of , the Hessian never has to be evaluated after discretization, and the resulting algorithms are genuinely first-order.
Attouch, Chbani, Fadili and Riahi (arXiv:1907.10536, Math. Program. 2020) study the system (DIN-AVD), , with general time-dependent coefficients, and derive algorithms from it. This mission formalizes their first discrete result: the convergence rate of the implicit (proximal) discretization.
Let be a real Hilbert space with inner product and norm , and let be a convex function of class with gradient , attaining its minimum at some point . Fix , a step size with , and two non-negative sequences (the Hessian damping) and (the time scaling of the gradient).
For and , the proximal point is the minimizer of .
The Inertial Proximal Algorithm with Hessian Damping (IPAHD) generates a sequence by, for ,
It is the implicit time discretization, with step , of (DIN-AVD):
The rate is measured by the sequence
under two growth conditions: and . They are the discrete counterparts of the conditions , of the continuous analysis.
If and hold for every , for some , then every sequence generated by (IPAHD) satisfies: for , and
The rate is stated in terms of , with no constant fixed in advance, so it covers every admissible choice of and at once.
With and one gets , so Theorem 4 gives the accelerated rate for a proximal algorithm with Hessian damping, together with the summability of , a fast decay of the gradients that the plain inertial proximal algorithm does not provide. The time-dependent coefficients let the user trade damping against speed, and Remark 2 of the paper gives under a uniform version of . The proximal scheme only needs of class ; the non-smooth case (Theorem 5) is obtained from it through the Moreau envelope.
The result is proved in the paper. As far as the platform's catalog shows, neither the algorithm nor any Lyapunov analysis of an inertial algorithm with Hessian-driven damping has been machine-checked. A formal proof would certify a discrete energy argument whose printed version contains an index slip (a dropped factor in an intermediate display on p. 12), and the definitions are reused by the other missions of this series.
The proof is a discrete Lyapunov argument, and the difficulty is bookkeeping rather than a single deep step. The coefficient is not chosen in advance: it is forced by the requirement that the terms cancel in , and the inequality for only closes after the signs of , and are used in the right places. The convexity of enters twice, at different points ( and ). Reading the proximal step as the first-order optimality condition and converting it into (8) requires matching with and the coefficient with . A naive direct estimate of from the proximal inequality alone gives only the unaccelerated rate.
The space is {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H], is Mathlib's gradient f, convexity is ConvexOn ℝ Set.univ f and is ContDiff ℝ 1 f. The minimizer is a point with for all , the concrete form of the paper's standing hypothesis . The proximal step is the published predicate GoldenRatioVI.Shared.IsProxPoint: minimizes . No proximal function with a junk value is defined. Sequences are indexed by , the recursion is required for , and , are free. is =O[Filter.atTop] and the series is Summable in .
Hypotheses added relative to the printed theorem, all disclosed in the statements:
At , reads , so reading the conditions "for all " would make every hypothesis set unsatisfiable and the theorem empty. A sorry-free check shows the hypotheses hold for , , , , . The goal statement mentions only , the run and ; it does not refer to , or , and a formalization that assumes an energy inequality would not prove Theorem 4.
The definitions , , the run predicate, , , and live in one definition file. Proofs of the milestones are welcome individually; the identities (milestones 1–2) are algebra plus the first-order condition of the proximal step, and the inequalities (3–6) need the gradient inequality of a differentiable convex function. Theorem 5 (the non-smooth case) is not part of this mission.
Accelerated gradient methods use information from earlier iterates to reduce the objective gap of a smooth convex optimization problem faster than ordinary gradient descent. Their behavior depends on the precise momentum rule. Attouch, Chbani, Fadili, and Riahi study a discrete rule with an additional difference of consecutive gradients, motivated by an inertial differential equation with Hessian driven damping. This mission concerns their inertial gradient algorithm with Hessian damping, called IGAHD, and the rates proved for it in Theorem 6 of the source paper. The result matters when one wants a rate for objective values together with control of the gradients seen during the run.
The paper appeared as a 2020 preprint and subsequently in Mathematical Programming. The mission follows the pinned arXiv version, whose theorem and equation numbers supply all citations here. The proximal and strongly convex algorithms elsewhere in the paper have separate missions; their dynamics and rate statements differ from IGAHD.
Let be a real Hilbert space and let be convex and differentiable. Assume that its gradient is -Lipschitz: for every , where . Choose a minimizer , so . The positive step size satisfies . The momentum parameter is at least , and the damping parameter lies in .
Given , the algorithm takes the following two steps for every integer :
The paper sets and . Its Lyapunov quantity is for . These expressions are fixed by the source formulas (14)–(15), p. 15, not chosen to simplify a later proof.
The central target is the full rate statement of Theorem 6. In the range where the paper's monotonicity argument applies, is eventually nonincreasing. For every IGAHD run,
When , the theorem also gives both weighted gradient summability claims:
The milestone list follows claims the authors state while proving that target. It begins with the extended descent inequality (Lemma 1, (28)), records the identities for and , and then captures the displayed energy and inequalities. Remark 4 asks for the bound on the smallest squared gradient norm among the first iterates; Remark 5 asks for the objective gap at . Those are companion statements and are not substituted for the main theorem.
The rate bounds give three kinds of information about one trajectory. The objective gap controls the values attained at the iterates. The two summable series imply that the gradients at both the extrapolated points and the iterates become small in a weighted aggregate sense when damping is positive. The paper then uses this series estimate to derive the best-iterate estimate of Remark 4 and the extrapolated-value estimate of Remark 5, all on p. 18.
The result is proved in the cited paper; the open work here is its Lean proof and the supporting smooth convex analysis. The development makes the precise discrete algorithm, the Lyapunov quantity, and the descent inequality reusable as mathematical interfaces. A complete formal proof would also make explicit where the author's finite-index monotonicity wording needs correction.
The usual smooth descent estimate alone gives a decrease after one gradient step, but the extrapolated point also carries a momentum term and a gradient difference. Its objective value is therefore not the same quantity as , and a direct comparison of successive objective values does not give the claimed summability. The source uses a stronger descent inequality with a squared difference of gradients. The energy change then contains a quadratic expression in and whose sign depends on and, at first, on how large is. Establishing that sign uniformly over the relevant tail of the run is the central obstruction.
The Lean space is a complete real inner product space. Convexity is ConvexOn ℝ Set.univ f; differentiability is explicit because the phrase “whose gradient is -Lipschitz” presupposes a gradient. The existence of a minimizer is represented by a selected with for every . Positive and positive make meaningful. The algorithm is a predicate on sequences , imposed from so no coefficient is divided by zero. The first two terms are free, and is unused. The statements use the filter at infinity, so finite initial terms do not affect them; summability uses the ordinary series over natural indices.
The printed claim that is nonincreasing from its first term is false for the paper's own definitions. On with , , , , , and , one gets and . The formal goal keeps eventual monotonicity, as supported by the proof on pp. 16–18. This correction is disclosed rather than treated as a new hypothesis. No energy decrease, gradient bound, or conclusion is assumed in the run predicate. The milestone definitions also specify exactly as on p. 17. Contributions to the goal, to the extended descent lemma, or to the explicit energy estimates are all useful; the definition layer and smooth convex lemmas can serve later optimization formalizations.
Accelerated first-order methods for convex minimization, such as Nesterov's method and Polyak's heavy ball method, are now routinely studied through their continuous-time limits: second-order differential equations whose trajectories descend toward a minimizer. In the time-continuous setting the convergence analysis is a Lyapunov argument, and a good Lyapunov function for the ODE usually suggests one for the algorithm obtained by discretizing it.
Attouch, Chbani, Fadili and Riahi (arXiv:1907.10536v2, Math. Program. 2020) study inertial dynamics with Hessian-driven damping: besides the viscous friction term , the equation contains a term , which equals . This damping is known to reduce the oscillations of the heavy ball trajectory, and because it is a time derivative of the gradient, explicit and implicit time discretizations of it produce first-order algorithms with no Hessian evaluation. This mission covers the strongly convex continuous-time result of the paper, Theorem 7 (§4.1, pp. 19–21). For it reduces to the heavy ball equation with friction , whose exponential rate is due to Siegel (arXiv:1903.05671, Theorem 2.2), as the paper's Remark 7 records. For , Remark 7 points to a result on a related but different dynamical system by Wilson, Recht and Jordan (arXiv:1611.02635, Theorem 1), whose rate is slightly worse. The algorithms (IPAHD-SC) and (IGAHD-SC) of §5 of the paper are the discrete counterparts of this theorem.
Let be a real Hilbert space with inner product and norm . Let be a convex function of class , with gradient and Hessian . For , is -strongly convex (Definition 1) if is convex. Such an is assumed to have a minimizer , and .
Fix and a real constant . A solution trajectory of
is a twice differentiable map satisfying the equation at every . This is the dynamic of the paper with the constant viscous damping .
The proof uses two auxiliary functions. The first is the Lyapunov function
The second is . Both appear in the milestones under the names lyap and Zfun.
Assume . Then three statements hold. First, for all ,
Second, there is such that for all
Third,
The milestones are the displayed steps of the paper's proof, in order:
The last sentence of Theorem 7 states that for , . The paper gives no proof of it and attributes it to Siegel. It is a separate item, listed as the last milestone, and is not part of the goal.
Theorem 7 gives exponential decay, at the rate , of the values and of the distance to the minimizer for the whole range of Hessian damping. It also gives an averaged exponential decay of , which the authors describe as new in the literature, and weighted integrability of the squared velocity. These estimates guide the design of the strongly convex algorithms of §5, whose linear rates mirror the continuous rate.
Formalizing it builds machine-checked continuous-time Lyapunov arguments in a Hilbert space: differentiation of energy functions along a trajectory that is only one-sidedly differentiable at , the chain rule through (the Hessian term), and Grönwall-type integration of differential inequalities. To our knowledge none of Theorem 7 has a machine-checked proof; the paper's proof is complete apart from the gap at in part (ii) noted under Difficulty.
The algebra of the first differential inequality is a direct but long expansion, and the quadratic form is where the upper bound on enters. The main analytic steps are elsewhere. First, the energy must be shown differentiable along the trajectory, which requires the derivative of , a chain rule through the Fréchet derivative of the gradient. Second, the differential inequalities must be integrated on with one-sided derivatives at . Third, part (ii) must be derived from the -inequality. The paper's derivation divides by , so it covers only . At part (ii) is still true, but it needs a separate argument, for example local Lipschitz continuity of near together with the convergence from part (i). A proof that only follows the printed text does not cover the case .
ConvexOn ℝ univ and ContDiff ℝ 2, is Mathlib's gradient f, and the Hessian applied to at is fderiv ℝ (gradient f) x v.xstar with for all . is written f xstar.A retailer choosing which products to display faces a physical limit: different products consume different amounts of shelf space. Under a nested logit choice model, the value of an assortment also depends on how customers substitute among products within a nest and on whether they leave without buying. Gallego and Topaloglu study this combination of choice and feasibility constraints in Constrained Assortment Optimization for the Nested Logit Model. Their authors' manuscript of September 11, 2013 is the numbered source for this mission. Its §5 isolates a finite family of candidate assortments for each nest, despite the per-nest space-constrained problem being a knapsack problem. A small family matters because the paper's earlier Theorem 4 can then combine the families across nests while controlling expected revenue.
The paper contrasts this case with cardinality constraints. When every product consumes one unit, the per-nest optimization can be solved exactly by a short list of candidates. General space requirements turn it into a knapsack problem, so the paper gives quantitative approximation factors instead. The factor improves when no single product occupies much of a nest's capacity. These statements and their dependencies occur in §§5.1–5.2, pp. 19–22 of the manuscript.
There is a finite set of nests and a nonempty finite product set in each nest. In nest , product has preference weight , real revenue , and space requirement . The nest's capacity is , and each product fits by itself: . An assortment is feasible when its total space requirement is at most . The empty assortment is feasible and gives zero revenue. The full nested logit model has a no-purchase preference weight and a dissimilarity parameter for each nest; these parameters are relevant to the cross-nest expected revenue, but the local problem of this mission uses only one nest's product data.
For an assortment , write and , with . The paper's parameterized local problem, problem (7), maximizes over feasible assortments for each . Since the within-nest no-purchase weight is zero, equation (8) gives its equivalent sum of product utilities:
Problem (10) is this objective written as a zero-one knapsack: each product decision is zero or one and . Its LP relaxation permits . At parameter , the product's utility-to-space ratio is . Rounding a relaxation solution down retains precisely the products with . The candidate family also contains each singleton assortment .
Theorem 6 asserts that a collection of at most quadratic size includes a two-approximate solution to problem (7) for every . Here an assortment is -approximate at if it is feasible and is at least the objective of every feasible assortment. The statement is pinned to the explicit bound .
The §5.2 target keeps the same collection and adds the finer guarantee whenever each product is small relative to capacity. For every such that for all , and for every , some member of satisfies
The two members need not be the same, but the finite family is fixed before and are chosen. Together the claims yield the paper's factor . The main goal formalizes both parts; Theorem 6 and the paper's intermediate statements are milestones.
The local result converts infinitely many parameter values into a finite search domain. Theorem 4 of the same paper says that if each nest has candidates containing an -approximate local solution for every , then some cross-nest combination obtains at least the optimal expected revenue divided by . Theorem 2 relates the best combination of candidates to a linear program. Thus the finite collection in this mission supplies the local ingredient needed for the paper's global factor two, or the smaller factor under the product-size condition. These consequences are stated in the paragraphs immediately following Theorem 6 and the §5.2 conclusion.
The paper already proves these mathematical results. This mission asks for machine-checked proofs of its specific knapsack relaxation, rounding inequality, and approximation statements. It also creates reusable finite-knapsack definitions and explicit interfaces between the paper's local objective and the published nested logit model. The goal and milestones here remain open Lean statements until solvers provide proofs; compiling a statement with sorry checks its syntax and types, not its mathematical validity.
The parameter ranges over a continuum, yet one family of bounded size must work for all of it. Different values of change the objective coefficients and may change which products belong in an LP optimum. At ties or sign changes, the optimum need not be unique, so a statement about a particular chosen solution requires care. A second difficulty is the fractional LP coordinate: its value can exceed the rounded set's objective, and the refined factor uses a comparison between its utility and the space already occupied. The displayed chain in §5.2 contains quotients that can have zero denominators; the formal milestone states its endpoint inequality directly. A fractional product with zero utility need not force capacity to be filled, which is why the capacity-consumption milestone states positive utility explicitly.
The existing NestedLogitVariants.LP.Model supplies the nested logit instance and its and functions. A general finite continuous-knapsack definition is separate from the paper-specific assortment data. Products use Fin n, nests use a finite type, and assortments use finite sets. The empty finite set represents . The model's within-nest no-purchase weight is fixed to zero, as in the manuscript's main local formulation. Revenues remain arbitrary real numbers; there is no assumption that they are nonnegative or sorted. The capacity and product space requirements are real numbers, with and . Positive preference weights and nonempty are explicit. No condition on or is needed for this local problem (7).
The candidate family is a finite set of rounded LP optima and all singletons. Its size is bounded before and are quantified. Each approximation compares against feasible integer assortments using problem (7), including the empty assortment. The LP optimum itself is never substituted for the integer comparator. General unequal space requirements remain in scope. Contributions that formalize the parametric LP behavior, its one-fractional-coordinate optimum, and the paper's two rounding guarantees fit this mission.
The Frank–Wolfe method, also called the conditional-gradient method, minimizes a smooth convex objective over a compact convex set while asking only for a minimizer of a linear function over that set. In domains where a linear optimization oracle is easier than a projection, this distinction changes which algorithms are practical. Examples in Jaggi's paper include optimization over convex hulls of atomic sets, norm-constrained matrix problems, and domains where iterates can be stored as combinations of a few atoms (Jaggi 2013, §§1–2).
A bound on the unknown difference between the current objective and the optimum does not, by itself, tell an implementation when to stop. The duality gap in this paper can be computed from the same linear optimization problem the method already solves. It provides a certificate tied to the current iterate, so an observed small gap is meaningful even when the optimal objective value is unavailable. The paper's Theorem 2 guarantees that one of the first iterates of four variants has such a certificate, including variants whose linear subproblems are solved only approximately (Jaggi 2013, PDF pp. 2–4).
Let be a compact convex subset of a real vector space and let be a convex, continuously differentiable real-valued function. The optimization problem is , and denotes a minimizer. A Frank–Wolfe step begins at , chooses an atom by approximately minimizing the linear function , and forms a new point from the current point and the chosen atom. In Algorithm 1 the minimization is exact; Algorithm 2 allows an additive oracle error. Algorithm 3 uses a line search along the segment to the atom. Algorithm 4 minimizes over the convex hull of all atoms selected so far, including (Jaggi 2013, Algorithms 1–4).
For , the paper defines the duality gap by
Convexity gives . An exact minimizer of the linear subproblem attains the maximum defining , so its chosen atom gives the certificate directly (Jaggi 2013, equation (2) and §2).
The curvature constant measures the scaled departure of from its linearization along chords of :
The paper uses in both the oracle tolerance and the convergence bounds, where and measures linear-subproblem accuracy. For a linear objective ; for , it is the squared Euclidean diameter of (Jaggi 2013, equation (3) and §3).
The milestone path records the linearization inequality and its primal-error certificate, the identity between the exact linear subproblem and the gap, and the paper's primal convergence Theorem 1:
The mission goal is primal-dual convergence, Theorem 2. If one of Algorithms 1–4 runs for iterations, there is an index for which
Both targets retain the paper's constants and its approximate-oracle tolerance. The mission also states the paper's curvature examples, Lipschitz-gradient comparison, and invariance of curvature under affine reparameterization. These companions clarify what measures; the goal itself is the duality-gap theorem (Jaggi 2013, PDF pp. 3–4).
Theorem 2 converts a rate expressed using an unknown optimum into a guarantee about a quantity available through the algorithm's linear oracle. Combined with the certificate inequality, a small observed gap also bounds the primal error. The same theorem covers an exact oracle, an approximate oracle, line search, and full correction over past atoms, with one numerical constant. That common guarantee is the reason the four update rules belong in one formal target rather than four unrelated asymptotic statements (Jaggi 2013, Theorems 1–2).
The paper proves these statements; this mission asks for machine-checked proofs of their precise Lean versions. The source PDF held here is the nine-page published proceedings paper, which states the results but does not contain its supplementary appendices with proofs. A complete formal development would therefore also be useful as a self-contained account of the gap, curvature, and four algorithms. The definitions of the gap and curvature, and the exact-oracle certificate, can be reused in later convex-optimization developments.
Theorem 1 bounds the objective difference at each iterate, but the bound on asks for a good certificate at some iterate in a finite window. A small primal error alone does not assert that the current linear oracle sees a small gap. The analysis has to connect the gap to progress across steps while accounting for the approximate linear oracle and for updates that differ from the fixed convex-combination step. The fully corrective variant also remembers all prior atoms, whereas the line-search variant chooses its step length from the current segment. These differences are present in the Lean step predicate and cannot be erased by assuming a gap bound on the run (Jaggi 2013, Algorithm 2–4 and Theorem 2).
Lean represents as a set in a real normed vector space and writes the pairing with as the Fréchet derivative applied to a displacement. The paper's footnote names a Hilbert space; the normed-space statement is a disclosed generalization because the results use the inner product only through the derivative pairing. Convexity is required on , rather than on the whole ambient space, while the paper's continuously differentiable hypothesis is retained. Compactness, convexity, feasibility of , and existence of appear explicitly in the convergence statements.
The curvature supremum excludes , where the source formula contains division by zero. Its defining set is required to be bounded above when a convergence theorem treats as a finite real number; compactness and an existing feasible point make the duality-gap supremum meaningful. The selected variant is one of four explicit step rules. Algorithm 3's oracle tolerance uses before line search, and Algorithm 4's atom hull contains . The iterates are zero-based; the goal constrains the source algorithm's steps and selects from . For Algorithm 1, the exact oracle is encoded for all ; recovers the page's stated case.
The construction relies on Mathlib's topology, convexity, continuous derivatives, real suprema, metric diameter, and continuous affine maps. Contributions that prove the milestone certificates, establish the curvature identities, or connect the four concrete step rules to the main finite-iteration bound are in scope. A run hypothesis that directly bounds its gap or primal error would remove the assertion being formalized and is excluded.
A matrix is singular exactly when the pair of linear systems , has a solution with both and nonzero, and this is decided in polynomial time by Gaussian elimination. The natural analogue for a 3-tensor replaces the two linear systems by three families of bilinear equations, one for each way of contracting the tensor against two vectors. For tensors whose dimensions satisfy the Gelfand–Kapranov–Zelevinsky condition, solvability of that system is equivalent to the vanishing of the hyperdeterminant, and for any tensor it is equivalent to being a singular value in the sense of Lim (2005). The same system appears in multiview geometry (Cohen and Tomasi 1997).
C. J. Hillar and L.-H. Lim, Most Tensor Problems Are NP-Hard (J. ACM 60(6), 2013; arXiv:0911.1393), show that, unlike the matrix case, this feasibility question is NP-hard over and over (their Theorem 3.7). The proof is a reduction from graph 3-colorability through the polynomial color encoding of a graph, an idea the authors trace to Bayer's thesis (1982) and to Lovász (1994) and De Loera (1995). This mission formalizes that reduction and its consequence for tensor singular values (Theorem 6.2).
A 3-tensor over a field is an array . Its slices are the matrices , all read off the same array.
Tensor bilinear feasibility (Problem 3.1) asks, for a rational tensor and or , whether the system (9)
has a solution , , with each of the three vectors nonzero. In Lean this is TBF A.
The color encoding of a graph on vertices (Definition 2.9) is the set of quadratics in :
The tensor of the proof of Theorem 3.7 has and slices: slices whose bilinear forms are the minors of the matrix , then slices whose bilinear forms restrict, on , to the polynomials of (Lean: AG G).
The tensor of Lemma 3.6 doubles a real tensor into through the slices , (Lean: doubling A).
An -singular value of (Definition 6.1) admits nonzero with and the two analogous equations; an -singular value has , , on the right. At both reduce to (9).
polynomial-time many-one reductions between languages of binary codes. NP-hardness of tensor bilinear feasibility then follows from the NP-completeness of 3-colorability (Karp 1972), which is cited and not part of the statement.
Theorem 3.7 is the hub of the paper's bilinear results: Section 6 derives from it the NP-hardness of deciding whether is a tensor singular value (Theorem 6.2), and the triple bilinear problem (Theorem 3.8) is handled by the same techniques. It separates tensors from matrices in a precise sense: the matrix analogue of (9) is decided by a determinant, while the tensor version encodes a classical NP-complete problem. It does not settle the hardness of the hyperdeterminant, since the dimensions , of violate the GKZ condition; the paper leaves that as a conjecture.
The result is proved in the paper; none of it is formalized on Prove2Me or, to our knowledge, elsewhere. A complete development produces a machine-checked polynomial-time reduction in Cook's Turing-machine model between two concrete algebraic problems, the color-encoding lemma for 3-colorability (reusable by any reduction that goes through polynomial systems, including Theorems 1.3 and 2.6 of the same paper), and the realification of bilinear systems.
The algebra of the reduction is short; two places need care. First, the bilinear system does not see directly: (9) involves two independent vectors , and the reduction recovers the quadratic system only because the minors force , which requires both vectors to be nonzero. Second, the converse direction must produce a nonzero satisfying the second and third families, a homogeneous linear system of equations in unknowns; this works only when , which fails for the empty graph, so the reduction has to treat separately.
The goal also asks for polynomial-time computability in a Turing-machine model: decoding a graph code, rejecting malformed words, and writing the binary code of (or of its doubling over ). This bookkeeping, not the algebra, is the bulk of a complete proof.
I → J → K → F over finite index types, 0-based: the paper's is A (i-1) (j-1) (k-1). Problem 3.1 requires , , each nonzero, not merely , and the three equation families come from one tensor.I ⊕ I, J ⊕ J, K ⊕ K, with Sum.inr i standing for the paper's index . Lemma 3.6 is stated for this explicit ; a bare existential would be witnessed by any tensor with the right truth value. Only the equivalence of existence is stated, not the paper's "one-to-one" correspondence (which pairs with the conjugate-type vector ).CookPvsNP.PolyReducible), which the paper's proof constructs and which implies the paper's oracle notion of §1.4. "NP-hard" in Theorem 6.2 is rendered the same way, and "( or )" as the claim for each notion. Rational inputs are coded as numerator and denominator in binary; tensors as and then their entries in lexicographic order.The mission reuses the published definitions CookPvsNP_defs (Turing machines, polynomial-time computability, many-one reducibility) and ProjSchedTW.Complexity.Encoding (the binary alphabet and number codes), and Mathlib's SimpleGraph.Colorable. Contributions welcome: the algebraic milestones (Lemma 2.10, the minors, Lemma 3.6) are independent and self-contained; a library of polynomial-time computable list and arithmetic operations on BSym codes would serve both this goal and Theorem 6.2.
Analysts of first-order optimization methods often know how quickly an error bound decreases as the number of iterations grows, but the bound may leave a substantial gap from the method's actual worst case at a fixed iteration count. This matters when comparing concrete methods or step sizes: an asymptotic rate alone does not determine which method has the smaller worst-case error after ten or twenty steps. A performance estimation problem asks for that fixed-count worst case over a specified function class, initial radius, method, and performance criterion. Taylor, Hendrickx, and Glineur show that, for a broad class of fixed-step methods, this question has an exact semidefinite formulation rather than merely a relaxation Taylor, Hendrickx & Glineur, 2016, §§1–3.
Work in Euclidean space with its usual norm and inner product. Fix . The class consists of convex functions for which is convex and any subgradients and satisfy . A subgradient here means that for every . The interpolation milestones also cover , using and Taylor, Hendrickx & Glineur, 2016, Definition 1, p. 5.
A fixed-step method uses coefficients chosen before seeing the function. Starting at , its iterates satisfy for . The coefficients are recorded in a lower triangular matrix . A minimizer and radius constrain the start by . The criterion uses coefficients and a symmetric matrix . Its function values are normalized as , and its Gram matrix comes from the columns . The value to maximize is Taylor, Hendrickx & Glineur, 2016, Definition 4 and §§3.2–3.3, pp. 12–13.
The semidefinite performance estimation program, denoted (sdp-PEP), instead chooses a positive semidefinite matrix and normalized values . For each ordered pair from , it requires , where the star value is zero. It also requires . The matrices and are the explicit coefficient matrices on page 13, computed from , , and Taylor, Hendrickx & Glineur, 2016, §3.3, pp. 13–14.
The main target is Theorem 5. Write for the supremum of the criterion over actual class members, minimizers, and fixed-step runs in , and for the (sdp-PEP) supremum. For every ,
The milestones follow the paper's path: convex interpolation (Theorem 1), curvature subtraction (Theorem 3 and Lemma 1), conjugate interpolation (Lemma 2), the exact pairwise interpolation criterion (Theorem 4), and the page 13 translation between that criterion, actual runs, and SDP feasible points. Theorem 4 states a necessary and sufficient condition for finite triples to be realized by one function in . The final two milestones require both directions of the correspondence between a function instance and a feasible SDP pair. These targets use the paper's fixed constants and its full ordered-pair index set Taylor, Hendrickx & Glineur, 2016, Theorems 1, 3–5 and §3.3, pp. 7–14.
The equality means an SDP optimum is the exact worst-case value for the stated dimension range, for every linear criterion of this form. A feasible SDP point can represent a concrete adverse function and run when its rank fits the dimension; a dual certificate can supply an upper bound. The paper also gives a rank-constrained formulation below dimension , so the dimension threshold has a precise role rather than being a technical ornament Taylor, Hendrickx & Glineur, 2016, Theorem 5 and Proposition 2, pp. 14–15.
The result is already proved in the cited paper. The formalization task is to give its definitions, interpolation claims, matrix constraints, and two-way correspondence machine-checkable statements and eventually proofs. The subgradient predicate, finite interpolation interface, and Gram-matrix representation are reusable beyond this mission. Formalized instances can then support verified worst-case calculations for particular methods and choices of and .
Sampling a smooth convex function at finitely many points gives necessary inequalities, but arbitrary triples satisfying familiar local smoothness or convexity bounds need not come from one common function. Theorem 4 supplies a simultaneous criterion over every ordered pair. The next obstacle is that the function-level problem contains whole functions and iterates, while the SDP retains only normalized values and inner products. Its matrix must encode every iterate relation and interpolation condition, and its rank determines whether those inner products can be realized in . Dropping the rank condition below changes the problem Taylor, Hendrickx & Glineur, 2016, §§2–3.
Lean uses EuclideanSpace ℝ (Fin d) and the ordinary Euclidean inner product. A general subgradient has its defining inequality; FClass records Definition 1, and Interpolable quantifies over a single class member realizing all finite data. The SDP file defines the fixed-step run, the coefficient vectors and matrices, Gram matrices, the criterion, feasibility, and both optimal values. The values lie in EReal, preserving empty or unbounded suprema. The function-level problem explicitly quantifies over a minimizer and actual runs. A gradient appears in a run only in the finite- regime, where the class is differentiable. The theorem requires , , symmetric, , and .
The original Definition 1 allows proper closed functions taking , and Definition 2 allows an arbitrary index set. This mission uses real-valued functions and finite interpolation data. For the finite- result, the paper notes that functions in its class have full domain; its interpolation constructions also yield real-valued functions. The SDP coefficients and do not have values at under the paper's two stated conventions, and Remark 4 confines the later SDP analysis to finite Taylor, Hendrickx & Glineur, 2016, pp. 5, 14. The radius domain is explicit because the SDP constraint squares : a negative radius would admit in the SDP while excluding every actual start.
The goal cannot be met by a junk gradient, a real-valued supremum with a default at an empty or unbounded set, omitting the minimizer, allowing , or discarding the rank requirement at small dimensions. Contributions that establish the interpolation equivalences, the matrix identities, Gram realization, and the two directions of instance correspondence directly advance the goal.
A retailer that decides which products to put on a shelf, or an airline that decides which fare classes to open, faces an assortment problem: the set of products offered changes which product a customer buys, and the firm wants the offer set that maximizes expected revenue. When customers first pick a category (a brand, a store aisle, a flight time) and then a product within it, the standard choice model is the nested logit model of Williams (1977) and McFadden (1978). Real offer sets are constrained: a shelf section displays at most a fixed number of products, and that limit is set per category.
Gallego and Topaloglu (Management Science, 2014) study assortment optimization under the nested logit model when the assortment in each nest must satisfy a cardinality or a space constraint. Their method reduces the joint problem over all nests to a small linear program, provided that each nest admits a short list of candidate assortments that always contains an optimal solution of a one-parameter single-nest subproblem. This mission formalizes the cardinality case, where the paper shows such a list of candidates exists. For a single nest and the multinomial logit model, the cardinality-constrained problem was solved earlier by Rusmevichientong, Shen and Shmoys (Operations Research, 2010).
There are nests and products in every nest. Product of nest has a preference weight and a revenue . An assortment of nest is a subset (the paper writes it as a vector ; the empty assortment is ). The total preference weight and the expected revenue of nest given that the customer chooses it are
with . Under cardinality constraints the feasible assortments of nest are
where is the maximum number of products that can be offered in nest .
For a parameter , the paper's single-nest problem (7) is
By identity (8), its objective equals , so under cardinality constraints (7) is the unit-weight knapsack problem (9)
The utility lines of the products are for , together with .
For every nest there is a collection , fixed before is chosen, with
such that for every some is an optimal solution of problem (7):
The paper states . The goal pins this to , which the paper's count of the intersection points of the utility lines supports, and leaves the exact constant unfixed beyond that.
Combined with the paper's Theorem 4 (candidates containing an optimal solution of (7) for every contain an optimal combination for the full problem) and Theorem 2 (the best combination of candidates is found by a linear program), Theorem 5 shows that the nested logit assortment problem with per-nest cardinality limits is solved exactly by a linear program with variables and constraints. The same parametric argument, in which a one-dimensional parameter sweeps the line and the combinatorial optimum changes only at intersection points of finitely many lines, recurs in the paper's treatment of space constraints and of joint assortment and pricing.
The result is proved in the paper; it has no machine-checked proof. A formal proof also makes explicit two points the paper leaves to the reader: that a solution optimal on an open interval of remains optimal at its endpoints, and how ties between utilities are handled.
The parameter ranges over an uncountable set, and the number of feasible assortments, , is exponential in when grows with . Taking the candidates to be all of satisfies everything except the size bound, and choosing a different collection for each satisfies the size bound trivially. The content is the uniform bound with the collection chosen first. The step that needs care is passing from "the optimum does not change inside an interval between breakpoints" to a statement covering every , including the breakpoints themselves, where ties occur and the greedy choice is not unique.
Fin n (0-based); assortments are Finset (Fin n) and is ∅; is a natural number.NestedLogitVariants.LP.Instance, with V, R from NestedLogitVariants.LP.Model. That model carries a within-nest no-purchase weight vnp i; every statement assumes vnp i = 0, which is this paper's model, so V I i S = ∑ j ∈ S, I.v i j. The paper's extension (p. 15) is not formalized.ConstrNestedLogit.Card.Knapsack defines , the objective of (9), and optimality for (7) and (9) over .The goal cannot be satisfied by an unbounded collection ( is excluded by the bound ), by a collection chosen after (the collection is quantified first), or by a special case of the constraint: is arbitrary, and the optimal member must beat every assortment of , not only the other candidates.
Contributions welcome: proofs of the three milestones and the goal; a general lemma that finitely many affine functions of one real variable keep a fixed weak order and sign pattern between consecutive pairwise intersection points, which is reusable for the paper's §5 and §6 and for other parametric optimization results.
A retailer chooses which products to offer, knowing that what customers buy depends on what is on the shelf. In the nested logit model (Williams 1977) products are grouped into nests, and a customer first picks a nest (or leaves) and then a product inside it. Choosing the offer set to maximize expected revenue is the assortment problem. In practice each nest carries its own limit: at most products (a cardinality constraint) or a shelf of size (a space constraint). Gallego and Topaloglu (2014) show that the problem with cardinality constraints is solvable in polynomial time, and that the problem with space constraints, which is NP-hard, admits approximation guarantees.
The paper's method has two parts. The first (Theorem 2, mission 1 of this series) finds, by a small linear program, the best assortment that can be stitched together from given candidate assortments in each nest. The second, which this mission formalizes, says when such candidates are good enough: it reduces the multi-nest problem to a family of single-nest problems with a linear objective, one for each threshold . The authors call the two results the pivot of their approach; every later section of the paper (cardinality, space, joint pricing, the approximation scheme) invokes Theorem 4.
There are nests and products . Product in nest has preference weight and revenue (no sign is assumed); the no-purchase option has weight ; nest has a dissimilarity parameter . An assortment in nest is a set ; the empty assortment is written . Define
and the expected revenue per customer of the assortment ,
Each nest has a set of feasible assortments, and problem (1) is
with optimal solution . For a threshold , problem (7) of nest is
whose objective equals and so is linear in the assortment. An -approximate solution of (7) at is some with for every . A candidate collection of nest is a set .
Let . If, for every nest , the candidate collection contains an -approximate solution of (7) for every , then there is with each a candidate and
The collection is fixed before ; the conclusion holds for any constraint family, any and any .
Milestones 1–3 are steps of the proof of Lemma 3, in the order the proof uses them; Lemma 3 holds at the single, unknown thresholds , and Theorem 4 is its threshold-free form.
The result. Theorem 4 turns the combinatorial problem (1), whose objective couples all nests through a ratio and through the powers , into a family of single-nest problems with a linear objective, one per threshold. A candidate collection that is good for every threshold is then fed to the linear program of Theorem 2, with variables and constraints. The paper builds an exact collection of candidates per nest under cardinality constraints (Theorem 5), a factor- and a factor- collection under space constraints (§5), an exact collection for joint assortment and pricing (§6), and a polynomial-time approximation scheme (Theorem 9); each of these rests on Theorem 4. The paper also notes (p. 15) that the argument uses only , so it extends to a within-nest no-purchase option of the form ; that extension is not formalized here.
Formalizing it. The result is proved in the paper; it has no machine-checked proof. A formal proof supplies the reduction that the other missions of this series (cardinality, space, pricing, the approximation scheme) need to turn their per-nest statements into guarantees for problem (1). The related criterion of Davis, Gallego and Topaloglu (2014, Theorem 1), already on the platform for the unconstrained problem, is a different route to a factor and does not imply Theorem 4.
The obvious approach compares the approximate and the optimal assortment nest by nest, but the objective is not separable: is a ratio, and each nest enters through , not . Problem (7) has no power , so a solution that is good for (7) is not obviously good for the nest's contribution . The threshold at which the comparison works depends on and , which are unknown, and it is not itself when . A further subtlety is the empty assortment: a nest offering nothing has , where the factor is not finite, so the case split on the sign of and the positivity of have to be handled before any division.
NestedLogitVariants.LP.Model (referenced, not redefined). Every statement sets its within-nest no-purchase weight to zero (I.vnp i = 0), so V is the paper's .Fin n, indexed from . Assortments are Finset (Fin n); is ∅. via , the paper's convention. Powers are Real.rpow, with for .C : ι → Set (Finset (Fin n)), covering cardinality and space constraints alike. Candidate collections are sets A i ⊆ C i; the index set is not named and no finiteness is required.revenue I Sstar for a hypothesised optimum Sstar (IsOptimal1: feasible, and at least the revenue of every feasible assortment), not a defined maximum.Real.rpow with exponent in .Interior-point methods for conic optimization are best understood on symmetric cones: the nonnegative orthant, the second-order cone and the cone of positive semidefinite matrices. On these cones the barrier functions are self-scaled, and Nesterov and Todd showed that every primal-dual pair then has a unique scaling point with and . The resulting primal-dual algorithms, implemented in solvers such as SeDuMi and MOSEK, combine long steps with good worst-case complexity.
Many models in statistics, geometric programming, entropy maximization and logistic regression need the exponential cone, which is not symmetric. Dahl and Andersen (Math. Program. 194, 2022) designed the primal-dual algorithm behind MOSEK's exponential-cone support. To explain why they cannot simply transplant the Nesterov–Todd construction, they use a property that sits between "self-scaled" and "arbitrary": negative curvature of the barrier. Barriers of symmetric cones have it; a barrier is self-scaled if and only if both it and its conjugate have it (Nesterov–Tunçel, 2016); and barriers with negative curvature still admit a unique scaling point satisfying one secant equation. Dahl and Andersen observe in §5 that the exponential-cone barrier lies outside this class, by an explicit witness. This mission formalizes that observation and the derivative formulas of their Appendix A it rests on.
Timeline:
Points of are written . The exponential cone is the closure
whose interior is . Its standard barrier is
defined and smooth on . Appendix A of the paper writes with
For a smooth on an open set, is its Hessian, a symmetric linear map of , and the third directional derivative is the symmetric linear map
A barrier of a cone has negative curvature if for all and for
where is the Loewner order: for every . The direction ranges over the closed cone , including its boundary.
The goal asserts only the qualitative failure, so it does not depend on the particular witness.
The result. Negative curvature is the property that gives symmetric-cone barriers their long-step Hessian estimates and a unique scaling point with one secant equation. Its failure for the exponential-cone barrier means that none of these consequences can be invoked for the exponential cone. An algorithm for this cone has to obtain its scalings by other means; Dahl and Andersen take them from Tunçel's framework, via the quasi-Newton secant updates of §5. The witness also shows that the failure occurs already for a direction on the boundary of the cone, at an interior point with simple coordinates.
Formalizing it. The claim is proved in the paper by a computation "using the expressions in the appendix", with the details left to the reader. The appendix formulas for the gradient, Hessian and third directional derivative of the exponential-cone barrier are the ones an implementation evaluates, including the higher-order corrector term . A machine-checked version certifies these closed forms, including the zero padding of the "leading parts" in (33), and gives a reusable definition of negative curvature that applies to any cone and barrier. As far as is known, none of these statements has a machine-checked proof.
The obstacle is computational, not conceptual. The barrier is a composition of logarithms with a function that is itself a perspective of the logarithm, so its third derivative is a sum of terms with denominators , and . Stating it as a derivative of the Hessian map requires showing that the Hessian is differentiable on the open interior, which in turn requires a description of that interior, a set defined as the interior of a closure. The membership claims about are not definitional either: lies on the boundary, reached only as a limit of points of the generating set, and its non-interiority needs a neighbourhood argument. Finally, the cone condition on matters: replacing by makes the claim nearly trivial, because .
EuclideanSpace ℝ (Fin 3); the paper's are (x 0, x 1, x 2), and vectors are written !₂[·, ·, ·].Real.log; every statement evaluates them, and their derivatives, only at points of , where all logarithms are the genuine ones. The appendix formulas carry the hypothesis .SelfScaledIPM.ShortStep.hess (derivative of the gradient), and is fderiv ℝ (hess F) x u. The Loewner order is stated through the quadratic form for every . Matrices act through the standard basis (Matrix.toEuclideanCLM).Eigenvalues of matrices are computable in polynomial time to any accuracy, and numerical linear algebra rests on that fact. Higher-order tensors appear in statistics (moment and cumulant tensors), signal processing, quantum information and polynomial optimization, and several notions of tensor eigenvalue were proposed for them, independently by Lim and by Qi in 2005 (Lim 2005; Qi 2005). Hillar and Lim (J. ACM 60(6), 2013, Art. 45; arXiv:0911.1393) showed that most of the natural tensor analogues of tractable matrix problems are NP-hard. Their first example, Theorem 1.3, concerns the simplest one: deciding whether a given number is an eigenvalue of a 3-tensor.
This mission formalizes that theorem together with the lemmas its proof uses. The reduction starts from graph 3-colorability, and its intermediate step, quadratic feasibility (Theorem 2.6), is reused throughout the paper: the bilinear, singular value and triple-bilinear results all go through the same color encoding.
A 3-tensor over a field is an array . A scalar is an eigenvalue of (eq. (3) of the paper) if there is a nonzero with
The sum is over the first two indices. For the condition is invariant under scaling of , so no normalization enters.
Problem 1.2 (tensor -eigenvalue) fixes and , and asks, for a rational tensor , whether is an eigenvalue of with an eigenvector in .
Problem 2.2 (quadratic feasibility) asks, for rational matrices , whether the system () has a nonzero solution .
A proper 3-coloring of a simple graph assigns one of three colors to each vertex so that adjacent vertices receive different colors.
The color encoding of a graph on vertices (Definition 2.9) is the family of quadratics in :
Lemma 2.7 replaces a complex quadratic system by a real one of twice the size, and Lemma 2.8 pads a real system to a square one. Applied to , they give real quadratics in unknowns. The tensor with is the output of the reduction.
Graph 3-colorability is polynomial-time many-one reducible to the language of binary codes of rational tensors having as a real eigenvalue.
The result. Theorem 1.3 shows that deciding whether is an eigenvalue of a rational 3-tensor over is NP-hard, in contrast to the matrix case. Because the instance is a single rational tensor with small integer entries, the hardness does not come from numerical precision: it is a property of the exact problem. The same encoding underlies the paper's hardness of approximating an eigenvector (Theorem 1.5) and its remarks on counting eigenvectors (Corollary 1.16).
Formalizing it. The result is proved in the paper, but no part of it is machine-checked. The mission adds three things. It gives a precise language-level statement of what "polynomially reducible" means for this problem. It gives a checked equivalence between 3-colorability and the eigenvalue condition for the explicit tensor . And it gives reusable statements about homogeneous quadratic systems (realification and padding), which the bilinear and singular value missions of this series also need.
The algebraic core is Lemma 2.10, and its reverse direction is where a first attempt fails. The fourth family of does not say that each term vanishes; it says only that their sum over the neighbours of vanishes, over , where nonzero terms can cancel. A common zero yields a coloring only after the first three families have pinned down each coordinate, and the case must be excluded separately.
Lemma 2.7 needs care because the matrices are not assumed symmetric: the imaginary part of is , not . Lemma 2.8 uses that is formally real; it fails over .
At the language level, the reduction must be exhibited as a Turing machine computation on binary codes in polynomial time. That is bookkeeping, but it is the part the paper does not write down.
Fin n → Fin n → Fin n → F, vectors Fin n → F, and indices are 0-based. The eigenvalue condition is eq. (3) verbatim, without normalization; for none is needed. Rational data are cast into or .CookPvsNP.PolyReducible, published definition CookPvsNP_defs). The paper's reduction maps one graph to one tensor, and a many-one reduction implies the oracle notion of its §1.4.BSym with the binary codes of the published definition ProjSchedTW.Complexity.Encoding. A graph is followed by its adjacency matrix. A rational is its numerator then its denominator. A tensor is followed by its entries in lexicographic order. The target language contains all rational tensors, not only integral ones.Contributions are welcome in four places:
CookPvsNP.PolyReducible.A data curator holds a database of individual records and wants to publish something from which many statistics can be computed, while guaranteeing differential privacy: no single record should noticeably change what is published (Dwork, McSherry, Nissim, Smith 2006). Interactive mechanisms answer queries one at a time and add noise to each answer, so their accuracy degrades as more queries are asked; Dinur and Nissim showed that answering too many arbitrary queries accurately reveals the database (Dinur, Nissim 2003).
Blum, Ligett and Roth asked a different question: can a curator release, once and non-interactively, a synthetic database that is accurate simultaneously for every query of a large, structured class, while remaining differentially private? Their answer (arXiv:1109.2229; JACM 60(2), 2013; conference version STOC 2008) is yes for every class of counting queries over a discretized universe, with accuracy governed by the class's VC-dimension rather than its cardinality. The mechanism it introduces, the Net mechanism, became the starting point of the literature on private query release (SmallDB, private multiplicative weights, and the lower bounds that followed).
Fix a finite data universe (for instance ). The curator's input is an -tuple , read as a multiset of records. Two inputs are neighbouring if they differ in exactly one entry.
A database of arbitrary size is a finite nonempty multiset of elements of . For a predicate the counting query is
the fraction of records satisfying . A class of predicates is identified with its class of counting queries, and its VC-dimension is the size of the largest set of points that shatters.
A randomized mechanism , whose output on input is a random database , is -differentially private if for all neighbouring and all sets of outputs. It is -useful for if for every input , with probability at least , for every .
The global sensitivity of is over neighbouring pairs. An -net for is a finite set such that every has some with for all ; denotes a net of minimum size.
The exponential mechanism with quality score over a finite range outputs with probability proportional to . The Net mechanism is the exponential mechanism over with score .
There is an absolute constant such that, for every finite , , , , , , whenever
a minimum -net exists and the Net mechanism run on any minimum -net is -useful for . The constant is left unspecified, as in the paper; the goal asserts the shape of the bound, not a value of .
The result. Theorem 3.10 shows that a database of size roughly suffices to release, privately, a synthetic database answering every query of to within . This is only a polynomial factor above what sampling needs without privacy, and it covers classes with exponentially many queries in , which interactive noise addition cannot. Together with Property 3.3 it is the first general feasibility result for non-interactive private release, and it identified VC-dimension as the governing parameter.
Formalizing it. The result is proved in the paper, modulo the cited uniform-convergence lemma (Lemma 3.8). No part of it is machine-checked on the platform. A complete development would give a formal exponential mechanism with a general score and its privacy proof, a formal utility analysis of a mechanism with a finite range, and a formal ε-approximation theorem for VC classes, which is the deepest dependency and reusable across learning theory.
The privacy and utility of the exponential mechanism (Theorem 3.2, Property 3.4) are short ratio arguments. The difficulty is concentrated in bounding the size of the net. For finite classes a random-sampling and union-bound argument suffices (Lemma 3.7). For infinite classes the union bound over is unavailable, and Lemma 3.8 needs uniform convergence over a class of finite VC-dimension, uniformly over every finite multiset : a symmetrization or chaining argument together with the Sauer–Shelah lemma, none of which is in Mathlib in this form. The obvious route of applying the finite-class bound to the restriction of to the support of gives a size depending on and fails.
Fin n → X with X : Type finite; neighbouring means "replace one entry", the platform's PrivLearn.Generic.Neighbors. The paper's "" read literally for equal-size multisets forces and would make every mechanism private.Database X), with every set measurable. Queries are real functions on multisets, so the same query reads inputs and outputs. Predicates are X → Bool; VC-dimension is the platform's HighDimProb.Chaining.vcDim (valued in ℕ∞; the theorems take it finite, equal to ).Welcome contributions: a general ε-approximation theorem for VC classes (Lemma 3.8), reusable well beyond this mission; a reusable exponential-mechanism privacy proof; the finite-range utility analysis of Property 3.4.
Many estimation problems ask for a vector with few nonzero entries that fits data well. The best-known case is compressed sensing: recover a sparse from noisy linear measurements . Fitting such data under an explicit sparsity budget leads to the sparse least-squares problem
a nonconvex problem that is NP-hard in general. A standard heuristic for it is iterative hard thresholding (IHT): take a gradient step on the least-squares term and keep the entries of largest magnitude. Blumensath and Davies analysed it first under the normalization (Blumensath, Davies 2008) and then with an adaptive step size (Blumensath, Davies 2010).
Beck and Eldar (SIAM J. Optim. 2013, arXiv:1203.4580) place IHT inside a general theory of necessary optimality conditions for minimizing a smooth function under a sparsity constraint. In that theory IHT is a fixed-point method for a condition they call -stationarity, and for least squares with a mild condition on they prove that the iterates converge with a fixed step size tied to the Lipschitz constant of the gradient. That convergence theorem is the goal of this mission.
Fix integers . For let be the number of nonzero entries of , let be its support and the complement, and let
Write for the -th largest of , counted with multiplicity; exactly when .
The problem is
with continuously differentiable and bounded below (Assumption 1). Where stated, is Lipschitz with constant (Assumption 2).
The projection onto is the set of nearest points . Since is not convex this set can have more than one element: . For , a point is -stationary if
A point is a basic feasible (BF) vector if when , and for when .
The IHT method with stepsize produces any sequence with
A matrix is -regular if every of its columns are linearly independent. The least-squares objective is , whose gradient is Lipschitz with .
For with -regular, and any IHT run ,
Theorem 3.1 alone gives only subsequential information, and it says nothing when the iterates have no accumulation point. Theorem 3.2 turns it into convergence of the whole sequence for sparse least squares, with an explicit admissible step size for any . It removes the normalization that the original analysis of IHT required, and it identifies the limit as a point satisfying a necessary optimality condition that is strictly stronger than basic feasibility.
These results are proved on paper. To our knowledge none of them has a machine-checked proof. A completed mission would give a formal convergence theorem for a hard-thresholding algorithm that is used in practice, and a reusable layer for sparsity-constrained optimization: the set-valued projection onto , its coordinate characterization (Lemma 2.2), and the order statistic . The sibling missions of this series (coordinate-wise minima and sparse-simplex methods) use the same objects.
The projection onto is set-valued and discontinuous: a tiny perturbation of can change which entries are kept. So the usual argument for projected gradient methods on convex sets, which passes to the limit in a continuous fixed-point map, does not apply to Theorem 3.1. The limit has to be taken coordinate by coordinate, separately on the support of the accumulation point and off it.
For Theorem 3.2, sufficient decrease and do not by themselves give convergence of a sequence. Two further facts are needed. The iterates must stay bounded, which uses -regularity on every support of size at most . The candidate limits must be isolated, which uses the finiteness of the BF points (Lemma 2.1). Neither holds for a general smooth , which is why the goal is specific to least squares.
Vectors live in EuclideanSpace ℝ (Fin n). Indices are instead of , and is the Euclidean norm. The gradient is Mathlib's gradient f with = gradient f x i, and is assumed ContDiff ℝ 1. The standing hypotheses appear in every statement. Assumption 1 (∃ γ, ∀ x, γ ≤ f x) is a hypothesis wherever is general, also where the proof does not use it, because the paper makes it throughout. It is omitted for . Assumption 2 takes the form of a constant Lf : ℝ≥0 with LipschitzWith Lf (gradient f) together with Lf < L. The statements hold for every such constant, and for this is equivalent to . is the entry at position of the absolute values sorted in nonincreasing order. is Matrix.toEuclideanLin A x. An accumulation point is MapClusterPt xstar atTop x, and convergence is Tendsto x atTop (𝓝 xstar).
is formalized as the full set of minimizers. An IHT run is any sequence of selections from it, and every theorem quantifies over all runs. Formalizing the projection as one chosen top- vector would change and Theorem 3.1, and is ruled out. The theorems assume the strict inequality that the paper's results use, not the algorithm box's input condition . A sanity check confirms that the hypotheses of Theorem 3.1 are jointly satisfiable, so the run predicate is not vacuous.
Theorem numbers and page references are those of the arXiv version (arXiv:1203.4580v1), which differs in typesetting from the SIAM publication.
The objects sit in two definition files: the shared SparseNLO.CWOpt.Setting (, , , , , BF vectors) and SparseNLO.IHT.Setting (the projection, -stationarity, -regularity, , IHT runs). A complete development needs the following:
Proofs of any milestone are welcome, as are reusable lemmas on top- projections and order statistics.
Coordinate descent methods update one block of variables at a time. They are the method of choice when the number of variables is so large that even one full gradient is too expensive, while a single partial derivative is cheap: support vector machines, -regularized regression, and large sparse least-squares problems are the standard examples. Yu. Nesterov's paper Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012), doi:10.1137/100802001) gave the first global efficiency estimates for randomized coordinate descent, and these estimates started a large literature on random coordinate and block methods.
Many applications carry simple constraints on each block: bounds on each variable, a simplex or a ball per block. Section 4 of the paper shows that randomized coordinate descent handles such block-separable constraints at no loss: a projected block step, chosen uniformly at random, enjoys the same expected rate as the unconstrained method, and a linear rate under strong convexity. This mission formalizes that result, Theorem 5.
The space is split into blocks, with and every . A point is the family of its blocks , and is the point whose -th block is and whose other blocks are zero. Each block carries a Euclidean norm with (3.4).
The objective is convex and differentiable, and its gradient is coordinate-wise Lipschitz (2.2): writing for the -th block of the gradient, there are constants with
The weighted norm is (3.5). The function is strongly convex in with constant if for all (3.1).
The problem is (4.1), with and each nonempty, closed and convex. Its optimal value is , attained at an optimal solution . The constrained coordinate update (4.2) is
The uniform coordinate descent method UCDM (4.5) draws uniformly from and sets . Its expected objective is , the expectation over . The level-set radius is the largest -distance between a feasible with and an optimal solution.
For every ,
and, if is strongly convex in with constant ,
The result. Theorem 5 shows that the cost of a constrained problem with separable constraints is, up to the projection onto each , the cost of the unconstrained one: block steps for accuracy , and under strong convexity. The method needs no knowledge of ; the same iteration attains whichever rate applies. The Lyapunov function of (4.7) needs no level-set argument, so it applies wherever the projected step is cheap.
Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any rate for a randomized constrained coordinate method, appears in the Prove2Me catalogue or in Mathlib. The Prove2Me catalogue holds Bubeck's scalar, unconstrained random coordinate descent results (ConvexOptAlg.CoordDescent.*) and the deterministic Tseng–Yun coordinate gradient descent; neither covers a projected block step. A formalization produces the first verified rate for a randomized method with constraints, and a reusable model of block-structured spaces, block projections and expectations over random index sequences.
The unconstrained analysis of the paper (Theorem 1) bounds the distance to the optimum by a level-set radius and uses the decrease of a gradient step. Neither carries over: with constraints the gradient at the optimum need not vanish, so the decrease of a projected step is not controlled by the gradient norm, and the unconstrained recursion is not available. A different potential is needed, and its one-step estimate (4.7) is the central milestone. For the linear rate, the contraction factor must be shown nonnegative without assuming , which is where footnote 2 enters.
is the dependent product Blocks E , each a finite-dimensional real inner product space whose inner product is the paper's . Indices are 0-based. The dual norm is the operator norm of linear functionals, and is the Fréchet derivative of composed with the block inclusion. Random draws are explicit index sequences, so is the finite average of over all sequences of draws; no measure theory is involved.
Explicit choices where the paper is silent:
A formalization in which the update is an arbitrary point of or an unprojected gradient step, the draws are not uniform, or is the unconstrained minimum, proves a different theorem and is ruled out by the definitions above.
Needed infrastructure: existence and the variational characterization of the minimizer of a strongly convex quadratic over a closed convex set (Mathlib has projections onto closed convex sets in Hilbert spaces), the block descent inequality (2.3) obtained from (2.2), and manipulation of the finite expectations over index sequences (conditioning on the last draw). The block model, the weighted norm and the expectation are shared with the other missions of this series. Proofs of the milestones, and of (2.3) as a supporting lemma, are welcome.
Coordinate descent methods update one block of variables at a time. For problems with millions or billions of variables, where even one full gradient is too expensive to compute or store, a step that touches a single block can be orders of magnitude cheaper than a full gradient step. Nesterov's Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012) 341–362, doi:10.1137/100802001) gave the first global complexity bounds for randomized coordinate descent on smooth convex functions: choosing the block at random makes the expected progress per step comparable to that of a full gradient step divided by the number of blocks.
Section 5 of the paper asks whether the multistep acceleration of the full gradient method (Nesterov 1983) carries over to the randomized coordinate setting, and answers it with the accelerated coordinate descent method ACDM. This mission formalizes that answer: Theorem 6, the expected rate of ACDM, together with the lemmas of its proof.
Timeline. Nesterov (1983) introduced the accelerated full-gradient method with rate . Nesterov (CORE DP 2010/2; SIAM J. Optim. 2012) proved the rate of random block coordinate descent and the rate of its accelerated variant ACDM. Later work (Lee and Sidford 2013; Fercoq and Richtárik 2015, arXiv:1312.5799; Allen-Zhu, Qu, Richtárik and Yuan 2016, arXiv:1512.09103) made the accelerated scheme efficient per iteration and sharpened its constants.
The space is , split into blocks. A point has blocks , and is the point whose -th block is and whose other blocks vanish. Each block carries a Euclidean norm with .
The objective is convex and differentiable, and has a coordinate-wise Lipschitz gradient: the partial gradient satisfies with constants . The method weighs blocks by these constants through the norm
The function is strongly convex in this norm with parameter if for all ; is plain convexity. A point minimizes , and .
The optimal coordinate step is , where maximizes . ACDM keeps two sequences with and deterministic scalars , . At step it computes from , sets and , forms , draws a block uniformly at random, and updates
, . The quantity is the expectation over the first draws.
For every , with ,
and, when ,
The result. Theorem 6 shows that randomized coordinate descent can be accelerated: the expected error falls as instead of the of the plain method, so after iterations (about full-gradient equivalents) the error is , the rate of the accelerated full-gradient method. For the same scheme converges linearly with a ratio governed by rather than . This is the starting point of the accelerated randomized coordinate methods (APPROX, NU-ACDM, accelerated proximal coordinate gradient) now used in large-scale machine learning.
Formalizing it. The theorem is proved in the paper; to our knowledge neither it nor any accelerated coordinate method has a machine-checked proof. The Lean development pins down a scheme whose correctness rests on a delicate parameter identity and on several conventions left implicit in the text (the range of , the reading of (5.3) at ).
The plain coordinate descent analysis tracks alone and fails to accelerate: one coordinate step gains only of a full gradient step, and a momentum term built naively from coordinate steps does not keep the expected progress. The accelerated proof needs a potential mixing the function gap with a squared distance , weighted by the deterministic sequences and ; the weights must make the cross terms in and cancel exactly after taking the expectation in the drawn block, which is what the coupled choice of achieves. The second difficulty is quantitative: the growth of follows from coupled recursions for and , not from a closed form.
Blocks E, the dependent product of finite-dimensional real inner-product spaces E i over Fin n (indices ); is absorbed into the inner product of E i. The dual norm is the operator norm of E i →L[ℝ] ℝ.Fin k → Fin n; and are finite averages over all sequences with weight . No measure theory is needed.Blocks, partialGrad, CoordLipschitz, coordStep, wnorm, expect) is shared verbatim with the other missions of this series. The coefficient lemmas (5.2), (5.4), (5.5) and the growth bounds are pure real analysis and welcome as standalone contributions; so is a Lean proof of the block descent inequality (2.3)–(2.4) for Euclidean blocks, which the potential inequality needs.ConvexOptAlg.NesterovSmooth.theorem_3_19). https://arxiv.org/abs/1405.4980Sums of random matrices appear throughout numerical linear algebra, statistics, combinatorics and quantum information: randomized sketching and sparsification, covariance estimation, graph sparsifiers, and the analysis of random features all reduce to controlling the largest eigenvalue of a sum of random self-adjoint matrices. Scalar concentration inequalities (Chernoff, Hoeffding, Bernstein, Azuma) have matrix analogues, and J. A. Tropp's User-Friendly Tail Bounds for Sums of Random Matrices (arXiv:1004.4389v7, Found. Comput. Math. 12 (2012) 389–434, doi:10.1007/s10208-011-9099-z) gives a unified derivation of them with explicit constants.
Many applications do not have independent summands: adaptive algorithms, online learning and sequential estimation produce sums whose terms depend on the past. The scalar tool for such sums is Azuma's inequality for martingales with bounded differences, and its corollary, McDiarmid's bounded differences inequality (McDiarmid 1998). This mission is the fifth of a series formalizing Tropp's paper; it targets §7, the matrix Azuma inequality.
Timeline. Ahlswede and Winter (2002) introduced a matrix analogue of the Laplace transform bound for independent sums; Oliveira (2010) gave the variant used in this paper. Tropp (this paper, 2010–2012) proved the matrix Azuma and McDiarmid inequalities below. More refined matrix martingale inequalities appear in Oliveira (2010) and in Tropp's Freedman's inequality for matrix martingales (2011), which the paper cites (p. 27) as requiring additional machinery.
All matrices are with complex entries, . A matrix is self-adjoint (s.a.) when it is Hermitian. For s.a. , is its largest eigenvalue and its spectral norm. Functions of s.a. matrices are defined spectrally: if then , and is defined the same way on positive-definite matrices. is the semidefinite order: is positive semidefinite.
Let be a probability space with a filtration , and write . The expectation and the conditional expectation of a random matrix are taken entrywise. A sequence of random matrices is adapted when each is -measurable. A matrix martingale is an adapted sequence of s.a. matrices with and ; its difference sequence satisfies .
The hypotheses of the main theorem are: is an adapted sequence of random s.a. matrices, and is a fixed (non-random) sequence of s.a. matrices, with
The variance parameter is .
For all ,
In the order they are used:
Corollary 7.2 is the martingale form, . Corollary 7.5 (Matrix Bounded Differences) is the matrix McDiarmid inequality, for a matrix-valued function of independent variables whose changes in one coordinate have squares bounded by .
The result. The bound has the scalar subgaussian shape with two matrix features: a dimensional factor , and a variance parameter equal to the norm of the sum rather than the sum of the norms . In the commuting case the two coincide; in general the first can be smaller by a factor of up to . The theorem needs no independence, so it covers adapted constructions such as Doob martingales. Corollary 7.5, obtained from it, is the standard matrix tool for concentration of matrix-valued functions of independent data. With independent summands the theorem gives a matrix Hoeffding inequality (Theorem 1.3 of the paper).
Formalizing it. The result is proved in the paper; none of it is formalized. Mathlib has the continuous functional calculus, conditional expectation and filtrations, but no Golden–Thompson inequality, no Lieb concavity theorem, and no matrix tail inequality. A formalization produces a machine-checked matrix Azuma inequality, the Golden–Thompson inequality, and a symmetrization lemma for the trace exponential, all of which have uses beyond this paper.
The scalar proof of Azuma's inequality multiplies conditional moment generating functions, , and bounds each factor. For matrices this fails: unless and commute, and is false, so the Golden–Thompson inequality cannot be iterated over terms. The paper itself notes (p. 28) that the classical approach does not seem to extend. A second obstacle is that the hypothesis bounds squares, not the matrices themselves; it does not give , so the scalar Hoeffding lemma for bounded centred variables has no direct matrix analogue. The infrastructure is also heavy: Lieb's concavity theorem underlies Corollary 3.3, and operator monotonicity of the logarithm is needed.
Matrices are Matrix (Fin d) (Fin d) ℂ, self-adjointness is IsHermitian, and is Mathlib's order under MatrixOrder. Matrix exponential and logarithm are cfc Real.exp and cfc Real.log. is the supremum of the real spectrum, which is why is assumed (NeZero d). Expectation and conditional expectation of matrices are entrywise Bochner integrals; adaptedness is entrywise strong measurability with respect to a Mathlib Filtration ℕ. The summands are indexed by , so is never truncated. The bound is required almost surely. The bounds are deterministic matrices. The infimum over in Proposition 3.1 is posed as the bound for each at which the expectation is finite.
The hypotheses must not be made vacuous. Integrability of each is assumed explicitly, because for a non-integrable variable Lean's conditional expectation is and the centring hypothesis would say nothing. The are not assumed independent: an independence hypothesis would turn the goal into the weaker matrix Hoeffding inequality.
Two readings are recorded in the statements. In Lemma 7.7 the conditional expectation given is replaced by the expectation over at each fixed value with ; by independence these agree. Corollary 7.2 adds the hypothesis that is almost surely constant, without which .
A complete development needs: Golden–Thompson; Lieb's concavity theorem (or Corollary 3.3 directly); operator monotonicity of the matrix logarithm; monotonicity of the trace exponential; conditional expectation of matrix-valued variables and its interaction with the semidefinite order. All of these are reusable well beyond this mission, and contributions of any of them are welcome. Proposition 3.1, Corollary 3.3 and Lemma 4.3 are also milestones of other missions in this series.
City logistics often moves goods in two stages: large trucks bring freight from a central depot to a few intermediate satellites, and small vehicles distribute it from the satellites to the customers. The two-echelon capacitated vehicle routing problem (2E-CVRP) is the basic optimization model of such systems; it contains the capacitated location-routing problem as a special case. Baldacci, Mingozzi, Roberti and Wolfler Calvo (Oper. Res. 61(2), 2013) gave an exact method that solved benchmark instances out of reach for earlier algorithms.
Their method does not attack the whole problem at once. It enumerates configurations, sets of first-level (depot–satellite) routes, discards most of them with cheap tests, and solves a second-level problem only for the survivors. The correctness of the method rests on two facts stated in §5 of the paper: the problem decomposes exactly over configurations (Eq. (26)), and the pruning tests of Propositions 1 and 2 never discard the configuration of a solution better than the incumbent. This mission formalizes those facts.
An instance has a depot , satellites and customers , a symmetric cost on the edges (with the fixed vehicle costs folded in), positive integer demands with total , first-level vehicles of capacity , second-level vehicles of capacity at satellite with a global limit , satellite capacities and handling costs .
A first-level route leaves the depot, visits a set of satellites and returns; its cost is the length of the closed walk. A second-level route leaves satellite , visits a set of customers of total demand and returns; its cost is the walk length plus . Formulation chooses binary , and integer deliveries minimizing subject to: each customer on exactly one used second-level route; at most used routes at and in total; load at at most ; at most first-level routes; the deliveries to equal the load leaving ; each used first-level route carries at most . Its optimal value is , when infeasible.
The set of configurations is
For , , and . Problem is with the first-level routes fixed to : second-level routes only at satellites of , real deliveries for , and . Its value is when infeasible.
The bounds of §5.1 use multipliers , , and marginal costs satisfying the penalty system (12), for every route of satellite :
Let be a real number and a feasible solution of of cost less than , with configuration . Then and
Eq. (26) is what makes the method exact: once every configuration that can carry a solution better than the incumbent is examined, the best is the optimum. Propositions 1 and 2 are what make it fast: they remove configurations from before any second-level problem is solved. If a pruning test discarded the configuration of a cheaper solution, the method would return a suboptimal value and still report it as optimal; the formal statements rule this out for every instance, not just the benchmark ones. The capacity constraints (33) play the same role inside : a cut that removed a feasible solution would make the bound invalid.
The paper's proofs are in an electronic companion; none of these statements has been machine-checked before, and none is on the platform. The formalization also records exactly what the tests need: positive demands, integral vehicle counts, and the sign conditions on the multipliers, and nothing about the optimality of the incumbent.
Most statements are elementary counting and Lagrangean weak-duality arguments over finite index sets. The work lies in the bookkeeping between two formulations with different index sets: sums over all satellites, only over , and a solution of one must be turned into a solution of the other. One step is not elementary: has integer deliveries and real ones, so the inequality in (26) needs an integral delivery plan from a fractional one. That is an integrality property of a bipartite transportation problem (routes to satellites, integral capacities and demands), which no counting argument gives.
Satellites and customers are Fin ns and Fin nc, 0-based. The route families and are arbitrary finite families of elementary routes with costs computed along the closed walk; the paper uses all such routes, so every statement here is a generalization. Demands are positive integers; the triangle inequality is not assumed. Binary variables are Bool; optimal values are infima in EReal, with ⊤ for an infeasible problem. A configuration is a Finset of route indices. The penalties are any , , and satisfying (12), not only those producing the paper's bound LD1. Ceilings of and are natural-number ceilings of rationals; those in Proposition 2 are integer ceilings of reals.
The goal departs from the printed proposition in three disclosed ways. Only necessity is stated: the "if" direction is false, because (b)–(e) ignore the satellite capacities . Condition (a), , is omitted: it holds for some optimal solution, not every one (its split-delivery analogue is posed, and open, on the platform as SplitDeliveryVRPTW.Known.exists_optimal_split_customers; it is not reused here). "An optimal solution" becomes "a feasible solution of cost below ", the property the paper's own justification uses. Proposition 2 is stated with as a hypothesis; the paper's computation of by problem (27)–(32) is not formalized, because (32) forces positive deliveries that does not require. The goal is not trivialized by an infeasible hypothesis: feasible solutions of exist on small instances, and a toy instance was checked in Lean.
A complete development needs finite-sum manipulations, Lagrangean weak duality for (12), and, for (26), integrality of bipartite transportation polytopes, which is reusable well beyond this mission. Proofs of any milestone, and a general transportation-integrality lemma, are welcome.