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?
The convex feasibility problem asks for a point in the intersection of closed convex sets. It underlies signal and image reconstruction, phase retrieval relaxations, and the constraint handling inside larger optimization methods. The workhorse algorithms are projection methods: the method of alternating projections (MAP), going back to von Neumann for subspaces, and the Douglas–Rachford and Peaceman–Rachford splitting schemes, which can be applied to the indicator, distance or squared-distance functions of the sets.
Without a regularity condition on how the sets meet, projection methods can converge arbitrarily slowly. Bounded linear regularity, an error bound saying that a point close to every set is close to their intersection, is the standard condition under which linear rates are obtained (Bauschke and Borwein, SIAM Review, 1996, doi:10.1137/S0036144593251710). Section 5 of D. Davis and W. Yin, Faster convergence rates of relaxed Peaceman–Rachford and ADMM under regularity assumptions (arXiv:1407.5210v3, Math. Oper. Res. 42(3), 2017) applies relaxed Peaceman–Rachford splitting (PRS) to the squared distance functions of two sets and proves that, under bounded linear regularity, the distance of the iterates to the intersection contracts by an explicit factor at every step, with step sizes and relaxation parameters allowed to vary between iterations. MAP is the special case of step size and relaxation .
Let be a real Hilbert space and closed convex sets with . For the distance function is , and is the metric projection, the nearest point of . The problem is modelled with
For the proximal map is the minimiser of , and the reflection is . With two step sizes, , and .
Given , step sizes and relaxation parameters , iteration (5.1) is
The pair is boundedly linearly regular (Definition 5.1) if for every there is such that
where is the open ball. The rate function is
Suppose is boundedly linearly regular, is generated by (5.1), every lies in , and on . Then for all
and if , the iterates converge to a point with
The milestones follow the paper's own argument: Proposition 5.1 Parts 2 and 3 (the gradient of and the closed form ); Proposition 5.2, the fundamental inequality specialised to squared distances; Propositions C.1 and C.2 (the fixed-point set of is , and the iterates are Fejér monotone for ); and the displays (5.5)–(5.7), (5.8), (5.10) and (5.11) of the proof of Theorem 5.1, ending with the one-step contraction at a single point.
With and , iteration (5.1) is MAP, , and under the assumptions of Theorem 5.1 it contracts the distance to by from the second iterate on, converging linearly to a point of the intersection.
Theorem 5.1 gives an explicit, iteration-wise linear rate for relaxed PRS on the two-set feasibility problem with step sizes and relaxation parameters that may change from step to step. Its specialisation, Corollary 5.1, recovers linear convergence of MAP under bounded linear regularity with rate , better than the derived in earlier work on cyclic projections. Remark 5.1 of the paper notes that Douglas–Rachford on indicator functions is a limiting case of the scheme as the step sizes grow, though the rate degenerates in that limit.
The results are proved in the paper; the proof of the convergence statement cites Bauschke–Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Theorem 5.12 (Fejér monotone sequences whose distance to a closed convex set decays converge strongly). No machine-checked proof of these statements was found on Prove2Me (search of 2026-10-07). A formalization produces a checked chain from the closed form of the prox of through the fundamental inequality to the linear rate, and with it reusable facts about squared distance functions, metric projections onto closed convex sets in Hilbert space, and Fejér monotone sequences.
The obvious argument would contract the distance to directly, but one PRS step measures only at and at the reflected point , never . Transferring the second distance back to costs a factor with , and only after that does the regularity inequality turn into . The fundamental inequality (5.2) itself rests on the prox-gradient calculus of the earlier sections, specialised to functions whose gradients are Lipschitz. Passing from a contracting distance to convergence of the iterates to one point needs Fejér monotonicity and a completeness argument; a contracting distance alone does not give a limit.
Everything lives in a real Hilbert space (InnerProductSpace ℝ H with CompleteSpace H); is Mathlib's Metric.infDist. The squared distance is viewed as an extended-real function so that the published proximal predicate ThreeOpSplitting.ConvexRates.IsProx applies, and prox maps are arbitrary maps satisfying it (unique here). Metric projections are maps satisfying the published RandomGradFree.Nonsmooth.IsMetricProjection. Step sizes and prox maps are indexed by the iteration. The hypotheses of the goal are: closed and convex with nonempty intersection; bounded linear regularity of the pair; ; ; iterates in an open ball on which the regularity inequality holds with . The range is Algorithm 1's standing assumption, used in the proof but not restated in (5.1). The condition is stated as a uniform bound on all rate factors. The product in (5.4) runs over ; the page prints the upper index , which claims an extra factor that the proof does not give. In the proof's (5.9)–(5.10) the page swaps and relative to (5.2); the milestone states the pairing that (5.2) produces. Corollary 5.1's improved rate is stated for , since it uses .
A trivializing formalization is ruled out: the goal mentions none of the proof's intermediate quantities, takes the prox maps as genuine minimisers of the squared-distance objective rather than chosen points, and measures distances to a nonempty intersection, so the junk value of infDist on the empty set never arises.
A complete development needs the closed form of , differentiability of , the fundamental inequality of the paper's §1 specialised to these functions, and the convergence theorem for Fejér monotone sequences. The last three are reusable well beyond this mission. Proofs of any milestone, and of Mathlib-level lemmas on metric projections, are welcome.
Manufacturers increasingly sell directly to consumers while continuing to supply independent retailers, a practice known as supply chain encroachment. The direct channel competes with the retailer for the same consumers, and the conventional advice for easing that conflict is to sell different products in the two channels. Ha, Long and Nasiry (MSOM 18(2), 2016; authors' manuscript SSRN 3970373) study this advice in a model where the manufacturer chooses product quality herself. This mission formalizes their Section 5: when the manufacturer may offer one quality directly and another through the retailer, which channel gets the better product, when is differentiation worth it, and who gains from encroachment.
The model builds on two lines of work. With exogenous quality, Arya, Mittendorf and Sappington (Marketing Science, 2007) showed that encroachment can benefit both firms, through a lower wholesale price. Vertical differentiation with a convex cost of quality goes back to Mussa and Rosen (JET, 1978), Moorthy (1988) and Motta (1993), where differentiation lets firms segment the market. The paper combines the two and finds that, once quality is endogenous, the retailer never gains.
A market of size consists of consumers with types uniformly distributed on ; a consumer of type obtains surplus from a product of quality at price . A manufacturer sells a product of quality through her direct channel and a product of quality , with quality ratio , through a retailer. Producing one unit of quality costs (); every unit sold directly costs a further direct selling cost ; the retailer's selling cost is .
With quantities (direct) and (retailer), the market-clearing prices are, for (direct channel carries the higher quality),
and for (retailer carries the higher quality)
The profits are and .
The game has three stages: (i) the manufacturer chooses a wholesale price , the quality and the ratio ; (ii) the retailer orders ; (iii) the manufacturer chooses . Solutions are subgame-perfect equilibria. The manufacturer encroaches when on the equilibrium path. Fixing gives the uniform-quality game of §4.1. The benchmark of §3.2 has no direct channel; its equilibrium profits are and .
In every subgame-perfect equilibrium with ,
The statement makes no assumption on which quality the manufacturer chooses, on the size of or on the form of the equilibrium; the constants are the benchmark's.
The §6.1 benchmark in which both qualities go through the retailer (, ), Proposition 5 (the win–lose outcome against that benchmark), and the existence of an equilibrium. The threshold milestones assert existence for each cost, so their conclusions have an equilibrium to describe.
Proposition 4(ii) says that letting the manufacturer differentiate quality across channels does not change who wins: the manufacturer still gains from encroachment and the retailer still loses, although one might expect the retailer to benefit from not facing an identical product. Proposition 3 adds that differentiation, when used, puts the higher quality in the direct channel, and Proposition 4(i) shows that for intermediate selling costs the manufacturer prefers no differentiation at all, contrary to the monopoly intuition that segmentation always pays. Proposition 5 shows the conclusion persists against a benchmark in which the retailer already carries a two-product line.
The results are proved in the paper, in part with numerical verification (e.g. the bounds on in the proof of Proposition 3, and the location of and ). None of them has been machine-checked. A formal development would turn these numerical steps into proofs and would leave a reusable, explicit model of a three-stage Stackelberg game with a vertically differentiated linear demand.
The equilibrium analysis is not a single concave program. Backward induction produces closed forms only on regions (the retailer's order must leave the manufacturer a positive direct quantity, and the retailer's quantity must stay positive), and the manufacturer's stage-1 problem is a comparison across these regions and across , and . The profit of low-quality encroachment, , involves a square root in , and the paper controls its critical points by a case analysis on polynomial derivatives with numerically located crossing points (pp. 39–40). The thresholds and are defined implicitly by the equality of maximized profits. Comparing the equilibrium profit with therefore requires bounding a maximum taken over a piecewise-defined family, not evaluating one formula.
The game is defined in QualityEncroach.Differ.Game. Quantities are restricted to be nonnegative; the wholesale price is unrestricted, as in the paper; qualities satisfy , . The price formulas are used for all nonnegative quantities, as in the paper; the case, which the paper says "can be derived similarly", is that derivation. The equilibrium notion is subgame perfection written in one-shot-deviation form at every history, on and off the path. Benchmark profits appear as the constants , (and , ); separate items derive them from the benchmark games. Threshold statements give and depending only on , assert equilibrium existence at every , and say nothing at , where the paper's statements disagree. Lemma 1 and Claim 1 are stated about the paper's reduced-form profits, defined by the displayed formulas in QualityEncroach.Differ.Reduced; the item reduced_profit_high links for to the game. Claim 1 retains and quantifies only over positive qualities, so no reduced form is evaluated at .
The goal is about subgame-perfect equilibria of the game, not about the reduced forms: a proof that only compares closed-form profits does not prove it without the milestones linking those forms to equilibrium play. The goal is not vacuous only if an equilibrium with exists; the companion spe_exists asserts existence.
Contributions are welcome at every level: the benchmark and the quantity subgame are routine calculus on quadratics; Lemma 1(i)–(ii) are one-variable sign analyses; Claim 1, Lemma 1(iii), Proposition 3 and the thresholds require the case analyses of the appendix.
Mean field games, introduced independently by Lasry and Lions (Mean field games, Jpn. J. Math. 2007) and by Huang, Malhamé and Caines (2006), describe the Nash equilibria of games with a very large number of symmetric players, each of whom reacts only to the empirical distribution of the others. In the limit, an equilibrium is a fixed point: a flow of population laws such that the optimal response of a single representative player to that flow reproduces it.
Existence of such fixed points is typically obtained by compactness, and says nothing about whether the equilibrium is determined by the data. Uniqueness matters for the use of the model: a unique equilibrium can be computed, approximated, and compared across parameters, while multiple equilibria raise a selection problem. Lasry and Lions showed by counterexamples that uniqueness fails in general, and identified a monotonicity condition on the population-dependent part of the reward under which it holds; outside that condition, uniqueness is typically available only for short horizons and Lipschitz coefficients.
Carmona and Lacker (arXiv:1307.1152v2, 2014; Ann. Appl. Probab. 25(3), 2015) set up a weak formulation of mean field games in which the controlled state is obtained from a fixed driftless diffusion by a Girsanov change of measure, so that the coefficients may be merely measurable in the state and path dependent. This mission formalizes their uniqueness theorem (Theorem 3.8): the Lasry–Lions argument carried out in the weak formulation, through backward stochastic differential equations.
Fix a horizon , a dimension , the path space with the sup norm, and a measurable . Write for the probability measures on with . A control set is a compact convex subset of a normed space, and is the set of probability measures on with the weak topology.
On a probability space carrying an initial state and an independent -dimensional Brownian motion , filtered by the augmented filtration of , let solve the driftless state equation , . The admissible controls are the progressively measurable -valued processes. For and the measure has density
under which has drift . For a flow the reward is
A pair is a solution of the MFG (Definition 3.4) if some maximizes over , , and for almost every .
The Hamiltonian is , with maximum over and maximizer set . Assumption (U) asks that (U.1) the maximizer is unique; (U.2) does not depend on ; (U.3) ; and (U.4) the Lasry–Lions monotonicity condition
The standing assumptions (S) of the paper (measurability, continuity in , nonsingular , bounded , a -growth bound on , and a separation of ) are in force throughout.
Under (S) and (U), if and are solutions of the MFG, then
Definition 3.4 constrains only for almost every , so this is the strongest identification possible.
Theorem 3.8, combined with the existence theorem of the same paper (Theorem 3.5, the first mission of this series), gives existence and uniqueness of the equilibrium (Corollary 3.9) for coefficients that are only measurable and path dependent in the state, under a monotonicity condition and no Lipschitz or small-horizon requirement. Uniqueness is also what makes the approximation result of the paper (Theorem 4.2, the third mission) refer to the equilibrium.
The result is proved in the paper. It has not been machine-checked; no mean field game uniqueness theorem in a weak or Girsanov formulation is formalized in Lean or Mathlib. The formal development would contain, as reusable parts, the Doléans exponential of a bounded Itô integrand as a probability density, the change of Brownian motion under it, the comparison principle for BSDEs with Lipschitz drivers, and the Lasry–Lions monotonicity argument.
The argument compares two equilibria through two different measures and . The direct Lasry–Lions computation, which differentiates a pairing of a Hamilton–Jacobi–Bellman solution with a Fokker–Planck solution, is not available: there is no PDE, and the value functions are only known through BSDEs. The proof needs (a) that an optimal control maximizes the Hamiltonian along the adjoint process — the necessity half of the BSDE optimality criterion, which the paper uses without a displayed proof; (b) the representation of under each of the two measures, which requires that the stochastic integrals be true martingales under the changed measures; and (c) turning a strict pointwise inequality on a set of positive -measure into a strict inequality of expectations, which uses the equivalence .
The Lean development lives in the namespace WeakMFG.Uniqueness and builds on the published definition Peng1990.SMP.Stochastic (Brownian motion, Itô integrals, Itô processes, BSDEs). Conventions:
A formalization whose hypotheses contain the conclusion is ruled out: the goal assumes only that the two pairs are solutions in the sense of Definition 3.4 — no BSDE solution, no Hamiltonian maximization, no equality of densities is assumed. Uniqueness of is stated almost everywhere in time, and nowhere is equality of the two optimal controls as functions asked for.
Contributions welcome: the Doléans exponential and Girsanov's theorem for bounded drifts in the Itô layer, existence and comparison for Lipschitz BSDEs on a filtration enlarged by an independent initial condition, and the measurable maximum theorem for the Hamiltonian. These are reusable beyond this mission, in particular by the other two missions of the series.
How fast does the empirical measure of an i.i.d. sample approach the law it is drawn from? When distance is measured by optimal transport, the answer enters the analysis of statistical estimators built from empirical distributions, quantization of probability measures, Monte Carlo and particle approximations of nonlinear PDEs (McKean–Vlasov systems), and the radius calibration of Wasserstein ambiguity sets in data-driven distributionally robust optimization.
The question has a long history. Ajtai, Komlós and Tusnády (1984) found the rate for uniform samples in the unit square. Horowitz–Karandikar (1994), Rachev–Rüschendorf and Mischler–Mouhot gave bounds that were far from optimal outside the compactly supported case. Boissard and Le Gouic (2014) and Dereich, Scheutzow and Schottstedt (2013) introduced multiscale couplings; the latter obtained sharp moment bounds for , , under a moment condition . Fournier and Guillin (arXiv:1312.2128, Probab. Theory Relat. Fields 162, 2015) extended these bounds to every , every dimension and every moment order , with explicit dependence on the moment.
Fix and write for the Euclidean norm on . For probability measures on and , the transport cost is
where is the set of couplings, measures on with marginals and . The Wasserstein distance is for and for ; the statements here are about itself. The moment of order is .
Let be i.i.d. with law and let . The quantity of interest is .
The proof works through a multiscale distance. For , is the partition of into dyadic cubes of side . The dyadic shells are and . For measures on , , and for measures on ,
where is conditioned on and rescaled by .
In Lean, is EuclideanSpace ℝ (Fin d); , , are transportCost, moment, Dp (compact case Dcube) in FournierGuillin.Moment, valued in ℝ≥0∞. is the published WassersteinDRO.Duality.empiricalDistribution, and the published WassersteinLinOpt.Ball.couplings.
For and there is such that for every with and every ,
The constant is left unspecified, as in the paper.
Theorem 1 is the standard non-asymptotic rate for empirical measures in Wasserstein distance under moment assumptions alone. The three regimes are sharp for general laws: is attained by two-point laws, by the uniform law on a cube, and the term by heavy-tailed laws (examples on pp. 2–3 of the paper). It is the input to finite-sample guarantees for Wasserstein distributionally robust optimization, to propagation-of-chaos rates for particle systems, and to quantization error bounds.
The paper result is proved; it has, to our knowledge, no machine-checked proof. A formalization adds the multiscale coupling bound (Lemma 5), a reusable comparison between transport costs and dyadic mass differences, and binomial mean-deviation estimates for empirical measures, all of which serve other rates of convergence (the concentration bounds of Theorem 2 of the same paper rest on Lemma 5).
The obvious route bounds by a coupling on a single partition of fixed mesh and optimizes the mesh. This loses a logarithm or a power in every regime and cannot reach for or for : the error at all scales must be controlled simultaneously, which is what does. The step that requires work in Lean is Lemma 5: it builds an explicit coupling scale by scale inside and glues the shells together, and it must hold for arbitrary probability measures with possibly infinite cost. The remaining steps are careful summations of geometric series in and whose regimes depend on versus and on versus or .
Conventions: with the Euclidean norm (the paper's constant uses the diameter bound of , which holds for that norm); , , , a probability measure. The sample is a point of under the product measure , i.e. the first terms of the i.i.d. sequence. Expectations are lower Lebesgue integrals of -valued functions and all series of nonnegative terms are summed in , so no bound holds by a junk value of a non-integrable integrand or a non-summable series. Constants "depending only on " are quantified after and before and ; a statement with the constant chosen after would only assert finiteness and is ruled out.
Corrections of the print, disclosed in the items: the third case of Theorem 1 is printed with ; the remark below the theorem and Step 4 of the proof show the excluded value is (the two agree only for ), and the goal excludes . Step 1 is printed for but applied at ; it is stated for . The display defining says , but the paper uses it for all , and so does the definition.
Needed infrastructure: couplings and gluing of measures on products, dyadic partitions of boxes and their counting, binomial variance, and summation of geometric series with case analysis. Lemma 5 and the binomial estimates are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of the goal.
An assignment problem pairs each of sources with exactly one of destinations while minimizing a specified cost. A permutation records those pairings. The number of permutations grows as , so a direct search quickly becomes impractical. In discrete optimal transport, the same data can be placed in a linear optimization problem over nonnegative matrices: a matrix entry records how much mass moves from one source to one destination. That formulation permits a source's mass to be split, which gives it many more feasible solutions than the assignment problem. The question for this mission is whether the added flexibility can improve the optimum when every source and destination carries the same mass. The setting and answer are given in Peyré and Cuturi, Computational Optimal Transport, §2.2–2.3.
This capstone is the first in a series based on the textbook. It links a finite combinatorial optimization problem to the matrix model used throughout later chapters. The general transport model is needed again when marginals are unequal, when cost matrices come from distances, and when entropy is added to the objective. The uniform matching case isolates a useful boundary: relaxing an assignment to allow fractional flows expands the feasible set, yet it does not change the best objective value.
Fix an integer and a real cost matrix . The entry is the cost of sending a unit of mass from source to destination . No sign or metric assumption is imposed on . A permutation assigns source to destination , with every destination used once. The assignment objective of equation (2.2) is
The factor matters: it treats each source as having mass , so the assignment and transport objectives use the same total mass.
A histogram is a vector of masses. The uniform histogram has at each of the indices. A coupling of histograms and is a nonnegative matrix with row sums and column sums . The set of such matrices is
Its linear cost is , and denotes the minimum cost over , as in equations (2.10)–(2.11). For a permutation , the scaled permutation matrix has entry in column of row and zero elsewhere. Consequently is a coupling of with itself, and its transport cost equals . A general member of may distribute a row's mass across several columns.
Because every scaled permutation matrix is feasible for the transport problem, the unrestricted minimum cannot exceed the assignment minimum:
This is the weaker claim in the milestone list. The symmetry of couplings under transposition and the identity supply reusable statements about the model. The list also states the book's scaled form of Birkhoff's extreme point characterization.
The goal is the stronger statement: there is an assignment that also minimizes over the full coupling polytope,
This is Proposition 2.1, pp. 372–373. It quantifies over every real cost matrix of the given size. The equality of optimal values follows from the stated common optimizer; the proposition does not claim that every optimal transport plan is a permutation matrix.
The result gives an exact linear relaxation for uniform assignment. One can optimize over a convex set of matrices without paying an optimal value penalty for allowing fractional mass. The conclusion has a precise limit: it guarantees at least one integral, scaled permutation optimizer, while other optimal couplings can coexist when the cost matrix has ties. When source and destination weights are unequal, the assignment formulation may not even be feasible; the broader coupling model then carries information that a permutation cannot represent.
For formalization, the result fixes a finite transport interface that later missions can compare with their own conventions: nonnegative matrix entries, prescribed row and column sums, and a cost that is linear in the matrix. Mathlib already contains Birkhoff's theorem for doubly stochastic matrices with row sums equal to . This mission's formal target uses the probability normalization , so the scaling is part of the mathematical statement. The textbook result is known; the goal here is a machine checked Lean proof of this precise version and its cited supporting claims. The listed Lean declarations are currently open statements with sorry placeholders.
The evident inequality points in the easy direction: enlarging a feasible set can only reduce a minimum. It gives no reason why a minimizer over the larger set should happen to be a permutation matrix. A generic feasible coupling can split mass between several destinations, and even a unique assignment need not be the only point under consideration in the relaxed problem. The central issue is the geometry of the uniform coupling polytope and its relation to permutation matrices. Its normalization differs from the usual doubly stochastic convention, so a proof using a standard library theorem must retain the factor at every point where a matrix or objective is converted.
The Lean index types are Fin n and Fin m; they have and elements but are numbered from zero. Histograms are real valued functions on those types, and couplings are real matrices constrained to be nonnegative with exact finite row and column sums. The pairing is a finite double sum. The goal assumes so that the displayed is meaningful and the assignment problem has an index to assign. There is no additional positivity requirement on . The minimum values are represented by real infima only in statements where the uniform coupling polytope and permutation set are nonempty and their finite dimensional objectives are bounded below.
An optimal coupling in the goal is compared with all matrices in , including fractional ones. Restricting that comparison to permutation matrices would erase the proposition's content. The definitions of coupling feasibility, scaled permutation matrices, and the assignment cost are reusable beyond this chapter. Contributions that establish the scaling relation to Mathlib's doubly stochastic matrices, the extreme point characterization in this normalization, or the goal from these components fit the mission. The optional strict inclusion claim on p. 372 is excluded from the milestones because its printed formulation fails at ; it would require a separate statement. The page also prints row and column sums of as despite defining entries ; the Lean statement uses .
A manufacturer that sells through an independent retailer may also open its own direct channel, an online store or a factory outlet. This is called supply chain encroachment. The operations literature has asked whether encroachment helps or hurts the two firms. The usual approach compares the double-marginalization cost of a pure retail channel with the competition the direct channel creates. With quality exogenous and uniform across channels, Arya, Mittendorf and Sappington (2007) showed that encroachment can lead to a win–win outcome when the manufacturer's direct selling cost is large, because it pushes the wholesale price down.
Ha, Long and Nasiry (Quality in Supply Chain Encroachment, MSOM 18(2), 2016; authors' manuscript SSRN 3970373) make product quality a decision of the manufacturer. Their main model lets her commit to the qualities of both channels before the retailer orders. In that model quality differentiation is not always optimal: for some parameters she sells the same quality in both channels (their Proposition 4).
Commitment is a modelling assumption. When design lead times are short, the manufacturer can redesign the direct-channel product after seeing the retailer's order, so she cannot credibly announce its quality in advance. Section 6.3 of the paper studies this fast-design case. Its only analytical result is Proposition 7: without commitment, quality differentiation across channels is always optimal. This mission formalizes that proposition and the three steps of its proof.
Consumers. A consumer has quality sensitivity , uniform on , and obtains surplus from one unit of quality at price . The manufacturer sells units of quality directly and the retailer sells units of quality . Each consumer buys at most one unit, and the market-clearing prices depend on which product has the higher quality:
At both channels clear at .
Costs. One unit of quality costs the manufacturer , with . She pays a selling cost for each unit sold directly; the retailer's selling cost is .
Profits. For a wholesale price ,
Timing without commitment.
The game has perfect information and is solved by backward induction. A strategy profile has three parts: a stage-1 choice , a retailer rule , and a stage-3 rule . The profile is a subgame perfect equilibrium (SPE) when, at every history on or off the path, the mover's action is feasible and no feasible alternative gives the mover more. The manufacturer encroaches when on the equilibrium path.
For every , and every SPE whose equilibrium path has and ,
Write with .
The case gives in the same way, and the two agree at . 2. Derivatives (31)–(32). The -derivatives of and , their values at , and the equivalence
Milestone 3 is stronger than the goal: it holds at every stage-3 history, not only on the equilibrium path.
The result. Proposition 7 shows that the structure of the optimal product line depends on the timing of design decisions. With commitment, the manufacturer sometimes keeps a single quality. A lower-quality direct product would draw a larger retail order but forgo market segmentation, and with some parameter values she accepts that trade. Without commitment, the direct-channel quality can no longer influence the retailer's order. She then always differentiates, so whenever both channels sell, consumers face a two-product line. The paper's numerical work (Figure 6) compares the two regimes. The analytical statement that differentiation is universal without commitment is this proposition.
Formalizing it. The proposition has a short, informal proof in the e-Companion. That proof argues through first-order conditions, "given that is optimal". It uses the strict signs printed in (31) and (32), although optimality gives only weak inequalities. Its contradiction relies on the retailer's order being positive, which the statement leaves implicit. A machine-checked proof pins down exactly which hypotheses the result needs. It also contributes reusable facts about Cournot-type stage games with vertically differentiated products. No part of this paper has been formalized before.
The stage-3 problem is a joint choice of quality and quantity , and the demand system changes form at , so the manufacturer's profit is not differentiable in there. The value function after optimizing is a piecewise expression: to the right of , to the left, and the linear profit wherever the optimal is zero. An argument that is not optimal has to work with one-sided derivatives of this function at a kink. It must also check that the optimal quantity stays positive on both sides near .
An obvious shortcut is to argue that differentiation is optimal because segmentation always pays. That argument fails at . There the manufacturer is a one-product monopolist, and is optimal whenever happens to equal her monopoly quality. The positive retail order is therefore essential.
All definitions live in the namespace QualityEncroach.NoCommit. They are real-valued throughout, and the formalization fixes the following conventions:
A trivializing formalization is ruled out: the stage-3 rule maps to , so is chosen after the order. Putting at stage 1 would give the committed game, where the proposition is false. The goal is conditional on an SPE existing, which the paper does not prove. A verification file checks the price formulas on hand instances in both branches. At , , , and , it checks that the basic parameter conditions hold and a uniform stage-3 choice is strictly beaten by . The numerical check does not establish the existence of an optimal stage-3 choice or an SPE.
A complete development needs elementary real analysis only: maximization of concave quadratics, one-variable derivatives, and one-sided optimality conditions at a kink. Proofs of any milestone, and proofs of the goal from milestone 3, are welcome.
Best subset selection with ridge shrinkage asks for a coefficient vector that fits a response through a design matrix while using few nonzero coefficients:
This -regularized least squares problem is NP-hard, and exact methods solve it as a mixed integer program by branch-and-bound (BnB). The speed of BnB is governed by the strength of the continuous relaxation solved at every node: a larger relaxation value prunes more nodes. Hazimeh, Mazumder and Saab (arXiv:2004.06152, Mathematical Programming 2022) build the solver L0BnB on a perspective formulation and compare its relaxation with two standard alternatives. Their Proposition 1 quantifies that comparison, and their experiments (Section 4.2.1 of the paper) report speed-ups of more than 90× from using the perspective formulation with a tight bound instead of the bound-free formulation.
The mission formalizes Proposition 1 together with the three steps of its proof in the paper's Appendix A.
Fix , , regularization parameters and a bound on ; write .
The Big-M formulation introduces indicators and minimizes subject to , . Its interval relaxation lets ; its optimal value is .
The reverse Huber penalty is for and for . Put
and let if and if . The paper's Theorem 1 shows that the interval relaxation of the perspective formulation is equivalent to
and denotes the optimal value of (5). Without a bound, the relaxation value of is
Finally , and denotes an optimal solution of (5).
For ,
The goal is the conjunction of milestones 2 and 4.
In the regime both added terms are nonnegative: because , and because whenever . So the perspective relaxation is at least as strong as both the Big-M relaxation and , strictly so as soon as one coordinate of lies strictly inside in absolute value (for (7)) or (for (8)). The bounds are explicit in the relaxation's own solution, so they can be evaluated at a BnB node. This is the theoretical justification for the paper's design choice of building its solver on with a valid, tight ; the regime , where (5) is (6) with the additional box constraint , is complementary.
Proposition 1 is proved in the paper; it has no machine-checked proof. The mission produces one, together with reusable Lean definitions of the three relaxation values and of the reverse Huber penalty that other statements about perspective relaxations of sparse regression can be stated against.
The arithmetic of the coordinate-wise penalties is short. The substance is in comparing optimal values that are defined as infima over different feasible sets. The obvious argument "" requires that the Big-M relaxation, which is posed over pairs , have value at most ; that is the content of (37), a statement about a different feasible set in more variables. Likewise (8) needs , i.e. that the infimum in (6) is a genuine lower bound of a set bounded below, and both inequalities use the regime , in which . Dropping the regime hypothesis makes (8) false in general: for one has and , and the right side can exceed .
All objects live in the namespace L0BnB.Strength. Data are X : Matrix (Fin n) (Fin p) ℝ, y : Fin n → ℝ, reals lam0 lam2 M with 0 < lam0, 0 < lam2, 0 < M as hypotheses; is Fin p. Norms are explicit sums: is ∑ i, v i ^ 2, is ∑ i, |β i|, and is ∀ i, |β i| ≤ M. The regime is written M < Real.sqrt (lam0 / lam2).
Optimal values are sInf of the image of the feasible set in ℝ. Each set is nonempty (, ) and bounded below by under the positivity hypotheses, so sInf is the true infimum and never a junk value. is defined over pairs with , not through ; (37) is a theorem. is (6) as printed: the paper attributes to its reference [21] the identification of (6) with the interval relaxation of in variables, and that identification is not part of the mission. is the value of (5), which is the paper's definition; Theorem 1 (the equivalence of (5) with the relaxation) belongs to a sibling mission.
The optimal solution is a binder with the hypotheses and for every in the box. A formalization in which is an arbitrary feasible point, or in which or is defined through a chosen minimizer, would change the statement and is ruled out. The paper uses no in this result, so no constant is instantiated.
Needed infrastructure is light: continuity of and compactness of the box for the attainment in (37), and csInf lemmas on ℝ. Contributions of proofs of any milestone, and of the attainment of the infimum in (5), are welcome.
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.
In classical optimal transport on the real line, one coupling plays a distinguished role: the monotone (Hoeffding–Fréchet) coupling, which sends the -quantile of the first marginal to the -quantile of the second. It is canonical (every initial segment of the first marginal goes as far left as possible) and it is optimal for a whole family of costs at once.
Martingale optimal transport adds the constraint that the coupling be the law of a one-step martingale , . The problem arises in robust (model-independent) mathematical finance: prices of vanilla options fix the marginal laws of and of , and bounds on the price of an exotic option that hold under every arbitrage-free model are values of the martingale transport problem (Beiglböck, Henry-Labordère, Penkner 2013; Galichon, Henry-Labordère, Touzi 2014). Martingale couplings exist exactly when and are in convex order (Strassen 1965).
Beiglböck and Juillet (arXiv:1208.1509, Ann. Probab. 44(1), 2016) asked for the martingale counterpart of the monotone coupling, and found it: the left-curtain coupling . This mission formalizes its existence and uniqueness (Theorem 1.5), which is the foundation for the paper's later optimality results (Theorems 1.7, 6.1 and 6.3, other missions of this series).
All measures are Borel measures on or . is the set of finite measures with . For :
In Lean these are InM, ConvexLE, ExtConvexLE, IsMartingalePlan, IsLeftMonotone, IsShadow, IsLeftCurtain and targetUpTo in the shared namespace MartOT.Var. The mission's own theorems are in MartOT.Curtain.
For probability measures on with finite first moments,
Existence alone, or uniqueness only among left-curtain plans, is not the goal: the statement says that monotonicity alone singles out one martingale coupling.
Theorem 1.5 identifies a canonical martingale coupling defined by a geometric property of its support alone. The paper then shows that is the unique optimizer of the martingale transport problem for costs with strictly convex (Theorem 1.7) and that it is characterized by the convex-order minimality of Theorem 1.8. The left-curtain coupling has since been studied and generalized in a series of works (for instance Henry-Labordère and Touzi 2016).
The result is proved in the paper. It has, as far as the platform's catalogue shows, no machine-checked proof: no statement about martingale transport plans, shadows or the left-curtain coupling exists on Prove2Me. A formal development would produce reusable infrastructure: the convex order on finite measures of arbitrary mass, shadows, and the passage between the barycentre characterization (4) of martingale plans and their disintegrations.
Existence is not the hard part in the abstract: a left-monotone plan can be obtained as an optimizer for a suitable cost via the variational lemma. The construction through shadows is more delicate: one must show that the shadows of the initial segments increase with (this rests on Theorem 4.8, the shadow of a sum) and that the resulting plan satisfies the martingale property.
Uniqueness is the main obstacle. The classical argument for uniqueness of optimal plans (averaging two candidates and using strict convexity) requires a continuous first marginal and does not apply to arbitrary with atoms. The paper's argument is specific to the problem: it compares with the shadow through the test functions and a case analysis at the support end-points, which needs the measure-theoretic Lemmas 5.1 and 5.2.
MeasureTheory.Measure ℝ and Measure (ℝ × ℝ) with Borel σ-algebras. The goal and Theorems 1.8, 4.18, 4.21 take probability measures (IsProbabilityMeasure) in convex order; Lemma 4.6, the shadow monotonicity, Lemma 5.1 and Theorem 5.3 work in , as the paper's Sections 4–5 do.EReal, through the published ModelRiskOT.Duality.extIntegral), so no Bochner integral of a non-integrable function enters a statement. is encoded by characterization (4) of the paper, not by disintegrations.IsShadow, IsLeftCurtain), never chosen functions: their existence and uniqueness are milestones, not definitions. A formalization that defined by a choice and the left-monotone plan as "the left-curtain plan" would make the goal circular; the goal mentions only and left-monotonicity.Measure.support.BddAbove; at Lean's convention applies.PalmQueueing.Ordering.strassen_cx.Contributions are welcome at every level: proofs of the milestones, auxiliary lemmas on the convex order of finite measures (potential functions , equality of mass and mean), and the equivalence between (4) and the disintegration form of the martingale property.
Adam (Kingma and Ba, 2015) is the default optimizer for training neural networks: a stochastic gradient method that keeps an exponential moving average of past gradients and an exponential moving average of their coordinatewise squares, and divides the first by the square root of the second. Its practical success came well before any convergence theory for nonconvex objectives. Reddi, Kale and Kumar (2018) showed that Adam with constant momentum parameters can fail to converge even on convex problems, which made the question of under which parameter schedules Adam provably converges a live one.
Barakat and Bianchi (arXiv:1810.02263, SIAM J. Math. Data Sci. 2021) answer it through the ODE method of stochastic approximation (Benaïm, 1999). This mission takes the paper's almost-sure convergence theorem for Adam with decreasing stepsizes, Theorem 5.2. Under a stepsize schedule in which and shrink in proportion to the stepsize , the iterates converge almost surely to the critical points of the objective, provided they stay bounded.
Let be a random variable on a measurable space with law , let be an integrand with gradient in , and set
where is the coordinatewise square and is the critical set. Let be iid copies of on a probability space .
Algorithm 5.1 takes stepsizes , weights and a constant . Starting from , and , it computes for , with all vector operations coordinatewise:
The divisions by , are the bias correction.
The stepsizes satisfy Assumption 5.1: , , , and there are with , and . The limiting dynamics is the autonomous ODE on , written , with
Assume Assumption 2.2 (regularity and moments of ), coercive (2.3), coordinatewise (2.4), iid samples (4.1), Assumption 5.1, on compacts (4.2 i) with ), that has empty interior, and that is bounded with probability one. Then, almost surely,
and if is countable, almost surely for some .
The theorem identifies a regime of Adam's hyperparameters, and with , in which the algorithm behaves like a gradient method with vanishing noise: the iterates approach critical points, the momentum dies out, and the second-moment estimate converges to . The condition ties the two averaging rates together. It is the condition under which the paper's Lyapunov function for the continuous dynamics decreases (Lemma 7.5). The argument structure is also a template for other adaptive methods: once the limiting ODE has a strict Lyapunov function, almost-sure convergence of the iterates follows from the same steps.
The paper proves the result on paper; none of it is machine-checked. A formal proof would also be the first formal instance on Prove2Me of the full ODE method for a concrete stochastic algorithm. That pipeline runs from the iterates to a perturbed Euler scheme, then to an asymptotic pseudotrajectory and a limit-set theorem, and finally to convergence. Benaïm's general results are being formalized separately on the platform (the asymptotic-pseudotrajectory definition this mission reuses comes from that effort), so the two developments meet in milestone 3.
The obvious approach is to treat Adam as stochastic gradient descent with a preconditioner and run a descent-lemma argument on . This fails because the update direction is not a descent direction for : lags behind . Any Lyapunov function has to involve the momentum, and alone does not decrease. The continuous-time energy decreases only weakly, and only its perturbation is strict, and only on compact sets. A second difficulty is that the stepsize-dependent coefficients and the bias corrections , make the recursion a non-autonomous perturbation of the Euler scheme of . The remainder must be shown to vanish along almost every path before the general theory applies. Finally, the abstract limit-set theorem needs the semiflow to be well defined on the closed set , where involves and is not Lipschitz at .
is EuclideanSpace ℝ (Fin d). The state space is the product of three copies with Mathlib's max-of-factors norm, which is equivalent to the Euclidean norm of and leaves boundedness and limits unchanged. and are Bochner integrals against the law . Assumption 2.2 makes the integrands integrable, so they are the true expectations. Moments are lower Lebesgue integrals. Algorithm 5.1 is a pathwise recursion adamIter, driven by a random sequence whose index is unused. The iid hypothesis is iIndepFun with every of law .
Two hypotheses are left implicit on the page and are added explicitly. The first is . The second is and : Assumption 5.1 iii) permits , which gives , and Lean's division by zero returns . Lemma 9.1 is stated with and , which its convergence claim needs. Semiflows are Flow ℝ≥0 on the subtype , and the asymptotic pseudotrajectory and limit set are the published StochApproxDyn.LimitSet definitions. The ODE milestones 4–6 hold for abstract , under Assumptions 7.1–7.2 with , as in the paper's §7.
The goal concerns the iterates of Algorithm 5.1 itself. A statement about trajectories of , or one that replaces almost-sure boundedness by a bound uniform in together with deterministic gradients, is a different and much weaker theorem and is ruled out. The interior condition on and the countability of enter exactly as on the page.
A complete development needs the following:
The last two are reusable for any stochastic approximation scheme, and contributions to them are welcome independently of Adam.
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.
Many methods for minimizing a smooth convex function on a Hilbert space can be read as discretizations of second order ordinary differential equations, and the asymptotic behaviour of the continuous trajectories predicts the behaviour of the iterates. The inertial system with vanishing damping is the continuous counterpart of Nesterov's accelerated gradient method (Su, Boyd, Candès 2016); for its trajectories converge weakly to some minimizer of (Attouch, Chbani, Peypouquet, Redont 2018). Two modifications of this system have been studied separately. A Hessian driven damping term reduces oscillations while keeping the fast rate of the values (Attouch, Peypouquet, Redont 2016). A Tikhonov regularization term with selects a particular minimizer: under suitable decay of , trajectories approach the minimizer of minimum norm in the strong (norm) topology (Attouch, Chbani, Riahi 2018).
Boţ, Csetnek and László (arXiv:1911.12845v2, published in Mathematical Programming 2021) combine both terms and ask which properties of the two separate systems survive. This mission formalizes their strong convergence result, Theorem 4.4.
Let be a real Hilbert space, , , , and . The General assumption of the paper (p. 2) is:
A global -solution of the system
is a twice continuously differentiable curve satisfying (5) at every . The set is nonempty, closed and convex, so it has a unique element of minimum norm, denoted . The open ball is . In the Lean development these objects are GeneralAssumption g t₀ ε ε', IsSolution g α β t₀ ε u₀ v₀ x xd xdd and IsMinNormMinimizer g xstar in the namespace TikhonovHDD.Strong, with written minValue g.
Assume, in addition to the above,
that for all , for some and , and that if , while for large , for some , if . Then
and
if there exists such that stays either in or in its complement.
The three cases are exhaustive, so Cases I–III together give the goal.
Theorem 4.4 shows that adding Hessian driven damping does not destroy the selection property of Tikhonov regularization: the trajectory comes arbitrarily close to the minimum-norm minimizer, and converges to it in norm whenever it does not oscillate across the sphere forever. Since , the system still approaches , but the limit is a canonical minimizer determined by alone, not by the initial data. In infinite dimensions this is the difference between weak and strong convergence, a distinction that matters for ill-posed problems and inverse problems, where the minimum-norm solution is the one usually sought. Remark 4.5 of the paper compares the hypotheses with those of Attouch, Chbani and Riahi for the system without Hessian damping: for the lower bound required of when is, in the authors' words, "less tight" than theirs.
The result is proved in the paper; no part of it has a machine-checked proof. Formalizing it requires a Lyapunov-energy argument for a second order ODE in a Hilbert space, the weak lower semicontinuity of convex functions and of the norm, and the passage from weak to strong convergence via convergence of norms. Theorem 3.1 and Lemma A.1 are standalone results reusable for other Tikhonov-regularized inertial systems.
The weak convergence argument for the unregularized system (Opial's lemma) does not identify the limit, and it does not give strong convergence. Tikhonov regularization supplies the identification only through the Tikhonov curve , the minimizer of , and comparing with requires an energy whose derivative is controlled with weights tuned to . The Hessian term produces cross terms of the form that are absent from the system without Hessian damping; the integral hypothesis on and the slow-decay condition exist to absorb them. A direct energy estimate only works when ; inside the ball a different argument is required, and when the trajectory crosses the sphere infinitely often neither argument yields convergence of the whole trajectory, only a liminf statement.
Conventions committed to in Lean:
xd, xdd, ε'; and are continuous there.gradient g; is the Fréchet derivative of gradient g at applied to . "Lipschitz on bounded sets" means Lipschitz on every closed ball centred at .Filter.liminf is not used, since it returns for a function tending to .No statement of the mission has been repaired against the printed text.
A complete development needs: weak lower semicontinuity of convex continuous functions and of the norm on Hilbert spaces; weak sequential compactness of bounded sets; existence of the minimum-norm element of a closed convex set (Mathlib's projection onto closed convex sets); the strongly convex Tikhonov curve and its convergence to ; and calculus for energy functionals along curves on half-lines. Lemma A.1 and the Tikhonov-curve facts are reusable for every Tikhonov-regularized dynamics. Contributions of proofs of individual milestones, of supporting lemmas, and of alternative arguments are welcome.
Online retailers, search engines and streaming services show products on a sequence of pages, and most consumers look at only the first few. Which products are seen therefore depends on where they are placed. Gallego, Li, Truong and Wang (Operations Research, 2020) call the problem of placing products on pages to maximize expected revenue product framing. They show that it is NP-hard even with two pages and the multinomial logit model, and they give simple algorithms with constant-factor guarantees.
This mission concerns their second guarantee. In their basic model every consumer chooses with the same choice model, whatever the number of pages she views. In practice the number of pages viewed is itself informative: consumers who browse many pages may be keener buyers. Section 6 of the paper lets the choice model depend on the number of pages viewed and proposes the TRUNC algorithm for this setting. The guarantee is that TRUNC earns at least one third of the optimal expected revenue.
There are products with revenues and virtual pages, each holding at most products; write . A framing places each product on at most one page, with at most products per page. A consumer views a random number of pages, with law , tail and failure rate . Her consideration set is the set of products on pages .
A consumer who views pages is of type and buys product from consideration set with probability , where , for , and . The revenue of for type and the best capacitated revenue are
A framing earns , where is the set of products on pages . Its maximum over all framings is . The assumptions are:
TRUNC(), for , picks an optimal assortment for and places it, in any arrangement, on pages , leaving the remaining pages blank. TRUNC takes the best of these framings; its revenue is .
The analysis passes through the bound-revealing program (10): minimize over nondecreasing with nonincreasing and over tails with , subject to .
Under Assumptions B1–B4, for every choice of optimal assortments and every arrangement on the pages,
In the order the proof uses them:
The theorem shows that framing under type-dependent choice admits a constant-factor approximation using only calls to an assortment oracle, although the framing problem itself is NP-hard. The constant does not depend on the number of products, pages or page capacity. The bound-revealing program (10) is a self-contained extremal problem about log-concave tails and is reusable wherever a revenue curve with decreasing average returns meets an IFR horizon. The numerical value of (10) decreases with ( at , about at ), so the constant is approached only as the number of pages grows.
The result is proved in the paper. No part of it has a machine-checked proof: the platform has no item on product framing, discrete failure rates or program (10). A complete development would give a machine-checked proof of the approximation ratio. It would also give a checked treatment of the perturbation arguments of Appendix A.4, which the paper presents briefly.
Two steps are elementary: the upper bound (a consumer of type never sees more than products) and the lower bound (every consumer of type sees all of ).
The difficulty lies in the extremal problem (10). It is not convex: the IFR constraint is a log-concavity condition, and the objective is a maximum of products . A direct bound such as gives a constant that decays with . The uniform constant comes from showing that the extremal tail is geometric beyond the maximizing page and that the extremal is pinned down on both sides of it. The paper reaches this structure through optimality conditions, so a formal proof must also establish that (10) attains its minimum, or must avoid that step.
Products are Fin n. Pages are the natural numbers , as in the paper, with and . A framing is f : Fin n → ℕ: product is on page f i when , and f i = 0 means it is not displayed. The law and the functions of (10) are functions on of which only the values on are used, and .
and are maxima over finite nonempty families, and is a Finset.sup' over . TRUNC is a predicate on its outputs, not a function, and the goal is quantified over every family of runs. Assumption B3 is used with , as everywhere in the paper. IFR is required only where the failure rate is defined (), so laws whose support ends before page are allowed. Nonnegative revenues are assumed; the lower bound of milestone 2 needs them.
No trivializing reading. The goal is not stated for one particular filling heuristic, or for some run only, and is the revenue of the framings themselves, not the lower bound .
Page numbers refer to the authors' accepted manuscript of the Operations Research article, which differ from the journal typesetting. The development needs only Mathlib (finite sums and maxima over Finset). Program (10) and Lemma 8 are independent of the framing model. Contributions are welcome at every milestone: Lemma 8 and the bound for (10) are the most self-contained.
Best subset selection with ridge shrinkage asks for a sparse linear model: given a design matrix and responses , minimize
where counts nonzero coefficients. The problem is NP-hard, and exact methods solve it as a mixed integer program by branch-and-bound (Bertsimas, King, Mazumder 2016). The speed of branch-and-bound is governed by two things: how tight the continuous relaxation at each node is, and how cheaply that relaxation can be solved.
Hazimeh, Mazumder and Saab (arXiv:2004.06152v2; Mathematical Programming 2022) build a branch-and-bound solver whose node relaxations are solved by first-order methods rather than by a conic interior-point solver. Their starting point is the perspective formulation, a standard device for strengthening relaxations of mixed integer programs with indicator variables (Frangioni, Gentile 2006; Günlük, Linderoth 2010). Theorem 1 of the paper shows that the interval relaxation of this formulation is a box-constrained least squares problem with a separable penalty in alone. This mission formalizes Theorem 1.
Timeline. Owen (2007) introduced the reverse Huber penalty as a hybrid of lasso and ridge. Dong, Chen, Linderoth (2015) showed that the interval relaxation of the perspective formulation without a Big-M bound reduces to least squares with a reverse Huber penalty. Hazimeh, Mazumder and Saab (2020–2021) added the Big-M constraint and obtained Theorem 1, with a second regime in which the penalty becomes .
Fix , , , and , and write . The perspective formulation is problem (3) of the paper:
Here indicates whether may be nonzero, stands in for through the rotated second-order cone constraint , and bounds . The interval relaxation replaces with .
The reverse Huber penalty (4) is for and for . Put
and let if and if . The reduced relaxation (5) is
with optimal value . For one coordinate , is the minimum of over , , , .
The interval relaxation of (3) is equivalent to (5):
and both problems attain the common optimal value .
The result. Theorem 1 removes the auxiliary variables and all conic constraints from the node relaxation. What remains is a composite problem, a smooth least squares loss plus a separable, convex penalty under a box constraint, to which coordinate descent and proximal methods apply directly. The paper's solver, its active-set strategy, and the dual bounds of its Section 3 are all built on (5). The theorem also exposes a regime change: when , the ridge term of the perspective formulation disappears from the relaxation and the penalty is pure . Propositions 1 and 2 of the paper, which compare the strengths of the perspective, Big-M and relaxations, use this reduced form.
Formalizing it. The result is proved in the paper (Appendix A) by a coordinatewise argument. To our knowledge it has no machine-checked proof. Formalizing it gives a verified bridge from the conic mixed integer formulation to the penalized form that later results of the paper use, and a checked case analysis at the regime boundary , where the two formulas must agree with the stated tie-breaking.
The obvious approach, "minimize over and coordinate by coordinate", is correct in outline, but each step hides a boundary case. The rotated cone constraint degenerates at or , where is undefined, and the paper's convention for must be handled. The one-variable problem (36) is a minimum of a pointwise maximum of two functions of , one convex and decreasing then increasing, the other increasing. Its minimizer lies either in the interior of the region where the first term dominates or on the crossover , depending on the regime. The paper's proof describes the cases loosely: it optimizes the Case I term without imposing the side condition that Case I attains the maximum. A complete argument must prove the lower bound over all feasible , not just evaluate at a candidate. Finally, the minimum over must be shown to split into a sum of coordinate minima, each attained.
Data are X : Matrix (Fin n) (Fin p) ℝ, y : Fin n → ℝ, and reals lam0 lam2 M with 0 < lam0, 0 < lam2, 0 < M; the paper's is Fin p. The squared norm is the explicit sum , and is for all . The cone constraint is kept in product form . In and (36), Lean's coincides with the paper's convention for . Every "min" is stated with IsLeast (membership plus lower bound), so attainment is part of each statement. is defined as a real infimum over the box, and Theorem 1 asserts that this infimum is attained by both problems. No normalization of or is assumed; the paper's unit-norm assumption starts in Section 3. The paper writes no in these results, so there are no constants to instantiate.
A goal stating only one inequality (that is achieved by some , or that it bounds the relaxation from below), or a goal over , would not be Theorem 1. The IsLeast form rules out both. The goal uses with both regimes.
A complete development needs: a two-variable convexity argument for on ; a lemma that the infimum of a separable objective over a product of feasible sets is the sum of the coordinate infima; and continuity of with compactness of the box to obtain an optimal . The coordinate lemmas and the definition of the reverse Huber penalty are reusable in the companion missions on relaxation strength and Lagrangian duality. Contributions to any milestone, or an alternative proof of the goal, are welcome.
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.
Thompson sampling (TS) selects each action by sampling a parameter from the current posterior and playing the action that is optimal for the sample. It is a stationary randomized strategy: the distribution of the action is a fixed function of the posterior, the same in every period, and the action is drawn at random from it. Its Bayesian regret bounds, surveyed in §8.1 of the tutorial by Russo, Van Roy, Kazerouni, Osband and Wen (Found. Trends Mach. Learn. 11(1), 2018), grow sublinearly in the horizon .
A natural question is whether the randomization is essential. A strategy that maps the posterior to an action deterministically, for example "play the action with the highest posterior mean", is equally stationary and conceptually simpler. §8.1.3 of the tutorial answers the question with Example 8.1 (A Known Standard), taken from Russo and Van Roy, Learning to optimize via information-directed sampling (Operations Research 66(1), 2018): in a two-action problem with a known baseline action, every stationary deterministic strategy suffers linearly growing expected regret under some prior. The example is the standard justification for why posterior sampling, and not a deterministic function of the posterior, is the right stationary rule.
There are two actions and a binary unknown parameter with prior
In each period the agent selects an action and observes a binary reward . Rewards are conditionally independent across periods given and the actions:
The mean reward of action is its success probability, and the optimal action is action if and action if , so or .
The history lists the actions and rewards of the first periods. The posterior is given by Bayes' rule (4.2) of the tutorial, applied period by period:
with the prior on the empty history.
A stationary deterministic strategy is one function from posterior probabilities to actions, used in every period: . The expected cumulative regret (Bayesian regret, p. 71) of running from the prior for periods is
the expectation taken over and the rewards. The Lean development names these objects succProb (), optMean (), post (), Strategy (), lawGiven (the probability of a history given ) and expRegret.
This is the sentence "for any deterministic stationary strategy, there exists a prior probability such that expected cumulative regret grows linearly with time" (p. 79). The prior is chosen after the strategy. No constant is fixed; only the linear shape is asserted.
The example separates two properties that regret analyses often conflate: being a function of the posterior alone (stationarity) and achieving sublinear Bayesian regret. It shows that a stationary strategy with sublinear regret on all priors must randomize, which is the structural reason TS samples rather than maximizes. It also explains why deterministic algorithms with good regret, such as upper confidence bound methods, are necessarily nonstationary: their confidence radii depend on the period and on counts, not only on the posterior.
The tutorial gives the argument in one paragraph. A formal version makes precise what is left implicit there: that the posterior is the actual conditional probability computed from the history, that "uninformative" means the posterior is invariant under action , and that under action the posterior never leaves . The result is a closed-form regret identity in each case, not only an asymptotic statement. As far as is known, neither the example nor its source in Russo and Van Roy (2018) has been machine-checked.
The mathematics is elementary; the work lies in the bookkeeping of a history-dependent strategy. The strategy's action in period depends on the whole history through , so the law of is a product of indicator factors, each evaluating at a posterior computed from a prefix of the same history. A direct computation of the regret must show that every history of positive probability follows a single action path, and that is a statement about the posterior along every prefix, not only at the first period. A first attempt that defines the posterior by a recursion in which "the posterior stays at " is built in proves nothing about the example; the posterior must be Bayes' rule applied to the history.
0 : Fin 2, action is 1 : Fin 2; is true; a reward of is true. Lean period s : Fin T is the paper's period .Fin t → Fin 2 × Bool; every probability and expectation is a finite sum, so no measure theory is needed.post is the closed form of iterated Bayes' rule (4.2). The probabilities with which the strategy picks its actions are or and do not depend on ; on histories of positive probability they cancel, so post is the true conditional probability there. For its denominator is positive, so Lean's convention is never used.ℝ → Fin 2; its values outside are never used. The same function acts in every period, which is what "stationary" means.The tutorial's argument for the example is on p. 79; the tutorial attributes the example to Russo and Van Roy (2018).
Many algorithms in signal processing, statistics and machine learning share one template: replace a hard objective by a simpler function that lies above and touches it at the current point , minimise that surrogate, and repeat. The expectation–maximisation (EM) algorithm, difference-of-convex (DC) programming, proximal minimisation and many majorisation–minimisation schemes are of this form. Razaviyayn, Hong and Luo (arXiv:1209.2385; SIAM J. Optim. 23 (2013) 1126–1153) call the single-block version Successive Upper-bound Minimization (SUM) and give a short set of conditions on the surrogate under which every limit point of the iterates is a stationary point, without convexity or smoothness of .
Their single-block result, Theorem 1, is the base case of the paper. The block versions (BSUM, and block successive convex approximation with Armijo steps) are the subjects of the next two missions in this series. Earlier convergence results for related schemes were weaker: the inner approximation algorithm of Marks and Wright (1978), cited on p. 5–6 of the paper, guarantees stationarity only if the whole sequence converges, and only for smooth objectives.
Let be a closed convex set and an objective whose relevant values are those on (the paper assumes ). The problem is
The directional derivative of a function at in direction is the lower limit
an extended real number. A point is a stationary point of (2) if and for every with ; the set of stationary points is .
An approximation function satisfies Assumption 1 if
The SUM algorithm starts from and, for , sets to an arbitrary element of . A limit point of the iterates is the limit of some subsequence .
Under Assumption 1, every limit point of the iterates generated by the SUM algorithm is a stationary point of (2):
The theorem asserts nothing about existence of limit points or of minimisers of the subproblems; it holds for every run the algorithm can produce.
Theorem 1 reduces the convergence analysis of an entire family of algorithms to checking four properties of a surrogate. Proposition 1 makes (A3) checkable in the common composite case "smooth plus nonsmooth": majorise only the smooth part and keep the nonsmooth part unchanged. Corollary 1 turns the limit-point statement into convergence of the whole sequence to the stationary set when the level set is compact. The block-coordinate results of the same paper (Theorems 2–4) reuse the structure of this argument block by block.
The results are proved on paper; to our knowledge none of them has a machine-checked proof. A formal development would supply a reusable account of extended-real lower directional derivatives on convex sets, the first-order necessary condition for constrained minimisers in that generality, and the limit-point argument for descent methods with a continuous surrogate, all of which recur in the analysis of block coordinate and majorisation–minimisation methods.
The argument is short, and the difficulty lies in its precise use of the hypotheses. The surrogate inequality must be passed to the limit along a subsequence, and only joint continuity of (A4) on allows this: itself is not assumed continuous, so the natural first idea of passing to the limit is not available. The derivative is a liminf in the extended reals, so it may be , and the comparison between and is made only through (A3) at the single point and only in feasible directions. For Proposition 1, (4)–(5) give only a one-sided inequality between the derivatives of and at , because may lie on the boundary of ; equality needs an argument at interior points of a feasible segment and the continuity of the derivatives.
The space is EuclideanSpace ℝ (Fin m) (the 2-norm of p. 4). The directional derivative is the published TsengBCD.Stationary.dirDeriv (Tseng 2001), an EReal-valued liminf over , used as a reference item. The definitions module BSUMConv.SUM.Setting provides IsStationaryOn, stationarySet, AssumptionA1–AssumptionA4, Assumption1, the run predicate IsSUMRun and the level set levelSet0.
Conventions committed to:
MapClusterPt), not the limit of a convergent sequence.The statements cannot be trivialised: Assumption 1 is satisfiable (for instance by the proximal surrogate of §VIII-B for suitable ), stationarity is a genuine condition (it fails for at any on ), and Theorem 1 is about every cluster point, not about runs assumed convergent. Contributions welcome: proofs of the three milestones, of Theorem 1 from them, and of the two companion statements; general lemmas about dirDeriv (constants, sums with a function having a finite one-sided derivative, first-order conditions on convex sets) are reusable across this series.
The optimal assignment problem asks for a one-to-one matching of points to objects of least total cost. It is the discrete optimal transport problem between two uniform measures with the same number of atoms, and by the Birkhoff–von Neumann theorem it coincides with the Kantorovich linear program on that instance (Peyré and Cuturi, Computational Optimal Transport, Proposition 2.1). Assignment solvers are therefore the inner routine of exact discrete optimal transport, of matching-based estimators in statistics and of many combinatorial optimization pipelines.
The auction algorithm was introduced by Bertsekas in 1981 (Bertsekas 1981) and refined with ε-scaling by Bertsekas and Eckstein in 1988 (Bertsekas & Eckstein 1988). It is a dual coordinate method with an economic reading: unassigned points bid for objects, prices of contested objects move, and an object changes hands when outbid. Its practical appeal is that each iteration is local and cheap, and that it parallelizes well. Peyré and Cuturi present it in §3.7 of their monograph (pp. 417–422) as an alternative use of the machinery of C-transforms, and as a precursor to the Sinkhorn algorithm of Chapter 4.
Fix , write , and let be a cost matrix: is the cost of assigning point to object . A permutation of is an assignment, of cost .
A dual vector (price vector) is indexed by the objects. Its -transform is , the best adjusted cost available to point ; a pair is dual feasible if for all .
The algorithm maintains a triplet : a set of assigned points, a partial assignment vector (an injective map from to ) and a dual vector . The state satisfies ε-complementary slackness (ε-CS) if
One iteration picks a point , a lowest adjusted cost index and a second lowest , and performs
removes from the point with (if there is one), sets and adds to . The algorithm starts from , , and terminates when .
For every and every run of the algorithm that terminates, the final is a permutation and
The goal fixes no particular tie-breaking rule and no order in which unassigned points bid: it holds for all of them.
For , every run has at most iterations. This is the termination statement; the goal does not depend on it.
Proposition 3.9 is the accuracy guarantee of the auction algorithm. With integer costs and it yields an exactly optimal assignment, which is how the algorithm is used as an exact solver; combined with ε-scaling it gives the complexity bounds quoted in Remark 3.3. The argument is also the template for every ε-relaxed primal–dual method: an approximate optimality certificate maintained by local moves, turned into a global suboptimality bound by weak duality.
The results are classical and proved in the book and in Bertsekas's monographs; they are not open. What this mission adds is a machine-checked account of the algorithm with all of its nondeterminism (ties in the argmins, the order of bidders) quantified explicitly, together with the corrected iteration bound. To the best of the mission's prior-art search, no Lean formalization of the auction algorithm exists on the platform or in Mathlib, which has the assignment problem only implicitly (through permutations and doubly stochastic matrices).
The obvious argument for the goal sums the ε-CS inequality over and compares with an arbitrary permutation . The sum telescopes only if the final is a bijection, so the proof must carry, through every iteration, the invariant that is injective on , and this invariant interacts with the removal of the displaced point in step 2: the set update has to remove exactly the point holding , which needs injectivity at the previous step.
Preserving ε-CS for the points that are not bidding relies on prices only ever decreasing, which in turn needs and the specific form of (3.9); preserving it for the bidder needs the second-best index to realize the minimum over , including in the presence of ties. The printed termination bound is false (see below), so the companion requires reconstructing the counting argument: an object that is still unassigned has never been bid on and keeps price , which caps the number of bids on any other object.
Fin n; is a Matrix (Fin n) (Fin n) ℝ; prices are Fin n → ℝ; is the infimum over the finite nonempty index set.S : Finset (Fin n), ξ : Fin n → Fin n and g : Fin n → ℝ. Only the values of ξ on S are meaningful; injectivity on S is a property to be proved, not a field.AuctionStep), with the choice of bidder, of and of existential. A run of iterations is a sequence of states starting from , ; it is terminated when at step . The results hold for every run, whatever the tie-breaking.Contributions welcome: the injectivity invariant of ξ on S as a reusable lemma; the milestones in any order; a proof of termination (the companion) and of the existence of a terminated run for every .
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.
A buyer can reduce production cost by using a supplier whose operations carry a risk of a responsibility violation. That choice can also bring a direct penalty and cause customers to leave. Guo, Lee, and Swinney study how the cost saving, consumer demand, and violation risk jointly determine the buyer’s sourcing decision in a transparent supply chain. Their model distinguishes customers who value responsible production from those who do not, making it possible to ask when the buyer uses a responsible supplier, a risky supplier, or both. The question concerns supplier selection when the buyer knows each supplier’s responsibility type and customers can react to a violation. Guo, Lee, and Swinney (2016) give the model and its four strategy regions.
A single buyer sells to a market whose total size is normalized to one. A responsible supplier has marginal cost and no responsibility violation in the model. A risky supplier has lower marginal cost and a violation occurs with probability . Write for the responsible supplier’s cost premium. A violation costs the buyer a fixed amount .
Every consumer has baseline willingness to pay . A fraction is socially conscious and has additional willingness to pay for a responsibly sourced product. Upon a violation, a fraction of this group exits the market. The remaining fraction has no responsible-sourcing premium and does not exit for that reason. These symbols and ranges follow the paper’s Section 3; the theorem adds no sign restriction to , , or .
The buyer chooses among four sourcing strategies. Low-cost sourcing (LC) uses the risky supplier for the whole market. Dual sourcing (DS) serves socially conscious consumers with responsible units and other consumers with risky units. Responsible niche sourcing (RN) serves only socially conscious consumers with responsible units. Responsible mass market sourcing (RM) serves everyone with responsible units. With denoting strategy ’s expected profit, Table 2 gives
A strategy is optimal when its profit is at least the profit of each of the four strategies. This definition allows ties. In the statements below, , as defined immediately before Proposition 1. Section 4 and Table 2 are the sources for these formulas.
The goal is all four clauses of Proposition 1, p. 2729, as printed. For LC, the sufficient conditions are
For DS, they are
For RN, the threshold is ; for RM it is . Each of these last two clauses also requires that neither LC nor DS be optimal. They are stated for , since their displayed quotient is undefined at zero. The six milestones record the pairwise strategy comparisons stated in the appendix proof, in its order: LC with DS, RM, and RN; RN with RM; and DS with RN and RM. Proposition 1 and its appendix proof supply these targets.
The proposition partitions the buyer’s decision into explicit sufficient regions. It identifies when the low cost of risky sourcing outweighs expected violation costs, when serving both segments separately pays, and when responsible sourcing should serve only the conscious segment or the full market. The four profits also provide the base for the paper’s later comparative statics on sourcing quantities, penalties, and transparency. Those later propositions are outside this mission; their exact treatment of strategy ties and sourcing quantities warrants a separate development. Guo, Lee, and Swinney (2016) establish these results in the published article.
The mathematical result is proved in that article. The formalization task is to give its parameter ranges, four profits, and optimality claims a machine-checkable statement, then prove the pairwise comparisons and the four-clause goal. The draft statements compile locally, but their proofs are open. The resulting model and comparisons can support later formalizations of the article’s other propositions.
The four choices must be compared under a single, consistent profit table. A comparison with one competitor does not establish optimality among all four, and the positive-part term in Proposition 1 compresses two distinct comparisons into one threshold. Boundary cases also matter: a strict “preferred to” comparison can disappear when its profit difference is zero, even though weak optimality remains meaningful. The printed sufficient condition in part (ii) uses inside the violation term, while the appendix’s DS comparisons use . Both statements must retain their respective printed forms; treating them as the same expression would change the source claim.
Lean represents the eight parameters by real fields of one record and the four strategies by a finite inductive type. The range assumptions are and . The cost premium is defined from the two costs. The theorem compares exactly the four Table 2 profits; the Section 3–4 derivation of prices and quantities from the underlying selling game is outside this mission. An optimal strategy is weakly best against all four strategies, including itself. A model with fewer competitors or profits that differ from Table 2 would not capture the proposition.
The clauses containing division by require . The appendix’s strict LC–DS equivalence additionally requires and ; otherwise equal profits can defeat its “if and only if” wording. Proposition 1 itself retains the full standing ranges. No positivity of , , or is assumed. Part (ii) retains the printed , which makes its hypothesis stronger than the corresponding appendix conditions with . Its conclusion remains valid under the standing ranges. These conventions are visible in the statements and can be checked independently of the paper’s informal derivation.
The development needs only real arithmetic, finite case analysis, the four profit definitions, and the maximum of a real number with zero. The parameter record and strategy comparison interface are reusable for later propositions in the same paper. Contributions that prove the exact milestone statements, establish the goal, or clarify behavior at ties are within scope.
A large share of the optimization problems solved in statistics, signal processing and machine learning have the composite form
where is smooth and is convex but possibly nonsmooth or extended-valued (a norm penalty, the indicator of a constraint set). The workhorse algorithm for such problems is the proximal gradient method, which takes a gradient step on followed by a proximal step on . Its worst-case rate on convex problems is sublinear, yet in practice it often converges linearly. The classical explanation, going back to Luo and Tseng (1993) Ann. Oper. Res. 46, is an error bound condition: near the solution set, the distance to the minimizers is controlled by the length of the algorithm's own step. Under such a condition the method converges linearly.
The difficulty is that the error bound is stated in terms of the algorithm, not the problem. Drusvyatskiy and Lewis (arXiv:1602.06661, Math. Oper. Res. 43(3), 2018) showed that, for convex problems, it is equivalent to a purely geometric property of : quadratic growth away from the set of minimizers. This mission formalizes that equivalence (§3 of the paper) together with the three comparison results that build it.
Write for Euclidean space with norm , , and . A function is closed if it is lower semicontinuous. For real , the sublevel set is .
The problem is (3.1): is a closed convex function, and is convex, -smooth, with -Lipschitz gradient, . Let be the (nonempty) set of minimizers of and its minimal value. For the proximal map is
the proximal gradient method iterates , and the prox-gradient mapping is
so that and exactly at minimizers.
For , has quadratic growth with constant if on (3.12), and the error bound condition with parameters holds if on the same sublevel set (Definition 3.1, (3.13)).
for every step size and every .
For a closed convex with minimizers and minimal value :
The result. Corollary 3.6 converts a condition on an algorithm into a condition on the objective. Quadratic growth can be checked by hand in many models (strongly convex losses, polyhedral problems, problems with a sharp minimum), and once it holds, Theorem 3.2 gives linear convergence of the proximal gradient method with an iteration count of order , matching the rate familiar from strongly convex problems. The rest of the paper uses this equivalence as its main tool: §4 proves quadratic growth for structured problems under dual strict complementarity, and §§5–8 extend the comparison to prox-linear methods for nonconvex compositions. Theorems 3.3 and 3.4 are statements about a single closed convex function and are of independent use in the analysis of proximal point methods.
Formalizing it. All results here are proved on paper; none of them is machine-checked. The mission produces a Lean statement of the equivalence with the paper's explicit constants, and of the step-length comparison between the forward-backward and the proximal point methods for maximal monotone operators. Formal proofs require the existence, uniqueness and nonexpansiveness of resolvents and proximal maps, the subdifferential sum rule for a smooth plus a convex function, and a quadratic growth argument for convex functions; these are reusable well beyond this paper.
The forward direction is a chain of three inequalities, but each link compares objects that live in different worlds: the subdifferential of , the proximal map of , and the proximal map of evaluated at a gradient-shifted point. The proximal gradient step is not the proximal point step on , and the obvious attempt to compare with directly gives only one inequality (3.10); the reverse comparison (3.11) needs the resolvent of the sum and the Lipschitz constant of . The converse half of Theorem 3.3 (error bound implies growth) is the deepest step: the paper omits its proof and cites Drusvyatskiy–Ioffe and Drusvyatskiy–Mordukhovich–Nghia. It has to pass from a pointwise bound on subgradients to a bound on function values over the whole sublevel set, which no single subgradient inequality provides.
EuclideanSpace ℝ (Fin n); -valued functions are EReal-valued; is real-valued and is computed in EReal. "Closed convex" is the published RockafellarMaxMono.Shared.ProperConvex (never , somewhere finite, convex) together with LowerSemicontinuous.Metric.infDist; is real.GoldenRatioVI.Shared.IsProxPoint (fun y => t * g y) z p (same argmin for ), and resolvents are maps satisfying the published ThreeOpSplitting.Convergence.IsResolvent. Conditions are stated for every such point; existence and uniqueness are facts a solver proves.Metric.infDist 0 (∂h x), which is on the empty set, would turn (3.7) into the false claim that every point of the sublevel set where is empty is a minimizer; this trivializing or falsifying encoding is ruled out.ProxAlg.FixedPoint.subdifferential, the gradient is Mathlib's gradient.Contributions welcome: proofs of the milestones in any order, general lemmas on resolvents of maximal monotone operators and on proximal maps of EReal-valued convex functions, and a proof of the converse half of Theorem 3.3.
Nesterov's accelerated gradient method minimizes a smooth convex function at the rate in the number of iterations , against for plain gradient descent. Su, Boyd and Candès (arXiv:1503.01243) observed that, as the step size tends to zero, Nesterov's scheme becomes the second-order differential equation
with , a heavy-ball system whose friction coefficient vanishes as (asymptotic vanishing damping). Studying (1) in continuous time gives Lyapunov arguments that are then discretized into new algorithms.
Attouch, Chbani, Peypouquet and Redont (Math. Program. 168 (2018), DOI 10.1007/s10107-016-0992-8) analyse (1) for general . This mission formalizes their result for strongly convex , where the rate of convergence of (1) depends on and improves without bound as grows.
Timeline.
Let be a real Hilbert space with inner product and norm , and let be continuously differentiable with gradient . Fix and . A solution of (1) is a twice differentiable trajectory with velocity satisfying (1) at every .
is strongly convex with constant if
Such a has exactly one minimizer , and .
For , the anchored energy is
a sum of nonnegative terms. The proof of the main theorem fixes
For strongly convex and , every solution of (1) converges strongly to the unique minimizer , and
as . The goal states the asymptotic form; the explicit constants are milestones.
The theorem shows that the rate of (1) on strongly convex functions is not capped at or : the exponent grows linearly in , and it already exceeds for every . It extends [44, Theorem 4.2], which needs and gives . The same parametrized energy is the template for the discrete analyses of Nesterov-type algorithms with parameter , so its derivative identity (10) is reusable beyond this mission.
The result is proved on paper. To the best of current knowledge none of it is formalized: Mathlib has no theory of inertial dynamics, and the platform's strongly convex rates concern discrete methods. A completed mission gives a machine-checked Lyapunov analysis of a non-autonomous second-order ODE in a Hilbert space, with the explicit constants of the paper.
The derivative identity (10) is a computation, but it must be carried out with one-sided derivatives at , real powers , and the chain rule for in an infinite-dimensional space. The obvious argument, that is nonincreasing, fails: even with the best choice of and the bound on its derivative keeps a term of no fixed sign, and only for is the quadratic term in nonpositive. Passing from the differential inequality to (26) therefore needs integration on for functions known only through one-sided derivatives. The velocity bound then combines (26), (27) and (28) through square roots, and the goal additionally requires the existence of the minimizer in an infinite-dimensional space, which is a compactness argument (weak lower semicontinuity) and not an algebraic one.
InnerProductSpace ℝ H, CompleteSpace H), not . is ContDiff ℝ 1 and is Mathlib's gradient.Asymptotics.IsBigO along atTop; strong convergence is norm convergence. The existence and uniqueness of are conclusions of the goal, not hypotheses, so the goal cannot be satisfied vacuously by an empty argmin; the strong-convexity hypothesis is satisfiable (e.g. with , and solves (1)).Useful infrastructure: the derivative of via gradient, integration of differential inequalities on , and existence of minimizers of strongly convex continuous functions on Hilbert spaces. Proofs of any milestone, and of the goal from the milestones, 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 .