Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A martingale transport plan between two laws and on is a joint law of a pair with , and . Minimizing or maximizing over such plans gives the model-independent price bounds of an option with payoff when the market quotes vanilla options at two maturities, and so fixes the marginal laws and of the asset price. For the forward-starting straddle, with payoff , the two bounds are the problems with costs and .
and are Borel probability measures on with finite first moments, in convex order: for every convex (Definition 2.1). is the set of measures on with marginals and such that is -integrable and
which is the paper's characterization (4) of "the disintegration has barycentre ". For the cost the cost of a plan is , and is optimal if it minimizes this over . is continuous if for every .
is the largest measure below both and (Example 2.5); is the image of under , a measure on the diagonal . For , , and .
If and is continuous, there is a unique optimal for ; it is concentrated on a set with for every ; and
for some functions .
The theorem identifies the lower model-independent bound for the forward-starting straddle: the extremal model keeps the mass that and share in place and splits every other starting point between at most two destinations. With Theorem 7.3 for it settles both bounds for continuous without any dual attainment, which is known to fail in general. The decomposition into a static part and a part between marginals with is a reduction that applies to other costs vanishing on the diagonal.
The result is proved in the paper; nothing in it has been machine-checked. The mission produces a formal statement of Theorem 7.4 and of each step of its proof, a Lean vocabulary for martingale transport on shared with the other missions of this series, and the general measure-theoretic lemmas (3.2, 5.5, 5.6) that the structure theorems of the paper all use.
Lemma 7.5 and (24) are elementary; the work lies in passing from them to statements about measures. The variational lemma needs Kellerer's duality-type result for finitely optimal sets. The static part requires showing that a positive defect produces, at -almost every point, a forbidden configuration, which uses the disintegration of the moving part. The cardinality bound requires the accumulation argument of Lemma 3.2, and the forbidden configurations only hold for points that lie strictly inside the range of their own fibre, which the martingale condition supplies only almost everywhere. Uniqueness does not follow from strict convexity of a cost functional, since the problem is linear: it comes from the two-graph structure through Lemma 5.6, and it fails if has atoms (Remark 7.7).
Measures are Mathlib Measure ℝ and Measure (ℝ × ℝ) with Borel σ-algebras. Costs are integrals in the extended reals through the published ModelRiskOT.Duality.extIntegral; the cost is nonnegative and, under finite first moments, finite. Martingale plans are encoded by condition (4), competitors by the same device. is the infimum in Mathlib's complete lattice of measures, measure subtraction is Mathlib's truncated subtraction, cardinalities of fibres are Set.encard in , and "concentrated on " is . Continuity of is for all . As on the page, , and in the goal carry no measurability requirement.
Two choices differ from a literal reading and are disclosed in the items: (24) carries the hypothesis of Lemma 7.5, which the page invokes and without which (24) is false; and the steps that do not need continuity of (the static part, the reduced problem) are stated without it.
A trivializing formalization is ruled out: is the lattice infimum of measures, not a product and not a pointwise minimum of set values, and all four conjuncts of the goal (existence, uniqueness, the bound 3, the decomposition) are asserted together.
Reusable beyond this mission: the Setting layer (convex order, , competitors), Lemma 3.2, Lemma 5.5 (a Lusin–Novikov consequence) and Lemma 5.6. Proofs of any milestone, and infrastructure on disintegrations of plans on , are welcome.
Martingale optimal transport asks for the cheapest way to couple two given laws and on by a one-step martingale: a pair with , and . The problem arises in mathematical finance, where and are the risk-neutral laws of an asset at two maturities, implied by quoted vanilla option prices, and the extremal values of over all such couplings are model-independent price bounds for the exotic payoff (Beiglböck, Henry-Labordère, Penkner 2013; Galichon, Henry-Labordère, Touzi 2014). In classical optimal transport on the line, a single coupling, the monotone (quantile) coupling, is optimal for a whole family of costs. Beiglböck and Juillet (arXiv:1208.1509, Ann. Probab. 2016) identify its martingale counterpart, the left-curtain coupling , and determine costs for which it is optimal.
This mission formalizes one of those optimality results, Theorem 6.3: for product costs with strictly convex and decreasing, is the unique optimizer.
Let be the set of finite Borel measures on with finite first moment. For the convex order means for every convex ; it forces equal mass and equal mean. The extended convex order asks this only for nonnegative convex .
A transport plan from to is a measure on with marginals and ; the set of them is . It is a martingale transport plan, , if is -integrable and
that is, the conditional law of given has barycentre for -almost every . For a cost the cost of a plan is , the value is , and is optimal if it belongs to and attains this infimum.
For a plan and , the measure is where sends the left part of . Given , the shadow is the measure with and that is -below every other such measure. The left-curtain coupling of is the plan with
It sends every left part of to the most concentrated part of that can receive it by a martingale.
Let be finite measures, strictly convex, strictly decreasing, , and assume . Then
Theorem 6.3 gives a class of costs for which the martingale transport problem has an explicit, cost-independent solution, and does so with uniqueness and without any regularity of beyond monotonicity. In the financial reading, every payoff of the form with these shape properties has its model-independent lower price bound attained by one and the same model, the left-curtain martingale, which depends only on the marginals. The result complements Theorem 6.1 of the same paper (costs with strictly convex), proved by a different, variational route.
The theorem is proved in the paper. No machine-checked version is known: neither the left-curtain coupling nor shadows nor martingale optimal transport on appears in Mathlib or on the platform. A formalization produces the shadow construction, the left-curtain coupling as a Lean object with its characterization, and the comparison principle " has the -least targets", all of which are reused by the other results of the series (uniqueness of the left-monotone plan, Theorem 6.1, the support bounds of §7).
The obvious argument compares costs plan by plan, but the convex order of two measures alone does not order the integrals of a strictly convex strictly: that forces requires representing as a martingale image of (Strassen's theorem on ) and the equality case of Jensen's inequality, with care about infinite integrals. The second obstacle is the passage from "equal targets for almost every level of " to "equal plans": the superlevel sets of a strictly decreasing are half-lines that may be open or closed at the jumps of , so the targets must be controlled for both kinds of half-line, and a null set of levels must be bridged by monotonicity of . Existence of shadows (Lemma 4.6) is itself a nontrivial construction through potential functions .
Measures are Mathlib Measure ℝ and Measure (ℝ × ℝ) with the Borel σ-algebras. and are finite, not necessarily probability, measures, as the theorem states; membership in is part of ConvexLE. Integrals that may be infinite take values in EReal, through the published ModelRiskOT.Duality.extIntegral (). is encoded by the characterization above with bounded test functions . The shadow and the left-curtain coupling are predicates (IsShadow, IsLeftCurtain); their existence and uniqueness are milestones, never built into definitions. "Optimal" is minimality of cost over martingale plans; attainment is not assumed.
Two hypotheses are read into the printed statement. "Decreasing" is strict: with all martingale plans have the same cost , and for uniform on , uniform on there are infinitely many of them. is added, as the proof assumes a plan of finite cost; otherwise every plan is optimal. A formalization in which is merely some plan, the cost is a Bochner integral (which is for non-integrable integrands), or optimality is taken among all plans rather than martingale plans would not be Theorem 6.3. Theorem 4.18 is stated for finite measures of equal mass, the generality Theorem 6.3 needs. Strassen's theorem is already posed on the platform (PalmQueueing.Ordering.strassen_cx) and is not restated.
A complete development needs the convex order on finite measures, shadows, the left-curtain coupling, a layer-cake identity for product integrands and the equality case of the convex order for strictly convex test functions. The shadow and left-curtain layers are reusable across the whole series; contributions to any milestone, and to general lemmas on the convex order of finite (not only probability) measures, are welcome.
A forward-start straddle pays , the absolute change of an asset price between two future dates. A trader who knows the market prices of all vanilla options at both dates knows the laws of and of , but not their joint law. Under a pricing measure the price is a martingale, so the admissible joint laws are exactly the martingale couplings of and . The highest price consistent with the data is therefore the value of an optimization problem over martingale couplings: maximize . Hobson and Neuberger (Robust bounds for forward start options, 2012) studied this problem and identified the maximizing coupling through the dual problem. Beiglböck, Henry-Labordère and Penkner (arXiv:1106.5929) showed that the dual maximizers need not exist in general.
Beiglböck and Juillet (arXiv:1208.1509v2, Ann. Probab. 2016) approach martingale transport through the structure of the support of optimal plans. Their Theorem 7.3 recovers the Hobson–Neuberger optimizer for every continuous starting law : it is unique and splits each starting point into at most two destinations along two monotone maps.
Timeline.
A martingale transport plan between probability measures on with finite first moments is a probability measure on with first marginal , second marginal , and
that is, the conditional mean of given is . Their set is . It is nonempty exactly when and are in convex order, : for every convex .
For a cost the problem is
and is optimal if it attains this infimum. This mission concerns the Hobson–Neuberger cost , so optimal plans maximize . The measure is continuous: for every .
For write . A competitor of a finitely supported measure on is a measure with the same two marginals and the same conditional barycentres .
If are probability measures and is continuous, there is a unique optimal for . Moreover there are a Borel set with and functions , nondecreasing on , with
The result. Theorem 7.3 gives the extremal martingale coupling for the forward-start straddle in closed structural form: a plan that sends each to one point below and one point above it, both chosen monotonically in . Combined with the martingale constraint, this determines the transition probabilities at each , so the plan, and the model-independent upper price bound, are pinned down by and . Remark 7.6 of the paper shows that continuity of cannot be dropped: for atomic uniqueness can fail.
Formalizing it. The result is proved in the paper; to our knowledge none of it is machine-checked. The mission produces a formal account of a support-based method (variational lemma, forbidden configurations, fibre counting, selection of Borel graphs, uniqueness from convexity). Lemma 3.2, Lemma 5.5 and Lemma 5.6 are general statements reused by the paper's other structure theorems (Corollary 1.6, Theorems 7.1, 7.4) and are of independent use.
The forbidden configurations (23) are pointwise statements about a set of full measure, while the conclusion is about functions. Passing from one to the other needs three ingredients that do not follow from (23) alone: a counting argument showing that only countably many fibres can have three or more points (this is where continuity of enters, through Lemma 3.2), a measurable selection of the two branches (Lemma 5.5, a Lusin–Novikov type theorem not in Mathlib), and a uniqueness argument comparing two optimizers through their average. The naive idea of reading uniqueness off from (23) directly fails: (23) constrains each optimizer separately, and two optimizers could a priori live on different pairs of graphs.
Lemma 1.11 itself rests on a duality theorem of Kellerer type for product sets and is the subject of a separate mission of this series.
The Lean development works with measures on ℝ and ℝ × ℝ and their Borel σ-algebras. Integrals that may be infinite are taken in EReal through the published ModelRiskOT.Duality.extIntegral (positive minus negative part, with ); the cost of a plan, , and the convex order are defined through it. is encoded by the paper's own characterization (4) with bounded test functions, and competitors by the same device; no disintegrations appear in the statements. Cardinalities of fibres are Set.encard, valued in . Continuity of is the hypothesis for every . "Concentrated on " is .
The attainment milestone uses the finite-measure class introduced in §2.1: probability normalization is required for Lemma 1.11 and the goal, but not for attainment. The first moments of both marginals are explicit hypotheses in that milestone.
The goal states as nondecreasing on a Borel set of full -measure, with on . The page writes nondecreasing everywhere; read literally that version fails when has bounded support and does not, and the paper's proof produces exactly the full-measure form (as in its Corollary 1.6).
Statements (23), the fibre count and the monotonicity of are stated for an arbitrary set with the finite-optimality property of Lemma 1.11 for , so they do not depend on a plan. A formalization proving only existence of an optimizer, or uniqueness without the two-graph structure, does not settle the goal: both parts are required.
Needed infrastructure: weak compactness of and lower semicontinuity of the cost functional; a Kellerer-type duality for Lemma 1.11; a Lusin–Novikov selection theorem for Lemma 5.5. Contributions to any of these, and alternative proofs of Lemma 5.6, are welcome.
Martingale optimal transport asks for the cheapest way to couple two given laws and of a price at two dates under the constraint that the coupling is a martingale: the conditional mean of the later price given the earlier one equals the earlier one. It is the model-independent pricing problem of mathematical finance: given the marginal laws implied by vanilla option prices, the extreme values of over all martingale couplings bound the price of the exotic payoff (Beiglböck, Henry-Labordère, Penkner 2013; Galichon, Henry-Labordère, Touzi 2014). In the classical (non-martingale) transport problem, the shape of the cost determines the shape of the optimal coupling: for strictly convex costs of on the line the optimizer is a monotone map. The question this mission addresses is the martingale analogue: how much can an optimal martingale coupling split a single starting point, as a function of the cost?
Beiglböck and Juillet (arXiv:1208.1509, Ann. Probab. 2016) introduced the variational lemma for this problem and used it to prove, among other results, that the left-curtain coupling is optimal for a family of costs and that, for costs , the number of points into which an optimal plan sends a non-atom of is bounded by a geometric property of alone (their Theorem 7.1). This mission formalizes that bound.
All measures are Borel measures on or . A martingale transport plan between probability measures on is a measure on with marginals and such that for every bounded Borel ; equivalently, the disintegration of along its first coordinate satisfies for -almost every . The set of such plans is ; it is nonempty exactly when and are in convex order, , meaning for every convex .
A cost is a function . It satisfies the sufficient integrability condition if for some , ; then is well defined for every plan. A plan is optimal if for every .
A competitor of a finitely supported measure on is a measure with the same two marginals and the same conditional barycentres . For a set , is its fibre over .
This mission concerns costs of the form with twice continuously differentiable, and the hypothesis that affine functions meet in at most points: for all , . For instance satisfies it with .
Under the hypotheses above, with an optimal martingale plan of finite cost, there is a disintegration of such that for every
and if has no atoms, holds -almost surely for every disintegration of .
The result itself. Theorem 7.1 converts a one-dimensional condition on into a sparsity statement for every optimal martingale coupling: non-atoms of are sent to at most points. For this gives at most three points, and Section 7.3 of the paper gives an example with continuous where the optimizer splits into more than two points, so for this cost the bound cannot be lowered to two. For costs where is strictly convex (so ), it gives the two-point structure also enjoyed by the left-curtain coupling, which is optimal for those costs (Theorem 1.9). Such support bounds are what make the optimizers computable and the corresponding robust price bounds explicit.
Formalizing it. The theorem is proved in the paper; to our knowledge none of it is formalized. A formal proof requires machine-checked versions of the variational lemma (itself resting on a duality theorem of Kellerer type), the countability argument of Lemma 3.2, and the real-analysis estimate behind the three-point rerouting. Each of these is reusable: Lemma 1.11 drives every structural result of the paper, and Lemma 3.2 is used again for the left-monotonicity theorems.
The natural first attempt is to argue pointwise: if a fibre has points, reroute mass within that fibre to lower the cost. This fails, because a competitor must preserve the barycentre of each fibre, and within a single fibre no rerouting both preserves the barycentre and the marginals. Any improvement must move mass between two different starting points and , and this requires the two fibres to be close to each other and arranged consistently, which a single fibre cannot guarantee. Producing such pairs of fibres needs uncountably many exceptional points (Lemma 3.2) and the set of the variational lemma, whose existence is the deep part (it rests on a duality theorem for measures with given marginals). A second difficulty is that the conclusion is required at every non-atom , not only almost everywhere, so the exceptional set must be controlled exactly.
Lean represents measures with Mathlib's Measure ℝ and Measure (ℝ × ℝ). is encoded through the test-function characterization for bounded Borel ; costs are extended-real integrals (the published ModelRiskOT.Duality.extIntegral); competitors of a finitely supported are encoded through the same test-function device. A disintegration is a Markov kernel with , and is written as " is concentrated on a set of at most points", which is equivalent for probability measures on . Cardinalities take values in ; is deriv h.
Standing and added hypotheses of the goal: are probability measures in convex order; "optimal transport plan" means optimal martingale plan, as throughout Section 7; and, because the proof starts from Lemma 1.11, the hypotheses of that lemma are added: the sufficient integrability condition for and finite cost of . "Continuous " is for every .
The conclusion is not trivialized: the first part holds for every with a single chosen kernel, not almost everywhere, and the second part quantifies over all kernels, not one. The hypotheses are jointly satisfiable (for example , , ).
A complete development needs disintegration of measures on (available in Mathlib as condKernel), the variational lemma with its duality ingredient, and elementary real analysis. Contributions to the variational lemma are reusable across the whole series of missions on this paper.
Mean field games (MFGs) describe Nash equilibria of stochastic differential games with a very large number of symmetric players, each of whom interacts with the others only through the empirical distribution of their states (and, in this paper, of their controls). They were introduced independently by Lasry and Lions and by Huang, Malhamé and Caines around 2006, and are used for models of systemic risk, price impact in optimal execution, flocking and crowd motion, and large-population economics. The basic mathematical question is existence of an equilibrium: a flow of measures that is reproduced by the optimal behaviour of a representative player who takes that flow as given.
Two families of methods dominate the literature. The analytic approach of Lasry and Lions solves a coupled Hamilton–Jacobi–Bellman / Fokker–Planck system. The probabilistic approach of Carmona and Delarue (arXiv:1210.5780) solves a forward–backward SDE of McKean–Vlasov type in the strong formulation, on a fixed probability space with the controlled state as a strong solution. Both require the coefficients to be regular (Lipschitz or continuous) in the state variable. Carmona and Lacker (arXiv:1307.1152, Ann. Appl. Probab. 2015) introduce a weak formulation, in which controls act through a Girsanov change of measure on a fixed driftless state process. This lets the drift, running reward and terminal reward be merely measurable and path-dependent in the state. The interaction can enter through the law of the state path and through the law of the control. This mission formalizes their existence theorem.
Fix a dimension , a horizon and the path space with the sup norm. A measurable fixes the admissible population laws, . The topology is the weakest one making continuous for every measurable with . A compact convex control set sits in a normed space, and carries the weak topology.
A probability space carries an initial state and an independent Brownian motion , with filtration generated by . Admissible controls are the progressively measurable -valued processes. The driftless state solves , , and its law is . For a population law and a control , the measure has density with respect to . Under , is a weak solution of . Given also a measurable flow of control laws, the reward is
The standing assumptions (S) ask for:
The Hamiltonian is . Its maximum over is , and the set of maximizers is .
Assume (S), (E) (for each , the maps , , are sequentially continuous in the measure and control arguments, on the laws with ) and (C) (each is convex). Then there exist , a measurable and with
This is Definition 3.4 of a solution of the MFG. No constants or rates appear; the goal asserts existence only.
The milestones are the statements the paper's proof (§7) names, in attack order:
The theorem yields equilibria for interactions that are discontinuous in the state and nonlocal in time. Examples are rank-based rewards, path-dependent payoffs, and dependence on the law of the controls ("extended" MFGs, needed for price impact models). Strong-formulation methods do not cover these. It is also the input to the companion results: uniqueness under Lasry–Lions monotonicity (Theorem 3.8) and the construction of approximate Nash equilibria for the -player game (Theorem 4.2), formalized as missions 2 and 3 of this series.
The result is proved in the paper. What this mission adds is a machine-checked development of the weak formulation:
None of these is in Mathlib, and no mean field game existence theorem in the weak formulation has been formalized. Formalization also checks the proof. The fixed point theorem as printed (Proposition 7.4, with closed rather than compact values) is false, and the milestone states the corrected version. Connecting it to Lemma 7.11, whose values are closed but not compact in the norm , is part of the work.
The fixed point is set-valued. Without uniqueness of maximizers, the best response to is a set of controls. Kakutani's theorem in finite dimensions does not apply: the laws live in , which with is neither metrizable nor separable.
The obvious argument would apply Schauder's theorem to for a measurable selection of the maximizers. It fails twice. A selection need not depend continuously on . And the adjoint process , which enters the maximizer, depends on only through a BSDE, with no pointwise regularity.
Compactness has to come from somewhere other than the coefficients. All laws of the form lie in a set of laws with bounded densities relative to . Turning that into compactness for needs the -moment of to upgrade -convergence to -convergence. Continuity in the control law goes through the stable topology on measures over .
The Lean development (namespace WeakMFG.Existence) builds on the published Brownian/Itô/BSDE layer Peng1990.SMP.Stochastic. It commits to these conventions:
Fin d → ℝ, time is ℝ≥0, and paths are continuous maps on .Some formalizations would be trivial and are ruled out. Every clause of Definition 3.4 is stated. No density version may be missing. Optimality is over the whole admissible class, not a subclass. Replacing the goal by a fixed-point statement about the map is not acceptable, since that is a step of the proof.
Milestone conventions:
Infrastructure that is reusable beyond this mission:
Contributions to any of these, and alternative proofs that avoid the non-compact-valued fixed point step, are welcome.
Many problems in statistics, signal processing and machine learning minimize a smooth loss plus a nonsmooth regularizer over a set that is a manifold rather than a vector space: sparse principal component analysis over the Stiefel manifold, sparse blind deconvolution over the sphere, low-rank recovery over fixed-rank matrices. In Euclidean space the standard tool for with smooth and nonsmooth is the proximal gradient method, whose convergence theory (stationarity of limit points, an bound on the number of iterations to reach an -small step, an rate under convexity) is classical (Beck–Teboulle 2009).
Huang and Wei (arXiv:1909.06065, Mathematical Programming 2021) proposed the Riemannian proximal gradient method (RPG): at each iterate the proximal subproblem is posed on the tangent space, the nonsmooth term is pulled back through a retraction, and the next iterate is obtained by retracting the computed step. Unlike the earlier ManPG method of Chen, Ma, So and Zhang (2020), which uses the Euclidean proximal mapping of an embedding space, RPG is defined intrinsically on any manifold with a retraction. Its global convergence theorem is the subject of this mission.
Let be a finite-dimensional manifold with a smooth Riemannian metric on each tangent space , with norm . A retraction is a smooth map , , with and . The vector transport by differentiated retraction is ; denotes its adjoint for the two metrics and the adjoint of its inverse.
The problem is
with continuously differentiable, Riemannian gradient , and continuous, possibly nonsmooth. For the Riemannian Clarke subdifferential is defined through the pull-back on the Hilbert space :
A point is stationary if .
Algorithm 1 (RPG). Given and a constant , for let
choose that is a stationary point of with (condition (3.1)), and set .
Assumption 3.1. is bounded below and is compact. Assumption 3.2. is -retraction-smooth on : (inequality (3.2)).
For every run of Algorithm 1: if then is stationary. Under Assumptions 3.1 and 3.2, has an accumulation point, every accumulation point is stationary, and for every some iterate with index at most
satisfies .
Theorem 3.1 is the basic convergence guarantee of RPG: the method is a descent method without any convexity of , its limit points satisfy the first-order necessary condition , and the number of iterations needed to make the step small is explicit, with the same dependence as in the Euclidean case. It underlies the further analyses of the same paper (the rate under retraction convexity and the Kurdyka–Łojasiewicz analysis) and of later Riemannian proximal methods.
The theorem is proved on paper; no machine-checked version exists. Formalizing it requires a Clarke subdifferential on tangent spaces, its calculus (sum rule with a function, chain rule through a local diffeomorphism) and its closedness along convergent sequences on a manifold. None of these is in Mathlib. They are reusable well beyond this paper by any Riemannian nonsmooth optimization method.
The descent inequality and the iteration bound are elementary once Lemma 3.1 is available. The difficulty is the stationarity of accumulation points. The subproblem's optimality condition (3.8) lives in the tangent space at and involves a subgradient of at ; to pass to the limit, the gradients and subgradients must be compared across different tangent spaces, which is what the inverse-adjoint transport and Lemma 3.2 do. This needs joint continuity of the retraction and its differential on the tangent bundle and continuity of the metric, and then a closedness property of the Riemannian Clarke subdifferential that the paper cites from Hosseini, Huang and Yousefpour (2018, Theorem 2.2(c)) and that a complete development must prove. A pointwise argument at a fixed base point does not suffice, because the base points move.
Theorem numbers and pages are those of arXiv:1909.06065v4. The manifold is modelled on a finite-dimensional real inner-product space and carries a RiemannianBundle with a smooth metric (IsContMDiffRiemannianBundle). Retraction, differentiated-retraction transport and Riemannian gradient are the published definitions RiemOpt.BFGS.Setting and RiemOpt.FR.Setting; joint smoothness of on the tangent bundle is added, as on p. 4. The Clarke limit superior is taken in EReal along , so it never takes a default value. Accumulation points are MapClusterPt, and "in at most iterations" is an index . A run of Algorithm 1 is any sequence of iterates and steps satisfying (3.1); the step is a selection, not a function of the iterate.
Two hypotheses are explicit in the Lean statements. Each pull-back is locally Lipschitz, which p. 5 requires for the subdifferential to be defined. is , because the proof applies Lemma 3.2 to . Assumption 3.2 is stated in the form the proof of Lemma 3.1 uses: (3.2) at every for every tangent vector. Definition 3.1 read literally only constrains with , and under that reading Lemma 3.1 fails: a nonconvex can send far outside . The paper's own sufficient condition gives the strengthened form.
The formalization must not trivialize stationarity. The subdifferential is defined from the Clarke derivative of the pull-back alone. It does not involve or ContinuousLinearMap.inverse, so is a genuine condition. The run hypotheses are satisfiable, for instance on with , , , , .
Welcome contributions: the Clarke calculus on a real Hilbert space (sum rule, chain rule through a map, upper semicontinuity), local invertibility of near the zero section, and the closedness of the Riemannian subdifferential on the tangent bundle.
Adam (Kingma and Ba, 2015, arXiv:1412.6980) is one of the most widely used optimizers for training neural networks. It is a stochastic gradient method that keeps exponential moving averages of the stochastic gradients and of their coordinatewise squares, rescales both by bias-correction factors, and divides the first by the square root of the second. Its original convergence analysis was shown to be flawed (Reddi, Kale and Kumar, 2018, arXiv:1904.09237), and in the regime in which practitioners actually run it, with a constant step size, the iterates do not converge.
Barakat and Bianchi (arXiv:1810.02263, SIAM J. Math. Data Sci. 3(1), 2021) describe what constant-step Adam does instead: as the step size tends to zero, with the averaging parameters tending to one at rates proportional to , the interpolated iterates follow a deterministic non-autonomous ordinary differential equation. This mission formalizes that statement, Theorem 4.3 of the paper, together with the lemmas of its proof (§8.1).
Let with points , and its subset with coordinatewise. A random sample with law on a measurable space enters through an integrand with gradient in . The objective is and the second-moment map is .
Given a step size , parameters , in and , the Adam map sends to
coordinatewise. The constant-step iterates are and , driven by iid samples with law . The interpolated process is the piecewise linear function with .
The parameters satisfy and as , with . The limiting Adam ODE is , , where for
The vector field is singular at . A global solution is a continuous map , continuously differentiable on , that satisfies the equation for every .
Under the paper's assumptions (Assumptions 2.2 to 2.5, 4.1, and 4.2 ii) with ),
where is the global solution of the Adam ODE from .
The theorem justifies the continuous-time model of Adam that the rest of the paper studies. The convergence of the ODE to critical points of (Theorem 3.2) and its rates (Theorem 3.4) say something about the algorithm only through this approximation. It also isolates the role of the bias correction: the initial condition and the singular factors are exactly the trace of the debiasing step. The result is also the first step towards the long-run statement, Theorem 4.5, which bounds the time the iterates spend away from the critical points as .
The result is proved on paper. To the knowledge of the mission, none of it is machine-checked: there is no formal statement of Adam's dynamics on Prove2Me. A complete development would give a checked instance of the ODE method for a non-autonomous, non-Lipschitz limit field and a non-homogeneous Markov chain. The surrounding stochastic-approximation library (truncation by stopping, uniform integrability, tightness of interpolated processes, identification of limits by uniqueness) applies to other adaptive methods, such as RMSProp and AdaGrad variants, whose limits have the same structure.
The standard argument for constant-step stochastic approximation assumes a time-homogeneous mean field that is locally Lipschitz. Neither holds here. The mean field depends on the iteration index through the bias-correction factors . Its limit blows up as , and it is not Lipschitz in near . A direct Gronwall comparison between the iterates and the ODE therefore fails at the origin of time, which is exactly where the iterates start.
The iterates are also not known to be bounded. Moment bounds are only available while the debiased iterate stays in a ball. This forces the truncation and an argument that the truncation is asymptotically never triggered. That argument needs uniform-in-time bounds on the ODE solution (Proposition 7.6) and uniqueness of the solution (Proposition 7.12), and both rest on a Lyapunov function specific to the case .
E d × E d × E d with E d = EuclideanSpace ℝ (Fin d). The paper's is the Euclidean norm of , written zNorm, not Mathlib's max norm on products.iIndepFun. Every with has law , and is unused.𝓝[>] 0). The event is written as , which is the same event.A trivializing formalization is ruled out. and are universally quantified before the limit and do not depend on . The limit is in , not in at fixed ; constant-step Adam does not converge in . The solution is tied to the , , , of the stochastic model. All hypotheses are satisfiable, for example by with equiprobable.
A complete development needs:
Contributions to any of these, including reusable statements about interpolated processes, are welcome.
A chance-constrained program chooses a decision so that a random vector falls outside a decision-dependent safety set with probability at most . Chance constraints are a standard model for reliability requirements in power systems, supply chains and transportation, where a plan must survive random demand or supply with high probability. In practice the distribution of is known only through samples , and the sample average approximation (SAA) that replaces it by the empirical distribution is sensitive to the particular sample.
Distributionally robust chance constraints regularize SAA by requiring the probability bound for every distribution within Wasserstein distance of . Chen, Kuhn and Wiesemann (arXiv:1809.00210) and Xie (doi:10.1007/s10107-019-01445-5) showed that, for safety sets defined by linear inequalities, the resulting program (DR-CCP) is a mixed-integer linear program with a big-M constant. These big-M formulations are hard for solvers to close when is small. Ho-Nguyen, Kılınç-Karzan, Küçükyavuz and Lee (doi:10.1007/s10107-020-01605-y) connect the formulation to the mixing sets of SAA and to robust 0–1 programming, and derive a smaller and tighter formulation that is still exact.
The random vector lives in with an arbitrary norm ; in the formalization it is a finite-dimensional real normed space . The dual norm of a linear functional is . The decision ranges over a set .
The 1-Wasserstein distance between distributions is the infimum of over couplings of and . The ambiguity set is the set of distributions within distance of . The feasible region of (DR-CCP) is
Throughout, and are fixed.
The paper studies joint chance constraints with right-hand side uncertainty: for there are , and , and
Write and . Let be the -th largest value among , and let .
The big-M formulation (5) of Chen et al. uses binaries , slacks and a scalar with
The paper's improved formulation (20) keeps the first two families, adds the knapsack constraint , replaces in the third family by , imposes it only for , and adds for every .
The goal states equality of feasible sets of . Because the objective depends on alone, this is the paper's "exact reformulation".
Milestones 2 and 3 are results of Chen, Kuhn and Wiesemann that this paper cites and uses, not results it proves.
Theorem 3 says that the scenario-wise big-M rows of the Wasserstein chance constraint can be replaced by at most rows per , with coefficients computed from the data. Remark 2 of the paper counts at least fewer rows than (17). The reduced form exposes a robust 0–1 substructure, and the paper adapts Atamtürk's valid inequalities for it. Its computational study reports order-of-magnitude speed-ups on stochastic transportation problems.
The results are proved on paper; none is machine-checked. The formalization would give a verified chain from the Wasserstein worst-case probability to a finite mixed-integer system. Milestone (3), the dual reformulation, is reusable for any distributionally robust chance constraint over a 1-Wasserstein ball around an empirical distribution, and (4b) for any polyhedral safety set. A second formalization layer would verify the order-statistic arguments (Lemma 1, Proposition 1) used throughout the quantile-strengthening literature.
The deterministic parts — Theorems 1–3 given (3) and (4b) — are finite case analyses on , but each step relies on order statistics of the sample with ties. Lemma 1 rests on the paper's "without loss of generality, sort the distances", and a formal proof must handle ties and the floor exactly. The paper's proof of Theorem 2 argues "at optimality"; for a statement about feasible sets that argument has to be replaced by an explicit choice of .
The hard step is (3). It exchanges a supremum over all Borel probability measures in a Wasserstein ball for a scalar system. The naive attempt, which perturbs by moving mass from the samples to the nearest unsafe points, proves only one inclusion. The other needs strong duality for worst-case probabilities over transport balls, together with attainment of the dual infimum, which uses .
E with [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] and its Borel σ-algebra. The norm is arbitrary, not the sup norm of Fin K → ℝ.StrongDual ℝ E), so is its operator norm.Fin L → ℝ, with written a p ⬝ᵥ x. Indices are 0-based.ModelRiskOT.WorstProb.worstProb with cost , valued in , around the published WassersteinDRO.Duality.empiricalDistribution.Metric.infDist.Standing assumptions and pins in every statement:
In (17b), the printed "(5b)–(5d) and (5c)" is read as "(5b)–(5d) and (8c)", following the proof of Theorem 2 and (20b).
Several trivializing formalizations are ruled out:
infDist never sees the empty set;Welcome contributions:
A distributionally robust decision evaluates a rule against every data distribution within a specified transport budget of a baseline law. The budget is a modeling choice: increasing it expresses more uncertainty about the data. A robust objective value can increase with that budget, but the value alone does not describe how the adverse distribution changes. For a fixed linear decision, Blanchet, Murthy, and Zhang identify the worst-case distribution and ask what happens to each observation as the budget increases. Their Theorem 7 gives a sample-wise answer in a small-radius regime: adverse observations move along straight lines, and their distance from the original observations grows monotonically.
This matters when a robust solution is interpreted through its adverse scenarios. The result says that two nearby ambiguity budgets do not produce unrelated worst-case data sets. They produce a coherent family of transported observations whose directions are determined by the sign of the loss derivative. The theorem is a structural property of an optimal-transport ambiguity set, beyond a bound on its optimal value. It appears in a paper that also develops dual formulas and iterative optimization schemes for the same model Blanchet, Murthy, and Zhang, 2022.
Let take values in with baseline law . A decision belongs to a convex set and incurs loss . At each source point , a positive-definite matrix defines the transport cost
The matrix may depend on , so movement can be cheaper in different directions and at different observations. The model requires lower semicontinuity of and almost-sure lower and upper spectral bounds for . A distribution is within the ambiguity ball of radius when it can be coupled with at expected cost at most . The worst-case objective is the supremum of over that ball. In Lean, the equivalent coupling formulation records a joint law with first marginal , second marginal , and cost at most .
The paper reduces the worst-case calculation to a dual objective , where prices the transport budget. Its pointwise term is the supremum over a scalar of the function in display (7). The set of maximizing scalars is . A scalar maximizer produces a transported observation
Assumptions 2–4 require a convex loss with controlled growth, a fourth moment of , bounded second derivatives of the loss, a nondegenerate loss derivative, and compactness of . The statement here also uses Assumption 5, local strong convexity with a positive-probability nondegeneracy condition. The paper’s proof of Theorem 7 uses that condition through its small-radius strong-convexity result Theorems 4 and 7.
For each fixed , the goal asserts that there is a common threshold and a family such that the law of is the unique worst-case distribution for every . For any pair , it asserts, -almost surely,
Consequently,
The goal keeps the uniqueness and primal attainment clauses together with these comparisons. The milestones follow the paper’s prerequisites: the optimizer and curvature bounds of Proposition 9, the unique worst-case law of Theorem 6(e), uniqueness of the dual minimizer at small radius, and the sign of the pointwise maximizer. Each has its own statement so solvers can use it elsewhere.
The theorem gives a consistent interpretation of changes in the ambiguity radius. If the loss increases locally in the decision direction, an adverse observation moves farther in that direction; if the loss decreases, it moves farther in the opposite direction; at a stationary score it stays put. The corresponding displacement norm is monotone for each radius pair, almost surely. This is stronger than monotonicity of the worst-case objective value: it describes the geometry of a family of optimizers, not only their values.
The paper proves the result in §5.4. The work of this mission is to formalize its hypotheses, optimality claims, and sample-wise inequalities in Lean. The published ModelRiskOT.Duality coupling definitions already give a reusable primal interface; this mission adds the state-dependent quadratic cost, the scalar dual model, its small-radius regions, and the comparative-statics statements. The proof obligations remain open in this draft. Their formalization would also make the dual optimizer bounds and the deterministic transport representation reusable in later optimal-transport DRO developments.
The worst-case value being monotone in does not force a particular worst-case distribution, or each observation in one, to move monotonically. The theorem needs a unique worst-case law and a coherent choice of pointwise maximizers as varies. The scalar maximizer depends on both the radius and the dual price, while the optimal dual price itself changes with the radius. The paper’s small-radius conditions keep this joint variation controlled. Without uniqueness, two optimal laws could differ even at the same radius, and a sample-wise comparison would have no fixed object to compare.
The result also involves several layers of almost-sure reasoning. Spectral bounds on hold only outside a null set; the relevant maximizer and its transported law must be measurable enough to define pushforwards and expectations. These conditions must be carried through the theorem without silently replacing an almost-sure claim by a pointwise one.
Vectors use EuclideanSpace ℝ (Fin d), and the baseline is a Borel probability measure. The decision set is convex and compact and is explicitly nonempty. Assumption 1 gives positive definiteness of everywhere, lower semicontinuity of the cost, and almost-sure uniform spectral bounds. The loss satisfies Assumptions 2–5. The fourth moment in Assumption 2 and the bounds on control the integrals used by the dual theory. A positive ambiguity radius is required whenever its square root appears.
The dual terms and use extended-real values, since the pointwise supremum can be infinite. The worst-case value is a supremum over feasible couplings, with signed loss integrated using the published extended-real integral. A graph coupling witnesses attainment, and every optimal coupling must have the same second marginal. This ties the family to the actual worst-case distribution rather than an arbitrary monotone scalar field. Almost-everywhere measurability of and the transport map is part of the conclusion.
The radius varies inside the goal. The threshold is chosen before any radius pair, and the comparisons are stated almost surely for each pair. The paper prints Theorem 7 under Assumptions 1–4 while referring to and invoking Theorem 4, which uses Assumption 5; this mission includes Assumption 5 explicitly. It also reads the singleton clause of Theorem 6(e) almost surely, because its threshold is an essential supremum, and uses a non-strict lower curvature bound in Proposition 9(b), as its proof permits. Contributions on the small-radius dual theory, measurable maximizers, primal attainment, and the radius comparisons are all within scope.
The alternating direction method of multipliers (ADMM) is a standard method for convex problems whose objective splits into two blocks coupled by a linear constraint (Gabay & Mercier 1976; Boyd et al. 2011). Many models in imaging, statistics and sparse or low-rank recovery have three or more blocks, and the scheme practitioners reach for first is the direct extension of ADMM: minimize the augmented Lagrangian over each block in turn, then update the multiplier. For years it was unknown whether this scheme converges in general.
Chen, He, Ye and Yuan (Math. Program., 2016) settled the question negatively: on a three-variable linear system with zero objective, the direct extension diverges for every penalty parameter (their Theorem 3.1). Their Section 4.1 then asks whether strong convexity of the objective rescues convergence. Han and Yuan (J. Optim. Theory Appl., 2012) had proved convergence for strongly convex objectives under a restriction on the penalty parameter determined by the strong convexity moduli. Theorem 4.1 shows that this restriction cannot simply be removed. This mission formalizes Theorem 4.1 and the three facts on p. 14 that support it.
Timeline:
The three-block problem (1.1) is
with , , closed convex sets and convex functions ; the solution set is assumed nonempty.
For a penalty parameter and a multiplier , the augmented Lagrangian (1.6) is
The direct extension of ADMM (1.5) starts from and, for , sets , , to minimizers of over in that order, each with the newest values of the other blocks, and then sets .
A function is -strongly convex if is convex.
The instance (4.1) is
with scalar , and . Its unique solution is . For the state after an iteration is , and denotes the iteration matrix that maps to .
For the model (1.1) with strongly convex objective, (1.5) is not necessarily convergent for all . Formally, (4.1) satisfies the standing assumptions, each is -strongly convex, and at there is a starting point from which a run of (1.5) exists and
The goal fixes the witness instance and , because those are what the paper computes. It does not fix the starting point.
Theorem 4.1 says that strong convexity of each , on its own, does not make the three-block direct extension of ADMM converge. Convergence results for strongly convex models therefore have to restrict , as Han and Yuan do, or modify the scheme. Examples of modified schemes are a shrunken multiplier step (discussed in §4.2 of the paper) and Gaussian back substitution (He, Tao & Yuan 2012). The example is also a concrete test case: any proposed sufficient condition for convergence has to exclude (4.1) at .
The theorem is proved in the paper, but only in outline: the iteration matrix is not printed, the spectral radius is reported as the outcome of "a simple calculation", and the construction of a divergent starting point is "omitted for succinctness". A formalization makes each step explicit and machine-checked. That means the exact iteration matrix, a certified enclosure of its spectral radius, and a real starting point whose iterates are unbounded. As far as is known, none of these results has been machine-checked.
There are three separate difficulties.
A natural first idea is to argue that strong convexity of the objective forces the iterates toward the unique solution. This fails because the multiplier and the coupling between blocks are not controlled by the objective's curvature once is large relative to the moduli.
Vectors in are Fin n → ℝ and matrices are Matrix (Fin p) (Fin n) ℝ. The Euclidean square norm in (1.6) is written (⬝ᵥ), never Mathlib's sup norm. Norms appear otherwise only in "", where every norm on gives the same meaning. Blocks are separate fields, and multiplier components are 0-based. A run is a predicate on sequences: "" means " is a minimizer", and is never read. "Converges" means convergence of in the product topology.
Strong convexity is Mathlib's StrongConvexOn Set.univ (1/10). The paper's "closed convex" are real-valued on all of , hence continuous, so only convexity is stated.
The quantifier "for all " is read as "not for every ", witnessed at . The stronger reading, divergence for every , is false for (4.1), where the spectral radius is below for small .
Trivializations ruled out. The goal asserts the existence of a run, so non-convergence cannot hold vacuously. Runs are characterized by minimizer conditions rather than an argmin choice function with junk values. Spectral statements are over rather than over real eigenvalues only; the only real eigenvalue of is .
What a complete development needs: first-order optimality for strictly convex scalar quadratics; existence and uniqueness of the subproblem minimizers; a certified root enclosure for a quartic with rational coefficients (via Rouché-type bounds, interval arithmetic or an explicit factorization over ); and the passage from a dominant complex eigenpair to a real unbounded orbit. The last two are reusable for any linear-iteration divergence argument, including Theorem 3.1 of the same paper. Contributions of any of these lemmas, as separate theorems, are welcome.
In classical optimal transport, a transport plan that minimizes the total cost is characterized through its support: an optimal plan is -cyclically monotone, meaning that no finite collection of its transported particles can be re-paired more cheaply (Villani, Optimal Transport, Old and New, 2009, Ch. 4–5). This pointwise criterion is how most structural results in optimal transport are proved: it is what turns a global minimization over measures into a statement about finitely many points.
The martingale transport problem adds a constraint motivated by mathematical finance: the plan must be the law of a one-step martingale with given marginals , . Its value gives model-independent bounds on the price of an exotic option whose payoff is the cost function, given the prices of all vanilla options at two dates (Beiglböck, Henry-Labordère, Penkner, Model-independent bounds for option prices, Finance Stoch. 2013). Because the martingale constraint ties together all points with the same first coordinate, the classical re-pairing argument does not carry over: swapping two destinations generally destroys the martingale property.
M. Beiglböck and N. Juillet (On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 2016; arXiv:1208.1509v2) prove a martingale replacement for -cyclical monotonicity, the variational lemma (Lemma 1.11). It is the tool from which they derive the left-monotone structure of optimal plans, the uniqueness of the left-curtain coupling as optimizer for costs with strictly convex, and the support bounds for optimizers. This mission is the first of a series formalizing that paper.
All measures live on or with their Borel -algebras. Two probability measures on with finite first moment are in convex order, , if for every convex .
A transport plan is a measure on with first marginal and second marginal . It is a martingale transport plan, , if under the conditional mean of given equals ; equivalently,
A cost is a Borel function satisfying the sufficient integrability condition with , ; then the cost of a plan, , is well defined in . A plan is optimal if for every , and it leads to finite costs if .
A measure on is a competitor of (Definition 1.10) if it has the same two marginals as and the same conditional barycentres: for almost every , where , are disintegrations with respect to the first marginal. A competitor redistributes the mass of in a way that a martingale plan could absorb: replacing a piece of a martingale plan by keeps both marginals and the martingale property.
Let be probability measures, a Borel cost satisfying the sufficient integrability condition, and optimal with . Then there is a Borel set with such that
The set is chosen once, before ; the quantifier order is the content.
The milestones are the steps of the paper's proof (§3, pp. 16–19), in attack order:
The result. The variational lemma converts optimality of a martingale plan, a property of a measure, into a condition on finite configurations of points in its support. In the paper it is applied, together with a lemma on accumulation points of sections (Lemma 3.2), to show that optimizers for costs with strictly convex are left-monotone, which by the paper's Theorem 1.5 identifies them as the left-curtain coupling; it also yields the bound of Theorem 7.1 and the two-graph structure of the optimizers for . Later missions of this series use it as a milestone. Its converse, under continuity assumptions, is the separate Lemma A.2 of the paper's appendix.
Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization needs a usable form of Kellerer's duality for multi-marginal problems, which is not in Mathlib, and the bookkeeping that finite rearrangements of a martingale plan stay in . Both are reusable well beyond this paper: Kellerer's theorem underlies the analogous results for classical, multi-marginal and martingale transport.
The classical proof of -cyclical monotonicity perturbs an optimal plan by moving a small amount of mass around a finite cycle of its support points. For martingale plans this fails: the perturbation must preserve the conditional barycentre of every , and mass sitting at isolated points of a non-atomic plan cannot be moved without moving mass at uncountably many other points. The proof therefore cannot argue point by point. It works with whole families of bad configurations at once, which requires the measure-theoretic duality of Kellerer (resting on Choquet's capacitability theorem) and a measurable choice of an optimal competitor for each configuration. Proving that the set of bad configurations is Borel, and that a positive-mass family of them can be glued into a cheaper competitor of a piece , is the technical core.
The Lean development uses Mathlib's Measure ℝ and Measure (ℝ × ℝ). Costs and integrals that may be infinite take values in EReal, through the published definition ModelRiskOT.Duality.extIntegral (, with ); no Bochner integral of a possibly non-integrable function is compared. Martingale plans and competitors are encoded through test functions (the paper's characterization (4), p. 10) instead of disintegrations. A finitely supported finite measure is written with a finite set and weights ; this covers every such measure, and masses are taken finite. is Fin n → ℝ × ℝ.
Committed conventions and disclosed additions:
A formalization in which is empty or -null, or in which is allowed to depend on , is trivial and is ruled out by the statement: and . The competitor ranges over all measures, not only finitely supported ones.
Welcome contributions: a general form of Kellerer's duality theorem (milestone 1), the Borel-measurability of the bad set, and the gluing step of milestone 6.
Proximal gradient methods are used to minimize an objective with one smooth part and one convex part whose proximal map can be evaluated. A small proximal gradient step is a practical stopping signal, but it indicates proximity to an optimizer only when the objective has an appropriate error bound. Section 4 of Drusvyatskiy and Lewis gives conditions for that bound in the structured problem : the conditions concern the dual problem and the growth of the two component functions, rather than requiring strong convexity of their sum. This matters for problems with a nontrivial solution set and for penalties that are not strongly convex. The paper places this result after its §3 comparison of quadratic growth and proximal gradient error bounds (pp. 9–11).
Let and , with their Euclidean inner products and norms. Let be linear, be continuously differentiable and convex, and be proper, lower semicontinuous, and convex. The primal objective and its minimizer set are
The mission assumes is nonempty and bounded. Its minimum is finite. For an extended-real function , its Fenchel conjugate is . The dual objective is , and denotes a dual minimizer. The effective domain is ; denotes relative interior. The paper assumes dual nondegeneracy, , and dual strict complementarity, (p. 10).
A closed convex function is firmly convex relative to when its tilt grows at least quadratically away from its minimizers on each compact set. The positive coefficient may depend on the compact set. Theorem 4.2 assumes this property for at and for at (Definition 4.1, p. 11).
For , a proximal gradient step is , and its residual is . The error bound asks whether the distance from to is controlled by whenever lies below a prescribed objective threshold (Definition 3.1, p. 5).
The milestone path records the Kuhn–Tucker description of , the relative-interior identity (4.3), the compact-set distance estimate (4.4), the two component inequalities (4.5), and the resulting quadratic growth of on every sublevel set. In particular, for each there is such that
These are the claims stated in §4 and in the proof of Theorem 4.2, pp. 10–11. The milestone for (4.5) retains the paper's printed in its quotation, while the Lean statement uses positive constants, as Definition 4.1 requires for nontrivial quadratic growth.
The goal is Theorem 4.2: under the conditions above, for every there exist such that
The formal statement makes explicit that has a Lipschitz constant. This is part of the §3 setting used by the paper's Corollary 3.6 to reach the displayed error bound. A companion statement, Theorem 4.5, pp. 12–13, says that the Moreau envelope of a firmly convex function retains firm convexity relative to the same vector.
The conclusion converts dual geometric information and component growth into an error bound expressed through a proximal gradient step. The residual is available when running the method, whereas the distance to is generally not. Combined with the paper's §3 results, the error bound yields local convergence guarantees for the proximal gradient method in structured convex problems (Corollary 3.6 and Theorem 4.2). The statement covers settings in which component functions have local quadratic growth after a tilt while the composite objective need not be strongly convex.
The research result is proved in the paper. The work of this mission is to formalize its exact assumptions and claims, including the convex dual and the relative-interior statements, then supply machine-checked proofs. The resulting Euclidean conjugate, firm-convexity, and structured-objective definitions can also support other convex optimization formalizations. The statements in this proposal are proof obligations; compiling the statements alone does not establish the theorems.
Component growth concerns distance to separate subdifferential inverse images. The desired error bound concerns distance to their intersection, which is the primal solution set. Two small component distances do not automatically control distance to an intersection: the sets can meet at a poor angle. The dual interior hypotheses supply the regularity needed in (4.4). The argument also changes the quantity being controlled from objective growth to a proximal gradient residual. Those two changes are the substantive steps a proof must justify; treating either as an unrestricted distance identity would change the theorem.
The Lean spaces are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); dimensions zero are permitted. The linear map is continuous, and is its adjoint. Extended-real values use EReal; properness excludes values, and lower semicontinuity encodes closedness. Conjugates take suprema in EReal, and the dual objective follows (4.2). Relative interior is intrinsicInterior ℝ. The published convex subdifferential, proper-convex predicate, and proximal-point predicate are imported as reference items because their meanings match the paper's objects. The paper's Euclidean conjugate is defined locally because the available published conjugate has a strong-dual codomain.
The minimum value is real and is pinned to the nonempty primal minimizer set. The dual point is pinned as a minimizer of . Proximal steps are expressed as argmin predicates, so no default result is chosen for a failed minimization. The firm-convexity predicate requires a nonempty minimizer set of the tilted function: otherwise Lean's real distance to the empty set would be zero while the source uses an infinite distance. The growth constant of Definition 4.1 and the constants of (4.5) are strictly positive: the page leaves the sign implicit or prints , but with a zero constant every convex function would be firmly convex, contradicting the page's own example , and the growth statements would be empty. The error bound is restricted to the stated sublevel set, and all of its constants are positive. The goal includes a nonnegative Lipschitz constant for , disclosed because the source's §3 bridge to the error bound assumes one; the component-growth milestones do not assume it.
Contributions should establish the Euclidean convex-duality identities, the compact-set regularity estimate, the component and composite growth claims, and the proximal gradient conclusion. The Moreau-envelope preservation theorem is a separate companion target. None of the dual interior conditions or the firm-convexity assumptions may be replaced by a vacuous condition: the goal concerns their effect on the actual solution set of .
Many quantities in stochastic analysis and mathematical finance depend on the whole past of a process, not only on its current value: running maxima, averages, integrals against the quadratic variation, payoffs of path-dependent options, conditional expectations of path functionals. The classical Itô formula describes the evolution of for a smooth function of the current state; it says nothing directly about a process that depends on the path .
In 2009 Dupire proposed two pathwise derivatives for such functionals, a horizontal (time) derivative obtained by freezing the path and a vertical (space) derivative obtained by bumping its endpoint, and a change-of-variable formula built on them (Dupire 2009). Cont and Fournié gave this calculus a rigorous framework and proved the functional Itô formula for continuous semimartingales (Cont and Fournié, Ann. Probab. 2013; preprint arXiv:1002.2446v5). The companion paper (Cont and Fournié, J. Funct. Anal. 2010) gives a pathwise version in the spirit of Föllmer. The formula underlies the martingale representation results of the same paper and the later theory of path-dependent PDEs.
Fix a horizon . A path is a cadlag function on ; denotes the -valued ones and the paths with values in the positive semidefinite matrices. For a path :
A nonanticipative functional assigns a real number to each pair , measurably for the -algebra generated by the evaluations of the paths (Definition 2.1). Paths at different times are compared with the distance (9),
is left-continuous (, Definition 2.4) if is close to whenever is -close to ; it is boundedness preserving (, Definition 2.5) if it is bounded on sets of paths with values in a compact set. The horizontal derivative is
and the vertical derivative is the gradient at of ; is the vertical derivative of . (Definition 3.6) is the class of left-continuous with continuous at fixed times, left-continuous, and .
On a filtered probability space satisfying the usual hypotheses, is a continuous -valued semimartingale and its quadratic covariation has a density, (3), with cadlag, adapted, -valued. has predictable dependence on when (10).
For every verifying (10) and every , almost surely,
Theorem 4.1 shows that a path-dependent process is a semimartingale whose decomposition is computed from the jet along the path of . It contains the classical Itô formula () and covers functionals such as , and . Downstream it yields the identification of the martingale part of , the intrinsic character of the vertical derivative of an adapted process (Corollary 4.4), and the representation of smooth martingales (Theorem 5.2), which is the subject of the second mission of this series.
The result is proved in the paper. No machine-checked proof of it exists; the classical multidimensional Itô formula itself is an open goal on this platform (EthierKurtz.ito_formula). This mission produces a formal definition layer for functional Itô calculus (stopped paths, the metric , the regularity classes, pathwise derivatives) and a formal statement of the formula with its supporting lemmas.
The obvious argument fails at its first step: a path functional cannot be differentiated along the path of . The horizontal derivative freezes the path and the vertical derivative bumps only its endpoint; neither is a perturbation of in the direction of its own increments, so the chain rule behind the classical Itô formula has nothing to act on. A second obstruction is regularity: is only cadlag, the derivatives of are only left-continuous or continuous at fixed times for , and the paths at which they must be evaluated live on intervals of different lengths. Any limit procedure therefore needs uniform control of cadlag paths in the sup norm, which fails across their jumps, together with convergence theorems for stochastic integrals whose integrands are only locally bounded. Finally, the classical Itô formula, which is a special case, is itself not yet formalized.
Time is with horizon , and every statement concerns . Paths are functions on ; a path on is represented by its stopped version , which also serves as the horizontal extension. Functionals are defined on all path pairs and are required to be nonanticipative (); every continuity, boundedness and differentiability condition quantifies only over pairs cadlag on with positive semidefinite , as in the paper. The norm on pairs (vector, matrix) is the largest absolute value of the entries; "" is an explicit bound, so unbounded suprema never count. The derivatives are witnesses tied to by one-sided and Fréchet derivative statements, which makes them unique; free derivative witnesses, a functional that is not nonanticipative, and conditions over non-cadlag paths are each excluded. Definition 2.1's measurability is part of the class: without it Theorem 2.7 fails.
The semimartingale is with continuous, adapted, of bounded variation, and a continuous local martingale componentwise (the published EthierKurtz.IsSourceLocalMartingale); (3) uses the published EthierKurtz.HasCrossVariation. The Itô integral in (30) is the limit in probability of dyadic left Riemann sums (the published EthierKurtz.itoStepSum): the goal states that these sums converge to the remaining terms of (30). This is the a.s. identity, not a weakening, because limits in probability are unique; it is not a junk limit, because the integrand is left-continuous up to a -null set, adapted and locally bounded. The -integrals have bounded integrands by , so the Bochner integrals are genuine.
A complete development needs: cadlag path lemmas (A.1–A.3), stopping times of jumps, the predictable -algebra (in Mathlib), the classical Itô formula, and dominated convergence for stochastic integrals. The cadlag lemmas and the path-space layer are reusable beyond this mission. Proofs of any milestone, of the classical Itô formula, and of the stochastic-integral convergence theorems are welcome.
An online retailer does not show its catalogue at once. Products are arranged on a sequence of pages, and a consumer looks at the first few pages and then chooses among what she has seen, or leaves. Where a product is placed therefore decides whether it is considered at all. Gallego, Li, Truong and Wang (Operations Research, 2020) call the placement decision product framing. They show that the optimal framing problem is NP-hard even with two pages and a multinomial logit choice model, and give polynomial-time framing algorithms with constant performance guarantees.
The paper builds on the assortment optimization literature, where a seller chooses one set of products to offer under a choice model, and on work in which consideration sets depend on how products are presented. Davis, Topaloglu and Williamson (2015) studied a sequential assortment problem in which products are added over time. Two of their results, on how per-product revenue behaves when products are removed, are the structural inputs of this mission. Aouad and Segev (2016) studied a variant with one product per page under the MNL model, in which every product must be displayed.
There are products , and product earns unit revenue . The products are placed on pages, each holding at most products, and a product may be left undisplayed. A consumer views the first pages, where is random with law and tail , independent of the framing. Her consideration set is the set of products on pages .
A choice model gives, for each consideration set , purchase probabilities with for and . The expected revenue of is . The optimal framing value is
the maximum over all placements with at most products per page (problem (1)). The cardinality-constrained assortment problem is (problem (2)), and is the best revenue from a consumer who sees pages.
The analysis rests on three assumptions:
The algorithm NEST(), for , first takes an optimal solution of (2) with bound . Then, for down to , it chooses of size whose per-product revenue is at least that of . Page displays , and pages after stay blank. is the expected revenue of this framing, and .
The goal holds under A1, A2 with and A3, for every run of NEST(), . Here .
The milestones are the numbered results the proof of Theorem 3 uses, in the order it uses them:
taken over NBUE tails and functions that are increasing with decreasing and . Proposition 3 states . 7. Lemma 7 and Corollaries 5–6, comparing NBUE with an exponential variable of the same mean. 8. The evaluation for exponential with mean . 9. The bound .
Theorem 3 gives a constant-factor guarantee for a problem that is NP-hard under the same assumptions. The constant does not depend on the choice model beyond A1, on the number of pages, or on the page capacity, and the paper shows it is tight relative to the upper bound (Proposition 4, in the geometric limit). NEST needs only a cardinality-constrained assortment oracle, which exists in polynomial time for the MNL and nested logit models. The same bound-revealing program, problem (5), is reused in the paper for joint framing and pricing (Theorem 7).
The paper proves the result in full. No part of it has been machine-checked. The mission formalizes the model and states the guarantee and every intermediate result. The proofs combine finite combinatorics (Lemmas 1 and 2, Proposition 1) with a comparison of a discrete NBUE law against the exponential distribution, and that comparison is reusable for other approximation analyses with the same structure. The equality of the exponential integral with connects to Mathlib's hasSum_zeta_two.
The upper bound (Theorem 2) and the lower bound (Proposition 1) are each elementary. The difficulty is to compare them uniformly over all choice models and all NBUE page-count laws. The ratio of to depends on the whole function and the whole law of , and the worst case cannot be read off from any single instance. Replacing the instance by the program (5) removes the choice model. Bounding the program still requires an optimization over distributions, and its value is attained only in a limit (Proposition 4).
The comparison with the exponential law goes through the increasing convex order. Here is a discrete law on and the comparison variable is continuous. The function to which Lemma 7 is applied is increasing and convex only on , so a formal argument has to track the domain.
Theorem numbers and pages are those of the authors' accepted manuscript (49 pp.), which differ from the journal typesetting. The conventions are:
Fin n. Pages are the naturals , kept 1-based, with .Fin n → ℕ: page means "not displayed", and each page holds at most products. is the maximum over the finite, nonempty set of feasible framings.expMeasure with rate . The independence in Corollary 6 is encoded by iterated integrals.NEST makes arbitrary choices, so a run is a predicate on its output. Theorem 3 is stated for every family of runs, and a separate milestone shows that runs exist. The value is the expected revenue of the framing the run actually displays, not the closed form , whose equality with it is part of the proof of Proposition 1. A formalization that quantified over some run, that defined by that closed form, or that assumed Lemma 2 for would not be Theorem 3.
Program (5) is stated with its tail variable and law , . The page's typos are corrected in the statements and recorded in the notes: "" in (5), and the right-hand side of Corollary 5. Proposition 2 is formalized in its existential reading: some optimal solution of (5) has constant .
A complete development needs:
The exponential comparison and the integral are reusable beyond this mission. Proofs of any milestone are welcome, including alternative proofs of Lemmas 1 and 2 from A1.
Adam (Kingma and Ba, 2015, arXiv:1412.6980) is the default optimizer for training deep neural networks. At each step it keeps exponential moving averages and of the stochastic gradients and of their coordinatewise squares, corrects both for their initialization at zero (the bias-correction or debiasing step , ), and moves the iterate by . Despite its use, its convergence theory for nonconvex objectives was thin; the original convergence argument was later shown to be flawed (Reddi, Kale and Kumar, 2018, arXiv:1904.09237).
Barakat and Bianchi (arXiv:1810.02263v4, SIAM J. Math. Data Sci. 3(1), 2021, doi:10.1137/19M1263443) study Adam through the ODE method: when the stepsize tends to zero and the averaging constants satisfy , , the interpolated iterates follow a deterministic non-autonomous differential equation, the continuous-time Adam ODE. Everything else in the paper (convergence of the trajectory, rates under a Łojasiewicz condition, tracking by the constant-step iterates, almost-sure convergence of a decreasing-step variant) presupposes that this ODE is well posed from Adam's initialization. This mission formalizes that well-posedness result, Theorem 3.1 of the paper.
Let and , with points ; set , and . The data are reals , a function (the objective) and a map (in the paper, and , the mean squared gradient). All vector operations are coordinatewise. The Adam vector field is, for ,
and (ODE) is . The factors and are the continuous-time debiasing. A global solution with initial condition is a continuous map , continuously differentiable on , satisfying (ODE) for every , with .
The proof works with the regularized equations : for , and for , where . The fields are extended to by replacing with , and denotes the set of solutions on , . The Lyapunov function is with , and its limit is . The debiasing map is .
The hypotheses are those of §7 of the paper: is with locally Lipschitz gradient (Assumption 7.1) and coercive (Assumption 2.3); is locally Lipschitz (Assumption 7.2) with coordinatewise (Assumption 2.4); and (Assumption 2.5).
For every there is a global solution of (ODE) with initial condition such that
and any two global solutions with initial condition coincide on .
Theorem 3.1 makes the continuous-time Adam trajectory a well-defined object. The paper's convergence theorem for this trajectory (Theorem 3.2), its rate under a Łojasiewicz condition (Theorem 3.4) and the tracking result for the constant-step iterates (Theorem 4.3) are all stated about "the" solution, and the semiflow used for the asymptotic pseudotrajectory argument rests on the same uniqueness. The bound of Proposition 7.6 also gives the cost decrease , which the authors read as evidence that the bias correction makes early Adam steps safe.
The result is proved in the paper, and as far as is known nothing here has been formalized; no statement about this ODE exists on the platform. The mission formalizes the statement and the numbered lemmas of its proof. A complete development would also be a worked example of existence for an ODE whose field is neither continuous in time at nor Lipschitz in space, by regularization, compactness and passage to the limit.
Off-the-shelf theory does not apply. Cauchy–Lipschitz fails because contains , which is not Lipschitz at , and the initial condition has . Cauchy–Peano fails because blows up as : the factor behaves like . The obvious remedy, shifting time by , gives solutions , but passing to the limit needs bounds uniform in , both on the trajectory and on how far stays from zero. Uniqueness then has to be proved by a Grönwall argument whose coefficient is not integrable at , so the initial behaviour of solutions must be controlled to second order. Solutions from initial conditions with , need not exist at all (p. 5), so the special initialization is essential, not cosmetic.
Vectors are EuclideanSpace ℝ (Fin d) and states are triples; Lean's norm on the product is the maximum of the three Euclidean norms, which changes no boundedness, compactness or continuity statement. and are abstract functions satisfying Assumptions 7.1, 7.2, 2.3 and 2.4, as in §7 of the paper. Under Assumption 2.2 the expectation-defined and of (2.2) satisfy these, so the goal implies the theorem as printed. Coercivity is Tendsto F (cocompact _) atTop. Solutions are maps constrained only on : uniqueness is agreement on , never ∃! over all functions. The field is evaluated only at , where Lean's (1 - exp 0)⁻¹ = 0 cannot interfere. ranges over WithTop ℝ≥0 ( is and selects ), and over WithTop ℝ. The solution sets are -valued with the extension, as on p. 12, so positivity of is a theorem (Lemma 7.4), not an assumption.
A notion of solution without the differential equation, with it only away from on a set like , or with a derivative not tied to would make existence trivial. The definitions here require at every , continuity at and the exact initial value.
Mathlib provides Picard–Lindelöf, Grönwall-type bounds and Arzelà–Ascoli, but no Cauchy–Peano theorem; a reusable Peano existence theorem with maximal-interval extension would be a valuable contribution beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of the goal.
A McKean–Vlasov or mean-field stochastic differential equation is an SDE whose coefficients depend on the law of the solution itself. Such equations describe the limit of large systems of weakly interacting particles (Kac's kinetic models, McKean's propagation of chaos) and are the state dynamics of mean-field games and mean-field control. For a classical diffusion the expectation of a terminal payoff is a function of time and state and solves a linear parabolic PDE (the Feynman–Kac connection). For a mean-field diffusion the same expectation depends on time, on the state and on the current law of the population, so the associated PDE lives on , an infinite-dimensional space of probability measures. Buckdahn, Li, Peng and Rainer (arXiv:1407.1215, Ann. Probab. 2017) prove that this value function is the unique classical solution of its PDE, using the derivative with respect to measures introduced by P.-L. Lions in his Collège de France lectures.
Timeline. McKean (1966) introduced the equations; Sznitman (1991) gave the propagation-of-chaos theory. Buckdahn, Djehiche, Li and Peng (2009) and Buckdahn, Li and Peng (2009) studied mean-field backward SDEs and the associated PDEs in a form where the law enters only through the coefficients. Lions (2007–2012 lectures, notes by Cardaliaguet 2013) introduced differentiation on through lifts to . Carmona and Delarue (arXiv:1303.5835, 2013; arXiv:1404.4694, 2014) developed the Itô formula on the Wasserstein space and the master equation for mean-field games. The present paper (2014) proves the classical-solution result for the decoupled forward equation under second-order regularity of the coefficients in .
Let be a complete probability space carrying a -dimensional Brownian motion , let , and let be a sub--field independent of that is rich: every is the law of some . Here is the set of probability measures with finite second moment, with the 2-Wasserstein distance , the infimum over couplings of and . The filtration is .
Given Lipschitz coefficients , , a time , and , the processes and solve on
The second process depends on only through , so for the value function is a function on .
A function has Lions derivative if its lift on is Fréchet differentiable with derivative . The classes and ask for one or two such derivatives (together with derivatives in and in the extra variable ), all bounded and Lipschitz. Hypothesis (H.2) asks that and be bounded and that every component be in .
Under (H.2) and , belongs to and is the unique solution in that class of
The goal also records that does not depend on the choice of with a given law.
In the order the proof uses them: the second-order expansion on (Lemma 2.1); symmetry of mixed derivatives (Lemma 4.1); the substitution identity and flow property (3.4)–(3.5); the stability estimate (Lemma 3.1) and its consequence that depends only on (Remark 3.1); first- and second-order regularity of in (Lemmas 5.1, 5.2) and in (Lemma 6.1); the mean-field Itô formulas (Proposition 6.1, Theorem 6.1); the martingale identity (6.15); and uniqueness (6.19)–(6.20). A companion theorem states the existence and pathwise uniqueness of solutions of both SDEs under Lipschitz coefficients.
The result is a Feynman–Kac representation on the Wasserstein space: it identifies the expectation functional of a McKean–Vlasov diffusion with the unique classical solution of a second-order PDE in , of the type that appears as the master equation of mean-field games and as the dynamic-programming equation of mean-field control. It gives a mean-field Itô formula for functions of the state and of the law, which is the basic tool for verification arguments in these problems.
All results of the mission are proved in the paper, which takes the well-posedness of the SDEs from Carmona and Delarue. None is formalized: the platform has the Itô integral as an definition, but no Itô isometry, no Burkholder–Davis–Gundy inequality, no SDE existence theorem and no Itô formula (the classical Itô formula is posed separately as an open goal). Formalizing the mission produces a calculus on in Lean, together with existence, stability and flow results for McKean–Vlasov equations.
The obvious route, differentiating in by the chain rule, fails because is not a map between finite-dimensional spaces: the measure derivative of requires Fréchet differentiability of in , the identification of the derivative through a family of auxiliary linear SDEs indexed by a point , and estimates uniform in . A second difficulty is that the second-order expansion on has remainder of order , not , so the Itô formula is not a direct Taylor argument in and needs a partition argument with control of each increment. A third is regularity in time: is differentiable in only after the Itô formula has been applied to , and the time derivative must again be bounded and Hölder. The paper writes its proofs for and and leaves some estimates to the reader, so a solver must supply them.
Time is ℝ≥0, is EuclideanSpace ℝ (Fin d), measures are Measure (E d), and every condition on a measure argument is quantified over only. is the real value of the published WassersteinDRO.Duality.wassersteinDistance 2, finite on . Brownian motion, the Brownian filtration and the Itô integral are the published Peng1990.SMP objects, and the null sets are ReflectedBSDE.Existence.nullSigma. The standing assumptions of §3 are hypotheses of every statement: completeness, , independence of and , richness of , and the Lipschitz condition (stated even where (H.2) implies it). Matrices carry the Frobenius norm.
Solutions of (3.1) and (3.2) are processes in satisfying the integral equation at every almost surely, with for Itô integrals of . Statements about take solution families as hypotheses; the companion well-posedness theorem states that such families exist, and a sanity file shows that zero coefficients with constant solutions and satisfy every hypothesis. The decoupled equation takes a random initial value, so (3.4) needs no measurable selection in .
Derivatives in , and are genuine (HasGradientAt; HasDerivWithinAt on , one-sided at the ends). Derivatives in are witness functions with the Fréchet property of the lift, the lift being taken on the paper's own rich space; this rules out the trivializing reading in which every function is differentiable because the underlying space carries only Dirac laws. The subscript bounds the derivatives, not the function, except that (H.1)/(H.2) also require and themselves to be bounded on : this is the of (H.1) ii), read uniformly in as the paper's proofs use it, and without it the bounded time derivative of fails (e.g. ). The class additionally requires the derivatives entering the Itô formula to be jointly continuous in for ; this is the reading of the letter , and satisfies it. over an independent copy is the integral against the corresponding law. Where the page writes or without , the bounded classes the paper defines are used. The uniqueness statement ranges over every function of the class with its own derivatives.
A complete development needs the Itô isometry and BDG inequality for the published integral, Gronwall's inequality, strong existence for McKean–Vlasov SDEs, -differentiability of SDE solutions with respect to the initial condition, and a classical multidimensional Itô formula. The Lions-derivative calculus and the Wasserstein estimates are reusable for any mean-field mission. Contributions to any of these pieces are welcome.
A cap in an affine or projective space over a finite field is a set of points no three of which are collinear; a cap is complete when it is maximal with respect to inclusion, so that every point outside it lies on a line through two of its points. Caps are closely connected with error-correcting codes: projective caps can serve as parity-check columns for linear codes with minimum distance at least 4. Constructing small complete caps explicitly is a long-standing question in finite geometry; Giulietti's survey collects the known families.
Counting the lines through pairs of points gives the trivial lower bound
for the size of a complete cap in a Galois space of dimension and order . A short timeline:
Let and let be the field with elements. The affine space has as points the vectors ; three points are collinear when they lie on a common affine line over .
For an additive subgroup of , is the set of points whose coordinate vectors lie in . A translation cap is a cap of the form . By Giulietti, Proposition 2.5, for a translation cap has at most points; one attaining this bound is a maximal translation cap.
On the projective side, let , so that . An -subspace of (an additive subgroup) of -dimension , the rank, defines the -linear set . It is scattered when every point meets in exactly , i.e. has weight one. A scattered linear set has rank at most (Blokhuis–Lavrauw); one of rank in the plane is called maximum.
For , even, and even, there is a complete cap in with
The exponent is an integer because is even.
Theorem 1.3 shows that the trivial bound (1) is sharp up to the factor in even dimension for every even square , extending to even dimension what the constructions of Segre and Pambianco–Storme give in odd dimension. The construction supplies caps near the elementary size lower bound in a parameter range where the paper reports no comparably small infinite family. Remark 4.8 of the paper extends the construction to complete caps of comparable size in . The proof also establishes Proposition 4.3, a dictionary between scattered -linear sets and translation caps, so that any new maximum scattered linear set yields new small complete caps.
The result is proved on paper; no machine-checked proof of it or of the cited results of [6] (Lemmas 4.5, 4.6 and the bound of Prop. 2.5, whose proofs are not in this paper) is known to exist. The mission produces a formal statement of Theorem 1.3, the cap–linear set correspondence, and formal statements of the three results the paper imports from [6].
Assembling Proposition 4.7 from the milestones is short. The difficulty lies in the inputs. The doubling construction requires showing that every point of outside lies on a secant, which uses the maximality in a counting argument; it is cited from [6], not proved in the paper. The existence of a maximum scattered linear set in is the deep input: Lemma 2.8 needs a bound on the value set of a non-permutation polynomial (Turnwald) and a point count on a plane curve over . A tempting shortcut, taking any maximal cap obtained by greedy extension, gives a complete cap of unknown and generally much larger size; the content of the theorem is the exact size.
Fin r → K for a finite field with ; collinearity is Mathlib's affine Collinear K, over itself. A complete cap is quantified against every point of .Set.ncard. The goal's size is written with natural-number division, exact because is even; maximality of a translation cap is the squared form , and the [6] bound is .Welcome contributions: a general library of caps and translation caps in ; the scattered-linear-set/translation-cap dictionary; a formalization of the doubling construction of [6]; transport of the -model of Theorem 2.10 to coordinates . The linear-set definitions mirror those of the companion mission on scattered linear sets and are reusable there.
A decision maker wants to choose in a compact set to minimize an expected cost , but the distribution of is unknown; only independent samples are available. The standard remedy, minimizing the cost under the empirical distribution, is known to produce decisions whose realized cost exceeds the in-sample estimate: the "optimizer's curse" of decision analysis (Smith and Winkler, 2006) and overfitting in statistics. Distributionally robust optimization (DRO) replaces the empirical distribution by a worst case over a set of nearby distributions. Many such sets have been proposed, and the question of which one is best has no answer unless "best" is made precise.
Van Parys, Mohajerin Esfahani and Kuhn (arXiv:1704.04118v3, published in Management Science 67(6), 2021) give such a precise meaning. They ask for the least conservative data-driven decision rule whose out-of-sample disappointment decays exponentially at a prescribed rate under every possible data-generating distribution, and they prove that DRO over a relative-entropy ball of radius is that rule. This mission formalizes the prescription half of the result (Theorem 7 of the paper), in which decisions, not only cost estimates, are optimized. The prediction half (Theorem 4) is the subject of mission 1 of this series, and the extension to continuous state spaces (Theorem 10) is mission 3. All page and result numbers below refer to the arXiv version v3 (22 Dec 2019).
The random parameter takes values in a finite set . The model class is the probability simplex with the topology inherited from . The cost is continuous in for each , and . From a sample path the decision maker forms the empirical distribution . When the samples are drawn independently from , the probability of an event about is written .
A data-driven predictor is a continuous function ; estimates . A function is quasi-continuous if for every , every and every neighbourhood of there is a non-empty open on which (the set need not contain ). A data-driven prescriptor induced by is a quasi-continuous with for every . The family consists of all such pairs .
The prescription disappointment of a pair under a model is
the probability that the true cost of the prescribed decision exceeds its in-sample estimate. Pairs are ordered by their in-sample optimal values: iff for all . Problem (6) of the paper is the vector optimization problem
and a pair is strongly optimal if it is feasible and every feasible pair.
The relative entropy is , with and . The distributionally robust predictor and prescriptor are
with quasi-continuous (Definition 7). The estimator realization is the first argument of , the reverse of the usual Kullback–Leibler ball.
The proof of Theorem 7 also uses results posed as milestones of mission 1 of this series: the large deviation bounds of Theorem 1, (7a) and (7b) (p. 12); the continuity of (Proposition 3, p. 16); the inclusion of the disappointment set in from the proof of Theorem 3 (pp. 16–17); and the construction of a perturbed model with from the proof of Theorem 4 ((14)–(16), pp. 17–18). They are not posed again here.
Theorem 7 says that no decision rule whose prescriptions disappoint with probability decaying at rate can report a smaller in-sample optimal value than relative-entropy DRO, at any realization of the data. It turns a modelling choice (which ambiguity set to use) into a consequence of a statistical requirement, and it identifies the radius of the ball with the decay rate of the out-of-sample disappointment. Theorem 8 complements this with a finite-sample bound that holds before any data are observed.
The theorem is proved in the paper, and its proof is short given the earlier results; there is no machine-checked version. A complete formalization adds a finite-alphabet Sanov theorem with the infinity convention of the relative entropy, an elementary theory of quasi-continuous functions on the simplex (density of continuity points, selection of quasi-continuous minimizers from an upper semicontinuous arg-min map), and Berge's maximum theorem in the form used here. The paper itself only sketches several steps (the construction of "exactly as in the proof of Theorem 4", and the proof of Theorem 8 is omitted).
Theorem 7 does not follow from the predictor result (Theorem 4). The order compares only the in-sample optimal values, so a competing pair may use a predictor that lies below away from its own minimizers, and the pointwise comparison of predictors that settles Theorem 4 says nothing about such a pair. What the data can detect is governed by the large deviations of , which only see sets with non-empty interior in , while the competitor's prescriptor need not be continuous. Without quasi-continuity of the argument breaks: a selector that jumps to a cheaper decision only on a set with empty interior is invisible to the data, and the theorem is not claimed for such selectors. The existence half (Proposition 4) rests on a selection theorem for upper semicontinuous set-valued maps on Baire spaces (Matejdes 1987, Corollary 4), for which there is no Mathlib counterpart.
Lean conventions:
Fin d, and is the subtype of stdSimplex ℝ (Fin d) with its subspace topology.EuclideanSpace ℝ (Fin n), with decisions in the subtype ↥X and the Euclidean distance; is continuous in for each . These are the standing assumptions of §2 (p. 5).EReal, equal to unless .Ruled out:
Real.log would treat a probability that vanishes as having rate .Each of these makes the statement different from the paper's, and none is used.
Reusable infrastructure includes quasi-continuity (with the Bledsoe density theorem), Berge's maximum theorem for the minimum value, and finite-alphabet large deviations for empirical distributions. Contributions of any of these, or of the mission 1 milestones, are welcome.
Adam (Kingma and Ba, 2015) is the default optimizer for training neural networks. At step it keeps an exponential moving average of stochastic gradients and an exponential moving average of their squared coordinates, corrects both for their initialization at zero (the bias correction or debiasing step), and moves the iterate by coordinatewise. Despite its use, its convergence on nonconvex objectives was poorly understood when Barakat and Bianchi wrote their paper: Reddi, Kale and Kumar (2018) exhibited convex online problems on which constant-parameter Adam fails to converge, and earlier analyses either dropped the bias correction or replaced Adam by a modified algorithm.
Barakat and Bianchi (arXiv:1810.02263v4, SIAM J. Math. Data Sci. 2021) study Adam through the ODE method: as the step size with and , the interpolated iterates follow a non-autonomous ordinary differential equation, the continuous-time version of Adam. This mission formalizes their convergence theorem for that ODE (Theorem 3.2): trajectories started as Adam is started, with zero moment estimates, approach the critical points of the objective.
Let be continuously differentiable with locally Lipschitz gradient , and let be locally Lipschitz. In the paper is the objective and the coordinatewise second moment of the stochastic gradient; §7 only uses the two properties above. Assume is coercive ( as ) and coordinatewise for every . Fix constants with .
The state is , and is the part where . All vector operations are coordinatewise. The Adam field (3.3) is, for ,
and (ODE) is . The factors and are the continuous-time bias corrections; they blow up as . A global solution with initial condition is a continuous , continuously differentiable on , satisfying (ODE) for every , with . The critical set is .
The proof passes through the autonomous field , its semiflow on , and the notions of equilibrium point, strict Lyapunov function and asymptotic pseudotrajectory (APT) of a semiflow.
Assume in addition that has empty interior in . For every global solution with initial condition , the set is non-empty and
The theorem does not claim that converges; convergence to a single critical point needs a Łojasiewicz condition (Theorem 3.4, a separate mission).
The milestones are the numbered results of §7.1–7.3 used in the proof, in the order the proof uses them: positivity of along solutions (Lemma 7.4); decrease of along (Lemma 7.5, autonomous part); compactness of trajectories (Propositions 7.6, 7.7) and lower bounds on (Lemma 7.8); well-posedness of the autonomous system and its semiflow (Proposition 7.13); the abstract limit-set theorem for APTs (Proposition 7.14, quoted from Benaïm); the strict Lyapunov function (Proposition 7.15); and the APT property of the (ODE) solution (Proposition 7.17).
Theorem 3.2 is the deterministic core of the paper's analysis of Adam. Combined with the paper's tracking result (constant-step Adam converges in probability to the ODE solution as , Theorem 4.3) it says that for small steps Adam's iterates spend their time near critical points of ; it is also the input of the decreasing-step almost-sure convergence theorem (Theorem 5.2) and of the convergence-rate theorem (Theorem 3.4), which both rely on the same Lyapunov function and limit-set argument. The condition under which the Lyapunov function decreases is satisfied by the default parameters , .
The result is proved in the paper; to the best of current knowledge it has not been machine-checked. The mission produces a formal proof of the theorem, and reusable formal statements about semiflows on metric spaces: strict Lyapunov functions, and the limit set of a relatively compact asymptotic pseudotrajectory.
The obvious route is to show that decreases and apply LaSalle's invariance principle. This fails on two counts. First, (ODE) is non-autonomous, and LaSalle's principle is a statement about autonomous systems: the derivative of along the flow vanishes only on a set that depends on . Second, the field is singular: blows up at and is not Lipschitz near , because of , so neither existence and uniqueness nor continuous dependence on initial data come from standard theorems. The energy of the autonomous limit is a Lyapunov function but not a strict one: it is constant along some non-equilibrium orbits, so non-increase of an energy alone does not identify the limit points.
Each block lives in EuclideanSpace ℝ (Fin d) and is their product; Mathlib's norm on the product is the maximum of the three Euclidean norms, which is equivalent to the Euclidean norm of and changes no statement. and are abstract, with the hypotheses of the paper's §7 (Assumptions 7.1, 7.2, 2.3, 2.4); this generality implies the printed theorem for the , of (2.2). Solutions are maps constrained only on (or ), and the equation is required at only. The field is extended off by , as on p. 12 of the paper. A semiflow is Mathlib's Flow ℝ≥0 M, on the subtype or on a compact subset of it. The semiflow in the milestones is always assumed to be the flow of , never an arbitrary flow. The APT and limit-set definitions are the published StochApproxDyn.LimitSet ones.
The goal is stated for every global solution of the specific field (3.3), and keeps " is non-empty" in the conclusion. A statement about some solution of an unspecified field, or with " has empty interior" strengthened to " is finite", is a different theorem and does not count.
A complete development needs: Grönwall-type comparison and chain-rule arguments along trajectories; well-posedness of the autonomous system on and continuity of its flow; and the limit-set theory of asymptotic pseudotrajectories (Benaïm 1999), adapted to strict Lyapunov functions in the paper's sense. The last part is independent of Adam and reusable in stochastic approximation. Contributions to any milestone are welcome; Propositions 7.13 and 7.14 are the largest pieces of infrastructure.
In ordinary statistical learning, a hypothesis is chosen from training data drawn from a distribution and judged by its risk under that same . In practice the test distribution often differs from the training one: covariate shift, domain drift, adversarial perturbation of inputs. Distributionally robust learning replaces the risk at by the worst risk over a neighbourhood of . When the neighbourhood is a ball in a Wasserstein distance, the perturbed distributions may move mass to nearby points of the instance space rather than only reweight the observed ones, which makes the model a natural description of small domain drifts and adversarial perturbations (Esfahani–Kuhn 2018, Gao–Kleywegt 2016, Sinha–Namkoong–Duchi 2018).
Lee and Raginsky (NeurIPS 2018) asked whether minimising the empirical version of this worst-case risk learns: does the empirical minimiser come close, in worst-case risk, to the best hypothesis of the class, at the usual rate? Their §3.2 answers yes when every hypothesis is uniformly Lipschitz. Their §3.3, the subject of this mission, removes that assumption: one hypothesis with controlled growth is enough.
The instance space is a Polish metric space with metric and Borel -algebra; fix . For Borel probability measures on , the -Wasserstein distance is
the infimum over couplings of and . For a radius , is the Wasserstein ball around .
A hypothesis is a function , read as a loss; a hypothesis class is a set of them. The risk of under is . The local worst-case risk and the local minimax risk are
Given i.i.d. samples with empirical distribution , the local minimax ERM is
The standing assumptions are:
The complexity of is measured by the entropy integral , where is the covering number of in the uniform norm.
Under Assumptions 1, 2 and 4, for every , with probability at least ,
The goal carries the paper's constants. The mission does not ask for sharper constants; a proof of the stated bound closes it.
The result. Theorem 3 is a generalisation guarantee for Wasserstein distributionally robust ERM that needs no uniform smoothness of the class. The uniformly Lipschitz assumption of the companion Theorem 2 fails for most classes of interest when : a function with is constant (p. 6). Assumption 4 holds, for example, for regression with quadratic loss whenever the predictor class contains the zero predictor (p. 6). The second term of (11) decreases as grows, which quantifies how a larger ambiguity set screens out non-smooth hypotheses (Remark 4).
Formalizing it. The theorem has a published pen-and-paper proof (Appendix C.5 of the arXiv version); it has no machine-checked proof. A formalization produces machine-checked statements of the dual characterisation of Wasserstein worst-case risk on a bounded Polish space, of a symmetrization-plus-McDiarmid uniform deviation bound for a parametrised class, and of a Dudley-entropy bound on a product class. The proof (C.5) on p. 16 starts from an achiever of , which need not exist; the goal is stated without that assumption, so a complete proof also handles the infimum.
The obvious argument decomposes the excess risk through and bounds by a uniform deviation over . That step fails: is a supremum over a ball of measures, not an expectation, so it is not an empirical process in . Passing to the dual makes it one, but the dual multiplier depends on the sample and has no a priori bound, so the class over all is too large. Without uniform smoothness of there is no obvious a priori bound on , and the entropy of the resulting two-parameter class must still be controlled at rate . Strong duality itself (Proposition 4) needs the existence of optimal couplings and a measurable-selection argument on a Polish space; it is not in Mathlib.
MetricSpace with BorelSpace and PolishSpace instances; Assumption 1 is Bornology.IsBounded (Set.univ : Set 𝒵), and is Metric.diam Set.univ. Throughout, and (the paper's standing choice, p. 3).WassersteinLinOpt.Ball.wassersteinDist and wassersteinBall, which range over all Borel probability measures; on a bounded space this equals the paper's ball.The following formalizations would trivialize the goal and are ruled out: a bound for each fixed in place of ; an defined by Classical.choose of an unproved existence; a supremum over all measures instead of over the ball; and the real conversion of an infinite .
The infrastructure is reusable beyond this mission: Wasserstein strong duality on Polish spaces (Proposition 4 specialises the general optimal-transport duality of Blanchet–Murthy 2019, whose transport-plan form is a proved theorem on the platform as ModelRiskOT.Duality.theorem_1); Dudley's entropy bound for sub-Gaussian processes indexed by infinite classes; and McDiarmid's inequality for suprema of empirical processes. Contributions of these general tools, as separate theorems, are welcome. Source: the arXiv v2 preprint, which is the NeurIPS 2018 camera-ready text followed by the supplementary appendices.
A decision based on observed data can change when the data law differs from the one used to choose it. Distributionally robust optimization addresses this by evaluating each decision against a family of nearby probability laws. Optimal transport gives one way to define “nearby”: a candidate law is admissible when probability mass can be moved from the baseline law at a bounded expected cost. For a linear decision rule, the resulting worst-case expectation is usually harder to optimize than an ordinary sample-average loss. Blanchet, Murthy, and Zhang identify a dual objective whose variables are the decision vector and a scalar transport multiplier, then study its curvature near the multipliers that actually minimize it (Blanchet–Murthy–Zhang, 2022).
The paper proves that this dual objective is jointly strongly convex on a specified region for sufficiently small transport radius. This matters because ordinary convexity allows flat directions in the joint decision–multiplier space. The joint lower Hessian bound gives local curvature in every direction with one positive modulus that remains independent of the radius apart from the paper's explicit factor (Theorem 4, p. 11).
Let have a baseline probability law , and let a decision be a vector in a nonempty compact convex set . The loss of a possible outcome is for a convex function . A state-dependent positive-definite matrix sets the cost of moving mass from to :
Assumption 1 requires this cost to be lower semicontinuous and the eigenvalues of to lie between positive constants and for -almost every . Assumption 2 requires at most quadratic growth of and a finite fourth moment of . The ambiguity radius is positive (Assumptions 1–2, pp. 9–10).
The paper's dual objective is an expectation under the known law . Write . For a scalar and an auxiliary scalar , set
This value may be . Under the paper's duality conditions, minimizing over gives the worst-case loss at (Theorem 1 and (7), p. 10).
Assumption 3 bounds above by and excludes an almost surely zero for each . Assumption 4 makes compact. Lemma 6 supplies positive constants bounding uniformly over . With , the constants are those of (28), and
Theorem 3 first gives a bounded Hessian on and a positive lower bound on its block when , with the explicit from p. 36. The goal, Theorem 4, adds Assumption 5: is locally strongly convex and, at each , the loss derivative and the linear score are simultaneously separated from zero with positive probability. It asserts the joint bound
The order of the quantifiers is part of the target: works for every sufficiently small (Theorems 3–4, p. 11).
The Hessian bound makes the joint dual parameters locally identifiable by curvature on a region that contains every dual optimizer. In the paper, this structure also underlies the analysis of algorithms and of how the optimizer changes with the transport radius (Proposition 1, p. 11; §3 and §5.4). Theorem 4 is already proved in the paper; this mission asks for its machine-checked formalization, together with the stated bounds on multipliers, the maximizing scalar, and the intermediate curvature results. The general optimal-transport integral used here already has a published Prove2Me definition from Blanchet and Murthy's earlier model-risk work. The new definitions specify this paper's Mahalanobis model, regions, and smoothness assumptions.
Convexity alone gives only a nonnegative Hessian; it cannot produce a strictly positive joint lower bound. Even curvature of does not by itself control directions that combine a change in with a change in . The inner supremum over can become infinite outside its effective domain, while at its maximizer ceases to be unique. The theorem therefore needs a region where the dual objective is finite and differentiable and a probabilistic condition that prevents the relevant score and derivative from vanishing together. The target keeps the actual scale instead of settling for a radius-dependent positive constant (§2.2.2 and Remark 4, pp. 10–12, 39).
Lean uses EuclideanSpace ℝ (Fin d) for , a Borel probability measure for , and EReal for and the inner supremum. The reused extended-real integral records the and cases; the Hessian is taken only where is finite on a neighborhood and its real representative is differentiable there. Quadratic Hessian forms use , since Lean's product norm is not the paper's Euclidean norm. The compact set is explicitly nonempty, and the positive ambiguity radius is quantified inside the goal so that and are uniform in . Theorem 3 additionally assumes for the proof's explicit formula for : nonempty compact would make that formula zero. Assumption 5 already gives in the goal.
The goal retains Assumption 5's per-decision quantifiers. That assumption itself excludes : its strict score event is empty at . Intermediate statements where the printed wording includes but the claim fails there state explicitly. Lemma 5 also states the differentiability and positive-multiplier conditions needed for its derivative and division. Proposition 9(b)'s printed strict curvature-margin inequality is corrected to the nonstrict inequality derived in its proof; its original wording is preserved in the milestone quotation. The claims are about the expectation , with independent of , rather than a pointwise or merely convex substitute.
A complete development needs measurable extended-real integration, the matrix quadratic form and its inverse, almost-everywhere spectral bounds, differentiability under an expectation, and Hessian estimates for an optimized scalar. The transport integral, the assumptions and constants, and the multiplier bounds are intended as reusable interfaces for the companion missions. Contributions that close the listed lemmas or add the paper's omitted second-order kernel formula are within scope.
A linear two-stage stochastic program chooses a first-stage decision before an uncertain parameter is revealed, and pays the optimal value of a second-stage linear program once the realization is known. Such programs are the basic model of planning under uncertainty in operations research, and their computational complexity determines which solution methods can be expected to work. In 2006, Dyer and Stougie argued that linear two-stage stochastic programs with fixed recourse are #P-hard even when the random data follow independent uniform distributions. Hanasusanto, Kuhn and Wiesemann showed that this proof is not correct and gave a corrected one, which also covers approximate evaluation to sufficiently high accuracy; their note also shows that, when the second-stage constraint matrix itself depends on (random recourse), even finding an approximately optimal decision is strongly NP-hard.
This mission formalizes that last result, Theorem 4 of the note. The previous missions of the series treat the hardness of evaluating the expected recourse with fixed and with random recourse.
The Integer Feasibility Problem. An instance is an integer matrix and an integer vector such that the polytope lies in the unit cube . The question is whether some binary vector satisfies . This problem is strongly NP-hard (Garey and Johnson).
The second-stage problem. For a decision and a realization , write for the all-ones vector and consider
The coefficient of in each constraint depends on , which is what makes the recourse random.
Problem (11). With uniformly distributed on ,
The second stage is not feasible for every (the problem lacks relatively complete recourse), so a decision is feasible only if the second stage is feasible for every . Let be the infimum of the objective over feasible decisions. A feasible is -optimal if
The constant . Lemma 4 fixes with and for every row .
For an instance with nonempty polytope, , as above, , and any -optimal decision of (11),
This is the mathematical content of "determining an -optimal decision is strongly NP-hard whenever ": a single comparison of any approximate decision with a threshold answers the NP-hard question.
The result. Theorem 4 implies that, unless the problems in NP admit an efficient solution scheme, there is no fully polynomial-time approximation scheme for two-stage stochastic programs with random recourse, even with a one-dimensional first stage and a uniform distribution. Together with the #P-hardness results of the same note, it delimits what algorithms such as sample average approximation can guarantee once relatively complete recourse and fixed recourse are dropped.
Formalizing it. The theorem has a short published proof, but that proof leaves several conventions implicit: the index set of the constraint block, the meaning of first-stage feasibility, and the condition on when has a zero row. A machine-checked version fixes each of them and verifies that the claimed formula for is correct under the chosen reading. To our knowledge none of these statements has been formalized before. The objects are elementary (finite-dimensional linear programs, a set integral on the unit cube), and the second-stage solution and rounding lemma are reusable for related reductions from integer feasibility.
The individual steps are short; the difficulty is bookkeeping across three layers. The second stage is an optimisation over whose feasibility depends on the sign pattern of ; the first stage requires a supremum over a polytope to be attained (compactness), and the expected recourse to be the same integral for all feasible decisions (integrability of a piecewise-defined value function over the cube). The tempting shortcut, reading off feasibility from the value of , fails: an infeasible linear program has no meaningful value, and treating it as cost would make every decision look optimal. Similarly, an almost-sure notion of feasibility looks natural for a stochastic program but invalidates the formula for whenever the polytope has measure zero, as it typically does for integer feasibility instances written with equalities.
All objects live in SPHardness.IntFeas. Vectors are functions on Fin n and Fin m; and are integer and are cast to , and integrality is kept because Lemma 4 depends on it. The uniform law on is Lebesgue measure restricted to the cube (volume ); expectations are set integrals. The recourse value, and are sInf/sSup in , and second-stage feasibility, first-stage feasibility and -optimality are separate predicates, so no statement depends on the junk value of an empty infimum.
Pinned readings and added conventions:
Strong NP-hardness, the FPTAS consequence, running times and encoding lengths are not formalized; the goal is the correctness of the reduction. A statement in which ranges over arbitrary reals satisfying a hypothesised identity, rather than over -optimal decisions of the program (11) built from , would be trivial and is ruled out: every object in the goal is defined from the instance.
Contributions welcome: proofs of the milestones, in particular measurability and integrability of the recourse function on the cube and attainment of , which are reusable for other piecewise-linear recourse functions.
The ℓ1-regularized least squares problem (the Lasso, or basis pursuit denoising) is the model problem of compressed sensing and sparse inverse problems: given a matrix , data and a weight , one seeks a vector that fits while having few nonzero entries. The standard first-order method for it is the iterative shrinkage thresholding algorithm (ISTA), a forward-backward splitting scheme whose backward step is componentwise soft thresholding. Each iteration costs two matrix–vector products, which is why ISTA and its variants are used on problems far too large for interior-point methods.
The classical complexity guarantee for ISTA is , the rate of the proximal gradient method on any convex composite problem (Beck–Teboulle 2009). ISTA itself goes back to Daubechies–Defrise–De Mol 2004, and its link with forward-backward splitting to Combettes–Wajs 2005. An asymptotic linear rate was known, with an explanation through partial smoothness (Liang–Fadili–Peyré), but there was no global, explicit, non-asymptotic bound. Bolte, Nguyen, Peypouquet and Suter (arXiv:1510.08234v3, Math. Program. 2017) derive such a bound from two ingredients: an error bound for the Lasso objective on balls, with a constant written through a Hoffman constant, and their general theory turning a Kurdyka–Łojasiewicz (KL) inequality into complexity bounds for descent methods.
Write with the Euclidean norm , and . For a matrix , is its spectral norm, the operator norm from to with Euclidean norms. The objective is
with and . Put and . Then is convex with gradient , Lipschitz with constant .
Given stepsizes with and any , ISTA is
where is the minimizer of . More generally, in a real Hilbert space with proper, lower semicontinuous and convex and convex with -Lipschitz gradient, the forward-backward method takes to be a minimizer of .
A sequence is a subgradient descent sequence for a convex with constants if and, for every ,
With , has the KL property on a set with desingularizing function if for every such and every .
A number is a Hoffman constant for a pair of matrices if, for every right-hand side with and intersecting, for all .
Put and , and . Let be such that whenever . Then ISTA converges to some and
The result. The theorem replaces the sublinear guarantee of ISTA by a global linear rate with explicit constants depending only on , , , the stepsizes, and a Hoffman constant. It also bounds the distance of the iterates to the limit, not only the objective gap, and needs no uniqueness of the minimizer. Through , it shows that conditioning of the objective near its minimizers, rather than strong convexity, governs the complexity of the method. The general machinery behind it (Theorem 16 of the paper, a separate mission of this series) applies to any method producing subgradient descent sequences.
Formalizing it. The result is proved on paper, and no machine-checked proof of it or of its ingredients is known. A formalization would give a verified linear-rate certificate for a widely deployed algorithm. It would also yield reusable lemmas: the descent and relative-error properties of the forward-backward method in a Hilbert space, and quadratic growth for the Lasso on balls. Lemma 10 rests on an external result (Beck–Shtern, Lemma 2.5) that a complete development must also formalize.
The Lasso objective is not strongly convex when has a nontrivial kernel, and its minimizer need not be unique. The textbook argument for linear convergence of proximal gradient methods, which uses strong convexity, therefore does not apply. Quadratic growth is the substitute, but it holds only on bounded sets, with a constant degrading in the radius. The analysis must therefore show that the iterates stay in a fixed ball and keep track of how the growth constant enters the rate. Deriving the explicit requires recasting the problem as a quadratic program over a polyhedron with facets and invoking a Hoffman-type error bound for it.
Citations refer to the arXiv preprint arXiv:1510.08234v3 (20 July 2016), with its numbering and pages; the journal version is not used. is EuclideanSpace ℝ (Fin n) and matrices act through Matrix.toEuclideanLin. Spectral norms are operator norms of the associated continuous linear maps, never Mathlib's default entrywise matrix norm. The data vector, called in §3.2.1 of the paper and in §5.3, is throughout; is the constant of (H2).
Functions with values in are EReal-valued. The convex subdifferential, Γ₀, , the prox predicate and the class of desingularizing functions are reused from published platform definitions. The stepsize condition is written , so that (where ) is covered. is the infimum of , and is a real power.
In the goal, is any positive constant satisfying the error bound on the ball of radius ; it is not fixed to the value (10) and not existentially quantified. The constants are fixed formulas, never existentials. A statement with an unspecified constant, with chosen after the sequence, or with the stepsize hypothesis written as (unsatisfiable or vacuous at ) would trivialize the goal and is ruled out.
The subgradient-descent and KL notions duplicate, in the sub-namespace ErrBoundCplx.ISTA, those of the series' first mission, because draft items cannot import each other. Proofs of any milestone are welcome, in particular Proposition 13 and the KL consequence of Lemma 10, which are self-contained. A formalization of Hoffman's error bound and of Beck–Shtern's Lemma 2.5 is the main infrastructure Lemma 10 needs.
Linear sets are the main tool for building point sets with few intersection sizes in finite projective spaces: sets meeting every hyperplane, two-intersection sets, translation ovoids, and the geometric side of finite semifields and rank-metric codes (Polverino, 2010). Among them, scattered linear sets are those whose points all carry the smallest possible weight, and a scattered linear set of the largest possible rank is called maximum scattered. By Blokhuis and Lavrauw (2000), a maximum scattered linear set of of rank is a two-intersection set with respect to hyperplanes, so each one yields a two-weight code and a strongly regular graph.
Timeline.
Let be a prime power, , and let be an -dimensional vector space over ; has as points the spans of nonzero . An -subspace is a subset closed under addition and under multiplication by . It defines the -linear set
whose rank is . A linear set comes paired with , so every statement here is about . The weight of a point is , and is scattered when every point of has weight ; equivalently, for every nonzero ,
The plane construction (§2). Fix and the field with its subfields and . As an -space has dimension , so . For and an -linear the paper studies
with a monomial or a binomial . The relative norms enter the hypotheses.
For even and , in each of the cases (a) , ; (b) ; (c) , ,
Theorem 1.2 gives maximum scattered linear sets, and hence two-intersection sets, two-weight codes and strongly regular graphs, for infinitely many with odd, a regime where earlier existence results covered only a few values of . The case feeds the paper's second main result: scattered -linear sets of of rank are translation caps, from which complete caps of size in are built.
All statements are proved in the preprint; none has a machine-checked proof. Formalizing them requires a usable theory of subfields of a finite field as Frobenius fixed fields, relative norms and their images, linearized polynomials and their trace adjoints, and the passage between -dimension, cardinality and weight. Each of these is reusable for later work on linear sets, MRD codes and semifields.
The criterion of Proposition 2.2 reduces scatteredness to a polynomial system, but the system has to be solved for a specific . For the monomials this rests on the solvability of in , a norm condition interacting with the gcd hypotheses. For the binomial with , the existence of a suitable (Lemma 2.8) needs a value-set bound for non-permutation polynomials (Turnwald, 1995) and a point count on a plane curve. The higher-dimensional statement then needs the elementary bound for scattered to obtain the rank equivalence in Theorem 3.1. A tempting shortcut, taking or any small subspace, is scattered but has the wrong rank; the content is in the rank .
Fin r → K; the plane of §2 on itself.Distributionally robust optimization (DRO) replaces the expected loss of a decision under a baseline distribution by its worst case over all distributions that are close to . When closeness is measured by an optimal transport cost, the worst case over this infinite-dimensional ball has a one-dimensional dual: by Theorem 1 of Blanchet, Murthy and Zhang (arXiv:1810.02403v3, Math. Oper. Res. 47(2), 2022), building on the strong duality of Blanchet and Murthy (arXiv:1604.01446),
The robust problem thus becomes a joint minimization of the dual objective over . Whether that minimization is a convex program, and on which set the objective is finite, decides whether first-order methods such as the stochastic gradient schemes of the same paper apply at all. This mission formalizes the paper's answer, Theorem 2.
The data take values in with law , a Borel probability measure. A decision is a vector in a convex set , the loss is for , and is the transport budget.
The transport cost is the state-dependent Mahalanobis cost for a map from to positive definite matrices. Assumption 1: is lower semicontinuous (1a), and for -almost every , with (1b). Write .
Assumption 2: is convex, its growth exponent
is finite, and .
For , and define, as in display (7),
the robust loss , its set of maximizers , and the dual objective
The effective domain is , and with the threshold the paper sets and inside .
Under Assumptions 1 and 2, is proper and convex: on ; for each some has ; and for , ,
Lemma 3 is stated with constants depending only on (and the fixed data), as its proof produces them and as the paper's later arguments integrate bound (b) over .
Theorem 2 is the structural fact behind the paper's algorithms: with Theorem 1 it turns a minimax problem over probability measures into a convex minimization in real variables, on which the paper's strong convexity results (Theorems 3–5) and its stochastic gradient schemes are built. Lemma 1 identifies the effective domain up to its boundary, which tells an algorithm where the dual multiplier must lie, and Lemma 3 gives the growth control of the robust loss used throughout the appendix.
The results are proved in the paper; none of them has a machine-checked proof. The mission produces a Lean statement of the dual objective as an extended-real integral and of its convexity and properness, reusable by the other missions of this series (strong convexity near the optimizers, worst-case distributions, comparative statics in ), and contributions of formal proofs of the milestones and the goal.
The objective takes the value on part of its domain: Lemma 1(b) shows that below the threshold, so the naive reading " is a real convex function" is false, and convexity must be handled for functions with values in , including the conventions at the endpoints of the segment. Properness requires a bound on that is integrable in , so the constants of Lemma 3 must not depend on ; a bound that is only pointwise finite does not suffice. The identity (25) relates a supremum over to a supremum over through a change of the dual variable, and the two multipliers must be kept apart. Finally, the expectation in is an integral of an extended-real function whose measurability is not assumed but has to be derived from Assumption 1.
is EuclideanSpace ℝ (Fin d) and parameters live in EuclideanSpace ℝ (Fin d) × ℝ. is an EReal supremum; is the published ModelRiskOT.Duality.extIntegral, with lower Lebesgue integrals. is a real infimum and uses the real essential supremum; both are used only under Assumptions 1–2, which make them meaningful. Convexity of extended-real maps is written as the explicit inequality in EReal, since ConvexOn does not apply.
Standing assumptions carried by every statement: a probability measure, , convex (the paper's standing assumption). Conventions committed to: "for any " in Lemmas 1–2 is every , not almost every; Lemma 2 assumes only Assumption 1a and the convexity of ; the identity (25) is stated with the old multiplier written as ; the typo "" in Lemma 1 is read as ; the goal's "finite somewhere" is stated for each , so the goal is vacuous only when . The fourth-moment condition of Assumption 2 is kept as printed.
A trivializing formalization is ruled out: "proper" is not encoded as "finite everywhere" (false by Lemma 1(b)), and pointwise convexity of (Lemma 2) is a milestone, not the goal, which is about the expectation .
A complete development needs: positive definite matrices and the quadratic minimization behind (25); continuity of convex functions and growth bounds; lower Lebesgue integrals of extended-real functions and their monotonicity and additivity; measurability of a supremum over of continuous functions. The definitions layer is shared with the other four missions of this series. Proofs of any milestone and of the goal are welcome.