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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
In statistical learning a hypothesis is chosen from a class using samples drawn from an unknown distribution , and its quality is measured by the risk . When the distribution at deployment time may differ from the one that generated the data (domain drift, adversarial perturbation, model misspecification), a natural replacement is the worst-case risk over a neighbourhood of . Distributionally robust optimization with Wasserstein neighbourhoods takes these neighbourhoods to be balls in an optimal-transport distance, which compare distributions through the geometry of the instance space instead of through likelihood ratios. Wasserstein balls also contain distributions with support different from that of , which divergence balls do not.
J. Lee and M. Raginsky, Minimax statistical learning with Wasserstein distances (NeurIPS 2018, arXiv:1705.07815), give generalization guarantees for the empirical version of this procedure, the local minimax ERM. Their analysis rests on the strong duality theorem of Gao and Kleywegt (arXiv:1604.02199), which turns the supremum over a Wasserstein ball into a minimization over one real multiplier . This mission formalizes their Theorem 2, the excess-risk bound for a class of uniformly Lipschitz hypotheses, together with the steps of its proof. The source is the arXiv v2 preprint, which contains the NeurIPS camera-ready text and the supplementary appendices.
The instance space is a Polish space (complete separable metric space) with metric , and it is bounded: (Assumption 1). Fix . The -Wasserstein distance between Borel probability measures is
the infimum over couplings of and . For a radius the ball is .
The hypothesis class consists of upper semicontinuous functions with (Assumption 2). The local worst-case risk and the local minimax risk are
Given i.i.d. samples from with empirical distribution , the local minimax ERM is .
Assumption 3 asks that every be -Lipschitz with one constant : . The complexity of is measured by the entropy integral
where is the covering number of in the uniform metric. The dual integrand of Gao–Kleywegt duality is .
Under Assumptions 1–3, for every , with probability at least ,
Theorem 2 says that robust ERM over a uniformly Lipschitz class is nearly optimal for the robust risk at the unknown distribution, with excess of order and explicit constants. The dependence on enters only through ; at the bound does not depend on and recovers the usual rate of ordinary ERM. The paper derives Corollaries 1 and 2 (regression with a Lipschitz link, and Gaussian-kernel classes) and the domain-adaptation bound of Theorem 4 from it. Lemma 1, which confines the dual multiplier to a fixed interval, is also used outside the theorem: Remark 3 proposes it as the search range for the fixed- adversarial training of Sinha et al.
The result is proved in the paper; to our knowledge none of it has been machine-checked. What this mission adds is a verified version of a complete distributionally robust generalization argument: Gao–Kleywegt strong duality on a bounded Polish space, the multiplier bound, symmetrization and bounded differences for a class indexed by a function and a real parameter, and a Dudley entropy bound for that joint class. The paper's appendix states the Rademacher bound with a stray constant that belongs to a different assumption (Assumption 4); the milestone states the bound without it, which is what the proof gives and what the constant of (10) needs.
The obvious route bounds uniformly over . That needs uniform control of the dual multiplier for every and every empirical distribution, and without it the class is indexed by an unbounded , so its complexity is infinite. Lemma 1 resolves this only for the minimizers, which is why the argument is organized around and an achiever rather than a uniform bound.
The formal difficulties are separate. Strong duality with attainment of the minimum is a measure-theoretic theorem about couplings on a Polish space (existence of optimal couplings, measurable selection of near-maximizers), none of which is in Mathlib for Wasserstein balls. The supremum over must be shown measurable before its expectation means anything. Dudley's chaining bound over a separable, infinite index set is also missing from Mathlib in the form needed here. Finally, the theorem does not assume that is attained, while the paper's proof uses an achiever , so a complete proof needs an approximation argument that the paper does not write out.
MetricSpace with BorelSpace and PolishSpace instances, and Assumption 1 is Bornology.IsBounded (Set.univ : Set 𝒵). is Metric.diam univ.WassersteinLinOpt.Ball.wassersteinDist and wassersteinBall. Membership in is automatic on a bounded space.∀ f ∈ ℱ, ∀ z z', f z' - f z ≤ L * dist z' z, with one quantified before , and is a disclosed pin.ω : Fin n → 𝒵 with law Measure.pi (fun _ => P), and . "With probability at least " means the outer measure of the failure set is at most , for .Classical.choose. Such a selection exists exactly when empirical minimizers exist, which display (7) presupposes.Trivializing formalizations are ruled out:
toReal, and an infinite is never converted to .A complete development needs:
The last three are reusable well beyond this mission. Contributions of any of these as stand-alone results are welcome, as are proofs of the milestones.
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.
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 .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.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.
Prove Lieb’s concavity theorem (Theorem 8.1.1, also stated as Theorem 3.4.1): for fixed Hermitian H, the function A ↦ tr exp(H + log A) is concave on positive-definite matrices. This is the deterministic foundation of Chapter 3’s probabilistic argument.
Milestones follow the book’s route through generalized Klein, relative-entropy nonnegativity, variational trace formulas, operator Jensen, matrix perspectives, and joint convexity of relative entropy. Logarithm and trace-exponential monotonicity are included as reusable comparisons. The domain allows noncommuting positive-definite matrices without trace normalization.
Source: Tropp, January 2015 version, Chapter 8. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Control the spectral norm of a matrix series with independent standard Gaussian or Rademacher coefficients. The goal is Theorem 4.1.1, including its variance identity, expected-norm estimate, and tail bound for rectangular complex matrices.
Milestones are the Gaussian and Rademacher matrix mgf/cgf estimates (Lemmas 4.6.2–3) and the Hermitian series bound (Theorem 4.6.1). The formulation keeps the source’s constants, both coefficient laws, and the zero-variance case. The shared Chapter 3 tools connect these transform estimates to concentration.
Source: Tropp, January 2015 version, Chapter 4. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Replace ambient matrix dimension by intrinsic dimension, the ratio of trace to spectral norm. The goal is intrinsic Matrix Bernstein (Theorem 7.3.1). Intrinsic Matrix Chernoff (Theorem 7.2.1) is a second major target within the mission.
Supporting milestones include the generalized Laplace bound, intrinsic-dimension trace estimate, block-diagonal identities, Hermitian Bernstein, and the expected-norm corollary. The statements retain the source’s constants, threshold restrictions, and matrix-valued mean or variance bounds. Nonzero proxies keep intrinsic dimension well-defined; the expectation constant is universal.
Source: Tropp, January 2015 version, Chapter 7. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Control the spectral norm of a sum of independent, centered, bounded rectangular random matrices. The goal is Matrix Bernstein (Theorem 6.1.1), including the variance identity and both expected-norm and tail estimates.
Milestones cover Hermitian dilation, variance additivity, the bounded-summand mgf/cgf estimate (Lemma 6.6.2), and Hermitian Bernstein (Theorem 6.6.1). Chapter 3 supplies the general Laplace-transform machinery. The formulation uses the Euclidean operator norm, preserves the one-sided eigenvalue assumption in the Hermitian result, and includes deterministic zero sums.
Source: Tropp, January 2015 version, Chapter 6. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Bound the extreme eigenvalues of a sum of independent positive-semidefinite random matrices. The goal is the complete Matrix Chernoff theorem (Theorem 5.1.1): both expectation estimates, both tails, and the identities for the mean’s extreme eigenvalues.
The supporting milestone is the matrix mgf/cgf estimate (Lemma 5.4.1); Chapter 3 supplies the master bounds. The Lean statement retains the different lower- and upper-tail deviation ranges, permits zero mean eigenvalues, and handles a zero summand bound explicitly.
Source: Tropp, January 2015 version, Chapter 5. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.
Develop the reusable matrix Laplace-transform method behind Tropp’s concentration inequalities. The goal is Theorem 3.6.1: upper and lower tail and expectation bounds for sums of independent Hermitian random matrices, expressed through their matrix cumulant-generating functions.
Milestones cover the eigenvalue tail and expectation bounds (Propositions 3.2.1–2), probabilistic Lieb inequality (Corollary 3.4.2), and trace-cgf subadditivity (Lemma 3.5.1). This mission also supplies the series’ shared spectral, probability, and dilation definitions. Lieb’s underlying concavity theorem is the Chapter 8 goal.
The Lean statements give bounds for each admissible transform parameter, with explicit integrability hypotheses; optimization recovers the source’s infimum/supremum forms.
Source: Tropp, January 2015 version, Chapter 3. Lean statements compile; proofs remain open.
How many Euclidean symmetries can a real plane algebraic curve of degree have? Rotational symmetry of a curve is classically detected from the monomials of its equation in the complex coordinate : a rotation of order about the origin can preserve the curve only if the differences of the nonzero monomials satisfy a congruence modulo (Lebmeir and Richter-Gebert, Section 4; Lebmeir, Theorem 5.4). Bounds on the number of symmetries in terms of the degree enter symmetry detection algorithms (Alcázar, Lávička and Vršek) and incidence geometry: Pach and de Zeeuw, Lemma 2.6 use a bound of on the number of isometries of a curve in a distinct-distances argument.
The note Sharp symmetry bounds for real algebraic curves (C. Perassi, 2026; PDF) determines the sharp bounds, classifies the curves attaining the rotation bound in degree , and describes their Möbius geometry. This mission is the complete Lean formalization of that note.
Let be irreducible in , of total degree , and let , identified with a subset of through . Assume that is infinite and is not a circle. Write for the group of Euclidean isometries of with , and for its orientation-preserving subgroup (the rotations and translations preserving ).
For an integer and a nonreal with , the extremal family is
a curve of degree . Its closure in the Riemann sphere is acted on by Möbius maps and by anti-Möbius maps, a Möbius map composed with complex conjugation. In the coordinates , the family has the equation , whose zero set has bidegree .
The goal asserts the bounds only; their sharpness and the equality case are milestones.
The result. The bounds and are attained in every degree, so they cannot be improved as functions of alone; for the curves attaining the rotation bound form one explicit family up to similarity, with a complete invariant. The bound sharpens the auxiliary estimate used by Pach and de Zeeuw (no improvement of their distance exponent is claimed), and the quintic of equation (2) contradicts the degree restriction stated in Lemma 9 of the arXiv version of Alcázar, Lávička and Vršek (the journal version has not been checked).
The formalization. Every statement of the note is proved in Lean 4 with Mathlib: 208 theorems and 12 definition files here, all proved, using only the axioms propext, Classical.choice and Quot.sound. It contains material that Mathlib does not have yet and that is reusable on its own: the genus of a function field over defined through its places and holomorphic differentials, and its invariance under isomorphism; the places of quadratic covers and Kummer covers , with uniformizers and local Kähler differentials; the classification of places of a Dedekind domain; the four-chart atlas of with its Zariski topology; and Möbius and anti-Möbius maps acting on the Riemann sphere. Theorem 1 is also registered with the Palomar registry as PALOMAR-2026-09-18-000007. The Lean code was written by AI agents under the author's direction; the Lean kernel checks it. The results have not been reviewed by an independent human, and neither the kernel checks nor the registration certify novelty.
The first argument is Bézout: the images of a point of under the rotations about a common center are distinct points on one circle, so there are at most of them. This gives for , not , and it says nothing about which curves are extremal. A second obstacle is that a symmetry of the zero set need only fix the polynomial up to sign, as equation (2) shows, so invariant-theoretic arguments that assume do not apply directly. For the Möbius statements the difficulty is that a Möbius map of the sphere does not act on the real equation; the curve must be compactified and its singular points identified. In the formalization, the genus comparison of Remark 5 needs a genus that does not depend on a chosen model, which Mathlib does not provide.
MvPolynomial (Fin 2) ℝ), and the curve is their real zero set as a subset of . Geometric irreducibility means irreducibility over .ℂ ≃ᵢ ℂ preserving that subset. Group orders use Nat.card, which is for an infinite set, so finiteness is part of the statements.OnePoint ℂ with the action of .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.
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.
A real number is normal in base when every block of base- digits occurs in its expansion with limiting frequency , exactly as it would in a sequence of independent uniformly random digits. It is normal (absolutely normal) when it is normal in every base . Whether the classical constants of analysis, above all , are normal is one of the oldest open questions linking number theory and probability: it asks whether a number defined by geometry has digits that are statistically indistinguishable from random ones.
Timeline.
Large-scale digit computations of are statistically consistent with normality. No base is known in which is normal, and it is not even known that any particular digit occurs infinitely often in its decimal expansion.
A digit sequence is a function ; is the first digit after the point. A word is a finite list of naturals. For , the occurrence count is the number of positions with for every . Overlapping occurrences each count.
The sequence is normal in base (IsNormalSeq b s) if, for every word with all entries ,
The -th base- digit of a real after the point is
The real is normal in base (IsNormalReal b x) if is normal in base . Two remarks:
This is the conjecture in its standard form, normality in every base. The base-ten case is the special case .
None are listed. No decomposition of this problem into intermediate statements is known that would be a faithful attack path, and the mission does not invent one. Proposals for intermediate targets are welcome in the discussion; see the contributions listed under Formalization scope.
The known theorems of the subject (Champernowne's constructions, the Copeland–Erdős theorem, Borel's theorem) concern numbers built to be normal or almost every number; they are not steps toward and are kept in the separate mission Explicit normal numbers: Champernowne and Copeland–Erdős.
A proof that is normal in base would give every finite digit pattern a definite limiting frequency in its expansion. It would be the first normality result for a classical constant not built to be normal. Every known normal number is constructed digit by digit (Champernowne, Copeland–Erdős, Sierpiński, Becher–Figueira) or shown to exist by a measure argument (Borel). Even the base-2 case would settle the Bailey–Crandall programme for .
Formalization status. The goal is open mathematics. The definitions it is stated with are published and are shared with the mission Explicit normal numbers: Champernowne and Copeland–Erdős, where Champernowne's theorems and the Copeland–Erdős theorem have machine-checked proofs.
The constructive results all prove normality from the digit-by-digit description of the number. In particular, the Copeland–Erdős block criterion needs the expansion to be an explicit concatenation of blocks. has no such description. Its known series (Machin-type formulas, BBP) give digits as values of exponential sums, and no known method controls the joint distribution of long digit blocks of such values.
Borel's theorem does not help: it only says that the exceptional set is null, and gives no criterion for deciding whether a given number lies in it. Neither high-precision digit statistics nor irrationality measures for imply normality.
All declarations live in the namespace Normal and use the definition bundle Normal_Core:
count, IsNormalSeq, digit, IsNormalReal;ofDigits b s ;flatten, digitsBE, concatDigits;Committed conventions:
The definitions agree with Borel's, and the mission does not admit a trivialising reading. A real number is not normal merely because it is irrational, and the empty word imposes only the trivial condition.
The bundle also contains a verbatim copy of the integer-arithmetic definition IsNormal from xiangyazi24/agafonov; its equivalence with IsNormalSeq is proved on the platform (Normal.isNormalSeq_iff_isNormal), so results stated in either form transfer.
Welcome contributions:
A real number is normal in base when every block of base- digits occurs in its expansion with limiting frequency , as it would in a sequence of independent uniformly random digits. Borel introduced the notion in 1909 and proved that almost every real number is normal in every base, by an argument that produces no example. This mission collects the two classical papers that do produce examples: Champernowne's construction of and the theorem of Copeland and Erdős, which shows that the concatenation of any sufficiently dense increasing sequence of integers, the primes included, is normal.
Timeline.
A digit sequence is a function ; is the first digit after the point. A word is a finite list of naturals. For , the occurrence count is the number of positions with for every ; overlapping occurrences each count.
The sequence is normal in base (IsNormalSeq b s) if, for every word with all entries ,
The -th base- digit of a real after the point is , and is normal in base (IsNormalReal b x) if is normal in base . The integer part of plays no role; for a rational with two expansions the floor selects the one not ending in repeated 's.
If is an increasing sequence of positive integers such that, for every , the number of exceeds for all large , then the digit sequence obtained by writing the base- expansions of one after another is normal in base . A machine-checked proof is on the platform.
These are the standard examples of explicitly given normal numbers, and the Copeland–Erdős block argument is the model for most later constructions. The mission also fixes a definition of normality for real numbers together with the transfer from digit sequences to reals, which other work on normal numbers can import.
All declarations live in the namespace Normal and use the definition bundle Normal_Core: count, IsNormalSeq, digit, IsNormalReal; ofDigits b s ; the concatenation operators flatten, digitsBE, concatDigits; the Champernowne and Copeland–Erdős constants.
Conventions: digits are read after the point with the floor convention above; frequencies are limits of real quotients; words of every length with entries are quantified; results for real numbers are stated for bases by hypothesis.
The proofs are imported from the repository xiangyazi24/normal and verified by the platform. Their auxiliary lemmas are published on the platform as dependencies of the milestones and are not listed as items of this mission.
The open question whether is normal is a separate mission and is not approached by the methods here, which rely on the number being given as an explicit concatenation of blocks.
Random time changes occur when a process is observed on an operational clock rather than calendar time. In queueing models, for example, an arrival-count path may be evaluated at an evolving service clock. A functional limit theorem for the outer path and another for the clock are useful together only when evaluating one path at the times supplied by the other preserves convergence. Ward Whitt's 1980 paper studies several path operations with this question in mind; composition is its first main operation. The issue is specific to paths with jumps, because a small shift of the clock can move an evaluation across a jump.
Let be nonempty intervals of real time, with , and let be a complete separable metric space. The càdlàg path space consists of paths that are right continuous and have left limits on . Its subspace contains the continuous paths. The nondecreasing clock space consists of càdlàg real-valued paths on that are nondecreasing and take their values in . Its subspace contains the continuous, strictly increasing clocks. For and , composition is the path on .
Convergence uses the Skorohod topology. On a compact interval , let be the increasing homeomorphisms of and let . With denoting uniform distance, Whitt's metric is
Thus close paths may have nearby jumps at different times, provided an increasing time change aligns them. On a general interval, convergence is checked on compact subintervals whose endpoints are continuity points of the limit or endpoints of the full interval. Whitt gives this definition in §2, then gives , , and in §3. All subsets carry relative topologies and products carry product topologies.
For in and in , the first milestone states
The path-space definition and the two preparatory milestones are a small-oscillation partition for a càdlàg path, cited by Whitt from Billingsley, and Whitt's Lemma 2.2, which relates convergence on a compact interval to convergence on the two pieces made by splitting it at a continuity point.
The second case, and the combined goal, also allow the outer limit path to jump. Let mean the endpoints of that belong to . The corrected target is
The goal includes both cases for simultaneously varying and . The endpoint condition is vacuous for an endpoint excluded from . It is part of the strictly increasing clock case only; it imposes no extra restriction when the outer limit path is continuous.
This theorem supplies a precise condition for carrying two path limits through a random time transformation. In particular, the assertion includes convergence of the composed paths as elements of a càdlàg space, not merely convergence of their values at individual times. The distinction matters at jumps: pointwise convergence does not control the placement or ordering of nearby jumps. The result is a deterministic continuity statement that can be paired with probabilistic mapping theorems when the corresponding random paths are available.
Whitt proved the composition theorem in 1980, subject to the endpoint issue described below. The formalization work here is to construct its path-space interface in Lean, state the corrected continuity theorem with every domain condition visible, and eventually replace the open sorry proofs with checked proofs. The interface can also support the paper's later results on reflection, first passage, and time reversal; those results are separate missions. No proof of this mission's goal is claimed yet.
The tempting argument is to use separate continuity of and and then substitute into the first convergence. That argument loses control of evaluations near a jump of . A time change may align a jump of with the corresponding jump of , while the clock may cross those times differently. Continuity of the outer limit path removes that difficulty in one case; in the other, the clock must be continuous and strictly increasing. The source explicitly shows that composition is not continuous on all of (§3, p. 75).
The endpoints impose a further obstruction because increasing homeomorphisms of a closed time interval fix its endpoints. Bauer's Remark on p. 75 observes a failure at the right endpoint. There is a symmetric failure at the left endpoint, so the statement here includes both. This is a correction to the printed theorem, not a new claim that the uncorrected theorem is true.
Paths are represented as total functions , with only values on the named interval used. The domain assumptions OrdConnected and Nonempty express nonempty real intervals. The outer interval is also required to have nonempty interior: the formal convergence predicate checks only compact intervals with , so on a one-point it imposes nothing, and the case would fail for constant outer paths with different values. A clock's range condition is explicit, as is nondecreasingness for every prelimit clock. Membership of all paths in the relevant càdlàg spaces is part of the convergence predicates. The output predicate likewise requires every composition and its limit to be càdlàg. This rules out the trivialization in which one merely proves convergence of selected point evaluations or assumes the compositions already have the conclusion's path-space properties.
The compact uniform distance and the infimum over time changes take values in . They use the actual metric on , not a real supremum with a default value on an unbounded set. A time change is a total function whose restriction to the compact interval is continuous, strictly increasing, and onto. Continuity at a time means continuity relative to the path's interval. The general-interval convergence predicate checks the compact intervals specified by Whitt and requires each sequence member to belong to . The theorem is written as sequential continuity; Whitt's spaces are metrizable, making that equivalent to topological continuity. The real-valued clock space uses the relative topology inherited from real-valued càdlàg paths.
The endpoint correction is exact in the Lean statement. At the right endpoint, take , , for , and . Then is zero while . At the left endpoint, take , , , , and . The outer paths converge in on , but the compositions disagree at . Both examples show why continuity of at the image of every included endpoint is required in the case.
The development needs the càdlàg definition, metric and convergence predicates, compact restriction lemma, and the finite oscillation partition. Their definitions and lemmas are reusable for other functionals on path spaces. Contributions that prove the milestones and goal under the stated hypotheses are welcome. This mission does not formalize the Borel measurability or probability-measure machinery discussed elsewhere in Whitt's paper; Theorem 3.1 itself is a deterministic continuity claim.
Random coordinate descent minimizes a smooth convex function by updating one coordinate at a time, chosen at random. Each iteration needs a single partial derivative instead of the full gradient, which is what makes the method usable on problems whose dimension is in the millions or billions ("huge-scale" problems). Nesterov's paper Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012) 341–362, doi:10.1137/100802001) gave the first global efficiency estimates for such methods and started a large literature on randomized block and coordinate methods.
The basic method RCDM of the paper takes, along coordinate , a step of length , where is a Lipschitz constant of the -th partial derivative along the -th coordinate. For simple functions these constants are known; for more complicated ones they are not, and a practical method has to estimate them on the fly. Section 6.1 of the paper analyses a backtracking strategy with restore for this purpose and proves that it keeps the efficiency of RCDM up to a constant factor. This mission formalizes that analysis, Theorem 7 of the paper.
Write and for the -th standard basis vector of , . The function is convex and differentiable, attains its minimum , and its partial derivatives are coordinate-wise Lipschitz with constants ((2.2) with one-dimensional blocks):
The weighted norm and its dual are and ((2.7) with ), and
measures the size of the initial level set, being the set of minimizers.
The random adaptive coordinate descent method RACDM (6.1) keeps estimates , initialised with given lower bounds . At iteration it
The loop test uses only the sign of one partial derivative and never a function value. With (the expectation over ) and the number of partial derivatives computed in iterations , Theorem 7 states three facts about this method.
This is the rate of RCDM, ((2.14)), with a larger constant.
The result shows that the constants in RCDM need not be known: a method that starts from any lower bounds and adjusts them by doubling and halving converges at the same rate, and pays on average about two partial derivatives per iteration plus a logarithmic one-time overhead. This is what makes random coordinate descent applicable to functions whose coordinate smoothness is not available in closed form, and the doubling-with-restore pattern recurs in later adaptive and accelerated coordinate methods (the paper itself indicates the same technique for its accelerated method, (6.5)).
The theorem is proved in the paper; to our knowledge no machine-checked proof exists. The known-constant analogues for scalar coordinates are on Prove2Me in Bubeck's §6.4 development (the one-step and expected decreases are proved there; the rate is open). This mission adds a formal model of the adaptive method itself, including its doubling loop as a first-failure search, and the three statements of Theorem 7 on top of the published coordinate-descent definitions.
The analysis of RCDM rests on the one-step bound , which follows from the smoothness of along the coordinate line. For RACDM the step uses an estimate that may be smaller than , and then the same argument gives no decrease at all: a step that is too long can increase . The method never checks function values, so the decrease has to be extracted from the sign test alone, and it holds only because is convex along the line, not merely smooth. A second point is that the estimates are random and depend on the whole history, so the expected decrease must hold for every state the method can reach; this is what item 1 secures. The counting statement needs the exact number of loop iterations, so the loop has to be modelled as the least number of doublings after which the test fails, not as some number of doublings.
The formalization works with scalar coordinates (, as the paper does in §6.1) on EuclideanSpace ℝ (Fin n), coordinates indexed . It reuses the published definition ConvexOptAlg_CoordDescent_Defs: IsCoordSmooth f g L is (2.2) with an explicit gradient map , wnorm L 1 and wnormDual L 1 are and , and rcdExpect L 0 k is the expectation over uniform draws as a finite weighted sum. The mission's own definition NesterovRCD.Adaptive.RACDM encodes the trial point, the number of doublings (a minimum over ), one iteration, the run along an explicit sequence of draws, and the count .
The following choices are made explicitly.
A trivializing encoding is ruled out: the loop count is the least at which the sign test fails (an arbitrary admissible would change the method and make the count meaningless), the draws are uniform, and the rate is stated in the norm of the true constants , not of the estimates. Contributions welcome: proofs of the milestones, a one-dimensional co-coercivity lemma for convex smooth functions of one variable (reusable well beyond this mission), and the recursion argument from the expected decrease to the rate.
Dynamic programming rests on time consistency: a control that is optimal when viewed from time stays optimal when viewed from any later time. Many problems of mathematical finance lack this property. The continuous-time mean–variance portfolio problem (Zhou–Li 2000) contains a variance, that is, a nonlinear function of an expectation, and state-dependent risk aversion (Björk–Murgoci–Zhou) lets the criterion itself depend on the current state. For such problems an optimal control computed today is abandoned tomorrow, and the HJB equation is not available.
One response, going back to the game-theoretic view of non-commitment (Ekeland–Lazrak, arXiv:math/0604264; Björk–Murgoci, SSRN 1694759), is to replace optimality by equilibrium: a control that no "future self" can improve by deviating on an infinitesimally short interval. Those works consider feedback (Markov) controls. Hu, Jin and Zhou (arXiv:1111.0818v1) define equilibrium within open-loop controls for a general stochastic linear–quadratic (LQ) problem with random coefficients, and characterize it by a flow of forward–backward SDEs, in the spirit of the stochastic maximum principle (Peng 1990). This mission formalizes that characterization: §2 and §3 of the paper, up to Theorem 3.2. The other two missions of the series build on it. Mission II treats a scalar state with deterministic coefficients (Theorem 4.4), and Mission III treats mean–variance portfolio selection (Theorem 5.4).
Let be a standard -dimensional Brownian motion on with its filtration , and let . A control is a process , that is, progressively measurable with . Its state solves the linear SDE
Here is a bounded deterministic matrix function. (), () and () are essentially bounded progressive processes, and . At time , with state and , the cost is
are bounded symmetric processes with , and are symmetric with . The last two terms make the problem time-inconsistent. Given with state , the spike variation at is for . The control is an equilibrium (Definition 2.1) if for every and every such , almost surely
For each , the first adjoint process solves on the BSDE (3.1) with driver and terminal value . The second adjoint process solves the matrix BSDE (3.2) with terminal value . With these, define
Suppose , its state , and for every a solution of (3.1) are given, and suppose satisfies condition (3.4):
Then is an equilibrium control.
Theorem 3.2 is the paper's general tool. Its two explicit results are applications of it. With a scalar state and deterministic coefficients, a pair of coupled Riccati-type equations gives a linear feedback equilibrium (Theorem 4.4). In mean–variance portfolio selection with state-dependent risk aversion and a possibly random risk premium, the equilibrium strategy is found through a quadratic BSDE (Theorem 5.4). Each is proved by exhibiting a solution of the flow (3.6) and checking (3.4). The theorem therefore separates the existence question (solving a flow of FBSDEs) from the equilibrium question. The paper notes that the general existence question remains open.
The results are proved in the paper and have no machine-checked proof. The mission produces a precise statement of open-loop equilibrium for a stochastic LQ problem with random coefficients, together with Lean statements of the spike expansion and of the adjoint flows. Mission II and Mission III restate the same model, and their final steps apply this theorem. Formal proofs of the milestones exercise Itô calculus for linear SDEs and BSDEs with bounded coefficients: product rules, conditional estimates, and uniqueness and sign properties of linear BSDEs. This is infrastructure that Mathlib does not yet have.
The obvious argument is a first-order expansion of in . It fails because the spike changes the control by , which is not small, on a set of small measure. The state's deviation is then of order in , its square contributes at order , and a second-order term appears that a first-order adjoint cannot capture. Two features are absent from the classical maximum principle. The adjoint equations form a whole flow indexed by , because the terminal value of (3.1) contains and . And every statement is conditional on , so the expansion has to hold almost surely at the level of conditional expectations. That rules out arguments based on unconditional expectations.
Brownian motion, , Itô integrals and SDE solutions come from the published definition Peng1990_SMP_Stochastic. The formalization commits to the following conventions.
The conclusion of the goal is Definition 2.1 itself. It mentions neither nor the adjoint processes, so the goal cannot be closed by unfolding. A definition of equilibrium in terms of (3.4) or (3.5) would make Theorem 3.2 trivially true and is ruled out. Condition (3.5) of p. 6 is not a hypothesis of any statement. A degenerate, noise-free example checks that the hypotheses of the goal can hold together.
Contributions are welcome as follows. Proofs of the three milestones are reusable for Missions II and III and for any spike-variation argument. So are general lemmas on linear SDEs and BSDEs over Peng's Itô integral: uniqueness, conditional moment bounds, the Itô product rule, and positivity of linear matrix BSDEs.
A differential variational inequality (DVI) couples an ordinary differential equation for a state with a finite-dimensional variational inequality that the algebraic variable must solve at every instant. The class contains complementarity systems from contact mechanics and electrical circuits with diodes, linear complementarity systems from control theory, differential Nash games, and the first-order optimality conditions of optimal control problems with inequality constraints. J.-S. Pang and D. E. Stewart introduced the unified framework in Differential variational inequalities, Math. Program. 113 (2008) (author's version, hal-01366027), and Section 6 of that paper settles the first question any such model raises: when does the initial-value problem have a solution on a whole prescribed time interval?
Before this work, existence results for these systems were tied to special structure: linear complementarity systems with "minimal" and "passive" data, or a given initial condition compatible with the complementarity kernel. Theorem 6.1 gives existence for every initial state under five separate conditions on the variational inequality, each describing a different class of DVIs.
Fix and write . For a set and a map , the variational inequality asks for with for all ; its solution set is . The initial-value DVI studied here is
with nonempty, closed and convex, , , and . Two standing assumptions hold throughout: (A) , , are Lipschitz continuous on ; (B) is bounded on in operator norm.
A pair is a weak solution (in the sense of Carathéodory) on if ; is integrable on with almost everywhere; for , with an integrable integrand; and for every continuous ,
with an integrable integrand. The existence proof passes through the differential inclusion with the set-valued right-hand side
Further objects: the recession cone ; the dual cone ; the VI kernel , the solution set of ; an R₀ pair , one with ; a psd-plus matrix , one with for all and ; and the linear growth property
Under (A) and (B), if any one of the following holds, then (6.2) has a weak solution on for every :
Theorem 6.1 is the existence result behind the rest of the paper: Sections 7 and 8 prove that time-stepping schemes converge to weak solutions of (6.2), and those results are informative only for problems that have solutions. Condition (d) gives existence for every initial state of linear complementarity systems , with , where earlier results required passivity or a compatible initial state. Propositions 6.2–6.5 are results on static variational inequalities in their own right: the linear growth of solution sets in the data had not been a focus of VI theory.
The result is proved in the paper, modulo two cited theorems (Deimling's existence theorem for convex-valued differential inclusions and Filippov's measurable selection lemma). None of it is formalized. A Lean development would supply set-valued upper semicontinuity, Carathéodory solutions of differential inclusions, and existence and linear growth theory for VIs on closed convex and polyhedral sets: material with uses well beyond this paper.
The obvious route, solving the VI for as a function of and substituting into the ODE, fails: the solution map is in general set-valued and discontinuous, so the resulting right-hand side is neither single-valued nor continuous, and classical ODE existence does not apply. The detour through the differential inclusion (6.4) requires convex values, which hold when is monotone but must be proved separately in case (e), where is not monotone. It also requires linear growth (6.5), which for unbounded is a genuine statement about the asymptotics of VI solutions and needs a different argument under each of the five conditions: coercivity, a recession-cone condition, the VI kernel, or a fixed-point argument on polyhedra. Finally, Deimling's theorem and Filippov's lemma are substantial results of set-valued analysis that are not in Mathlib.
Points of are EuclideanSpace ℝ (Fin k); matrices are continuous linear maps, is the operator norm and the adjoint. Data on are curried functions on of which only the values on matter, and Lipschitz continuity on uses the metric . is the published definition SolodovSvaiterVI.Alg21.viSol Φ K. Positive semidefinite matrices are not assumed symmetric. "Monotone" in (a) and Proposition 6.2 means monotone on . The coercivity (6.6) is written in the equivalent form " for with ". Upper semicontinuity is the open-neighbourhood form relative to . In Proposition 6.4 (b) the Lipschitz property is stated on the dual cone , where the paper's proof establishes it (the statement prints ). Nonemptiness of , the paper's standing assumption on variational inequalities, is a hypothesis throughout.
The weak-solution definitions carry explicit integrability conditions on the integrands of the integral equation and of (2.4), and (2.4) is required for every continuous with values in . A definition without those integrability conditions (a Lean integral of a non-integrable function is zero), a variational condition tested only on constant , or (A)–(B) replaced by global boundedness of and would make the goal a different and weaker statement; none of these is used.
Contributions welcome at every level: proofs of the milestones, a general theory of upper semicontinuous set-valued maps and Carathéodory solutions of differential inclusions, and existence results for variational inequalities via recession cones and degree theory.
A manufacturer must commit to production before a retailer knows how much it will buy. In practice the retailer sends a forecast first, and the manufacturer plans against it. When the forecast binds neither party, the retailer has no reason to report it honestly, and the manufacturer has no reason to plan for the market rather than for its own margin. Purchasing managers have described this to Tsay directly, and Lee, Padmanabhan and Whang (1997) document such "phantom ordering" in several case studies.
A. A. Tsay, The Quantity Flexibility Contract and Supplier-Customer Incentives (Management Science, 1999), models the situation as a two-stage newsvendor game with a demand-information update between production and purchase. Its first result, Proposition 1, is the benchmark the rest of the paper builds on. Even when both parties share the same beliefs about demand, a linear transfer price alone leaves the manufacturer underproducing relative to a central planner, and the supply chain loses expected profit, for every transfer price. That inefficiency motivates the quantity flexibility (QF) contract studied in the remainder of the paper and in the companion mission of this series.
Costs. The retail price is and the unit transfer price paid by the retailer to the manufacturer (the EM) is . The unit production cost is , the unit salvage value is (the same for either party), and the unit goodwill loss on unmet demand is . The paper's standing assumptions (§3.1, p. 1344) are
Three critical fractiles recur:
Demand (§3.3). Market demand is . The signal has distribution function , which is differentiable and strictly increasing, and finite variance. The error is independent of . is the distribution function of , is the standard normal distribution function, and .
Timing (§3.2). The EM produces knowing only the prior. Then is observed and the retailer buys . Then is realized, and both parties salvage their surplus. Given , the retailer's expected profit from purchase is
Without commitment the retailer buys . The EM's expected profit is
and the retailer's is . A central planner producing before the signal earns
Let maximize and maximize . Then, for every transfer price admitted by the standing assumptions,
and the retailer's optimal purchase under is . 3. §5.2, p. 1347. The EM's optimal production exists and is unique:
Proposition 1 shows that sharing demand information does not remove inefficiency. Under common beliefs and with no commitment, no linear transfer price makes the decentralized chain efficient. Adjusting moves profit between the parties but cannot recover the planner's expected profit. This is the reason the paper studies richer contracts, and the efficiency result for the QF contract (the paper's Proposition 6) is measured against the benchmark defined here.
The paper prints no proofs ("All proofs are omitted due to space limitations", p. 1341). A machine-checked development therefore supplies arguments the published record does not contain. It also exhibits the exact hypotheses the result needs. In particular it covers the degenerate case , where the signal is perfect. No part of this mission has a prior formal proof. Newsvendor critical-fractile results exist on Prove2Me for single-decision models, but without the production stage and information update used here.
The EM and the planner solve newsvendor problems against different demand laws. The EM faces the retailer's purchase , while the planner faces . Their fractiles are and . The obvious comparison, , settles the case only. For the two quantities are inverse distribution functions of different random variables. may be negative, and the planner's distribution is a convolution. A comparison of fractiles alone therefore does not order and . The strict profit gap also needs more than optimality of : it requires comparing the decentralized system profit at with the planner's profit at the same production, and then using uniqueness of the planner's optimum.
The analytic infrastructure is also substantial. It includes differentiating expectations of piecewise-linear functions under a Gaussian law and under a general prior, continuity and strict monotonicity of a convolution's distribution function, and existence of a root of .
All objects live in the namespace TsayQF.NoCommit, in one definitions file Model.
Data with fields and the standing assumptions (i)–(iii) as fields. "For any " is quantification over all Data. No sign is imposed on .ν on ℝ; is cdf ν. "Differentiable and invertible" is Differentiable ℝ (cdf ν) together with StrictMono (cdf ν), and "mean and variance" is MemLp id 2 ν.v : ℝ≥0, so and v = 0 is allowed. The law of is the pushforward of ν.prod (gaussianReal 0 v) under addition, and given demand has law gaussianReal μ v.z with hypothesis cdf (gaussianReal 0 1) z = kR D. The milestones state existence of a solution of each fractile equation and characterize the maximizers by it.IsMaxOn over Set.univ for productions and over Set.Iic Q for the purchase. Productions range over ; the paper's presumption that and are almost certainly nonnegative is not imposed, because no result here needs it.The goal must not be weakened to non-strict inequalities, and the EM's demand must remain the retailer's purchase , not market demand. Either change trivializes the result or changes it. Reusable pieces are the newsvendor critical-fractile characterization for a general continuous strictly increasing distribution, and monotonicity and continuity of the distribution function of a sum of independent variables with one Gaussian summand. Proofs of the milestones as standalone lemmas are welcome.
In the job shop problem, jobs are sequences of operations, each to be processed on a given machine for a given time, and the goal is a schedule of minimum makespan (the time at which the last job finishes). Two numbers bound the optimum from below: the longest job and the most loaded machine. Their maximum is written . The best approximation algorithms for job shops have a performance guarantee polylogarithmic in (Shmoys, Stein and Wein 1994; Goldberg, Paterson, Srinivasan and Sweedyk 2001). Whether flow shops and job shops admit a constant-factor approximation was Open Problem 7 of Schuurman and Woeginger (1999).
Mastrolilli and Svensson (J. ACM 58(5), 2011) answered it negatively for the generalized flow shop. Their Theorem 1.2 states that for all sufficiently large constants it is NP-hard to distinguish generalized flow shop instances with a schedule of makespan from instances in which no schedule finishes more than half of the jobs within . The proof is a gap-preserving reduction from graph colouring. This mission formalizes the combinatorial heart of that reduction.
Timeline. Shmoys, Stein and Wein (1994) gave an -approximation for job shops, improved by a factor by Goldberg et al. (2001). Williamson et al. (1997) proved that approximating flow shops with unit operations within a ratio better than is NP-hard. Feige and Scheideler (2002) gave acyclic job shop instances with optimum and asked whether flow shops admit a much better upper bound than . Khot (2001) proved the colouring hardness this reduction starts from. Mastrolilli and Svensson (FOCS 2008; J. ACM 2011) proved Theorem 1.2 and its job shop variants.
A generalized flow shop (flow shop with jumps) is a job shop with a fixed linear order on the machines in which every job visits its machines in increasing order but may skip machines. Operations may have length . A zero-length operation still occupies its machine for an instant, so it cannot be processed strictly inside another operation on the same machine.
Let be a simple graph with vertices whose vertices are partitioned into independent sets . Vertex has frequency . For an integer write . The instance has groups of machines, each with one machine per vertex. The machines are ordered by group first and, within a group, by decreasing frequency. A vertex of frequency owns groups of identical jobs. The job has a long-operation of length on each of the machines , where . It also has a short-operation of length on every machine of every neighbour of , in every group. A long-operation is good if the next long-operation of the same job starts at most time units after it ends. is the set of first halves of the good long-operations on , and is the time they cover.
is the chromatic number of and the size of its largest independent set.
For every graph with a proper colouring into classes and every integer , with :
Remark 3.6 (lengths, loads, operation count), Claim 3.8 (an independent set's jobs fit in ), Lemma 3.7 (completeness), Lemma 3.10 (most long-operations are good), Lemma 3.11 (adjacent vertices have disjoint -intervals), Lemma 3.12 (one group carries of first-half time), and Lemma 3.9 (soundness: an independent set of size ).
The result. Together with Khot's colouring hardness, the gap shows that no polynomial-time algorithm approximates the generalized flow shop within any constant factor unless P = NP, and rules out an -approximation under a stronger complexity assumption (Theorem 1.3). It also shows that on the no-instances of the reduction every schedule has makespan greater than , far above the trivial lower bound . Because soundness bounds the number of jobs finished early, the same reduction also gives hardness for the sum of completion times (footnote 2).
Formalizing it. The paper proves every statement of this mission; none is open. As far as the catalog shows, none has a machine-checked proof. The soundness argument rests on a timing property of zero-length operations: a job of higher frequency must wait for a long-operation of an adjacent lower-frequency job. Such properties are easy to state loosely and easy to get wrong, so a verified proof would be useful. A formal proof would also make explicit the thresholds the paper leaves as "sufficiently large ".
Completeness is constructive and routine once the job and machine indexing is under control. The difficulty is soundness. One might argue directly that jobs of adjacent vertices never overlap in time, but that is false: a schedule may run them in parallel at the cost of delays. The argument controls it only on average. It throws away the jobs that finish late and the long-operations followed by a long delay. It shows that the first halves of the remaining long-operations of adjacent vertices are disjoint in each machine group. Then it finds a moment covered by many such first halves. Each step needs a precise count: of good operations per job, of covered time per group, and of overlap multiplicity at a point. The degenerate conventions (empty colour classes, , the last long-operation of a job) have to be handled throughout.
The instance is the published JobShopLTAS.Core.Instance (machines and jobs Fin (r^{2d} n), real nonnegative processing times, disjunctive machine constraint under which a zero-length operation cannot sit strictly inside another operation on its machine), with its IsFeasibleSchedule and makespan. The graph has vertex set Fin n and the partition into independent sets is a Mathlib proper colouring G.Coloring (Fin d). Frequencies are 1-based, as are group indices. Within a group the paper leaves machines of equal frequency unordered; they are ordered by vertex index. Every job's operation list is its machine set sorted by the global order. is the Lebesgue measure of the union of the intervals.
Explicit readings of the paper's wording:
Not formalized: "NP-hard", "for all sufficiently large ", "in time polynomial in and ", Khot's Theorem 1.7, the choice , , and the randomized Lemma 3.1 behind Theorem 1.3.
A model in which zero-length operations occupy no machine time would make soundness false, and stating soundness only for schedules of an independent set's jobs would make it vacuous. The goal is about every feasible schedule of , built from , in the published model, where zero-length operations do conflict.
A complete development needs counting lemmas for the indexing of jobs and machines, sorting facts for the operation lists, and a measure-theoretic averaging argument (a point covered by many intervals). The averaging argument and the good-operation counting are shared with the flow shop gap of Theorem 1.1 and reusable there. Proofs of any milestone, and sorry-free sanity checks on small instances, are welcome.