Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Many polynomial optimization problems are invariant under permuting the variables: the objective and the constraints are symmetric polynomials. Lasserre's moment–sum-of-squares hierarchy solves such problems by a sequence of semidefinite programs whose size grows quickly with the number of variables and the degree, and symmetry is the main tool for shrinking them. Riener, Theobald, Jansson Andrén and Lasserre (arXiv:1103.0486, Math. Oper. Res. 38(1), 2013, doi:10.1287/moor.1120.0558) develop symmetry reductions of the hierarchy and, in their Section 6, a second route: instead of reducing the moment matrices, describe the orbit space of the symmetry group directly by polynomial inequalities, following Procesi and Schwarz, and optimize over it.
For the symmetric group the orbit space is described by a single Hankel matrix of power sums. This mission formalizes the lower bound that results for a basic family of symmetric problems: minimize one power sum subject to prescribed values of the lower power sums.
Fix and a point . The power sum of order is ; note .
The problem (6.4). Given with , , and prescribed reals , minimize over all with for . Its optimal value is written .
The Hankel matrix. For a real sequence and , .
The matrix (6.1). For a finite group acting on with fundamental invariants , the matrix has -invariant entries . For the symmetric group with , is the Hankel matrix of power sums.
The SDP (6.5). For and ,
The variable is the sequence ; the constraint is a single linear matrix inequality of size .
For and :
(a)
(b) If , put , and . If , then
The goal is the conjunction of (a) and (b).
Part (a) bounds a nonconvex polynomial problem of degree in variables by a semidefinite program with one matrix variable, whose size does not depend on . Part (b) evaluates the bound in closed form in the even case , where the SDP reduces to a single scalar constraint on the free moment . Together with the upper bound of Theorem 6.7 (a separate mission of this series), it brackets the optimal value of power-sum problems, which appear in moment problems, in the analysis of symmetric inequalities, and as test cases for symmetry-adapted relaxations.
The paper's proof is a few lines, citing the Procesi–Schwarz theorem and Schur's complement. A formal development makes each step explicit: the positive semidefiniteness of the Hankel matrix of power sums of a real point, the principal-submatrix argument, and the Schur complement for a Hankel block. It also fixes a misprint: the bound of (b) is printed as without the inverse, which is false (for , , the minimum is but the printed bound is ). No machine-checked version of this result is known to exist.
The individual steps are classical, and the difficulty is in the bookkeeping. The paper reaches (a) through the Procesi–Schwarz description of the orbit space, a deep result stated for general finite groups; the formal route needs only the positive semidefiniteness of the Hankel matrix of power sums of every real point, which the page leaves implicit. The identity requires computing partial derivatives of power sums with the right index shifts. In (b), must be identified with a block matrix whose top-left block is with , which needs the prescribed values and a reindexing of as . The extended-real values must be handled: the problem can be infeasible (value ), and for odd unbounded below.
Lean namespace SymPolyOpt.PowerSumLB. Conventions:
x : Fin n → ℝ; is powerSum x j, so powerSum x 0 = n.γ : ℕ → ℝ of which only are read. The page's "" in (6.4) is read as .EReal: for an infeasible problem, possibly . They are compared only by ≤.s : ℕ → ℝ; its entries past are unconstrained and irrelevant since .MvPolynomial.psum and pderiv.Disclosed changes relative to the page:
Trivializing formalizations are ruled out: real-valued infima (which return on empty or unbounded sets) are not used; is an SDP over arbitrary sequences, not over power-sum vectors of points, so (a) is not definitional; the constraint is kept; Lean's junk inverse of a singular matrix is excluded by the positive-definiteness hypothesis; and the printed false bound is not stated.
Needed infrastructure: Mathlib's Matrix.PosSemidef, Matrix.PosDef, PosSemidef.submatrix and the Schur-complement lemmas for block matrices (fromBlocks). A reusable lemma that Hankel matrices of power sums (and, more generally, of moments of a finitely supported measure) are positive semidefinite would serve other moment-problem missions. Contributions to any milestone are welcome.
Linear-quadratic (LQ) control is the setting in which stochastic optimal control has a closed-form answer: the optimal control is a linear feedback of the state, and the feedback gain comes from a Riccati differential equation. In the mean-field version, the expectation of the state and of the control appear in the dynamics and in the cost. Mean-field SDEs go back to Kac (1956) and McKean (1966) as models of interacting particle systems. A cost containing can penalize the variance of the state, which is what is wanted when the optimal state should not be too sensitive to the noise (mean–variance portfolio selection is the standard example). With such a cost the problem is no longer a classical LQ problem: the weights on may be negative definite, and the cost is not an expectation of a function of the state path, so the classical Riccati theory does not apply as it stands.
J. Yong (SIAM J. Control Optim. 51(4), 2013, pp. 2809–2838) solved the problem with deterministic coefficients. He derives the optimality system, a linear mean-field forward–backward SDE, and decouples it with two Riccati equations. One governs the deviation , the other the mean . The optimal control is then an explicit state feedback.
Timeline:
Let be a complete probability space carrying a one-dimensional standard Brownian motion , and let be the natural filtration of augmented by the -null sets. Fix a horizon . An admissible control is an -progressively measurable with ; the set of them is . For the state solves
with deterministic matrix-valued coefficients. The cost is
Problem (MF-LQ): minimize over . The assumptions are:
The weights themselves need not be semidefinite.
With and , the two Riccati equations are
with . Write and .
Under (H1)–(H2), (4.8) and (4.9) have unique solutions and on . The closed-loop system obtained by substituting
into the state equation has a unique solution . With and the explicit , the 4-tuple solves the optimality system, and is optimal. Moreover
The Woodbury identity used on p. 2826 is already proved on the platform (FamousTheorems.woodbury_identity) and is referenced.
The result. Theorem 4.1 reduces a mean-field stochastic control problem, whose state law enters the dynamics, to two matrix ODEs. The optimal control is computable offline: integrate and backward, then feed back the state and its mean. The value is explicit, so cost comparisons between the mean-field problem and its classical counterpart become comparisons between Riccati solutions; §5 of the paper does exactly this for variance-penalized costs. When all barred coefficients vanish, and the classical stochastic LQ feedback is recovered.
Formalizing it. The result is proved, not open; this mission formalizes the known proof. No continuous-time stochastic LQ theorem exists on the platform. The mission builds on the published stochastic calculus of Peng1990.SMP.Stochastic (Itô integrals, SDE and BSDE solutions, ) and adds a reusable mean-field LQ setting, matrix Riccati equations in integral form, and a verification theorem. None of the statements has a machine-checked proof yet.
The Riccati equations are nonlinear matrix ODEs with only coefficients. Local existence is routine, but global existence on needs an a priori bound, which a local fixed-point argument does not give. The bound comes from the control interpretation of the equation, and it requires semidefiniteness of . The second equation contains , and its quadratic term is only controlled when , which in turn needs . Its "state weight" is semidefinite only through the identity of milestone 7, even though itself may be negative definite. On the stochastic side, the verification step (milestone 9) and the duality arguments of Theorems 3.1–3.2 apply Itô's product rule to and to for processes driven by the same Brownian motion, with an absolutely continuous (not differentiable) . Itô's formula is not yet available on the platform: it is the open goal EthierKurtz.ito_formula. Existence in Proposition 2.8 needs a minimizer of a coercive continuous quadratic functional on the Hilbert space .
States are Fin n → ℝ, controls Fin m → ℝ, time is ℝ≥0, and the horizon satisfies . The probability space is complete. is Peng1990.SMP.IsStdBrownian with one coordinate, and is ReflectedBSDE.Existence.augmentedFiltration. is the Bochner integral of the solution itself. Every mean-field term is a closure over the process being solved for, never a free deterministic input. Solutions of the forward and backward equations are the published SolvesSDE/SolvesBSDE notions: progressive, square-integrable, with the integral identity at each almost surely. Controls and -components are identified up to -null sets.
Other conventions:
Matrix.inv is a true inverse. For (4.9), follows from (H2) once .A formalization in which the mean is an independent input, or in which a Riccati "solution" may use the junk value of a singular inverse, would trivialize the problem. Both are ruled out by the definitions above. A sorry-free sanity file shows that (H1)–(H2) hold for data with negative definite, and that the Riccati class is non-empty.
Contributions are welcome on all of the following:
An online learner repeatedly chooses a point, observes a loss, and is judged by the difference between its accumulated loss and that of a fixed competitor. In practice, an available learner may operate on a broad feasible set , while the application permits decisions only in a smaller set . Replacing each output by a feasible point changes the learner's losses, so its existing regret guarantee no longer directly applies. Chapter 12 of Orabona's text develops reductions that use the learner as a black box: they change the feedback sent to it and recover a guarantee for the constrained predictions.
The chapter treats Euclidean and other norms, Bregman projections, sleeping experts, and the separation of magnitude from direction. This mission focuses on its first general construction, Theorem 12.5. It is useful when the internal update of the learner is unavailable or when a solver wants to reuse one unconstrained algorithm across several constraint sets. The theorem gives four explicit surrogate losses and an explicit bound on their subgradient norms. Orabona, Chapter 12 also explains how its distance based construction relates to regret matching on the simplex.
Work in a finite-dimensional real vector space with an arbitrary norm . Its continuous dual consists of real-valued linear functionals; is the pairing and is the dual norm. Let , with nonempty, closed, and convex. The distance to and the generalized projection are
The minimum exists under these assumptions. A projection need not be unique for an arbitrary norm; the construction accepts any . In round , an underlying learner outputs , the reduction predicts , and the environment reveals a real-valued loss . Choose a subgradient of at that satisfies the subgradient inequality for competitors in . Choose any full-space subgradient . For a fixed , the constrained regret is
The surrogate losses are functions passed back to the learner. Their four formulas are the distance-penalized linear loss, its linear form using , a distance penalty activated only when , and that activated penalty's linear form. Each is defined on the ambient space, then used on . The projection rule and the selected subgradients are the only information the reduction needs from a run.
For each of the four choices in Theorem 12.5 and every , the goal is
The theorem is pathwise: it applies to any sequence of predictions that the underlying learner could produce. No particular learner or regret rate is built into the target. Equation (12.2) isolates the linearized regret term that each surrogate must cover. The four clauses of Lemma 12.2 establish convexity, the exact Lipschitz constant, the zero subgradient on , and the subdifferential characterization outside .
The companion clause of Theorem 12.5 says that every full-space subgradient of a surrogate at a point of satisfies
The factor is part of the printed result. It applies to all four choices, including the branches at which the activation term vanishes.
The result transfers a regret guarantee from an algorithm working on to feasible decisions in through a loss transformation. The norm bound makes this transfer quantitative for algorithms whose guarantees depend on subgradient magnitudes: the new losses have controlled scale. Lemma 12.2 is reusable apart from online learning, because it describes distance and subgradients for a closed convex set in any finite-dimensional normed geometry.
Orabona presents these as established mathematical results in Theorem 12.5 and Lemma 12.2. The work here is to give them auditable Lean statements and, subsequently, machine-checked proofs. The chapter's Bregman projection, sleeping-experts, and magnitude/direction reductions are separate results; this proposal leaves them for later missions or additions. A proof of the present goal would make the first black-box reduction reusable without depending on a specific unconstrained learner's implementation.
Simply projecting into leaves an extra term in the linearized regret: the old learner was evaluated at while the actual loss was incurred at . An arbitrary correction to the feedback can cover that term while destroying convexity or greatly enlarging gradients. The four formulas balance both requirements, and the two activated formulas must also handle the boundary case , where a normalized direction would otherwise divide by zero. Generalized projections create another issue: an argument cannot silently assume one canonical nearest point when the norm is not Euclidean.
Lean uses a finite-dimensional real normed space and represents dual vectors as continuous linear functionals. Their operator norm is the book's dual norm. The distance is Metric.infDist; nonemptiness keeps its value meaningful, and closedness plus finite dimensionality supplies an attained minimum. Projection is a relation, so all valid choices are covered. Sequences start at index ; index is unused, and the horizon is explicitly at least one. The original losses are real-valued on the ambient space, with the subgradient inequality required only for comparators in . The distance and surrogate subgradients use the full-space inequality. This matters when has empty interior: a relative subgradient on can have an arbitrary normal component and would make the printed norm bound false.
The underlying algorithm is abstracted by its sequence ; its surrogate regret is exactly the sum on the right of the goal. is allowed to be strictly larger than , so the statement retains the constraint-reduction content. The normalized direction in the third and fourth surrogates appears only in the branch with , which implies . Contributions toward the distance-function lemmas, the surrogate inequalities, and the gradient bound all support the goal. The same geometric definitions can also support later reductions based on other projections.
In online learning, a learner chooses a point before seeing each round's loss. Ordinary regret compares the learner with one fixed point chosen after all rounds. That comparison can be too coarse when a useful action changes over time. A portfolio allocation, a prediction rule, or an operating point may need to move after the environment shifts. Dynamic regret compares the learner with a specified sequence of feasible points, one for each round. The sequence is allowed to move, but its movement appears explicitly in the bound. Chapter 14 of Orabona's Online Learning: A Modern Introduction Using Convex Optimization develops this comparison, then studies strongly adaptive and tracking regret. This mission isolates its first capstone, Theorem 14.2.
The result extends the book's earlier analysis of online mirror descent to changing comparators. As the chapter explains, a moving comparator can achieve a smaller cumulative loss than any single fixed point, so a dynamic bound answers a stricter performance question. The bound also makes its own limit clear: frequent or large comparator changes cost more. The chapter relates this framework to earlier work on drift in online learning; the formal target here is the precise statement in the pinned arXiv version, with its explicit constants and final Bregman term. Source, Chapter 14, pp. 227–229.
Let be a finite-dimensional real normed space, , and a nonempty closed convex feasible set. On round , the learner plays , receives a real-valued loss , and selects a subgradient at . A comparison sequence consists of arbitrary points in . The dynamic regret is
The path length of the comparison sequence is the total distance between successive points:
It is zero for a constant sequence. The path starts at round two, so neither nor an artificial first movement enters the claim. The norm on is arbitrary. Its dual norm on continuous linear functionals is written .
Online mirror descent uses a differentiable regularizer and its Bregman divergence
At each round, the next point minimizes over , with one constant step size . The regularizer is closed and -strongly convex, with , on the stated domain. Its derivative must be evaluated at interior points of . For a horizon , the theorem measures the range of the gradients seen along the run by the finite maximum
The maximum includes , at which the difference is zero, and stops at . These conventions are the ones in Definition 14.1 and Theorem 14.2.
The first milestone is the inequality part of Lemma 6.10. For each feasible comparator, one OMD update controls the loss difference by a decrease in Bregman divergence plus a quadratic dual-norm term. The milestone records the book's whole inequality chain, including the intermediate term that exposes the change in the iterate. It is the local estimate used at every round of Theorem 14.2. Lemma 6.10, p. 67.
The second milestone is the display in the proof of Theorem 14.2 immediately before the final choice . It keeps that additional comparator free and shows the gradient-difference sum explicitly. This intermediate statement is useful for inspecting the sign and time index of each comparator shift. Proof of Theorem 14.2, pp. 228–229.
The goal is the full bound of Theorem 14.2:
It applies to every feasible comparator sequence, including a constant one. The negative terminal divergence is part of the target. Retaining it makes the statement match the source and preserves information for later use. Theorem 14.2, p. 228.
The theorem quantifies how much a comparator may move before its performance becomes hard to match. The cost of movement is linear in the path length and scaled by the regularizer-gradient range . With a bounded dual norm for the observed subgradients and a suitable constant step size, the chapter derives a square-root dependence on the horizon for slowly moving sequences. A static comparator has path length zero and recovers the familiar mirror-descent setting. The bound also applies to arbitrary norms and regularizers, so it is not limited to Euclidean projection. Discussion after Theorem 14.2, p. 229.
The mathematical result is proved in the book. The remaining task is to give its exact assumptions, update rule, intermediate inequality, and final inequality machine-checked proofs. The already published Bregman definition supplies a reusable representation of ; the new run, path-length, and gradient-maximum definitions supply the chapter's missing interface. Those definitions can support later formalizations of tracking regret and other moving-comparator results. No proof of the present chapter result is claimed by these draft statements.
For a fixed comparator, the Bregman terms from successive rounds line up directly. With changing, they do not: each transition changes the first argument of . The resulting correction depends on differences of regularizer gradients, and its time index must agree with the path-length sum. A simple replacement of the static comparator by in a static regret theorem therefore leaves an unaccounted term. The terminal point is also essential to the full telescoping statement. The mission asks for the book's exact constant and terminal term rather than only an asymptotic rate.
The Lean model uses a finite-dimensional real normed space. Losses and the regularizer are real-valued on their evaluated domains; the feasible-set and domain predicates represent the book's extended-real convention outside those domains. Closedness of the regularizer is represented by a closed epigraph over . Subgradients are continuous linear functionals, so their operator norm is the dual norm. The run predicate represents every admissible subgradient and argmin choice for Algorithm 6.1; it also carries the required membership of in . The run is a predicate on sequences, not a selected canonical sequence.
The book's round labels start at one. Index zero is unused. The horizon is at least one, and are positive. These conditions keep the finite maximum nonempty and every denominator meaningful. The subgradient condition is relative to , which is sufficient for the theorem's comparisons and slightly weaker than the book's full-space subgradient convention. This choice is disclosed in the item statements. The comparator sequence is universally quantified through its feasibility condition; it is never restricted to a constant sequence or assumed to satisfy the conclusion. The definitions and theorem statements invite proofs of the one-step inequality, the summed estimate, and the final bound, as well as reusable results about Bregman divergence on arbitrary normed spaces.
Many operational decisions are linear programs whose cost vector is uncertain but predictable from side information: routing with travel times that depend on weather and time of day, procurement with prices that depend on market signals, assignment with costs that depend on observed features. Contextual linear optimization (CLO) formalizes this: observe features , choose a decision in a polytope , pay for an unobserved random cost vector .
Two families of data-driven methods compete. Estimate-then-optimize (ETO) fits a regression and then solves the linear program with the estimated costs. Integrated methods (for example the SPO+ approach of Elmachtoub and Grigas, 2022) choose a decision rule by minimizing the empirical decision cost directly over a policy class, on the argument that a regression fit ignores how its errors affect decisions. Hu, Kallus and Mao (arXiv:2011.03030v3, Management Science 2022) show that, under a margin condition on the problem, the comparison goes the other way: ETO attains faster regret rates than any method that only uses a policy class.
This mission formalizes their ETO upper bound, Theorem 8. It is the third of a three-mission series on the paper; the first formalizes the upper bound for empirical risk minimization over a policy class (Theorem 6) and the second the matching lower bound for policy-class methods (Theorem 7).
Write for Euclidean space with inner product and norm .
the extra cost of the best suboptimal vertex; otherwise .
It always holds with ; larger means less mass near dual degeneracy.
In Lean the polytope is FastCLO.ETO.Polytope, the distribution is FastCLO.ETO.Instance (the law of and the conditional law of given ), and optVal, Zstar, gap, NoiseCond, IsPlugIn and regret are the objects above.
Fix and . There is a constant depending only on these such that, for every instance satisfying the noise condition, every , every and every estimator with
the plug-in policy satisfies
The constant is existential, as on the page; the proof gives an explicit value, but the goal does not commit to it.
The milestones are the displayed steps of the paper's proof (Appendix A.5, p. 30), in order:
For well-specified least squares regression, is of order up to a logarithmic factor (Corollary 4 of the paper), and Theorem 8 gives regret of order up to logarithms. Theorem 7 of the same paper shows that no algorithm that only uses a policy class of Natarajan dimension can beat in the worst case over such instances. Since for every , the two results separate ETO from integrated methods when the regression model is well specified. This runs against the common intuition behind end-to-end learning. The noise condition is the CLO analogue of the Tsybakov margin condition in classification (Tsybakov, 2004): the gap plays the role of the distance of the regression function from the decision boundary.
The result is proved in the paper; as far as is known it has not been machine-checked. Formalizing it fixes the exact hypotheses (which quantifiers the tail condition carries, what "universal" means for , and the measurability the regret integral needs) and yields reusable pieces: the extreme-point argument behind the implication display and the peeling bound in .
The obvious argument bounds regret by , which gives only the rate and ignores the noise condition (this is Theorem 4 of the paper). The faster rate needs two things the naive bound does not use. First, a wrong decision at is possible only where the gap is positive and at most a multiple of the estimation error. This uses that plug-in decisions are extreme points, so a strictly suboptimal decision is at least worse than optimal; it requires finiteness of , which must be proved for an H-polytope. Second, the error must be controlled pointwise in , with sub-Gaussian tails over the data, and combined with the noise condition shell by shell, through a Fubini exchange between the data and the feature.
EuclideanSpace ℝ (Fin k). The polytope bundles , , , nonemptiness and the bound . The distribution is a probability measure on features and a Markov kernel with ; , and the data law is the -fold product of .Nesterov's accelerated gradient method minimizes a convex function with -Lipschitz gradient at the rate , which is optimal among first-order methods. For a -strongly convex the method with the generic momentum coefficient does not exploit the strong convexity: Su, Boyd and Candès show in §4.2 of arXiv:1503.01243 that its rate stays polynomial. Linear convergence is available with the momentum , but this requires knowing , which is rarely available in practice.
Restarting is the practical remedy. O'Donoghue and Candès (2013) proposed gradient restarting: reset the momentum whenever the objective increases. It is observed to recover linear convergence, but no rate was proved for it. Section 5 of Su, Boyd and Candès proposes a variant, speed restarting, which resets the momentum when the speed of the iterates stops increasing, and proves a linear rate for its continuous-time limit. This mission formalizes that result, Theorem 10 of the paper, and the lemmas it rests on.
Write with the Euclidean norm. A function is in if it is convex and continuously differentiable with . It is in if it is continuously differentiable and is convex. The class with is the standing assumption of the whole mission. A minimizer is written and ; the ratio is the condition number.
The Nesterov ODE is
the continuous-time limit of Nesterov's scheme with step size tending to zero. The paper's Theorem 1 shows it has a unique solution in . In Lean a solution is a pair with (IsSolution f 3 x₀ X V).
The speed restarting time of the solution from is
the first time at which the speed decreases (restartTime; the set is restartSet).
The speed restarted ODE (29) replaces by , where is the time since the latest restart . Its solution starts at , follows (3) from for time , then follows (3) from for time , and so on. If a restart point is a minimizer the trajectory stays there. In Lean this is the predicate IsSpeedRestarted f x₀ Xsr.
There are positive constants , depending only on , such that for every , every and every ,
The constants are left unspecified, so the goal survives improvements of them.
For one unrestarted solution of (3), with :
Theorem 10 is a linear convergence guarantee for a momentum method that does not need : the restart rule only watches the speed. The paper presents it as a new result; gradient restarting has no comparable theorem. It also gives a framework for analyzing restart rules: each restart decreases the gap by a factor depending on (Lemma 12), and restarts happen at a rate bounded below (Lemmas 13 and 25). Section 5.3 of the paper reports that the discrete analogue of the scheme (Algorithm 1) converges linearly in experiments.
The results are proved in the paper, but not formalized anywhere to our knowledge; the platform has no statement about restarting the Nesterov ODE. The formal work is the full proof, in particular the analysis of (3) near its singular point . Sharper constants are of interest: the paper conjectures that for a large class of , which would improve , and the generalization to friction with mentioned after Theorem 10 is a natural further target.
The ODE (3) is singular at , so the standard Picard–Lindelöf theory does not apply there, and the small-time estimates (Lemma 11, (30), Lemma 25) must control the solution uniformly up to , where the friction coefficient is unbounded. Lemma 11 bounds a supremum by a quantity that involves the same supremum; this argument needs a separate proof that the supremum is finite.
The speed restarting time is defined as a supremum, and neither nor follows from the definition. The restarted trajectory is assembled from infinitely many segments, and the number of restarts before time needs a lower bound. The obvious route through the rate of the unrestarted ODE gives only a polynomial rate, because it does not use strong convexity in a way that survives the restarts.
is EuclideanSpace ℝ (Fin n), is Mathlib's gradient, is an NNReal, and is the paper's literal definition. The classes , and the solution predicate of (3) come from the series' shared definitions (NesterovODE.WellPosed.Setting, NesterovODE.StrongCvx.Setting); the speed restarting time and the restarted trajectory sit in this mission's Setting definition, namespace NesterovODE.Restart.
Conventions the formalization commits to:
sSup is on an empty or unbounded set. Lemma 25 is stated as membership of in the set defining , and Lemma 13 as a bound on every element of that set, so neither can hold through this junk value.A complete development needs the analysis of (3) at (also the subject of mission I of this series), monotonicity arguments from derivative signs, and properties of strongly convex functions with Lipschitz gradient. The last two are reusable beyond this mission. Proofs of any milestone, and statements with explicit constants, are welcome.
Phase recovery (also called phase retrieval) asks to reconstruct a complex signal from the magnitudes of linear measurements of it, the phases being lost. It arises wherever detectors record intensities only: X-ray crystallography, diffraction imaging, astronomy and optics, where a sensor measures and not . The classical algorithms are alternating projections of Gerchberg–Saxton type (Gerchberg and Saxton, 1972; Fienup, 1982), which are fast but non-convex and can stall at stationary points that are not solutions.
Two convex relaxations change this picture. PhaseLift (Chai, Moscoso and Papanicolaou, 2011; Candès, Strohmer and Voroninski, 2013) lifts the signal to the rank-one matrix and relaxes the rank constraint to a trace minimization; for random Gaussian measurements it provably recovers with high probability (Candès and Li, 2014). Waldspurger, d'Aspremont and Mallat (arXiv:1206.0102v3, Math. Programming 2015) instead separate amplitude and phase and obtain PhaseCut, a semidefinite program with the structure of the Goemans–Williamson MaxCut relaxation, for which MaxCut algorithms (block coordinate descent, rounding) apply. The question this mission formalizes is how the two relaxations compare in the noiseless case.
Timeline. An earlier version of the paper showed that PhaseLift tightness implies PhaseCut tightness; Voroninski (2012, working paper, cited in arXiv:1206.0102v3, §4.3) reversed the argument under additional assumptions. Version 3 of the paper (2013) introduces the refined program PhaseCutMod and proves that, for injective , PhaseCutMod is tight whenever PhaseLift is (Corollary 4.3).
Fix a measurement matrix with rows , and a vector of amplitudes . The phase recovery problem (1) is
i.e. for every . Write for the Hermitian matrices and for positive semidefiniteness. When is injective, is invertible and the pseudoinverse is ; is the orthogonal projector onto the range of . With the diagonal matrix of the , set
The three programs are
PhaseCutMod selects, among the optimal points of PhaseCut (which in the noiseless case are exactly its points with ), one of minimal . A relaxation is tight when it has a unique optimal solution and that solution has rank one. The two lifted programs are linked by the map
In Lean these objects are PhaseCut.Tight.pinv, Mmat, Bmat, Phi, IsSolvable, phaseLiftFeasible/phaseLiftOptimal, phaseCutFeasible/phaseCutOptimal, phaseCutModFeasible/phaseCutModOptimal and IsTight.
If is injective, for all , and (1) has an exact solution, then
The statement fixes no constants and no probabilistic model: it is a deterministic comparison of two programs, valid for every and meeting the three hypotheses.
The result. Corollary 4.3 says that the MaxCut-type relaxation, once refined to PhaseCutMod, is never worse than PhaseLift at exact recovery: every recovery guarantee proved for PhaseLift (for instance the Gaussian-measurement results of Candès–Strohmer–Voroninski and Candès–Li) transfers to PhaseCutMod. Since PhaseCutMod can be approached by solving PhaseCut with replaced by for small , the algorithms designed for PhaseCut (greedy and block-coordinate SDP solvers) inherit those guarantees. The bijection of Proposition 4.2 also gives a precise dictionary between the lifted signal space and the phase space .
Formalizing it. The result is proved in the paper; to the best of current knowledge none of it has a machine-checked proof. The mission produces a formal statement of the three programs over complex Hermitian matrices, of the pseudoinverse identities for injective matrices, and of the trace and rank transport under the congruence , which are reusable for other lifting arguments in phase retrieval and low-rank SDP.
The corollary itself is short once Proposition 4.2 and the two transport identities are available; the substance lies in Proposition 4.2. The natural first attempt is to check that maps feasible points to feasible points, which is direct. Surjectivity is the step that requires an argument: a PhaseCutMod-feasible satisfies only the scalar constraint , and one must first upgrade it to the matrix equation (using positive semidefiniteness of both factors) and then to a range condition on before a preimage can be written down. In Lean, an additional cost is the absence of a pseudoinverse and of trace-zero-product lemmas for complex Hermitian matrices in the form needed, and the bookkeeping between complex traces and real objectives.
Matrices are Matrix (Fin n) (Fin p) ℂ and Matrix (Fin m) (Fin m) ℂ; is Mathlib's Matrix.PosSemidef (Hermitian included); rank is Matrix.rank. Conventions committed to:
Function.Injective A.mulVec. is encoded as (Aᴴ * A)⁻¹ * Aᴴ, Mathlib's inverse returning on singular matrices; it is the pseudoinverse only for injective , so every statement mentioning , or assumes injectivity. This adds injectivity, not present on the page, to the claim (p. 4) and to the companion claim on p. 12.Set.BijOn Φ (PhaseLift feasible) (PhaseCutMod feasible).Infrastructure that a complete development needs, and that is reusable beyond this mission: the pseudoinverse identities and for injective complex , the fact that is a Hermitian idempotent, the lemma for complex positive semidefinite matrices, and rank invariance under congruence by injective matrices. Proofs of any milestone are welcome, as are general Mathlib-style lemmas on these points.
In D-optimal design, a statistician chooses weights for a collection of candidate observations. The weights determine an information matrix, and maximizing its determinant favors a design that estimates several parameters jointly with a small confidence region. The same determinant objective appears in the minimum-volume enclosing ellipsoid problem. These links, and the earlier methods developed specifically for this objective, are described by Lu, Freund and Nesterov (2018), §2.2. A convergence theorem matters because a numerical design is useful only when its objective value can be related to the best possible value.
The paper applies a general relative smoothness framework to this problem. The usual first-order analysis asks for a uniform Lipschitz bound on the gradient of the objective. The logarithmic determinant has curvature that grows near singular information matrices, so a Euclidean smoothness constant on the whole design region is unsuitable. A logarithmic reference function gives a scale adapted to the coordinate boundary. The mission isolates the matrix result that provides this scale and the resulting explicit iteration bound for the primal gradient scheme. Both results are proved in the paper; their Lean statements are targets for formal proof.
Fix an real matrix with row rank and . A design weight is a vector with nonnegative coordinates and . This set is the simplex . Write and . On the points where is positive definite, the optimization problem is
The optimum may occur on the boundary of . At a singular point has no finite real value in the paper's model. Accordingly, the formal optimum is an attained point for which x^*, minimal among all such points.
For the algorithm, the positive simplex is . The reference function and its Bregman distance are
h(x)=-\sum_{j=1}^n\log x_j, \qquad D_h(y,x)=h(y)-h(x)-\nabla h(x)\cdot$y-x$.A primal gradient run starts at . At each iteration , it chooses to minimize
The coefficient of is exactly one. Proposition 2.2 of Lu, Freund and Nesterov (2018) establishes this relative smoothness constant on the positive orthant. The displayed update represents the minimization condition; no tie-breaking rule is fixed.
For all positive vectors , Proposition 2.2 asserts
f(y)\le f(x)+\nabla f(x)\cdot$y-x$+D_h(y,x).Its source-stated matrix claims form the first part of the milestone list. If , the paper identifies , , and . Equation (17) then records the full comparison with . Proposition 1.1 connects this Hessian comparison to relative smoothness. These statements fix the constant used by the algorithm.
The mission goal is Theorem 4.1 of Lu, Freund and Nesterov (2018). For , it states
The remaining milestones are the instance of the paper's primal gradient rate used here, the interior comparison point bound (40), and the logarithmic Bregman estimate (41)–(42). They follow the objects and constants named in the proof of Theorem 4.1.
The theorem gives a concrete stopping threshold expressed in the number of design weights, the requested objective gap, and the gap at the uniform start. It applies the same primal gradient method analyzed for general relatively smooth functions to a determinant objective whose gradient becomes steep near the boundary. The rate is an iteration count; it does not claim a superior arithmetic-operation count to specialized Frank–Wolfe methods. The paper compares those costs in its Table 1, noting that dense primal gradient iterations require a matrix inverse computation Lu, Freund and Nesterov (2018), §4.
A machine-checked development would connect finite-dimensional matrix inequalities, determinant derivatives, relative smoothness, and the algorithmic rate in one formal model. The matrix and logarithmic derivative results can be reused for other determinant objectives and barrier-based methods. The article proves Theorem 4.1; the mission asks solvers to formalize that known proof or another proof of the same precise statement. None of the draft theorem items is represented as already machine-checked.
The determinant objective is well behaved on positive definite information matrices but is undefined at a singular design. A first attempt to apply a smoothness bound over the entire closed simplex encounters unbounded curvature near that boundary. A second issue is that an optimal design can have zero weights, while the logarithmic reference function and the algorithm use positive weights. The rate statement must therefore compare an interior run with an optimum that may lie on the boundary. The milestone list exposes the matrix curvature estimate and the boundary comparison as separate claims rather than hiding either in the goal's assumptions.
Vectors are functions , with explicit finite sums; matrices have the corresponding finite index types. The Bregman pairing y-x$$ is Lean's real Fréchet derivative applied to . Iterates are zero-based. A Loewner inequality means that is positive semidefinite. Rank and are the standing data of problem (16). The reference function is used on the positive orthant, and Algorithm 1 minimizes over , matching the positive subproblem minimizer described on p. 341.
The paper treats as infinite when the information matrix is singular and as infinite at a zero coordinate. Lean's real logarithm has a total value there, so every theorem restricts its meaningful objective evaluations to positive vectors or positive definite information matrices. The goal represents by an attained on that domain. It states because the source's iteration formula divides by and takes a logarithm of a ratio involving it. The interior point in (40) is constructed from ; it is not an unconstrained input. These conditions rule out a vacuous interior, a junk logarithm, or division by zero as a formalization of the paper's conclusion.
The development needs matrix rank and positive definiteness, determinant and logarithm differentiation, positive semidefinite matrix order and the Schur product property, finite-sum calculus, and convex analysis of the positive simplex. The finite-dimensional matrix estimates and the relative smoothness criterion are natural reusable contributions. A proof may establish the listed milestones in another order, provided it keeps the same statements and constants.
Online learning studies repeated decisions made before their losses are known. A learner chooses a point, observes a loss function, and then uses that observation to choose the next point. The natural performance measure is regret: the learner's cumulative loss minus the cumulative loss of one fixed competitor chosen after the sequence is known. A regret bound makes a claim for every loss sequence, including a sequence adapted to the learner's earlier decisions. Orabona's Chapter 6 develops online mirror descent as a way to obtain such bounds in geometries other than Euclidean distance Orabona, Chapter 6.
The geometry matters because the decision set and its loss gradients can have very different scales under different norms. On a simplex, for example, a Euclidean description treats coordinate changes differently from an entropy-based description. Theorem 6.11 expresses the guarantee in a primal norm chosen for the regularizer and the corresponding dual norm for the observed subgradients. It is the chapter's general regret statement for the basic mirror-descent algorithm Orabona, Theorem 6.11, p. 67.
Let be a finite-dimensional real normed space, representing the book's with a chosen norm . The learner chooses from a nonempty closed convex set . A regularizer has domain ; it is strictly convex on and differentiable on the interior of . Its Bregman divergence is
defined when and . It need not be symmetric or satisfy the triangle inequality. The regularizer is -strongly convex on with respect to the chosen norm, where . The norm of a gradient , written , is the norm dual to . These are the conventions of Definition 6.4 and Lemma 6.10 Orabona, pp. 63–67.
At round , beginning with , the learner has , then observes a loss and a selected subgradient at . With step size , Algorithm 6.1 chooses any minimizer
The book gives two ways to keep each update in the interior of . The statements assume either of them, (6.5) or (6.6), , so every iterate is a valid reference point for the next Bregman divergence Orabona, Algorithm 6.1 and (6.6), p. 65. Regret is measured against one fixed :
For and nonincreasing positive step sizes, Theorem 6.11 gives the chapter's general bound
When every step equals the same , it also gives the more specific bound
The decreasing-step bound is the goal; the constant-step conclusion is a companion theorem. The milestone list records the book's three-point identity (Lemma 6.7), the unique-minimizer theorem for a closed strongly convex function (Theorem 6.9), and the existence and full three-part inequality of the one-step mirror-descent lemma (Lemma 6.10). Theorem 6.11 follows these results in the source Orabona, pp. 64–67.
The first bound makes the cost of the update explicit: one term measures the divergence from the competitor to the iterates, and the other accumulates squared dual norms of the selected subgradients. The constant-step form depends only on the initial divergence, which can be substantially easier to estimate. These forms let a later analysis choose a regularizer and norm pair suited to its feasible set and gradients, as the chapter does in its subsequent examples Orabona, §§6.6–6.7.
The theorem and its proof are known mathematically from the textbook. The work here is to express the algorithm, its admissible oracle choices, and the exact bounds as Lean statements and then prove them. A formal proof of the one-step inequality would also be reusable for later dynamic-regret and optimistic mirror-descent results. The published Bregman-divergence definition is reused, but the statements in this mission remain proof targets; a related published three-point identity assumes continuous differentiability, stronger than the book's hypothesis.
The usual squared Euclidean distance has a symmetric algebraic expansion. Bregman divergence is asymmetric and its second argument must lie where the regularizer is differentiable. Thus a direct replacement of squared distance by does not by itself establish that every update is defined or that the terms in a regret sum have the right orientation. Theorem 6.11 also allows changing step sizes, so the divergence terms carry different denominators from one round to the next. The one-step lemma packages the exact inequality needed to make those issues precise Orabona, Lemma 6.10 and Theorem 6.11, p. 67.
The Lean development uses an arbitrary finite-dimensional real normed space; continuous linear functionals represent subgradients, and their operator norm is . The regularizer is a total real-valued Lean function, but only its values on represent the book's function. Closedness is expressed by the closed epigraph of the extension equal to outside . Bregman divergence uses the published definition with the derivative at the second argument. The run predicate records the initial point, a selected subgradient, and a minimizer over on each round; it imposes no tie-breaking rule. The loss functions are real valued on , and subgradient inequalities are stated relative to , the only points compared in the regret result.
All sums use rounds ; index zero carries no data. The maximum is a finite maximum with the explicit condition . Positive and protect every division in the displayed bounds. Every drafted statement assumes the book's "(6.5) or (6.6)", with (6.5) read as a one-sided limit . The update is required to minimize over itself, and ranges over ; allowing points outside that set would change the theorem. The minimizer result, the full one-step chain, and both regret bounds are welcome proof targets. The domain-restricted closed-function representation and the finite-round run predicate can be reused in related online convex optimization developments.
A Markov decision process (MDP) evaluates a policy by its expected discounted reward, which requires the transition probabilities. In practice these are estimated from data, and the optimal policy of the estimated model can perform badly under the true kernel. Robust MDPs replace the kernel by an ambiguity set of kernels and judge a policy by its worst-case expected reward over that set (Satia–Lave 1973; Nilim–El Ghaoui 2005; Iyengar 2005).
Robust evaluation is tractable when the ambiguity set is rectangular, meaning that the kernels of different states (or state–action pairs) can be chosen independently. Many natural ambiguity sets are not rectangular, for example confidence regions for jointly estimated parameters. Wiesemann, Kuhn and Rustem (Math. Oper. Res. 2013) show that for general sets robust policy evaluation is NP-hard even to approximate (their Theorem 2.6). They then give a lower bound computable by semidefinite programming, which is the subject of this mission.
Timeline:
There are finitely many states and actions . Choosing action in state and moving to earns a reward . Rewards are discounted by , and the initial state has distribution in the probability simplex . An unknown parameter lies in
where each is symmetric with . The set is bounded and has a Slater point , at which every constraint is strict. The transition probabilities depend affinely on : , and this is a probability vector for every .
A stationary randomized policy fixes a distribution over actions in each state. It induces the transition matrix and the expected rewards . The reward to-go is . Robust policy evaluation asks for .
Fix . The affine approximate policy evaluation problem restricts reward to-go functions to affine maps :
The semidefinite program (20) maximizes over with and , subject to linear matrix inequalities. Constraint (20b) involves , and the matrices . Constraints (20c), one per state, involve , , , , and .
Let be an optimal solution of (20).
The theorem takes an optimal solution of (20) as given; it does not assert that (20) has one.
When the ambiguity set is not rectangular, the robust value of a policy cannot be approximated efficiently in general. Theorem 3.8 gives a certified lower bound on it, computable by a semidefinite program of size polynomial in , , and . Proposition 3.1 (c) makes (19) a restriction of the exact evaluation problem. For , for example an ellipsoidal confidence region for , the bound is the best affine one. The paper uses the theorem to compare policies under non-rectangular ambiguity, and in Proposition 3.10 to show that the bound is tight for s-rectangular sets.
On the formal side, the theorems are proved in the paper, and none of them, nor Proposition 3.7, has been formalized before. The platform has the exact S-procedure for one constraint, reused here, and other S-lemma variants in other settings. It has no approximate S-lemma for several concave quadratic constraints, no convex-Farkas argument for , and no robust MDP with an affine parametrization. A completed mission would give a machine-checked SDP reformulation of a semi-infinite constraint in a dynamic programming setting.
Each direction rests on a different fact. The step from (20) to (19) is the elementary direction of the S-lemma, applied state by state and then combined with the objective's epigraph constraint. Showing that the bound is attained for needs four further facts:
A tempting shortcut is to treat (20c) as an ordinary positive semidefinite constraint on a symmetric matrix. That is wrong here: the matrix is not symmetric, and only its quadratic form carries meaning.
Everything is finite-dimensional, and no measure theory is used.
IsPolicy). and are built from the published InducedTransition and InducedReward.PosSemidef of ) are hypotheses.Unit ⊕ Fin q, with the scalar entry first. "" means for all . This agrees with positive semidefiniteness on symmetric matrices and is the only faithful reading for (20c). Encoding (20c) with Mathlib's PosSemidef would make (20) infeasible and the goal vacuous, which is ruled out here. A verification instance with , shows that the standing hypotheses hold and that is feasible in (20).Welcome contributions include:
A constraint on a decision needs the distribution of the random vector , which in practice is known only through partial information: a support, some moments, the probability mass of a few regions. Distributionally robust optimization requires the constraint for every distribution consistent with that information. Wiesemann, Kuhn and Sim (Optimization Online 3757, 2013; Oper. Res. 62(6), 2014) introduced a standardized ambiguity set built from expectation conditions and probability bounds on confidence sets. Their Theorem 1 shows that the worst-case constraint over such a set is equivalent to a finite conic system, provided the confidence sets satisfy a nesting condition: any two are strictly nested or disjoint.
Many natural ambiguity sets violate nesting, for instance two overlapping confidence ellipsoids. For these the paper (§2.2) proposes two conservative approximations, the naïve approximation and the infimal convolution bound, and Theorem 3 orders them: the naïve approximation implies the infimal convolution bound, which implies the robust constraint. Infimal convolution bounds of this type had been used in classical and distributionally robust optimization before, e.g. in Goh and Sim (2010), Theorem 4. This mission formalizes Theorem 3, the steps of its proof, and Proposition 1, which compares partitions.
The random vector is , with an auxiliary . A proper cone is a closed convex cone with and nonempty interior, and means . For the confidence sets are , and the ambiguity set is
The standing conditions are: (C1) is bounded with (it is the support); (C2) some meets every non-degenerate probability bound strictly; (C3) , a maximum of finitely many bi-affine pieces, so is convex in . The distributionally robust constraint (3) is for all .
Write when lies in the interior of . A partition of , with blocks, satisfies the weak nesting condition (N′) if within each block any two distinct confidence sets are strictly nested or disjoint. The outer approximation keeps the expectation condition and only the probability bounds of block :
With , the naïve approximation (6) and the infimal convolution bound (7) are
under (C1)–(C3), (N′) and one disclosed added hypothesis, the uniform first-moment bound (see Formalization scope).
The result. Theorem 1 of the paper needs nesting; Theorem 3 is what remains when nesting fails. It certifies that both surrogates are safe (a decision satisfying either satisfies the robust constraint) and that the infimal convolution bound is never looser than the naïve one. The paper also shows that (7), with replaced by a closed approximation, has a conic reformulation (Observation 1), while optimizing over (6) with several constraints is strongly NP-hard (Theorem 4). Proposition 1 then says coarser partitions give tighter bounds, which guides the choice of partition.
Formalizing it. The result is proved in the paper; no machine-checked version is known. Formalizing it produces a reusable layer of extended-real worst-case expectations over sets of probability measures, with the infimal convolution and the perspective , and it corrects a gap in the printed proof of (6) (7) (see below).
The implications (7) (3) and Proposition 1 are short on paper; in Lean the work lies in extended-real arithmetic, where , and in the integrability of . The step (6) (7) is the delicate one. The constraint forbids putting all weight on the minimizing block, so the bound is reached only in a limit, and the limit requires every block's worst-case expectation of , and of uniformly in , to be controlled. The outer approximations drop the support condition (C1) for blocks that do not contain , so these worst-case values can be , and the printed justification fails.
is Fin n → ℝ; the outcome space is with its Borel σ-algebra. Indices are 0-based: is Fin (nI + 1) (so ), is index Fin.last nI, and is Fin nJ. A partition is a surjective block map blk : Fin (nI + 1) → Fin nJ, so every block is nonempty; "" is nJ = 1. Distributions in and in every are probability measures with a finite first moment, since a Lean integral of a non-integrable function is . Worst-case expectations, (6) and (7) take values in EReal, with ; the minimum in (6) is a finite infimum, and is used only on , where . Constraint (3) is in its -form.
Added hypothesis. The goal, milestone 4 and milestone 5 assume a uniform first-moment bound: for every , . Without it (6) (7) is false: with , of probability at least , of probability , the singleton partition, and , (6) holds through , while contains for every , so (7) fails. The bound holds whenever every block contains a bounded confidence set with . No other hypothesis is added; (N′), (C1) and the cone conditions are kept as on the page although the proofs do not use them.
The definitions rule out the trivializing formalizations: no expectation is a junk integral, empty blocks are excluded by surjectivity, the ambiguity set is nonempty under (C2), and no real-valued supremum or division by a zero weight appears. Contributions welcome: proofs of the milestones, and reusable lemmas on EReal suprema of integrals and on perspectives of piecewise-affine functions.
Classifiers trained to be robust against small, adversarially chosen input perturbations routinely lose standard accuracy. Adversarial training (Madry et al., 2018) improves worst-case accuracy under an -bounded attack, but on MNIST, CIFAR-10 and ImageNet the resulting models are measurably less accurate on unperturbed inputs, and the loss grows with the attack radius. A natural reading is that this is an artefact of training procedures or of finite data.
Tsipras, Santurkar, Engstrom, Turner and Mądry (ICLR 2019) argue otherwise: they exhibit a simple distribution on which every classifier faces the trade-off, so that the tension is a property of the data distribution itself and survives infinite data, including for the Bayes-optimal classifier. The argument isolates a distinction that has since been influential: robust features, moderately correlated with the label and stable under small perturbations, versus non-robust features, individually weak but jointly highly predictive and easily flipped. This mission formalizes the paper's first theorem, Theorem 2.1, and its proof in Appendix C.
Fix , a probability with , and . The distribution of an input-label pair , , is the data model (3):
with and independent given . Write and for the law of the weak features given and .
A classifier is a measurable map . Its standard accuracy is , the objective (1) of the paper with the 0–1 loss. Its robust accuracy at radius is
the objective (2) with the 0–1 loss and perturbation set . In Lean these are stdAcc d p η f and robustAcc d p η f ε, each an average with weight of the two class-conditional probabilities. The proof also uses , the probability that predicts when and the weak features follow (pij), and the shift adversary for (shiftAdv, accuracy shiftAcc).
For every measurable classifier and every ,
The statement quantifies over all classifiers, not a parametric family, and over every radius .
Theorem 2.1 converts the empirical observation into a statement about a distribution: on , standard accuracy caps robust accuracy at , so as robust accuracy falls to , while the adversary's budget is small compared with the feature scale . Together with the companion statements it shows that the model admits a classifier with accuracy above and a classifier with robust accuracy , but no classifier with both. It underlies the paper's conclusion that robust training must give up non-robust features, and the later line of work on robust versus non-robust features.
The result is proved in the paper, with an elementary argument. As far as the platform record and a search of the literature show, it has not been machine-checked. The formalization adds an exact, convention-explicit version of the model and of robust accuracy (worst case over a closed ball, outer measure of a possibly non-measurable event), a Lean statement of the shift-invariance property of Gaussian products that the argument rests on, and a reusable template for 0–1-loss adversarial objectives that later missions on robustness in Gaussian models can follow.
The obvious attempt is to bound robust accuracy for a specific classifier, or for linear classifiers, where the adversary's best response is explicit. That does not reach the theorem: the claim is about every measurable , for which no best response is computable and the robust event need not even be measurable. On the formal side, the statements involve the pushforward of a product of Gaussians under a coordinatewise shift, the decomposition of the class-conditional law into the two-point law of and the product , and a measure applied to a possibly non-measurable robust event; none of these is available as a ready-made lemma for this model.
Inputs live in Fin (d + 1) → ℝ; coordinate 0 is and coordinate i.succ is . The Mathlib norm on this type is the sup norm, so ‖δ‖ ≤ ε is exactly the ball. Labels and predictions are the reals . The class-conditional law is ((x1Law p y).prod (weakLaw d η y)).map (Matrix.vecCons ·.1 ·.2) with weakLaw d η y = Measure.pi (fun _ => gaussianReal (y * η) 1). Accuracies are real numbers in computed with toReal. The robust event is measured by its outer measure, i.e. under the completion of ; no measurability of that event is assumed.
The standing assumption of model (3) is a hypothesis of every statement. Four hypotheses implicit on the page are explicit: in the goal (the bound divides by , and Lean's would make the statement false at ); (the page takes large, ; with the case has no adversary and the statement fails); measurability of ; and for every .
A trivializing formalization is ruled out: the goal is stated for every measurable -valued classifier and for the worst case over the full ball of every radius , not for linear classifiers, not for the fixed shift adversary, and not with the among its hypotheses; those appear only in milestones.
The development needs Mathlib's gaussianReal, Measure.pi, product measures and pushforwards. Welcome contributions: the Gaussian shift identity (reusable for any Gaussian location model), the disintegration of condLaw along , and the two accuracy formulas.
Matrix approximation replaces a large or complicated matrix with a random matrix that is easier to store or compute. Averaging independent realizations improves accuracy while retaining the structure of each realization. Examples in Tropp's monograph include sparse approximations and randomized matrix products. The practical question is how the number of samples, the size of one sample, and its second moment control the spectral norm error. Tropp, §6.2
The book proves a matrix Bernstein inequality in Theorem 6.1.1, then applies it to an empirical matrix average in Corollary 6.2.1. Theorem 6.1.1 is already posed as TroppMatrixConcentration.matrix_bernstein on Prove2Me and is currently Open. This mission records the application with its own hypotheses and constants. The capstone concerns the estimator that a reader would construct, rather than a sum of abstract centered summands. Tropp, §§6.1–6.2
Let be a fixed complex matrix. A sample matrix has the same size, has expectation , and has spectral norm at most almost surely. The equality makes one sample an unbiased estimate of . The almost-sure bound limits the size of every sample except on a probability-zero set. The dimensions are positive integers, and is a positive sample count.
Take independent copies with the distribution of . Their matrix sampling estimator is
For any rectangular matrix , denotes its conjugate transpose and its spectral norm. The per-sample second moment is
Both terms matter for a rectangular matrix: and act on different coordinate spaces. All expectations of matrices are entrywise expectations, represented by Bochner integrals in Lean. The almost-sure norm bound guarantees the moments used here are finite. Tropp, equations (6.2.4)–(6.2.6)
Corollary 6.2.1 gives an expectation estimate and a tail estimate for the same estimator. For every real ,
The goal includes both bounds. The expectation estimate controls average error; the tail estimate controls the chance of an error above a chosen threshold. The dimension enters only through in the expectation bound and the factor in the tail bound. These are the book's constants, including the factors and in the linear terms. Tropp, Corollary 6.2.1, p. 81
The milestone list follows Corollary 6.1.2 for uncentered summands, the bound , and the variance estimate . Equation (6.2.7) is a companion: a stated lower bound on implies for . Tropp, pp. 77, 82
The result turns a bound on one random matrix into a quantitative guarantee for an empirical approximation. It lets a user choose a sample count for a target error and evaluate both average error and failure probability. The same framework is instantiated later in the monograph for matrix sparsification and multiplication; those applications depend on controlling and for their particular sampling laws. Tropp, §§6.2–6.4
This is a known mathematical result proved in the book. Its Lean statement is an open formalization target. The mission adds a reusable empirical-mean definition and application statements built on the already published matrix spectral norm and rectangular second-moment definitions. A proof of the general matrix Bernstein theorem remains separate; the mission can draw on it when that platform theorem is proved.
The estimator error is a centered sum, but the sampling assumptions are given for an uncentered random matrix . Bounding the centered summands changes the uniform bound from to . The variance parameter must be related to the second moment of one uncentered sample, with the correct scaling. Dropping the common-distribution condition would leave no relation between the samples' second moments and . Applying scalar concentration to entries would not directly give the stated spectral norm bound or its dimension dependence. Tropp, proof of Corollary 6.2.1, p. 82
Matrices are Matrix (Fin d₁) (Fin d₂) ℂ. The spectral norm and rectSecondMoment are imported from tc's published TroppMatrixConcentration definitions. An arbitrary probability space carries a measurable reference matrix and a finite family ; iIndepFun expresses independence and IdentDistrib expresses equality in law with . The estimator is the finite sum scaled by . No particular sampling scheme or deterministic choice of is fixed: the formal goal requires only the source's unbiasedness and boundedness conditions.
The Lean statements explicitly require , , measurability, and the almost-sure form of . These make the logarithm and inverse sample count meaningful and make the random matrix laws well behaved. For the uncentered Bernstein corollary, integrability of each is explicit because a bounded deviation from an unspecified mean alone does not establish that the mean exists. The goal also asserts integrability of its error norm, preventing a Bochner integral from silently taking Lean's default value for a nonintegrable function. The bound on supplies that integrability. When the denominator in a tail formula is zero, the displayed total real division gives a loose bound at the degenerate case; the source's probabilistic claim remains valid.
Contributions that formalize the centered-summand calculation, the variance estimate, or the transfer from the general matrix Bernstein theorem are within scope. The imported matrix and probability definitions are reusable in other matrix concentration missions. The local empirical-mean definition is reusable whenever a matrix estimator averages finitely many random samples.
Large matrices are often reduced by retaining only some rows or columns. The reduced matrix is cheaper to store and apply, but its spectral norm can be distorted by a single unusually large row, column, or entry. A useful estimate must show both the average effect of sampling and the cost of these local concentrations. In §5.2 of Tropp's monograph, matrix Chernoff inequalities give numerical estimates for independently sampled columns and for independently sampled rows and columns. The latter is the capstone of this mission.
The general matrix Chernoff inequality, Theorem 5.1.1, is already an Open goal in tc's Chapter 5 mission on Prove2Me. The intrinsic-dimension Chernoff inequality, Theorem 7.2.1, is likewise Open in tc's Chapter 7 mission. This mission concerns the application statements that those chapter missions have not posed: the numerical bound (5.2.2), its three displayed intermediate estimates, and companion consequences in §§5.1.1, 5.2.1 and 7.2.2. The motivation for choosing this target is that it connects a general concentration result to a concrete random matrix model; its terms can be read directly from a deterministic input matrix.
Fix a complex matrix with . For each row , let equal one when that row is retained and zero otherwise. For each column , let have the analogous meaning. The whole family is independent, with and , where and . Thus and are the expected numbers of retained rows and columns. Put
The zeros remain in the matrix: has the same dimensions as , but entries in discarded rows or columns vanish. Write for row , for column , and for an entry. Their vector norms are Euclidean, while and denote the spectral operator norm. The source uses for expectation over the selections. Its maxima range over all rows, columns or entries of , so a highly uneven matrix is distinguished from one whose mass is spread evenly.
The first milestone is the streamlined upper matrix Chernoff expectation bound. For a finite independent family of positive semidefinite Hermitian matrices with eigenvalues at most , let and . The bound uses the book's numerical constant . The subsequent milestones specialize this setting to the row and column selectors above. A separate companion states the lower bound with and the two weakened tail inequalities of §5.1.1.
The goal is the exact displayed estimate (5.2.2), with the book's rounded constants:
Its milestone chain is (5.1.8), followed by (5.2.3), (5.2.4), and (5.2.5). These are the claims the text places immediately before the final estimate. They bound, respectively, the first column-selection stage, the norm of the row-selected matrix, and the largest column norm after row selection. The companion (5.2.1) gives both the top and least squared singular-value bounds for column selection alone. The companion from §7.2.2 replaces by , where is stable rank.
The goal separates four sources of size in a sampled matrix. The first term scales the squared spectral norm by the expected row and column retention fractions. The remaining terms record concentrations in a column, a row, and an individual entry. Consequently, the estimate can be evaluated from and the two sampling rates without specifying a distribution for itself. It is an expectation bound, not a claim that every realized submatrix is close to .
The formal development would make the application layer of Tropp's Chapter 5 available alongside tc's general, currently Open matrix Chernoff theorem. A proof of that general theorem does not itself identify the random projectors, their joint independence, or the deterministic quantities on the right side of (5.2.2). The stable-rank companion also links the Chapter 7 notion of intrinsic dimension to a concrete rectangular matrix statistic. Both the chapter's general theorems and this mission's statements remain Open on the platform; none is being presented as already machine proved. Tropp, §§5.2 and 7.2.2 gives the mathematical results.
Sampling both rows and columns introduces two interacting random projectors. Merely applying a one-stage column estimate to leaves the row selection uncontrolled; merely applying a one-stage row estimate leaves the sampled column norms random. The two families must be independent of each other as well as independent internally. That distinction is substantial: separate independence claims for the row family and the column family do not imply independence between and . The final estimate must also retain the book's exact and coefficients rather than replacing the right side by an unspecified constant times a simpler expression.
Matrices are Matrix (Fin d) (Fin n) ℂ, matching the book's general complex-matrix convention. The spectral norm, extreme eigenvalues, Borel measurable matrix space, and intrinsic dimension come from tc's published definitions, which this mission references. Random selectors are measurable real-valued functions on a probability space; their Bernoulli law specifies almost-sure values zero or one and the probability of one. The row and column selectors form one jointly independent family. Products with diagonal selector matrices define , and ; a deterministic diagonal or an unconstrained zero-one function would not be the sampled model.
Every sampling rate is within its Bernoulli domain. Nonzero dimensions keep the maxima over finite, inhabited sets and give the logarithms their intended arguments. Lean's Bochner integral otherwise returns zero on a nonintegrable function; each expectation inequality records integrability in its conclusion, which follows from measurable, bounded Bernoulli selectors and Tropp's standing regularity convention in §2.2.1. The maxima of column, row, and entry magnitudes are real finite suprema, equal to maxima for these finite nonempty index sets. The intrinsic-dimension identity assumes and for scale invariance; the final stable-rank bound itself includes zero sampling and the zero matrix.
The definitions of Bernoulli selection, random diagonal projections, sampled matrices, finite norm maxima and stable rank are reusable outside this mission. Contributions can address their structural identities, integrability, the four milestones, the goal, or the independent column-selection companions. The book's constants and are retained as decimals; and are the rounded coefficients printed in (5.2.2), as the text explains on p. 66.
In a game, each participant chooses a strategy while the cost of that choice depends on what everyone else does. A network user may choose a route, for example, but its travel time depends on the routes chosen by other users. The price of anarchy compares the cost of self-interested outcomes with the best joint outcome. A guarantee restricted to a Nash equilibrium leaves open what happens when players repeatedly adapt their choices without settling on any equilibrium. Roughgarden's extension theorem addresses sequences produced by players whose accumulated costs are asymptotically competitive with fixed alternatives. Its bound depends on a property of the game, rather than on a particular learning algorithm or on convergence of play. Roughgarden, §§1 and 3.2.
There is a finite set of players , and player has a strategy set . These sets may be infinite. An outcome specifies one strategy for every player. The real number is player 's cost, and the joint cost is . The paper treats this objective as nonnegative. If player alone changes to the strategy of another outcome , its cost is written ; every other player's strategy stays as in . Roughgarden, §2.1.
A game is -smooth if every pair satisfies . The robust price of anarchy is the infimum of over all such smoothness pairs with . This number packages every bound obtainable from the same smoothness condition. It is taken in the extended reals, with value when no pair exists; the mission assumes an admissible pair exists, so it is below . Roughgarden, Definitions 2.1–2.2.
For a played outcome at time and a comparison outcome , define the hypothetical improvement . A player has vanishing average external regret when its average cost, up to an error tending to zero, is no greater than the average cost it would have paid by using any one fixed strategy throughout the first rounds. The comparison strategy is held fixed across time, while the other players' strategies may change on every round. Each player may have its own error function. Roughgarden, (22), (24).
The paragraph following equation (25) asserts a bound with a vanishing additive error. For any comparison outcome and every horizon , there is a function with
This target includes the case . The paper states the conclusion for an optimal outcome; the same displayed relations also apply to any comparison outcome. Relations (23) and (25) are separate milestones: the former bounds one outcome using the players' hypothetical improvements, and the latter averages that bound over time. Roughgarden, §3.2, pp. 13–14.
The mission goal is Theorem 3.3's multiplicative presentation. For a comparison outcome with , there is a function such that
The positive-cost condition is needed to make the printed statement true. Consider one player with strategies of costs and , playing the costly strategy once and the zero-cost strategy thereafter. Its average regret tends to zero, but its average cost is at every finite horizon. Taking the zero-cost strategy as makes the right-hand side of the printed multiplicative bound zero for any . The additive milestone preserves the valid zero-cost case. Roughgarden, Theorem 3.3 and the paragraph preceding it.
The result transfers a bound defined by the game's smoothness condition to repeated play even when the sequence does not converge. It therefore gives a welfare guarantee for the behavior captured by vanishing external regret without identifying which learning rule generated the sequence. The additive statement also records exactly what remains true when an optimal outcome has zero cost. Roughgarden, §3.2.
Formalizing the result makes the quantifiers behind explicit: for each fixed game, sequence, and comparison outcome, one error sequence works across all positive horizons and tends to zero. The development also distinguishes the paper's valid additive consequence from its multiplicative display at zero cost. The paper proves the result mathematically; the Lean files in this mission are theorem statements for solvers and do not yet contain machine-checked proofs.
For a fixed smoothness pair, a finite-time inequality controls average joint cost by the comparison cost and players' average hypothetical improvements. Regret controls those improvements asymptotically, but the robust price of anarchy takes an infimum over all admissible pairs. Passing from bounds for individual pairs to that infimum requires the sign and boundedness conditions on the joint cost to be tracked correctly. A direct replacement of the fixed pair's ratio by does not itself justify the limit. The zero-cost example also shows why an additive error cannot simply be displayed as a multiplicative term in every case. Roughgarden, (23)–(25) and Theorem 3.3.
Lean uses a finite type of players, arbitrary strategy types, and real-valued player costs. It defines the joint objective by the finite sum ; it does not assume that each individual cost is nonnegative. The goal and additive milestone assume that the joint objective is nonnegative at every outcome, matching the paper's standing convention. They also assume at least one smoothness pair with , the case in which and the page's bound is vacuous. is an extended-real infimum and the inequalities are compared in the extended reals. For a nonnegative game with an admissible pair, is a real number at least 1 when some outcome has positive cost; if all outcomes cost zero, the target cost bounds are zero. Roughgarden, §§1, 2.1, 3.2.
Time indices are , with . The Lean sequence is infinite so that the asymptotic assertion concerns prefixes of one sequence; its value at index zero is unused. The regret definition quantifies over every fixed alternative strategy rather than assuming a minimum is attained when a strategy set is infinite. A separate vanishing error sequence may be chosen for each player. The conclusion chooses one vanishing error sequence after the game, play sequence, and comparison outcome, and uses it at every horizon. These choices make the terms genuine limits, rather than unconstrained values chosen separately for each . Roughgarden, (24), Theorem 3.3.
The game objective, smoothness predicate, robust price of anarchy, deviation improvement, and regret predicate are the reusable definitions. Solvers can contribute proofs of the one-step bound, its averaged form, the additive conclusion, and the main theorem. Mixed-outcome sequences from Remark 3.4 are outside this mission's core; their probability and integrability conventions would require another definition layer.
Accelerated gradient methods minimize smooth convex functions with a characteristic momentum term. Su, Boyd, and Candès identified a continuous-time differential equation whose trajectories model that acceleration. The equation replaces an iteration index by continuous time and makes the effects of damping visible. This mission concerns the paper's strongly convex regime: the function has curvature everywhere, yet the ODE with damping proportional to is not simply a linear-rate method. Theorem 8 quantifies the faster polynomial rate that the authors establish when the damping parameter is large enough.
The paper first treats the coefficient , obtaining an inverse-square objective bound. In §4 it replaces by , and in §4.3 it combines larger damping with strong convexity. The result gives a family of exponents rather than a single preferred exponent. The rate reaches at the end of the allowed range. The paper also explains that simply raising does not automatically improve every finite-time bound, because its constant can grow with .
The state space is Euclidean . A function belongs to when it is convex, continuously differentiable, and its gradient is -Lipschitz for some . It belongs to when it is continuously differentiable and is convex. The class is their intersection. For this mission . A point is any global minimizer, and .
Given an initial point , a damping parameter , and time , the ODE trajectory satisfies
The velocity records . The regularity asserted is . The paper writes “the solution” and says an earlier existence argument applies to general ; the formal statements quantify over every trajectory satisfying the ODE and initial conditions. This captures the rate claim without identifying functions at irrelevant negative times.
Two energy functions organize the chapter. The first, , weights the objective gap by and adds . The second, , weights the gap by and adds . The threshold is for . These are the paper's objects in §4.1 and §4.3, not alternate energies chosen for ease of formalization.
For , the paper proves both a pointwise inverse-square estimate and a bound on accumulated weighted error:
Its energy derivative inequality (18) is an earlier milestone. Equation (24) gives the integrated bound for at and after , and equation (26) bounds the energy at that threshold. Those two displays are additional milestones. Their full statements, including the intermediate inequalities, are retained in Lean.
For every with , there is a constant such that
The constant does not depend on , , , , the minimizer, initial point, chosen solution, or time. At the claim includes ; the threshold arguments used for are not imposed on that boundary case.
The theorem says how curvature and damping change the continuous-time objective rate. It separates the exponent, which is set by and , from the explicit dependence on strong convexity, . The baseline Theorem 5 is also useful independently: its weighted integral estimate records more than an pointwise statement. The paper uses these continuous-time estimates to motivate comparisons with generalized discrete Nesterov schemes Su, Boyd, and Candès, §4.
This result is proved in the cited paper. The work here is to state its hypotheses, energy identities, and rate in Lean so that the established argument can be checked. The definitions of smooth and strongly convex classes, the singular-time solution predicate, and the calculus of real-power energies are reusable in other continuous-time optimization results. No machine-checked proof of these newly drafted statements is claimed by this proposal.
At the damping coefficient is singular, so a statement that applies ordinary second-order ODE calculus across zero would miss the actual boundary condition. Away from zero, the ordinary inverse-square energy does not by itself deliver the stronger exponents of Theorem 8. The stronger energy has real powers of and its derivative contains terms with different signs. Strong convexity controls some terms only after the threshold ; the early-time and late-time regimes therefore have different estimates. The argument must also cover real exponents throughout , including the endpoint .
Lean uses EuclideanSpace ℝ (Fin n) for , with any natural number . The function classes follow the literal definitions on page 5: convexity, continuous differentiability, a Lipschitz gradient with positive constant , and convexity of . The rate assumes , implicit in the paper's denominator and in . A minimizer is supplied as a point satisfying for every ; it is not assumed to be a special optimizer returned by a choice function.
The ODE predicate includes the initial data, a right derivative for at zero, right continuity of at zero, and derivatives of both functions for positive time. It says nothing about negative time. Theorem 5 explicitly asserts integrability on before bounding its integral, preventing the default value of a nonintegrable Bochner integral from satisfying the statement. Real powers are used only with positive bases. Every appearance of is under , and every use of in a milestone is under and , so its denominators are nonzero.
In the goal, is existentially quantified before the dimension, function, curvature and smoothness constants, trajectory, and time. A constant selected separately for each function or time would weaken Theorem 8 and is excluded. Contributions establishing the energy derivatives, the improper integral, the threshold estimates, and the real-exponent induction are all within scope. The statement of Theorem 8 keeps the paper's full exponent range even if some parts demand substantial new calculus support.
Gradient methods for convex minimisation are usually analysed under two assumptions on the objective : its gradient is Lipschitz continuous (-smoothness), and, for linear rates, is strongly convex. Many objectives met in practice satisfy neither on their whole domain. The D-optimal design objective , the univariate function on and objectives with polynomially growing Hessians have Hessians that blow up near the boundary or grow without bound at infinity, so no single Lipschitz constant exists and the classical rates of gradient descent say nothing.
Lu, Freund and Nesterov (SIAM J. Optim. 28 (2018) 333–354) replace the Euclidean yardstick by a reference function and measure smoothness and strong convexity of relative to the Bregman distance of . The same notion was introduced independently by Bauschke, Bolte and Teboulle (Math. Oper. Res. 42 (2017)), whose NoLips algorithm coincides with the scheme studied here. The paper shows that the plain primal gradient scheme, run with in place of the squared norm, keeps the rate of gradient descent, and converges linearly when is also strongly convex relative to . This mission formalizes that result, Theorem 3.1 of the paper, together with the steps of its proof.
Let be a finite-dimensional real inner-product space and a convex set. Let be differentiable at every point of and convex on . The function is the reference function; it need not be strongly or even strictly convex.
The Bregman distance of is
with the derivative taken at the second argument. For convex it is nonnegative, but it is neither symmetric nor a metric.
Given , is -smooth relative to if
for all in the interior of (the relative interior when has empty interior). Given , is -strongly convex relative to if the reverse inequality holds with in place of . With these are the classical notions.
The primal gradient scheme (Algorithm 1) starts from and sets
In Lean, bregman h y x is , IsRelSmooth Q f h L and IsRelStronglyConvex Q f h μ are the two relative conditions, and IsPrimalGradientRun Q f h L x says that the sequence x : ℕ → E is a run.
Under the hypotheses above, with , for every run of Algorithm 1 the values are nonincreasing, and for all and
where for only the outer bound is asserted.
Companion statements: the geometric decay (27) of the linear bound, and Proposition 1.1 (a), (b), the convexity and gradient-monotonicity characterisations of the two relative conditions.
The theorem shows that the convergence theory of gradient descent does not depend on the Euclidean geometry: whenever a reference function can be found for which is relatively smooth, and the subproblem of Algorithm 1 can be solved, the method converges at rate , and linearly under relative strong convexity, with constants that depend only on , and . In the paper this is applied to the D-optimal design problem, whose objective is 1-smooth relative to but has no Lipschitz gradient on the simplex, and to objectives with polynomially growing Hessians, for which reference functions are constructed.
The result is proved in the paper. No machine-checked proof of the result is known to us. The mission formalizes relative smoothness and a Bregman gradient method under the paper's weak assumptions: no strong or strict convexity of , no Legendre or essential-smoothness conditions, and no closedness of . The definitions and the three-point lemma are reusable for mirror descent, Bregman proximal point methods and the dual averaging scheme of the same paper.
The obvious route is to copy the textbook proof for -smooth functions, which uses the descent lemma together with the Pythagorean or cosine identity for the squared norm. For a general neither tool is available: is not symmetric, is not a squared norm, and satisfies no triangle inequality, so all distance bookkeeping has to go through the three-point property and the exact weights .
A second difficulty is that relative smoothness and strong convexity are assumed only on the (relative) interior of , while the iterates of Algorithm 1 and the comparison point may lie on the boundary of . Using the hypotheses at boundary points requires extending them from the relative interior, which needs the continuity of and on and the convex-analytic fact that a convex set lies in the closure of its relative interior.
is a finite-dimensional real inner-product space (InnerProductSpace ℝ E, FiniteDimensional ℝ E); are differentiable as functions on at every point of , and convex on . The pairing is the Fréchet derivative fderiv ℝ f x v. "Interior, or relative interior when there is no interior" is intrinsicInterior ℝ Q. Iterates are indexed from , as in the paper; sums are over Finset.Icc 1 k; powers are natural-number powers.
Hypotheses added or dropped relative to the page: is added wherever appears in a denominator (Theorem 3.1 says only , ; Theorem 3.2 of the paper states itself). The middle term of (26) "defined in the limit as " is not formalized as a limit: the goal asserts the outer bound for all and the full chain for . "Monotonically decreasing" is read as nonincreasing. Closedness of is dropped, which strengthens every statement. The monotonicity milestone drops relative strong convexity, which it does not use.
Ruled out: the argmin step is a property of the next iterate, never a choice function, so no statement can hold because of an arbitrary choice; the relative conditions range over the relative interior, never over interior Q, which is empty for lower-dimensional and would make the hypotheses vacuous; every division by carries , so Lean's convention never enters; and are assumed differentiable on , so fderiv never takes its junk value at a point where the statements use it.
Infrastructure needed: nonnegativity of on for convex differentiable ; extension of first-order inequalities from the relative interior to ; the first-order optimality condition for minimisation over a convex set; geometric sums and Bernoulli's inequality. Contributions of proofs of the milestones, and of reusable lemmas on Bregman distances, are welcome.
Classical complexity bounds for first-order methods assume that the gradient of the objective is Lipschitz continuous, or that the objective is strongly convex, with respect to a norm. Many convex problems of practical interest satisfy neither assumption: the objective of D-optimal experimental design, , has a gradient that blows up near the boundary of the simplex, and Poisson inverse problems and some regularised regression problems behave similarly. Lu, Freund and Nesterov (SIAM J. Optim. 28 (2018), arXiv:1610.05708) replace the norm by a convex reference function and measure smoothness and strong convexity through the Bregman distance of . Independently, Bauschke, Bolte and Teboulle (Math. Oper. Res. 42 (2017)) introduced the same smoothness notion as a "Lipschitz-like/convexity condition" for the NoLips method.
The paper proves guarantees, and linear rates under relative strong convexity, for two first-order methods: the primal gradient scheme (Theorem 3.1) and the dual averaging scheme (Theorem 3.2), the method of Nesterov (Math. Program. 120 (2009)) adapted to a Bregman geometry. This mission formalizes Theorem 3.2 and the steps of its proof.
Let be a finite-dimensional real inner-product space and a convex set. Let be convex on and differentiable at every point of , and let be another such function, the reference function; need not be strongly or even strictly convex. The Bregman distance of is
Relative smoothness and strong convexity. For constants and , is -smooth relative to on if
and -strongly convex relative to on if
both for all in the interior of (in the relative interior when has empty interior). With these are the usual -smoothness and -strong convexity.
The dual averaging scheme (Algorithm 2). Assume and set the weights
The starting point is the -center of : a minimiser of over , normalised so that . For the scheme sets
In Lean these objects are bregman, IsRelSmooth, IsRelStronglyConvex, daWeight L μ i (), daSum L μ k (), daModel f h L μ x k () and IsDualAveragingRun. We write .
If is -smooth and -strongly convex relative to with , then every run of the dual averaging scheme satisfies, for all and ,
where at the middle term is read as its limit , which equals the right-hand side.
A companion item states (33), , the linear-rate reading of the middle bound.
Theorem 3.2 gives the dual averaging scheme the same guarantee in the relative setting that the primal gradient scheme obtains in Theorem 3.1: an bound on the best iterate with constant when , and linear convergence with ratio when . The bound depends on rather than on , and the scheme aggregates all past linearisations rather than only the last one, so a single analysis covers both regimes and with one weight sequence. Neither the smoothness nor the convexity of is needed with respect to any norm, which is what allows applications such as D-optimal design (the third mission of this series).
The result is proved in the paper. As far as the platform's catalogue shows, neither relative smoothness nor this theorem has a machine-checked proof. Formalizing it produces a reusable Bregman-geometry layer (Bregman distances of differentiable convex functions, first-order optimality over a convex set, aggregation of linear models) and a checked statement of the rate.
The algebra of the weights is elementary; the difficulty lies in the analytic steps. Identity (35) requires the derivative of the model at , so it depends on computing the Fréchet derivative of a finite sum of affine terms and multiples of , and its inequality is the first-order optimality condition for a minimiser over a convex set that may have empty interior. The relative conditions are assumed only on the (relative) interior of , while the iterates may lie on its relative boundary and the conclusion is claimed for every : passing from one to the other uses the differentiability of and on all of , and cannot be done by assuming the iterates are interior. A direct induction on the iterates does not work either; the argument goes through the model values , and the index shift between and in (36) has to be tracked exactly.
InnerProductSpace of finite dimension; is any convex set (closedness, assumed on the page, is not required, which strengthens the statement).DifferentiableAt every point of . The pairing is fderiv ℝ g x v. No strong or strict convexity of is assumed.intrinsicInterior ℝ Q, which is the interior when it is nonempty and the relative interior otherwise; and are fixed before the points. The page's "" with is the pair .x : ℕ → E indexed from . Each argmin is a property of the next iterate (membership in and minimality of its model value), never a choice function. The -center normalisation is part of the run, as Algorithm 2 states it.Finset.Icc 1 k. The limit is not formalised: the goal states the outer bound for all and the middle bound for .These choices rule out the trivializing readings: no junk fderiv is used (all derivatives are taken at points of , where differentiability is assumed), no condition is quantified over an empty interior, no argmin is a choice function, and no division by occurs.
A complete development needs: derivatives of finite sums, first-order optimality of a minimiser over a convex set, the extension of the relative conditions from the relative interior of to , and geometric sums. The Bregman layer and the extension lemma are reusable for Theorem 3.1 and for other Bregman methods. Proofs of the milestones, and of the companion (33), are welcome independently.
A firm selling a fixed stock of a perishable product over a finite season must set prices without knowing how demand responds to them. Online retail and travel platforms often see a customer's segment before quoting a price, so they can price-discriminate across consumer types. Learning a separate demand curve for each type, however, seems to cost more exploration as the number of types grows. Chen and Gallego (arXiv:1812.09234v3, 2021; Mathematics of Operations Research, 2022) give a learning algorithm whose regret does not depend on the number of types. Their key step is to learn a single scalar first: the shadow price of inventory.
Earlier work on the single-type problem frames the question. Besbes and Zeevi (Operations Research, 2009) defined the regret against the fluid benchmark and showed that no policy can achieve regret decaying faster than . Wang, Deng and Ye (Operations Research, 2014) gave a single-product algorithm whose regret matches this rate up to logarithmic factors. Chen and Gallego extend the rate to types with one inventory constraint.
There are consumer types, a season and an inventory . When the firm charges price to type , type- consumers arrive at rate . Prices range over , where is a choke price with . Assumption 1 asks that each be strictly decreasing, bounded and Lipschitz, and that the revenue rate be Lipschitz and twice differentiable, with .
The fluid problem (2) maximizes subject to . Its optimal value is . Its dual is one-dimensional. With
the dual optimum is , and the optimal fluid prices are the constants .
In the -th system demand and inventory scale together: type arrives as a Poisson process with rate , and the inventory is . The firm does not know . It knows , , , the constants of Assumption 1 and, by Assumption 2, intervals and that contain every and . A policy has expected revenue , and its regret is
Algorithm 1, the primal-dual learning algorithm, runs phases of shrinking lengths . In each learning phase it tests a price grid inside the current interval estimators of every . It then minimizes an empirical dual function on a grid of and re-centres the interval estimators of and . In the last phase it either charges a marked-up price (sufficient capacity), or tests two prices and interpolates between them so that total sales end close to (insufficient capacity). Its tuning depends on a constant .
For every one can choose and a constant , independent of , such that
Theorem 1 states that personalized pricing for types under a shared inventory constraint is learnable at the single-type rate , up to logarithms, with a constant independent of . Combined with the Besbes–Zeevi lower bound, the algorithm is rate-optimal. Learning the scalar shadow price , instead of the joint optimum of an -dimensional problem, is what avoids the curse of dimensionality.
The result is proved in the paper; no machine-checked version exists. A formalization would add to the platform a multi-type Poisson pricing model with stock-outs, the one-dimensional Lagrangian dual of the fluid revenue-management problem, an exactly specified multi-phase learning algorithm, and reusable Poisson deviation lemmas. Lemmas 1, 2, 9 and 10 and Proposition 1 can be proved independently of the probabilistic analysis.
The obvious argument estimates every directly and charges the estimate. With interval estimators of width this loses revenue of order per unit time when the inventory constraint binds (), because is then not the unconstrained maximizer of . The paper's (11) and (19) show the loss. The bound requires steering the total sales to within of the inventory, which is Lemma 8, and a second-order expansion of the revenue around that uses the first-order condition .
Formally, a further difficulty is the closed loop: the prices of a phase depend on the counts of earlier phases, and the counts are Poisson only conditionally, through the random time change .
All declarations live in the namespace PrimalDualPricing.Regret. Printed page numbers equal PDF page numbers in the cited preprint.
Fin M. Each satisfies Assumption 1 on and is otherwise any extension with ; the last-phase prices and can leave . encodes the choke price. and are fields carrying their optimality properties.IsPoissonProcess) with right-continuous, jointly measurable paths. The inventory of the -th system is units, and nothing is sold after the stock-out. Lemmas 6–8 use the uncapped sales of the paper's modified system (§4).A formalization that lets the policy read the true demand, measures regret against anything other than , ignores the stock-out in , or assumes the high-probability events of Lemma 5 would trivialize the goal; none of these is done here.
Contributions to the reusable parts are welcome: Poisson tails, the envelope theorem for , and the time-change construction of policy-driven Poisson sales.
Random matrices arise when observations, signs, or model coefficients fluctuate. Their spectral norm measures the largest amplification they can cause to a vector. A bound on that norm can turn entrywise randomness into a statement about the behavior of an entire linear operator. Tropp's chapter develops a common framework for Gaussian and Rademacher sums of fixed matrices, then applies it to Wigner matrices, rectangular Gaussian matrices, random signs, Toeplitz matrices, and a rounding scheme for a quadratic optimization relaxation (Tropp, Chapter 4). The applications show what the general estimate says when the matrices have concrete structure.
The chapter's general matrix-series theorem, Theorem 4.1.1, is already an open statement in tc's Prove2Me Chapter 4 mission. This mission targets the squared-norm comparison in §4.1.2 and the worked consequences that are not part of that existing goal. They are useful benchmarks because their dimensions, coefficients, and variance statistics are explicit. The existing platform status is a formalization status: Tropp proves these mathematical bounds in the cited book; the Chapter 4 theorem and the results proposed here do not yet have machine-checked proofs.
Fix positive integers and a finite family of complex matrices . Let be independent standard Gaussian real variables, each with mean zero and variance one. Their matrix Gaussian series is . For a complex matrix , write for its conjugate transpose and for its Euclidean operator norm. The matrix variance statistic is
For this Gaussian series, the two expected products equal the corresponding sums of coefficient products, so can be computed from the fixed . This is the same statistic and norm as Theorem 4.1.1, equations (4.1.2)–(4.1.4) (Tropp, p. 42). Expectations are entrywise Bochner integrals for matrix-valued functions and ordinary integrals for real quantities.
A Rademacher variable takes values and with equal probability. Some companion examples replace the Gaussian coefficients by independent Rademacher variables. For a Hermitian square matrix , denotes its smallest real eigenvalue. In the signed-entry example, the relevant matrix statistic is the larger of the greatest squared row norm and the greatest squared column norm of a fixed matrix.
The goal is the pair of inequalities in (4.1.7), together with explicit integrability of the random squared norm:
The constants and the logarithm are exactly those printed on pp. 43–44. The left side identifies a necessary scale; the right side gives a dimension-dependent upper estimate. The two milestones are the Jensen lower-bound display and the tail-integration display in §4.1.2. The latter is stated for any measurable matrix with the chapter's tail bound and positive variance, because the displayed integration step itself uses only those properties. It retains the exact split-point expression and the factor .
Companion statements record the minimum-eigenvalue consequences (4.6.4)–(4.6.5), the Wigner estimate (4.2.3), the rectangular Gaussian estimate (4.2.6), the randomly signed-entry estimate (4.3.3), the Toeplitz estimate (4.4.3), and the MaxQP rounding scale in §4.5. Their deterministic variance identities are part of the statements, rather than assumptions. In particular the Wigner bound keeps and the Toeplitz bound keeps the exact coefficient sum (Tropp, pp. 46–52).
The squared-norm comparison says that is the correct baseline for the size of a Gaussian series in mean square, while allowing a logarithmic penalty for matrix dimension. It also shows why an expectation estimate and a tail estimate answer different questions: the chapter discusses examples where a tail bound can be loose even when the expected norm is controlled (Tropp, pp. 44–45). The example statements make the abstract variance statistic usable for standard matrix ensembles and for signed matrices with prescribed entries.
A machine-checked development would connect the existing spectral and probability definitions to explicit examples, finite-sum variance identities, and integrability of Gaussian matrix norms. Those components can be reused in later sampling and numerical linear algebra missions. The general Chapter 4 matrix-series theorem remains an open platform target; these application statements are not claimed to be already formalized or proved there.
The central obstacle is moving from a tail estimate for to a finite, sharp expectation for . The tail estimate has a dimension factor, while the desired bound has its logarithm; an unspecialized bound at a single threshold does not provide the stated constant. At the modeling level, matrix variance uses expectations of matrix products, so it must coincide with the finite sums of coefficient squares for each example. A definition that silently returns zero for a nonintegrable Bochner integral would make the upper inequality misleading. The Gaussian law, measurability, and moment behavior therefore matter to the statement as well as to eventual proofs.
Matrices use Matrix (Fin d₁) (Fin d₂) ℂ with and tc's spectralNorm and rectSecondMoment definitions. The probability space is arbitrary; coefficient functions are measurable and independent, and their pushforward laws are exactly standard Gaussian or Rademacher as the page requires. Families may be empty. Real random coefficients scale complex matrices. Integrability of is a conclusion of the goal and tail-integration milestone, while the minimum-eigenvalue expectation companion likewise asserts integrability. The tail-integration milestone assumes because its displayed denominator divides by ; the Gaussian goal itself includes .
The Wigner coefficients are indexed by pairs ; rectangular and signed-entry coefficients by row-column pairs; Toeplitz coefficients by diagonals . The Toeplitz index in Lean is shifted to Fin (2*d-1). Row and column maxima range over the nonempty finite row and column sets. The signed-entry theorem permits complex fixed entries and uses ; the printed example starts with real entries. MaxQP uses the positive scale and tc's positive-semidefinite order for the two relaxation constraints. None of the coefficient-square identities is supplied as a hypothesis; each is a conclusion to establish.
Context. The existing TroppMatrixConcentration.ch4_matrix_series formalizes Theorem 4.1.1 and is Open. Its Gaussian/Rademacher variance identity and norm/tail bounds provide the chapter context. The present goal specializes the same Gaussian model and asks for the separate second-moment result (4.1.7). Reusable contributions include finite-matrix identities, Gaussian moment integrability, and tail-integration lemmas. A valid proof must preserve the actual standard laws and independence, and cannot redefine as the expected squared norm.
Learning theory asks whether a rule that fits an observed sample will also perform well on future observations. A class with many functions can fit accidental patterns in the sample, so its size and geometry affect the reliability of empirical risk estimates. Empirical Rademacher complexity measures this ability to fit noise: attach an independent random sign to each observed point, let the class choose its best function after seeing all signs, and average the resulting signed score. A smaller value supports tighter uniform generalization bounds. Orabona, §16.1, pp. 270–271
Online learning studies a different protocol. A learner chooses a prediction before each round's loss is revealed, and its regret compares its cumulative loss with that of a fixed competitor chosen in hindsight. Chapter 16 of Orabona's book connects these two quantities. The connection matters because an online algorithm's regret estimate can be used to control the statistical complexity of a class of predictors, even though the online game and the random-sign experiment are defined differently. Orabona, Theorem 16.4, p. 272
Fix a horizon and vectors . For each , let be an independent Rademacher sign, equal to or with probability one half each. Given a nonempty bounded set , define its linear class by
The empirical complexity on the fixed sample is
This is a finite expectation over the possible sign assignments. The supremum is over the same comparison set for every assignment; the chosen may depend on the signs. The book's general Definition 16.1 allows an arbitrary class of real-valued functions, while this mission uses its linear specialization from the discussion immediately preceding Theorem 16.4. Orabona, Definition 16.1 and §16.1, pp. 270–272
For the final bound, is the probability simplex . The supremum of a linear score over this simplex is the maximum of its coordinate scores. Write for a common bound on the infinity norm of the sample vectors, so for every round and coordinate. Orabona, Corollary 16.7, p. 273
The central target is Corollary 16.7, called Massart's Lemma in the book:
Its constant and dependence on and are part of the target. The result includes : in that case the expectation and the bound are both zero. Orabona, Corollary 16.7, p. 273
Two statements supply the chapter's route to this target. Theorem 16.4 says that if a nonanticipating online linear algorithm has worst-case regret at most for all loss vectors in a symmetric set , then for any sample in . The Exponentiated Gradient regret bound of §6.6 gives, on the simplex, for every simplex competitor . The milestone list quotes both source statements. Orabona, Theorem 16.4, p. 272; §6.6, p. 81
The goal supplies a sample-dependent complexity bound using only a coordinate bound, the number of coordinates, and the sample size. Its square-root dependence on explains why a simplex-indexed class can have much smaller complexity than a crude bound that scales directly with . In applications where a generalization estimate contains empirical Rademacher complexity, this result gives a concrete quantity to insert for a finite coordinate class. Orabona, §16.1, pp. 271–273
The mathematical statements are proved in the book. This mission asks for machine-checked proofs of the exact finite-sign formulation of the goal, the regret-to-complexity reduction, and the source's Exponentiated Gradient regret estimate. The local proposal currently contains statements with proof placeholders; it does not claim that these three items have already been proved in Lean. The resulting finite-sign and bounded-supremum definitions can also support other empirical-process arguments.
The reduction has to respect the order of the online game. A bound for a learner allowed to inspect the current random sign would not imply the same complexity estimate: it could choose its round- point using information that a genuine online learner lacks. The algorithm therefore needs a precise causality condition, as well as a regret guarantee that holds for every admissible gradient sequence. Orabona, proof of Theorem 16.4, p. 272
The simplex result also depends on the exact regret coefficient. A generic estimate does not recover the displayed constant. At the boundaries, real division and logarithms in Lean are total, so the statements must say when and are positive. The one-dimensional case is meaningful and must stay in the theorem.
Vectors are functions Fin d → ℝ, representing with its coordinate pairing. Samples, predictions and gradients use rounds ; index zero is unused. The random-sign expectation is an exact average over Boolean assignments, with no measure-theoretic integrability convention. Both Rademacher averages require . The signed linear supremum is real-valued and receives evidence that is nonempty and bounded. Theorem 16.4 also records the book's closedness hypothesis.
Theorem 16.4 formalizes deterministic online algorithms. The source permits internal randomization as well; that extension requires an independent probability model for the algorithm's random choices. The Exponentiated Gradient item represents losses by real-valued functions and requires the subgradient inequality on the simplex, where the book evaluates them. Its run predicate requires and includes the uniform initial point and coordinate update of Algorithm 6.2. The goal itself has no algorithm hypothesis. Its infinity-norm assumption is expressed as coordinate absolute-value bounds.
The definitions exclude an empty comparison class or an unbounded real supremum being silently assigned a default Lean value. A complete development needs finite-sign averaging identities, properties of real suprema over bounded sets, simplex geometry, and the regret analysis of Exponentiated Gradient. Contributions to these reusable components, to the two milestones, and to the goal are in scope. The PAC-Bayes and time-uniform concentration parts of Chapter 16 are reserved for separate work because they need different probability and measure-theory objects.
Online prediction compares the losses of a sequence of decisions with the losses of one fixed decision chosen after the sequence is known. A learner would like a regret guarantee that remains valid for every such competitor, even when the losses arrive in an arbitrary order. Exponentially weighted averaging is a way to make each decision from all feasible points rather than committing to one candidate early. The method gives the Weighted Average Algorithm (WAA) in Chapter 11 of Orabona's text. It is particularly effective when the exponential of each negative loss is concave, a condition called exp-concavity.
The chapter first compares WAA with a competing probability distribution. Theorem 11.5 turns that guarantee into a bound against an individual feasible point. That distinction matters when the benchmark is a concrete portfolio, parameter vector, or other fixed decision, rather than a distribution over decisions. The same chapter later extends the weighted-average viewpoint to mixable losses through the Aggregating Algorithm; this mission focuses on the earlier deterministic-comparator result.
The feasible set is a closed, bounded, convex, full-dimensional subset of , with . Its uniform distribution assigns a measurable subset probability equal to its Euclidean volume divided by . Because is bounded and full-dimensional, its volume is finite and positive. Rounds are , with . In round , the learner predicts , then observes a loss and pays . A competitor is fixed across all rounds. Its regret is
For a parameter , a real-valued loss is -exp-concave on if is concave on . Definition 7.31 in the source also permits a loss value of , with . The mission defines that extended-valued concept for Proposition 7.34 and uses real-valued losses in its WAA target. The weighted average in round is
Thus is the centroid of . This formula is Algorithm 11.1 with the uniform initial distribution and . The existing published EWOO point definition uses precisely this one-based formula, so the mission imports that object. The integrals are with respect to Euclidean Lebesgue measure.
The main target is Theorem 11.5, equation (11.6): for every ,
The target fixes the exact dimension, horizon, and exp-concavity dependence from the source. It applies to each fixed competitor, with no distribution chosen in the statement. The milestone list records three source claims in reading order. Proposition 7.34 says that exp-concavity implies convexity, including the book's extended-real convention. Two displays in the proof of Theorem 11.5 describe the translated, contracted set : the exponential losses there are bounded against those at , and its uniform-prior mass is . These are the chapter's explicit geometric and loss-comparison targets.
The theorem converts a distributional WAA guarantee into a bound for each deterministic competitor. Its dimension factor is , and its logarithm contains . This exact expression is sharper than replacing that logarithm by for ; the distinction is visible in the target statement. A related EWOO result with the weaker form is already represented in the platform's library, but it does not establish the bound selected here. The source theorem is proved in the book; the remaining work is a machine-checked proof of this statement and the geometric milestones, with the source's constants intact.
The formal development can also support later results on exponentially weighted prediction. Its reusable pieces are the definition of exp-concavity, the extended-real epigraph convention, and the volume identity for a translated scaling of a convex body. The WAA prediction itself is represented by a previously published definition, giving future results a common algorithmic object rather than another copy of the same integral formula.
The general WAA statement compares the algorithm with a probability distribution, whereas Theorem 11.5 compares it with a point . A point mass at is unsuitable as a comparator to a uniform continuous prior: it has no density with respect to that prior, so its relative entropy is infinite. The finite bound depends on identifying a region around that has positive uniform mass while retaining control of every exp-concave loss on that region. A formal treatment must also ensure that the weighted vector integral denotes an actual mean and that the normalization denominator is positive, rather than inheriting a default value from a total integral or division operator.
The state space is EuclideanSpace ℝ (Fin d), and a loss is indexed from round one; index zero is unused. The prior is uniform on , and the point played is the published one-based EWOO weighted mean. The hypotheses make the printed ratios meaningful. Closedness, boundedness, convexity, and positive volume express the source's full-dimensional convex-body setting. The theorem additionally records almost-everywhere measurability of each loss on , and integrability of each exponential weight and its vector moment; these are explicit analytic conditions for the real and Bochner integrals in Lean. They are not algorithmic restrictions or assumptions of the regret inequality's conclusion. Positive volume and integrability rule out a vacuous zero denominator or Lean's zero value for a non-integrable integral.
The source allows extended-real losses, but the goal uses real-valued losses on . Proposition 7.34 separately retains the full extended-real statement through WithTop ℝ: maps to zero under the exponential, and convexity is expressed by a convex epigraph. A complete proof needs the exp-concavity and Jensen facts, the weighted-mean properties on convex , the measure and volume properties of , and the distributional WAA inequality from the chapter. Contributions that supply these lemmas under the stated conventions are within scope. The prediction cannot be replaced by an arbitrary point of : the exact uniform-prior weighted mean is part of the goal.
A saddle-point problem asks one player to choose a decision that keeps a payoff small while another chooses a decision that makes it large. Such problems include two-player zero-sum games and constrained optimization written through a Lagrangian. Online convex optimization supplies a way to construct approximate saddle points from repeated play: each player responds to losses generated by the other's current decision. Chapter 15 of Orabona's textbook develops this connection and studies the resulting averages. The chapter's earlier online-to-saddle-point result gives a duality-gap certificate from the two players' regrets; §15.5 asks how the certificate improves when the payoff is smooth and both players use predictions of their next gradients.
The minimax equality for continuous convex-concave payoffs on compact convex sets is already a known mathematical result. Theorem 15.11 in the book is a case of Sion's minimax theorem, and a proved Sion theorem already exists in the platform library. This mission centers on the algorithmic rate in Theorem 15.26, which has a separate statement and a different role.
Let and be nonempty closed convex sets in finite-dimensional real normed spaces, with norms and . The payoff is real-valued, convex as a function of for fixed , and concave as a function of for fixed . The -player tries to minimize it; the -player tries to maximize it. A saddle point would be a pair whose coordinate minimizes the payoff against its coordinate and whose coordinate maximizes it against its coordinate.
The duality gap of a pair , when the extrema are attained, is . It is nonnegative and measures how far the pair is from the simultaneous best-response condition. For iterates indexed from through , the book evaluates this gap at the averages and .
Optimistic follow-the-regularized-leader, or optimistic FTRL, chooses each point by minimizing a regularizer plus all earlier linearized losses and a hint for the next loss. Algorithm 15.6 sets the hint equal to the previous observed partial gradient, starting with zero at round . The -player's observed linear functional is ; the -player's is . Their regularizers and have strong-convexity parameters and with respect to their respective norms. The norm of each partial gradient is the corresponding dual norm.
Smoothness here means that the partial gradients exist on an open neighborhood of and satisfy four Lipschitz inequalities. Changes in the coordinate affect the gradient by at most times the distance; changes in the coordinate affect it by at most times the distance. For the gradient the cross constant is again , and the own-coordinate constant is , exactly as in equations (15.7)–(15.10) of the textbook.
The goal is the exact finite-horizon inequality of Theorem 15.26. Fix and parameters satisfying and . For any minimizer of and maximizer of , the target is
The milestones are the linear-loss, fixed-regularizer instance of Theorem 7.47 used in the chapter, Theorem 15.12 relating player regrets to the averaged duality gap, and the explicit summed-regret inequality on page 262. Together they specify the algorithmic input, the conversion to a saddle-point certificate, and the exact stability coefficients in the goal.
The bound certifies the quality of the averaged pair after a specified number of rounds. When the regularizers are bounded on the feasible sets, its numerator is uniformly bounded and the gap is , as stated in the paragraph before Theorem 15.26. Without that further boundedness, the displayed inequality remains the theorem's finite-horizon statement, but its numerator can depend on through and . The mission name's “constant over ” describes the bounded-regularizer setting; the formal goal preserves the more general printed bound.
The book proves the theorem mathematically. The work here is a machine-checked representation of Algorithm 15.6, its smoothness assumptions, the exact parameter thresholds, and the finite-horizon inequality. The run and smoothness definitions can be reused for other optimistic methods in the chapter, including Theorem 15.28. Existing library results about minimax equality address existence and equality of optimal values; they do not supply the quantitative guarantee for this run.
A standard regret bound for each player leaves variation terms involving successive iterates. With two players, each player's gradient variation depends on both players' movement and on different norms. A bound that discards this coupling loses the displayed coefficients and the rate in Theorem 15.26. The formal statement therefore keeps both sequences, both dual norms, and all four smoothness inequalities visible. It also has to treat the first round separately: the previous-gradient hint is zero there, while later rounds compare two observed gradients.
The Lean development uses finite-dimensional real normed spaces; a partial gradient is a continuous linear functional and its operator norm is the book's dual norm. The payoff and regularizers are represented by real-valued functions on the ambient spaces, restricted to and when optimized. Smoothness includes an open set containing the feasible product. Strong convexity uses Mathlib's set-relative StrongConvexOn. The run predicate enforces both argmin updates, and index is used only for the zero hint. It constrains exactly the rounds . In the optimistic FTRL milestone, the look-ahead point is the minimizer of the regularized loss sum with a zero hint. The book's proof uses the hint of round there instead, which makes that milestone's first inequality false.
The goal assumes , positive , and nonnegative smoothness constants. These record the book's parameter conventions and keep every denominator meaningful. The extrema in the conclusion are represented by arbitrary attained minimizer and maximizer witnesses, matching the theorem's nonempty-argmin and nonempty-argmax hypotheses. No boundedness or compactness of or is imposed. An arbitrary sequence of feasible points cannot satisfy the goal: the optimistic FTRL argmin updates are part of the run hypothesis. Contributions that establish the two-player regret estimate, the regret-to-gap step, or the final inequality against this run model directly support the mission.
Many problems in machine learning and statistics have the composite form , where is a smooth loss and is a non-smooth regularizer such as . When is separable, , the method of choice at scale is often randomized proximal coordinate descent: at each step one coordinate is drawn at random and a one-dimensional proximal problem is solved in that coordinate only. Each step is cheap, and the method underlies standard solvers for -regularized regression and for the dual of support vector machines.
Classical linear-convergence guarantees for this method assume strong convexity of or of (Richtárik and Takáč, 2014), or rely on the Kurdyka–Łojasiewicz property with constants that are hard to make explicit. Karimi, Nutini and Schmidt (arXiv:1608.04636, ECML PKDD 2016) introduced the proximal-PL inequality, a generalization of the Polyak–Łojasiewicz condition to composite problems, and showed that it alone yields linear rates for proximal-gradient methods. Theorem 6 of that paper, the subject of this mission, extends the analysis to randomized proximal coordinate descent.
Timeline. Polyak (1963) and Łojasiewicz (1963) introduced the gradient-domination inequality for smooth problems. Nesterov (2012) analysed randomized coordinate descent for smooth convex problems; Richtárik and Takáč (2014) extended it to composite separable problems under strong convexity. Karimi, Nutini and Schmidt (2016) obtained the rate for the proximal coordinate method under proximal-PL alone (Theorem 6, p. 10, proof in Appendix H, p. 23).
Write for the Euclidean space with inner product and norm ; is the -th coordinate of , the -th basis vector, and the -th coordinate of the gradient. The data are:
For the quantity
measures the best decrease of a quadratic upper model of at . satisfies the proximal-PL inequality with constant if
The coordinate-wise proximal-gradient method starts at . At step it draws uniformly from , independently of the past, and sets , where minimizes
For every ,
The constant is the paper's; no further constant is fixed.
A companion statement (not a milestone, not in the paper) asserts that the one-dimensional step (16) exists for convex and .
The result. Theorem 6 gives a linear rate for proximal coordinate descent on every composite problem satisfying proximal-PL, a class that contains -regularized least squares and other problems that are not strongly convex. The rate matches that of plain randomized coordinate descent under PL (Theorem 3 of the paper) with the composite term added, and the factor is the usual price of updating one coordinate per step.
Formalizing it. The result is proved on paper; no machine-checked proof is known. A formal proof requires the coordinate descent lemma, the exchange of a separable minimum with a sum, and an exact accounting of the expectation over random index sequences. The definitions of , proximal-PL and the random-coordinate run built here are reusable for other proximal and coordinate methods.
The one-step argument is short once the expected-improvement identity is available; the difficulty is in that identity. Its left side averages over coordinates the minima of one-dimensional models, while is a minimum over the whole space. Equating them requires that the full-space minimum split across coordinates, which is where separability of is used, and that each minimum be attained, which requires convexity of the and . A second point is the expectation: the iterate after steps is a function of the whole index word , and the one-step expected descent must be propagated through the tower of conditional expectations to the -step bound.
EuclideanSpace ℝ (Fin d) with (0 < d); the gradient is Mathlib's gradient f, and is gradient f x i.Differentiable ℝ f, as in the setup of Theorem 5. Appendix H uses only coordinate-wise Lipschitz continuity, which follows.Contributions welcome: proofs of the three milestones and the goal, the existence of the coordinate step, and a version with extended-valued .
In online learning with bandit feedback, the learner chooses one action and sees only that action's loss. This is the information pattern of sequential trials in which testing one option does not reveal the outcomes of the others. The learner must keep its cumulative loss close to that of a good fixed action while learning which actions are good. A full-information method can update from every arm's loss each round; here the unseen losses have to be handled through the observations the learner actually receives. Chapter 9 of Orabona's text develops this distinction for multi-armed bandits.
Two environments are treated in the chapter. With an oblivious adversary, all losses are fixed before play, although the learner does not know them. With a stochastic environment, each arm has a fixed loss distribution and new losses are drawn across rounds. An algorithm with a guarantee in both environments does not need to be told which generated its data. Theorem 9.17 gives such a pair of guarantees for the FTRL version of Tsallis-INF, using the precise constants stated in the pinned version of the book.
There are arms and rounds, numbered . In round , the learner forms a probability vector on the simplex , draws an arm with probability of choosing , and observes only . The loss of an unchosen arm is not revealed. For an oblivious adversary, the entire table is deterministic and the expectation is over the learner's draws.
Algorithm 9.6 uses the importance-weighted estimate if , and otherwise. Its Tsallis-INF FTRL prediction minimizes, over ,
The minimizer has positive coordinates. Thus each denominator used by the estimator is positive. In the stochastic environment, arm has mean ; if is a best arm, its gap is . The pull count is the number of rounds through in which arm is selected. Stochastic pseudo-regret compares the learner's expected loss with , the expected loss of always playing the best arm.
The mission's main theorem is the adversarial claim of Theorem 9.17, p. 165. For every fixed comparator arm and losses in ,
Taking to be the best arm in the fixed loss table yields the stated adversarial regret bound. The companion item formalizes the second claim of the same theorem: if the losses are stochastic with a unique best arm and , then
The milestone list contains the chapter's pseudo-regret decomposition (Lemma 9.10), its sub-Gaussian sample-mean bound (Corollary 9.9, reused from an existing formal statement), and the probability-sensitive Tsallis-INF inequality (9.8). These are distinct mathematical claims rather than alternate names for the final bound.
The adversarial bound grows like and remains valid for any fixed bounded loss table. The stochastic bound instead measures the difficulty of distinguishing arms through the positive gaps and grows logarithmically with the horizon for fixed gaps. Both refer to the same FTRL update and the same importance-weighted estimator. The finite-horizon constants and are part of the target, not unspecified factors hidden in asymptotic notation.
Both claims are proved in the book. The work here is to give their hypotheses, random experiment, and algorithm a machine-checkable Lean interface, then formalize the known arguments. At this drafting stage the theorem bodies are open Lean problems; a successful build checks that their statements are well formed, not that the regret bounds have been proved. The resulting finite-history bandit protocol and stochastic pseudo-regret definitions can also support other loss-based bandit algorithms. The existing formalized sub-Gaussian tail bound can be reused for concentration results elsewhere in the chapter.
The learner observes only one coordinate, while regret is measured against losses across all arms. The importance-weighted estimate corrects the missing observations in expectation, but its size can grow when a selected arm has small probability. Consequently, a bound based only on a uniform estimate of its magnitude loses the probability dependence needed for the theorem's constants. The stochastic claim adds another difficulty: the learner's choices depend on past observed losses, so a current loss must be related to a random pull count without letting the choice depend on that current loss.
There are two tempting but invalid shortcuts. Permitting to inspect would change the bandit protocol, and taking an expectation under an arbitrary path measure would no longer describe the arm draws of Algorithm 9.6. The formal statements tie each prediction to its FTRL objective and each path probability to the predictions made along that history.
Arms are Fin d; the main theorem permits , where both its regret and bound are zero. Rounds retain the book's indexing. A finite path has a dummy coordinate zero, fixed to an arbitrary anchor arm; this coordinate is never played or scored. The adversarial losses are a fixed table, selected before any draw. A path has probability equal to the product of the algorithm's conditional arm probabilities, and regret against a fixed arm is a finite weighted sum over paths. The FTRL run predicate requires simplex membership, strict positivity, minimization against every simplex point, and dependence only on past arm choices. The last two properties specify the intended update on every possible history.
The stochastic model first samples a loss table from a probability measure and then draws an arm path conditionally using the same Algorithm 9.6. Current-round loss vectors are independent across rounds, while coordinates within one round need not be independent. Each arm has the same mean in every round. The policy is a measurable function of the observed history (past arms and their losses); its expected loss is explicitly integrable. Loss bounds are imposed on every outcome in the chosen sample space, which can be taken as the support of bounded distributions. The stochastic statement adds to make the logarithmic formula's domain explicit, and the unique-best-arm assumption ensures every denominator in the displayed sum is positive. Lemma 9.10 also spells out the integrability of its means and pull counts.
The development needs finite probability laws, real integrals, simplex geometry, and properties of the square-root regularizer. The independent tail bound for sample means is already available as a referenced theorem. Contributions that establish existence and interiority of the FTRL minimizer, the normalization of the path law, or the stated regret inequalities fit this scope. A choice rule that sees the current loss, a path law unrelated to , or a zero integrability default does not satisfy the intended bandit model.