Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A retailer that sells products in categories must decide which products to offer in each category. When customers choose among the offered products according to the nested logit model, the expected revenue depends on the offered assortment in a nonlinear way, and the retailer's shelf space adds a knapsack constraint in every category. Gallego and Topaloglu (Management Science, 2014) show that the resulting space-constrained assortment problem is NP-hard even with a single nest (via Lemma 2.1 of Rusmevichientong, Shen and Shmoys, cited in the paper as 2009), give a factor-2 approximation through a linear program, and then, in Online Supplement C of the paper, refine the approach into an approximation scheme: for every desired guarantee , a polynomially sized family of candidate assortments per nest suffices.
The scheme follows the partial-enumeration idea of Frieze and Clarke (1984) for multi-dimensional knapsack problems, but has to work for a whole one-parameter family of knapsack problems, one for every value of a scalar , with a single collection of candidates fixed in advance.
There are nests and products . Product of nest has a preference weight , a revenue (no sign or order is assumed), and a space requirement ; nest has capacity with . An assortment of nest is a set ; it is feasible, , when . Write
For , problem (7) is , which equals the knapsack problem (10) . The quantity is the utility of product ; denotes the optimal value of (10). An assortment is -approximate at when for all .
For a set , problem (17) is the linear program
the LP relaxation of (10) with the products of fixed in the knapsack and every product whose utility exceeds the smallest utility in removed. Its optimal value is . Rounding a solution down gives the assortment . is the family of subsets of with at most elements.
For every , with , there is a collection such that
The paper writes ; the explicit bound above is of that order.
Together with Theorem 4 of the paper (an -approximate candidate per nest for every yields an -approximate assortment for the whole problem) and Theorem 2 (the best combination of candidates solves a linear program with variables), Theorem 9 gives, for every , an -approximation of the space-constrained nested logit assortment problem by a single linear program with constraints; for this is . It shows that the factor 2 of Section 5 is not a barrier of the method.
The result is proved in the paper. As far as the platform's records show, none of it is formalized; this mission produces a machine-checked proof of Lemma 8 and Theorem 9, including the explicit counting of parameter intervals that the paper only sketches.
A related but different construction, with large and small products and a continuous knapsack whose weights are preference weights, appears in the unconstrained variants of Davis, Gallego and Topaloglu (items NestedLogitVariants.PowersDelta.*); it is not reused here.
Two points resist the obvious argument. First, rounding down the plain LP relaxation of (10) drops one fractional product whose utility can be as large as the whole optimum, which is why Section 5 only reaches a factor 2; no choice of rounding of that relaxation alone does better. The guarantee has to come from the partially fixed problems (17), and their indicator constraint is delicate: it excludes only products of strictly larger utility than the least utility in , and a version that also excludes ties can cut off the optimal assortment of (10), and the comparison with is then lost.
Second, the collection must be fixed before . The optimal solution of (17) depends on through the ordering of the utilities, the ordering of the utility-to-space ratios and the signs of the utilities, which change only at the intersection points of lines. Because the feasible set of (17) itself depends on through the indicator constraint, the solution on an open interval between two such points need not remain optimal at its endpoints; the count must treat the breakpoints as pieces of their own.
ι; products are Fin n (0-based); assortments are Finset (Fin n), with for .NestedLogitVariants.LP.Model is referenced; its within-nest no-purchase weight is set to zero (I.vnp i = 0), which makes V and R the paper's and . The paper's extension is not formalized.Nat.ceil; is strict.Accelerated first-order methods for convex minimization, starting with Nesterov's 1983 scheme, reach the rate , which is optimal for the class of convex functions with Lipschitz gradient. Su, Boyd and Candès (NIPS 2014; JMLR 2016) showed that Nesterov's method is a discretization of the second-order ODE , and since then continuous-time inertial dynamics have been the main tool for designing and analysing accelerated algorithms: a Lyapunov argument for the ODE is found first, and then transcribed to the discrete scheme.
Nesterov-type methods oscillate. Adding to the dynamic a damping term driven by the Hessian, , attenuates these oscillations, and because is the time derivative of , time discretizations of such dynamics remain first-order methods. Attouch, Chbani, Fadili and Riahi (arXiv:1907.10536, Math. Program. 2020) develop this programme. This mission formalizes its first result: a convergence-rate theorem for the continuous dynamic with general damping and time-scale functions.
Timeline.
Let be a real Hilbert space with inner product and norm . Let be a convex function of class that attains its minimum at some point . Fix a starting time , a constant , and two non-negative continuous functions . These are the paper's standing assumptions (H).
A solution trajectory of
is a twice differentiable curve satisfying this equation at every . The coefficient is an asymptotically vanishing viscous damping, weights the Hessian-driven damping, and is a time-scale factor in front of the gradient.
When is differentiable, set
The rate in Theorem 1 is expressed through .
Assume is differentiable and the growth conditions
hold for all . Then and
The goal leaves and general. Specific choices are the companions below.
The paper's own proof steps, in order:
The result. Theorem 1 contains the rate of the continuous Nesterov dynamic as the case , , . It recovers the Attouch–Peypouquet–Redont theorem and the vanishing-coefficient system of Case 2 as special cases. The time scale gives faster rates when grows. For it also gives the integral estimate on , which is the continuous counterpart of the fast decay of gradients proved for the algorithms (IPAHD) and (IGAHD) later in the paper.
Formalizing it. The result is proved in the paper, and nothing about it has been machine-checked. The mission produces:
The energy estimate is an exact computation that has to match term by term. The cross terms cancel only because is chosen to match . That computation needs the chain rule in a Hilbert space.
The naive conclusion ", so integrate (4)" hides two analytic steps:
The (i) rate needs the positivity of from to divide by .
Lean conventions:
gradient f, and is fderiv ℝ (gradient f) x u.HasDerivWithinAt on . Values before are irrelevant, and derivatives at are one-sided.=O[atTop], with constants depending on all data.IntegrableOn on , never a bound on a Bochner integral that could be the junk value .These choices rule out trivial readings: Lean's zero value for the derivative of a non-differentiable function, an ODE with an unlinked velocity, and an integral that is zero because the integrand is not integrable. The goal assumes nothing about , or (4)–(6), which appear only in milestones.
Companion items:
Contributions are welcome: the chain rule for gradient along a curve, a monotonicity lemma for one-sided derivatives on Ici, and the integrability lemma for non-negative functions bounded by a non-increasing energy.
Many first-order methods for convex minimization — the forward–backward (proximal gradient) method, alternating minimization, trust-region and majorization–minimization schemes — produce sequences that decrease the objective by an amount proportional to the squared step and whose step controls a subgradient at the new point. Luo and Tseng (Ann. Oper. Res. 1993) used such conditions together with error bounds to derive convergence rates, and Attouch, Bolte and Svaiter (Math. Program. 2013) isolated them as an abstract definition of descent sequences analysed through the Kurdyka–Łojasiewicz (KL) inequality. Those analyses give convergence and asymptotic rates, but not explicit complexity bounds with the constants in view.
Bolte, Nguyen, Peypouquet and Suter (arXiv:1510.08234; Math. Program. 165, 2017) show that, for convex functions, the KL inequality yields such bounds: the values and iterates of every subgradient descent sequence are dominated by an explicit one-dimensional proximal recursion built from the desingularizing function. This is the paper's main theorem (Theorem 16), and the target of this mission.
Let be a real Hilbert space and proper, lower semicontinuous and convex, with and, after a shift, . The subdifferential is
and denotes its least-norm element, with when .
For , the class consists of the functions continuous on and on with , concave and . The function has the KL property on with desingularizing function if
A sequence is a subgradient descent sequence with constants if and, for every ,
Fix , put , and let , an increasing convex profile. Assumption (A): is Lipschitz continuous on with constant , and . With
is the one-dimensional worst-case proximal sequence.
If is a subgradient descent sequence with and (A) holds, then converges strongly to a minimizer and
Theorem 16 turns the qualitative KL convergence theory into explicit complexity: once a desingularizing function is known, the number of iterations needed to reach a given accuracy, for both the values and the iterates, can be read off a scalar recursion with constants , , taken from the method and the function. The authors apply it, through its corollaries, to obtain the linear rate of ISTA for -regularized least squares and complexity bounds for projection methods for convex feasibility problems. The bound on holds even when has a continuum of minimizers.
The theorem is proved in the paper and, to our knowledge, has no machine-checked proof. This mission asks for a Lean proof of Theorem 16 and of the six intermediate results its proof uses, each stated with the paper's exact constants.
The convergence part (Theorem 14) is set in an arbitrary Hilbert space: summability of the steps gives only a Cauchy sequence, identifying its limit as a minimizer needs a closedness property of that is not available in Mathlib for EReal-valued functions, and the degenerate cases ( or at some step) need separate treatment.
The complexity part requires one-dimensional analysis that Mathlib does not package: derivatives of the inverse on a closed interval, a descent inequality for when is Lipschitz only on , and monotonicity of the scalar resolvents . The obvious approach, comparing with one step at a time with the same step size, fails: the sequence is itself a proximal sequence for , but with step sizes that vary with and are not known in advance.
EReal satisfying the published GammaZero (never , somewhere finite, convex epigraph, lower semicontinuous), with CompleteSpace H. is the published subgrad; with is the hypothesis " and vanishes somewhere".IsDesingularizer; is deriv φ, used only on .EReal.Useful infrastructure, reusable beyond this mission: the inverse-function derivative on an interval, the one-dimensional descent lemma with a derivative Lipschitz on a closed interval, and monotonicity of scalar resolvents. Contributions of these as separate lemmas are welcome.
Mean-field games were introduced by Lasry and Lions (2007) and by Huang, Malhamé and Caines (2006) as limits of stochastic differential games with many symmetric players, each interacting with the others only through the empirical distribution of their states. The limit replaces a game of coupled players by one representative player facing a deterministic flow of distributions that it must reproduce. That flow is the equilibrium condition. The limit object is easier to solve. Whether it says anything about the finite game it came from is a separate question: a mean-field equilibrium is useful only if the strategies it produces are nearly optimal for each of actual players.
Carmona and Delarue (SIAM J. Control Optim. 51, 2013) solve the mean-field game through the stochastic maximum principle. For drifts that are affine and costs that are convex, the equilibrium is the solution of a forward–backward SDE of McKean–Vlasov type. Its existence is the subject of the first mission of this series. This mission formalizes §4 of the paper. The strategies read off from that solution are an approximate Nash equilibrium of the -player game, with an explicit rate in .
The state space is and the control space is , both with the Euclidean norm. Each player has a private state , driven by its own -dimensional Brownian motion , the motions being independent. The dynamics are
where is affine and is a constant matrix. Player chooses a strategy , a process that is progressively measurable for the filtration of and satisfies . It pays
The costs , satisfy the paper's assumptions (A.1)–(A.7): joint convexity in with strong convexity in , regularity, local Lipschitz continuity in the measure argument for the 2-Wasserstein distance , and growth conditions.
On the mean-field side, let solve the McKean–Vlasov FBSDE (3.1), let , and let be the FBSDE value function. This is a function that is Lipschitz in with linear growth and satisfies . Let minimize the Hamiltonian over , and let be the mean-field cost (4.1). The candidate strategies are
where solves the particle system (4.2): the dynamics above, with each player using this feedback against the frozen flow . Each player needs only its own state.
There exist and positive numbers with such that, for every , every player and every admissible deviation ,
The constant and the sequence come before , the player and the deviation.
The milestones follow the proof, in attack order:
Large deviations are unprofitable for every player (4.27). A bounded deviation of one player keeps every player's cost above (4.28).
The theorem justifies the mean-field game as a model of large finite games. Solving one McKean–Vlasov FBSDE produces distributed closed-loop strategies. No player can improve its cost by more than by deviating, even with a strategy that uses all players' noises. The rate gives a quantitative meaning to "large ". The milestones (4.11)–(4.12) are a quantitative propagation-of-chaos result for the particle system driven by the decoupling field. Such results are used on their own in the numerics and statistics of interacting particle systems.
The result is proved in the paper. No part of it has been machine-checked, as far as the platform's records show. The work that remains is to formalize the known proof. That needs Wasserstein estimates for empirical measures (Lemma 4.1, cited by the paper without proof), Gronwall arguments for SDE systems, and the optimality of the mean-field control (Theorem 2.2, the first mission's milestone, used here through ). Sharper rates are known in low dimension (Fournier and Guillin, 2015). They would be welcome as variants, but they are not the target.
The obvious argument compares the deviating player's cost with the mean-field cost of the same strategy. It fails in two places. The deviation changes the empirical measure that every other player sees, so the other players' states are no longer independent copies of . It must be shown that one player of bounded energy moves the population's empirical measure by only in ((4.17)–(4.20)). The second problem is that the deviation is adapted to the filtration of all Brownian motions, larger than the one in which the mean-field control problem is posed. The comparison must survive this enlargement. Finally, nothing bounds the energy of a deviation a priori. Deviations of large energy have to be excluded separately by a coercivity estimate ((4.25)), and only then can the rate be obtained uniformly.
The data live on EuclideanSpace ℝ (Fin n), so every norm, and is Euclidean. Matrix norms are operator norms. is the published WassersteinDRO.Duality.wassersteinDistance 2, valued in . Measures carry Mathlib's σ-algebra on Measure, which on probability measures on coincides with the paper's Borel σ-field of weak convergence. The SDEs and BSDEs are the published Itô-process predicates of Peng (Peng1990.SMP.SolvesSDE, SolvesBSDE). Solutions also have almost surely continuous paths on . The game filtration is generated by and augmented by the null sets. Players are indexed by Fin N, so the paper's player is index .
The mean-field solution and the game live on two probability spaces. Only , and pass between them. The value function enters through its properties (3.3), the identity and joint measurability, as in Lemma 3.5. is the chosen minimizer of the Hamiltonian, with default ; by Lemma 2.1 the default is never used on . The assumptions also contain a standing convention the page does not write: and are Borel measurable. Without it the expected costs would not be expectations of measurable integrands. Moments and expected energies are lower Lebesgue integrals in . Costs are real expectations, finite under (A.5) for admissible strategies.
The statements exclude the trivializing readings:
The goal does not mention the decoupled copies or Lemma 4.1.
A complete development needs:
Contributions on any of these are welcome. Well-posedness of the deviated system (4.5) is used but is not stated on the page; a proof of it is also welcome.
A decision maker who chooses to minimize an expected cost rarely knows the distribution of the random parameter . What is available is a sample . Any rule that turns the sample into a cost estimate can disappoint: the realized expected cost may exceed the estimate. In a cost-minimization context such underestimates are more harmful than overestimates, which is why distributionally robust optimization replaces the unknown by a worst case over a set of distributions consistent with the data.
Van Parys, Mohajerin Esfahani and Kuhn (arXiv:1704.04118, Management Science 2021) asked which such rule is best. They define a data-driven predictor to be least conservative among all predictors whose probability of disappointment decays exponentially at a prescribed rate , and they prove that a single predictor, the worst-case expected cost over a relative-entropy ball around the empirical distribution, is the unique strong solution. Their main results are for a finite set of outcomes . Section 5 extends the predictor result to an arbitrary compact ; this mission formalizes that extension. The version used throughout is the arXiv preprint arXiv:1704.04118v3 (22 December 2019), and every index below is the preprint's.
Fix compact sets (decisions) and (outcomes), and a cost that is jointly continuous.
and strongly optimal if it is feasible and for all and every feasible .
Both halves are in the goal. The case of feasibility is the statement that is continuous.
with a minimizer , and with equality for .
Proposition 5, the dual representation (23) of itself, is included as a further item; the proof of Theorem 10 goes through Lemmas 3–4 and does not use it.
Theorem 10 says that, on any compact outcome space, no continuous predictor is less conservative than while keeping its disappointment probability below to first order in the exponent. Relative-entropy distributionally robust optimization is therefore not one choice among many ambiguity sets but the optimal one for this criterion, and the dual representation turns its evaluation into a one-dimensional convex problem. The paper also shows that the continuous-state analogue of its prescriptor result (Theorem 11) only holds up to an arbitrarily small shift, so the predictor statement formalized here is the clean part of the extension.
The results are proved in the paper; none is formalized. A complete development yields a formal Sanov-type weak large deviation principle for empirical measures in the weak topology, joint convexity and lower semicontinuity of the Kullback–Leibler divergence for probability measures on a compact metric space, and a measure-theoretic dual representation of a relative-entropy worst-case expectation. Mathlib has the Kullback–Leibler divergence klDiv and the weak topology on probability measures, but none of these three results.
The finite-state proof of feasibility bounds the disappointment through the large deviations upper bound over the disappointment set itself. On a continuous space that bound only holds over the closure in the weak topology (24a), and the paper notes that this invalidates the finite-state argument (p. 25). The rate must then be controlled on a larger, closed set of empirical distributions, where the strict inequality defining a disappointment is lost; this is where the mass that puts on the worst-case scenarios starts to matter, as the hypothesis of (41) shows.
Continuity of in the weak topology is the second obstacle. The supremum runs over an infinite-dimensional set of distributions, a worst-case distribution may put mass outside the support of , and the integrals involved can diverge or take the value . Weak convergence controls integrals of bounded continuous functions only, and is unbounded below at .
ProbabilityMeasure ↥Ξ for the Borel σ-algebra of the subtype, with Mathlib's weak-convergence topology. and are compact subsets of Euclidean spaces, is jointly continuous; these standing assumptions of §2 (p. 5) and §5 (p. 23) appear as hypotheses of every theorem. No other hypothesis is added. Nonemptiness of is automatic wherever a distribution on is in scope.InformationTheory.klDiv, valued in . It equals Definition 8, including the value when or when the log-likelihood ratio is not integrable.Real.log encoding would be wrong, since Lean sets . Predictors must be continuous for the weak topology; dropping continuity, or replacing the weak topology by a finer one, changes the problem.Contributions are welcome at every level: a Sanov upper and lower bound for empirical measures on compact metric spaces, convexity and lower semicontinuity of klDiv, and the measure-theoretic duality of Lemma 4 are each reusable beyond this mission.
A mean-field game describes a population of agents whose individual dynamics and costs depend on the distribution of the population's states. In a large population, an individual agent has negligible influence on that distribution but still responds to it. The mathematical problem is to find a control whose induced state law agrees with the distribution used to choose the control. Carmona and Delarue's 2013 analysis formulates this matching condition through a coupled stochastic system. Mean-field games were introduced independently by Lasry and Lions (2006–2007), through a coupled Hamilton–Jacobi–Bellman/Fokker–Planck system of partial differential equations, and by Huang, Malhamé and Caines (2006). Carmona and Delarue replace the PDE system by a probabilistic one, which handles costs of quadratic growth and degenerate noise without a uniform ellipticity assumption. Its existence theorem supplies the state-dependent control used later in the paper to construct approximate Nash equilibria for finite-player games.
The article first treats a control problem with a prescribed flow of probability measures, then imposes the requirement that the flow equal the law of the resulting state process. This mission concerns that self-consistent system and the regularity of its backward component. Proposition 3.7, a companion target, adds a uniqueness conclusion under the paper's monotonicity condition.
Fix a horizon , an initial state , an -dimensional Brownian motion , and unrestricted controls . The state has values in . Its drift is affine in state and control,
where is a probability measure on with finite second moment. The volatility is constant and uncontrolled. A running cost and a terminal cost determine the control problem.
The Hamiltonian is . Under convexity, it has a unique minimizer . The forward-backward stochastic differential equation (FBSDE) couples a forward state to an adjoint process and a noise coefficient . The forward equation uses the feedback ; the backward equation has driver and terminal condition . The McKean–Vlasov requirement sets at every time, giving the system (3.1):
This law matching is the extra condition beyond solvability for a prescribed flow.
All seven standing assumptions of Theorem 3.2 are retained. (A.1)–(A.3) specify measurable, bounded affine drift and running costs with a positive control-convexity constant . (A.4) gives local boundedness, differentiability, and convexity of the terminal cost. (A.5) controls growth and dependence on the measure argument using the 2-Wasserstein distance ; (A.6) bounds the control gradient at zero; and (A.7) is a weak mean-reverting condition on the spatial gradients at Dirac laws. A measure flow is bounded when its second moments are uniformly bounded over .
The goal is Theorem 3.2. It asserts existence of solving the self-consistent system. For every solution, there is an FBSDE value function and a constant such that
It also gives for every real . The constant belongs to each solution; the theorem does not assert a single universal value for all models.
The milestone sequence follows the article's stated results: Lemma 2.1 characterizes the Hamiltonian minimizer; Theorem 2.2 and Proposition 2.5 compare controlled costs; Lemma 3.5 establishes a frozen-flow solution and a decoupling function; Proposition 3.8 handles bounded spatial gradients; Lemmas 3.9 and 3.10 state the approximation and stability results; and the first sentence of §3.7 records solvability under stronger state convexity. The companion Proposition 3.7 asks for uniqueness when the running cost separates into a measure-dependent and a control-dependent part and the measure-dependent costs satisfy the Lasry–Lions monotonicity inequalities.
A solution of the self-consistent FBSDE identifies a law flow consistent with the feedback chosen from that same law. The value function represents the adjoint state as a deterministic function of time and the forward state. Its linear growth and Lipschitz regularity control how feedback changes when states move. Those properties are used in the article's subsequent approximate-Nash analysis for the finite-player game; without them, its estimates cannot be stated in the same form. The moment conclusion gives the integrability needed for those comparisons.
The paper proves these results. The formalization task is to express its stochastic equations, probability laws, measure dependence, and analytic assumptions precisely enough that the known argument can be checked in Lean. The reusable outputs include a Euclidean mean-field control model, a finite-moment measure-flow interface, and a componentwise stochastic solution predicate compatible with published Brownian-motion and Itô-process definitions.
For a prescribed measure flow, the control problem produces a forward-backward system, but this does not by itself make the resulting state law equal to the prescribed flow. Standard Lipschitz contraction arguments may give short-time solvability; the theorem allows an arbitrary fixed horizon. The argument must also preserve control convexity and quantitative estimates while passing from models with bounded spatial gradients to the stated growth conditions. The adjoint value function must work simultaneously across the full time interval, and the theorem requires moment bounds of every order at least one.
Lean uses EuclideanSpace ℝ (Fin d) for states and EuclideanSpace ℝ (Fin k) for controls, so all norms in the costs, moment conditions, and are Euclidean. A joint state-control norm is computed from the sum of the two squared Euclidean norms. Time uses ; measures with finite second moment use extended nonnegative moments, and is the published coupling-based definition. The measure-space sigma algebra is Mathlib's Giry sigma algebra, agreeing with the weak-convergence Borel sigma algebra on the probability measures here. Matrix bounds use operator norms.
The stochastic layer reuses published predicates for a standard Brownian motion, progressive processes, Itô integrals, SDEs, and BSDEs. The filtration is the Brownian filtration augmented by null sets. Peng's componentwise stochastic predicates use coordinate functions, so the Lean development converts between those and Euclidean states. Solutions include continuous trajectories and the square-integrability condition (2.14). The real cost expectations are used only in settings where the hypotheses ensure integrability. The Hamiltonian minimizer has a total-function fallback outside its existence domain, while Lemma 2.1 ensures that branch is never used in the theorems. Laws are formed only from measurable state variables. An arbitrary prescribed flow cannot replace the state law in the goal.
The following readings are fixed. (A.5)'s joint display for is two inequalities, one for and one for without the time and control arguments. Every assumption is imposed for and for measures in only; measurability of , and is required on that domain. Gradients of and are computed from the functions, not supplied as separate data. A solution of (2.13) or (3.1) is a progressively measurable triple with a.s. continuous forward and adjoint paths satisfying (2.14). Costs are real expectations; under the theorem's hypotheses the integrands are integrable, so no default value of the integral is used. In Proposition 2.5 the term is written as an expectation, equal to the page's term because is a.s. constant for the augmented Brownian filtration.
The statements exclude the trivializing encodings: the flow in (3.1) is the law of the forward process in every coefficient, not a free flow; distances and moments use Euclidean norms, not the coordinate supremum norm; the minimizer is the minimizer of , not a free feedback; moment and admissibility conditions are extended-valued integrals compared with ; and constants declared uniform by the article (Lemma 2.1's Lipschitz constant, Lemma 3.5's , Lemma 3.10's ) are quantified before the data they are uniform over.
Definitions of the model and solution class, proofs of the eight source-indexed milestones, the goal theorem, and the companion uniqueness result are in scope. The result concerns the source's full class of models satisfying (A.1)–(A.7), rather than a convenient special case.
Training data describe one probability distribution, while a deployed prediction rule may be evaluated under a nearby distribution. Distributionally robust learning measures a rule by its worst expected loss over a specified set of nearby laws. This changes the question from how well the rule fits the observed sample to how well it performs when probability mass can move. Wasserstein distance supplies a geometric notion of “nearby”: moving mass farther across the instance space costs more. The setting is relevant to the domain drift discussed by Lee and Raginsky and to Wasserstein robust optimization as developed by Mohajerin Esfahani and Kuhn.
Theorem 1 of Lee and Raginsky's 2018 paper gives a finite-sample answer. It controls the local worst-case risk at the true population law using quantities computed from the empirical law, and also controls the empirical local worst-case risk using population quantities. Both assertions are simultaneous over the entire loss class. This mission concerns exactly those two probability inequalities and the displayed claims in Appendix C.1 that support them. The source is the pinned arXiv:1705.07815v2 preprint, containing the NeurIPS 2018 paper and its supplementary appendix.
The instance space is a bounded Polish metric space with distance . A probability measure generates independent observations . Their empirical distribution is . A loss has risk under a probability law . The class consists of upper semicontinuous losses satisfying for every and , as in Assumption 2 of the paper.
For , the -Wasserstein distance is the least th-power transport cost over couplings of and , raised to the power . The Wasserstein ball consists of probability laws with , where . The local worst-case risk is
The dual expression uses the envelope for . To measure the size of , let be its uniform-metric covering number at radius . The entropy integral is . These symbols match the local Lean setting and the source's notation.
For every , the mission goal is the conjunction of the paper's two displays:
The seven milestones preserve displayed claims from Appendix C.1: the deterministic comparison through the supremum deviation , its concentration and symmetrization bounds, the entropy-integral estimate with constant , the fixed- probability bound, and the integer-grid union and comparison with real multipliers. They are statements from the author's argument, ordered by their appearance. The goal retains both directions of the published theorem and every printed constant.
The first bound provides a sample-dependent certificate for the worst-case population loss of every member of at once. The second compares the robust empirical quantity with a population envelope. Together they make it possible to assess what a local Wasserstein ambiguity set buys in finite samples, rather than relying only on asymptotic convergence. The complexity term depends on the geometry of the loss class through its covering numbers, following a line of empirical-process bounds also seen in Bartlett and Mendelson's study of Rademacher complexity. Lee and Raginsky emphasize that this class complexity can reflect hypotheses outside the support of the data-generating law.
The mathematical theorem is proved in the 2018 paper; the particular declarations in this mission remain open Lean goals. A complete formal development would connect probability inequalities for supremum processes to the published Wasserstein distance and ball, make the entropy integral and its measurability consequences explicit, and verify both directions of the final bound. The reusable output includes a precise internal uniform covering number and a finite-sample Rademacher process for metric-space loss classes.
A fixed multiplier is easier to control than the infimum over all . A pointwise concentration bound alone does not produce a simultaneous statement over an uncountable multiplier set. The source's final formula contains a logarithmic multiplier penalty, and retaining its coefficient and the probability factor requires accounting for that parameter range exactly. Independently, the supremum over an arbitrary loss class is a genuine random variable only with enough regularity. The boundedness of individual losses does not by itself settle the measurability of their unrestricted supremum.
The envelope also mixes the metric geometry with empirical-process complexity. Estimating a class of envelopes must remain tied to the covering properties of the original class . Replacing the envelope class by a finite hand-picked subclass or assuming the desired concentration inequality as a new hypothesis would change the theorem being formalized.
Lean uses a metric space with its Borel measurable structure and a Polish-space instance, together with boundedness of the whole carrier. The Wasserstein distance and ball are imported from the published WassersteinLinOpt.Ball definitions. Because the carrier is bounded, every probability measure has a finite th moment, matching the source's . The ball is a subtype of probability measures; its supremum is taken only over feasible laws. Sample outcomes are functions Fin n → 𝒵, and the product measure gives their independent common law. The empirical law is a normalized finite sum of Dirac masses, while is written as its equal finite average.
The paper does not specify whether covering centres must lie in . This formalization uses the internal covering number, whose centres do; its value is at least the external covering number. The entropy integral is extended nonnegative and is required to be finite in statements that convert it to a real number. This disclosed restriction avoids the default conversion of to zero and supports the separability needed for expected suprema. Milestones using also require to be nonempty, so a real supremum never acquires the empty-family default value. The empty-class case of Theorem 1 remains valid because its failure events are empty.
The source writes minima over nonnegative real multipliers and positive integers. The Lean statements use bounded-below real infima; for the final bound, the appendix's comparison holds at every multiplier, so this reading is at least as strong as the printed minimum. All radii are positive, , , and where it appears. Failure probabilities use outer measure of the sample event directly, with no conversion through toReal. The goal never quantifies over arbitrary distributions outside the Wasserstein ball, and expectations of supremum processes are guarded by the finite-entropy hypothesis. Contributions are welcome on the concentration, symmetrization, covering-number, and transport-risk interfaces as well as the goal itself.
Best subset selection asks for the linear model that fits a response best using only a few of many candidate predictors. In its penalized form it is the least-squares problem with an penalty, the number of nonzero coefficients. The problem is NP-hard. Mixed-integer optimization can solve it to certified optimality at moderate sizes (Bertsimas, King, Mazumder 2016), but statisticians who fit whole regularization paths with tens of thousands of predictors need something faster. Hazimeh and Mazumder (arXiv:1803.01454, Operations Research 2020) proposed cyclic coordinate descent for the -penalized problem, the method that glmnet made standard for the lasso. Their algorithm underlies the L0Learn software package.
Coordinate descent on a convex smooth-plus-separable objective converges by classical arguments (Tseng 2001). Those arguments do not cover the penalty, which is discontinuous. The paper adds occasional spacer steps to plain cyclic coordinate descent and proves that the modified algorithm converges to a coordinate-wise minimum. This mission formalizes that convergence theorem.
Let be a model matrix whose columns have unit Euclidean norm, and let . For let
with and ; counts the nonzero coordinates. Problem (2) is . Its three named cases are (L0) (), (L0L1) () and (L0L2) (). .
Fix all coordinates but the -th. With unit-norm columns, minimizing over amounts to minimizing a scalar function of . The minimizer set is (7). The thresholding operator (12) picks one element of it:
A coordinate-wise (CW) minimum is a such that every minimizes in coordinate with the others fixed (Definition 2). A stationary solution is a whose lower directional derivative is nonnegative in every direction (Definition 1).
Algorithm 1 (CDSS) takes an initial point and a positive integer . It sweeps the coordinates cyclically. Each non-spacer step sets the current coordinate to and increments a counter for the resulting support. When the counter of a support reaches , a spacer step follows: one sequential pass over the coordinates of with the term switched off, . The counter of is then reset. The iterates count both kinds of step.
For (L0) and (L0L1) the paper adds Assumption 1: every columns of are linearly independent. It also adds Assumption 2, which constrains the initial point when : for (L0), and for (L0L1).
For (L0), (L0L1) and (L0L2), under Assumptions 1–2 in the first two cases, there are and a support with
The two parts share : the support stabilizes, and the limit is a CW minimum on that support.
Theorem 2 guarantees that exact cyclic coordinate descent on Problem (2), with spacer steps, has a limit, and that the limit is a CW minimum. That class is strictly smaller than the stationary solutions and the fixed points of iterative hard thresholding ((4), p. 5). It also serves as the inner solver of the paper's local combinatorial search (Algorithm 2, Theorem 4). So the guarantee transfers to the partial-swap-inescapable minima studied in the companion mission. Support stabilization (part 1) is also what reduces the asymptotic analysis to smooth strongly convex coordinate descent on a fixed support (Theorem 3).
The result is proved in the paper; no machine-checked version exists. A formalization would check the convergence argument for a discontinuous objective, where the bookkeeping of supports, counters and step indices is easy to get wrong. It would also provide a reusable Lean model of -penalized least squares and its thresholding operators.
The standard proof for cyclic coordinate descent needs a uniform decrease per step or a continuous objective. Neither holds here. A coordinate may switch between zero and a nonzero value infinitely often while decreases by arbitrarily small amounts, so the descent property alone gives neither support stabilization nor convergence of the iterates. Coordinates dropped infinitely often and coordinates added infinitely often must both be excluded. The tie-breaking rule in matters here: with the other choice on ties the algorithm is different. The exclusion of coordinates added infinitely often is only sketched in the paper (p. 43), and a complete proof has to supply it.
Vectors are Fin p → ℝ with 0-based indices. Every norm is written as an explicit sum; Mathlib's sup norm on function types is never used. Unit-norm columns, , and are hypotheses. The case , which the paper never names, is excluded from the statements about the algorithm's limits. is Real.sign. chooses the nonzero solution on ties, as in (12). The lower directional derivative takes values in EReal, since it is in directions leaving the support. Lemma 3 is stated with the condition on the support, taken from (5). The printed condition (8) omits it, and without it the equivalence fails for . Indices and pages throughout are those of arXiv:1803.01454v3.
Algorithm 1 is a deterministic state machine: iterate, cyclic pointer, the counter array Count, and a flag for a pending spacer step. The iterates are therefore defined from and , not quantified over. The pointer advances only on non-spacer steps, following the pseudocode box; the prose formula on p. 10 contradicts it. A statement about an arbitrary sequence satisfying a step predicate, or one that adds a step size or a sufficient-decrease hypothesis, would describe a different algorithm and is ruled out.
Useful infrastructure includes the scalar thresholding lemmas and coercivity of under Assumption 1 on supports of size at most . Contributions of proofs for any milestone are welcome, as are lemmas on the state machine (descent of each step type, the counter bookkeeping).
Adam (Kingma and Ba, 2015) is the default optimizer for training neural networks. At each step it keeps an exponential moving average of stochastic gradients and an exponential moving average of their squared coordinates, corrects both for their initialization at zero (the bias correction), and moves the iterate by coordinatewise.
Barakat and Bianchi (arXiv:1810.02263v4, SIAM J. Math. Data Sci. 2021) study Adam through the ODE method: as the step size with and , the interpolated iterates follow a non-autonomous ordinary differential equation. Their Theorem 3.2 shows that the trajectory of this ODE approaches the critical set of the objective. That leaves open whether the trajectory settles at a single critical point, and how fast. For gradient-like systems the classical answer goes through the Łojasiewicz gradient inequality (Łojasiewicz, 1963, for real-analytic functions), and the dissipative-systems framework of Haraux and Jendoubi (2015) turns such an inequality into convergence with a rate. This mission formalizes the paper's Theorem 3.4, which brings that conclusion to the continuous-time Adam dynamics.
Timeline.
Let be continuously differentiable with locally Lipschitz gradient , and let be locally Lipschitz. In the paper and . Its §7 uses only the two properties above, and so does this mission. Assume is coercive ( as ) and coordinatewise for every . Fix constants with .
The state is , and all vector operations are coordinatewise. The Adam field (3.3) is, for ,
and (ODE) is . A global solution with initial condition is a continuous that is continuously differentiable on , satisfies (ODE) for every , and has . The critical set is .
A number is a Łojasiewicz exponent of at if there are and with
Assumption 3.3 (the Łojasiewicz property) requires an exponent at every . It holds for real-analytic and semialgebraic .
The proof uses the Lyapunov function , where (3.4)–(3.5). It also uses its perturbation (7.11) and .
Assume Assumption 3.3 and that has empty interior in . Let be a global solution with initial condition . Then there is with as . Moreover, if is a Łojasiewicz exponent of at , then
for a constant (and, in the second case, some ) depending on the trajectory, and but not on .
The milestones follow the proof in §7.4:
Theorem 3.2 only places the limit points of the trajectory in . When contains a continuum of critical points, the trajectory could in principle drift along it forever. Theorem 3.4 excludes this under the Łojasiewicz property. It shows that continuous-time Adam has finite length and converges to one critical point, and it makes the speed explicit. The speed is polynomial with exponent in general and exponential when , which holds for instance at a nondegenerate critical point. The theorem places continuous-time Adam in the same class as gradient flow, heavy-ball dynamics and proximal methods.
The result is proved in the paper (§7.4, with the final integration delegated to arguments of Haraux and Jendoubi). It has not, to current knowledge, been machine-checked. The mission produces a formal proof, together with formal statements of the Lyapunov estimates (7.12)–(7.13) for the Adam ODE. The Łojasiewicz-rate step is reusable for other perturbed gradient-like systems.
The standard Łojasiewicz argument for gradient flow uses itself as the Lyapunov function, whose derivative is . For the Adam ODE neither nor works. decreases only at the rate , which says nothing about when the momentum is small. The system is also non-autonomous, with a field that is singular at and only locally Lipschitz in . As a result is only absolutely continuous, so all derivative inequalities hold only almost everywhere. A further obstacle is that the Łojasiewicz inequality at a single critical point does not by itself control the trajectory: the limit set is a connected compact subset of , and the inequality has to be made uniform on a neighbourhood of it. Finally, the rate has to be stated for an arbitrary exponent at the limit point, not only for the uniform exponent the argument produces.
is EuclideanSpace ℝ (Fin d) and is the product E × E × E, whose Mathlib norm is the maximum of the three Euclidean norms. This does not change any statement here, which concern , , separately. and are abstract, under the hypotheses of §7 (ContDiff ℝ 1 F, LocallyLipschitz (gradient F), LocallyLipschitz S, coordinatewise, coercivity as Tendsto F (cocompact _) atTop). Under Assumption 2.2 the paper's and satisfy these, so the statements imply the printed ones. A solution is a map ℝ → E × E × E constrained only on . The field uses in place of (the paper's extension, p. 12) and is never evaluated at . Statements are made for every global solution; there is exactly one (Theorem 3.1, a separate mission).
The polynomial bound is stated for , because Lean's real power gives while the paper's right-hand side is at . The constant is quantified before . A version with chosen after , or one that assumes converges, would be trivial and is not the theorem. (7.13) states absolute continuity of on every together with the almost-everywhere derivative bound, since an almost-everywhere bound alone says nothing about .
A complete development needs the Lyapunov calculus of §7.1, compactness of the trajectory, the limit-set theory behind Theorem 3.2, the uniformisation of the Łojasiewicz inequality on a compact connected set of critical points, and the Haraux–Jendoubi integration lemmas. Contributions to the last two are reusable beyond this mission and are welcome, as are proofs of the individual milestones.
Complexity bounds for first-order methods (proximal gradient, forward–backward splitting, alternating minimization) rest on a quantitative description of how a function grows away from its set of minimizers. Two such descriptions are in common use. An error bound controls the distance to the minimizers by the function value; a Kurdyka–Łojasiewicz (KL) inequality controls the function value by the size of the subgradients, after a reparameterization . KL inequalities with an explicit are what the convergence-rate analysis of descent methods needs (Attouch–Bolte 2009, Bolte–Sabach–Teboulle 2014), while error bounds with explicit constants are known for many concrete problem classes (Hölderian bounds for convex polynomials, Hoffman-type bounds, the bounds surveyed by Pang 1997).
Bolte, Nguyen, Peypouquet and Suter (arXiv:1510.08234v3, Math. Program. 165 (2017)) show that for convex functions on a Hilbert space the two notions coincide, with essentially the same function , as soon as has a mild regularity property they call moderate behavior. This mission formalizes that equivalence (Theorem 5 of the paper) together with the subgradient-curve results its proof rests on.
Timeline:
Let be a real Hilbert space and a proper, convex, lower semicontinuous function. Its minimizers form the set , assumed nonempty, and is normalized so that . The subdifferential of at is
and is the set of points where it is nonempty. For , is the element of least norm of ; for one sets . The band is , and is the ball of radius around .
A desingularizing function is an element of
satisfies the KL inequality on with if there, and the error bound with residual function if there. has moderate behavior if on for some .
A subgradient curve issued from is a curve with and for almost every ; its length between and is .
Let , , , and . Then
and, if on ,
Both directions form the single goal theorem.
and then converges strongly to a minimizer.
Theorem 5 makes the computation of desingularizing functions a matter of proving error bounds. Since every semi-algebraic or subanalytic has moderate behavior (Lemma 4 of the paper), any known error bound with such a residual function yields a KL inequality with the same function up to the constant , and through the complexity theorem of §4 of the paper an explicit iteration bound for subgradient descent sequences. The paper uses this route to obtain the linear rate of ISTA for -regularized least squares and complexity bounds for projection methods.
The result is proved in the paper; to our knowledge none of it is machine-checked. A formalization adds three things: a Lean development of the Brézis subgradient semiflow on a general real Hilbert space (cited, not proved, in the paper), a checked proof of the length estimate of Theorem 27, and the two directions of Theorem 5 on top of them. The semiflow results are reusable well beyond this paper: they underlie the continuous-time analysis of proximal and gradient methods.
Direction (ii) is elementary convex analysis. Direction (i) is not: the error bound is a statement about , while the hypothesis only constrains subgradients on a band, and the minimizer realizing the bound must be produced. The paper produces it as the strong limit of the subgradient curve from , which requires the existence and regularity theory of the nonlinear evolution equation in an infinite-dimensional Hilbert space (Theorem 1), the energy identity along the curve, and strong (not merely weak) convergence. In finite dimensions compactness would supply limit points; in a Hilbert space Bruck's theorem only gives weak convergence, and it is the length bound of Theorem 27 that upgrades it. Neither the semiflow nor absolutely continuous Hilbert-valued curves with their a.e. derivative calculus are developed in Mathlib to the extent this needs.
[NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]; EReal with the published GammaZero f (never , somewhere finite, convex epigraph, lower semicontinuous) and the published subdifferential subgrad. is the hypothesis " and attains "; is argminSet f, is Metric.infDist.IsDesingularizer r0 φ for ; values outside are irrelevant, and is deriv φ, used only on .A constraint satisfaction problem (CSP) asks whether variables can be assigned values from a finite domain so that every constraint, drawn from a fixed list of allowed relations, is satisfied. A promise CSP (PCSP) relaxes the question: given two templates and with a homomorphism , distinguish instances satisfiable in from instances not even satisfiable in the weaker . Approximate graph colouring (colour a graph with more colours than its chromatic number) is the standard example. For CSPs, the resolution of the Feder–Vardi dichotomy conjecture by Bulatov and Zhuk (FOCS 2017) ties tractability to the existence of polymorphisms satisfying non-trivial identities; for PCSPs no such dichotomy is known, and the question of which polymorphism families yield algorithms is open in general.
A polymorphism of a PCSP is a function mapping tuples of rows satisfying the strict constraints to columns satisfying the weak ones. Brakensiek, Guruswami, Wrochna and Živný (arXiv:1907.04383v3, SIAM J. Comput. 2020) give a single algorithm, BLP+Affine, that decides every PCSP with infinitely many symmetric polymorphisms, and extend it to block-symmetric polymorphisms. As a corollary the same algorithm solves all tractable Boolean CSPs of Schaefer's dichotomy (2-SAT, Horn-SAT and its dual, linear equations mod 2).
Timeline, as recorded in the paper's introduction:
A signature is a set of symbols with arities . A relational structure on a finite domain gives, for each , a relation . A homomorphism is a map sending every tuple of , componentwise, into ; is a promise template when one exists.
An instance has variables and constraints , , where is a tuple of variables. is satisfiable in if some assignment sends every into .
A polymorphism of of arity is such that for every and every matrix whose rows lie in , applying to each column gives a tuple in . It is symmetric if it is invariant under all permutations of its arguments.
The Basic LP has rational unknowns , a distribution on for each variable, and , a distribution on for each constraint, linked by the marginal conditions when is the -th variable of . The affine relaxation is the same system of equations in integer unknowns , , with no sign constraints.
The BLP+Affine algorithm (Figure 1) finds a relative interior point of , rejecting if there is none; restricts the affine system to by forcing wherever and wherever ; and accepts if and only if the restricted system has an integer solution. It correctly solves (Definition 1) if it accepts every instance satisfiable in and rejects every instance unsatisfiable in .
The hypothesis is a property of the template alone; the conclusion quantifies over all instances.
The same conclusion when contains block-symmetric polymorphisms of arbitrarily large width: is split into blocks, each of size at least , within which is invariant.
Theorem 2 gives one algorithm that decides every PCSP with an infinite family of symmetric polymorphisms, without knowing or evaluating the polymorphisms; it subsumes the BLP-then-AIP algorithm of Brakensiek and Guruswami for Boolean templates and applies over any finite domain. Theorem 3 extends this to block-symmetric families, which covers nearly all known tractable Boolean PCSPs, including 1-in-3-SAT versus NAE-SAT, whose alternating threshold polymorphisms are block-symmetric but not symmetric.
The results are proved in the paper. No machine-checked formalization of PCSPs, polymorphisms or the Basic LP is known to exist; Mathlib has no theory of constraint satisfaction. This mission produces a formal model of promise templates, instances, polymorphisms, the two relaxations and the algorithm's acceptance condition, together with a formal proof of the correctness theorem. The same model is the starting point for the characterization theorem (Theorem 4) treated in the companion mission.
Completeness is routine. Soundness is the substance: from a rational LP solution and an integer solution of the refined affine system one must produce an actual assignment in , using a polymorphism whose arity is chosen only after the instance is known. The natural first idea, clearing denominators of the LP solution and feeding the resulting multiplicities to a polymorphism, needs a polymorphism of exactly the arity the denominators dictate; with polymorphisms of only some arities it fails, and the paper's introduction notes that the LP alone does not suffice there. An integer affine solution, on the other hand, may have negative entries, which are not multiplicities. The paper stresses that the affine system must be the one refined by the support of a relative interior point: an arbitrary solution of the unrefined lattice gives no control on where the negative entries sit. In the formalization, the counting step (the columns of the matrix built from the constraint multiplicities have the variable multiplicities) and the passage from equal multiplicities to equal values of a symmetric function require explicit combinatorics on finite tuples, and the existence of a maximal-support LP solution requires an averaging argument over the finite set of coordinates.
All declarations are in the namespace PCSPBLPAff.Symmetric. Conventions:
Fintype and DecidableEq; variables are Fin n, constraints Fin m, and a constraint's scope is a function Fin (ar R_j) → Fin n, possibly repeating variables.The acceptance condition must not be replaced by "the LP is feasible and has a solution", nor by an affine solution vanishing outside the support of an arbitrary LP solution; the first is a different algorithm and the second bypasses footnote 1.
Contributions welcome: proofs of the milestones, in particular the combinatorial lemma that a symmetric function takes the same value on tuples with the same multiplicities, and the averaging argument for maximal-support solutions; the block-wise version for Theorem 3.
Many stochastic differential equations used in physics, biology and Bayesian sampling are ergodic: their law converges to an invariant measure , and quantities of interest are averages . Estimating such averages by simulation requires a numerical method whose accuracy does not deteriorate as the simulated time grows. Two obstacles meet here. First, the drifts of interest (the FENE polymer model, Langevin dynamics with polynomial potentials) are not globally Lipschitz, and for such drifts the explicit Euler–Maruyama method with a uniform timestep has moments that blow up as the step tends to zero (Hutzenthaler, Jentzen, Kloeden 2011). Second, standard strong error bounds grow exponentially with the time horizon, which makes them useless for long-time averages.
W. Fang and M. B. Giles (Ann. Appl. Probab. 30 (2020) 526–560) answer both with an adaptive timestep: the step is chosen from the current state, small where the drift is large. On a finite interval they prove strong convergence of order ; for a class of contractive ergodic SDEs they prove that the moments of the numerical solution and its strong error are bounded uniformly in time. The second result is the subject of this mission. It underlies the paper's multilevel Monte Carlo estimator for invariant measures.
Earlier work on the same problem used tamed schemes, which modify the drift instead of the step: Hutzenthaler, Jentzen, Kloeden 2012 on finite intervals and Sabanis 2016 with a time-uniform rate. An adaptive Euler–Maruyama scheme of a different form, with error control, was shown to converge and to be stable by Lamba, Mattingly, Stuart 2007.
Let carry a filtration and a -dimensional standard Brownian motion with respect to it. On (Euclidean norm , inner product ) consider
with drift and diffusion ; matrices carry the Frobenius norm .
Given a timestep function , the adaptive Euler–Maruyama scheme is
For let be the last grid time not after . The piecewise-constant interpolant is and the continuous interpolant is .
The hypotheses are:
Under Assumption 9, with bounded, satisfying Assumption 8 and satisfying Assumption 3, for every there is such that, with computed with timestep ,
The constant is fixed before and ; uniformity in is the content of the theorem.
The remaining step from (52) to Theorem 6 is a time-uniform bound , obtained as in the finite-time analysis of §6.2.
Theorem 6 says that the adaptive scheme tracks the true solution with error of order forever, not merely on a fixed window. Combined with ergodicity, it bounds the bias of long-time averages of the scheme uniformly in the averaging horizon, which is what the paper's adaptive multilevel Monte Carlo method for invariant measures (§3) needs. Theorem 5 is of independent use: it shows that the adaptive scheme preserves the time-uniform moment bounds of a dissipative SDE, a property the uniform-step Euler scheme lacks for superlinear drift.
All results here are proved in the source; none is open. To our knowledge none has a machine-checked proof. A complete formalization would give the first verified strong convergence result for an adaptive-step SDE scheme, and the infinite-horizon energy estimates (45)–(47) and the error inequality (52) would be the first verified time-uniform estimates of this kind.
The timestep is random and depends on the state, so the grid times are stopping times rather than fixed numbers, and the number of steps up to time is random. Standard discrete Grönwall arguments, which iterate over a deterministic grid, do not apply directly; neither does the usual argument that the scheme is an Itô process with adapted, piecewise-constant coefficients, which must be rebuilt for random grids.
The obvious route to a time-uniform bound — a finite-time bound with constant followed by — fails because grows exponentially. Uniformity has to come from an exponential weight ( in (45)–(47), in (52)) that converts dissipation or contractivity into a bound that survives division by the weight, with every constant independent of and of the timestep function.
The state space is EuclideanSpace ℝ (Fin m); diffusion values are EuclideanSpace ℝ (Fin m × Fin d), whose norm is the Frobenius norm. Times are in ℝ≥0, grid indices start at , and is deterministic. The grid is defined by recursion; the index is the least with and equals the junk value on the event that the grid never passes (a null event under the hypotheses). Moments are lower Lebesgue integrals ∫⁻ … ‖·‖ₑ ^ p in with real exponents, never Bochner integrals. A solution on is a process that solves the SDE on every horizon , in the sense of the published definition SabanisEuler.Shared.IsSolution. Existential constants are placed before every quantifier they must not depend on: before in Lemma 3, before , , and in Theorem 5, before , , , and in Step 2, before and in Theorem 6. A constant chosen after , or a moment that is a Bochner integral of a possibly non-integrable function, would make these statements trivial; both are ruled out. Pages are the journal's printed pages (PDF page + 525).
Two deviations from the printed text are deliberate. Theorem 6 additionally assumes : its proof invokes Theorem 5, whose Assumption 7 contains this bound, which Assumption 9 does not imply, and the introduction (p. 527) assumes "a bounded and non-degenerate diffusion coefficient". Each is assumed measurable. Separately, the printed (47) has in its last term; the formalized inequality uses , as the expansion and the source's (48) require. The undefined word "nondegenerate" in Assumption 7 is not encoded.
A full development needs the Itô formula for applied to Itô processes with random-grid coefficients, the Burkholder–Davis–Gundy inequality, and moment bounds for Brownian increments over stopping-time intervals. These are reusable well beyond this mission. Contributions of any of them, or of proofs of the deterministic inequalities (45) and (47), are welcome.
Stochastic differential equations (SDEs) model physical, biological and financial systems whose drift often grows superlinearly: the stochastic Lorenz equation, the stochastic van der Pol and Duffing–van der Pol oscillators, Langevin dynamics. Solutions are rarely explicit, so they are simulated by time-stepping schemes. For multilevel Monte Carlo methods (Giles 2008) the cost of a simulation is governed by the strong convergence rate, the speed at which tends to as the step size shrinks.
For superlinearly growing coefficients the classical Euler–Maruyama method diverges in (Hutzenthaler, Jentzen, Kloeden 2011). Tamed schemes repair this, and rate was proved for them under a global monotonicity condition: for all (Hutzenthaler, Jentzen, Kloeden 2012; Sabanis 2016). Most of the examples above violate that condition. Before this paper no strong rate was known for any time-discrete scheme for a multidimensional SDE with non-globally monotone coefficients.
Timeline. 2011: divergence of explicit Euler for superlinear drifts. 2012: tamed Euler, rate under one-sided Lipschitz drift and globally Lipschitz diffusion. 2012–2013: strong convergence without rates for non-globally monotone SDEs (stopped and tamed schemes). 2014: this paper (arXiv:1401.0295), rate for the stopped-tamed Euler–Maruyama scheme under the conditions below; published in Ann. Probab. 48 (2020).
Fix and . On a probability space with a normal filtration , is a standard -dimensional -Brownian motion. Matrices carry the Hilbert–Schmidt norm . Given coefficients and , is an adapted continuous process with
The taming map is . The stopped-tamed Euler–Maruyama scheme with steps is and
The whole increment, drift and noise together, is tamed, and the scheme freezes once it leaves a ball whose radius grows slowly as .
The conditions use a Lyapunov-type function and a function . The generator is , where is the -th column of . For partitions with mesh , the same recursion run in continuous time on defines interpolations .
Let , , and with . Let be with polynomially growing derivatives. Let satisfy , , and , and assume for
Then there is such that for all ,
The constant is not specified. Only the rate is asserted, and that is the stable content of the result.
In the proof's order:
Theorem 1.3 gives strong rate , and with it the complexity bounds of multilevel Monte Carlo, for SDEs with non-globally monotone coefficients. The paper's applications include the stochastic Lorenz equation with bounded noise, the stochastic van der Pol and Duffing–van der Pol oscillators, a model from experimental psychology and overdamped Langevin dynamics. The perturbation estimate, Theorem 2.10, is a separate tool. It compares a solution with any Itô process, so it also gives local Lipschitz dependence on the initial value and, in the paper's §3.2, rates for Galerkin approximations of SPDEs.
All results listed here are proved in the paper, and none has been machine-checked so far. This mission produces Lean statements of the goal and of every numbered step of its proof. The development needs Itô calculus for , a localization argument, exponential-moment bounds via Lyapunov functions, and calculus for the taming map. Several of these pieces are reusable well beyond this paper.
The obvious argument is Gronwall's lemma applied to . It needs the global bound , which fails for the Lorenz and van der Pol drifts: there the one-sided Lipschitz "constant" grows with . The difficulty is to control a random, state-dependent Gronwall exponent . That requires exponential integrability of and along both the solution and the scheme. For the scheme it holds only because of the taming and the stopping, and only up to an error of the right order.
EuclideanSpace ℝ (Fin d). Diffusion values are the published Diffusion d m, whose norm is the Hilbert–Schmidt norm the paper uses throughout. Time is .SabanisEuler.Shared.IsSolution / IsItoProcess. The normal filtration is right-continuity plus completion, and is the published IsWienerMartingale, a Brownian motion on . For , the paper's cylindrical Wiener process is exactly such a Brownian motion. All processes are hypotheses; existence is never claimed.For a real symmetric matrix, the largest eigenvalue is the maximum of the quadratic form on the unit sphere, and it is computable to any accuracy in polynomial time. Tensor eigenvalues, introduced independently by Lim (2005) and Qi (2005), extend this picture to higher order: they are the stationary values of the cubic form on the unit sphere. They appear in multilinear statistics, signal processing, hypergraph theory and polynomial optimization, and for these applications the symmetric case is the natural one.
Hillar and Lim, in Most Tensor Problems Are NP-Hard (J. ACM 2013), show that the eigenvalue problem stays NP-hard when the tensor is required to be symmetric (their Theorem 9.3). The proof is short once one ingredient is available: a theorem of Nesterov (2003), in a form corrected by Hillar and Lim, that expresses the stability number of a graph as the maximum of an explicit cubic polynomial over a sphere. This mission formalizes that chain.
Let be a simple graph on , . A set of vertices is stable if no two of its members are adjacent; the stability number is the size of a largest stable set, so .
Put and write a vector of as , with indexed by vertices and indexed by pairs of vertices. The tensor has entry at the six orderings of the triple of coordinates for every non-adjacent pair , and elsewhere. It is symmetric: its entries do not change under any permutation of the three indices.
For a real 3-tensor the cubic form is , and a real is a unit -eigenvalue of if
Finally, for . In Lean these are TensorNP.SymEigen.stabTensor, cubicForm, IsUnitL2Eigenvalue and lambdaL, and is Mathlib's SimpleGraph.indepNum.
That is, is an eigenvalue of , and no with is. This is the statement on which the paper's -query reduction rests; nothing is claimed about .
both sides finite. The paper uses it in §10 to transfer Theorem 9.3 to the spectral norm and the best rank-one approximation of symmetric tensors.
The result. Theorem 9.3 places symmetric tensor eigenvalue among the NP-hard problems of Hillar and Lim's Table I, and through Banach's theorem (Theorem 10.2 of the paper) the same holds for the largest singular value, the spectral norm and the best rank-one approximation of a symmetric 3-tensor. These are the quantities computed by higher-order power methods and by moment-based estimators, so the result marks where the matrix theory stops transferring.
Formalizing it. All results here are proved in the literature; none is machine-checked. Nesterov's theorem, which rests on the Motzkin–Straus theorem for the complement graph, is not on the platform or in Mathlib, and its formal statement settles the constant that the original paper got wrong by a factor (Hillar–Lim, footnote 12). Banach's theorem on symmetric multilinear forms is likewise absent from Mathlib and is useful well beyond this mission.
The tensor identity (milestone 2) is bookkeeping. The analytic content sits in two places. First, Nesterov's theorem: the obvious route, fixing and maximizing over by Cauchy–Schwarz, reduces the cubic problem to a quartic one in , whose value still has to be identified with ; that identification is the Motzkin–Straus theorem, which is not available in Lean and is itself a nontrivial optimization over the simplex. Second, the passage from a maximum to an eigenvalue needs a Lagrange multiplier argument on the sphere, and the symmetry of is what makes the gradient of the cubic form match the eigen-equation. Part (b) of the goal needs a further, unprinted observation relating every unit eigenpair to the cubic form. Banach's theorem has no short proof; the classical arguments go through polarization estimates or a variational argument specific to symmetric forms.
ι → ι → ι → ℝ on a finite index type. For the index type is the disjoint union of the vertices Fin v and the pairs ; this is with coordinates labelled by name instead of by the paper's enumeration . Vertices are .SimpleGraph.indepNum, real analysis on finite-dimensional spaces, Lagrange multipliers). A Motzkin–Straus theorem for SimpleGraph and Banach's theorem for symmetric trilinear forms are both reusable beyond this mission; contributions of either, or of a general "maximum of a symmetric cubic form on the sphere is an eigenvalue" lemma, are welcome.The spectral norm of a matrix, its largest singular value, is computable in polynomial time to any accuracy. Its analogue for 3-tensors appears in the analysis of multilinear systems, in the best rank-1 approximation of a data array, in quantum information (the geometric measure of entanglement), and in the injective norm of tensor products. Hillar and Lim, Most Tensor Problems Are NP-Hard (J. ACM 60(6), 2013, Article 45; final version arXiv:0911.1393v5), show that, in contrast with matrices, deciding whether a fixed nonzero rational number is a singular value or the spectral norm of a rational 3-tensor is NP-hard (their Theorems 6.5 and 1.10).
The proof is a reduction from the clique number of a graph. It combines three classical ingredients: the theorem of Motzkin and Straus (1965), which expresses as the value of a quadratic program over the simplex; a theorem of Banach (1938) on the spectral norm of symmetric tensors; and an observation from He, Li and Zhang (2010) on maxima of sums of squared bilinear forms. Deciding is one of Karp's (1972) NP-complete problems.
A real 3-tensor is an array with trilinear form . With the Euclidean norm , its spectral norm is
A real is a unit -singular value of if there are unit vectors with
for all : the stationarity conditions of on a product of unit spheres.
Let be a simple graph on , , with edges , , and clique number . Let be the standard simplex, the adjacency matrix and the all-ones matrix. For a positive integer set and . Let , and let be the maximum over unit , of the multilinear form
The graph tensor has as entry the coefficient of in (26).
For every graph on vertices and every enumeration of its edges:
so is the largest for which is a unit singular value of . The paper's -query Turing reductions rest on exactly this.
The result. The goal shows that a single comparison with of the spectral norm, or of the singular-value spectrum, of an explicit rational tensor of size encodes whether . It is the step that makes the spectral norm, the largest singular value, and (through §7) the best rank-1 approximation of a 3-tensor NP-hard, whereas all three are polynomial-time for matrices. It explains why the higher-order power method and its relatives carry no global guarantees, and it is the starting point for inapproximability results such as the paper's Theorem 1.11.
Formalizing it. The results are proved on paper; none of them is formalized. Motzkin–Straus, Banach's polarization theorem for symmetric 4-tensors, and the He–Li–Zhang identity are classical results that are not in Mathlib and not on the platform; each is reusable well beyond this mission (Turán-type bounds, polynomial optimization over spheres, injective norms). The mission also checks the paper's construction at the level of indices and constants.
The construction of is explicit, and the comparison with is arithmetic once is known. Everything rests on the three cited theorems. Motzkin–Straus is an optimization statement over the simplex whose maximizers may lie on the boundary and need not be unique, so a first-order computation at an interior critical point does not settle it. Banach's theorem asserts equality, not equality up to a constant: the standard polarization identity bounds the 4-linear form by its diagonal values only up to a factor. Proposition 6.10 is where the paper's own argument is loose: the 4-linear form it introduces is not symmetric, so (24) does not apply as printed. Finally, the singular-value clauses require that the maximum of a trilinear form on a product of spheres is a stationary value. This must be proved, not assumed.
Tensors are arrays Fin l → Fin m → Fin n → ℝ with 0-based indices: the paper's is A (i-1) (j-1) (k-1). The Euclidean norm is Real.sqrt (∑ i, x i ^ 2). Suprema and maxima are sSup of sets that are nonempty and bounded under the stated hypotheses; where the paper's "max" carries content (Motzkin–Straus, (22), §7), attainment is stated with IsGreatest/IsLeast. The graph is a SimpleGraph (Fin v) with , clique number Mathlib's SimpleGraph.cliqueNum, and its edges are enumerated by an arbitrary Fin e ≃ G.edgeSet. Every statement holds for each enumeration, so the tensor depends on the choice and the conclusions do not. is a rational tensor, read over by casting.
Explicit readings of the paper:
This is the mathematical core of a polynomial-time Turing reduction, not an NP-hardness theorem. The polynomial size of , the -query procedure, the scaling to a general fixed , and the NP-completeness of CLIQUE (Karp 1972, cited) are not formalized. Theorem 1.11 and Corollary 1.12 are out of scope.
Two formalizations would make the goal trivial, and both are excluded. One is dropping the unit-norm constraint, which makes every nonzero number a singular value. The other is a spectral norm taken as a supremum over all vectors without normalization, which makes it unbounded and junk-valued; here the quotients are normalized.
Contributions are welcome on each milestone. Motzkin–Straus, Banach (24) and He–Li–Zhang are self-contained and reusable. Lemma 6.11 and milestone 7 need Cauchy–Schwarz and a Lagrange-type stationarity argument on spheres, which Mathlib supports through IsLocalExtrOn and the Lagrange multiplier files.
Conic optimization over the exponential cone models entropy, relative entropy, logistic regression, log-sum-exp and geometric programming. Unlike the nonnegative orthant, the second-order cone and the semidefinite cone, the exponential cone is not symmetric (self-scaled), so the Nesterov–Todd primal-dual machinery that makes solvers such as SeDuMi and MOSEK fast does not apply as is. Dahl and Andersen (Math. Program. 194 (2022) 341–370) describe the nonsymmetric-cone algorithm implemented in MOSEK (version 9.2 in the paper's experiments). Its central new ingredient is a corrector for nonsymmetric cones, an analogue of Mehrotra's predictor-corrector that is responsible for much of the practical performance of symmetric-cone solvers. The paper reports that the corrector gives a substantial and consistent reduction in iteration counts across its test sets.
Timeline. Nesterov and Todd (1997, 1998) built primal-dual methods for self-scaled cones. Nesterov, Todd and Ye (1999) and Tunçel (2001) studied primal-dual scalings for general cones, Tunçel proving polynomial complexity of an infeasible method without a corrector under bounded scalings. Skajaa and Ye (2015) gave a homogeneous method for nonsymmetric cones with a Runge–Kutta corrector. Myklebust and Tunçel (2014) analysed BFGS-type scalings. Dahl and Andersen (2022) introduced the third-order corrector studied in this mission.
Let be linear with full row rank, , , and let be a proper cone (pointed, closed, convex, with nonempty interior). A -logarithmically homogeneous self-concordant barrier (LHSCB) for is a convex function on with and . The primal problem minimizes subject to , ; the dual maximizes subject to .
The homogeneous model adds : , , , , . With , the residual is
a linear map whose -block is skew-symmetric. An iterate has , , and . The shadow iterates are and , with the conjugate barrier. A scaling is a nonsingular with and (the double secant equations (8)).
The affine direction solves , (11). The corrector is (16). For a centering parameter , the combined direction solves
Every solution of (18) satisfies
and for all
The goal fixes no constants beyond those of the direction itself. It holds for every solution of (18), not a chosen one.
The result. Lemma 4 says that a step of any length along the combined direction reduces the infeasibility residuals and the complementarity gap by exactly the same factor. Starting from a point with , the iterates satisfy and , so the algorithm needs no merit function to balance feasibility against optimality, in contrast with earlier nonsymmetric methods. The lemma also shows that adding the third-order corrector does not cost this property, which is what justifies using the corrector in MOSEK's exponential-cone solver.
Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of Lemmas 2–4, the §2 homogeneity identities or the barrier sum rule has a machine-checked proof. The mission produces a formal homogeneous model for a general proper cone with a general LHSCB and a formal account of third-derivative calculus for logarithmically homogeneous barriers. Both are reusable in any analysis of interior-point methods for nonsymmetric cones (power cones, generalized power cones, hyperbolicity cones).
The obvious reading of Lemma 4 as bookkeeping with the linear map stalls at the corrector: the term
in (18) involves the third derivative of the barrier, and nothing in linear algebra says how it
interacts with the complementarity gap. Controlling it needs the third-derivative calculus of logarithmically
homogeneous barriers. In Lean that means relating gradient, the Hessian as fderiv of the gradient, and the
third derivative as fderiv of the Hessian, and working with the symmetry of iterated Fréchet derivatives of a
function, for which the Mathlib interface is thin. A second obstacle is the augmented barrier: the
barrier properties of must be transported to on through the
splitting , including the boundary behaviour at the corner
, .
The first identity of Lemma 4 is misprinted in the paper as . A formalization following the printed statement would be false, not merely awkward.
Vectors of the augmented space are EuclideanSpace ℝ (Fin (n + 1)); is the first coordinates and
(resp. ) the last. is a continuous linear map and its Hilbert adjoint; full row rank
is surjectivity. Proper cones, the Hessian hess, the barrier class IsLogHomBarrier and the conjugate
conj are the published SelfScaledIPM.ShortStep.Setting. That barrier class adds three standard conditions
to the paper's two (boundary blow-up, the -inequality and a positive definite Hessian), which the
paper uses implicitly when it writes and calls a barrier. is a continuous linear
equivalence and the adjoint of . is fderiv ℝ (hess F) x u w and
is ContinuousLinearMap.inverse. Every inner product includes the homogenizing term .
Repairs, generalizations and specializations, each disclosed in the item statements:
The directions are predicates (" solves (11)"), and the lemmas quantify over all solutions. The hypotheses are satisfiable. For the linear program , , , , , , , , system (11) has the unique solution , , . Statements that hold only because a junk value appears are ruled out: every statement requires and , where , the inverse Hessian and the conjugate barrier take their true values. A formalization that drops from the inner products, or that fixes one solution of (18) instead of quantifying over all, would be a different lemma and does not count.
Welcome contributions: the general sum rule for products of cones, a Fin.append splitting library for
EuclideanSpace, and proofs of the homogeneity identities that can be reused by the series' other missions.
The explicit Euler–Maruyama scheme is the standard way to simulate a stochastic differential equation
on driven by a -dimensional Brownian motion. When and are globally Lipschitz it converges strongly with order in the step size (Kloeden and Platen 1992). Many models of interest in physics, chemistry and statistics have a drift that grows faster than linearly but points inwards, such as . For these the SDE is well posed and its solution has finite moments of all orders, but the uniform-step scheme does not: for , Hutzenthaler, Jentzen and Kloeden proved that as the step size , for every and (Proc. R. Soc. A 2011).
Several remedies have been proposed: implicit schemes (Higham, Mao and Stuart 2002; Mao and Szpruch 2013), the tamed Euler scheme (Hutzenthaler, Jentzen and Kloeden 2012), truncated schemes (Mao 2015). Fang and Giles (Ann. Appl. Probab. 2020) keep the explicit Euler–Maruyama update and change only the step: the timestep is a function of the current state, small where the drift is large. This mission formalizes their finite-time results: stability of the adaptive scheme (Theorem 1) and strong convergence of order (Theorem 3).
Let and be the Euclidean norm and inner product on , and the Frobenius norm of an matrix. Given a timestep function , the scheme (5) starts from , and sets ,
The grid is random: it depends on the path. For a time , is the last grid time not after ; the piecewise constant interpolant is and the continuous interpolant is
The hypotheses (Assumptions 1–4, pp. 528–530):
For in one dimension, satisfies Assumption 2.
Under Assumption 4, with satisfying Assumption 3 for an satisfying Assumption 2, for every there is such that for all
Theorem 1 shows that an explicit scheme, at the cost of one drift and one diffusion evaluation per step, is stable for one-sided Lipschitz drifts of polynomial growth, the class where the uniform-step scheme fails. Theorem 3 shows that refining the timestep function keeps the classical order . Combined with the paper's bound on the expected number of steps (Lemma 2) this gives order in terms of computational cost, and the results underpin the paper's adaptive multilevel Monte Carlo estimators. The uniform-in- form of Theorem 1 is what lets Theorem 3 apply the stability bound to the whole family .
The paper's proofs are complete on paper; none of these results has a machine-checked proof. Formalizing them needs a theory of Euler schemes on a random, state-dependent grid, which is not in Mathlib and is not covered by uniform-grid formalizations of tamed or implicit schemes. The definitions here (the scheme on random times, the projected K-scheme) are reusable for the infinite-time companion mission and for other adaptive schemes.
The obvious argument for the uniform-step scheme bounds moments step by step, using deterministic step sizes and independent Gaussian increments. Here the step depends on , so the grid times are stopping times and the increments have random length. Sums over steps become Itô integrals only after the scheme is written as the solution of , and moment bounds for those integrals need the Burkholder–Davis–Gundy inequality on a random grid. A second difficulty is that need not be reached: if decays fast enough, could converge below . Excluding this needs a positive lower bound on over bounded sets together with moment bounds, which the paper obtains by first analysing a version of the scheme projected onto a ball.
Lean conventions: is the published SDEState m (EuclideanSpace ℝ (Fin m)); matrices are the published Diffusion m d, whose norm is the Frobenius norm; is a standard -dimensional -Brownian motion in the sense of the published IsWienerMartingale; the SDE solution is any process satisfying the published IsSolution on (existence and uniqueness are not claimed). Times are in , indices start at , and is deterministic. The scheme is defined pathwise; the index of is a junk value when the grid never passes , an event of probability zero (Theorem 1). and are real-valued and their positivity is a hypothesis; each is assumed measurable. Moments are -valued integrals of extended norms, never Bochner integrals. Every existential constant is chosen before the parameter it must not depend on: before in Theorem 3 and its milestones, before (and ) in Theorem 1 and Step 3. Results the paper proves for inside its proofs are stated for . Pages are the journal's printed pages (PDF page + 525).
A formalization that places the constant after , uses a deterministic grid, or allows would be trivially true or a different theorem; these are ruled out by the statements.
Contributions welcome: proofs of the milestones, and of general facts they need (Burkholder–Davis–Gundy, moments of Brownian increments over stopping-time intervals, Grönwall's inequality for -valued functions).
The classical Chernoff bound controls the probability that a sum of independent, nonnegative, uniformly bounded random variables deviates from its mean, with exponentially small tails governed by the Kullback–Leibler divergence between two Bernoulli laws. Many problems in numerical linear algebra, graph sparsification, compressed sensing and randomized algorithms instead require control of a sum of independent random matrices: the smallest singular value of a random matrix with independent columns, the spectrum of a sampled Laplacian, or the conditioning of a random submatrix. For these, what matters is not a scalar sum but the extreme eigenvalues of a random positive-semidefinite matrix.
Ahlswede and Winter (2002) introduced a matrix version of the Laplace transform method and proved a matrix Chernoff bound for identically distributed summands. Tropp's paper (arXiv:1004.4389, Found. Comput. Math. 2012) replaced the Golden–Thompson step of their argument with Lieb's concavity theorem, obtaining a master tail bound for independent sums, and derived from it matrix Chernoff, Bernstein and Azuma inequalities that require no identical distribution and lose only a dimensional factor. This mission formalizes the matrix Chernoff inequalities of §5 of that paper.
Timeline:
All matrices are complex matrices with . For a self-adjoint (Hermitian) matrix , and are its algebraically largest and smallest eigenvalues. The semidefinite order means that is positive semidefinite (psd). Functions of a self-adjoint matrix are defined spectrally: if then ; this gives the matrix exponential and, on positive-definite matrices, the matrix logarithm .
A random matrix is a measurable map on a probability space , and its expectation is taken entrywise. The matrix moment generating function of is .
The objects of the mission are independent random Hermitian matrices that are almost surely psd contractions: and . Their average expectation has extreme eigenvalues
and the binary information divergence is
In Lean these are lambdaMax, lambdaMin, mexp, mlog, mean and binDiv in the namespace MatrixTail.Chernoff.
Corollary 5.2 (Matrix Chernoff II), the form usually quoted: with , the extreme eigenvalues of ,
Theorem 5.1 matches the strongest scalar Chernoff bound for independent, non-identical Bernoulli trials, up to the factor , which cannot be removed (coupon collector, Remark 5.6). Corollary 5.2 is the version used in applications: lower bounds on the smallest singular value of matrices with independent columns (Remark 5.4), spectral sparsification, column subset selection and random sampling of matrices. Remark 5.5 derives from it the expectation bound .
The results are proved in the paper, from Lieb's concavity theorem. As far as is known, no machine-checked proof of a matrix Chernoff inequality exists in Lean or Mathlib. A formalization yields a reusable statement for the random-matrix and randomized-numerical-linear-algebra literature, and the milestones (the master bound, the single-logarithm corollary and the semidefinite mgf bound) are reusable beyond this mission.
The scalar Chernoff argument uses for independent . For matrices unless and commute, so the trace of the mgf of a sum does not factor. The Golden–Thompson inequality handles two summands but does not extend to three, which is why the Ahlswede–Winter bound needed identical distributions. The master bound (Theorem 3.6) requires Lieb's concavity theorem, which has no counterpart in Mathlib. Corollary 3.9 in addition needs operator concavity of the matrix logarithm, and Lemma 5.8 needs the transfer of a scalar inequality to the semidefinite order through the spectral calculus.
Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d]; the semidefinite order is Mathlib's MatrixOrder (A ≤ B ↔ (B − A).PosSemidef). exp and log of a matrix are the continuous functional calculus cfc. , are sSup/sInf of the real spectrum. Expectation is entrywise. Random matrices are measurable with respect to the Borel σ-algebra on matrices, independence is iIndepFun, and the probability measure is a probability measure. The summands are Hermitian for every outcome; "psd" and "" hold almost surely. The sequence has terms wherever an average appears. An infimum over is stated as a bound for every admissible ; integrability of is a hypothesis only in Theorem 3.6 and Corollary 3.9, where the summands are unbounded. In Lean , so at the boundary values the divergence is finite where the paper's is ; this only weakens the stated bound.
A formalization in which (empty spectrum, ) or (the average ) were allowed, or in which the range of were dropped, would state a different, partly false theorem; these cases are excluded.
A complete development needs Lieb's theorem or another route to the master bound, operator concavity of the logarithm, the spectral mapping theorem and the transfer rule for the functional calculus on Hermitian matrices, monotonicity of the trace exponential, and the scalar optimization in . Contributions of any of these as stand-alone lemmas are welcome.
A data curator holds a database of records and wants to publish answers to a large family of statistical questions about it without revealing any individual record. Differential privacy (Dwork, McSherry, Nissim, Smith 2006) makes the requirement precise, and the most basic questions are counting queries: what fraction of the records satisfy a given predicate? Blum, Ligett and Roth (arXiv:1109.2229, JACM 2013) showed that a single private release can answer every query of a class to error once the database has size roughly , so that the sample size depends on the class only through its VC-dimension, a quantity from learning theory.
This mission formalizes the converse in §3.1 of that paper: the dependence on the VC-dimension cannot be removed. On databases of fewer than records, every differentially private mechanism has constant error on some query of . The argument is an early instance of the reconstruction attack idea of Dinur and Nissim (2003): accurate answers to many counting queries determine the database, and a mechanism that determines its input cannot be private.
Let be a set (the data universe). An input database of size is a tuple . A predicate is a map , and its counting query is
A class of predicates is identified with its class of counting queries. A finite set is shattered by if every function is the restriction of some ; the VC-dimension is the supremum of the sizes of shattered sets.
A mechanism maps each input to a probability distribution on an output space ; an output is read through an answer map . Two inputs are neighbours if they differ in exactly one entry. The mechanism is -differentially private if for all neighbours and all measurable events . It is -useful for if for every input , with probability at least over , every query is answered to within :
In the paper the output is a synthetic database and .
There is an absolute constant such that for every universe , class , size with , and : every -differentially private mechanism that is -useful for on databases of size satisfies
Theorem 3.11 shows that the VC-dimension term in the paper's upper bound is necessary: for a class of VC-dimension , no private mechanism is accurate on databases of size below , whatever its running time. It thereby locates the sample complexity of private query release between and up to accuracy and privacy factors, a gap that later work on private learning and on fingerprinting codes studied in detail (Bun, Ullman, Vadhan 2014).
The theorem is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it produces a checked reconstruction-attack lower bound for differential privacy, together with the corrected statement disclosed below: the printed proof drops the failure probability of the two reconstructions, and keeping it shows that the conclusion requires below , not merely "bounded away from 1". Milestone 3 records the inequality the argument actually yields.
The combinatorial core (Lemmas 3.12 and 3.13) is elementary. The difficulty lies in the last step, which compares the output distributions on two different inputs. The paper argues about a uniformly random , a random element and a random , and the swapped set . Privacy applies to one fixed pair of neighbouring inputs and one fixed event, while the reconstruction guarantee only controls , not whether a particular element is recovered. The "probabilities" of the printed proof mix the mechanism's randomness with the random choice of , , , and they are not the probability of any single event under any single , so the privacy inequality cannot be applied to them as written. The reconstruction event must also be measurable, which depends on the readout, and the failure probability must be carried through both reconstructions. A proof that sets , as the printed one does, does not prove the stated theorem.
Fin n → X with ; the empty database is excluded because every mechanism is private on it and there. In the proof, a set is given to the mechanism as any injective listing of its elements.PrivLearn.Generic.Neighbors); read literally, it would make every mechanism private and the theorem false. Under this reading and are neighbours, so the paper's factor becomes .ans. Synthetic-data mechanisms are the special case databases, so the lower bound covers a larger class of mechanisms. The hypotheses require IsProbabilityMeasure (M z) and the measurability of o ↦ ans o φ for . Without the first, the zero measure is private; without the second, a mechanism into a trivial -algebra would be private and "useful".PrivLearn.Generic.Privacy (neighbours, IsDP) and Vershynin's HighDimProb.Chaining.Shatters and vcDim. Contributions needed: subsets of shattered sets are shattered, and yields a shattered set of size exactly ; measurability of the argmin reconstruction; the averaging/bijection argument. The first two are reusable beyond this mission.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.
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.
Mean–variance portfolio selection (Markowitz, 1952) trades off the expected terminal wealth of an investor against its variance. In a dynamic setting the problem is time-inconsistent: the variance is not a conditional expectation of a function of terminal wealth, so the dynamic-programming principle fails, and a strategy that is optimal when computed at time is no longer optimal when re-evaluated at a later time. A standard response is to treat the investor at each time as a separate player and to look for a subgame-perfect equilibrium strategy, which no future self wishes to deviate from locally (Björk–Murgoci, Ekeland–Lazrak, and others).
Hu, Jin and Zhou (arXiv:1111.0818v1; SIAM J. Control Optim. 50(3), 2012) define open-loop equilibria for a general class of time-inconsistent stochastic linear–quadratic (LQ) problems and characterize them through a flow of forward–backward SDEs. Their §5 applies this to mean–variance investment in a complete market with a random risk premium, where the weight on expected wealth depends on current wealth (a state-dependent risk aversion, motivated in Björk–Murgoci–Zhou, 2014). Earlier equilibrium results for mean–variance investment (Basak–Chabakauri, 2010; Björk–Murgoci–Zhou) work with deterministic or Markovian coefficients and within feedback classes.
This mission is the third of a series on the paper. Mission I formalizes the general sufficient condition (Theorem 3.2); Mission II treats deterministic coefficients and coupled Riccati equations (Theorem 4.4). This mission targets the explicit mean–variance equilibrium of Theorem 5.4.
Fix a horizon and a probability space carrying a standard -dimensional Brownian motion with its filtration ; write . The market has a deterministic bounded interest rate and a progressively measurable, essentially bounded risk premium with values in . A strategy is a progressively measurable with (the class ); the wealth under solves
At time , with current wealth , the investor's cost is
This is the case of the paper's general LQ problem, with , , , , , ; the mission states it that way. For , and an -measurable square-integrable , the spike perturbs on a short window. A strategy with wealth is an equilibrium (Definition 2.1) if, for all such and ,
The equilibrium is built from , , and two backward SDEs: an indefinite stochastic Riccati equation for ,
and a linear BSDE (5.13) for whose coefficients involve and . A process gives a BMO martingale if for all stopping times .
If solves (5.8) with bounded and , and solves (5.13) with bounded, then
is an equilibrium: the closed-loop wealth exists, and for every closed-loop wealth the strategy satisfies Definition 2.1.
Theorem 5.4 gives the equilibrium of a time-inconsistent mean–variance investor in closed form, linear in current wealth, for a random risk premium. With a deterministic premium it reduces to explicit formulas (§5.4), and for it recovers the equilibrium of Basak–Chabakauri and Björk–Murgoci; for it differs from the feedback equilibrium of Björk–Murgoci–Zhou, which shows that open-loop and feedback equilibria are different notions. The random premium is what makes and the feedback gain unbounded.
The result is proved in the paper; nothing here is formalized elsewhere. The mission produces machine-checked statements of the equilibrium, of solvability of the Riccati-type BSDE (5.8), and of the integrability of a linear SDE with BMO-type coefficients, on the platform's published stochastic-calculus substrate. The definition of BMO martingales and the encoding of open-loop equilibria are reusable beyond this paper.
The verification step that most readers try first, plugging into the wealth equation and applying standard SDE estimates, fails: the gain is unbounded, because is only BMO, so the closed-loop SDE is linear with non-Lipschitz-bounded random coefficients and neither existence of the wealth nor follows from standard theory (Proposition 5.3). The BSDE (5.8) has a driver with quadratic growth in and a singular factor ; it is not covered by the standard theory of stochastic Riccati equations and its solution must be bounded away from zero for the feedback to make sense. Uniqueness in (5.8) and solvability of (5.13) rely on BMO-martingale and change-of-measure facts (Kazamaki) that are not in Mathlib. Finally, the equilibrium property is a statement about every and every perturbation, and the sufficient condition (Theorem 3.3) needs the limit behaviour of conditional expectations as .
Everything is built on the published definition Peng1990_SMP_Stochastic (Brownian motion, , Itô integrals, SDEs and BSDEs as relations). The general LQ model, the spike, the conditional cost and Definition 2.1 are in Model; the adjoint equation on , and condition (3.4) in Adjoint; the market, , , BMO, (5.8), (5.13) and (5.14) in Market. Conventions the statements commit to:
The goal does not assume the BMO properties of and (they are conclusions of Propositions 5.1–5.2), does not assume deterministic or (that is the special case of §5.4), and keeps , ; a formalization that assumes any of these, or that admits the junk value on a non-null set, proves a different theorem. Theorem 3.3, the sufficient condition used in the last line of the proof, is the case of Mission I's goal and is not restated here. Welcome contributions: a BMO and Girsanov library on the Peng substrate, existence for quadratic BSDEs, and a proof of the sufficient condition.