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.
Track exact exponent savings κ for integer multiplication in time, where . Higher κ is better. Every entry uses the same public IntMul.KappaBound definition: one deterministic machine, a fixed finite alphabet and tape count, exact multiplication for every positive input length, and an eventual worst-case time bound.
Avi’s Harvey–van der Hoeven mission supplies the shared foundation. Its main goal uses the natural-logarithm formulation of the 2021 bound, so it serves as the foundation rather than a numeric entry. Avi’s positive-κ mission targets Jain’s round-six value 0.00003666565558019; it is a historical checkpoint. The reviewed community PR #62 checkpoint targets 0.000051016920170078. Open entries record goals to prove, not established records. The full multiplication theorem remains Open even when finite numerical certificates have been verified.
Community checkpoint and credits · Original framework · Harvey–van der Hoeven
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?
Linear convergence of first-order methods is usually proved through an error bound: near a solution, the distance to the solution set is controlled by the size of a computable residual, such as the length of a proximal-gradient step. For the prox-linear method, which minimizes a composition of a nonsmooth outer function with a smooth map by repeatedly solving the subproblem obtained from linearizing , Drusvyatskiy and Lewis showed in §5 of their paper (arXiv:1602.06661, Theorem 5.10) that the error bound is equivalent to subregularity of the subdifferential , a property of the objective alone and closely tied to quadratic growth. That result needs convex and finite-valued.
Many composite models violate both assumptions: constraints enter as indicator functions ( off a set), and outer functions such as truncated or concave-composite penalties are nonconvex. §8 of the paper extends the equivalence to closed, extended-real-valued, prox-regular . This mission formalizes that extension (Theorem 8.11) together with the results of §8 its proof rests on.
Fix a -smooth map and a closed (lower semicontinuous) function , and consider
The linearized function is and, for , .
Subgradients are built in three layers (Definition 8.1). A vector is a proximal subgradient of at ( finite) if for some and all near . The limiting subdifferential collects limits of proximal subgradients with ; is stationary if . The horizon subdifferential collects limits of with , , .
The map is transverse to at , written , if (8.3). The stationary point map is the set of stationary points of , and the prox-gradient mapping is ; both are set-valued.
A set-valued map is subregular at with constant if for near (Definition 5.7), and metrically regular around if the same holds with replaced by every near (Definition 8.3). A closed is prox-regular at for if the quadratic minorant holds uniformly for near with near and near (Definition 8.7). Finally, a -attentive localization of around is a map agreeing with near whenever is near and is near ; a -attentive localization of agrees with at points near with near , and one of has the form with such a localization of (Definition 8.10).
Assume , , Lipschitz around , and prox-regular at for every with . Let (i) be "some -attentive localization of is subregular at " and (ii) "some -attentive localization of is subregular at ". Then
and, when is convex, is subregular at if and only if is, for every . The constants of subregularity are left existential: the goal asserts the shape of the equivalence, not a particular constant.
Subregularity of at is exactly the error bound property of the prox-linear step, the hypothesis under which linear convergence arguments run. Theorem 8.11 says that, for the attentive parts of the graphs, this property is equivalent to subregularity of , which does not refer to any algorithm or step size. It therefore covers constrained composite problems (indicator functions ), nonconvex prox-regular penalties, and, in the convex case, removes the finite-valuedness assumption of Theorem 5.10.
The results are proved in the paper, partly by citation to Dontchev, Lewis and Rockafellar and to Lewis and Wright's analysis of prox-linear subproblems (arXiv:0812.0423). None of them is formalized: Mathlib has no proximal, limiting or horizon subdifferential, no metric regularity, and no prox-regularity. A formalization supplies these notions, checks the constant-chasing in Theorems 8.9 and 8.11, and fixes the precise quantifier order the prose leaves implicit.
The obvious route, copying the §5 argument, fails at its first step: §5 starts from the inequalities , and when takes the value one of , can be finite while the other is infinite, so no such inequality holds. Theorem 8.6 replaces it by a comparison after perturbing , which needs the stability of metric regularity (Theorem 8.4) and the epigraphical description of subgradients. A second obstacle is that collects stationary points of nonconvex subproblems, so it is set-valued and possibly empty; the proofs need prox-regularity that is uniform over the family (Proposition 8.8) and a local existence result for to obtain the threshold . The limiting-subdifferential calculus (the chain rule under transversality) is itself a substantial piece of variational analysis.
Points are in EuclideanSpace ℝ (Fin n); , , and are EReal-valued. Standing assumptions on every statement: is (ContDiff ℝ 1 c), is lower semicontinuous and never (the page's closed functions are only ever evaluated where finite or ; this is a disclosed addition). is fderiv ℝ c x and its adjoint. "" requires finite. , so (sub)regularity inequalities are stated for every element of , and metric regularity carries nonemptiness of ; is the existence of a subgradient of norm at most . and are sets defined by stationarity, never a chosen minimizer. Two printed slips are corrected and disclosed: in Definition 8.10 (2) the neighbourhood is a neighbourhood of , and in Theorem 8.11 the threshold satisfies (with the converse would be vacuous). "When is convex" is the convexity inequality in , with the theorem's other hypotheses kept.
A trivializing formalization is ruled out: subregularity always includes , a constant and a neighbourhood, so the content of (i) and (ii) cannot collapse into the trivial existence of a localization (any map is a localization of itself); and distances to empty sets are never junk zeros.
A complete development needs the three subdifferentials and their basic calculus (sum rule with a smooth function, chain rule under transversality, closedness of the limiting subdifferential), metric regularity and its perturbation stability, Ekeland's variational principle (on the platform as EkelandVP.General.ekeland_variational_principle), and a local existence result for stationary points of the subproblems. The subdifferential and regularity layer is reusable well beyond this mission. Proofs of any milestone, and of supporting lemmas on the variational-analysis substrate, are welcome.
Approximating an unknown probability measure by the empirical measure of an i.i.d. sample is the basic operation of statistics, Monte Carlo integration, quantization and particle approximations of nonlinear PDEs. The natural way to compare with on is an optimal-transport cost, because it metrizes weak convergence together with convergence of moments. For many applications the mean of this cost is not enough: one needs to know how unlikely a large deviation is, for a fixed sample size .
The main consumer in operations research is data-driven distributionally robust optimization. Mohajerin Esfahani and Kuhn (Math. Program. 171, 2018) build Wasserstein balls around whose radius is calibrated so that the true distribution lies inside with probability ; their finite-sample guarantee (their inequality (7), quoted from this paper for ) is exactly a concentration inequality of the kind proved here. On Prove2Me that inequality appears as the hypothesis Concentration7 of WassDDRO.Consistency.Setting; Theorem 2 of this mission is the statement that discharges it.
Timeline. Bolley, Guillin and Villani (PTRF 137, 2007) proved concentration inequalities for on non-compact spaces, under assumptions that often included functional inequalities for , and for rather large deviations. Boissard (Electron. J. Probab. 16, 2011) gave bounds in for empirical and occupation measures. Boissard and Le Gouic (arXiv:1105.5263) and Dereich, Scheutzow and Schottstedt (Ann. IHP 49, 2013) studied the mean speed of convergence; the latter introduced the multiscale bound used here and obtained sharp moment estimates for a limited range of parameters. Fournier and Guillin (arXiv:1312.2128, 2013; PTRF 162, 2015) gave moment bounds for all and under a -th moment (their Theorem 1, mission I of this series) and the concentration inequalities of their Theorem 2, the subject of this mission, under integrability conditions only.
Fix and give the Euclidean norm . Let be a Borel probability measure on and i.i.d. with law . For the transport cost between probability measures is
where is the set of couplings, measures on with marginals and (no root is taken). The moment conditions use
The proof works with a multiscale distance . For let be the partition of into dyadic cubes of side . For measures on ,
For measures on one cuts space into the shells , , rescales each to (the measure ), and sums the compact distances with weights . Lemma 5 bounds by . The splitting separates the fluctuation of the shell masses, , from the fluctuation inside the shells, . A Poisson measure with intensity (a Poisson() number of i.i.d. points) and enter the compact case.
Assume or , and one of (1) with ; (2) with ; (3) with . Then for all , ,
with , or according as , , , and under (1), under (2), under (3). The constants depend only on , the parameters of the condition, the value of the moment and .
In attack order: Lemma 5 (the coupling bound ); Lemma 9 (Poisson moment generating function and tails); Proposition 8 (concentration for in the Poissonized compact case); Lemma 11 ( for ); Proposition 10 (the compact case of Theorem 2, ); Lemma 12 (binomial deviations); Lemma 13 (the tail of ); display (6) ().
The result. Theorem 2 gives, for every dimension and every in its range, a deviation inequality whose small- part has the same dimension-dependent exponent as the mean rate of Theorem 1, and whose large- part is governed only by the tail of . Under exponential moments the tail is again exponential; under a polynomial moment it is polynomial, which is the correct order. It is the input for finite-sample confidence radii in Wasserstein DRO, for non-asymptotic guarantees in quantization and for propagation-of-chaos estimates.
Formalizing it. The theorem is proved (2013, published 2015) and widely cited; no machine-checked proof of it, or of any rate for the empirical measure in transport cost, exists in Mathlib or on Prove2Me. The work is formalizing the known proof: Poisson and binomial concentration (Lemmas 9, 12), the local Poisson bound (Lemma 11), Poissonization and depoissonization (Propositions 8, 10), and the shell decomposition (Lemma 13, display (6)). Lemmas 9, 11 and 12 are general probability facts useful well beyond this paper.
The obvious route is a bounded-differences (McDiarmid) inequality for . On it is not available: moving a single sample point changes the cost by an amount that is unbounded, and the measures allowed here have only exponential or polynomial moments. Even on a compact set it bounds the deviation from the mean rather than from , so it gives nothing below the mean rate, and it does not see the dimension-dependent exponent of . The bound must hold at all scales of the dyadic decomposition simultaneously, while the cell counts of a multinomial sample are dependent, and in the non-compact case the masses of far-away shells, which are rare events, must be controlled with a tail that degrades exactly as the moment condition allows.
is EuclideanSpace ℝ (Fin d) with ; the Euclidean norm matters, since involves the diameter of . The sample is under the product measure , and is the published WassersteinDRO.Duality.empiricalDistribution; couplings are the published WassersteinLinOpt.Ball.couplings. Costs, moments, , , and expectations are valued in (lower Lebesgue integrals and -valued series), so no bound can hold through a junk value of a divergent integral. Probabilities are the product measure applied to the event. is represented by its law, a Poisson() mixture of i.i.d. samples, as on p. 13. Poisson and binomial laws are Mathlib's poissonMeasure and binomial.
Constants: in each of the three parts, the condition's parameters, the moment value (resp. ) and are fixed before , and come after. A formalization with fixed before the constants would be trivial (the constants could absorb ), and one stating the goal as the sum of the bounds for and would assume the proof; the goal mentions neither , , nor .
Departures from the print, each disclosed in the statements: the page writes for ; Theorem 2 opens with "" but prints only for , , , so it is posed for or ; Proposition 8's "" is relaxed to that range (its proof does not use , and Theorem 2 needs it for every ) (Proposition 10 is posed, as printed, for every ); Lemma 12 assumes and a positive success probability, without which (a) and (b) are false. "Supported in " is -null complement of .
The definitions of , , Notation 4 and Lemma 5 duplicate those of mission I of the series and are to be merged later. Contributions on Poisson and binomial concentration, and on transport costs between discrete measures, are reusable and welcome.
Peaceman–Rachford splitting separates the minimization of a sum into two proximal computations. That matters when each summand has a tractable proximal map but the sum does not. Douglas–Rachford splitting is its half-relaxed instance, and related iterations appear in the analysis of ADMM. Davis and Yin study how regularity of the two summands changes the rate at which a relaxed Peaceman–Rachford iteration approaches a fixed point. Their Section 4 distinguishes two arrangements: one summand may carry both strong convexity and a Lipschitz gradient, or the two properties may be shared between summands. The mixed case of Theorem 4.3 is the target of this mission. The authors describe it as a new result in the preprint version used here. Davis and Yin, §4, pp. 13–16.
Let be a real Hilbert space and let be proper, closed, convex functions. For a step size , the proximal map takes a point to the minimizer of ; define similarly. The reflection associated with a proximal map is . The Peaceman–Rachford operator is . Its relaxed iteration, Algorithm 1 of the paper, is
The analysis fixes a point satisfying and writes . It also uses the two proximal points and . Their selected proximal subgradients are and . Lemma 1.1 states that they belong to the respective convex subdifferentials and relates them to the iteration. These are selected subgradients, rather than arbitrary members of a set-valued subdifferential. Davis and Yin, §1.2 and Lemma 1.1, pp. 4–7.
A function is -strongly convex when its convexity inequality improves by the quadratic term . A -Lipschitz gradient means the function is real valued, differentiable, and , with . Section 1.10 also permits the parameters and to be zero when a property is unavailable. Its auxiliary term is the maximum of a squared-point-distance term weighted by and a squared-selected-subgradient-distance term weighted by . The one-step bound (2.1) controls the sum of the corresponding terms for and . Davis and Yin, (1.13)–(1.14) and (2.1), pp. 7–8.
Suppose . The goal covers both arrangements: is -strongly convex while has a -Lipschitz gradient, and the arrangement with and exchanged. In either case the target is
The factor is the paper's explicit factor, for . It is strictly below one for with fixed positive regularity parameters; at it equals one. A uniform geometric rate therefore requires relaxation parameters to remain in a range where these factors have a uniform upper bound below one. Davis and Yin, Theorem 4.3, p. 16.
Theorems 4.1 and 4.2 give the explicit factors when , or respectively , supplies both properties. Proposition 4.1 translates a fixed-point contraction sequence into bounds on the proximal points, selected subgradients, fixed-point residual, and objective error. These are companion items in the proposal. The milestone list follows Lemma 1.1, the auxiliary bound (2.1), and the displayed estimates (4.6) and (4.7) from the proof of the mixed case. Davis and Yin, Proposition 4.1 and Theorems 4.1–4.3, pp. 13–16.
Theorem 4.3 identifies a rate available when neither summand alone carries both regularity properties. The explicit dependence on , , , and lets a reader compare choices of step size and relaxation without hiding them in an unspecified constant. Proposition 4.1 explains what a contraction in the auxiliary fixed-point variable says about the quantities used to judge an optimization method: proximal point error, residual, and objective error. The distinction between a per-step bound and a uniform geometric rate is part of the mathematical result.
The inequalities are proved in the source paper; the remaining work here is to give their statements and eventual proofs a machine-checked account. The shared setting makes the proximal operator, selected subgradients, and regularity terms explicit, so the same formal definitions can be used across this mission's estimates. The two external platform definitions cited by this development already provide the closed proper convex class, proximal-map predicate, smooth convex class, and subdifferential. The results in this proposal are open Lean statements until solvers supply proofs.
Strong convexity and Lipschitz smoothness control different quantities in the mixed case. The decrease inequality directly bounds distances between proximal points and between gradients, whereas the desired conclusion concerns . Treating merely as a nonexpansive operator yields no factor below one. The displayed estimate (4.7) expresses the fixed-point distance through the quantities controlled by (4.6). The proof must also identify the proximal subgradient of the smooth summand with its ordinary gradient, rather than assume that identity as part of the goal. Davis and Yin, proof of Theorem 4.3, p. 16.
The Lean carrier is a complete real inner-product space, including the zero space. The functions take values in EReal to represent outside their effective domains. The published IsProperClosedConvex, IsProx, IsSmoothConvex, and subgrad definitions supply the common function and operator conventions. A proximal map is passed as a function together with a proof that it minimizes the defining objective; under the standing assumptions it is uniquely determined. Every result involving a proximal map assumes . Run statements require , and the mixed theorem requires . The goal has no hypothesis asserting any of its decrease estimates or a contraction; those are results to establish.
The contraction factors use Real.sqrt. For the mixed and -regular factors, the radicands are positive throughout the relaxation range. For the -regular factor, its nonnegativity follows from the compatibility of positive strong convexity and gradient Lipschitz parameters on a nonzero space; the zero space makes the contraction statement trivial even if that radicand is negative. Objective errors use real values only at proximal points where both summands are finite. The milestone (2.1) uses the paper's selected proximal subgradients. Proving the link between smooth gradients and those subgradients, and reusable proximal-map inequalities, are welcome contributions beyond the four named milestones.
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.
Many large optimization problems in signal processing, statistics and machine learning have a variable that splits naturally into blocks, and are solved by updating one block at a time. The classical method of this kind, block coordinate descent (BCD), minimises the objective exactly in one block while the others are held fixed. In practice the exact block subproblem is often too expensive, and one minimises instead a simpler function that upper-bounds the objective and touches it at the current point. The EM algorithm, DC (difference of convex) programming, proximal and linearised block updates and several alternating schemes for matrix factorisation and transceiver design are all of this form.
Razaviyayn, Hong and Luo (arXiv:1209.2385, SIAM J. Optim. 23 (2013)) gave one convergence analysis for this whole family, the block successive upper-bound minimization (BSUM) method, without convexity or smoothness of the objective. This mission formalizes the block part of that analysis: the cyclic BSUM method (Theorem 2) and its maximum-improvement variant MISUM (Theorem 3).
Timeline. Bertsekas (Nonlinear Programming, 1999, Prop. 2.7.1) proved that limit points of cyclic BCD are stationary for continuously differentiable objectives over a product of closed convex sets when each block minimiser is unique. Tseng (J. Optim. Theory Appl. 109, 2001) treated nondifferentiable objectives using regularity and coordinatewise minima. Chen, He, Li and Zhang (SIAM J. Optim. 22, 2012) introduced maximum block improvement, which drops the uniqueness assumption. The 2013 paper extends these results from exact block minimisation of to minimisation of block upper bounds.
The problem is
where each is a closed convex set and is a continuous real function on . A point is with . The directional derivative is , a value in . A point is stationary for (12) if for every with . The function is regular at if holds for every such that for every block . A point is coordinatewise stationary if for every with , for every .
For each block an approximation function is given, with and . Assumption 2 requires:
The BSUM algorithm (Fig. 2) starts at and, at each iteration, picks a block by the cyclic rule, replaces by any minimiser of over , and keeps the other blocks. The MISUM algorithm (Fig. 3) instead updates a block attaining .
If each is quasi-convex in , Assumption 2 holds and every block subproblem , , has a unique solution, then every limit point of the cyclic BSUM iterates satisfies
and is a stationary point of (12) if is regular at .
The proof passes through the monotonicity (14); the limit at a limit point (15); the claim that forces ; block minimality for all and every ; and the first-order condition for feasible (22).
Theorem 2(b): if the level set is compact, block minimisers are unique in at least blocks and is regular on , then , where is the set of stationary points. Theorem 3: under Assumption 2 alone, every limit point of the MISUM iterates is coordinatewise stationary, and stationary where is regular.
Theorem 2 is the stationarity guarantee for every method that can be written as cyclic block minimisation of tight upper bounds: block EM, alternating DC iterations, proximal block updates, and the matrix-factorisation and beamforming schemes of Section VIII of the paper. Each such method needs only a check of (B1)–(B4) to inherit it. Theorem 3 shows that the uniqueness assumption, which part (a) needs and BCD needs too, can be traded for a greedy block choice.
The results are proved in the paper. As far as the platform's catalogue shows, none of them has been formalized; the related published work is the formalization of Tseng's 2001 setting (directional derivative, stationarity, regularity, cyclic rule), which this mission reuses. Formalizing the analysis checks the "without loss of generality" and "by further restricting to a subsequence" steps, which carry most of the argument, and gives reusable statements about limit points of block methods.
The obvious argument shows that decreases and that a limit point satisfies the block optimality condition for the block updated along the convergent subsequence. It does not say anything about the other blocks: consecutive iterates may stay a fixed distance apart, so the next iterate need not converge to , and then nothing is known about in the next block. Showing that is the central step, and it is exactly where quasi-convexity and uniqueness of the block minimisers are used. Without uniqueness, limit points of even exact cyclic BCD need not be stationary (Powell's examples, which the paper cites), which is why Theorem 2(b) needs compactness and Theorem 3 needs a different update rule.
The step from block minimality to stationarity is a second gap: (B3) only matches derivatives in coordinate directions, and passing to all directions requires regularity of .
The space is the dependent product X n of the referenced Tseng setting, with blocks indexed (paper block is index ). It carries the sup norm over blocks, which matters only for distances; convergence statements do not depend on the norm. The block sets are closed and convex, is a real function continuous on , and ; these standing hypotheses of Section IV appear in every statement.
The paper assumes . Accordingly is extended by off , and stationarity and regularity are those of the extension. Directional derivatives are extended-real liminfs, never real-valued limits with a junk value. A run is a predicate on a sequence: each new block is a minimiser of the block subproblem, but existence of minimisers is not assumed. The cyclic rule updates block on the step , a relabelling of Fig. 2's . Limit points are cluster points of the sequence.
Deviations from the printed statements, each disclosed in the items:
Trivializing formalizations are ruled out: hypotheses on are required on all of , not just along the run; uniqueness is required at every ; and a sorry-free check shows that all hypotheses of Theorem 2(a) hold together for a one-block instance.
Not formalized: Proposition 2 (a sufficient condition for (B3)), Corollaries 2 and 3 (essentially cyclic and overlapping rules) and the applications of Section VIII. Contributions of reusable lemmas about cluster points of block methods and first-order conditions for constrained minimisers in a single block 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.
Mean field games (Lasry–Lions 2006–2007; Huang–Malhamé–Caines 2006) describe Nash equilibria of games with a very large number of symmetric players, each interacting with the others only through the empirical distribution of their states. When all players are also exposed to a common noise, the equilibrium is no longer described by a forward–backward pair of PDEs but by a single equation on the space of probability measures, the master equation. The master equation is the object that lets one prove convergence of -player equilibria to the mean field limit (Cardaliaguet–Delarue–Lasry–Lions 2019), so a global classical solution is the starting point of that theory.
Global well-posedness requires a monotonicity condition; without one, uniqueness of equilibria fails. Before this paper, global results were known under the Lasry–Lions monotonicity condition and for separable Hamiltonians , and under displacement convexity in deterministic potential games (Gangbo–Mészáros 2022). Gangbo, Mészáros, Mou and Zhang (Ann. Probab. 50 (2022)) prove global well-posedness for nonseparable Hamiltonians under displacement monotonicity, a condition that is different from Lasry–Lions monotonicity and that has a natural extension to Hamiltonians depending jointly on .
Let be the Borel probability measures on with finite second moment, with the 2-Wasserstein distance . For , the Lions derivative is characterized by
The class consists of continuous for which , , , , and exist and extend to jointly continuous functions of all their arguments.
The data are a horizon , a common-noise intensity with , a Hamiltonian and a terminal cost . The master equation on is
with the nonlocal operator
where are independent with law . A classical solution is a satisfying the equation on and the terminal condition.
is displacement monotone (2.16) if for all square-integrable with and an independent copy ,
The Hamiltonian is displacement monotone (Definition 3.4) if a bilinear form built from , and a correction is nonpositive, with for every bounded Lipschitz map . Assumptions 3.1 and 3.2 impose regularity and bounds on and ; Assumption 3.5 imposes the two monotonicity conditions.
Under Assumptions 3.1, 3.2 and 3.5, the master equation on has a classical solution with bounded , , , , and it is the only classical solution in that class:
The theorem gives global classical well-posedness of the master equation with common noise for a class of Hamiltonians that need not be separable and data that need not be Lasry–Lions monotone. A classical solution is what the convergence analysis of -player games and the construction of approximate equilibria take as input. Theorem 4.1, displacement monotonicity propagating backward along the equation, is the central structural fact; Theorem 5.1 converts it into an a priori Lipschitz bound in that is uniform in time, which is what allows local solutions to be continued.
The result is proved in the paper; nothing in this mission is open mathematically. No part of it is formalized anywhere. The mission produces a formal statement of the master equation, its classical solutions and the displacement monotonicity conditions, plus targets for a machine-checked proof. Calculus on Wasserstein space with Lions derivatives is absent from Mathlib, so even Lemma 2.1 requires new infrastructure.
Local well-posedness holds for any regular data; the obstacle is continuing the solution to the whole interval. The length of the local interval depends on the Lipschitz constant of the terminal data in , and without a uniform-in-time bound on that constant the local intervals can shrink to zero. Lasry–Lions monotonicity is not available here, and for nonseparable it has no obvious analogue. Any argument that controls this constant has to work with second-order Lions derivatives, which needs full regularity in the measure variable. That regularity is itself only known on short intervals.
EuclideanSpace ℝ (Fin d). is a subtype of measures, so functions of are defined only on . is the published WassersteinDRO.Duality.wassersteinDistance with , converted to a real number.A large stochastic game has one state process per player. Each player's feedback changes with the empirical distribution of all states, so a finite population remains coupled even when the idiosyncratic Brownian motions are independent. A useful quantitative question is whether a statistic of the entire collection of equilibrium trajectories can deviate substantially from its mean as the population grows. Delarue, Lacker, and Ramanan answer this for smooth closed-loop mean-field games in their large-deviations and concentration paper. Their result concerns the equilibrium state paths themselves, rather than only a fixed-time empirical measure.
The paper is part of a two-paper limit theory. Its companion central-limit paper supplies the Nash-to-McKean–Vlasov estimates quoted here as Theorems 4.1 and 4.2. The concentration argument also uses transport inequalities: Gozlan's dimension-free characterization explains the quadratic transport assumption on the initial law, while Djellout, Guillin, and Wu provide a transport principle for diffusion path laws. The present mission records the paper's main concentration theorem and four of its explicit intermediate targets.
Fix a horizon and a positive state dimension . Player has a continuous state path . The empirical measure of a vector is ; the same formula applies to paths. The norm on is , and the product norm relevant to this mission is .
The game is posed on a filtered probability space with a common Wiener process , independent idiosyncratic Wiener processes , and i.i.d. initial states of law . The action space is Polish. A drift , running cost , and terminal cost specify the control problem. The Hamiltonian minimizes over actions; a selected minimizer defines and .
Classical solutions of the -player Nash system (2.6) determine the feedback in the equilibrium state equation (2.7). A classical solution of the master equation (2.8) determines the comparison particle equation (4.1). Both equations retain common-noise terms in their definitions. The goal sets the common-noise coefficient to zero. Assumption A imposes Hamiltonian attainment, Lipschitz , nondegenerate idiosyncratic diffusion, an initial moment above order four, and the stated classical solutions. Either B or B′ controls the selected running cost; B′ also bounds and as specified on pp. 8–9.
The goal is Theorem 3.4. If satisfies the quadratic transport inequality for every with finite second moment, then constants exist such that, for , , and every 1-Lipschitz on the product path space,
The four milestones retain the paper's two main comparison layers. Theorem 4.3 controls both the path-space Wasserstein distance between the Nash and comparison empirical measures and their synchronous squared path distance by for . Theorem 5.3 gives a dimension-uniform transport inequality and concentration bound for the law of a Lipschitz SDE in the coordinatewise product-supremum norm. Equation (5.7) bounds the change in a 1-Lipschitz path expectation when the deterministic initial vector changes. Theorem 5.4 gives for the interacting comparison system. The labels, constants, and domains follow the pinned preprint, pp. 12 and 16–20.
Theorem 3.4 supplies a finite-population tail estimate for every 1-Lipschitz observable of the entire equilibrium path vector. The first term becomes small at a population-dependent scale, while the second term has a rate independent of the number of players. This is stronger information than convergence of the empirical measure alone: it applies to path-dependent statistics and includes explicit deviation probabilities Theorem 3.4.
The mathematical statements are proved in the source paper, subject to its assumptions; Theorems 4.1 and 4.2 that support its comparison result are proved in the companion paper. The work here is to give these claims faithful machine-checkable statements and ultimately machine-checked proofs. The present draft is a set of open Lean theorem statements with sorry, so it asserts no completed formal proof. A completed development would also make its definitions of empirical path laws, Wasserstein continuity, flat derivatives, and interacting SDE solutions reusable for other mean-field models.
Independent-noise concentration cannot simply be applied to the Nash state paths. A player's drift depends on the empirical state measure and on a derivative of the -player Nash solution, so changing one input can change every trajectory. The master equation describes a comparison system, but using it requires matching the Nash and master feedbacks on the same filtered probability space. The regularity in Assumptions A, B, and B′ is substantial: the master field has first and second derivatives in both space and measure, with uniform bounds. A formal proof must also preserve the exact path norm and the population-independent placement of constants. The SDE transport theorem's uniformity over dimensions is particularly consequential for Theorem 5.4 §§4–5.
State vectors use finite-dimensional Euclidean spaces; time uses nonnegative reals and only is evaluated. A continuous path is a ContinuousMap on that interval with its supremum norm. Finite products use PiLp 2; the scalar-coordinate version of the norm is used for Theorem 5.3. Players are indexed from zero, corresponding to the paper's indices , and every theorem requires . Probabilities and entropy are extended nonnegative values. Transport distances stay extended until a finite-moment hypothesis justifies their real value.
The filtered Wiener processes, i.i.d. initial states, Borel coefficients, Polish action space, Nash and master PDEs, and either B or B′ are represented explicitly. The master equation is imposed on ; its spatial gradient is also required on , as Assumption A(5) specifies. A flat measure derivative is a normalized witness satisfying (2.2), while spatial derivatives are actual Fréchet derivatives. SDE solutions are path-valued processes satisfying coordinate Itô integral relations; solution families are supplied as hypotheses, since their existence is asserted by the source. Expectations appearing in the conclusions are stated integrable, so a default zero integral cannot satisfy a tail bound accidentally. The model cannot be replaced by arbitrary paths or a vacuous solution predicate: the Nash and comparison paths must satisfy their respective equations with the same noises and initial states.
The mission includes Theorem 4.3, Theorem 5.3, (5.7), and Theorem 5.4. The quoted Theorems 4.1 and 4.2, the general transport equivalence of Theorem 5.1, and tensorization in Theorem 5.2 remain useful later contributions, with their original hypotheses and conclusions intact. The printed constant in the “moreover” clause of Theorem 5.1 is omitted because it is dimensionally incorrect; no substitute assertion is placed in this mission.
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 .
Many problems in statistics, signal processing and machine learning minimize a smooth loss plus a nonsmooth regularizer over a set with manifold structure: sparse principal component analysis over the Stiefel manifold, sparse blind deconvolution over the sphere, and clustering and dictionary-learning models with orthogonality constraints. In Euclidean space the standard method for such composite problems is the proximal gradient method, whose rate for convex problems is classical (Beck–Teboulle 2009). Huang and Wei (arXiv:1909.06065v4, Mathematical Programming 2021) propose a Riemannian proximal gradient method (RPG) that solves its proximal subproblem on the tangent space and returns to the manifold through a retraction. They prove three things about it: global convergence, an rate under a convexity notion adapted to retractions, and local rates under a Riemannian Kurdyka–Łojasiewicz property. This mission covers the second result, Theorem 3.2.
Earlier Riemannian proximal methods either required the exponential map and parallel transport, or solved a Euclidean proximal problem in the ambient space (Chen, Ma, So, Zhang 2020, ManPG). Theorem 3.2 is stated for a general retraction, with an explicit constant.
Let be a finite-dimensional Riemannian manifold, with inner product and norm on each tangent space . A retraction is a family of smooth maps with and . The problem is
where is differentiable with Riemannian gradient , and is continuous and possibly nonsmooth.
For a function on a real inner-product space , the Clarke generalized directional derivative is . The generalized subdifferential is . A point is stationary for if .
Given a constant , the RPG method (Algorithm 1) produces iterates and steps as follows. Set
Choose a stationary point of on with , and set .
The assumptions involve the sublevel set and two notions defined with respect to on a set :
Assumption 3.1 asks that be bounded below and compact. Assumption 3.3 provides an open on which is -retraction-smooth and retraction-convex and is retraction-convex. Assumption 3.4 bounds how far the retraction is from Euclidean: for all ,
Finally, .
Let , suppose Assumptions 3.1, 3.3 and 3.4 hold, and let be any accumulation point of . Then for every
The constants are those of the paper.
Theorem 3.2 extends the function-value rate of the proximal gradient method to manifolds and general retractions. The constant is explicit: it combines the initial distance with a correction proportional to , which measures how far the retraction is from Euclidean. In the Euclidean case one can take , and the bound reduces to the classical one. The rate concerns , which the iteration bound of Theorem 3.1 (the norm of ) does not control.
The result is proved in the paper. None of it is formalized, and no machine-checked version of the Euclidean proximal-gradient rate is on the platform either. A formalization would supply the first checked version of Clarke stationarity on tangent spaces, of the retraction-based convexity and smoothness notions, and of a rate proof for a nonsmooth Riemannian algorithm. These pieces carry over to other retraction-based methods, such as the accelerated variants of §4 of the paper.
The arithmetic of the rate proof is a telescoping sum, so the work lies elsewhere. First, Lemma 3.4 needs a usable form of the stationarity condition : a subgradient of at equal to . This requires a sum rule for the Clarke subdifferential of a function plus a locally Lipschitz one, on a tangent space whose norm comes from the Riemannian metric rather than from the model space. Second, the gradient of at has to be identified with through . In Mathlib this mixes manifold derivatives (mfderiv) with Fréchet derivatives on a space carrying two equivalent norms. Third, it has to be shown that the iterates and the accumulation point remain in , so that Assumptions 3.3 and 3.4 apply at every step.
Theorem numbers and pages are those of arXiv:1909.06065v4. is a smooth manifold modelled on a finite-dimensional real inner-product space , with Mathlib's RiemannianBundle on the tangent bundle. All norms and inner products on are the Riemannian ones. Retractions and gradients are the published RiemOpt.BFGS.IsRetraction and RiemOpt.FR.IsGradient. The Clarke derivative is an EReal-valued limit superior along . Algorithm 1 is modelled as a run (sequences , with the three defining properties), and every statement holds for every run. Indices start at , accumulation points are cluster points of the sequence, and the bounds divided by are stated for .
The formalization commits to the following readings:
A single for all in (3.10) would make retraction-convexity force to be affine, and the theorem would only cover affine problems. That reading is excluded. Statements with the case , where Lean's makes (3.16) false, are excluded as well.
Contributions welcome: a Clarke sum rule for plus locally Lipschitz functions, the identification of the Fréchet derivative of at with the Riemannian gradient, and the five milestones in order. The Clarke layer and the derivative identification are reusable beyond this mission.
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.
Douglas–Rachford splitting is a method for minimizing a sum of two convex functions when each function has an accessible proximal operator. Its iterates are easy to state, but the speed of convergence of the objective at an individual proximal point is less immediate than convergence of an averaged point or of a residual. For optimization models in which one summand has a Lipschitz continuous gradient, Davis and Yin give explicit objective-error bounds that depend on the proximal stepsize. Their paper compares these bounds with forward–backward splitting and shows that DRS has an objective rate at least as fast when the stepsize is sufficiently small.
The present mission formalizes the rate in Theorem 3.2 and the Appendix B estimates that state the relevant contraction, monotonicity and summability properties. The companion Theorem 3.3 concerns the squared fixed-point residual. Both results are proved in the 2015 arXiv version of the paper, which fixes the numbering and constants used here; the journal article appeared in Mathematics of Operations Research in 2017.
Let be a real Hilbert space. Let be proper, lower semicontinuous and convex, and let be convex and differentiable with a -Lipschitz gradient for some . The proximal map of a function at stepsize sends to the minimizer of . Write and , and let be the reflection associated with a proximal map .
The Peaceman–Rachford map is . The DRS run is the relaxed PRS run with relaxation parameter at every step:
Equivalently, . The initial is arbitrary. Let be a fixed point of , and put . The objective value compared in this mission is at for both summands: . These values are finite under the standing assumptions. The section's Assumption 5 requires the smoothness of and constant relaxation ; it applies to Theorems 3.2 and 3.3 even though their own sentences do not repeat it.
Let be the positive root of , and the positive root of . The first target bounds the best objective error at every :
For every , this best error is . When , the same first-case upper bound holds for each , and . The goal states all four clauses together. The paper prints , the positive root of . That threshold does not match the coefficient the proof needs to be nonpositive, and with it the first case fails: for , on , and the error is twice the bound. The mission states the theorem with the threshold the proof supports, the positive root of .
For and , the companion target is
The Appendix B milestones give the contraction of the smooth gradient at proximal points, a fundamental one-step inequality, monotonicity, the extremal admissible stepsize ratio, and two summability bounds. Their constants and indices match the printed displays (B.1), (B.4), (B.7), (B.8), (B.10) and (B.12).
The objective theorem gives a rate directly at the proximal point when the stepsize is below the smaller threshold. Outside that regime, it still gives a best-iterate rate for every positive stepsize, including the explicit correction term for larger . The residual theorem controls the change in the DRS state at the faster squared rate. These statements let later work compare DRS against other splitting methods using the same objective and residual quantities, rather than changing the point at which the objective is measured.
The paper proves these results (Theorem 3.2 with the corrected threshold ); their statements are not new conjectures. The formalization work is to connect extended-real convex functions, actual proximal minimizers, smooth gradients, infinite sums, finite minima, and little-o assertions in a single Lean development. The seven Appendix B milestones are also useful as separately importable facts about proximal splitting. A machine-checked proof is still needed for the draft theorems of this mission.
The familiar convergence of the DRS fixed-point residual does not by itself give the objective error at . An objective comparison involves the two different proximal points and the smooth gradient evaluated at successive . The large-stepsize regime changes the coefficient of the gradient increment and therefore changes the explicit bound. For the per-iterate conclusion, one must establish a monotone, summable quantity that dominates the objective error; a best-iterate estimate alone does not yield the stated nonergodic little-o claim. This explains why the mission retains the Appendix B estimates rather than replacing the goal with a generic statement.
The Lean carrier is a complete real inner-product space. The proper, closed, convex predicate for and the proximal-map predicate are imported from the published ThreeOpSplitting.ConvexRates.Problem definition; the published MoreauProx.Characterization.GammaZero supplies the subgradient notion used by the paper's surrounding analysis. The smooth is a real-valued function, with its actual gradient supplied by Mathlib's gradient and constrained by the imported smoothness predicate. Each proximal map is a function with the defining minimization property; the theorems do not assume an arbitrary map can stand in for a prox.
The fixed point is an explicit hypothesis, as in the paper. The two root constants are positive real numbers satisfying their defining cubics, never decimal approximations. A finite minimum ranges over ; infinite sums come with summability; asymptotic claims use genuine little-o. The condition protects the denominator in Theorem 3.3. The objective error is taken at , never at , and the goal contains no auxiliary monotonicity or summability assumption that would assert part of its proof. Further contributions that establish proximal finiteness, the Appendix B inequalities, and the rates themselves fit within this scope.
Manufacturers increasingly sell directly to consumers through their own stores and websites, alongside the independent retailers that carry their products. This practice is called supply chain encroachment. Retailers routinely resent it, and examples range from beer brewers to personal computers. Arya, Mittendorf and Sappington (Marketing Science, 2007) showed that, when product quality is fixed, encroachment can benefit the retailer too: the manufacturer lowers the wholesale price to keep the retailer channel competitive, and this wholesale price effect can outweigh the lost sales.
Ha, Long and Nasiry (Manufacturing & Service Operations Management, 2016; authors' manuscript SSRN 3970373) ask what changes when the manufacturer also chooses product quality. Their first result, formalized in this mission, is that the win–win outcome disappears: with endogenous quality and a single product sold in both channels, encroachment always helps the manufacturer and always hurts the retailer.
Consumers have a quality sensitivity uniformly distributed on , and a consumer who buys a product of quality at price obtains surplus . When one product of quality is sold in total quantity , the market-clearing price is . The manufacturer's unit production cost for quality is , with the cost of quality. Selling one unit through her own direct channel costs her an additional ; the retailer's selling cost is .
Benchmark (no direct channel). The manufacturer chooses a wholesale price and a quality ; after observing them the retailer orders . The profits are
Encroachment with uniform quality. The game has three stages and perfect information:
Both channels sell the same product at the price , so
The solution concept is subgame perfect equilibrium: at every decision node, on or off the equilibrium path, the mover's rule picks a feasible action that no feasible alternative beats. The manufacturer encroaches when on the equilibrium path.
In the Lean development these are the structures Outcome and Profile, the payoffs retailerPayoff and mfrPayoff k c, and the predicate IsSPE k c σ of the definition QualityEncroach.Uniform.Game, with the benchmark counterparts BenchProfile and IsBenchSPE k τ.
In the benchmark, every equilibrium has and profits , . The goal states that, for every , and every subgame perfect equilibrium of the encroachment game in which the manufacturer encroaches,
The statement fixes no threshold value, and it holds for every equilibrium.
The milestones follow the paper's backward induction:
The mission also contains:
The result separates two regimes that look alike. With quality fixed, a retailer facing an encroaching manufacturer is better off exactly when condition (6) holds. With quality chosen by the manufacturer, that region disappears. The manufacturer distorts quality, upward when is small and downward when it is large, and so relies less on the wholesale price to steer the retailer's order. The retailer then loses in every equilibrium in which encroachment occurs. The paper's later sections (quality differentiation, a fixed cost of quality, no quality commitment, a general cost function) all measure against this base case.
The result is proved on paper, by backward induction with closed-form profits, an envelope-theorem convexity argument in , and a numerically located threshold . None of it is formalized. A machine-checked proof would certify:
Each step of the backward induction is a one-variable concave problem, but the steps do not compose into a single smooth problem. The retailer's best order depends on whether his order leaves room for direct sales. As a result the manufacturer's profit given is the piecewise function . Its middle piece describes a retailer who orders exactly enough to keep the manufacturer out, and that piece is not a stationary point of anything. The global optimum over switches between the first piece and the other two at a threshold that the paper locates only numerically.
The goal compares the optimum of this piecewise problem with a constant, for every equilibrium. The natural first idea, comparing the reduced profits with the benchmark ones pointwise in , does not work for the retailer: for a fixed quality his encroachment profit exceeds the benchmark profit on part of the range, which is exactly condition (6). The comparison has to use the quality the manufacturer actually chooses, and that quality is known only through the case analysis above.
All quantities are real numbers. The following conventions are fixed:
Subgame perfection is written in one-shot-deviation form at every history, which in this three-stage game with perfect information is subgame perfection. It constrains the retailer's rule at every and the manufacturer's stage-3 rule at every , not only on the path.
The benchmark profits in the goal are the paper's constants and . The milestone benchmark_equilibrium proves that a benchmark equilibrium exists and that these are its profits.
Two formalizations would trivialize the goal, and both are ruled out:
The encroachment threshold of Proposition 1(i) is stated in both directions, with chosen before . The boundary point is left open, because the paper's statements disagree there.
The closed forms , , , , , , , , , and are definitions that cite their page. Every statement that uses one with in a denominator assumes .
A complete development needs:
The game definitions are reusable for the other missions of this series, which keep this cost structure. Proofs of any milestone are welcome, as are alternative arguments for the goal that bypass the threshold computation.
A promise constraint satisfaction problem is given by two finite relational structures with a homomorphism . An instance is a third structure , and the task is to answer yes if and no if ; the promise is that one of the two holds. Approximate graph colouring (colour a -colourable graph with colours) and the search for a not-all-equal assignment of a 1-in-3-satisfiable formula are of this form, and their complexity has been open since the 1970s and 2010s respectively.
For ordinary CSPs () the algebraic approach, in which the complexity is governed by the polymorphisms of the template, led to the classification of all finite-template CSPs (Bulatov 2017, Zhuk 2017). Barto, Bulín, Krokhin and Opršal (arXiv:1811.00970, J. ACM 2021) extend that approach to promise problems. Their central structural result is Theorem 4.12: the existence of a minion homomorphism between polymorphism minions, which by their Theorem 3.1 yields a log-space reduction between the PCSPs, is characterized in five other ways, two of them purely relational.
Timeline:
A signature is a finite set of relation symbols with arities . A structure on a finite set gives a relation for each ; a homomorphism maps every tuple of into . A PCSP template is a pair of structures with the same signature and .
An -ary polymorphism , , applied coordinatewise to any tuples of , gives a tuple of . The minor of an -ary given by is . A minion is a nonempty set of functions of positive arity closed under minors; is one. A minion homomorphism preserves arities and satisfies .
A bipartite minor condition is a finite set of identities between symbols from two disjoint sets; a minion satisfies it if the symbols can be assigned members of matching arity that make every identity true. For a structure with and an instance , the condition has an -ary symbol per element of , an -ary symbol per constraint , and one identity per position of each constraint, read off the list of tuples of . The free structure has universe , and a tuple lies in its relation when all are minors of one -ary member of in the pattern given by .
A pp-power of lives on , , each relation being defined in and in by one and the same primitive positive formula. A homomorphic relaxation of has homomorphisms and . pp-constructibility is the closure under finitely many such steps.
For PCSP templates of finite structures and , the following are equivalent:
In the order of the proof on p. 27: Lemma 4.8 (relaxations and pp-powers give minion homomorphisms) and Corollary 4.10 for (6) ⇒ (1); Lemma 4.3 () for (2) ⇒ (3); Lemma 3.14 for (3) ⇒ (4); Lemma 4.11 ( relaxes a pp-power of ) for (4) ⇒ (5). Lemma 4.4, the bijection between homomorphisms and minion homomorphisms , is included as an extra item.
Theorem 4.12 replaces a property of infinitely many functions, the existence of a minion homomorphism, by a homomorphism between two finite structures (item 4), which is decidable, and by a relational construction (items 5–6). The free-structure criterion is what bounds the arity of polymorphisms that a hardness proof must inspect, and the paper uses it to prove NP-hardness of and to analyse the 1-in-3 versus not-all-equal problem. Later work on approximate graph and hypergraph colouring states its reductions in these terms.
The result is proved in the paper. As far as is known it has not been machine-checked: Mathlib has no minions, minor conditions, pp-formulas or pp-constructions. The mission produces a reusable Lean vocabulary for the algebraic theory of promise CSPs, together with a formal proof of the equivalence. The complexity consequences are not formalized.
Four of the implications are short once the definitions are fixed. The substantial step is (4) ⇒ (5), Lemma 4.11: a statement about the polymorphism minion, an object defined by infinitely many conditions, must be turned into a finite relational construction, and the relations of the pp-power have to be defined by one formula that is correct in and in at the same time. The indices involved, tuples over a power of , coordinates indexed by , and the enumeration of each , are where an informal reading leaves the most to check. Lemma 4.8(2) needs that polymorphisms preserve every pp-definable relation, a statement about arbitrary formulas, not only about the relations of the template. Corollary 4.10 is an induction over a sequence of templates whose signatures and domains change from step to step, which a formal statement cannot treat as a sequence in one fixed type.
Structures, homomorphisms, templates and polymorphisms are the published PCSPBLPAff.Symmetric definitions (RelStruct, IsHom, IsPromiseTemplate, IsPolymorphism). All structures are finite with nonempty domains: domains carry Fintype, DecidableEq and Nonempty (nonemptiness is the field's standing convention, which the paper uses when it identifies a domain with ; without it items (4) and (5) of the goal are not equivalent). The goal and Lemma 4.11 also assume that every relation of is nonempty; the paper does not say so, but if then , and when has an element on which every relation holds constantly no pp-power can have an empty relation, so (4) ⇒ (5) fails, signatures are Fintype, arities are positive, minions in Lemmas 4.3–4.4 live on finite sets. Theorem 4.12 is stated only for finite templates, as in the paper (p. 46 notes that it fails for infinite ones). Minions have no nullary members. A minion homomorphism is a family of maps on the members , so it cannot be made trivial by values outside the minion. Bipartite minor conditions have finite symbol and identity types in Type; item (2) quantifies over all of them. and take the enumeration of and of each as explicit equivalences; the paper's identification is one such choice. A pp-power uses one formula for both structures, with free variables indexed by . Templates are bundled for pp-constructibility, which is an inductive predicate.
The goal is the six-way equivalence (List.TFAE) and not any of its trivial fragments; the goal cannot be closed by choosing degenerate enumerations, because every statement quantifies over all of them.
Not formalized: the log-space reductions of Theorems 3.1 and 3.12, Remark 3.11's reduction between promise minor-condition problems, and the cited Theorem 2.25 [Pip02, BG16b]. Contributions are welcome on general facts that are reusable beyond this mission: polymorphisms preserve pp-definable relations, composition of minion homomorphisms, and the natural minion homomorphism .
Many problems in signal processing, statistics and machine learning ask to minimise a sum of two convex functions, each of which is easy to handle on its own through its proximal operator but not jointly. Operator-splitting methods exploit exactly that structure. The Douglas–Rachford (DRS) and Peaceman–Rachford (PRS) splitting schemes, introduced for linear equations in the 1950s and extended to maximal monotone operators by Lions and Mercier (1979), are the classical examples; applied to the dual of a linearly constrained problem, DRS is the alternating direction method of multipliers (ADMM) of Gabay and Mercier (1976).
Convergence of these methods has been known for decades, but convergence rates in terms of the objective value were established only recently. Davis and Yin (arXiv:1406.4834) showed that for general convex the objective error of relaxed PRS converges at the nonergodic rate , and that this is sharp. The paper behind this mission (arXiv:1407.5210v3) asks how much faster the method becomes when or is more regular. Its Theorem 3.1 answers the question for the case of one smooth function: the best objective error found in the first iterations is , for any stepsize. This matches the rate of forward–backward splitting (FBS), the method one would otherwise use when one of the two functions is smooth, without FBS's stepsize restriction.
Let be a real Hilbert space and let be closed, proper and convex. For the proximal operator is
the reflection is , and the PRS operator is . For write .
Relaxed PRS (Algorithm 1) starts from any and iterates
The choice is DRS and is PRS. Each step computes two auxiliary points,
which are the method's candidate solutions. If is a fixed point of , then minimises . The objective error at a point is .
A function has a -Lipschitz gradient () if it is real-valued and differentiable and for all .
Suppose . If is -Lipschitz and , or if is -Lipschitz and , then
Both cases are part of the goal. The statement fixes no constants: it asserts only the order of the best-iterate error, so it holds for every stepsize .
A companion item states the explicit bounds of the proof of Theorem 3.1 (p. 11), of the form times a case-dependent factor.
The result separates relaxed PRS from FBS. FBS needs to converge, so it needs the Lipschitz constant of the gradient, or a line search to estimate it. Theorem 3.1 says relaxed PRS reaches the same best-iterate order for every , and the companion bounds show how the constant depends on . The theorem and its explicit bounds are part of the paper's catalogue of rates (its Tables 1.1–1.2), which records how the rates of relaxed PRS and ADMM improve under regularity.
The result is proved in the paper. As far as is known, none of these statements is machine-checked. Formalizing it means building the prox calculus for extended-valued convex functions on a Hilbert space (Lemma 1.1, Lemma C.1), the descent and cocoercivity inequalities for smooth convex functions (Theorem A.1), the Fejér-type summability of the fixed-point residual of averaged nonexpansive maps (Fact 1.2), and the summable-sequence rate lemma (Fact 1.1). Each of these is reused across operator-splitting analyses.
The objective errors are nonnegative and, by Proposition 3.1 and Fact 1.2, weighted-summable. They are not monotone, however. A summable nonnegative sequence need not be term by term, which is why only the best iterate gets the little-o rate. A summability argument that ignores this, or that claims the rate for the last iterate, proves something false.
Proposition 3.1 is the substantive step. The upper fundamental inequality contains an inner-product term that does not telescope, and it must be absorbed through the optimality condition (C.2) and the smoothness inequalities (A.1)–(A.2). When the residual term that remains has the wrong sign. It is controlled only by a second use of the Lipschitz gradient, through the regularity term , which costs the factor .
InnerProductSpace with CompleteSpace. are H → EReal, closed, proper and convex in the sense of the published IsProperClosedConvex. A prox map is a map with the published IsProx γ f P, which for determines it uniquely. The subdifferential is the published subgrad.IsSmoothConvex β h (convex, Fréchet differentiable, -Lipschitz gradient), .Asymptotics.IsLittleO along atTop. The best iterate is Finset.inf' over .EReal.toReal, evaluated only where all four values are finite. These points are prox outputs of a proper function, and values of the real-valued smooth function.Contributions are welcome at every level: the prox calculus of Lemma 1.1 and Lemma C.1, Theorem A.1, the summability results, and the final assembly.
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.
Every square-integrable martingale of a Brownian filtration is a stochastic integral, (Itô's representation theorem). The classical theorem gives no formula for . In hedging, is the replicating strategy of a claim. In filtering and stochastic control it is the quantity one has to compute. The Clark–Haussmann–Ocone formula identifies through the Malliavin derivative . That derivative is anticipative, defined only up to null sets, and acts on the Wiener space rather than on the observed path.
Cont and Fournié (arXiv:1002.2446, Ann. Probab. 2013) develop a nonanticipative alternative from Dupire's functional Itô calculus (Dupire 2009). The integrand of the representation is a vertical derivative , computed pathwise from a functional representation of the martingale. Their main structural result is that this derivative, first defined on regular functionals, extends to all square-integrable stochastic integrals and inverts the Itô integral there. This mission formalizes that extension.
Timeline:
Fix a horizon and a dimension . A path is a map . A path is cadlag on if it is right-continuous there with left limits. The stopped path is , and the vertical perturbation shifts the value at time by while keeping on . Paths with values in the positive semidefinite matrices carry the density of the quadratic variation.
A nonanticipative functional depends only on . Its vertical derivative is the gradient at of . Its horizontal derivative is the right derivative of along the flat extension. The class consists of functionals with the following properties:
All functionals also satisfy (10), .
Assumption 5.1. is a standard -dimensional Brownian motion, and
with adapted to . The density of is cadlag and adapted. The working filtration is , the completed natural filtration of , right-continuous on .
The spaces involved are:
The operator is closable on . Its closure is a bijective isometry
and is the unique element of with
In particular in . The adjoint identity (55),
is a separate item.
The theorem identifies the integrand of the martingale representation of any square-integrable -martingale as a limit of pathwise derivatives. On regular functionals, those derivatives are computed by perturbing the endpoint of the observed path. The integrand is therefore adapted by construction, and it can be approximated by finite differences. This is the basis of the paper's general representation formula (Theorem 5.9) and of its comparison with Malliavin calculus (Theorem 6.1, ). The isometry also gives the structure of a Hilbert space on which is a weak derivative. This is a nonanticipative counterpart of the Wiener–Sobolev space .
The results are proved in the paper; none of them has a machine-checked proof. Neither Mathlib nor the platform has a square-integrable Itô integral with its isometry, a functional Itô calculus, or a martingale representation theorem. A complete development would provide the first formal statement and proof of a martingale representation formula with an explicit, nonanticipative integrand. The path-space and layers are reusable for any work on path-dependent functionals.
The proof of the goal is short once its inputs are available, but each input is substantial.
A tempting shortcut is to define on as the inverse of the Itô integral. That makes (56) a tautology and erases the link with the pathwise derivative, so the closure must be built from .
Time is , statements are made on , and functionals are defined on all paths, with every quantifier over path space restricted to cadlag pairs. The derivatives of a functional are explicit witnesses tied to it by HasDerivWithinAt and HasFDerivAt, so a derivative is never a junk value. The distance uses the max norm on (sup norm on vectors, entrywise sup norm on matrices) and appears only through explicit bounds.
The formal setting makes these hypotheses explicit:
In dimensions, means . The square-integrable Itô integral is a relation, defined through simple dyadic integrands and an almost-surely continuous integral process on . This continuity selects the stochastic integral version from the limits at fixed times. The derivative of each test process is required to belong to , as Definition 5.4 states. Theorem 5.2 integrates by dyadic left Riemann sums in probability (EthierKurtz.itoStepSum). Corollary 4.4 is stated for , because the printed version fails at .
The statements must not be trivialized. The closure of is a relation, and its existence, uniqueness up to -null sets, isometry and surjectivity are all conclusions, never definitions. Expectations of squares are lower integrals in , and every real expectation in (51), (53) and (55) comes with its integrability as part of the conclusion. is not reduced to , because . A derivative witness cannot be chosen freely, because it is tied to .
Contributions are welcome on:
Best subset selection with ridge shrinkage, the -regularized least squares problem
is a mixed integer program. Exact solvers for it rely on branch-and-bound: at every node of the search tree a convex relaxation is solved, and the node is discarded if a lower bound on that relaxation already exceeds the best objective value found so far. Hazimeh, Mazumder and Saab (arXiv:2004.06152v2, Mathematical Programming 2022) build such a solver, L0BnB, for instances with in the millions. Its relaxations are solved only approximately, by first-order methods, and an approximate primal solution does not by itself certify a lower bound. The bound has to come from a dual feasible point. Theorem 2 of the paper supplies the duals of the node relaxation in closed form, together with explicit formulas for the optimal dual variables as functions of the primal optimum. Everything the paper later proves about the quality of its dual bounds (Section 3.2, Theorem 3) starts from these formulas.
Data are a matrix with columns , a response , and parameters , where bounds the coefficients. Write and . The reverse Huber penalty is for and for . Define
and let if and if . The reduced relaxation (5) is
By Theorem 1 of the paper it is the interval relaxation of the perspective formulation, projected onto .
The two dual objectives of Theorem 2 are, for and ,
where is maximized over all of (problem (20)) and subject to for (problem (22)). For an optimal of (5), with residual , the candidate dual variables are
In the Lean development these objects are F, box, h1, v, h2, Feas22, alphaStar, gammaStar, rhoStar, muStar in the namespace L0BnB.Duality.
Let minimize over .
This is "(20), respectively (22), is a dual of (5), and (23), respectively (24), are optimal dual variables", with the paper's remark that strong duality holds.
The result. Theorem 2 turns the node relaxation of L0BnB into a pair of explicit concave maximization problems, one per regime of versus . The dual (20) is unconstrained, so any gives a valid lower bound; the paper's dual bounds (25)–(28) evaluate or at built from an inexact primal solution , with the remaining variable chosen in closed form. The formulas (23)–(24) explain why this choice is right: at the exact optimum it recovers the primal value. Theorem 3 of the paper, which bounds the loss of this dual bound by a quantity depending on the support size rather than on , compares to term by term and therefore depends on (23).
Formalizing it. The paper proves the case in Appendix A and omits the proof of the case ("follows along the lines similar to what was shown above"). The appendix also contains an intermediate formula for the coordinate minimum, , that is incorrect when is large; the final dual (49) = (20) is nevertheless correct. A machine-checked proof supplies the omitted case and settles the correct statement. To our knowledge neither half has been formalized.
The dual objective (20) hides the box constraint inside the term and the penalty inside , and the reverse Huber penalty is piecewise, so even the weak-duality half has to handle both pieces of and the junction . The attainment half is where the work lies: it needs the optimality conditions of a nonsmooth convex problem over a box, at coordinates where (where is not differentiable), where (where the box is active), and where both may interact with the regime boundary . The natural first idea, to read (23) off the Lagrangian derivation in the paper, does not yield a proof: that derivation assumes a dual optimum exists and relates it to by complementary slackness, whereas the theorem asserts an identity for the explicit built from alone.
Data are X : Matrix (Fin n) (Fin p) ℝ, y : Fin n → ℝ and reals lam0 lam2 M with 0 < lam0, 0 < lam2, 0 < M as hypotheses; is Fin p. Norms and inner products are explicit sums: , , , , and is for every . The regime split is written versus . sign is Real.sign, with ; where it is evaluated in (23) the argument is nonzero at an optimum. The optimal solution is a hypothesis (feasible and minimizing over the box); its existence is not part of the statements. The coordinate milestones (45) and (47) are stated for a scalar standing for and a multiplier . No normalization of or is assumed: the unit-norm convention that opens Section 3 is not used by Theorem 2. The paper writes no in these results, so no constants are instantiated.
"A dual is given by" is formalized as weak duality over all dual-feasible points together with equality at the explicit dual variables. Weak duality alone would not be Theorem 2, and neither would the equality alone; the goal requires both in both regimes. Uniqueness of the dual optimum is not claimed.
A complete development needs elementary convex analysis of the scalar penalty (its conjugate and subdifferential), first-order optimality conditions for a convex function over a box in , and finite-sum bookkeeping. The scalar facts about the reverse Huber penalty are reusable in the companion missions on the reduced relaxation and on dual-bound quality. Contributions to any milestone, or a direct proof of the goal, are welcome.
The martingale optimal transport problem asks for a coupling of two probability measures on that is the law of a one-step martingale and minimizes an expected cost. It arises in robust finance, where the marginals are the risk-neutral laws of an asset at two dates implied by option prices, and model-independent price bounds for exotic options are the extreme values of the problem (Beiglböck, Henry-Labordère, Penkner 2013; Galichon, Henry-Labordère, Touzi 2014).
Beiglböck and Juillet (arXiv:1208.1509v2, Ann. Probab. 44(1), 2016) construct a canonical martingale coupling, the left-curtain coupling, which plays the role that the monotone (quantile) coupling plays in classical transport. Its construction rests on one object, the shadow of a measure in another, and on one structural property of it: shadows are associative. This mission formalizes that property, Theorem 4.8 of the paper, together with the chain of results in §2.3 and §4.1–4.3 on which it rests.
Let be the set of finite Borel measures on with finite first moment, of any total mass. For :
If , a shadow of in is a measure with (i) , (ii) , and (iii) for every satisfying (i) and (ii). Lemma 4.6 of the paper shows that it exists and is unique; it is written . It is the least spread-out part of into which can be transported by a martingale. An atom is a measure with .
In the Lean development these objects are InM, ConvexLE, ExtConvexLE, potential, ConvergesInM and the predicate IsShadow ν μ η, in the namespace MartOT.Shadow.
For with ,
Theorem 4.8 is what makes the left-curtain coupling well defined and consistent. That coupling is the martingale plan which, for every , sends onto (Theorem 4.18). Associativity says that the parts of assigned to and to fit together into the part assigned to , so the family of shadows defines a single coupling. The uniqueness of left-monotone martingale plans and the optimality of the left-curtain coupling for the costs with strictly convex, both later results of the paper, rest on it.
The result is proved in the paper. As far as is known it has no machine-checked proof. This mission produces a statement of it, and of the supporting results, in terms of measures of arbitrary finite mass with no reference to a chosen shadow function. A complete development would give Lean a theory of the convex order on finite measures through potential functions, which is reusable well beyond martingale transport.
For finitely atomic measures the identity follows by adding one atom at a time (Lemmas 4.12, 4.13, 4.16), but even the single-atom step needs a monotonicity property of shadows of atoms in varying targets (Lemma 4.11), and that property comes from their explicit description through quantile functions. The general case cannot be obtained by a direct manipulation of the minimality property (iii): minimality of and of separately says nothing obvious about minimality of their sum among measures dominating , because a competitor for the sum need not split into competitors for the summands. The paper passes to the limit along convex-order approximations, which requires a continuity property of the shadow (Proposition 4.15) in the topology of .
MeasureTheory.Measure ℝ with membership in stated explicitly (InM: finite measure, identity integrable). Masses are arbitrary; nothing is normalized to probability measures.EReal through the published ModelRiskOT.Duality.extIntegral (positive minus negative part), never as Bochner integrals, so a non-integrable test function cannot produce a junk value. The extended convex order uses lower Lebesgue integrals of nonnegative functions.IsShadow ν μ η, never a function built by choice. Every statement about quantifies over all shadows, which with existence and uniqueness (Lemma 4.6, a milestone) is the paper's statement. Uniqueness is part of the conclusion of Lemma 4.6 and is not assumed elsewhere.IsShadow ν (γ1 + γ2) (η1 + η2).Online retailers show their catalogue on a sequence of pages, and most visitors never reach the last one. Which products appear on the first page, and at what prices, therefore decides what a typical consumer can buy at all. Gallego, Li, Truong and Wang (Operations Research, 2020) model this as the product framing problem: the consideration set of a consumer is the set of products on the pages that consumer is willing to view, and the number of pages viewed is random. Their Section 7 adds prices to the problem and asks how a retailer should frame and price jointly when consumers choose by the multinomial logit (MNL) model.
The question connects two literatures. In assortment pricing under MNL with a common price sensitivity, the optimal prices of all offered products are known to be equal (Anderson, de Palma and Thisse 1992; Gallego and Stefanescu, as cited on p. 16 of the paper), and the nested-logit extension of Gallego and Wang (Operations Research, 2014) keeps an adjusted markup constant across nests. In search and ranking models, the order in which products are shown changes which ones are bought. The paper's structural results say what survives of the equal-price rule once consideration sets are nested by page, and which products belong on the early pages.
There are products, , and pages, each holding at most products. A framing places each product on one page or leaves it undisplayed. A consumer views the first pages, where is random with law , independent of the framing. A consumer who views pages considers , the products on pages , so .
Product has a quality and a price , and the price sensitivity is . The mean utility of product is , and the outside option has utility . Under the MNL model a consumer with consideration set buys with probability
and for . The expected revenue from that consumer is , and the total expected revenue of a framing and a price vector is
For a fixed framing, denotes the optimal value of this quantity over all price vectors, as a function of the quality vector .
The goal is the existence of an optimal joint solution with the paper's structure: there are a feasible framing and prices such that no feasible framing with any prices earns more, and
Pages are filled in order until all products are displayed, and the products appear in descending order of quality.
Theorem 5 reduces the pricing problem of a fixed framing from prices to page prices and says that later pages carry higher prices; this is the page-level analogue of the constant-markup property of MNL pricing, and it runs opposite to the ordering found in oligopoly search models (Arbatskaya 2007). Theorem 6 removes the framing decision almost entirely: a joint optimum is obtained by sorting the products by quality and filling pages in that order, leaving only page prices to choose. The paper's approximation algorithm for joint pricing and framing (Theorem 7, NEST-P, with guarantee ) starts from this structure.
None of these statements has a machine-checked proof. A complete development would give the first formal treatment of MNL price optimization with nested consideration sets, including the existence of optimal prices, which the paper takes for granted. The paper's argument for the monotonicity and its envelope-theorem step (19) are informal; a formal proof has to supply both.
The expected revenue is not concave in the prices, even with two products on two pages (Example 1, p. 17), so the first-order condition alone does not identify the optimum, and existence of an optimal price vector has to be argued from the behaviour of the revenue as prices tend to . The within-page equality of prices follows from the first-order condition, but the ordering of page prices needs a global comparison of revenues across consideration sets. In Theorem 6, the obvious exchange argument (swap a higher-quality product forward) does not obviously keep revenue from decreasing when the swapped products have different prices; the paper splits into two cases, and in one of them the improvement comes from continuously moving qualities, which requires control of the optimal value as a function of rather than of a fixed price vector.
Products are Fin n, pages are the natural numbers with , and capacities satisfy . A framing is f : Fin n → ℕ with page f i ∈ [m] for displayed products and f i = 0 for undisplayed ones (the paper's ); feasibility means at most products per page. The law of is a nonnegative function on summing to one. Prices are finite reals: the paper's priced-out products () coincide with undisplayed ones, which the framing already allows. "Descending order" and "increases" are read weakly.
Theorem 5 and (17) are stated for every maximizing price vector and only for products on pages that some consumer reaches (), a restriction the paper never discusses: a product on a page no consumer reaches can carry any price at an optimum. They do not assert that a maximizer exists. Theorem 6 is read existentially ("some optimal solution has this structure"); the universal reading is false when some , because exchanging products between pages and then changes no revenue. (19) is formalized as its stated consequence, the monotonicity of the optimal value , together with the boundedness of the revenues; the envelope identity itself would need a differentiable selection of optimal prices that the paper does not establish.
A trivializing formalization of the goal would take the optimum over framings that are already sorted, over a single fixed framing, or over prices fixed in advance; the goal's optimality clause ranges over all feasible framings and all real price vectors. The development needs elementary calculus of the MNL revenue (HasDerivAt, Real.exp), finite sums over pages, and a compactness or limiting argument for the existence of optimal prices. Pages are those of the authors' accepted manuscript, which differ from the journal typesetting. Proofs of any milestone, and lemmas on MNL pricing reusable beyond this paper (boundedness of , existence of optimal MNL prices, the constant-price property for a single assortment), 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.