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?
Many stochastic models evolve on two time scales: a fast component that equilibrates quickly and a slow component driven by it. Planetary motion, climate models, geophysical flows and intracellular reaction networks are standard examples, and multiscale numerical methods for them approximate the slow component by a reduced equation. Such approximations are only useful with an error bound, and for the fully coupled case, where the fast and slow equations each depend on both components and the slow equation contains a large fluctuating drift, rates of convergence were missing.
Röckner and Xie (Ann. Probab. 49 (2021) 1205–1236) treat this case with only Hölder continuous coefficients and obtain explicit rates in four regimes. This mission poses the first regime, the classical averaging principle.
Timeline. Papanicolaou, Stroock and Varadhan (1977) proved the diffusion approximation for with a compact fast state space and time-independent coefficients. Pardoux and Veretennikov (2001, 2003, 2005) treated a noncompact homogeneous case with and by martingale problems and the Poisson equation. Rates for the averaging principle when were obtained by several authors, e.g. Givon (2007) and Liu (2010). Röckner and Xie (2021) give rates for the fully coupled system with Hölder coefficients in all four regimes.
Let (fast) and (slow), . For small parameters tending to , with , the two-scale system (1.4) is
with , and independent Brownian motions .
Freezing gives the frozen equation (1.7), with generator , , and invariant probability measure . A function is centered if its -average vanishes for every . The standing assumptions are: (Aσ), uniform nondegeneracy of ; (Ab), ; (AG), uniform nondegeneracy of ; (AH), is centered; and (2.7), the analogue of (Ab) for , small.
The averaged coefficients of Regime 1 are and , and the averaged equation (2.9) is , .
Regularity is measured in weighted Hölder classes: (index in , in , polynomial growth in ), its bounded version , the time-dependent , the class of measurable functions of polynomial growth, and for test functions.
In Regime 1, and , assume , with , and . Then for every and ,
The result. The theorem gives a rate for the weak error of the averaging principle under Hölder regularity only, and the rate depends only on the regularity in the slow variable , not on . It covers the fully coupled case, in which the slow equation contains the singular drift , and it identifies the extra condition under which this drift averages out. For it reduces to the rate (Remark 2.5), optimal for . Error bounds of this kind are what heterogeneous multiscale methods need to be quantitative.
Formalizing it. The result is proved in the paper; nothing in it is machine-checked. A formalization needs an Itô calculus for weak solutions, the elliptic Poisson equation in with parameter (the companion mission's Theorem 2.1), and the parabolic Kolmogorov equation of the averaged SDE. The two fluctuation lemmas are stated for general centered functions and are reusable for other limit theorems.
The obvious argument writes through the Kolmogorov equation of the averaged SDE and Itô's formula, which leaves and . Both integrands are centered but only Hölder continuous in , so the standard corrector argument, which applies Itô's formula to the solution of the Poisson equation along , needs derivatives in and that do not exist. The term with is a central-limit-scale fluctuation, which is why its control needs the regime conditions. Existence and regularity of the averaged coefficients also have to come from the Poisson equation, since is not explicit.
Spaces are EuclideanSpace ℝ (Fin d). Coefficients are , a matrix, , a matrix. The Itô layer (Brownian motion, Itô integral, Itô processes, SDE solutions) is the published Peng1990.SMP.Stochastic. A solution of (1.4) is a weak solution: any filtered probability space, any Brownian motion for that filtration, any progressive process satisfying the integral equation. The theorem compares every weak solution of (1.4) with every weak solution of (2.9). The paper does not prove existence for (1.4), so the statement is conditional on solutions, as it is used in the paper. A sanity file shows the parameter hypotheses are consistent (, ) and that (2.7) holds for a bounded dissipative drift.
Committed conventions and readings of the page:
A formalization in which the expectations are junk Bochner integrals, the constant depends on , or a single strong solution is fixed would be a different and weaker statement; the posed statements rule these out.
Not posed: Regimes 2–4 of Theorem 2.3 and Lemma 4.4(ii)–(iv). The printed differs by a factor in the term from the generator used in the proof, so a faithful statement needs a correction that is left to moderation. Regime 2 needs the Poisson solution in the averaged drift. Lemma 5.2 is also not posed: as printed, solves (5.1) only for time-independent coefficients, and its class has time index above , which the paper's notations do not define. Contributions toward Itô's formula for these processes, the Poisson equation (companion mission 1) and parabolic Schauder theory are welcome.
Poisson equations for the generator of an ergodic diffusion are a standard tool in stochastic averaging, homogenization and diffusion approximation: to show that a fast ergodic component averages out in a slow equation, one writes the fluctuation as and applies Itô's formula to . This requires a solution whose regularity is controlled in two variables at once: the fast variable , in which the operator is elliptic, and the slow variable , which enters as a parameter.
Fix , a matrix field and a vector field on . The frozen operator acts on functions of with held fixed:
The Poisson equation (1.1) is for all , for each parameter .
The standing assumptions are:
Under these, for each the frozen diffusion has a unique invariant measure . Since constants solve , the equation is only solvable for centered right-hand sides, for every (1.3), and the solution is fixed by requiring it to be centered as well.
Regularity is measured in weighted Hölder classes. () means and , uniformly in . adds derivatives in , with a -Hölder top derivative. The subscript denotes the bounded version, and asks the same of together with growth bounds on and .
If (Aσ), (Ab) hold and with , , then for every centered there is a unique centered with . For some ,
and, for , .
The theorem supplies the corrector used in Theorem 2.3 of the same paper, the weak convergence rate of the slow component of a fully coupled multiscale SDE to its averaged limit. Its form, regularity in matching that of the data and no derivative of in , is what lets the rates depend only on the regularity of the coefficients in the slow variable. The transfer formulas (3.9)–(3.10) also show that averaged coefficients inherit the -regularity of , a question that comes up in every averaging or homogenization limit.
The result is proved in the paper. None of it is formalized: Lean and Mathlib have no fundamental solutions of non-divergence elliptic operators, no Schauder theory and no invariant measures of diffusions. The mission poses the statements, so that the proof can be built in layers and the parts that do not depend on the Gaussian kernel bounds (the transfer formulas given a solution, the induction in Steps 3–4) can be proved separately.
Existence and the estimates (2.1)–(2.2) rest on the probabilistic representation and on Gaussian bounds and ergodic decay for the fundamental solution of (Lemma 3.1, cited from Ladyzhenskaya–Solonnikov–Ural'tseva and Pardoux–Veretennikov II, Proposition 3). The coefficients are only Hölder in , so the Hessian bound needs the cancellation (3.3), not just a size estimate on . The obvious approach to -regularity, differentiating or in , needs derivatives of the invariant density in the parameter, which are hard to control. The paper's route, differentiating the equation and using the transfer formula to recenter, only works if the differentiated right-hand side is again centered. That centering is the content of Lemma 3.2.
EuclideanSpace ℝ (Fin d); , are fderiv and iteratedFDeriv ℝ 2 in , is iteratedFDeriv ℝ j in , with operator norms. -derivatives in the milestones are directional.Hemivariational inequalities were introduced by Panagiotopoulos in the 1980s to model mechanical problems whose energy functional is neither convex nor smooth: nonmonotone friction, adhesion, delamination and unilateral contact with nonmonotone multivalued laws. Where a variational inequality expresses the optimality condition of a convex energy, a hemivariational inequality expresses a stationarity condition of a locally Lipschitz energy through Clarke's generalized directional derivative. When in addition the admissible set depends on the unknown state, as in contact problems with a solution-dependent gap or in Nash-type equilibrium problems with coupled constraints, the problem becomes a quasi-hemivariational inequality.
Zeng, Migórski and Khan (SIAM J. Control Optim. 59 (2021)) treat a general form of this problem that contains a multivalued operator , a bifunction and a constraint map at once. Their existence theorem for it, Theorem 3.8, is the base of an optimal control result (Section 4) and of an application to a frictional contact problem in elasticity (Section 5). This mission formalizes the existence part, Sections 2 and 3 of the paper.
Let be a real reflexive Banach space with dual and pairing , and let , be real Banach spaces. The data are: a nonempty closed convex set ; a multivalued constraint map ; a multivalued operator ; a function ; a locally Lipschitz functional ; bounded linear operators and ; a functional ; and an auxiliary function .
For a locally Lipschitz , the Clarke generalized directional derivative and the generalized gradient are
Problem 1.1 asks for and such that and
Its solution set is . Fixing the constraint set gives Problem 3.3: find and with the same inequality for all ; its solution set is . The variational selection maps to the solution set of Problem 3.3 with replaced by ; its fixed points are exactly the solutions of Problem 1.1.
The hypotheses of the paper (p. 1250) are: has nonempty, compact, convex values and is upper semicontinuous; is -stably pseudomonotone with respect to , where and is weakly sequentially upper semicontinuous in the limsup sense (3.1); is convex and l.s.c. in its first argument, concave and u.s.c. in its second, and vanishes on the diagonal; has nonempty closed convex values and satisfies two Mosco-type conditions (HK); a bounded set meets every and, if is unbounded, a coercivity condition (3.2) holds at each point of . Theorem 3.8 adds that is compact, is convex, and whenever strongly and weakly (3.19).
Under all hypotheses of Theorem 3.8,
nonemptiness, boundedness and weak closedness of ; and its convexity when is convex. 4. Theorem 3.8 (i): the same characterization for Problem 1.1, with replaced by . 5. Two claims from the proof of Theorem 3.8 (ii): the graph of is sequentially weakly closed, and is bounded.
Theorem 3.8 is the existence result on which the rest of the paper rests: the optimal control problem of Section 4 minimizes over , and Section 5 casts an approximate static elastic contact model, with a multivalued normal compliance condition and a frictional law with slip-dependent friction coefficient, in the form of Problem 1.1 on a space of displacements. The theorem unifies several existence results for variational, hemivariational and quasi-variational inequalities: for single-valued , , , and , its Corollary 3.9 reduces to an earlier existence result for quasi-variational inequalities (Remark 3.10), and Theorem 3.4 removes the compactness of required in earlier work (Remark 3.6).
The results are proved in the paper. None of them, nor Clarke's calculus on a Banach space, nor Kluge's fixed point theorem, has a machine-checked proof to our knowledge. A formalization adds a checked version of a proof that combines a KKM-type fixed point theorem, Minty's trick for pseudomonotone multivalued operators, and a fixed point argument for the variational selection.
The obvious route to Problem 1.1 is to fix , solve the inequality on , and take a fixed point of the solution map. Two steps resist. First, the solution map is multivalued and its values are only weakly closed, so a Schauder- or Kakutani-type theorem in the norm topology does not apply; the fixed point theorem must work with sequentially weakly closed graphs, and the graph closedness of has to be proved by passing to the limit in inequalities in which converges only weakly while the test points must converge strongly. That passage uses the compactness of , the upper semicontinuity of , condition (3.19) and the Mosco-type conditions together. Second, in the "there exists " form of the problem the inequality is not stable under weak limits in , which is why the Minty reformulation and the stable pseudomonotonicity with the auxiliary function are needed.
All spaces are real normed spaces with CompleteSpace; is V →L[ℝ] ℝ with the operator-norm topology; reflexivity is surjectivity of NormedSpace.inclusionInDoubleDual ℝ V. No inner product and no finite dimension is assumed. Multivalued maps are total functions V → Set _, constrained on only. Weak convergence means for every ; "weakly closed" is sequential weak closedness, which for the bounded sets and in a reflexive space agrees with weak closedness. Adjoints are composition: , . is a real Filter.limsup and is used only under LocallyLipschitz J. Every , infimum and limit in the hypotheses (, (3.1), (3.2), (3.19)) is written with explicit – quantifiers, so no default value of a real or can make a hypothesis vacuous.
Four corrections to the printed hypotheses are built in and stated in each item's note: the pairing in (3.2) is (the page's does not typecheck); is nonempty for ; the condition (3.2) assumed in Theorem 3.4 refers to a bounded set that meets ; and for Theorem 3.8 (ii) and the boundedness of , (3.2) in (HC0) holds uniformly in (one for each ), which is what the proof on pp. 1260–1261 uses. With (3.2) only at each fixed , as printed, can be unbounded; the counterexample is in the note of Theorem 3.8 (ii). Theorem 3.8 (i) and the graph-closedness of keep (HC0) as printed. A formalization in which may have empty values, may be empty or disjoint from , is a Hilbert or finite-dimensional space, a real default value makes the conditions on or (3.19) vacuous, or "bounded" or "weakly closed" is dropped from the conclusion, would be a different and weaker theorem.
The development needs Clarke's calculus on a Banach space (Proposition 2.5, which relies on the Hahn–Banach theorem), Eberlein–Šmulian or Kakutani's theorem on weak compactness of bounded closed convex sets in reflexive spaces, Mazur's lemma, a KKM-type fixed point theorem in Hausdorff topological vector spaces, and Kluge's fixed point theorem. These pieces are reusable beyond this mission: Clarke's calculus for every nonsmooth optimization statement on Banach spaces, and the fixed point theorems for variational and quasi-variational inequalities in general. Contributions of any of them, of alternative proofs, and of proofs of the milestones in any order are welcome.
Mean field control asks a central planner to steer a large population of interacting agents. Each agent's state follows a stochastic differential equation whose coefficients depend on the agent's own state and on the empirical distribution of the population; as the population grows, the system is described by a single McKean–Vlasov equation whose coefficients depend on the law of the solution itself. The planner's value is then a function of time and of a probability measure, and its dynamic programming equation, the HJB master equation, is a partial differential equation on the Wasserstein space of measures.
C. Wu and J. Zhang (Ann. Appl. Probab. 30(2), 2020) develop a viscosity theory for such master equations in a path-dependent setting and apply it to McKean–Vlasov control with closed-loop controls, i.e. controls that depend on the observed state path rather than on the driving Brownian motion. Closed-loop information is the natural one when the noise is not observable, and it is the information structure relevant for games; but the value function is then not known to be smooth, so classical solutions are out of reach. This mission formalizes the paper's §5: the value function of the closed-loop problem with piecewise constant controls is a viscosity solution of the HJB master equation.
Fix and a horizon . The path space is with the uniform norm, the canonical process is , and is its natural filtration. is the set of probability measures on with ; is the law of the stopped path . On the pseudometric is
with the 2-Wasserstein distance on laws of paths.
The data are a control set and coefficients , , , satisfying Assumption 5.1: measurability and adaptedness, boundedness of by , Lipschitz continuity of and uniform continuity of in , local uniform continuity in , and positive definiteness of .
An admissible control (5.3) is piecewise constant: for a partition , with -measurable. The controlled law agrees with on and solves, for a Brownian motion ,
The value function (3.20) is
and is the same supremum over the controls (5.12) whose pieces depend on the path before only through finitely many values .
The HJB master equation (3.22) is with , where
Viscosity solutions (Definition 4.4) are defined by test functions that satisfy a functional Itô formula on , where is the set of laws agreeing with on under which is a semimartingale on with drift and diffusion bounded by , and touch from above or below at on that set.
Under Assumption 5.1, is finite on and is a viscosity solution of (3.22).
The result characterizes the closed-loop value function through a PDE on the space of path laws without assuming any smoothness of . Combined with a comparison principle for (3.22), which the paper leaves open, it would identify the closed-loop and open-loop values (Remark 5.9). The regularity result (Theorem 5.7) is itself delicate: Example 5.6 shows that a natural restricted class of closed-loop controls produces a value function that is discontinuous in , and the piecewise constant class (5.3) is chosen to avoid this.
The theorems are proved in the paper; none of them is formalized. A formalization would supply a machine-checked path from a path-dependent McKean–Vlasov control problem to its HJB master equation, together with reusable statements on weak solutions of path-dependent McKean–Vlasov equations, their uniform moment bounds, and the dynamic programming principle in the Wasserstein space.
Definition 4.4 requires , and the central difficulty is continuity in . Closed-loop controls are functions of the observed path; changing the initial law from to changes the information available to the control, and when is degenerate a control adapted to cannot be written as a function of the -path. The obvious argument, transporting an -optimal control for along an optimal coupling of and , fails for exactly this reason (Example 5.6).
Time is and every statement quantifies over and . Paths are continuous maps with the sup norm and Borel -algebra; is the published WassersteinDRO.Duality.wassersteinDistance with . Brownian motion and Itô integrals are the published EthierKurtz.IsStandardBrownian and EthierKurtz.HasBrownianItoIntegral.
Committed conventions:
The test classes are not vacuous: constant functions satisfy every clause of the test-function class, and Assumption 5.1 holds for , , . A formalization that makes or the admissible set empty, or that lets be , does not prove the theorem.
Needed infrastructure: weak existence and uniqueness for path-dependent McKean–Vlasov SDEs with Lipschitz coefficients; Burkholder–Davis–Gundy-type moment bounds; measurable selection on Polish spaces; couplings and gluing on of a path space. The moment bound and the McKean–Vlasov well-posedness are reusable beyond this mission. Contributions to any milestone are welcome.
Master equations are partial differential equations whose state variable is a probability measure. They arise as the Hamilton–Jacobi–Bellman equations of mean field control problems, where a planner steers a large population through its distribution, and as the limit description of large games. Their basic computational tool is an Itô formula for functions of measures: if is a semimartingale with law at time , how does evolve? For functions on the Wasserstein space this formula is due to Buckdahn, Li, Peng and Rainer (Ann. Probab. 2017) and Chassagneux, Crisan and Delarue (arXiv:1411.3009), with the derivative in the measure introduced by Lions through the lifting to random variables.
Many models are path dependent: exotic options, rough volatility, and control problems with constant controls all lead to functions of the law of a whole path rather than of its time marginal. Wu and Zhang (Ann. Appl. Probab. 2020) extend the measure derivative and the Itô formula to this setting, following Dupire's functional Itô calculus (Dupire 2009). This mission formalizes §2 of their paper: the derivative of a function of a path law and the functional Itô formula of Theorem 2.7. It is the first of three missions on the paper; the other two treat viscosity solutions of master equations and McKean–Vlasov control.
Fix and . Continuous paths form with . Càdlàg paths form with the Skorokhod distance
the infimum over continuous strictly increasing bijections of . The canonical process is , with natural filtration ; is the path stopped at .
is the set of probability measures on with , with the Wasserstein distance whose cost is . The state space is with the pseudometric
where is the law of .
For the time derivative is the right derivative . The spatial derivative comes from lifting to on square-integrable path-valued random variables of an atomless Polish probability space: the Fréchet derivative of under the perturbation has the form . The second derivative is the pathwise (Dupire vertical) derivative of . consists of the continuous with continuous derivatives, bounded , and .
is the set of laws of Itô processes with , and square integrable.
For , and ,
The formula is the chain rule of calculus on path laws. It is what makes functions admissible test functions for viscosity solutions of path-dependent master equations, and what identifies the value function of a McKean–Vlasov control problem with a solution of its HJB master equation (§§4–5 of the paper, the other two missions of this series). Without it, the notion of viscosity solution in that paper has no link to the underlying dynamics.
The result is proved in the paper. It has no machine-checked proof: Lean's Mathlib has neither the Skorokhod space, nor Wasserstein spaces of path laws, nor a derivative with respect to a measure. Formalizing it would also produce a reusable Lean account of càdlàg path spaces and of the Lions derivative, both of which are absent today.
The obvious argument would expand along the time marginals of . That fails for path-dependent : the stopped laws do not change continuously when a path is perturbed after , and the perturbation of the derivative's definition leaves the space of continuous paths. This is why the paper passes to càdlàg paths and the Skorokhod distance. Any argument then has to control and its derivatives along laws of discontinuous paths, which is where the joint continuity of all derivatives in under and convergence of laws in become unavoidable. Separately, Theorem 2.2 must show that a derivative defined through one probability space is a deterministic function of the stopped path, and atomlessness of that space is essential to it.
Paths are functions on , constant after ; is C(Set.Icc 0 T, ℝ^d) with the sup norm, embedded in . carries the -algebra of the evaluations. Distances, sup norms and are -valued. A law in is given with an explicit representation: a filtered probability space, a standard Brownian motion with independent increments, progressively measurable bounded coefficients, and the Itô integral of the published EthierKurtz.HasBrownianItoIntegral. The goal holds for every representation of , and (2.20) is stated in drift form: , the stochastic integral having mean zero.
The class fixes together with its derivatives and states that they are the derivatives (2.7), (2.16), (2.18). It also requires and to be -adapted, a property the paper's has by Theorem 2.2. Without these clauses every continuous function would qualify, and (2.20) would be false. The printed is read as . The proof's computations are stated in dimension . Limits indexed by are stated for .
A complete development needs: the Skorokhod space and the fact that its Borel -algebra is the evaluation -algebra; Wasserstein distances on it; dominated convergence for path laws; and Itô's formula for the drift–diffusion representation. These are reusable well beyond this mission. Contributions to any milestone, or to these foundations as separate lemmas, are welcome.
Binary polynomial optimization asks for the maximum of a polynomial over . Linearizing each monomial by a new variable turns the problem into a linear program over the convex hull of a set of 0/1 points, the multilinear polytope of the hypergraph whose edges are the monomials. Global solvers such as BARON build polyhedral relaxations of this polytope at every node of their branch-and-bound trees, so valid inequalities that are as strong as possible, that is, facet-defining, translate directly into smaller root gaps.
Del Pia and Khajavirad introduced running intersection inequalities in The running intersection relaxation of the multilinear polytope (Math. Oper. Res. 46 (2021) 1008–1037, doi:10.1287/moor.2021.1121). They generalize the flower inequalities of the same authors (SIAM J. Optim. 2018), which are facet-defining when the support hypergraph is -acyclic, to support hypergraphs that are not. This mission formalizes the paper's sufficient condition for a running intersection inequality to define a facet (§2.4, Proposition 4) together with the structural results it rests on.
Timeline. Crama (1993) studied the standard linearization; Del Pia and Khajavirad (2017, Math. Oper. Res.) proved that the multilinear polytope is full dimensional and gave lifting theorems for facets; flower inequalities followed in 2018; running intersection inequalities and the facet conditions formalized here appeared in 2021.
A hypergraph has a finite node set and a set of subsets of of cardinality at least two. Its multilinear set is
and its multilinear polytope is .
A multiset of sets has the running intersection property if its elements can be ordered so that each , , is contained in a single earlier . Such an ordering defines and . A leaf of is an element that comes last in some such ordering.
Fix an edge (the center) and edges , , adjacent to (the neighbors), such that the multiset has the running intersection property. Choose an ordering of , and for each with a node . The running intersection inequality is
where is the number of connected components of the hypergraph . Its support hypergraph has node set and edge set . An inequality defines a facet of if it is valid and the face it cuts out is nonempty of dimension .
Assume
Then the running intersection inequality defines a facet of for its support hypergraph .
Lemma 1 (p. 1011, leaves and reorderings), Lemma 2 (p. 1011, components ), Proposition 1 (p. 1012, validity), and the full dimensionality of (cited on p. 1016 from [12]):
Corollary 2 (p. 1017): and for suffice. Proposition 2 and Corollary 1 (pp. 1013–1014): the multiset , hence the system of inequalities, does not depend on the ordering. Proposition 3 (p. 1014): necessary conditions for a facet of the running intersection relaxation .
Proposition 4 certifies a large family of facets of multilinear polytopes whose support hypergraphs contain cycles that flower inequalities cannot handle. Together with the lifting theorems of Del Pia and Khajavirad (2017), it yields sufficient conditions under which these inequalities define facets of the multilinear polytope of general hypergraphs (p. 1015); §2.5 of the paper reports that running intersection cuts reduce BARON's root-node relaxation gap on image-restoration instances. Proposition 3 and Example 1 show that condition 1 is necessary while conditions 2–3 are not, so the result is a sufficient condition and not a characterization.
The results are proved in the paper; none is formalized. A Lean development would provide the first machine-checked library for the running intersection property (orderings, leaves, the multiset of -sets), the connected-component count of Lemma 2, and the multilinear polytope as a convex hull with an exact dimension count, all reusable for the companion missions on the tightness of for kite-free -acyclic hypergraphs and its strictness otherwise.
Validity (Proposition 1) decomposes over the connected components of ; the facet claim does not, because a face of codimension one is a global object and the neighbors of different components, and the nodes shared between neighbors, interact in it. Conditions 2 and 3 are exactly where this interaction is controlled, and Example 1 of the paper shows that dropping condition 3 does not destroy facetness, so no simple equivalence is available to fall back on. Formally, three nontrivial ingredients have no Mathlib counterpart: the combinatorics of running intersection orderings (Lemma 1, Proposition 2), the count of connected components of a hypergraph with loops and parallel edges (Lemma 2), and the affine dimension of a convex hull of 0/1 points in a space indexed by nodes and edges.
Nodes form a finite type α; every hypergraph's space lives inside α ⊕ Finset α → ℝ, with the coordinates outside pinned to in the definition of , so is meaningful. Orderings are lists indexed from . The number of components is that of the 2-section graph on the node set. An inequality is given by its data: center, a set of distinct neighbors other than , an ordering of whose traces form a running intersection ordering of , and the choice ; the first sum runs over neighbors, so a node chosen for two neighbors has coefficient . "Defines a facet" requires a nonempty face and compares dimensions as , so the empty face can never qualify and no truncated subtraction occurs. The facet statement is about for the support hypergraph only, not for a larger host hypergraph, which would require the lifting theorems. The reading is used where the page's "for all " would otherwise be contradictory (Corollary 2, Proposition 3(i)); Lemma 2 is stated for lists of nonempty sets, which covers its use on .
Contributions welcome: proofs of the milestones, a reusable library for the running intersection property and -acyclic hypergraphs, and the full-dimensionality proof.
In a financial market with a single probability model, the Optional Decomposition Theorem describes the processes that can be dominated by trading. If a process is a supermartingale under every equivalent martingale measure, then it can be written as an initial value plus a stochastic integral against the stock price, minus an increasing process that represents consumption. El Karoui and Quenez proved it for diffusion models (SIAM J. Control Optim. 33 (1995)) and Kramkov for locally bounded semimartingales (Probab. Theory Related Fields 105 (1996)). It is the step that turns the superhedging price, a supremum of expectations over martingale measures, into an actual dynamic hedging strategy.
Model uncertainty replaces the single model by a set of probability measures that may be mutually singular. This happens, for example, when volatility is only known to lie in an interval. There is then no reference measure, "almost surely" becomes "quasi surely" (outside a set that is null under every model), and the classical proofs, which rely on one dominating measure, do not apply. Bouchard and Nutz (Ann. Appl. Probab. 2015, arXiv:1305.6008) built the discrete-time theory of this setting: no-arbitrage, the fundamental theorem of asset pricing, superhedging duality and, in §6, a nondominated optional decomposition. This mission formalizes that last result.
Timeline:
Fix a Polish space , a horizon and . Let for . Then is a single point and , and a point of is read as the first coordinates of a path. The -field is the universal completion of .
For each and each node a nonempty convex set of probability measures on is given, and its graph is an analytic set. The set of possible models consists of all products whose kernels take values in . A set is -polar if it is null under every . A property holds -quasi surely (q.s.) if it holds outside a polar set.
Stock prices are Borel. A strategy is predictable: is a function of the first coordinates. The wealth at time is
NA() holds if q.s. implies q.s. A martingale measure is a probability under which is a martingale. The set
contains those that are absolutely continuous with respect to some (written ). A function with values in is upper semianalytic if every set is analytic.
At one node , the increment defines a one-period market under , with its own no-arbitrage condition NA() and one-period martingale measures . The conditional sublinear expectation is
Let NA() hold and let be an adapted process such that is upper semianalytic and in for all and . Then the following are equivalent:
at every arbitrage-free node where q.s.
The decomposition is the dynamic counterpart of superhedging duality. Duality identifies the price . The optional decomposition, applied to the process of conditional superhedging prices, produces one strategy that superhedges under all models at once and a nonnegative increasing process recording the surplus. The proof works in a nondominated model with one strategy that is measurable in the universal completion, and this is what makes the theorem usable under volatility or model uncertainty, where no single model can be singled out. The equivalence also characterizes the processes that are supermartingales under every : up to a polar set they are exactly the wealth processes of strategies that consume.
The result is proved in the paper; no part of it has a machine-checked proof, on the platform or in Mathlib. Mathlib has martingales, conditional expectation and analytic sets. It has no quasi-sure analysis, no product of measurable selectors of a random set of measures, no conditional sublinear expectation and no superhedging. The mission produces a machine-checked development of the one-period-to-multi-period machinery of the paper (Theorem 4.5, Lemmas 4.6 and 4.10) and of the decomposition itself.
With one dominating measure, the classical proof works under a fixed equivalent martingale measure and uses conditional expectations and a single null-set structure. Here the measures in may be mutually singular, so conditional expectations under different disagree off their supports, and no countable family of measures controls all null sets. The proof has to work node by node, . Every object built at a node (the worst-case conditional expectation, a near-optimal measure, a hedging ratio) must then be glued back together measurably in . Borel measurability is not preserved by taking suprema over the random set . Upper semianalyticity is, but only together with measurable selection theorems for analytic sets (Jankov–von Neumann) and the universal completion. The first idea, which is to apply the classical theorem under each separately, fails. It gives one strategy per model, and in general uncountably many models cannot be aggregated into one strategy.
The Lean development uses the following conventions.
Fin t → Ω₁, and measures are Borel. -measurability is universal measurability, which is the published platform definition BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable.V t : (Fin t → Ω₁) → ℝ, so adaptedness is built into the type.H u is the paper's .EReal, with . Suprema over are taken in EReal.The increasing process must be adapted and nondecreasing on every path. Dropping monotonicity would make condition 2 trivially true, with for any . Integrability and supermartingale properties are always stated with explicit -integrability, so Bochner integrals of non-integrable functions cannot make a statement vacuous.
The development needs the following infrastructure:
These pieces are shared with the companion mission Arbitrage and Duality in Nondominated Discrete-Time Models I, which formalizes the superhedging theorem. Contributions to either side are welcome. The paper derives (ii) ⇒ (i) from Lemma A.1, a classical fact about local and generalized martingales under one measure, which is not posed as a milestone here.
Master equations are partial differential equations whose state variable is a probability measure. They arise as the dynamic programming equations of mean-field control problems, as the limits of large particle systems, and as the pricing equations of options on a whole population. Their coefficients and solutions are functions on a Wasserstein space, which is infinite dimensional, and classical (smooth) solutions are known only under strong regularity assumptions (Cardaliaguet–Delarue–Lasry–Lions 2019). A notion of weak solution for which existence, comparison and uniqueness can all be proved is therefore the basic missing tool.
C. Wu and J. Zhang (Ann. Appl. Probab. 2020) propose such a notion for parabolic master equations on the space of laws of continuous paths, in the spirit of the viscosity theory for path-dependent PDEs of Ekren, Keller, Touzi and Zhang (Ann. Probab. 2014). This mission formalizes its §4: the definition of viscosity solutions and the comparison principle that makes them unique.
Fix a horizon and a dimension . The canonical space is with the uniform norm , the canonical process is , and . is the set of probability measures on with ; is the law of the stopped path . The state space is with the pseudometric
where on laws is the 2-Wasserstein distance. A function has a time derivative , a path derivative and a second derivative , defined through a functional Itô formula along semimartingale laws.
The master equation (3.1) is
with a generator that is continuous in , Lipschitz in , and Lipschitz in in the averaged sense (3.2) of Assumption 3.1.
For , is the set of laws that agree with up to time and under which is a semimartingale on with drift bounded by and half squared diffusion bounded by . Test functions at are functions on touching from above or below there, (4.2). is an -viscosity subsolution (supersolution) if () for every such test function, and a viscosity solution if it is both for one (Definition 4.4). The Perron envelopes , of (4.17) are the infimum of piecewise classical supersolutions above and the supremum of piecewise classical subsolutions below .
Under Assumption 3.1 and , if is a viscosity subsolution, a viscosity supersolution, , the classes are nonempty, and
then on , and is the unique viscosity solution with terminal condition .
The comparison principle is what turns a definition into a theory: it gives uniqueness, it identifies value functions of mean-field control problems with the solution of their master equation, and it is the input of stability and convergence arguments for numerical schemes. Theorem 4.13 reduces well-posedness to condition (4.19), and the authors verify (4.19) in examples (§4.6) via Theorem 4.14. The compactness of (Lemma 4.1) is the device that replaces local compactness, which the Wasserstein space lacks; it is reusable for any viscosity theory over semimartingale laws.
These results are proved on paper. No machine-checked development of viscosity solutions on Wasserstein spaces, or of the path-dependent functional Itô calculus on laws, is known to exist. A formalization would produce a checked notion of viscosity solution for master equations, the compactness of bounded-characteristic semimartingale laws, and the comparison machinery, and would expose the points where the printed proofs are sketched (see below).
The obvious route, copying the finite-dimensional theory, fails at two places. First, the doubling-of-variables argument for comparison needs a penalization on the state space that is smooth and coercive; on under neither is available, which is why comparison is reached through partial comparison and Perron envelopes. Second, maxima of need not be attained on Wasserstein balls, which are not compact; the theory therefore tests only on , and Lemma 4.1 (via Zheng's tightness criterion for semimartingale laws and uniform integrability of ) is what makes the extrema exist. The printed proof of Theorem 4.13 opens with " is lower semicontinuous and is upper semicontinuous"; as printed the directions are swapped (an infimum of functions continuous in is upper semicontinuous in ), and the members of are only càdlàg in , so the continuity of needed for the conclusion requires an argument of its own.
Time is , and every condition is imposed only at , . is the Euclidean space, matrices are real matrices with the Frobenius norm, and . is the published WassersteinDRO.Duality.wassersteinDistance on laws of paths; Brownian motion and the Itô integral are the published EthierKurtz definitions. Membership in is the existence of a representation of as the law of an Itô process from time with , (§2.4). A object is a record of a function and three derivative functions, and the functional Itô formula (2.25) is required in drift form for every representation, which equals (2.25) because the stochastic integral has mean zero. Test sets encode "" literally, and the data of a test function at are its values at , . The Perron envelopes are extended-real infima and suprema over the classes (4.18); (4.19) is stated with a real-valued .
Two readings are fixed. Assumption 3.1(i) is continuity of for fixed continuous of linear growth. "" in Theorems 4.6 and 4.11 is replaced by the larger class it is used through (Remark 4.3(i)): data continuous on lying in for all , , , so those statements are at least as strong as printed.
The definitions cannot be satisfied vacuously: every test set requires a witness law in , the class contains the constants (checked in Lean), and a viscosity solution uses one for both halves. The semi-jets range only over -measurable continuous arguments of linear growth, as printed.
Contributions are welcome at every level: the moment bound (4.1) and Lemma 4.1 need tightness and uniform-integrability results for semimartingale laws on path space that Mathlib does not have; Theorems 4.7 and 4.9 are self-contained manipulations of the definitions; Theorems 4.6 and 4.11 and Proposition 4.12 need the compactness lemma and the Itô identity of test functions.
Games with many interacting agents, such as traffic participants, users of a shared communication channel or firms in a market, are rarely solvable exactly: a Nash equilibrium of an -player stochastic game requires each agent to track the whole population, and its computation grows with . Mean-field game theory replaces the population by its limiting distribution. A single representative agent faces a deterministic flow of state distributions, and consistency requires that this flow is the one the agent's own optimal policy generates. The equilibrium of this limit problem is then used as an approximate equilibrium of the finite game, with each agent acting only on its own state.
Most of this theory concerns risk-neutral agents, who minimize an expected cost. Saldi, Başar and Raginsky (arXiv:1808.03929; Math. Oper. Res. 2020) treat discrete-time agents with an exponential utility of the discounted cost, the classical risk-sensitive criterion that penalizes the variance of the cost as well as its mean. The paper proves two results: a mean-field equilibrium exists (Theorem 1, the first mission of this series), and the equilibrium policy is an approximate Nash equilibrium of every large enough finite game (Theorem 3, this mission). The risk-neutral counterpart is Saldi, Başar and Raginsky, SIAM J. Control Optim. 2018 (arXiv:1612.07878).
States lie in a Polish metric space , actions in a compact Polish space , and is the set of Borel probability measures with the weak topology. The model consists of a transition kernel , a one-stage cost , an initial law , a discount factor and a risk factor .
In the -agent game, the states are i.i.d. . At each time , agent draws from its Markov policy , and the next states are drawn independently from , where is the empirical distribution of the states. Agent 's cost is
A profile is an -Markov-Nash equilibrium if no agent can lower its by more than by switching to another Markov policy.
In the mean-field game, one agent faces a flow : , with cost . A mean-field equilibrium is a pair in which minimizes and is the flow of state laws that generates.
The hypotheses are Assumption 1 (bounded continuous with , weakly continuous , compact , and a moment function with and ) and Assumption 2. Part (a) of Assumption 2 asks that the moduli
tend to , where is the bounded-Lipschitz metric. Part (b) asks that the equilibrium policy be weakly continuous in the state.
For every there is such that, for every , the profile is an -Markov-Nash equilibrium:
The statement fixes no rate. It is the paper's main approximation result.
The milestones follow the paper's proof. The first seven work in an augmented model, whose state carries the accumulated discounted cost, so that the exponential criterion becomes a terminal cost . They are: Proposition 6 (the augmented model has the same finite-horizon costs); Lemma 5 (the augmented flow ); Proposition 7 (propagation of chaos, ); Proposition 8 (convergence of the augmented cost); Proposition 9 (propagation of chaos with one deviating agent); Proposition 10 (the deviating agent's state law); Proposition 11 (the deviating agent's augmented cost). The last three are stated in the original model: Theorem 4 (the finite-horizon limits (14)–(15)), Corollary 1 (the infinite-horizon comparison), and the first display of the proof of Theorem 3 (deviations may be restricted to weakly continuous policies).
Theorem 3 justifies the use of a mean-field equilibrium as a decentralized policy in risk-sensitive games with many players. The equilibrium is computed once, from a single-agent problem, and each agent uses only its own state, yet no agent of a large enough population gains more than by deviating. The result extends the risk-neutral approximation theorem to the multiplicative criterion. Because the exponential cost does not decompose over time, the risk-neutral argument cannot be applied directly: the proof first passes through the augmented model and a finite-horizon truncation.
The result is proved in the paper; none of it is formalized. The mission formalizes the statement and the proof's intermediate results. That requires the -agent law, a product of kernels driven by the empirical measure, built from Mathlib's Ionescu-Tulcea construction, and propagation of chaos for an interacting Markov chain on a Polish space. Alternative proofs of any milestone are welcome, as are quantitative versions of the limits.
The cost is the expectation of a product of one-stage factors, not a sum, so the convergence of the empirical measure gives no direct control of it. The paper therefore enlarges the state with the accumulated cost, and the finite-horizon limits must then be transferred back to the infinite horizon through a uniform tail bound. The coupling between agents runs through the empirical measure, which enters both the transition and the cost. Propagation of chaos (Proposition 7) is an induction over time that needs continuity of and in the measure argument uniformly in (Assumption 2-(a)) and a conditional variance bound. The deviating agent is not exchangeable with the others: its state law must be compared with that of a mean-field chain under its own policy (Proposition 10), uniformly over arbitrary sequences of deviations. Finally, a best response may be only measurable. The reduction to weakly continuous deviations, which the paper takes from its risk-neutral predecessor, is needed before any weak-convergence argument applies.
Lean namespace RiskSensMFG.Nash. The definitions are in four files: the model, policies, the single-agent law and the flow (Model); the mean-field equilibrium, , total variation and Assumption 2-(a) (Equilibrium); the -agent game (Game); and the augmented model (Augmented). Conventions:
ProbabilityMeasure with the weak topology and its Borel -field (not the Giry one), and is a Markov Kernel. The standing assumptions , and measurable are a predicate Model.Standing. Assumption 1 is stated in full, including the moment function, although the proof of Theorem 3 does not use parts (d)–(e).Fin N, and the paper's Agent 1 is index 0; limits in are taken along so that Agent 1 exists. The empirical measure of the empty configuration is set to and enters no statement.No hypothesis is vacuous: a sorry-free check exhibits a model satisfying the standing assumptions, Assumptions 1 and 2 and the equilibrium condition simultaneously, with . This rules out the trivial reading in which a non-integrable integrand makes every cost and every profile an -equilibrium. Theorem 1 (existence of the equilibrium) is the other mission of the series; here the equilibrium is a hypothesis.
Distributionally robust optimization (DRO) hedges a decision against uncertainty in the data distribution. It minimizes the worst-case expected loss over an ambiguity set of distributions around a nominal one, typically the empirical distribution of the data. Ambiguity sets built from the Wasserstein (optimal-transport) distance are standard in operations research and machine learning, because they contain distributions with supports different from the nominal one. A known drawback is that the worst case is attained at discrete distributions, which is unrealistic when the true distribution is continuous.
Wang, Gao and Xie (arXiv:2109.11926v5) replace the Wasserstein distance by the Sinkhorn distance, the entropically regularized optimal-transport cost of Cuturi (NeurIPS 2013). Their main theorem is a strong duality result: the infinite-dimensional worst-case problem over a Sinkhorn ball equals a one-dimensional convex minimization. This mission formalizes that theorem.
Timeline:
Let be a measurable space. The data are:
For a probability distribution , the Sinkhorn distance (Definition 1, with reference measures and ) is
where is the set of couplings with these marginals. The primal value is the worst-case expected loss over the Sinkhorn ball,
The dual problem uses three more objects. The kernel distribution is . The adjusted radius is . The dual value is
where the objective at is .
Assumption 1 requires:
Condition 1 asks for some with for -a.e. .
Under Assumption 1:
(III) If , then when the dual objective is finite at some , and otherwise.
(IV) If and Condition 1 holds, then is the unique dual minimizer if and only if
The milestones are the numbered lemmas of the paper's proof, in the order the proof uses them:
The result. Theorem 1 turns a supremum over an infinite-dimensional set of distributions into a scalar convex program. That program can be solved by first-order methods using only samples from and from the kernels , which is the basis of the paper's algorithm (Section 4). The proof also constructs the worst-case distribution: it is absolutely continuous with respect to , not discrete. Theorem 1(IV) says exactly when the ambiguity constraint is binding. The finite-support conic reformulation (Corollary 1) and the closed form for linear losses (Example 1) both follow from the theorem.
Formalizing it. The theorem is proved in the paper; no machine-checked proof exists. Formalization adds two things. First, it pins down the extended-valued conventions: , and all take values in , and the paper does not specify how undefined expectations and the objective are treated. Second, it checks every case of the proof, including the degenerate ones. Doing so has already corrected two statements; see Formalization scope.
Weak duality (Lemma 1) is Lagrangian relaxation plus the Gibbs principle. The difficulty is the reverse inequality . Interchanging the supremum over distributions with the infimum over requires a minimax theorem. The usual minimax theorems need compactness or semicontinuity in the distribution variable. The paper's setting has neither: is an arbitrary measurable space, is only measurable and may be , and is arbitrary. So a minimax theorem cannot be applied directly.
The proof instead constructs near-optimal primal distributions from the dual minimizer. This needs three separate cases:
Each case needs integrability facts about in which and interact. Disintegrating couplings (Assumption 1(IV)) and making the extended-valued expectations meaningful are a further source of work in Lean.
All values (primal value, Sinkhorn distance, dual objective) are EReal. Expectations are the published DupacovaWets.Consistency.expect: , with lower Lebesgue integrals in and the convention . The Bochner integral appears only in , which every theorem assumes finite.
Further conventions:
essSup f ν, not as a limit. Logarithms are ENNReal.log, so and ; .withDensity measure. Families are Markov kernels on all of .Hypotheses added to the page:
"" is read as "-a.e.". "" is read as " is the unique dual minimizer".
Corrections to the paper:
No statement involves an constant.
A formalization that lets an undefined Sinkhorn integrand evaluate to (Mathlib's ) is ruled out: it would put every distribution into the ball and make the theorem trivial. The combined integrand and the convention exclude this.
A complete development needs:
The first two are reusable well beyond this mission. Contributions toward any milestone, and toward these general lemmas, are welcome.
Classical arbitrage pricing fixes one probability measure describing the market and asks for the cheapest way to dominate a payoff -almost surely. When the model itself is uncertain, this choice is not available: a trader who only trusts a family of possible models wants a hedge that works under every one of them. Two literatures meet here. Robust (model-independent) finance studies hedging that must hold for all paths, as in the martingale-optimal-transport approach to option bounds (Beiglböck, Henry-Labordère, Penkner, 2013). Nondominated model uncertainty studies families with no single reference measure, as in the quasi-sure analysis of Denis–Martini (2006) and the volatility-uncertainty literature. Bouchard and Nutz (2015) give a discrete-time framework that contains both extremes (all measures on a path space; a single measure) and prove the fundamental theorems and superhedging duality for it.
Timeline of the dominated and robust predecessors:
Fix a horizon and a Polish space . Paths are , and holds the first coordinates. Information at time is the universal completion of the Borel -field of .
For each and history , a nonempty convex set of probability measures on describes the possible laws of the next coordinate. Its graph must be an analytic set. The set of models consists of all products whose kernels choose . A property holds -quasi surely (q.s.) if it holds -a.s. for every .
There are stocks with Borel prices and options , Borel on , bought or sold at time at price . A semistatic strategy consists of a predictable and a vector ; its terminal gain is
No-arbitrage NA() says that a gain which is q.s. nonnegative is q.s. zero. The superhedging price of a claim is
The dual objects are the martingale measures , meaning for some . Under the stock is a martingale and for all ; they form the set . Given a weight , set . Expectations of arbitrary measurable functions use the convention with .
Let be a random variable with , let NA() hold, and let be upper semianalytic with . Then
and some satisfies -q.s.
The milestones follow the paper's proof:
The superhedging theorem identifies the robust price of a claim as a supremum of linear prices. This turns a hedging problem into an optimization over measures, which is how robust option bounds are computed in practice. Remark 1.4 of the paper gives another consequence: every martingale inequality follows from a pathwise inequality . The first and second fundamental theorems make the nondominated framework a complete analogue of the classical theory. NA() is equivalent to and sharing their polar sets, and replicable claims are those whose price is the same under every martingale measure.
All results are proved in the paper. None of them, nor the classical dominated discrete-time FTAP, is formalized in Lean or Mathlib as far as is known. A formalization produces machine-checked statements of the model (analytic random sets, products of universally measurable kernels, quasi-sure analysis) and proofs of the fundamental theorems on top of it. Alternative arguments and extensions (portfolio constraints, infinitely many options) are also welcome.
There is no reference measure. Two dominated tools therefore fail. Closedness in cannot be applied, because convergence must hold quasi surely. A Hahn–Banach separation in a single space cannot produce martingale measures either. The paper argues one period at a time instead and glues the periods together measurably. That gluing is where the work lies. The one-period dual value and the one-period hedge must depend measurably on the history , but the value function of a Borel claim need not be Borel. The argument therefore runs in the class of upper semianalytic functions and needs measurable selection theorems for analytic sets. A recursion that tries to keep everything Borel breaks down at the first step.
Fin t → Ω₁ with [PolishSpace Ω₁] [BorelSpace Ω₁]. Measures are Borel measures, and -measurability is universal measurability. The published definition BertsekasShreve.AnalyticSelection.Measurability is reused for this.ProbabilityMeasure with the weak topology. is generated by Borel Markov kernels lying in almost surely; this is the paper's equivalent formulation on p. 4.H u is the paper's , a universally measurable function of the first coordinates.EReal. Expectations of non-integrable functions are the extended expectation . Prices are EReal infima with , and suprema over are EReal suprema.Two encodings would trivialize the mission and are excluded. Replacing by an arbitrary set of measures drops the product structure that the theorems need. Bochner integrals for would return on non-integrable claims and make the duality meaningless. Neither encoding is used.
A complete development needs:
The selection and kernel infrastructure is reusable well beyond this paper, for instance in dynamic programming on Borel spaces. Contributions of these foundations are welcome.
Elias S. W. Shiu and Xiaoyi Xiong (2021), An elementary derivation of Hattendorff's theorem, European Actuarial Journal 11, 319–323, https://doi.org/10.1007/s13385-020-00256-9. In that paper equation (1) defines the fully discrete insurer's complete-life loss; equation (2) gives the Hattendorff variance formula, and equations (3)–(5) connect annual reserve recursion to the net amount at risk by summation by parts.
The present mission proposes an original countable-outcome and L²-convergence formalisation of that discrete formula. It is not asserted that the authors stated this exact Lean theorem, and it does not inherit proofs from the earlier finite-scenario missions.
Let be the realised curtate lifetime, the number of full years remaining until the year of death. Its possible values are not uniformly bounded. Set , where and . Assume the survival tail is positive in every year:
These are unconditional death masses and conditional mortality and survival rates . Some individual may be zero. The outcome space is genuinely countable; a finite Fintype of realised death years would force a bounded support and undermine the claimed infinite-horizon extension.
The annual mortality martingale difference is defined pathwise by
For , ; at death , ; and after death , it is zero. Let the discounted net amount at risk for the payment at year-end be . This matches Shiu–Xiong's year-end death-benefit timing. The truncated centred reserve loss and the pathwise complete-life centred loss are
The complete-life variable is well-defined on each realised finite and whenever . These definitions only model the centred innovation component. A separate cashflow reserve-recursion bridge, as in earlier missions, is needed to identify a given insurer contract loss with ; this mission does not silently assert that for arbitrary premium sequences.
The discrete expectations are weighted countable sums. Show, under summability and positive in-force mass,
Using finite sums and cross-year orthogonality first gives
The capstone introduces the mathematically substantive L² risk condition
This implies that the sequence of truncated centred losses is Cauchy in the probability-weighted L² space; its limit equals the pathwise stabilised . Hence
The capstone explicitly assumes nonnegative weights, unit total mass, positive survival tails, countable weight summability and risk-variance summability. The formal statement must not be weakened to merely a pointwise convergence or an unjustified interchange of infinite sums.
A geometric law with , , and gives
Its finite-year variance is . The repository includes exact-rational tests for 13 horizons. The model allows an individually zero death mass but requires positive tails. Every scenario terminates in some finite year; adding a outcome with positive weight would require a separate transversality condition and is not part of this mission.
The mission supplies four mathematical definitions, eleven supporting milestone theorems and one combined capstone theorem. Prove the indicator identities, the countable weighted first and second moments, finite orthogonality and finite allocation, and finally the L² passage to the unbounded lifetime. The target Lean namespace is `ActuarialValuation` in the pinned Mathlib environment. Finite-year results from earlier actuarial missions are background, not automatic countable-measure proof imports. None of the present open theorem statements is an accepted proof.
A prospective insurance reserve is the conditional expected amount needed to fund the remaining liabilities of an in-force policy. Annual realised claims differ from their conditional expectations, and the variation in total discounted insurer loss can be allocated to these unexpected annual outcomes. Hattendorff's theorem expresses that allocation as a sum of year-specific variance contributions. The fully discrete case contains an important factor: the conditional probability of surviving the policy year.
Shiu and Xiong's article An elementary derivation of Hattendorff's theorem [1] gives a direct discrete derivation. With curtate lifetime , annual death benefits paid at time , premiums paid at time , discount factor and prospective reserve , their formulas include
In particular, the variance identity they derive has a mortality-year survival factor,
This mission establishes the finite-scenario mortality-innovation component of that result. It derives the orthogonality of annual death surprises rather than assuming it. It does not yet identify their weighted sum with the full insurance loss ; that requires the separate time-dependent reserve recursion and summation-by-parts identities in [1, equation (3)]. Those insurance cashflow bridge obligations are explicitly reserved for the next mathematical stage.
Let be a finite scenario space, its weights and a curtate future lifetime, where means death during year , at the end of which the death benefit is payable.
For policy duration , define the in-force probability mass and the death-year mass:
For probabilistic interpretation assume in addition . The exact algebraic statements do not generally require weight normalisation, though they explicitly require nonnegative weights for probability inequalities.
The disjoint identity
gives . If , the conditional one-year death and survival probabilities are
Division by is totalised as a Lean real expression but is not interpreted as conditioning on an impossible event. All substantive annual-innovation results impose positive in-force mass for the years used.
For each outcome and policy year define the mortality innovation
It equals for death in year , equals for an individual surviving that year, and equals zero after death. Under ,
The orthogonality is more than a generic assumption. For , if then the policy is still in force at , so the preceding year must have been survived and . If , the product is also zero. Thus, pointwise,
Taking the weighted expectation and using the centring of gives
These innovations can be uncorrelated despite being highly dependent events generated by the same curtate lifetime. They must not be claimed independent.
By conditioning on the death-year and survival outcomes, the squared mortality surprise has expected value
The final conditional survival factor is characteristic of the fully discrete actuarial Hattendorff identity. It is not an arbitrary variance weight, and it cannot be dropped by borrowing a continuous-time formula.
For a finite horizon , let be any deterministic year-specific net-amount-at-risk coefficient. Define the discounted innovation portfolio
When for each , the annual zero-mean and cross-year orthogonality identities yield
For nonnegative unit-sum weights this is the usual finite-scenario variance. The capstone couples the derived pairwise cross-year zero moments with the resulting finite-horizon variance formula. No reserve balance, actuarial premium equation or conditional L² filtration theorem is silently assumed.
The formal graph contains seven definitions: survival and death masses, conditional death and survival rates, the mortality innovation, its finite discounted portfolio and a finite weighted variance. Supporting theorems establish event partitions, nonnegativity, , behaviour after death, innovation centring, a pointwise earlier/later product identity, orthogonality, the discrete second-moment formula, zero horizon and portfolio moments. The capstone packages zero covariance and the mortality-weighted variance allocation.
The variance theorem is valid for arbitrary deterministic coefficient sequence and any finite number of years with positive survival mass; it does not presume every life dies before that horizon. is covered by the empty sum. For standard actuarial application choose , as in [1]. A future bridge must show that this particular innovation portfolio equals the centred insurer loss under the correct reserve recursion and endpoint conventions.
The root theorem is therefore a genuine probabilistic predecessor, not an assertion that the entire traditional Hattendorff theorem has already been proved. The mission is proposed for formal proof: private remote statement elaboration and finite rational tests, if accepted, do not constitute public Prove2Me proof acceptance.
[1] Shiu, Elias S. W. and Xiong, Xiaoyi (2021), “An elementary derivation of Hattendorff's theorem”, European Actuarial Journal, 11, pp. 319–323, equations (1)–(3). This is the direct source for the fully discrete variance factor, net amount at risk and finite summation-by-parts strategy.
[2] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, §6.7, Allocation of the Overall Loss to Policy Years. The reserve-change and annual-loss decomposition provides broader actuarial context.
[3] Gerber, Hans U., Leung, Bartholomew P. K. and Shiu, Elias S. W. (2003), “Indicator Function and Hattendorff Theorem”, North American Actuarial Journal, 7(1), pp. 38–47. Explains the central role of indicator functions and the relationship to uncorrelated martingale increments.
An insurer may adjust its reinsurance retention or other risk-management decision repeatedly, rather than optimising a single future year's payments. Current action choices affect both the immediate net reward and the state of the business next year, which changes the value of all later decisions. A finite-horizon Markov decision process makes this multi-year optimisation precise.
Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Chapter 4 [1], develops the finite-horizon Bellman equations and existence of optimal deterministic Markov policies for finite decision problems. Mission XV introduces a finite-action Bellman operator and excess-of-loss claim splitting, but is still under moderator review. This mission formalises the full finite-horizon backward recursion and optimal deterministic policy existence, without importing an unreviewed declaration.
The reinsurance motivation comes from Brachetta and Ceci's optimal excess-of-loss study [2]. Their original problem is a continuous-time stochastic-factor and HJB verification problem. The present mission is strictly a finite-state, finite-action, discrete-time precursor. Neither the stochastic-factor diffusion nor the jump-process verification theorem is asserted here.
Let be a finite state type, and let be a finite nonempty set of admissible control actions. A state can encode a simplified surplus, rating, claims regime or any finite risk-class abstraction. At the beginning of a policy year the insurer is in state and selects an action .
Let be the transition weight for next state , and the immediate reward. The usual Markov model requires and for every . The general algebraic definitions accept real matrices, while the economic probabilistic interpretation requires valid row-stochasticity.
If is the continuation value in state , the return from action is
where is a deterministic annual discount factor. The discount is applied to following-year continuation, not to the current reward. For policy interpretation is conventional, but finite-horizon algebra makes sense at other fixed real as well.
The one-year Bellman optimisation is
The maximum is attained because is finite and nonempty. Both this attainment and the inequality are explicit supporting theorem obligations.
Let denote a terminal benefit or terminal value. A deterministic nonstationary Markov policy is a mapping
Here is the action chosen when decisions remain, so the index counts backwards towards the terminal time. This makes the recursion valid for a homogeneous one-step transition model without reversing calendar-time transitions.
For a fixed policy, recursively define
The policy is nonstationary because its choice at the same state may differ according to remaining time . It is Markov because the action depends only on current state and remaining horizon, not on the entire historical path. The mission does not introduce a path-space filtration or general history-dependent randomised policy, so the precise capstone compares deterministic nonstationary Markov policies.
Define by the finite Bellman recursion
Under and , a larger continuation function cannot reduce the value of any action; taking a finite maximum preserves this monotonicity. That simple inequality allows induction on the remaining horizon to show
The second substantive step is existence of an attaining policy. Since is finite and nonempty, at each remaining horizon and each state there is at least one maximising action. Choosing such actions and combining them recursively gives a single nonstationary deterministic Markov policy satisfying
The capstone combines the universal upper bound and existence of an attaining policy. This is genuinely more than a one-step maximum: it is an optimality result over an arbitrary finite number of sequential decisions.
A complete optimality result against all history-dependent randomised policies would need an additional equivalence argument showing no improvement from extra history or randomisation. Such an extension is well-known for suitable finite Markov models but is not silently claimed by this narrower Lean target.
Four proposed definitions encode the one-step action return, the finite Bellman maximum, policy evaluation and recursively optimal horizon value. Eleven supporting theorem targets establish zero-discount behaviour, action domination and attainment, monotonicity of action and Bellman values, zero-horizon and successor recursions, policy domination and existence of an attaining policy. The capstone packages the latter two results.
At there are no decisions and both values are precisely . At , any continuation is irrelevant to the one-step value. Nonnegative weights and discount are explicit hypotheses for monotonicity and policy domination, rather than false claims for signed matrix weights. The existence of an attaining maximiser in each finite action set does not itself require stochastic row-sum assumptions.
To obtain a reinsurance model from this graph, one must specify how each action corresponds to an admissible retention, how the retention changes reinsurance premiums and retained claim distributions, and how those assumptions determine the transition matrix and rewards . That specialised bridge is separate from the finite-horizon mathematical result.
All theorems are proposed Lean proof targets. Preliminary remote elaboration establishes statement well-formedness only if verified by the authoritative compiler. It does not constitute a completed proof or approval of the mission's mathematical design.
[1] Puterman, Martin L. (1994), Markov Decision Processes: Discrete Stochastic Dynamic Programming, Chapter 4, Finite-Horizon Markov Decision Processes, Wiley. This is the direct mathematical reference for finite-horizon Bellman recursions, backward induction and existence of optimal deterministic policies under finite-state/action assumptions.
[2] Brachetta, Matteo and Ceci, Claudia (2019), “Optimal Excess-of-Loss Reinsurance for Stochastic Factor Risk Models”, Risks 7(2), article 48. This motivates insurance retention as a controlled decision but uses a continuous-time stochastic-factor/HJB model not established by this mission.
[3] Schäffeler, Maximilian and Abdulaziz, Mohammad (2022), “Formally Verified Solution Methods for Markov Decision Processes”, computer-assisted formalisation of Bellman equations, value iteration and optimal policy existence in Isabelle/HOL. This is methodology context only; no proof code is imported into Lean from that project.
A tall matrix with independent standard normal entries is, with high probability, a near-isometry: all its singular values lie in up to Gaussian fluctuations. This is Gordon's theorem together with Gaussian concentration (Vershynin 2012, Theorem 5.32 and Corollary 5.35), the non-asymptotic counterpart of the Bai–Yin law and the model result for the whole theory of non-asymptotic random matrices. In randomized numerical linear algebra the same two ingredients give the expected spectral norm of (Halko–Martinsson–Tropp 2011, Proposition 10.1 (10.2)), its second moment (Tropp–Webber 2023, Lemma B.1), and the lower tail of of a Gaussian sketch, which controls the inverse moments that appear in the analysis of sketching algorithms with rank truncation. None of these results is available in Mathlib; this mission proves them.
A standard Gaussian matrix has independent entries; its law is . Its extreme singular values are
the infimum and supremum over the unit sphere of (); is the spectral norm. For a wide matrix , , the usual is . The Frobenius norm is ; a function on matrices is -Lipschitz if . A chi-square variable with degrees of freedom is for independent standard normals . The letter denotes Euler's number.
For every , with probability at least ,
This is the goal because it is the statement users of Gaussian matrices quote: a quantitative near-isometry with explicit sub-Gaussian deviations. It follows from the expectation bounds (Gordon) and concentration, both of which are milestones.
The results. Gordon's theorem is sharp: and are pinned to within of the Bai–Yin limits for every . Gaussian concentration upgrades it to tail bounds with the optimal sub-Gaussian rate, and the Chevet-type bound is the same mechanism for , where it yields the expected spectral error of the randomized SVD. The small-ball bound covers the other regime, , with polynomial decay of the exact order ; together the two tails make every negative moment , , finite and explicitly bounded, which is what the early-truncated analysis needs.
Formalizing them. Mathlib has the standard Gaussian measure on finite-dimensional inner product spaces but neither Gaussian concentration for Lipschitz functions, nor Slepian's or Gordon's comparison inequalities, nor any result on singular values of random matrices. These are foundational pieces of high-dimensional probability whose formalization would be reused far beyond this series.
The upper bound in Gordon's theorem is proved by Slepian's comparison lemma for the Gaussian process on , and the lower bound by Gordon's minimax comparison inequality for ; both require a theory of Gaussian processes indexed by continuous parameter sets, or at least a discretization argument with careful limits. Gaussian concentration (Tsirelson–Ibragimov–Sudakov) is usually proved through the Gaussian logarithmic Sobolev inequality or the Ornstein–Uhlenbeck semigroup, with a smoothing step to pass from smooth to Lipschitz functions. Both are long developments with no Mathlib support. The elementary alternatives do not reach the stated constants: an -net argument bounds by with , and a union bound over rows for the small-ball estimate is exactly how the stated bound is obtained, but it needs the fact that the distance from a Gaussian vector to a fixed -dimensional subspace is a variable, which again rests on rotational invariance.
Matrices are sampled from the product measure on arrays. is sMin, the real infimum over the unit sphere of ; is assumed so the sphere is nonempty, and is not assumed for Gordon's theorem (for one has and the lower bound is trivial, as in the source). is Mathlib's operator norm. Expectation bounds are stated together with integrability of their integrands, so the Lean convention that non-integrable functions integrate to cannot trivialize them. Probabilities are measures in compared with of the real bound; the goal's lower bound uses truncated subtraction and is vacuous for , exactly as in the source. Gaussian concentration is stated with and , which the sources leave implicit (for or the event has probability one). Results that the sketching literature states for wide matrices are stated here for tall matrices via , with .
Welcome contributions: Gaussian concentration for Lipschitz functions on (any proof), Slepian's and Gordon's inequalities, the -Lipschitz property of and , the chi-square Chernoff bounds, and the law of the distance from a Gaussian vector to a subspace.
Shared definitions: the items of this mission import Definitions.Def_GaussianMatrix_basic, a draft of Mission I; submit that proposal first so the import resolves at compile time.
Series: I. Rotation Invariance and Moment Identities · II. Inverse Moments of the Pseudoinverse · III. Extreme Singular Values and Concentration. All three missions share the definition bundle GaussianMatrix_basic, published with Mission I, and the namespace GaussianMatrix.
Randomized algorithms for low-rank approximation — the randomized SVD of Halko, Martinsson and Tropp (HMT 2011), generalized Nyström, randomized subspace iteration, one-pass sketching (Tropp–Webber 2023) — multiply the input matrix by a random test matrix with independent standard normal entries. Every error bound for these methods rests on a small number of facts about such standard Gaussian matrices: they are invariant under rotations, disjoint blocks of a rotated copy are independent, and the second and fourth moments of a linearly transformed Gaussian matrix are given by explicit formulas. These facts are classical, but none of them is available in Mathlib, so a Lean development of randomized numerical linear algebra currently has to carry every one of them as an explicit hypothesis of its main theorems. This mission removes those hypotheses.
For , a standard Gaussian matrix of size is a random matrix whose entries are independent random variables. Its law, written , is the product measure on real arrays.
For a real matrix , is the squared Frobenius norm; is the dimension of its column space. A matrix has orthonormal columns when ; a square such matrix is orthogonal. For , a matrix with independent entries is written with , so that is an unbiased sketch of the identity.
For fixed , and with independent entries,
This is the exact mean-squared error of the sketched product as an estimator of , a direct consequence of Isserlis' pairing formula for Gaussian fourth moments. It is the goal because it is the one fourth-moment computation the series needs and because every other identity in the mission is a step towards it.
The results. Rotational invariance and block independence are the mechanism behind every conditioning argument in randomized linear algebra: writing the right singular vectors of the input as , the sketch splits into independent standard Gaussian blocks and , and one may condition on while treating as fresh. The second-moment identity then turns the deterministic range-finder bound into , and the approximate-multiplication identity gives the one-pass error terms. Almost-sure full rank is what makes a genuine pseudoinverse.
Formalizing them. Mathlib has the one-dimensional Gaussian measure, product measures, independence of coordinate projections, and (recently) the standard Gaussian measure on a finite-dimensional inner product space together with its invariance under linear isometries. None of the matrix-level statements above is in Mathlib. Once proved here they are reusable by every later mission in the series and by any formalization of randomized low-rank approximation, whose expectation-level inputs (e.g. ) follow from these milestones together with the inverse moments of Mission II.
Rotational invariance is not a computation with densities on that Mathlib supports out of the box: the clean route is through characteristic functions or through the basis-independence of the standard Gaussian on an inner product space, transported along the linear isometry of with the Frobenius inner product. Independence of the blocks requires identifying with a product measure and then projecting onto disjoint coordinate sets, with a completion of to an orthogonal matrix when . The moment identities are finite computations, but the fourth-moment identity needs the Gaussian moments , organized through Isserlis' pairing formula over a four-fold sum of indices; the obvious entrywise expansion produces terms that must be collapsed symbolically. Almost-sure full rank is the statement that the zero set of a nonzero polynomial ( of a maximal square submatrix) is Lebesgue-null, which must be established for the product Gaussian measure.
The sample space is the function type with the product -algebra; a sample is viewed as a matrix through the identity map . Expectations are real Bochner integrals: for an identity with a nonzero right-hand side this forces integrability, and the integrands here are polynomials in Gaussian entries. Laws are stated as equalities of pushforward measures; independence is Mathlib's IndepFun. Dimensions may be ; all statements remain true in that case. The hypothesis silently forces (vacuous otherwise), which matches the source.
The definition bundle GaussianMatrix_basic supplies the law , , , the spectral norm (Mathlib's operator norm), the smallest singular value and the pseudoinverse ; it is shared by the whole series. Welcome contributions: the Gaussian integration-by-parts and Isserlis lemmas for finite index sets, the identification of with Mathlib's stdGaussian on the Frobenius inner product space, and the "polynomial zero sets are null" lemma for product measures.
Series: I. Rotation Invariance and Moment Identities · II. Inverse Moments of the Pseudoinverse · III. Extreme Singular Values and Concentration. All three missions share the definition bundle GaussianMatrix_basic, published with Mission I, and the namespace GaussianMatrix.
Networks of conductance-based neurons, such as FitzHugh–Nagumo networks, are modelled by systems of stochastic differential equations in which each neuron interacts with the others through synapses, and the signal from one neuron reaches another only after a transmission delay. Biological neurons sit at positions in space, belong to a few distinct subpopulations, are driven by Brownian and Poisson (jump) noise, and vary from one to another; the last feature is modelled by a random disorder parameter. When the number of neurons tends to infinity, the state of a typical neuron is expected to follow a McKean–Vlasov equation: an SDE whose coefficients depend on the law of its own solution. S. Mehri, M. Scheutzow, W. Stannat and B. Z. Zangeneh (arXiv:1805.01654; Ann. Appl. Probab. 30 (2020), DOI 10.1214/19-AAP1499) prove that this limit equation is well-posed, with coefficients that are only monotone (one-sided Lipschitz), a general delay, jump noise, spatial structure and disorder all at once, and then prove propagation of chaos towards it.
Earlier work, as surveyed on p. 3 of the paper, covered parts of this setting: global Lipschitz coefficients (Quiñinao and Touboul 2015, and the paper's references [10, 11]), locally Lipschitz coefficients (Baladron, Fasoli, Faugeras and Touboul 2012, with the clarification of Bossy, Faugeras and Talay 2015 on the localization by hitting times; the same issue affects Touboul 2012), one-sided Lipschitz coefficients with diffusive noise (Luçon and Stannat 2014), and Lévy noise under global Lipschitz assumptions or gradient-type local dynamics (Andreis, Dai Pra and Fischer 2018). The paper constructs the solution by an Euler approximation, which, by the authors' account, had not been applied to McKean–Vlasov equations before.
Fix dimensions (state), , (noise), (space), a delay and subpopulations, located at pairwise disjoint measurable regions whose union is bounded. A finite Borel measure on with describes the spatial distribution of neurons. A disorder probability space is fixed. On a filtered probability space there are an -dimensional Brownian motion , -dimensional Brownian motions , Poisson random measures on with intensity ( σ-finite; ), all independent, and initial paths .
For a path , write for the segment , . The equation is
where is an independent copy of the solution and its expectation. The local dynamics satisfy the monotonicity and growth conditions (H1)–(H3) of Hypothesis 1.1 with locally integrable random rates , , ; the synaptic coefficients are Lipschitz (H4) and of linear growth (H5) in , with rates , , the path variable measured through a probability measure on . In Lean, the model is the definition module NeuroMV.WellPosed.Setting: Space, Coeffs, Hyp1_1, Noise/IsNoise, IsStrongSol6, InClass and the constant C1 of (7).
For every there is a process , measurable in , such that for -almost every , is a strong solution of (6) on ,
and every other strong solution in that class satisfies for all .
Theorem 1.5 makes the infinite-population limit of the network well defined; the second main result of the paper, Theorem 1.8, proves that the network converges to it in . The theorem applies to coefficients that are only monotone in the state, which covers the cubic nonlinearity of FitzHugh–Nagumo neurons (Example 1.3), and to synaptic weights of conductance type driven by jump noise. Theorem A.2, proved in the appendix, is a well-posedness and Euler-convergence result for monotone stochastic delay equations with jumps and random coefficients, stated by the authors as new in this generality; it is reusable beyond this paper.
The results are proved in the paper; none of them has a machine-checked proof. The mission produces a Lean statement of the limit equation with the published Brownian and compensated Poisson integral relations, and invites formal proofs of the scheme estimates, the Cauchy property, the identification of the limit, the moment bound and uniqueness.
Under monotone coefficients there is no global contraction, so the Picard iteration that proves McKean–Vlasov well-posedness under Lipschitz assumptions does not apply. Localization by stopping times, the standard replacement for SDEs with monotone coefficients, does not localize the mean-field terms, which depend on the law of the solution at all positions; mishandling this step is the gap that Bossy, Faugeras and Talay pointed out in earlier work, and the acknowledgements (p. 30) record that the first version of this paper contained an unjustified application of the moment estimate of Lemma 1.4. A priori bounds must therefore be uniform in the approximation, and the limit of the mean-field stochastic integrals must be identified, with jumps and delay present. A second difficulty is measurability: the mean-field integrals require the solution to be measurable in the position , and the theorem asserts measurability in .
EuclideanSpace ℝ (Fin k), states EthierKurtz.SDEState d, matrices Matrix (Fin d) (Fin m) ℝ with the Hilbert–Schmidt norm; subpopulations are Fin P, 0-based. Processes are indexed by ℝ on ; drivers by ℝ≥0. Path segments are functions ℝ → ℝ^d read on with the product (cylinder) σ-algebra; the paper's sup-norm Borel σ-algebra is larger, so joint measurability of the coefficients for the cylinder σ-algebra is a mild added requirement.EthierKurtz.HasBrownianItoIntegral, compensated jump integrals the published JacodTodorov10.LLN.HasCompInt, coordinatewise, with integrands cut off after . All Poisson measures are one JacodTodorov10.LLN.IsFPoisson measure on a product mark space, equivalent to independent measures . Independence of the initial data from the drivers is encoded by -measurability.The bibliographic data of the last seven entries are taken from the reference list of the paper (pp. 30–31).
Mean-field games describe large populations of identical agents who interact only through the distribution of their states. Each agent solves a stochastic control problem in which the population appears through a deterministic flow of distributions, and an equilibrium requires that this flow coincide with the distribution the agents generate themselves. The theory goes back to Huang, Malhamé and Caines (2006) and Lasry and Lions (2007) in continuous time. In discrete time, Saldi, Başar and Raginsky (SIAM J. Control Optim. 2018) proved existence of equilibria for risk-neutral agents with discounted costs on Polish state spaces.
Risk-neutral agents care only about expected cost. Many applications in engineering and finance call for agents that also penalize the variability of their cost. A standard way to model this is the exponential (risk-sensitive) criterion with risk factor . Its theory for single-agent Markov decision processes goes back to Howard and Matheson (1972) and Jacobson (1973), and Bäuerle and Rieder (Math. Oper. Res. 2014) treat general utilities. Saldi, Başar and Raginsky (arXiv:1808.03929, Math. Oper. Res. 2020) carry the discrete-time mean-field program over to this criterion. This mission covers its first main result: existence of a mean-field equilibrium (Theorem 1).
The state space and the action space are Polish, and is compact. denotes the probability measures on , with the topology of weak convergence and its Borel σ-field. The model consists of:
A Markov policy is a sequence of kernels . A policy in general is allowed to depend on the whole history . Given a measure flow , a generic agent evolves as
and pays the risk-sensitive cost
For a Markov policy, is the flow of state laws it generates: it starts at and satisfies . A pair is a mean-field equilibrium if and minimizes over all policies.
Assumption 1 asks for the following:
Under Assumption 1 there are a Markov policy and a flow with
In the paper's order of proof:
The result. Theorem 1 is what makes the second main result of the paper meaningful. That result, Theorem 3 and the second mission of this series, states that the equilibrium policy is an -Markov–Nash equilibrium of every -agent game with large enough. Equilibria of finite risk-sensitive games with many agents are rarely computable, so a mean-field equilibrium gives an approximately optimal decentralized policy that ignores the other agents' states. Along the way, the paper proves results on nonhomogeneous risk-sensitive MDPs that it describes as "mostly absent and dispersed in the literature": uniform finite-to-infinite horizon bounds and a characterization of optimal Markov policies. These results are useful outside game theory.
Formalizing it. The result is proved on paper. No part of it, nor of the risk-neutral precursor, has a machine-checked proof. Formalization produces a verified theory of nonhomogeneous risk-sensitive MDPs on Polish spaces, a verified closed-graph argument for the mean-field map, and an exact record of the hypotheses. The paper omits or cites several steps: Proposition 1, Proposition 2, Lemma 2, the conditional optimality (8) and the nonemptiness and convexity of . A formalization has to supply them.
The obvious route is Banach's fixed point theorem for the dynamic programming operator, as in risk-neutral discounted MDPs. It fails here: the cost is multiplicative, and the operator is not a contraction. Uniform convergence of value iteration has to come from the explicit tail bound of Lemma 3 instead.
The second obstacle is the fixed point itself. The natural map, from a flow to the flows of its optimal policies, is set-valued and lives on an infinite product of spaces of measures. Kakutani–Fan–Glicksberg applies only after three steps:
The last step requires the optimal value functions to vary continuously with the flow (Proposition 5) and a portmanteau argument for sets defined by optimality conditions. None of this machinery (the Kakutani–Fan–Glicksberg theorem in locally convex spaces, Prokhorov compactness via moment functions, continuous convergence) is in Mathlib in the required form.
is a type synonym of Mathlib's ProbabilityMeasure E with the weak topology and its Borel σ-field. The kernel is a Mathlib Kernel on . Policies are sequences of Markov kernels, and history-dependent policies take as input. The law is built with the Ionescu–Tulcea kernel Kernel.trajMeasure, one coordinate per time step. Time is -based.
Standing hypotheses on every statement:
For §4.2 the pair defining is an explicit argument. In §4.1, "policy" means Markov policy, as the paper states on p. 11. The conditional expectations "given " are expectations for the chain started at time in . Lemma 1 is stated with , the quantity its proof uses; the page prints .
The goal asks for a Markov equilibrium policy that is optimal against all history-dependent policies, at least as strong as Definition 3. Optimality is " the cost of every policy", not an infimum, so it has no junk case. The cost is a genuine integral: with bounded, the integrand lies in , so no policy is trivially optimal. The moment-function predicate has no infimum, so compact is admitted.
Contributions are welcome at every level:
A chance-constrained program asks for a decision that satisfies uncertain constraints with high probability rather than surely:
Such models appear in power-system operation, portfolio selection, chemical-process and reservoir management, and other settings where requiring the constraints for every realization is too conservative (Nemirovski–Shapiro 2006; the paper's introduction lists applications). The probability is rarely available in closed form, and when the distribution of is only accessible through samples, the feasible set of the empirical counterpart is a union of polyhedral-like pieces: it is non-smooth and non-convex, and the empirical quantile introduces many spurious local minima (Peña-Ordieres, Luedtke, Wächter 2020, §2).
Peña-Ordieres, Luedtke and Wächter replace the indicator inside the empirical probability by a smooth kernel with bandwidth , which turns the sample constraint into a differentiable one suitable for nonlinear programming solvers. This mission formalizes the paper's consistency result: as the sample size grows and the bandwidth shrinks, jointly, the optimal values and optimal solutions of the smoothed sample problem converge to those of the true problem with probability one.
Timeline. Consistency of sample approximations of chance constraints with the plain empirical cdf goes back to Pagnoncelli, Ahmed, Shapiro 2009 (reference [36] of the paper; its Propositions 2.1 and 2.2). Luedtke–Ahmed 2008 gave finite-sample feasibility guarantees for the same empirical approximation. Convergence with respect to a smoothing parameter alone was studied by Geletu, Hoffmann, Klöppel and Li (SIAM J. Optim. 27, 2017), Hong, Yang, Zhang 2011 and Hu, Hong and Zhang (IIE Trans. 45, 2013) (references [15], [25], [26] of the paper). Peña-Ordieres–Luedtke–Wächter 2020 (SIAM J. Optim. 30(3)) treat both parameters simultaneously; Theorem 3.5 of the preprint arXiv:1905.07377v2 is the result posed here.
Decisions are vectors restricted to a closed set . The random data takes values in a measurable space with law . The constraints are aggregated into one scalar function , and the risk level is .
The standing assumptions are: Assumption 3.1, for each the random variable has a continuous distribution; Assumption 3.2, is Carathéodory, i.e. is measurable for each and is continuous for almost every ; Assumption 3.3, some optimal solution of (1.1) is a limit of points with .
If is compact, is continuous and Assumptions 3.1–3.3 hold, then with probability one, as and jointly,
Theorem 3.5 justifies solving the smooth problem (2.4) in place of (1.1): with enough samples and a small enough bandwidth, global solutions of the surrogate approximate global solutions of the chance-constrained program, and the optimal values agree in the limit. Unlike earlier results it controls the two approximation errors, sampling and smoothing, at once, so no order of limits has to be chosen in practice. It is the asymptotic counterpart of the paper's finite-sample feasibility bound (Theorem 3.13) and the theoretical basis for the trust-region method of §5.
The result is proved in the paper, with two steps imported from Shapiro–Dentcheva–Ruszczyński, second edition (a uniform law of large numbers, Theorem 7.53, and a convergence-of-expectations result, Theorem 4.91) and the deviation statement deferred to Theorem 5.3 there. None of these results, and no consistency theorem for sample approximations of chance constraints, is machine-checked on Prove2Me or, as far as is known, elsewhere. A formal proof requires writing the imported steps out for the specific integrands of this problem and completing the solution-set argument the paper leaves to the reference.
The pointwise statements are routine; the uniformity is not. The integrand converges, as , to the indicator , which is discontinuous in wherever . A uniform law of large numbers for a family that degenerates into indicators needs the no-atom Assumption 3.1 at every point of , not only at the limit. Moreover, the smoothing functions for different are unrelated, so the family is not continuous in , and a Glivenko–Cantelli argument over a joint parameter cannot be applied directly. The convergence of solution sets needs, in addition, that the limit of feasible points of (2.4) is feasible for (1.1), which uses the continuity of on ; that continuity again rests on Assumptions 3.1 and 3.2.
Fin n → ℝ with the sup norm. Assumption 3.3 is stated for every radius, so the norm choice does not change it.ξ : ℕ → Ω → Ξ of measurable, independent maps on a probability space, each with law ; uses the first draws.atTop ×ˢ 𝓝[>] 0 on , with because needs it; one null set serves every conclusion of a statement.The definitions layer (Γ_ε, admissibility, , , , , the shifted sample sets (3.2)) is shared with the companion mission on finite-sample feasibility. A uniform law of large numbers for almost-surely continuous, bounded integrands on a compact parameter set, and convergence of optimal values under uniform convergence of constraint functions, are reusable beyond this mission; contributions of either as standalone lemmas are welcome.
Mean field games describe large populations of agents who interact symmetrically: every agent sees the same average of all the others. Many populations interact instead along a network, where each agent responds only to its neighbours. Lacker and Soret (arXiv:2005.14102v2, 2021; Math. Oper. Res. 2022) study a linear-quadratic stochastic differential game on a finite graph that is simple enough to solve explicitly on every vertex-transitive graph, and then ask what happens to the equilibrium as the graph grows. The question is the network analogue of the classical convergence problem for mean field games: does the -player equilibrium have a limit, and does that limit depend on the graph only through a small amount of information?
The answer of the paper is that the limit is governed by the empirical eigenvalue distribution of the graph Laplacian. Dense graph sequences (degrees tending to infinity) all have the same limit, the mean field game; sparse ones (bounded degrees) have limits that depend on the graph, through its spectrum. This mission formalizes that large-graph limit theorem, Theorem 2.6 of the paper. Mission I of the series formalizes the explicit equilibrium on a fixed transitive graph (Theorem 2.5), on which this mission builds.
Let be a finite simple graph on vertex set with adjacency matrix and degree matrix . Its Laplacian is . is transitive if every vertex can be mapped to every other one by a graph automorphism; such a graph is regular, of degree , and is then symmetric with eigenvalues . The empirical eigenvalue distribution is .
Fix a horizon , a volatility and a weight . Player controls the state
driven by independent Brownian motions, with Markovian feedback controls , and pays
On a transitive graph without isolated vertices, Theorem 2.5 gives an explicit Nash equilibrium: with and the solution of , on , the feedback is with . The resulting equilibrium state process is Gaussian, and the value is .
For a probability measure define , so that .
Let be finite transitive graphs without isolated vertices, , with , and suppose weakly for a probability measure . Then (1) the ODE , has a unique solution on ; (2) for every vertex sequence and ,
(3) the empirical measure converges weakly in probability to ; (4)
The milestones are the statements the paper's proof (§3, §6, §7.1) relies on: the stability of in (Proposition 3.2, last sentence); the finite-graph variance formula (2.7); monotonicity and concavity of (Proposition 3.3, first sentence); correlation decay (Proposition 2.12) for distinct vertices; the relation between degrees and the spectral limit (Lemma 7.1); the Gaussian Poincaré bound (7.3) and the concentration (7.1) of the empirical measure; and the spectral form (2.9) of the value.
Theorem 2.6 reduces the large-population behaviour of a network game to one spectral object. For complete graphs and the limit is the mean field game; for sparse sequences such as cycles, tori, or random regular graphs, is a non-degenerate measure and the limiting variance and value differ from the mean field ones. The theorem thereby gives a quantitative criterion for when a mean field approximation of a network game is accurate, and it shows propagation of chaos in both regimes: in the dense case because interactions are weak, in the sparse case because typical players are far apart in the graph.
The result is proved in the paper; none of it has been machine-checked. A complete formalization requires a Lean account of Gaussian laws of linear SDEs with additive noise, of weak convergence of spectral measures of graph Laplacians, and of a Gaussian Poincaré inequality, none of which is currently in Mathlib in the needed form. Each of these is reusable well beyond this mission.
Parts (2) and (4) follow from the finite-graph formulas once uniformly, but that convergence requires stability of a nonlinear ODE whose vector field is defined through the spectral measure, uniformly over a class of measures. The harder step is (3). Convergence of one player's law does not imply convergence of the empirical measure: the players are correlated, and on sparse graphs every player has a bounded number of strong neighbours, so the correlations do not vanish uniformly. Bounding them requires an estimate that decays in the graph distance and in the degree, and combining it with the growth of graph balls, which is controlled differently in the dense and in the sparse regime. The usual mean field route is closed: unless the graph is complete, the state vector is not exchangeable, so propagation-of-chaos arguments based on exchangeability do not apply.
The Lean development lives in namespace GraphLQGame.Asymptotics.
Fin n; a graph sequence is G : ∀ k, SimpleGraph (Fin (N k)) with .lapMatrix. is built from the real roots of the characteristic polynomial of , with multiplicity.gaussianReal 0 V.toNNReal; .The goal quantifies over every solution , and every equilibrium state process, and also asserts that the graph ODE solutions and the state processes exist, so it cannot be discharged vacuously. Proposition 2.12 is stated for distinct vertices: as printed, (2.17) is also claimed for , where it fails on complete graphs of large degree; the off-diagonal case is the one the proof of Theorem 2.6 uses. Theorem 2.5 (mission I) is not restated here; a solver proves what is needed of it.
Contributions are welcome at every level: Gaussian laws of linear SDEs, spectral measures of graph matrices, ODE stability, a Gaussian Poincaré inequality, and the milestones themselves.
Mean field games (MFGs) describe the limit of symmetric stochastic differential games as the number of players tends to infinity, when every player interacts with the empirical distribution of all the others. Their main practical use is the converse direction: an equilibrium of the limiting game supplies a simple, decentralized control that is an approximate Nash equilibrium of the game with finitely many players. For the complete graph, where everybody interacts with everybody, this is classical, with the standard rate (Carmona and Delarue, Probabilistic Theory of Mean Field Games, Vol. II, §6.1; Huang, Malhamé and Caines 2006, Theorem 12), as recalled on p. 10 of the paper.
Many interacting systems are not complete graphs: players see only their neighbours in a network. The question is then how dense the network must be for the mean field approximation to remain valid. Lacker and Soret (arXiv:2005.14102v2) answer it exactly for a linear-quadratic "flocking" game, where explicit computations are possible. This mission formalizes their Theorem 2.11, which applies to every finite graph, with no transitivity or regularity assumed.
Let be a finite simple graph on the vertex set ; means and are adjacent and is the number of neighbours of . Fix a horizon , a volatility and a cost weight . Each player controls a real state through
where are independent standard Brownian motions and . A Markovian control is a Borel function of time and the full state , of linear growth. The cost of player under a profile is
and for an isolated vertex: each player wants to end near the average of its neighbours at minimal quadratic effort. For a vector , a profile is a Markovian -Nash equilibrium if no player can lower its cost by more than by switching unilaterally to another control , written .
The mean-field control is
each player looks only at its own state, as if its neighbours' average were frozen at its mean.
Define if and if , and with the minimal degree ,
Then, with zero initial states, the state equation for has a solution, and
The result. Theorem 2.11 gives an explicit threshold for the mean field approximation on networks: along any sequence of graphs whose minimal degree diverges, the decentralized control is an -Nash equilibrium with , and the vector form says more: if the average of over vertices tends to zero, the per-player errors vanish on average (the paper's (2.16)). The rate quantifies how the accuracy of the approximation depends on denseness. In the same paper, transitive graphs whose degrees stay bounded lead to equilibria that do not agree with the mean field one, so a denseness condition cannot be dropped.
Formalizing it. The theorem is proved in the paper; to our knowledge no part of it is machine-checked. A formal development needs, beyond the statement, a verification argument for a one-dimensional linear-quadratic control problem with additive noise, Gaussian computations for linear SDEs driven by Brownian motion, and the comparison of costs between the equilibrium system and a system with one deviating player. The one-player result (Lemma 7.2) and the Gaussian facts of (7.7) are reusable well beyond this mission.
The obvious argument compares a deviating player with an isolated player and treats the neighbour average as noise independent of the deviation. Two things stand in the way. The cost of player couples its terminal state with the neighbours' average through a cross term , and the deviation may look at the neighbours' states, so the cross term does not vanish; it has to be bounded through the size of the deviation's energy. And an arbitrary deviation has no a priori energy bound: one is available only for deviations that do at least as well as the zero control, which is why the argument passes through a (near-)optimal deviation. Lemma 7.2 itself requires a verification theorem over all progressively measurable controls, not only feedback ones.
The Lean development lives in the namespace GraphLQGame.DenseApprox and uses the shared encoding of this series:
Fin n (the paper's become ), the state space is EthierKurtz.SDEState n, and is any SimpleGraph (Fin n); isolated vertices are allowed;A formalization in which is compared only with deviations depending on the player's own state, or in which the costs are Bochner integrals that vanish when not integrable, would be trivially or wrongly satisfied; both are ruled out by the encoding above.
Welcome contributions: the verification argument for Lemma 7.2, the Gaussian law of linear SDEs with additive noise, and proofs of the three steps. Related missions in this series: I (an explicit Nash equilibrium on transitive graphs) and II (large-graph limits).
The circumference of a graph is the length of a longest cycle. Extremal graph theory asks how many edges force a long cycle. The Erdős–Gallai theorem (1959) states that every -vertex graph has at most edges. Bondy (1971) strengthened it by counting only the edges near a longest cycle: if is a longest cycle of length , the number of edges with at most one endpoint in is at most , and at most when is 2-connected. Since spans at most edges, this implies the Erdős–Gallai bound.
A stability result complements an extremal one: a graph close to the extremal bound must be close in structure to the extremal graphs. Jie Ma and Bo Ning (Combinatorica, 2020; arXiv:1708.00704) proved stability versions of Kopylov's edge theorem for 2-connected graphs of given circumference and of Bondy's theorem above. This mission formalizes their stability version of Bondy's theorem, Theorem 1.12. In the paper it is also one of the two halves of the proof of the main stability theorem; the other half is a separate mission in this series.
Timeline (as recorded in §1 of the paper). Dirac (1952): every 2-connected graph has . Erdős and Gallai (1959): . Bondy (1971): the bound on edges with at most one endpoint on a longest cycle, and the degree theorem stated here as Theorem 2.1. Woodall (1976): for 2-connected with circumference . Kopylov (1977): for 2-connected with circumference ; another proof by Fan, Lv and Wang (2004). Fan (1990): an improved version of Bondy's bound for 2-connected graphs, and average-degree bounds on long paths. Füredi, Kostochka and Verstraëte (2016): stability for Kopylov's theorem when ; Füredi, Kostochka, Luo and Verstraëte (2018): the complete stability version, with the families , . Ma and Ning (2017 preprint, 2020): the results of this mission.
All graphs are finite and simple, on the vertex set . A path or cycle of length has edges. A graph is 2-connected if it has at least three vertices, is connected, and remains connected after deleting any one vertex. A cycle is a longest cycle if no cycle of has more edges; is its vertex set and its length.
For a longest cycle , write for the number of edges with at most one endpoint in . A vertex is an isolated vertex of if and every neighbour of lies on ; is its number of neighbours on .
The extremal graphs are:
means that is isomorphic to a subgraph of .
Let be 2-connected on vertices and a longest cycle of length with . If
then , or is odd and is a subgraph of a member of .
In every one of the vertices off a longest cycle sends edges to the cycle, so Bondy's bound is attained. Theorem 1.12 says that exceeding already leaves only three structures: a subgraph of , or for odd a subgraph of a member of or . In the paper it is one of the two cases of the proof of the main stability theorem (Theorem 1.9): a graph with many edges and a longest cycle has either many edges with at most one endpoint on , handled here, or many edges inside , handled by the closure argument of the companion mission.
The result is proved in the paper; none of it, nor Bondy's or Fan's theorems, is formalized on the platform or in Mathlib. The mission produces machine-checked statements of the goal, of the cited tools (Bondy's Theorem 2.1, Fan's Theorem 2.2, Lemma 2.3), and of the steps Theorems 3.1, 3.2 and Lemma 3.3, together with reusable definitions of 2-connectivity, longest cycles and the extremal families.
The obvious approach counts edges at the vertices off : each such vertex has at most neighbours on , since otherwise two consecutive cycle vertices would let the cycle be extended. This bound is far from enough. The edge count also includes edges between vertices off , and components of can be large, 2-connected, and attached to in complicated ways. The bound has to be beaten by every such configuration at once, and Theorem 3.2 states exceptional small cycle lengths for which the analysis does not close. A second difficulty is the passage from one vertex of degree to a global description of : in the odd case, the structure of every component of has to be determined, which is where the families and appear.
Graphs are SimpleGraph (Fin n) with decidable adjacency. A cycle is a closed walk C : G.Walk u u with C.IsCycle; its length is C.length and its vertex set C.support.toFinset. "Longest cycle" is the predicate that every cycle of is at most as long as ; no supremum of cycle lengths is used. 2-connectivity is: at least three vertices, connected, and connected after deleting any one vertex. It is stated for an arbitrary finite vertex type so that it applies to the induced subgraph in Lemma 2.3. The edge count off is the number of edges with an endpoint outside , and is natural-number division; under the stated bounds every natural-number subtraction is exact.
is defined on fixed labels (clique , hubs ), and "" is a graph embedding G ⊑ W. Membership in and are predicates on labelled graphs, closed under relabelling, and " is a subgraph of a member" is G ≤ H for some member . No hypothesis is added to any statement. Fan's Theorem 2.2 is stated without its equality characterization.
Trivializing formalizations are ruled out explicitly: the alternative " is odd and …" is a conjunction, never an implication; the circumference is never a junk supremum; containment in is up to isomorphism, never ≤ on fixed labels; and 2-connectivity excludes and disconnected graphs.
The definitions are reusable for any work on circumference, longest cycles and Bondy–Erdős–Gallai-type problems. Contributions of proofs of the cited tools (Bondy's and Fan's theorems) are especially welcome, as is a proof of Erdős–Gallai's edge theorem, which the proof of Theorem 3.2 uses and which is posed elsewhere on the platform.
Distributionally robust stochastic optimization (DRSO) chooses a decision to minimize the worst expected loss over an ambiguity set of probability distributions, instead of the expectation under one estimated distribution. When is a ball around a nominal distribution (often the empirical distribution of data) in the Wasserstein distance, the set contains distributions with supports different from that of , and the worst case is driven by how far mass can be moved and how fast the loss grows along the way. This makes Wasserstein balls a standard choice in data-driven optimization, statistical learning and operations research.
The inner problem, a supremum over an infinite-dimensional set of measures, is not directly computable. Gao and Kleywegt (arXiv:1604.02199v3) show that it equals a minimization over a single scalar multiplier, for an arbitrary Polish space and nominal distribution and a merely measurable loss.
Timeline. Esfahani and Kuhn (2018, doi:10.1007/s10107-017-1172-1) proved a strong duality for and empirical on , giving finite convex reformulations for piecewise-affine losses. Blanchet and Murthy (2019, doi:10.1287/moor.2018.0936) proved duality for general optimal transport costs on Polish spaces under upper semicontinuity of the loss, with a dual over pairs . Gao and Kleywegt's result, first posted in 2016 and published in Mathematics of Operations Research (2023, doi:10.1287/moor.2022.1275), covers every order , every nominal and every measurable loss with finite growth rate, with a dual in one variable.
Let be a Polish space (complete, separable metric) with its Borel -algebra, the Borel probability measures, and . The decision variable is suppressed: is a Borel measurable loss with for a fixed nominal distribution .
The Wasserstein distance of order is given by
The primal value is the worst-case expectation over the Wasserstein ball,
The regularization operator is , the dual objective is , and the dual value is . The growth rate of is
with if no qualifies. The lemmas also use the near-optimal distances and , the limits as of the largest and smallest over -minimizers of .
In Lean these objects are DRSOWass.Duality.wassPow, vP, Phi, dualObj, vD, growthRate, DUpper, DLower.
If , then
This is the printed theorem: an equality of values together with finiteness. It fixes no constant and needs no regularity of beyond measurability and integrability.
The result. Strong duality turns the worst-case expectation over a Wasserstein ball into a convex problem in one scalar, , where is a Moreau–Yosida-type regularization of . For finite-supported this yields finite-dimensional reformulations of DRSO; the paper derives from it the structure of worst-case distributions (Corollaries 1 and 2) and applications to two-stage problems, point processes and Gaussian nominal distributions. The growth rate separates the finite case (this theorem) from the case (Proposition 2).
Formalizing it. The theorem is proved in the paper; to the best of current knowledge none of it is machine-checked. The mission produces a formal statement of the duality on general Polish spaces, together with reusable pieces: extended-valued integrals, the regularization operator and its one-sided derivatives, measurable selection on Polish spaces, and push-forward constructions of near-optimal measures. Formal proofs of Lemma 3 also give measurable-selection tools that Mathlib does not yet provide in this form.
Weak duality is a one-line Lagrangian argument. The difficulty is attainment from the primal side: one must construct, for every , a distribution in the ball whose expectation is within of . A worst-case distribution need not exist (when mass escapes to infinity), so a compactness argument on fails; and is only measurable, so the infimum defining cannot be reduced to a countable one, and the measurability of and of near-optimal transport maps needs projection and measurable-selection theorems for analytic sets. The case analysis on whether the dual minimizer exceeds is forced by the possible non-differentiability of at .
MetricSpace, CompleteSpace, SecondCountableTopology and BorelSpace instances; is a probability measure; is dist ξ ζ ^ p with real .RWPI.SqrtLasso.transportCost with cost , an infimum over probability couplings in ; is written .ModelRiskOT.Duality.extIntegral, in (with ). , , , are EReal-valued; , , are ENNReal-valued, so is representable and the empty infimum is .A complete development needs couplings and gluing in Mathlib's measure theory, the measurable projection theorem and a measurable selection theorem on Polish spaces, and one-sided derivatives of concave extended-valued functions; the first three are reusable well beyond this mission. Proofs of any milestone, alternative proofs of the goal (e.g. through the Blanchet–Murthy dual), and the companion result Proposition 2 () are welcome.
Most business-to-business sales are not paid in cash on delivery. The supplier lets the buyer pay later, which is trade credit, and often offers a discount for paying early. In the classic "2/10 net 30" the buyer gets 2% off for paying within 10 days and otherwise owes the full price in 30 days. Trade credit is a major source of short-term finance for firms. Empirical work documents both forms of contract: net terms, with one price and no discount, and two-part terms, with an early-payment discount. The discounts are large, and they vary a lot from one buyer to another (Petersen and Rajan 1997; Klapper, Laeven and Rajan 2012). The implied interest rate on a forgone discount is often far above a bank loan's. This raises two questions: why do cash-poor buyers use trade credit at all, and when should a supplier offer a discount?
Yang and Birge (Management Science 2018) answer this in a supplier–retailer model with a financially constrained retailer, who can finance inventory with a bank loan, with trade credit, or with both. Their answer is risk sharing. Trade credit is repaid out of realized sales, so the supplier bears part of the demand risk. She can therefore induce a larger order than a price-only contract does. The model builds on the selling-to-the-newsvendor model of Lariviere and Porteus (2001), and it complements the supplier-versus-bank analysis of Kouvelis and Zhao (2012). This mission formalizes the paper's main result on the structure of the optimal contract.
A retailer buys a single good from a supplier at unit cost and sells it at unit price . Demand is random with density on . Its distribution function is , the complementary distribution function is , the failure rate is , and the generalized failure rate is . Demand has an increasing failure rate (IFR). The retailer has cash .
The supplier offers a cash price and a credit price , with . The early-payment discount is . If the retailer's cash does not cover his cash purchases, he borrows from a competitive bank. The bank loan is senior to trade credit. A bank and a supplier recovering a defaulted claim lose fractions and of what they recover, with .
Default is described by two thresholds. The bank-loan default threshold is the demand below which the bank is not repaid in full, and it equals the amount owed to the bank. The trade-credit default threshold is the demand below which the supplier is not repaid in full. The retailer uses a bank loan iff , and uses trade credit iff .
The paper shows (p. 13) that the supplier's problem can be written in the thresholds alone. Let
The retailer orders , the prices are and , and the discount is . The supplier's expected profit is
She maximizes over a domain of thresholds. A maximizer is an optimal trade credit contract. Net terms correspond to , which is . Two-part terms correspond to .
For every optimal contract :
If , or if is sufficiently large, then and (net terms, no bank loan). If and is sufficiently small, then
"Sufficiently large" and "sufficiently small" are existential thresholds on that depend on the data , not on the contract.
They are listed in the order the proof uses them:
Proposition 3 is the paper's prediction about inventory financing portfolios. Once the supplier sets the terms, a retailer who needs external financing always uses trade credit. Early-payment discounts appear only when supplier default is costly and the retailer is cash-poor. A discount is then the supplier's way of moving part of the financing to the bank. The paper uses this to explain why discounts go to small, risky buyers, as observed by Klapper et al. (2012). The comparative statics of §5 (Propositions 4–6) are built on the same reduced problem.
The result is proved on paper but has not been formalized. The appendix lemmas it rests on (C.4, C.7, C.8, C.9) are stated without proof ("available upon request"). A machine-checked development would therefore settle whether these lemmas hold on the domain where the paper uses them. It would also produce a reusable library: IFR demand with failure rates, the bank-loan pricing kernel , and the implicit order quantity .
The order quantity is defined implicitly, as the smaller root of a unimodal equation, and the paper's arguments differentiate through it with the implicit function theorem. Every derivative of therefore involves , which blows up at the edge of where . The density is only assumed continuous, so and need not be differentiable when . Monotonicity and concavity have to be argued from the integral forms, or under a smoothness assumption the paper does not state.
The obvious argument for "sufficiently large " also fails. It perturbs the optimum at just below , but there the domain shrinks to a sliver near , and the derivative of in at can be negative. For exponential demand it tends to as . The proof's claim that there is not part of the theorem. Part 1 for general is reduced to through Proposition 6, which requires comparing optima over domains that themselves depend on .
All objects live in TradeCredit.Terms.Model.
Demand. Demand is a density that is continuous on , positive on , zero on , integrable with total mass , and has a weakly increasing failure rate on . is the interval integral of from . The normalizations are and . The parameters satisfy , and .
Domain. is the printed set of Corollary 3 ( and ) plus two pinned constraints: (that is, ) and . These are the image under (11) of §3.1's , which the printed omits.
Statements. is the infimum of the nonnegative roots. "The optimal contract" means every maximizer of on . Existence of a maximizer is not asserted; the paper does not prove it. Monotonicity is weak, and concavity is Mathlib's ConcaveOn on the sections of . Proposition 6 is stated by comparing attained values with .
Not in scope. The retailer's best response (Proposition 1) and the bijection between thresholds and contracts are not formalized. The goal is about the paper's own reduced problem. Lemma 1's first-order conditions are not a milestone: as printed they fail at a corner optimum , and they need , which is not defined under a merely continuous density.
Ruling out trivialization. The large- clause quantifies over with . For the domain has no point with and every "for every optimal contract" statement holds vacuously, so a large- clause that reached only those values would be empty.
Welcome contributions. Lemmas on IFR densities (positivity of , finiteness of the mean, monotonicity of and existence of ), the root structure of , and boundedness of on are reusable beyond this paper.
Source. The source PDF is the authors' accepted manuscript (LBS Research Online, eprint 801). All page numbers are the manuscript's.
DC programming is the minimization of a function that is a difference of two convex functions. The class contains every function on a compact convex set and most nonconvex models of sparse learning, clustering, combinatorial relaxations and robust optimization, and its standard method, the DC Algorithm (DCA), replaces by its affine minorant at the current iterate and solves a convex program at each step. DCA was introduced by Pham Dinh Tao in 1985 and developed jointly with Le Thi Hoai An from 1994 on (Pham Dinh & Le Thi 1998); the survey of Le Thi & Pham Dinh 2018 collects thirty years of that work.
DCA is guaranteed to reach critical or strongly critical points, notions that depend on the chosen decomposition , while a decomposition-free notion, directional (d-)stationarity of itself, is what a user of a nonconvex model usually wants. Ahn, Pang & Xin 2017 warned that DC criticality can be much weaker than d-stationarity. Theorem 1 of the 2018 survey (p. 9) states when the two coincide. Its proof is omitted in the paper ("can be easily deduced … It is omitted here").
Let with the canonical inner product . Functions take values in . The effective domain of is , and is the set of proper, lower semicontinuous, convex functions .
The standard DC program is
with the convention , and is assumed finite. Finiteness of forces , so .
The subdifferential of at is
A point is strongly critical for if .
The directional derivative of at in direction is . For convex it equals . A point is d-stationary for if for every . The support function of is , with . Finally, is the relative interior of , its interior inside the affine hull .
For ,
Part (iii) is the goal because it is the equivalence the paper uses to justify DCA, stated under a hypothesis symmetric in and ; (vi) is the more general companion.
The theorem connects the output of DCA with a stationarity notion intrinsic to . Without it, the strong criticality certified by DCA would be a property of a decomposition rather than of the problem, and different decompositions of the same could certify different points. With it, at points in the relative interiors of the domains, every strongly critical point is d-stationary, and conversely no d-stationary point is missed by the criticality test.
Parts (i) and (ii) are stated in the paper without proof, and so is the rest of Theorem 1; none of it has a machine-checked proof. The mission produces a formal statement of all six parts with the extended-real conventions made explicit. Three of the printed parts are false as stated without the nonemptiness of ; the formal versions add that hypothesis and record a counterexample for each, so the formalization also corrects the printed statement.
The obvious argument writes and reads off both directions from . Two steps of it fail. First, the difference can be or , and the limit defining need not be the difference of the limits; the nonemptiness of is exactly what rules out the first case. Second, passing from "" to "" needs to equal the support function of , which holds in the relative interior of but fails on its relative boundary, where need not be lower semicontinuous. The relative interior, not the interior, is essential: the domains may be lower-dimensional.
is EuclideanSpace ℝ (Fin n), and every function maps into EReal. The published definitions TaoAnDCA.GlobalOpt.Setting supply (effDom), the DC objective with (dcSub), the subdifferential (subdiff) and (primalValue); is the published IsProperClosedConvex. Every statement carries the standing assumptions of Theorem 1 as binders: , and . The mission's definitions are:
convDirDeriv: the convex directional derivative by the paper's infimum formula, in EReal;HasDirDerivE: the predicate that the one-sided limit along exists in EReal and equals a given value;IsDStationary: and, for every direction, the limit exists and is ;IsStronglyCritical: both and ;supportFn: the extended-real support function, on .The relative interior is Mathlib's intrinsicInterior ℝ, the affine hull is affineSpan ℝ. The subgradient inequality has the standard sign; display (1) of the paper prints the opposite sign, a slip. The only hypothesis added to the page is , in parts (i), (ii) first sentence and (iv), each of which is false without it; parts (ii) second sentence, (iii), (v) and (vi) are stated as printed.
The statement admits trivializing formalizations, which this one rules out. Strong criticality without the nonemptiness of is vacuous wherever . A d-stationarity defined through limUnder, a real-valued derivative, or "every limit is nonnegative" holds vacuously where the limit does not exist. And written in raw EReal would give .
A complete development needs the monotonicity of convex difference quotients in EReal, limit arithmetic for extended reals, and the formula for at points of (Rockafellar 1970, Theorem 23.4), together with the nonemptiness of there. These results on extended-real convex functions are reusable well beyond DC programming, and contributions of them as separate theorems are welcome.