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.
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?
Prove Lieb’s concavity theorem (Theorem 8.1.1, also stated as Theorem 3.4.1): for fixed Hermitian H, the function A ↦ tr exp(H + log A) is concave on positive-definite matrices. This is the deterministic foundation of Chapter 3’s probabilistic argument.
Milestones follow the book’s route through generalized Klein, relative-entropy nonnegativity, variational trace formulas, operator Jensen, matrix perspectives, and joint convexity of relative entropy. Logarithm and trace-exponential monotonicity are included as reusable comparisons. The domain allows noncommuting positive-definite matrices without trace normalization.
Source: Tropp, January 2015 version, Chapter 8. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Control the spectral norm of a matrix series with independent standard Gaussian or Rademacher coefficients. The goal is Theorem 4.1.1, including its variance identity, expected-norm estimate, and tail bound for rectangular complex matrices.
Milestones are the Gaussian and Rademacher matrix mgf/cgf estimates (Lemmas 4.6.2–3) and the Hermitian series bound (Theorem 4.6.1). The formulation keeps the source’s constants, both coefficient laws, and the zero-variance case. The shared Chapter 3 tools connect these transform estimates to concentration.
Source: Tropp, January 2015 version, Chapter 4. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Replace ambient matrix dimension by intrinsic dimension, the ratio of trace to spectral norm. The goal is intrinsic Matrix Bernstein (Theorem 7.3.1). Intrinsic Matrix Chernoff (Theorem 7.2.1) is a second major target within the mission.
Supporting milestones include the generalized Laplace bound, intrinsic-dimension trace estimate, block-diagonal identities, Hermitian Bernstein, and the expected-norm corollary. The statements retain the source’s constants, threshold restrictions, and matrix-valued mean or variance bounds. Nonzero proxies keep intrinsic dimension well-defined; the expectation constant is universal.
Source: Tropp, January 2015 version, Chapter 7. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Control the spectral norm of a sum of independent, centered, bounded rectangular random matrices. The goal is Matrix Bernstein (Theorem 6.1.1), including the variance identity and both expected-norm and tail estimates.
Milestones cover Hermitian dilation, variance additivity, the bounded-summand mgf/cgf estimate (Lemma 6.6.2), and Hermitian Bernstein (Theorem 6.6.1). Chapter 3 supplies the general Laplace-transform machinery. The formulation uses the Euclidean operator norm, preserves the one-sided eigenvalue assumption in the Hermitian result, and includes deterministic zero sums.
Source: Tropp, January 2015 version, Chapter 6. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Bound the extreme eigenvalues of a sum of independent positive-semidefinite random matrices. The goal is the complete Matrix Chernoff theorem (Theorem 5.1.1): both expectation estimates, both tails, and the identities for the mean’s extreme eigenvalues.
The supporting milestone is the matrix mgf/cgf estimate (Lemma 5.4.1); Chapter 3 supplies the master bounds. The Lean statement retains the different lower- and upper-tail deviation ranges, permits zero mean eigenvalues, and handles a zero summand bound explicitly.
Source: Tropp, January 2015 version, Chapter 5. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Develop the reusable matrix Laplace-transform method behind Tropp’s concentration inequalities. The goal is Theorem 3.6.1: upper and lower tail and expectation bounds for sums of independent Hermitian random matrices, expressed through their matrix cumulant-generating functions.
Milestones cover the eigenvalue tail and expectation bounds (Propositions 3.2.1–2), probabilistic Lieb inequality (Corollary 3.4.2), and trace-cgf subadditivity (Lemma 3.5.1). This mission also supplies the series’ shared spectral, probability, and dilation definitions. Lieb’s underlying concavity theorem is the Chapter 8 goal.
The Lean statements give bounds for each admissible transform parameter, with explicit integrability hypotheses; optimization recovers the source’s infimum/supremum forms.
Source: Tropp, January 2015 version, Chapter 3. Lean statements compile; proofs remain open.
Coordinate descent methods update one block of variables at a time. They are the method of choice when the number of variables is so large that even one full gradient is too expensive, while a single partial derivative is cheap: support vector machines, -regularized regression, and large sparse least-squares problems are the standard examples. Yu. Nesterov's paper Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012), doi:10.1137/100802001) gave the first global efficiency estimates for randomized coordinate descent, and these estimates started a large literature on random coordinate and block methods.
Many applications carry simple constraints on each block: bounds on each variable, a simplex or a ball per block. Section 4 of the paper shows that randomized coordinate descent handles such block-separable constraints at no loss: a projected block step, chosen uniformly at random, enjoys the same expected rate as the unconstrained method, and a linear rate under strong convexity. This mission formalizes that result, Theorem 5.
The space is split into blocks, with and every . A point is the family of its blocks , and is the point whose -th block is and whose other blocks are zero. Each block carries a Euclidean norm with (3.4).
The objective is convex and differentiable, and its gradient is coordinate-wise Lipschitz (2.2): writing for the -th block of the gradient, there are constants with
The weighted norm is (3.5). The function is strongly convex in with constant if for all (3.1).
The problem is (4.1), with and each nonempty, closed and convex. Its optimal value is , attained at an optimal solution . The constrained coordinate update (4.2) is
The uniform coordinate descent method UCDM (4.5) draws uniformly from and sets . Its expected objective is , the expectation over . The level-set radius is the largest -distance between a feasible with and an optimal solution.
For every ,
and, if is strongly convex in with constant ,
The result. Theorem 5 shows that the cost of a constrained problem with separable constraints is, up to the projection onto each , the cost of the unconstrained one: block steps for accuracy , and under strong convexity. The method needs no knowledge of ; the same iteration attains whichever rate applies. The Lyapunov function of (4.7) needs no level-set argument, so it applies wherever the projected step is cheap.
Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any rate for a randomized constrained coordinate method, appears in the Prove2Me catalogue or in Mathlib. The Prove2Me catalogue holds Bubeck's scalar, unconstrained random coordinate descent results (ConvexOptAlg.CoordDescent.*) and the deterministic Tseng–Yun coordinate gradient descent; neither covers a projected block step. A formalization produces the first verified rate for a randomized method with constraints, and a reusable model of block-structured spaces, block projections and expectations over random index sequences.
The unconstrained analysis of the paper (Theorem 1) bounds the distance to the optimum by a level-set radius and uses the decrease of a gradient step. Neither carries over: with constraints the gradient at the optimum need not vanish, so the decrease of a projected step is not controlled by the gradient norm, and the unconstrained recursion is not available. A different potential is needed, and its one-step estimate (4.7) is the central milestone. For the linear rate, the contraction factor must be shown nonnegative without assuming , which is where footnote 2 enters.
is the dependent product Blocks E , each a finite-dimensional real inner product space whose inner product is the paper's . Indices are 0-based. The dual norm is the operator norm of linear functionals, and is the Fréchet derivative of composed with the block inclusion. Random draws are explicit index sequences, so is the finite average of over all sequences of draws; no measure theory is involved.
Explicit choices where the paper is silent:
A formalization in which the update is an arbitrary point of or an unprojected gradient step, the draws are not uniform, or is the unconstrained minimum, proves a different theorem and is ruled out by the definitions above.
Needed infrastructure: existence and the variational characterization of the minimizer of a strongly convex quadratic over a closed convex set (Mathlib has projections onto closed convex sets in Hilbert spaces), the block descent inequality (2.3) obtained from (2.2), and manipulation of the finite expectations over index sequences (conditioning on the last draw). The block model, the weighted norm and the expectation are shared with the other missions of this series. Proofs of the milestones, and of (2.3) as a supporting lemma, are welcome.
Sums of independent random matrices appear wherever a large matrix is built from random pieces: sample covariance matrices in statistics, random sparsification and sampling in numerical linear algebra, random graphs and their Laplacians, and compressed sensing. The basic question is how far the largest eigenvalue of such a sum can stray above its typical value. For sums of independent real random variables the answer is given by the classical inequalities of Chernoff, Hoeffding and Bernstein, all derived by the Laplace transform method: bound the tail by the moment generating function, and use independence to factor the moment generating function of the sum.
Ahlswede and Winter (2002) showed that a matrix analogue of the Laplace transform method exists, and Oliveira (2010) refined the starting inequality. Tropp's paper (arXiv:1004.4389) replaced the Ahlswede–Winter decoupling step by a consequence of Lieb's concavity theorem (Lieb 1973) and obtained a single master tail bound from which matrix versions of the Gaussian-series, Chernoff, Bernstein and Azuma inequalities follow with sharp variance parameters. This mission formalizes that master bound, the first of five missions covering the paper.
Timeline:
All matrices are arrays of complex numbers with . A matrix is self-adjoint (Hermitian) when ; it then has real eigenvalues, and denotes the largest one. For a function and a self-adjoint with unitary and diagonal, . This defines the matrix exponential of every self-adjoint matrix and the matrix logarithm of every positive-definite matrix, with . The trace exponential is .
A random self-adjoint matrix is a measurable map from a probability space to the self-adjoint matrices. Its expectation is the matrix of the expectations of its entries. A finite sequence is independent when the maps are jointly independent. The matrix moment generating function and matrix cumulant generating function of are
which may fail to exist for some . In the Lean development these objects are lambdaMax, mexp, mlog, trExp and mean in the namespace MatrixTail.Master.
For independent random self-adjoint matrices and every ,
It contains no constants and no assumption beyond independence: every later inequality of the paper specializes it.
The master bound reduces every tail estimate for of an independent sum to semidefinite bounds on the individual cumulant generating functions. The paper's matrix Gaussian and Rademacher series bound, matrix Chernoff inequality and matrix Bernstein inequality are each one such bound away from it, and the matrix Bernstein inequality in particular is a standard tool in randomized numerical linear algebra, matrix completion and covariance estimation. Missions II–IV of this series take the master bound as their first milestone.
All results here are proved in the literature. What remains is formalization: none of Lieb's concavity theorem, the matrix Laplace transform bound or the subadditivity of matrix cumulant generating functions is in Mathlib, and a machine-checked Lieb theorem would be reusable throughout quantum information theory (strong subadditivity of entropy, joint convexity of relative entropy).
The scalar argument factors , which needs . For non-commuting matrices , so this step fails. The Golden–Thompson inequality handles two summands but its three-matrix analogue is false, so it does not iterate. Lieb's concavity theorem is the deep input; it does not follow from elementary properties of the exponential, which is neither operator monotone nor operator convex. On the formal side, the matrix functional calculus of Mathlib carries little of the trace-function theory the statements rely on.
Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d] wherever appears; for the largest eigenvalue would be and the bound would fail at . Exponential and logarithm are Mathlib's continuous functional calculus cfc. Random matrices are measurable maps for the Borel σ-algebra on the entries, independence is iIndepFun, and P is a probability measure. Expectation is entrywise.
The paper's standing assumption that expectations exist is made explicit and only where an expectation is taken: every entry of is integrable for the in question. The infimum over is stated as the bound for every at which the moment generating functions exist; since an inequality is equivalent to for every , and the paper treats a non-existent moment generating function as , this is exact. A real-valued infimum over , or dropping the integrability hypotheses, would make the statements trivially true through Lean's default values ( of an unbounded set and the integral of a non-integrable function are ); the formalization rules both out.
Useful infrastructure beyond this mission: trace inequalities for cfc on Hermitian matrices, monotonicity of the trace exponential in the semidefinite order, and Lieb's concavity theorem itself. Contributions of any of these as standalone lemmas are welcome.
In city logistics, goods often cannot be carried by large trucks all the way to the final customers. A common design routes the goods through intermediate depots, called satellites: large first-level vehicles carry freight from a central depot to the satellites, and small second-level vehicles deliver it from the satellites to the customers. The two-echelon capacitated vehicle routing problem (2E-CVRP) asks for the cheapest such two-level distribution plan. It contains the capacitated vehicle routing problem as a special case (a single satellite), and the location-routing problem can be reduced to it.
Exact methods for problems of this kind rest on lower bounds: a branch-and-bound or enumeration scheme can discard a partial solution only when it has a certified bound above the best known cost. Baldacci, Mingozzi, Roberti and Wolfler Calvo (Oper. Res. 61(2), 2013) built an exact algorithm for the 2E-CVRP on a chain of relaxations of a set-partitioning formulation . Its first link is a Lagrangean relaxation and a further relaxation , a multiple-choice knapsack problem solved by dynamic programming. Its optimal value, maximised over the penalties, gives the lower bound that drives the rest of the method. This mission formalizes the statements that make a valid bound.
An instance has a depot , satellites and customers , a symmetric cost matrix (with the vehicle fixed costs already added to the depot–satellite and satellite–customer entries), positive integer demands with total , first-level vehicles of capacity , second-level vehicles of capacity at satellite , a global limit on second-level vehicles, satellite capacities and handling costs per unit.
A first-level route leaves the depot, visits a set of satellites and returns; its cost is the cost of this closed walk. A second-level route is a simple cycle from satellite through a set of customers of total demand ; its cost is the cost of the cycle plus . In formulation , binary variables and select the routes and integers give the amount that route delivers to satellite . The constraints require that every customer is served exactly once (2), that the vehicle limits , , hold (3), (4), (6), that satellite capacities hold (5), that each satellite receives what its routes deliver (7), and that first-level capacities hold (8).
Relaxation removes (2)–(4) with penalties , , , and replaces the second-level routes by marginal costs of serving customer from satellite , subject to
where counts the visits of route to customer . Its variables are an assignment of customers to satellites and the first-level variables , .
Relaxation chooses for every first-level route at most one load in the interval of integers, so that the loads add up to . A route with load costs , where is the optimum of a continuous knapsack problem that serves demand at the cheapest marginal costs . Both objectives carry the constant .
For every satisfying (12), every , every , , and every feasible solution of with cost ,
The bound is the first lower bound of the paper's exact method. The configuration enumeration of its §5 and the reduced-cost elimination of second-level routes both use it as a certificate: a configuration or a route is discarded only when this bound shows that no cheaper solution contains it. If the bound were invalid, the method could discard the optimum. Theorem 4 provides, at every step of the paper's subgradient procedure, a to which the bound applies.
The paper's proofs are in an electronic companion. As printed, Theorem 3 () is false: does not limit a satellite's load by its fleet capacity , whereas the loads of are capped by it. A small instance with one satellite and two unit-demand customers, and has finite and . The bound (23) is nevertheless true, because the solutions that come from feasible solutions of respect the fleets. A machine-checked version pins down exactly which hypotheses the chain needs, including the positivity of demands, without which (23) fails. None of these results has been formalized before.
Theorems 1, 4 and Corollary 1 are bookkeeping with sums over routes, customers and satellites. The substantive step is the corrected Theorem 3. A solution of assigns whole customers to satellites, while sees each first-level route only through its total load and a continuous knapsack. The two descriptions have to be related, and that relation must respect every side condition of : the knapsack bounds , the load window (whose lower end depends on the vehicle count ) and the fleet cap . The obvious route, comparing the optimal values and directly as the paper states, does not work: the inequality between them is false, and the fleet condition is what has to be carried from .
Satellites are Fin ns, customers Fin nc (0-based). Demands are positive integers; capacities, fleet sizes and loads are natural numbers, and costs are real. Binary variables are Bool and integer variables ℕ. The route families and are arbitrary finite families of routes (nonempty, no repeated vertex, second-level loads at most ), not necessarily all routes as in the paper; every statement holds in this generality. Route costs are computed along the closed walk, so costs . The triangle inequality is not assumed. Optimal values , and are infima in EReal, equal to on infeasible problems, and comparisons with an upper bound are written with instead of . Where the paper writes "optimal solution of cost below ", the statements cover every feasible solution below any real .
The formalization cannot be trivialized: every optimal value is an infimum over the feasible set of the paper's own problem, so it equals , not , when that set is empty. The hypotheses of each theorem are satisfiable, which is checked on explicit small instances. The definitions of the instance, , and are written in the shape shared by the other missions of this series. Proofs of any milestone and reusable lemmas on finite sums over route families are welcome.
Coordinate descent methods update one block of variables at a time. For problems with millions or billions of variables, where even one full gradient is too expensive to compute or store, a step that touches a single block can be orders of magnitude cheaper than a full gradient step. Nesterov's Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012) 341–362, doi:10.1137/100802001) gave the first global complexity bounds for randomized coordinate descent on smooth convex functions: choosing the block at random makes the expected progress per step comparable to that of a full gradient step divided by the number of blocks.
Section 5 of the paper asks whether the multistep acceleration of the full gradient method (Nesterov 1983) carries over to the randomized coordinate setting, and answers it with the accelerated coordinate descent method ACDM. This mission formalizes that answer: Theorem 6, the expected rate of ACDM, together with the lemmas of its proof.
Timeline. Nesterov (1983) introduced the accelerated full-gradient method with rate . Nesterov (CORE DP 2010/2; SIAM J. Optim. 2012) proved the rate of random block coordinate descent and the rate of its accelerated variant ACDM. Later work (Lee and Sidford 2013; Fercoq and Richtárik 2015, arXiv:1312.5799; Allen-Zhu, Qu, Richtárik and Yuan 2016, arXiv:1512.09103) made the accelerated scheme efficient per iteration and sharpened its constants.
The space is , split into blocks. A point has blocks , and is the point whose -th block is and whose other blocks vanish. Each block carries a Euclidean norm with .
The objective is convex and differentiable, and has a coordinate-wise Lipschitz gradient: the partial gradient satisfies with constants . The method weighs blocks by these constants through the norm
The function is strongly convex in this norm with parameter if for all ; is plain convexity. A point minimizes , and .
The optimal coordinate step is , where maximizes . ACDM keeps two sequences with and deterministic scalars , . At step it computes from , sets and , forms , draws a block uniformly at random, and updates
, . The quantity is the expectation over the first draws.
For every , with ,
and, when ,
The result. Theorem 6 shows that randomized coordinate descent can be accelerated: the expected error falls as instead of the of the plain method, so after iterations (about full-gradient equivalents) the error is , the rate of the accelerated full-gradient method. For the same scheme converges linearly with a ratio governed by rather than . This is the starting point of the accelerated randomized coordinate methods (APPROX, NU-ACDM, accelerated proximal coordinate gradient) now used in large-scale machine learning.
Formalizing it. The theorem is proved in the paper; to our knowledge neither it nor any accelerated coordinate method has a machine-checked proof. The Lean development pins down a scheme whose correctness rests on a delicate parameter identity and on several conventions left implicit in the text (the range of , the reading of (5.3) at ).
The plain coordinate descent analysis tracks alone and fails to accelerate: one coordinate step gains only of a full gradient step, and a momentum term built naively from coordinate steps does not keep the expected progress. The accelerated proof needs a potential mixing the function gap with a squared distance , weighted by the deterministic sequences and ; the weights must make the cross terms in and cancel exactly after taking the expectation in the drawn block, which is what the coupled choice of achieves. The second difficulty is quantitative: the growth of follows from coupled recursions for and , not from a closed form.
Blocks E, the dependent product of finite-dimensional real inner-product spaces E i over Fin n (indices ); is absorbed into the inner product of E i. The dual norm is the operator norm of E i →L[ℝ] ℝ.Fin k → Fin n; and are finite averages over all sequences with weight . No measure theory is needed.Blocks, partialGrad, CoordLipschitz, coordStep, wnorm, expect) is shared verbatim with the other missions of this series. The coefficient lemmas (5.2), (5.4), (5.5) and the growth bounds are pure real analysis and welcome as standalone contributions; so is a Lean proof of the block descent inequality (2.3)–(2.4) for Euclidean blocks, which the potential inequality needs.ConvexOptAlg.NesterovSmooth.theorem_3_19). https://arxiv.org/abs/1405.4980Many problems in signal processing, statistics and machine learning ask for a minimizer of a smooth loss among vectors with few nonzero entries: compressed sensing with a nonlinear measurement model, sparse regression with a non-quadratic loss, sparse phase retrieval. The common abstraction is the sparsity constrained problem
where is continuously differentiable but not necessarily convex. The constraint set is a finite union of linear subspaces, so (P) is nonconvex and in general NP-hard, and its solutions are not characterized by the classical KKT theory.
Beck and Eldar (SIAM J. Optim. 2013, arXiv:1203.4580) introduced a hierarchy of necessary optimality conditions for (P) and matched each condition with an algorithm whose limit points satisfy it. Iterative hard thresholding (Blumensath and Davies 2008) reaches -stationarity for ; the greedy sparse-simplex method reaches coordinate-wise minimality, but each of its iterations calls up to one-dimensional minimizations. This mission formalizes the paper's compromise between the two: the partial sparse-simplex method, which examines only two candidate moves per saturated iteration, and whose limit points are -stationary.
Vectors live in with the Euclidean norm; is the -th unit vector. For :
The objective is continuously differentiable and bounded below (Assumption 1, standing throughout the paper). Assumption 2 asks that be Lipschitz with some constant . A constant satisfies the local Lipschitz condition (2.15) if for every pair , every and every supported in ,
The paper's local Lipschitz constant satisfies it, and .
The projection is the set of points of nearest to . For , a point is an -stationary point (Definition 2.3) if
The partial sparse-simplex method (p. 25) starts at . If , it moves to the best point over all and if that strictly decreases , and stops otherwise. If , it compares two candidates and takes the better one, preferring the second on ties:
Under Assumption 2, with satisfying (2.15), every accumulation point of a sequence generated by the partial sparse-simplex method satisfies
that is, is an -stationary point.
The theorem shows that a cheap index-selection rule does not cost optimality strength relative to iterative hard thresholding: every limit point satisfies , and since , this is a stronger necessary condition than the guaranteed by IHT with stepsize . In the paper's numerical comparison (Example 3.3 contd., Table 3) the method performs much better than IHT and only slightly worse than the greedy method, at a fraction of the greedy method's cost per iteration. The decrease estimates of Lemma 4.1 are the quantitative content: they turn each iteration into a lower bound on the objective decrease in terms of the violation of -stationarity.
The results are proved in the paper; to our knowledge none is machine-checked. This mission produces a formal model of the method (with its selection rules as inequality predicates, so every run is covered), the local descent lemma for two-sparse directions, and a checked proof of Theorem 3.4. The printed proof of the case contains two gaps (see Difficulty); a formal proof settles the argument.
The decrease estimates follow from the local descent lemma applied at well-chosen trial points, but passing to the limit is delicate. When , the supports of the subsequence eventually coincide with and becomes continuous there; when , the iterates along the subsequence may still have nonzeros, and does not by itself force , because kills the second term of . The swap move optimizes along a single off-support coordinate , chosen by the derivative at and not at the shifted point where the optimization happens. The printed display (4.19) claims the bound for the maximum over all of at the shifted point, which the argument does not give, and the final display takes a minimum of two bounds that each hold on only one class of indices. Theorem 3.4 itself is not affected, but a complete proof cannot follow those two displays as printed.
Lean works in EuclideanSpace ℝ (Fin n) (indices ), with of class and = gradient f. Conventions fixed by the formalization:
LipschitzWith Lf (gradient f)) are hypotheses.MapClusterPt xstar atTop x.The run predicate is satisfiable and does not force a STOP: on , , , the constant sequence at is a run. The conclusion is the projection condition itself, not the coordinate form (2.5), so it cannot be met by an empty or degenerate reading of stationarity.
Reusable parts: the local descent lemma for two-sparse directions, Lemma 2.2 (the coordinate characterization of , shared with the IHT mission of this series), and the order statistic . Contributions of proofs for any milestone are welcome, as is the companion result Lemma 3.3 (limit points are BF vectors without Assumption 2).
Many problems in signal processing, statistics and machine learning ask for a minimizer of a smooth loss among vectors with few nonzero entries: compressed sensing with a nonlinear measurement model, sparse regression with a non-quadratic loss, sparse phase retrieval. The common abstraction is the sparsity constrained problem
where is continuously differentiable but not necessarily convex. The constraint set is a finite union of linear subspaces, so (P) is nonconvex and in general NP-hard, and the classical optimality theory (KKT conditions, convex duality) gives no usable characterization of its solutions.
Beck and Eldar (SIAM J. Optim. 2013, arXiv:1203.4580) replaced that missing theory with a hierarchy of necessary optimality conditions of increasing strength, and matched each condition with an algorithm whose limit points satisfy it. This mission formalizes the comparison between the two strongest conditions of that hierarchy: coordinate-wise minimality and -stationarity.
Vectors live in with the Euclidean norm. For :
The objective is continuously differentiable and bounded below (Assumption 1). Assumption 2 asks that be Lipschitz with some constant .
The local Lipschitz condition (2.15) with constant asks that for every pair , every and every supported in ,
where . The paper's local Lipschitz constant satisfies it, and , often by a large factor.
A point is a basic feasible (BF) vector (Definition 2.1) if when , and on when .
A point is a coordinate-wise (CW) minimum (Definition 2.4) if either and for every and every (Case I), or and
(Case II): no swap of a support coordinate for any coordinate, with any value, decreases .
Every CW-minimum of (P) satisfies
that is, is an -stationary point. The constant multiplies exactly.
Optimality conditions for (P) matter because no efficient algorithm finds a global minimizer; what algorithms can guarantee is a limit point satisfying some necessary condition, and the strength of that condition is the guarantee. The paper's hierarchy runs: optimal CW-minimum -stationary -stationary for BF vector. Theorem 2.4 is the step that ties the coordinate-wise notion, which needs no Lipschitz constant to state, to the stationarity notion behind iterative hard thresholding. Combined with "every optimal solution is a CW-minimum", it shows that every optimal solution of (P) is -stationary, with the local constant instead of . It is the reason the greedy and partial sparse-simplex methods of the same paper, whose limit points are CW-minima or -stationary, are at least as strong as iterative hard thresholding.
The result is proved on paper. To our knowledge none of these notions (BF vectors, CW-minima, the local Lipschitz constant, the local descent lemma) has a machine-checked formalization. The mission produces a formal statement of the hierarchy's central step together with reusable definitions of the sparse-optimization objects, which the companion missions on the same paper (iterative hard thresholding, the greedy and partial sparse-simplex methods) state their results against.
The local descent lemma has no proof in the paper ("it is not difficult to see"). The global descent lemma integrates the gradient along the segment and applies the global Lipschitz bound; the local version must instead observe that along a direction supported on two coordinates only the two corresponding gradient components enter, and that the restricted Lipschitz bound (2.15) controls exactly those. Formally this requires the integral form of the mean value theorem for functions on a Euclidean space, together with the bookkeeping that stays in the class of perturbations allowed by (2.15).
In Theorem 2.4 the natural first attempt, perturbing a single zero coordinate and comparing with , fails when : the perturbed point has nonzeros and is infeasible, and Case II of the definition only compares with points obtained by swapping a support coordinate out. The bound on must therefore be extracted from swaps alone, and the degenerate case breaks the printed identity in the paper's chain (2.18).
All statements are in the namespace SparseNLO.CWOpt and work on EuclideanSpace ℝ (Fin n); indices run over Fin n, so instead of . The gradient is Mathlib's gradient, is EuclideanSpace.single i t, and is ContDiff ℝ 1. Assumption 1 is carried as a hypothesis on every statement, as the paper's standing assumption; Assumption 2 is carried wherever the page states it, with a free constant .
is the entry at position of the list of sorted in nonincreasing order; the hypotheses of (P) make it meaningful. The local Lipschitz constant is not computed as a maximum: is any real constant satisfying (2.15), with "at most two nonzero components" read as "supported in some , " (the reading of Example 2.1). Every statement therefore holds for every valid , in particular for . The minima in (2.11)–(2.12) are written as " every value", which is equivalent. The goal states the displayed condition (2.16); its identification with Definition 2.3's -stationarity goes through Lemma 2.2, which belongs to a companion mission.
A trivializing formalization is ruled out: the CW-minimum predicate requires feasibility in and is satisfiable (for , , , the point is a CW-minimum), is the -th largest absolute value, and is constrained by (2.15) rather than left free.
Contributions welcome: proofs of Lemma 2.6 (reusable for any coordinate-descent analysis on two coordinates), Lemma 2.5, (2.18) and the goal; general lemmas on (it is attained by some coordinate, and it vanishes exactly when ).
Theorem numbers and pages follow source.pdf, the arXiv version arXiv:1203.4580v1, not the SIAM typesetting.
How many Euclidean symmetries can a real plane algebraic curve of degree have? Rotational symmetry of a curve is classically detected from the monomials of its equation in the complex coordinate : a rotation of order about the origin can preserve the curve only if the differences of the nonzero monomials satisfy a congruence modulo (Lebmeir and Richter-Gebert, Section 4; Lebmeir, Theorem 5.4). Bounds on the number of symmetries in terms of the degree enter symmetry detection algorithms (Alcázar, Lávička and Vršek) and incidence geometry: Pach and de Zeeuw, Lemma 2.6 use a bound of on the number of isometries of a curve in a distinct-distances argument.
The note Sharp symmetry bounds for real algebraic curves (C. Perassi, 2026; PDF) determines the sharp bounds, classifies the curves attaining the rotation bound in degree , and describes their Möbius geometry. This mission is the complete Lean formalization of that note.
Let be irreducible in , of total degree , and let , identified with a subset of through . Assume that is infinite and is not a circle. Write for the group of Euclidean isometries of with , and for its orientation-preserving subgroup (the rotations and translations preserving ).
For an integer and a nonreal with , the extremal family is
a curve of degree . Its closure in the Riemann sphere is acted on by Möbius maps and by anti-Möbius maps, a Möbius map composed with complex conjugation. In the coordinates , the family has the equation , whose zero set has bidegree .
The goal asserts the bounds only; their sharpness and the equality case are milestones.
The result. The bounds and are attained in every degree, so they cannot be improved as functions of alone; for the curves attaining the rotation bound form one explicit family up to similarity, with a complete invariant. The bound sharpens the auxiliary estimate used by Pach and de Zeeuw (no improvement of their distance exponent is claimed), and the quintic of equation (2) contradicts the degree restriction stated in Lemma 9 of the arXiv version of Alcázar, Lávička and Vršek (the journal version has not been checked).
The formalization. Every statement of the note is proved in Lean 4 with Mathlib: 208 theorems and 12 definition files here, all proved, using only the axioms propext, Classical.choice and Quot.sound. It contains material that Mathlib does not have yet and that is reusable on its own: the genus of a function field over defined through its places and holomorphic differentials, and its invariance under isomorphism; the places of quadratic covers and Kummer covers , with uniformizers and local Kähler differentials; the classification of places of a Dedekind domain; the four-chart atlas of with its Zariski topology; and Möbius and anti-Möbius maps acting on the Riemann sphere. Theorem 1 is also registered with the Palomar registry as PALOMAR-2026-09-18-000007. The Lean code was written by AI agents under the author's direction; the Lean kernel checks it. The results have not been reviewed by an independent human, and neither the kernel checks nor the registration certify novelty.
The first argument is Bézout: the images of a point of under the rotations about a common center are distinct points on one circle, so there are at most of them. This gives for , not , and it says nothing about which curves are extremal. A second obstacle is that a symmetry of the zero set need only fix the polynomial up to sign, as equation (2) shows, so invariant-theoretic arguments that assume do not apply directly. For the Möbius statements the difficulty is that a Möbius map of the sphere does not act on the real equation; the curve must be compactified and its singular points identified. In the formalization, the genus comparison of Remark 5 needs a genus that does not depend on a chosen model, which Mathlib does not provide.
MvPolynomial (Fin 2) ℝ), and the curve is their real zero set as a subset of . Geometric irreducibility means irreducibility over .ℂ ≃ᵢ ℂ preserving that subset. Group orders use Nat.card, which is for an infinite set, so finiteness is part of the statements.OnePoint ℂ with the action of .Sums of random matrices appear throughout numerical linear algebra, statistics, combinatorics and quantum information: randomized sketching and sparsification, covariance estimation, graph sparsifiers, and the analysis of random features all reduce to controlling the largest eigenvalue of a sum of random self-adjoint matrices. Scalar concentration inequalities (Chernoff, Hoeffding, Bernstein, Azuma) have matrix analogues, and J. A. Tropp's User-Friendly Tail Bounds for Sums of Random Matrices (arXiv:1004.4389v7, Found. Comput. Math. 12 (2012) 389–434, doi:10.1007/s10208-011-9099-z) gives a unified derivation of them with explicit constants.
Many applications do not have independent summands: adaptive algorithms, online learning and sequential estimation produce sums whose terms depend on the past. The scalar tool for such sums is Azuma's inequality for martingales with bounded differences, and its corollary, McDiarmid's bounded differences inequality (McDiarmid 1998). This mission is the fifth of a series formalizing Tropp's paper; it targets §7, the matrix Azuma inequality.
Timeline. Ahlswede and Winter (2002) introduced a matrix analogue of the Laplace transform bound for independent sums; Oliveira (2010) gave the variant used in this paper. Tropp (this paper, 2010–2012) proved the matrix Azuma and McDiarmid inequalities below. More refined matrix martingale inequalities appear in Oliveira (2010) and in Tropp's Freedman's inequality for matrix martingales (2011), which the paper cites (p. 27) as requiring additional machinery.
All matrices are with complex entries, . A matrix is self-adjoint (s.a.) when it is Hermitian. For s.a. , is its largest eigenvalue and its spectral norm. Functions of s.a. matrices are defined spectrally: if then , and is defined the same way on positive-definite matrices. is the semidefinite order: is positive semidefinite.
Let be a probability space with a filtration , and write . The expectation and the conditional expectation of a random matrix are taken entrywise. A sequence of random matrices is adapted when each is -measurable. A matrix martingale is an adapted sequence of s.a. matrices with and ; its difference sequence satisfies .
The hypotheses of the main theorem are: is an adapted sequence of random s.a. matrices, and is a fixed (non-random) sequence of s.a. matrices, with
The variance parameter is .
For all ,
In the order they are used:
Corollary 7.2 is the martingale form, . Corollary 7.5 (Matrix Bounded Differences) is the matrix McDiarmid inequality, for a matrix-valued function of independent variables whose changes in one coordinate have squares bounded by .
The result. The bound has the scalar subgaussian shape with two matrix features: a dimensional factor , and a variance parameter equal to the norm of the sum rather than the sum of the norms . In the commuting case the two coincide; in general the first can be smaller by a factor of up to . The theorem needs no independence, so it covers adapted constructions such as Doob martingales. Corollary 7.5, obtained from it, is the standard matrix tool for concentration of matrix-valued functions of independent data. With independent summands the theorem gives a matrix Hoeffding inequality (Theorem 1.3 of the paper).
Formalizing it. The result is proved in the paper; none of it is formalized. Mathlib has the continuous functional calculus, conditional expectation and filtrations, but no Golden–Thompson inequality, no Lieb concavity theorem, and no matrix tail inequality. A formalization produces a machine-checked matrix Azuma inequality, the Golden–Thompson inequality, and a symmetrization lemma for the trace exponential, all of which have uses beyond this paper.
The scalar proof of Azuma's inequality multiplies conditional moment generating functions, , and bounds each factor. For matrices this fails: unless and commute, and is false, so the Golden–Thompson inequality cannot be iterated over terms. The paper itself notes (p. 28) that the classical approach does not seem to extend. A second obstacle is that the hypothesis bounds squares, not the matrices themselves; it does not give , so the scalar Hoeffding lemma for bounded centred variables has no direct matrix analogue. The infrastructure is also heavy: Lieb's concavity theorem underlies Corollary 3.3, and operator monotonicity of the logarithm is needed.
Matrices are Matrix (Fin d) (Fin d) ℂ, self-adjointness is IsHermitian, and is Mathlib's order under MatrixOrder. Matrix exponential and logarithm are cfc Real.exp and cfc Real.log. is the supremum of the real spectrum, which is why is assumed (NeZero d). Expectation and conditional expectation of matrices are entrywise Bochner integrals; adaptedness is entrywise strong measurability with respect to a Mathlib Filtration ℕ. The summands are indexed by , so is never truncated. The bound is required almost surely. The bounds are deterministic matrices. The infimum over in Proposition 3.1 is posed as the bound for each at which the expectation is finite.
The hypotheses must not be made vacuous. Integrability of each is assumed explicitly, because for a non-integrable variable Lean's conditional expectation is and the centring hypothesis would say nothing. The are not assumed independent: an independence hypothesis would turn the goal into the weaker matrix Hoeffding inequality.
Two readings are recorded in the statements. In Lemma 7.7 the conditional expectation given is replaced by the expectation over at each fixed value with ; by independence these agree. Corollary 7.2 adds the hypothesis that is almost surely constant, without which .
A complete development needs: Golden–Thompson; Lieb's concavity theorem (or Corollary 3.3 directly); operator monotonicity of the matrix logarithm; monotonicity of the trace exponential; conditional expectation of matrix-valued variables and its interaction with the semidefinite order. All of these are reusable well beyond this mission, and contributions of any of them are welcome. Proposition 3.1, Corollary 3.3 and Lemma 4.3 are also milestones of other missions in this series.
Online learning and stochastic learning ask different questions. An online learner faces an arbitrary sequence of loss functions and is judged by its regret: the excess of its cumulative loss over that of the best fixed hypothesis in hindsight. A stochastic learner receives independent samples from an unknown distribution and is judged by the risk of a single hypothesis it outputs. Regret bounds hold without any probabilistic assumption, so they are strong guarantees; risk bounds are what statistical learning and stochastic optimization actually need.
The online-to-batch conversion connects the two: run any online learner on losses built from i.i.d. samples and output either the average of its predictions or one prediction chosen at random. The expected excess risk of the output is then at most the expected regret divided by the number of rounds. A general form of the conversion is due to Cesa-Bianchi, Conconi and Gentile (IEEE Trans. Inf. Theory 2004). Shalev-Shwartz's survey (Found. Trends Mach. Learn. 2011) states it in expectation, in Vapnik's general setting of learning, as Theorem 5.1 and Corollary 5.2 (§5, pp. 186–189). Every stochastic-gradient analysis that goes "regret bound, then online-to-batch" rests on this statement.
Fix a dimension and a hypothesis class . Examples range over a measurable space and are drawn from a probability distribution on , which the learner does not know. A cost measures how badly hypothesis does on example , and the risk of is
This is Vapnik's general setting of learning (Definition 5.1); supervised classification, regression and stochastic convex optimization are special cases.
The conversion draws independently from and runs an online learner on the losses . Its prediction in round , , may depend only on . The output is either the average or the randomized choice , with uniform on the rounds and independent of the sample.
For every comparator , under the conditions of Theorem 5.1,
for the randomized output, and for the averaged output when and are convex. The right side is the expected regret divided by . The statement contains no constant: it is an exact reduction, valid for every online learner.
Corollary 5.2 makes every regret bound a risk bound. Combined with the regret of online gradient descent or online mirror descent, it gives the excess-risk rate of stochastic gradient methods for convex Lipschitz problems; combined with logarithmic regret for strongly convex losses, it gives rates. The survey's own "Stochastic Online Mirror Descent" box (p. 189) is exactly this composition.
The result is proved in the paper. What this mission adds is a machine-checked version in a measure-theoretic model with honest non-anticipation and a genuine model of the randomized output. The platform has a related statement, Mohri, Rostamizadeh and Talwalkar's Theorem 8.15 (FoundationsML.OnlineLearning.online_to_batch_conversion), which is a high-probability bound for bounded convex losses in supervised learning; it is a different statement and neither implies the other. The expectation form here is the one stochastic-optimization arguments use.
The result is short on paper; the formal content is the conditional-expectation step. The prediction is a random variable built from , while is a fresh draw, so must be computed by integrating out first, which means a Fubini–Tonelli argument on a product of copies of split into the past, the present and the future of round . The first idea, that has the same law as for a fixed , is wrong: is random. The identity also fails as soon as may look at (take a minimizer of ), so the argument must use the information structure, not only the marginal laws. The averaging part additionally needs Jensen's inequality for and the measurability of as a function of the hypothesis.
EuclideanSpace ℝ (Fin d) with a set, because averaging needs a vector space. Rounds are numbered , and .ψ : Fin T → Ψ under Measure.pi (fun _ => Q), with Q a probability measure: independent draws from .A t : (Fin t → Ψ) → ℝ^d of measurable maps with values in , so non-anticipation holds by typing: . The learner may read the examples, not only the losses; this class contains the paper's learners, so the statements are at least as strong.Fin T. The expectation over is not replaced by the average over rounds (that replacement is the first line of the proof).Infrastructure needed: Tonelli/Fubini on finite products split at a coordinate (Mathlib's Measure.pi), measurability of parametric integrals, and Jensen's inequality for a convex function of a finite average. The round- identity is reusable for any non-anticipating stochastic process; contributions of proofs of any milestone are welcome.
A monotone disjunction over Boolean variables is a rule of the form . Learning such a rule online — predicting the label of each example before it is revealed and paying one unit per wrong prediction — is the basic test case for learning when only a few of many features matter. Littlestone's Winnow algorithm (Littlestone 1988) learns a -literal disjunction with mistakes, while additive algorithms such as the Perceptron need a number of mistakes that grows linearly in on the same problem. Kivinen and Warmuth (1997) placed this gap inside a general theory of multiplicative versus additive updates. Shalev-Shwartz's survey (2011) derives Winnow as a special case of Online Mirror Descent with an unnormalized entropy regularizer, and obtains its mistake bound from a general local-norm regret bound. This mission formalizes that derivation.
Throughout, labels are and instances are . For with , the hypothesis is the disjunction of the variables with . A weight vector errs on when .
Winnow with parameter starts from . On round it receives , predicts , and receives . If it sets for every ; otherwise . The set collects the rounds on which it errs. On those rounds the surrogate loss is the hinge loss , and on all other rounds.
Unnormalized Exponentiated Gradient with parameters , run on linear losses , keeps , where . Winnow is this algorithm with and on , otherwise.
Online Mirror Descent (OMD) with link function predicts . Its analysis uses the Fenchel conjugate of a regularizer on a set , and the Bregman divergence .
For , and every with ,
and if for all , the run with satisfies
with equality at a minimizer of . 2. Theorem 2.23: if for all , then for all
together with its specialization to . 3. (3.3): for Winnow. 4. (3.4): for every round.
The theorem gives a mistake bound for learning sparse disjunctions that is logarithmic in the number of irrelevant features, against the of the Perceptron run on the same surrogate (p. 173). The first inequality also covers non-separable data: the bound degrades by , the total hinge violation of the best disjunction. The milestones are general and carry weight beyond Winnow. Lemma 2.20 is the standard duality form of the OMD regret bound. Theorem 2.23 is a local-norm bound that also allows negative losses down to .
All four results are proved on paper. To our knowledge none has a machine-checked proof, in Lean or elsewhere. This mission produces such proofs for the survey's own route: OMD duality, then unnormalized EG, then Winnow.
The obvious route bounds Winnow directly with a potential function, but the survey's statement sits at the end of a chain. The chain needs Fenchel–Young with an attained supremum, a telescoping identity for the conjugate, and the inequality for . It also needs a reduction in which the surrogate losses depend on the algorithm's own error set . Since is defined after the run, the subgradient inequality must be argued for exactly these losses. The bound uses that is Boolean and that ; for fractional or for it fails. Solving (3.3) and (3.4) for needs .
Vectors are Fin d → ℝ with explicit sums ; Lemma 2.20 is stated in an arbitrary real Hilbert space. Rounds are numbered in place of . Instances, labels and comparators carry the hypotheses , , , . is the natural logarithm, and through Real.log 0 = 0.
Erratum corrected. The Winnow box on p. 173 prints the update , and the proof on p. 174 uses . With that sign the algorithm demotes on a false negative, and Theorem 3.10 is false. Take , , , , and , on every round. The margin condition holds, and errs on round 1. The printed update only shrinks , so every round is an error, and exceeds . On an error round the hinge surrogate has gradient at . The mission therefore formalizes the update (Littlestone's Winnow) and on . With this update the run above errs once. The milestone texts are quoted verbatim, with the printed sign.
Implicit hypotheses made explicit.
Conventions.
The bounds carry no and no constant is instantiated. A trivializing formalization is ruled out: is the run's own surrogate, not a free function, and the conjunct quantifies over the weights.
Infrastructure needed: conjugates and the Fenchel–Young inequality on a subtype, telescoping sums, elementary exponential inequalities, and the case analysis on -valued data. Lemma 2.20 and Theorem 2.23 are reusable for other OMD and EG analyses. Lemma 2.20 is also stated in the companion mission on normalized EG. Proofs of any milestone, and alternative routes to the goal, are welcome. Excluded: the Perceptron comparison (p. 173), and Theorem 3.9 (Perceptron), which is already proved on the platform.
Many optimization problems in shape analysis, computer vision, numerical linear algebra and statistics have a nonlinear search space: a sphere, a Stiefel or Grassmann manifold, a space of curves modulo reparametrization. Projecting iterates of a Euclidean method back onto the constraint set loses the geometry, so one designs methods that move along the manifold itself. Riemannian line-search methods do this by replacing the update with for a retraction , and by carrying old search directions to the new tangent space with a transport.
Nonlinear conjugate gradient (NCG) methods are a natural candidate on manifolds: they need only first derivatives and store one previous direction. In the Euclidean case, Al-Baali showed in 1985 that the Fletcher–Reeves method with strong Wolfe step lengths and satisfies (doi:10.1093/imanum/5.1.121); Nocedal and Wright give the standard textbook proof (Lemma 5.6 and Theorem 5.7 in Numerical Optimization). Ring and Wirth (doi:10.1137/11082885X, SIAM J. Optim. 2012) transfer this analysis to Riemannian manifolds, possibly infinite-dimensional, which is the setting of their application to shape spaces. The mission formalizes that transfer.
is a smooth manifold modelled on a real Hilbert space , with a Riemannian metric on each tangent space and norm . For , is its differential, a continuous linear functional on with dual norm , and the gradient is its Riesz representative, .
A retraction is a family of smooth maps with and . Its transport is .
A run of Algorithm 1 consists of points , directions and steps with . With , the Wolfe conditions at are
and the strong Wolfe conditions replace (1b) by
The angle between and is given by .
The Fletcher–Reeves direction is
For a non-terminating Fletcher–Reeves run with strong Wolfe steps and , if the transport is non-expansive on the search directions, , is bounded below, and the pull-backs are Lipschitz continuously differentiable on with a uniform constant, then
Proposition 15 guarantees that Riemannian Fletcher–Reeves, with any retraction whose transport does not enlarge the search direction, cannot stall at a positive gradient level: some subsequence of the gradient norms tends to zero. Together with strict convexity in the sense of the paper's Proposition 4 this gives convergence of the iterates to the minimizer, and it justifies the use of the method on the shape spaces of the paper's §4. The hypothesis on the transport is the only new ingredient compared with the Euclidean theorem, and the paper's Remark 7 notes that convergence can no longer be guaranteed without it.
The result is proved in the paper. As far as is known, neither Zoutendijk's theorem on a manifold nor the Fletcher–Reeves convergence theorem has a machine-checked proof; Euclidean versions of both appear elsewhere on the platform, but the Riemannian statements, with retraction, transport and tangent-space-dependent norms, are new. The mission produces the line-search interface on a Riemannian manifold (retraction, transport, Wolfe conditions) in a form reusable by other Riemannian methods.
Each search direction is built from a vector in a different tangent space. The transported direction lives in , and only the step equation identifies it with a vector of ; norms, inner products and differentials all depend on the base point, so every Euclidean manipulation has to be carried through that identification. Zoutendijk's theorem has to connect two different descriptions of the same step: the curvature condition (1b) is stated with the differential of at the new point applied to the transported direction, while the Lipschitz hypothesis concerns the one-variable pull-back . They agree only because the transport is the derivative of the retraction, and the agreement is a chain rule for manifold derivatives, which has to be established in Mathlib's mfderiv framework for maps out of a tangent space. The growth bound cannot use ; it needs the non-expansiveness hypothesis exactly where the Euclidean argument uses the identity.
The manifold is a Mathlib manifold modelled on a real Hilbert space E, with Mathlib's RiemannianBundle on its tangent spaces; tangent-space norms and inner products are the Riemannian ones and is mfderiv. Geodesic completeness, separability, the distance and the Levi-Civita connection, standing assumptions of the paper, are not used by any statement and are dropped. The gradient is given as a field with its Riesz property. One retraction family is used for every step (the paper allows a different retraction at each step), the steps are positive, and indices start at .
The following readings are explicit:
Summable.The transport in the conclusion and in the Fletcher–Reeves update is the derivative of the retraction, not an arbitrary linear map; with an arbitrary map, condition (1b) would no longer be a statement about the pull-back , and Zoutendijk's theorem would fail. A run predicate that no sequence satisfies would make the goal vacuous; the one-dimensional run , , , , , satisfies every hypothesis.
The paper's other main result, R-linear convergence of Riemannian BFGS (Proposition 10), is a separate mission, and its superlinear-rate results (Propositions 5, 7, 8, 12, Corollary 13), which require parallel transport and the exponential map, are out of scope. Contributions welcome: proofs of the chain rule identities for retractions (reusable for any Riemannian line search), of Zoutendijk's theorem, and of the milestones in order.
A directed polymer in a random environment is a random up-right lattice path whose law is reweighted by random site weights. Its free energy, the logarithm of the partition function, is believed to belong to the Kardar–Parisi–Zhang (KPZ) universality class: for a path of length of order , the free energy fluctuates on the scale and the path wanders on the scale . For zero-temperature analogues (last-passage percolation with exponential or geometric weights) these exponents were established through exact formulas from random matrix theory (Johansson 2000) and later through a probabilistic coupling argument based on the Burke property of queues (Balázs–Cator–Seppäläinen 2006).
For directed polymers at positive temperature no model with the KPZ exponents was known until Seppäläinen (arXiv:0911.2446, Ann. Probab. 2012) introduced the log-gamma polymer, whose weights are reciprocals of gamma variables, and proved that its free energy has variance of order in the characteristic direction. The model has since become a basic exactly solvable polymer:
The present mission formalizes the 2009 variance theorem, which needs neither of the later exact formulas.
Sites are and . A weight configuration assigns a positive number to each site. On the axes, and for are the boundary weights, and , , are the bulk weights.
An up-right path from to is a sequence whose steps are or . The partition function is
the weight of the origin excluded, . The quenched polymer measure gives the path probability , and the annealed measure is its average over the environment. The exit points and are the numbers of initial steps the path takes along the -axis and along the -axis.
Assumption (2.4). Fix . The weights are independent with
Let and be the digamma and trigamma functions. The characteristic direction is . For a real scaling parameter and a constant , the endpoint satisfies
There are constants and , depending on , such that under (2.4) and (2.6)
The upper bound runs through the Burke property and the variance identity:
The lower bound runs through partition-function comparisons:
The result. Theorem 2.1 was the first proof of the KPZ fluctuation exponent for a directed polymer at positive temperature. Its upper bound also yields a strong law of large numbers for (2.7) and, with Theorem 3.3, a central limit theorem off the characteristic direction (Corollary 2.2). The exit-point estimates of Sections 4 and 5 give the path fluctuation exponent (Theorem 2.3) and are reused for the polymer without boundaries and the point-to-line polymer (Theorems 2.4–2.6).
Formalizing it. The theorem has been proved since 2009; no formal proof of it in a proof assistant is known. A formalization checks a proof with many interacting estimates and two corrected slips (below). The definitions made here (the lattice-path partition function, the inverse-gamma environment, the recursion (3.2), exit points, quenched and annealed measures) are the base for later missions on Theorems 2.3–2.7 of the same paper. Lemma 3.2 contains a gamma-distribution characterization (Lukacs' theorem) of independent interest.
The obvious route to a variance bound, a martingale decomposition of over the independent weights, gives only , i.e. order ; it cannot see the cancellation that produces . The order is specific to the characteristic direction: off it, satisfies a central limit theorem with variance of larger order (Corollary 2.2), so any argument must use the exact relation between the boundary parameters and the endpoint . The upper bound requires controlling the annealed exit point at the scale , with tail estimates whose constants are uniform in the parameters. The lower bound is a separate statement: the path must not exit an axis at distance from the origin with non-vanishing probability, which no upper-bound estimate implies.
Source: arXiv:0911.2446v4 (26 Aug 2015, revised version); its printed page numbers equal the PDF's. All declarations are in the namespace LogGammaPolymer.Variance.
ℕ × ℕ; a path is a step sequence with a fixed number of east steps; is a finite sum over these paths with the starting weight excluded. The environment Env θ μ P bundles one weight family Y : ℕ × ℕ → Ω → ℝ, measurability, mutual independence of every weight off the origin, and the three laws as images under equal to Mathlib's gammaMeasure (shape, rate ). Positivity of the weights is not assumed pointwise in the probabilistic statements; it holds almost surely. The deterministic lemmas (3.1, 5.1, 5.4) are stated for every weight function positive off the origin.variance, and every upper bound or identity also asserts (or integrability of the averaged quantity), so that the junk value of variance and of the Bochner integral cannot satisfy it.Type), the environment, and . Upper limits in are stated as "for every there is with the bound for ". The compact-set uniformity of Lemmas 4.1, 4.3 and (4.32) is formalized. The remark after Theorem 2.1 on uniform constants is not.A formalization in which includes the origin's weight, the laws are not exactly the inverse gammas with shapes and rate , independence is dropped, is allowed, or the constants depend on the environment or on does not state Theorem 2.1.
Needed infrastructure: gamma–beta algebra and a Lukacs-type characterization, independence of finite families built by the recursion (3.2), differentiation of expectations in the shape parameter, and moment bounds for sums of i.i.d. variables. All of these are reusable beyond this mission. Proofs of any milestone, and of supporting lemmas such as (3.3)–(3.4), are welcome.
City logistics often moves goods in two stages: large trucks bring freight from a central depot to a few intermediate satellites, and small vehicles distribute it from the satellites to the customers. The two-echelon capacitated vehicle routing problem (2E-CVRP) is the basic optimization model of such systems; it contains the capacitated location-routing problem as a special case. Baldacci, Mingozzi, Roberti and Wolfler Calvo (Oper. Res. 61(2), 2013) gave an exact method that solved benchmark instances out of reach for earlier algorithms.
Their method does not attack the whole problem at once. It enumerates configurations, sets of first-level (depot–satellite) routes, discards most of them with cheap tests, and solves a second-level problem only for the survivors. The correctness of the method rests on two facts stated in §5 of the paper: the problem decomposes exactly over configurations (Eq. (26)), and the pruning tests of Propositions 1 and 2 never discard the configuration of a solution better than the incumbent. This mission formalizes those facts.
An instance has a depot , satellites and customers , a symmetric cost on the edges (with the fixed vehicle costs folded in), positive integer demands with total , first-level vehicles of capacity , second-level vehicles of capacity at satellite with a global limit , satellite capacities and handling costs .
A first-level route leaves the depot, visits a set of satellites and returns; its cost is the length of the closed walk. A second-level route leaves satellite , visits a set of customers of total demand and returns; its cost is the walk length plus . Formulation chooses binary , and integer deliveries minimizing subject to: each customer on exactly one used second-level route; at most used routes at and in total; load at at most ; at most first-level routes; the deliveries to equal the load leaving ; each used first-level route carries at most . Its optimal value is , when infeasible.
The set of configurations is
For , , and . Problem is with the first-level routes fixed to : second-level routes only at satellites of , real deliveries for , and . Its value is when infeasible.
The bounds of §5.1 use multipliers , , and marginal costs satisfying the penalty system (12), for every route of satellite :
Let be a real number and a feasible solution of of cost less than , with configuration . Then and
Eq. (26) is what makes the method exact: once every configuration that can carry a solution better than the incumbent is examined, the best is the optimum. Propositions 1 and 2 are what make it fast: they remove configurations from before any second-level problem is solved. If a pruning test discarded the configuration of a cheaper solution, the method would return a suboptimal value and still report it as optimal; the formal statements rule this out for every instance, not just the benchmark ones. The capacity constraints (33) play the same role inside : a cut that removed a feasible solution would make the bound invalid.
The paper's proofs are in an electronic companion; none of these statements has been machine-checked before, and none is on the platform. The formalization also records exactly what the tests need: positive demands, integral vehicle counts, and the sign conditions on the multipliers, and nothing about the optimality of the incumbent.
Most statements are elementary counting and Lagrangean weak-duality arguments over finite index sets. The work lies in the bookkeeping between two formulations with different index sets: sums over all satellites, only over , and a solution of one must be turned into a solution of the other. One step is not elementary: has integer deliveries and real ones, so the inequality in (26) needs an integral delivery plan from a fractional one. That is an integrality property of a bipartite transportation problem (routes to satellites, integral capacities and demands), which no counting argument gives.
Satellites and customers are Fin ns and Fin nc, 0-based. The route families and are arbitrary finite families of elementary routes with costs computed along the closed walk; the paper uses all such routes, so every statement here is a generalization. Demands are positive integers; the triangle inequality is not assumed. Binary variables are Bool; optimal values are infima in EReal, with ⊤ for an infeasible problem. A configuration is a Finset of route indices. The penalties are any , , and satisfying (12), not only those producing the paper's bound LD1. Ceilings of and are natural-number ceilings of rationals; those in Proposition 2 are integer ceilings of reals.
The goal departs from the printed proposition in three disclosed ways. Only necessity is stated: the "if" direction is false, because (b)–(e) ignore the satellite capacities . Condition (a), , is omitted: it holds for some optimal solution, not every one (its split-delivery analogue is posed, and open, on the platform as SplitDeliveryVRPTW.Known.exists_optimal_split_customers; it is not reused here). "An optimal solution" becomes "a feasible solution of cost below ", the property the paper's own justification uses. Proposition 2 is stated with as a hypothesis; the paper's computation of by problem (27)–(32) is not formalized, because (32) forces positive deliveries that does not require. The goal is not trivialized by an infeasible hypothesis: feasible solutions of exist on small instances, and a toy instance was checked in Lean.
A complete development needs finite-sum manipulations, Lagrangean weak duality for (12), and, for (26), integrality of bipartite transportation polytopes, which is reusable well beyond this mission. Proofs of any milestone, and a general transportation-integrality lemma, are welcome.
Single-leg capacity allocation under customer choice is the basic dynamic problem of revenue management: a firm holds a fixed stock of a perishable resource (seats on a flight leg, rooms on a night), and in every period of a finite selling horizon it decides which products (fare classes) to offer to the arriving customer. Talluri and van Ryzin (Management Science, 2004) showed that under a multinomial logit (MNL) choice model with known parameters, the optimal assortment in every period is revenue-ordered and shrinks as capacity becomes scarcer ("nesting by fare order"), which is what justifies the protection levels and bid prices used in practice.
The MNL parameters are estimated from data and are never known exactly. Rusmevichientong and Topaloglu (Operations Research, 2012) study the robust version, in which an adversary picks the parameters of each period from an uncertainty set after seeing the offered assortment, following the robust Markov decision process framework of Iyengar (Mathematics of Operations Research, 2005). Their Section 4 shows that the structure of the known-parameter problem survives: the value function is concave in capacity, the optimal assortment is a revenue threshold set, and it grows with remaining capacity and, when uncertainty does not shrink, over time. This mission formalizes those results.
There are products with revenues . An MNL parameter vector is ; offered the assortment , a customer buys product with probability
and nothing with probability . The expected revenue is .
Static problem (Section 3). For a compact nonempty uncertainty set ,
and is an optimal assortment of smallest cardinality.
Dynamic problem (Section 4). Periods each bring one customer, whose parameter vector lies in a compact nonempty . A purchase consumes one unit of capacity. The value function , the maximum worst-case revenue from period on with units of capacity, satisfies
for , with and . The marginal value of capacity is , and is a maximizer of the right-hand side of smallest cardinality.
For every and , and, in the second part, every with :
The result. Theorems 4.1–4.3 say that robustness costs nothing structurally: the robust policy is still a nested threshold policy, so it can be implemented with the protection levels or bid-price controls already in use, and it can be computed by examining at most revenue-ordered assortments per state instead of . Theorem 4.3 gives the operational content: with less inventory, offer fewer, higher-revenue products; nearer the end of the season (when the uncertainty sets are nested), offer more.
Formalizing it. The results are proved in the paper; none of them has a machine-checked proof. A formalization produces a checked robust finite-horizon dynamic program over finite action sets with compact adversary sets, the reduction of each Bellman step to a static max–min problem with shifted revenues, and checked concavity and time-monotonicity arguments that are reusable for other single-resource problems. The known-parameter analogues for general regular choice models and for the Markov chain choice model are separate drafts on the platform (RevenueOrdered.Nesting.*, MarkovChainChoice.SingleResource.*); they have no uncertainty set and are not used here.
The obvious route to concavity, an induction on in which is a maximum of concave functions, fails: a maximum of concave functions is not concave, and here each candidate assortment is evaluated by a minimum over , and the worst-case parameter vector changes with the capacity level, so the known-parameter argument cannot be reused term by term. Any induction on also has to handle the boundary , where the Bellman equation does not apply and only is given. Every step involving a minimum must use that the minimum over a compact set is attained, and translating a minimum by a constant must be justified rather than assumed.
Fin n (Lean index is product ). A parameter vector is p : ℝ × (Fin n → ℝ) with p.1 . is the published ChoiceCDLP.MNL.mnlObjective. Minima over uncertainty sets are real infima (sInf), equal to the attained minima under the standing hypotheses; maxima are Finset.sup' over all assortments.V t, , is compact, nonempty and contained in (IsUncertaintySeq); the static results assume the same of V. The paper writes "" in Theorem 3.2 and Corollary 3.5; this is read as , compact.RobustMNL.Dynamic, the companion mission on Section 3 of the same paper, identically up to namespace.Randomized coordinate descent updates one block of variables per iteration, chosen at random. For problems whose dimension makes even one full gradient expensive (the "huge-scale" problems of the title, such as sparse least squares or truss topology design), a coordinate step can cost a tiny fraction of a gradient step. Nesterov's paper (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012) 341–362) gave the first global complexity bounds for such methods with non-uniform sampling, and it is the reference point for the later literature on randomized block methods (Richtárik and Takáč 2014, Lu and Xiao 2015, Allen-Zhu et al. 2016).
The first results of the paper (Theorem 1, the subject of a companion mission) bound the expected objective value after k iterations. An expected bound does not say what happens in a single run. This mission formalizes the paper's answer to that question in §3: by running the method on a slightly regularized objective, one run returns an ε-solution with any prescribed probability β, after a number of iterations that grows only logarithmically in 1/(1 − β).
The variable space is a product of blocks; a point has blocks , and is the point whose -th block is and whose other blocks vanish. In this mission each block carries a Euclidean norm with (3.4), and the whole space carries
The objective is convex and differentiable, has a minimizer with value , and its partial gradients are Lipschitz along their own block with constants (2.2): . Write .
The method RCDM (2.6) draws, independently at each step, block with probability and replaces by , where is a maximizer of (1.8). The quantity is the expectation of over the first draws.
The level-set radius is , and for the regularized objective is
It has block constants , so RCDM applied to samples block with probability and steps with .
For , , and
the point produced by RCDM on satisfies
Theorem 4 turns an in-expectation guarantee into a single-run guarantee with an explicit, non-asymptotic iteration count. Its dependence on the confidence level is logarithmic, so very high confidence costs little; and the count replaces the largest eigenvalue of the Hessian, which governs the full gradient method, by the trace-type quantity , which for sparse problems makes groups of coordinate steps competitive with one gradient step. Theorem 2 is the linear-rate result for strongly convex objectives that later analyses of randomized block methods take as their starting point.
The results are proved in the paper. None of them is formalized in the block setting. The scalar Euclidean case of Theorem 2 is proved on Prove2Me as ConvexOptAlg.CoordDescent.theorem_6_8 (Bubeck, Theorem 6.8), and the bound (3.2), for a -strongly convex in any norm, is proved as ConvexOptAlg.CoordDescent.lemma_6_9. This mission adds block variables with general norms (Theorem 2), the regularization constants, the gradient-norm bound, and the high-probability statement itself, which has no formalized counterpart.
The obvious argument fails. Theorem 2 controls the expected suboptimality of , not of , and Markov's inequality applied to does not reach accuracy ε: and differ by an amount comparable to ε, and the contraction factor itself depends on μ. Relating the run on to the original problem requires the global Lipschitz constant of in , which for is the weighted co-coercivity statement of Lemma 2 of the paper and is not a consequence of (2.2) alone without convexity. The constants of (3.11) are exact, including the factor 2 and the ½, so no estimate may lose a constant. Finally, the iterates depend on all previous draws, so even the finite-sum expectations need a careful account of linearity and of conditioning on the last draw.
Blocks E of finite-dimensional real spaces E i indexed by Fin n (0-based for the paper's 1, …, n). Euclidean blocks (3.4) are inner-product spaces, with absorbed into the inner product; Theorem 2 is stated for arbitrary normed blocks. The dual norm of a block is the operator norm of a functional.Fin k → Fin n; expectations and probabilities are finite sums weighted by . No measure theory is involved.Contributions are welcome on the probabilistic bookkeeping for expect (normalization, linearity, conditioning on the last draw, Jensen for a concave function), which is reusable by every mission of this series; on Lemma 2 of the paper in the block setting; and on the milestones in the stated order.
A retailer that orders stock months before the selling season carries inventory risk: its profit depends on a demand it cannot observe when it commits. For many goods that demand moves with a quantity traded on financial markets: sales of housing-related products with an interest-rate or construction index, sales of fashion or luxury goods with a stock index, sales of commodity-intensive products with a commodity price. V. Gaur and S. Seshadri, Hedging Inventory Risk Through Market Instruments (MSOM 7(2), 2005), ask what such a firm gains by trading in that market, and how the trade interacts with the ordering decision.
Their analysis has two halves. When demand is perfectly correlated with the asset price, the newsvendor payoff can be replicated by a portfolio of the asset and call options, and inventory risk can be removed completely (§2). When demand is only partially correlated, the hedge is imperfect, and the question becomes whether a decision maker with a concave utility still benefits from hedging, and whether hedging changes the order quantity (§3.2). This mission formalizes the first of these two questions in the partially correlated model: Proposition 5, which says that a small fair hedge never lowers expected utility at the margin. A companion mission of the same series treats Proposition 7, on the order quantity.
A firm orders units now at unit cost , sells at price at a future time , and salvages leftovers at . The demand is
where is the time- price of a traded asset and is a forecast error, independent of , with and (§3, p. 107). Write . The paper's standing assumptions (§2, p. 106) are , , and , where is the risk-free rate.
After scaling all cash flows by (p. 110) the firm's terminal wealth without hedging is
with and the scaled initial wealth plus . In these units reads and .
A hedge is a portfolio with time- payoff and time-0 price . The paper requires it to be a fair gamble, (12), and to be an increasing function of (p. 111). If the firm shorts units of the hedge, its wealth is
and a decision maker with utility evaluates it by .
In Lean, the law of is a probability measure ν on ℝ, the law of is a probability measure G on ℝ, the hedge is X_T = φ S_T for a function φ : ℝ → ℝ, the forward price is one real x0r, and every expectation is an integral against the product measure ν.prod G. The definitions file provides unhedgedPayoff, hedgedPayoff and expUtil.
For any concave and differentiable utility function , and any fixed order quantity ,
The Lean statement asserts that the two-sided derivative exists at and is nonnegative.
Proposition 5 is the paper's answer to "should a risk-averse newsvendor hedge at all?": with any concave utility and any order quantity, a small short position in a fair hedge that rises with the asset price weakly increases expected utility. It needs no assumption on the shape of the utility beyond concavity, no sign of , and no assumption on the law of the forecast error beyond independence. It is the starting point for the paper's later results on the optimal hedge (Proposition 4) and on how hedging raises the optimal order (Propositions 6 and 7), and it is a clean instance of a general principle in operations-finance: a fair bet that is negatively correlated with marginal utility is worth taking at the margin.
The result is proved in the paper in a few lines. What this mission adds is a machine-checked version with every regularity condition explicit: the paper differentiates under the expectation and multiplies expectations without stating when this is legitimate, and conditions on informally. To the best of a search of the Prove2Me catalog, neither the result nor the two steps of its proof (an integral version of Chebyshev's covariance inequality for monotone functions, and differentiation of a concave expected utility under the integral sign) is formalized there.
The obvious argument has two analytic gaps. First, exchanging with the expectation needs a dominating function, and the only integrability available is at finitely many values of , for both signs of . Second, " is a decreasing function of " is false as a statement about the pair : depends on too. The covariance step is Chebyshev's inequality for the function and the function , which needs independence (Fubini on the product measure) and has to cope with the conditional expectation being finite only almost everywhere. Neither nor the hedge payoff is bounded.
The Lean development commits to the following conventions.
ν (law of ) and G (law of ) on ℝ; independence is the product measure ν.prod G. The standing assumptions and are hypotheses (∫ e, e ∂G = 0, MemLp id 2 G).φ : ℝ → ℝ, monotone (nondecreasing, reading the paper's "increasing" weakly), measurable and ν-integrable; the fair-gamble condition (12) is ∫ s, φ s ∂ν = x0r. The paper's further remark that is piecewise continuous and a.e. differentiable is not needed and not imposed.u : ℝ → ℝ with ConcaveOn ℝ Set.univ u and Differentiable ℝ u, exactly "concave and differentiable"; no monotonicity of is assumed.A statement of the form 0 ≤ deriv (fun α => expUtil …) 0 would be trivially true whenever the derivative fails to exist (Lean's deriv returns 0 there); the goal instead asserts HasDerivAt with a value D and 0 ≤ D. The hypotheses are satisfiable with a non-constant hedge: a sorry-free check uses , uniform on , uniform on and .
Infrastructure that a complete proof needs, reusable beyond this mission: Chebyshev's integral (covariance) inequality for two monotone functions of a real random variable; differentiation under the integral sign for concave integrands with integrability at three points; Fubini-based conditioning on one coordinate of a product measure. Contributions of these general lemmas as separate theorems are welcome. The source PDF is a scan of the published article.
In a time-inconsistent control problem, a control that is optimal when planned at time stops being optimal when the problem is re-solved at a later time. Two sources of time inconsistency are common in finance and economics. One is a variance term in the objective, as in continuous-time Markowitz mean–variance portfolio selection (Zhou–Li 2000; Basak–Chabakauri 2010). The other is a state-dependent target, as in Björk–Murgoci–Zhou 2014. Dynamic programming does not apply. A standard response is to look for an equilibrium: a control that no planner at any time can improve by an infinitesimal deviation on .
Hu, Jin and Zhou define open-loop equilibria for a general stochastic linear–quadratic (LQ) problem with both sources of time inconsistency. They give a sufficient condition through a flow of forward–backward SDEs, which is the subject of mission I of this series. This mission covers §4 of the paper: the scalar-state case with deterministic coefficients, where the equilibrium is computed explicitly from a system of coupled Riccati equations. Mission III covers §5, the mean–variance application with random coefficients.
On a probability space carrying a standard -dimensional Brownian motion with its filtration , the state is scalar () and the control takes values in :
The coefficients are deterministic functions on : , , , and symmetric. are bounded, are square integrable, , , and . At time , in state , the planner evaluates
where . The third term (the variance-like term) and the fourth term (which depends on ) make the problem time-inconsistent. A control with state is an equilibrium (Definition 2.1) if, for every and every -measurable square-integrable , the spike satisfies
With , and , the coupled Riccati system (4.9) for deterministic is
Given , a linear ODE (4.8) determines with . The candidate equilibrium is the linear feedback (4.4)
Suppose and one of three cases holds:
Then
and, for every solution of (4.8), the closed-loop equation of (4.4) has a solution, and the feedback control along every closed-loop state is an equilibrium.
The theorem gives an equilibrium in closed form, as a linear feedback of the current state with deterministic gains. That makes the equilibrium computable and comparable with the classical, time-consistent LQ regulator. Setting recovers a standard LQ problem, but (4.9) differs from the classical Riccati equation even then: it is a nonsymmetric coupled system (footnote 2, p. 10), and the cases (i)–(iii) are the conditions under which it is solvable. The mean–variance results of §5 (mission III) follow the same pattern.
The result is proved in the paper; to our knowledge it has not been formalized. A formal proof needs global existence for a nonlinear, nonautonomous ODE system with Carathéodory coefficients, obtained by truncation and a priori bounds. It also needs linear SDEs with bounded feedback, Itô calculus for products of deterministic and Itô processes, and the sufficient condition of mission I. Uniqueness in case (iii) is claimed by Theorem 4.4 but not proved in Theorem 4.3; it is part of the goal.
The system (4.9) is quadratic in . Its solutions can blow up in finite time, and can degenerate when changes sign. Picard–Lindelöf therefore gives only local solutions, and a global solution needs a priori bounds and , with and independent of the truncation level. Those bounds are where the case hypotheses enter. In the stochastic half, the equilibrium property is not proved by computing directly. It requires checking that the explicit candidate meets the flow-of-FBSDE sufficient condition, and the flow carries a parameter and the conditional expectations for every .
The general model (data, standing assumptions, states, conditional cost, spike, equilibrium) is stated for arbitrary and instantiated at through toData. It is built on the published substrate Peng1990_SMP_Stochastic (Brownian motion, natural filtration, , Itô integrals, SDE solutions). The formalization commits to the following choices.
The goal's conclusion is Definition 2.1 itself; it does not mention , or (3.4). Existence of the closed-loop state is asserted, not assumed. A formalization that assumes existence, or that replaces equilibrium by condition (3.4), is a different and weaker theorem.
Theorem 3.3 (the sufficient condition) is not posed here. Under the shared model it is mission I's goal at . Contributions are welcome on the ODE layer (truncation, comparison and Gronwall bounds for Carathéodory systems), on linear SDEs with bounded feedback, and on the Itô product rule. These parts are reusable well beyond this paper.
Many optimization problems in shape analysis, computer vision, numerical linear algebra and statistics have a feasible set that is not a vector space but a Riemannian manifold: spaces of curves modulo reparametrization, the Stiefel and Grassmann manifolds, fixed-rank matrices. On such a set the classical recipe "add a multiple of the search direction to the iterate" is not available, and line-search methods replace it by a retraction, a map that follows a tangent direction back onto the manifold (Absil, Mahony, Sepulchre 2008).
Quasi-Newton methods are the most widely used line-search methods in the Euclidean setting, and BFGS is the most popular of them. Transferring BFGS to a manifold raises a specific problem: the Hessian approximation lives on the tangent space at , while the next one must live on the tangent space at , so a vector transport between tangent spaces enters the update.
Timeline:
Let be a smooth manifold modelled on a real Hilbert space , with a Riemannian inner product and norm on each tangent space . For , is its differential, a functional on with dual norm .
A retraction is a family of smooth maps with and . Write , a function on the vector space , with derivatives and .
Algorithm 1 produces iterates . The step satisfies the Wolfe conditions with :
The BFGS direction solves for a bounded bilinear form on . With and , the next form is defined on through an invertible linear map :
The analysis uses the angle and the Rayleigh quotient .
Assume:
Then there is with
The rate is not specified: the goal asserts only R-linear convergence, the shape of the result.
The result. Proposition 10 is a global convergence guarantee for a quasi-Newton method on manifolds, with no restriction to a neighbourhood of the minimizer and no finite-dimensionality. It applies to Riemannian shape spaces of curves, where the paper's numerical experiments take place. The paper's superlinear-rate theory (Proposition 12, Corollary 13) starts from this linear rate.
Formalizing it. The result is proved on paper but has not been machine-checked. A formal proof also checks the delicate points of the infinite-dimensional argument, in particular the use of traces and Fredholm determinants of trace-class perturbations of the identity. The statement as printed needs a correction: the printed bound fails at , and the formal goal bounds , as the appendix's own final display does.
The Euclidean proof idea of bounding the eigenvalues of uniformly does not work for BFGS: those eigenvalues are not uniformly controlled. The Byrd–Nocedal argument replaces them by trace and determinant estimates, which show that a fixed fraction of the iterations have well-conditioned angles. In infinite dimensions the trace and the determinant of do not exist. One must work with , which is trace class, and with the Fredholm determinant, and show that isometric transports leave these quantities invariant. That invariance is exactly where the isometry hypothesis enters. Lemma 9 is also not a finite-dimensional triviality: positive definiteness of does not give coercivity, and a separate compactness-free argument is needed.
The manifold is a Mathlib ChartedSpace E M, with a complete real inner-product space, IsManifold 𝓘(ℝ, E) ∞ M, and a RiemannianBundle on TangentSpace 𝓘(ℝ, E). Every norm on a tangent space is the Riemannian one. is mfderiv, read as a functional on , and its norm is the operator norm.
Committed conventions and explicit readings:
A trivializing formalization is ruled out on three fronts. A sorry-free check on , with , and , shows that the run hypotheses are satisfiable. Every quotient in a statement has a positive denominator along such a run. The rate is quantified after the run and before .
Infrastructure that a complete development needs, and that is reusable beyond this mission:
The last item is absent from Mathlib, and contributions toward it are welcome. The paper's other main result, convergence of Fletcher–Reeves conjugate gradients (Proposition 15), is a separate mission. The superlinear-rate results (Lemma 6, Propositions 5, 7, 8, 12, Corollaries 11, 13) and the numerical §4 are out of scope.
A prophet inequality compares a gambler who sees independent random rewards one at a time, and must accept or reject each on arrival, with a prophet who sees all rewards in advance. The classical inequality of Krengel, Sucheston and Garling (1977–78, as cited in the paper) says that when only one reward may be kept, a single threshold rule earns at least half of , and Samuel-Cahn (1984) showed that the threshold can be chosen as a median. Such statements are the analytical core of sequential posted-price mechanisms: Hajiaghayi, Kleinberg and Sandholm (2007) observed that threshold rules are truthful online auctions, and Chawla, Hartline, Malec and Sivan (2010) showed that sequential posted prices approximate the optimal Bayesian revenue in many settings, with prophet inequalities for the feasibility constraint as the key technique.
When several items may be accepted subject to a combinatorial constraint, the natural constraints in this application are matroids (for example, at most items, or at most one item per group) and intersections of matroids (for example, bipartite matchings, which are intersections of two partition matroids). Kleinberg and Weinberg (STOC 2012) proved that for every matroid there is an online algorithm with expected payoff at least half of the expected maximum-weight basis, and that for the intersection of matroids the summed version of the same algorithm earns at least of the expected optimum. This mission formalizes the second result.
Timeline:
A finite ground set carries matroids with independent sets and closure operators . A set is feasible if it lies in . Each element has a random weight ; the weights are independent and has law . For a set , , , and .
An online weight-adaptive adversary reveals the elements one at a time; it chooses the -th element after learning , but without knowing or any other unrevealed weight. A threshold algorithm offers a threshold computed from what has been revealed and from the set already selected, and selects exactly when and .
The algorithm of the paper uses a ghost sample , an independent copy of . Let be a -maximum feasible set. For a set and each , is a set of maximum -weight with and , and . Put and . For a parameter , the summed thresholds are
and the algorithm of §4.2 uses . An algorithm has -balanced thresholds (Definition 3) if, for every input sequence with selected set and every disjoint from with ,
For every , all matroids on , all laws on with finite means, and every online weight-adaptive adversary, the algorithm of §4.2 with selects a set with
For this is the factor-2 matroid prophet inequality.
If a threshold algorithm has -balanced thresholds for some , then against every online weight-adaptive adversary
Proposition 2 for each matroid ; the identity between the two forms of ; properties (13) and (14) for the summed thresholds; the identities (20)–(21); and the inequalities (23)–(24) of Appendix A. Together with Proposition 3 these give the goal.
The bound gives a posted-price style selection rule for any feasibility constraint that is an intersection of matroids, with a guarantee depending only on ; the paper's §5 shows that a ratio of order is necessary. Section 6 of the paper turns the result into sequential posted-price mechanisms for multi-dimensional mechanism design, and that application needs the guarantee against the online weight-adaptive adversary, not only against a fixed order. The reduction "balanced thresholds imply an approximation" (Proposition 3) is reusable for other threshold constructions.
The result is proved in the paper; to our knowledge no machine-checked proof exists. The mission produces a formal proof of the guarantee, with the probabilistic part (the ghost-sample argument against an adaptive adversary) and the combinatorial part (the per-matroid exchange inequality) as separate milestones. The paper justifies the per-matroid use of Proposition 2 in one paragraph; because maximizes over the intersection rather than over , the description of as a maximum-weight basis of a contraction (Lemma 2 in the single-matroid case) does not apply verbatim, and the formal proof of that milestone is not a copy of the paper's single-matroid argument.
Two steps do not follow from routine bookkeeping. First, the inequality (23) compares the gambler's surplus, collected along an order that the adversary adapts to the realized weights, with the ghost sample's surplus on the random set . The index revealed at step is itself random, so the step "the weight of the element offered next is distributed as its ghost weight" has to be justified for an adaptively chosen index under a product measure; it fails for an adversary that may look at unrevealed weights. Second, the paper obtains (14) by applying the single-matroid Proposition 2 to each , but its proof of Proposition 2 describes as a maximum-weight basis of a contraction, which uses that is optimal for the matroid in question. Here is optimal only for the intersection , so the obvious transfer of the single-matroid argument does not go through as written and the per-matroid statement needs its own proof.
The ground set is a Fintype; the matroids are Mathlib's Matroid α, indexed by Fin p, each with ground set Set.univ; sets are Finset α. Weights are functions α → ℝ, the weight law is Measure.pi F, and every theorem assumes each F x is a probability measure with F x (Iio 0) = 0 and a finite mean. Expectations are Bochner integrals; under these assumptions every integrand is integrable. Ties in the maximizers and are broken by a fixed rule that does not depend on the weights. is taken disjoint from . The threshold on infeasible steps is a feasibility test in the selection rule. Adversaries and generic threshold rules are deterministic, see only revealed weights, and are measurable in them; randomized adversaries are mixtures of deterministic ones. Generic thresholds in Proposition 3, (23) and (24) are non-negative, as in the paper's .
The goal fixes the thresholds to the summed thresholds of §4.2 with , computed from the ghost-sample objects. A version in which the thresholds are free parameters assumed to satisfy (13)–(14) would be Proposition 3 itself and is ruled out; conversely, Proposition 3 does not mention the §4.2 thresholds.
A complete development needs: elementary facts about maximizers over finite families; matroid exchange properties (a bijective exchange between equal-size independent sets, available in Schrijver's book but not in Mathlib); submodularity of weighted-rank-type functions; and the independence argument for adaptively chosen indices under a product measure. The last two are reusable beyond this mission, as is Proposition 3. Proofs of individual milestones and of these auxiliary facts are welcome.