Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Wasserstein distributionally robust optimization (Wasserstein DRO) replaces the empirical loss of a decision by its worst case over all distributions within Wasserstein distance of the empirical distribution . It is used in operations research (newsvendor, portfolio selection) and machine learning (adversarially robust training, regularized regression) because the robust loss is a computable upper estimate of the unknown true loss. The question every user faces is how large must be. Measure-concentration results for the empirical measure in Wasserstein distance (Fournier and Guillin, 2015) require on a -dimensional space, which is useless in high dimension.
Gao (arXiv:2009.04382, Operations Research 2023) shows that a radius of order suffices, with no dependence on dimension, as long as the true distribution satisfies a transportation-information inequality and the loss class has controlled complexity. This mission covers the paper's result for the 2-Wasserstein distance, where the robust loss is linked to gradient regularization. Two sibling missions cover the variation-concentration inequality (Theorem 1) and the 1-Wasserstein / Lipschitz case (Corollary 4).
is a separable real Banach space with norm and dual norm . is the set of Borel probability measures with finite second moment, and is the 2-Wasserstein distance: is the infimum of over couplings of and .
In Lean the mission's own objects live in the namespace WassFSG.Grad: W2sq, IsP2, regularizer, IsT2, GradLipBound, gradNorm, empGradNorm, gradClass, localized, SubRootLocalComplexity, productRegularizer, epsN, rhoN and rhoTilde. The empirical mean and measure (empMean, empMeasure), the Rademacher complexity (radComp, expectedRad), sub-root functions (IsSubRoot), the class −F (negClass) and the probability count (peelCount) are the shared definitions of the series in WassFSG.Lip.
Write and . Assume in addition that , and set . If , then with probability at least , every satisfies
and
where .
Corollary 6 says that solving 2-Wasserstein DRO at a radius gives, with high probability, an upper bound on the true loss of every decision, up to an gap. This holds whenever and , for example for finite-VC gradient classes, smooth neural networks and Markowitz portfolios (Section 5 of the paper). Combined with the robust-solution argument of Remark 1, this gives excess-risk bounds for the robust solution. Theorem 3 alone is a generalization bound for gradient-norm regularization, an estimator used in its own right.
None of these results is known to be machine-checked. The mission produces a Lean statement of the full chain from a transportation inequality to the DRO guarantee. It also produces reusable infrastructure: the 2-Wasserstein regularizer on a Banach space, transportation-information inequalities, local Rademacher complexities with sub-root bounds, and a peeling argument. The printed failure probability needs a correction (see below), so the formal statement is itself a contribution.
The obvious route is to bound by times a gradient bound. It fails because decays like . The radius must instead come from concentration of the loss, and the result has to hold uniformly over , which requires symmetrization and a localization in the gradient norm.
Three points carry the weight:
The source is arXiv:2009.04382 (preprint basis); its printed page numbers equal the PDF's.
Standing conventions:
Added hypotheses, all implicit on the page:
Corrected slip. The printed failure probability (Theorem 3, Corollary 6) is negative for small and disagrees with Lemma 14, and the peeling in Lemma 14's proof misses one band. The Lean uses events (and in Corollary 6). Milestone texts keep the printed count. Lemma 13's printed proof contains a step that is false in general for signed Rademacher sums. The statement is posed as printed; a correct argument uses the non-negativity of .
Ruled out. A trivializing encoding would take , let the radii be free existentials, use a real supremum (which is on unbounded sets), or rely on Lean's for . None of these is used: every radius is the printed formula, and each degenerate case is excluded by a hypothesis.
Welcome contributions include proofs of the milestones and general lemmas on the Wasserstein regularizer (Lemma 2 is a first-order expansion). McDiarmid's inequality, which Corollary 6's proof uses, is not a milestone and is a welcome general-purpose result.
The spectral radius of a graph , the largest eigenvalue of its adjacency matrix, is a standard measure of how densely and how centrally a graph is connected. A classical theme of spectral graph theory asks, for a natural family of graphs, which member of the family on vertices maximizes . For planar graphs this question was raised by geographers comparing road and transport networks, and for outerplanar graphs it was posed by Cvetković and Rowlinson in their 1990 survey of the largest eigenvalue of a graph, where they relate it to the study of subfamilies of Hamiltonian graphs.
Conjecture (Cvetković–Rowlinson, 1990). The outerplanar graph on vertices of maximum spectral radius is .
Timeline:
This mission formalizes Section 2 of Tait and Tobin.
All graphs are finite and simple. An -vertex graph has vertex set , adjacency matrix , and spectral radius , the largest eigenvalue of the real symmetric matrix . Write for the degree of a vertex and for its neighbourhood.
A plane drawing of places the vertices at distinct points of and each edge as a simple arc between its ends; an arc passes through no other vertex, and two arcs meet only at a common end. The union of the vertex points and arcs is a compact set, so its complement has exactly one unbounded connected component, the outer face. A graph is outerplanar if it has a plane drawing in which every vertex lies on the boundary of the outer face.
The join of two graphs is their disjoint union together with all edges between them. The fan is a single vertex joined to every vertex of a path on vertices; it is outerplanar and has edges.
An outerplanar graph on vertices is a spectral maximizer if for every outerplanar graph on the same vertices.
Several milestones refer to a Perron vector: an eigenvector of for with all entries positive, normalized so that its maximum entry is , together with a vertex with . For a connected graph such a vector exists by the Perron–Frobenius theorem.
There is such that for every and every graph on vertices,
The forward direction is the paper's Theorem 7; the converse says that the fan is the maximizer, as the conjecture reads. The threshold is left unspecified, as in the paper.
The milestones follow the proof in Section 2, in order:
The theorem settles, for all large , a conjecture that had been open since 1990 and had resisted several partial attacks. The same paper settles, in the same framework, the planar analogue (the Boots–Royle and Cao–Vince conjecture, ) and a conjecture on spectral irregularity. The outerplanar case is the shortest of the three.
On the formal side, the result is proved on paper but has no machine-checked proof. Completing the mission produces a formal theory of outerplanar plane drawings (edge bound, -freeness, outerplanarity of the fan), eigenvector estimates for extremal graphs, and the full extremal theorem. The edge bound and the exclusion are reusable for any later work on outerplanar or series–parallel graphs. Determining the exact threshold , or proving the statement for every , would be a strengthening beyond the paper.
There are two separate difficulties. The first is topological: the facts about outerplanar graphs that the spectral argument uses (at most edges, no subgraph, no cycle in when dominates, outerplanarity of the fan) are folklore on paper but require a Jordan-curve-type argument about plane drawings, of which Mathlib currently contains very little. The second is spectral: the edge-switching step that proves compares of two graphs through the Rayleigh quotient, and needs a positive Perron vector and the variational characterization of the largest eigenvalue for symmetric matrices. A purely combinatorial edge-maximization argument does not work: the fan is not the only outerplanar graph with edges, so maximizing the number of edges does not identify the spectral maximizer.
SimpleGraph (Fin n); is the published WangKangXue.SpectralTuran.specRad, the largest eigenvalue of G.adjMatrix ℝ.RobertsonSeymour1986.GM5.PlaneDrawing with every vertex point in the closure of the unbounded component of the complement of the drawing. It is not replaced by a forbidden-minor characterization; such characterizations are theorems about outerplanarity, and would change which graphs compete in the maximization.IsSpecMax IsOuterplanar G: is outerplanar and no outerplanar graph on the same vertex set has larger . It is never weakened to a comparison with the fan.G ≃g fan n, with the fan on Fin 1 ⊕ Fin (n - 1).∃ N, ∀ n ≥ N.A complete development needs the Perron–Frobenius theorem for symmetric nonnegative matrices and the Rayleigh quotient characterization of , both of general use; the theory of outerplanar drawings; and the counting arguments of the lemmas. Contributions to any of these layers are welcome, as are independent proofs of the outerplanar facts from the drawing definition.
A recurring question in revenue management with strategic consumers is whether a seller gains from price commitment. When customers are forward-looking, a seller who announces its whole price path in advance (pre-announced pricing) removes the customers' incentive to wait for a markdown the seller would otherwise be tempted to give; a seller who keeps the freedom to set later prices after observing the market (responsive pricing) cannot credibly promise not to cut prices. In the classical models without learning, commitment is valuable: Aviv and Pazgal (2008) find that announced pricing extracts more profit than contingent pricing from forward-looking customers, and Besanko and Winston (1990) analyse the responsive monopolist facing rational consumers.
Papanastasiou and Savva (Management Science, 2017) add social learning (SL): early buyers post product reviews, and the customers still in the market update their beliefs about the product's quality before deciding whether to buy later. The reviews create an informational reason to wait, and they also give the responsive seller something to respond to. This mission formalizes the paper's §7, which asks whether commitment remains valuable once learning is present, and its answer: for impatient consumers it is not.
A monopolist sells over two periods to a continuum of consumers of mass one. Consumer has a preference , uniform on . Mean product quality is unknown; consumers share the prior , and reviews carry noise of variance . The SL parameter is . Consumers discount second-period utility by ; the firm does not discount; the unit cost is .
If a mass of consumers buys in period 1, the posterior mean that the remaining consumers see is, before the reviews arrive, distributed as
the pre-posterior law (Lemma 1); when it is the point mass at . A remaining consumer of type who buys in period 2 at price gets .
The optimal values and are the suprema of expected profit over all prices and all equilibria. In Lean these are preValue P and respValue P for a parameter record P : Params, and P.withδc d is the same model with discount factor ; "absence of SL" is P.noSL, the same model with .
In the presence of SL there is a threshold such that
with , and fixed on both sides. The threshold is not specified; only its positivity is claimed.
Without SL (), both values are finite and
strictly positive for .
The two propositions together reverse a standard prediction. Without learning, commitment weakly dominates (Proposition 7, consistent with Aviv and Pazgal 2008). With learning and impatient consumers, flexibility strictly dominates (Proposition 8): the value of reacting to reviews outweighs the cost of being unable to commit. The paper's numerical study (Figure 4) suggests that the threshold equals one for moderate , so that responsive pricing wins for every discount factor; that numerical claim is not a theorem of the paper and is not posed here.
The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. Formalizing them requires a rigorous treatment of a continuum purchasing game whose equilibrium is defined through a Gaussian law whose variance depends on the equilibrium itself, the subgame-perfect second-period pricing rule, and the continuity of optimal values in a parameter.
The comparison at is elementary in spirit: myopic consumers buy early exactly when , so the two regimes produce the same reviews for the same , and the responsive firm can only do better state by state. Turning this into a strict inequality between two suprema requires a uniform gap, not just a pointwise one, because the paper's argument assumes an optimal pre-announced plan exists.
The step that extends the result to is the paper's appeal to the Maximum Theorem. It needs the expected profit to be jointly continuous in the prices and in over a compact set of relevant plans. But the expected profit depends on through the equilibrium threshold, which is defined implicitly by an indifference equation whose Gaussian kernel itself depends on the threshold (equations (3) and (9)), and equilibria are sets of types, not numbers. Continuity of the optimal value therefore requires continuity and uniqueness of these implicit thresholds, and a reduction of both suprema to compact sets of prices.
The model is one shared definition module (SLPricing.Compare.Model), plus the formula (6) as p2Star. Conventions it commits to:
Added hypotheses, disclosed in each item: in the two threshold milestones; for the uniqueness clause of Lemma 3. Proposition 7's "higher" is stated as the proof states it: non-negative gap on , strict on .
The comparison is meaningful only because the responsive firm cannot commit. Enlarging the responsive regime to arbitrary second-period rules, or defining either optimal value as a real supremum (whose junk value is on unbounded sets), would make the goal trivial or empty; both are excluded by the definitions. Hard-wiring the thresholds , or the price (6) into the definitions would make the milestones definitional; they are theorems here.
A complete development needs: Gaussian expectations of piecewise-linear functions of and their continuity in the variance; the implicit-function argument for the thresholds; a Maximum Theorem (Berge) for the optimal values. The Gaussian convex-order and Maximum-Theorem pieces are reusable well beyond this mission, and contributions of them as separate theorems are welcome.
In distributed optimization, agents cooperatively minimize the average of private cost functions , exchanging information only with their current neighbours in a communication network. The model covers sensor networks, multi-robot coordination and machine learning with data split across machines, where no node can see the whole objective. In many of these systems communication is one-directional (broadcast radios with unequal ranges, asymmetric links) and the network changes over time.
Directed links raise a specific obstacle: a node cannot in general choose weights that are both row and column stochastic, because it knows its out-degree but not how its messages are combined by others. The push-sum (ratio consensus) protocol of Kempe, Dobra and Gehrke (2003) circumvents this with column stochastic weights and a scalar correction. Nedić and Olshevsky (2015) combined it with diminishing-step subgradient methods over time-varying directed graphs, obtaining sublinear rates. Gradient tracking methods (Xu, Zhu, Soh and Xie, 2015; Qu and Li, 2016) and EXTRA (Shi, Ling, Wu and Yin, 2015) reached linear rates with constant steps on undirected or static graphs. Nedić, Olshevsky and Shi (arXiv 2016, SIAM J. Optim. 2017) proved geometric convergence of gradient tracking over graphs that are both time-varying and directed; this mission formalizes that result.
The agents are . At each time there is a set of arcs; an arc means agent can send to agent . The out-degree counts the agents with in .
Assumption 6. There is such that for every the union of the arc sets over the window is strongly connected. Put .
Assumption 7. The mixing matrix has if or , and otherwise; each is column stochastic.
Each is differentiable with -Lipschitz gradient (Assumption 4) and -strongly convex with , some (Assumption 5). Write , , , and for the minimizer of .
Iterates are matrices whose row belongs to agent ; has rows , and is the Frobenius norm. Push-DIGing starts from , , and iterates, with step size and ,
The constants of the rate are , , and, for an integer ,
For , with , and every step size
there is with for all , where is
The paper's proof runs a small gain argument around the cycle , where , are gradient increments, and is the deviation from the row average. The milestones are the paper's own statements: the equivalent recursion (48) in terms of the row stochastic ; the bound (49) and row stochasticity of ; Lemma 13 (-step contraction by ); Lemmas 14–17 (the four arrows); Lemma 8 (an error bound for inexact gradient descent); Theorem 3 (the small gain theorem) and Lemma 4.
The theorem gives a geometric rate, with explicit constants, for a first-order method that uses only out-degree information, constant step sizes, one gradient per agent per round, and networks that are directed and need only be strongly connected jointly over windows. Before it, linear rates for distributed gradient methods required undirected or static graphs. The explicit quantifies how the rate degrades with , and the condition number . The result is proved in the paper; to the extent known, no machine-checked proof exists. A formalization yields a checked statement of the rate together with reusable components: the ergodic-norm small gain theorem, the push-sum weight bound, and the inexact gradient lemma, which also serve the companion DIGing mission on undirected graphs.
The natural Lyapunov approach fails: with asymmetric, time-varying weights there is in general no quadratic function that decreases at every step, and the consensus error contracts only over windows of iterations. The analysis therefore works with ergodic norms and chains four inequalities. Two further inputs come from outside the paper: the lower bound (Corollary 2(b) of Nedić–Olshevsky 2015) and the contraction of products of row stochastic matrices with entries bounded below on arcs (Lemma 5 of Nedić–Ozdaglar 2010), both of which a complete development has to prove.
Stacked iterates are functions Fin n → EuclideanSpace ℝ (Fin p); agents are indexed from 0 and time from 0. An arc is a pair (j, i) in a finite set A k. The weights are defined from alone, so is a constant of the graph sequence; it enters statements as a number with the hypothesis that it is the least upper bound of , never as a real supremum. Real powers are Real.rpow. The ergodic norm is the truncated maximum; the untruncated supremum is replaced by its pointwise meaning.
Four hypotheses are added to the page, each disclosed in the statements:
The goal states only the hypotheses of Theorem 18 and the rate; it does not assume any of the arrows, gains, auxiliary parameters or ergodic-norm bounds, so it cannot be discharged by assembling hypotheses.
A complete development needs matrix-product contraction bounds for push-sum, Frobenius-norm calculus on stacked matrices, and strong convexity estimates for inexact gradient steps. The small gain theorem, Lemma 8 and the push-sum lemmas are reusable beyond this mission. Proofs of individual milestones are welcome independently.
Wasserstein distributionally robust optimization (DRO) replaces the empirical loss of a decision or model by its worst case over all distributions within a Wasserstein distance of the empirical distribution . It is used in operations research (newsvendor, portfolio and inventory problems) and in machine learning (robust classification and regression), and it is attractive because the worst-case loss is often a computable convex program (Mohajerin Esfahani and Kuhn 2018; Gao and Kleywegt 2023).
The practical question is how large must be for the robust loss to upper-bound the true, unknown loss with high probability. The classical answer goes through measure concentration of around in Wasserstein distance (Fournier and Guillin 2015), which forces in dimension : the curse of dimensionality. Rui Gao's paper (arXiv:2009.04382; Operations Research, 2023) shows that a radius of order suffices, independently of , under a transportation-information inequality and a complexity assumption on the loss class. This mission formalizes the paper's result for the 1-Wasserstein distance (Sec. 4.2, Theorem 2 and Corollary 4).
Let be a separable real Banach space with norm . is the set of Borel probability measures with . The 1-Wasserstein distance is
For a loss the Wasserstein regularizer is the gap between robust and nominal loss,
The Lipschitz norm is the best Lipschitz constant of .
The data are i.i.d. samples from , with empirical distribution . and refer to the product law. The distribution satisfies the transportation-information inequality if for every , where is relative entropy. It holds, for example, for every distribution with a sub-Gaussian norm.
The loss class satisfies Assumption 1(I) if for all , with . It satisfies Assumption 1(II) if is unbounded and each attains its Lipschitz norm at infinity, i.e. for some .
The Rademacher complexity of a class on the sample is , with i.i.d. uniform signs . Assumption 5 asks for a sub-root function that dominates the localized complexities:
Sub-root means non-negative, non-decreasing, non-constant, with non-increasing. Its positive fixed point is .
Set and . Under , Assumption 1 and Assumption 5, for , with probability at least ,
Corollary 4 justifies a radius of order whenever , which the paper verifies for kernel classes and other examples (Sec. 5). That rate is the one used in practice, and it was not covered by the concentration-based theory. Theorem 2 is a dimension-free generalization bound for Lipschitz-regularized learning in its own right. Lemma 1 links the two by identifying the 1-Wasserstein regularizer with Lipschitz regularization.
The results are proved in the paper. As far as known, none of them is machine-checked. A formalization would check the paper's peeling and fixed-point arguments, which turn out to need a corrected failure-probability count (see Formalization scope). It would also produce reusable Lean infrastructure: Rademacher complexity in the , no-absolute-value normalization, localized classes, sub-root functions, , and the Wasserstein regularizer on a Banach space.
The obvious route bounds and uses Kantorovich–Rubinstein duality. It fails because is of order , so no dimension-free radius comes out. A dimension-free bound must therefore hold uniformly over an infinite loss class without passing through the distance between and , and the bound must scale with each function's own Lipschitz norm rather than the class-wide constant . The statements also need measure-theoretic infrastructure that Mathlib lacks or has only partly: transport inequalities, Rademacher averages over classes, and suprema of uncountable families inside expectations.
RWPI.SqrtLasso.transportCost with cost . Expectations inside regularizers and complexities are extended integrals in (published ModelRiskOT.Duality.extIntegral). is the Bochner integral; it is the true expectation because a Lipschitz is integrable under . Relative entropy is Mathlib's klDiv.Lemma 5 (concentration on the product space under , used in Lemma 9's proof) belongs to the companion mission on variation-based concentration and is not restated here. Contributions are welcome at every level: sub-root fixed-point facts, symmetrization, the peeling lemma, and Lemma 1's two directions are independent entry points.
The source is arXiv:2009.04382; its printed page numbers equal the PDF's page numbers.
Wasserstein distributionally robust optimization (Wasserstein DRO) replaces the expected loss under an empirical distribution by the worst-case expected loss over all distributions within a Wasserstein distance of it. It is used in operations research, statistics and machine learning to guard decisions and predictors against the gap between the sample and the population. The statistical question it raises is how large must be for the robust loss to bound the true loss with high probability. Classical answers go through the concentration of the empirical measure in Wasserstein distance, which forces in dimension : the curse of dimensionality.
Gao (arXiv:2009.04382; Operations Research, 2023) shows that a radius of order suffices, independently of the dimension. The first ingredient, and the subject of this mission, is a new concentration inequality for the empirical mean of a single loss function, whose rate is governed by the Wasserstein regularizer itself.
Let be a separable Banach space with norm and let . is the set of Borel probability measures with , and the Wasserstein distance of order is
the infimum over couplings of and . For a loss , a nominal distribution and a radius , the Wasserstein regularizer is the excess of the robust loss over the nominal loss,
The data are i.i.d. samples from an unknown ; is their joint law and is the empirical loss. A distribution satisfies the transportation-information inequality if
with the relative entropy. holds for every distribution with a Gaussian moment , and (Talagrand's inequality) is implied by a log-Sobolev inequality.
The rate function is built from
If with and satisfies , then for every
and for every , with probability at least ,
Theorem 1 says that the large-deviation rate of the empirical loss is the inverse of the Wasserstein regularizer, and that the regularizer at radius is a valid high-probability correction of the empirical loss. Neither involves the dimension of or the complexity of a covering of it. The paper builds its covering-number and local-Rademacher guarantees for Wasserstein DRO (Sections 4.1–4.2, the subject of two companion missions) on this single-function result, and Corollary 1 recovers, for , the Lipschitz-norm bound known from transportation inequalities while sharpening it for .
The results are proved in the paper; none is formalized. A complete development would give a machine-checked tensorization of transportation-information inequalities on Banach spaces and a Marton–Herbst-type concentration argument, both of which are used well beyond DRO.
The proof combines three ingredients that Mathlib does not yet connect. Tensorization (Lemma 4) needs disintegration of a measure on and the chain rule for relative entropy, together with a gluing of couplings and Hölder's inequality for the dimension constant. Lemma 5 combines with Kantorovich duality for the cost and the entropy of an exponential tilt, then optimizes a Young-inequality split over two parameters for , and extends from bounded to -growth by monotone truncation. Proposition 1 rests on the strong duality (1) of Gao and Kleywegt, an external result, and on the first-order optimality condition of a convex perspective function. A naive approach that bounds the deviation by fails: that distance decays like , which is exactly the curse the theorem avoids.
The source is arXiv:2009.04382; its printed page numbers equal the PDF's. The Lean development lives in the namespace WassFSG.Conc and uses these conventions:
klDiv.A formalization that reads an infinite through a real coercion would turn the tail bound into the trivial bound ; the conventions above rule this out. Likewise a regularizer whose supremum ranged only over measures supported on the sample, or a condition over a restricted class of , would be a different statement.
Contributions welcome: Lemma 4 and Corollary 1 are independent entry points; a proof of the duality (1) under the paper's growth condition would be reusable by every Wasserstein DRO mission.
In a stochastic linear–quadratic (LQ) optimal control problem a controller steers a linear stochastic differential equation and pays a quadratic cost. When the cost weights are allowed to be indefinite — as in mean–variance portfolio selection, where the control weight is zero — the problem can still be well posed, and two different notions of solution appear. An open-loop optimal control is a process chosen for one given initial pair . A closed-loop optimal strategy is a feedback law that is optimal for every initial state at once. A closed-loop optimal strategy yields an open-loop optimal control for each initial state; the converse is the question.
Timeline. Chen, Li and Zhou (1998, doi:10.1137/S0363012996310478) started the theory of indefinite stochastic LQ control. Ait Rami, Moore and Zhou (2002, doi:10.1137/S0363012900371083) introduced the generalized Riccati equation with a Moore–Penrose pseudoinverse and stated that, for Problem (SLQ) with continuous coefficients and , a continuous open-loop optimal control exists at every initial pair if and only if the Riccati equation has a solution satisfying a range condition and a sign condition. Sun and Yong (2014, doi:10.1137/140953642) characterized closed-loop solvability by regular solutions of that Riccati equation. Sun, Li and Yong (2016, doi:10.1137/15M103532X) showed by two explicit examples that the 2002 equivalence fails in both directions, and that open-loop solvability is strictly weaker than closed-loop solvability. This mission formalizes those examples.
Let be a standard one-dimensional Brownian motion on a probability space and its augmented natural filtration. For and a control in the space of -progressively measurable -valued processes with , the state equation is
and the cost is the expectation of plus the time integral of a quadratic form in with weights and linear terms . Problem (SLQ) is the case , with cost and value function .
The Riccati equation (4.6) is
where is the Moore–Penrose pseudoinverse. A solution is regular if (4.7) a.e., (4.8) , and (4.9) a.e.
Example 7.1 is Problem (SLQ) with , , :
that is, , , , , , .
For every ,
while , and for every the problem is not closed-loop solvable on .
For and , the Riccati equation (7.12) has the unique solution , which satisfies (4.7) and (4.9), yet no open-loop optimal control exists at , .
The result. Example 7.1 refutes the necessity half of the Ait Rami–Moore–Zhou criterion: a continuous open-loop optimal control exists at every initial pair, but the Riccati equation has no regular solution. Example 7.2 refutes the sufficiency half. Together they show that the Riccati equation with conditions (4.7) and (4.9) characterizes neither notion, and that open-loop solvability is strictly weaker than closed-loop solvability; Example 7.1 also exhibits a finite value function that is discontinuous in time. These facts are why the paper develops separate characterizations of open-loop solvability (through the regularized Riccati solutions ) instead of the Riccati equation itself.
Formalizing it. The examples are proved in the paper by appeal to its Theorems 5.3 and 6.2 and to Theorem 4.3 from Sun–Yong (2014). Nothing in this chain is machine-checked anywhere. A formal proof of the goal must verify the explicit optimal control against the canonical stochastic state equation, compute the value function, and rule out every closed-loop strategy; it can use Theorem 4.3 (posed here as a milestone) or a direct argument. The definitions built here (the stochastic LQ problem, the pseudoinverse Riccati equation, regularity) are shared with the other missions of this series.
Open-loop optimality looks immediate because , but it requires showing that the state driven by hits at time , which means identifying the solution of the stochastic state equation for this control. The value at requires the degenerate interval to be handled inside the same SDE framework. The hard part is the negative claim: it quantifies over all feedback pairs with , and must show that no such pair drives every initial state to at time . The paper reduces this to Theorem 4.3, whose proof (in Sun–Yong 2014) is a substantial piece of stochastic LQ theory; checking that fails the range condition is the easy end of that chain.
Time is , vectors are Fin k → ℝ, inner products are dot products, and . The Brownian motion is the published Peng1990.SMP.IsStdBrownian, the filtration the published augmented filtration, the SDE solution concept the published Peng1990.SMP.SolvesSDE, and the pseudoinverse the published HarmonicGames.Decomposition.pinv.
Proving only that violates (4.7) does not settle the goal: the goal is about solvability of the control problem itself, and "not closed-loop solvable on any " is stated for every , not as the failure on some interval.
Contributions are welcome on any milestone, on the well-posedness of linear SDEs in this framework, and on the pseudoinverse identities (Penrose equations, the pseudoinverse of a scaled symmetric matrix) that the Riccati computations need.
Linear–quadratic (LQ) optimal control is the basic test case of stochastic control: a linear stochastic differential equation, a quadratic cost, and an optimal control that one expects to be a linear feedback of the state computed from a Riccati equation. In the indefinite stochastic case the weighting matrices , , carry no sign condition. The cost can then be convex without being uniformly convex, an optimal control may fail to exist although the value is finite, and the Riccati equation may have no solution of the kind the classical theory needs.
Sun, Li and Yong (SIAM J. Control Optim. 54 (2016) 2274–2308) separate finiteness, convexity, open-loop solvability and closed-loop solvability for this problem. This mission covers their Section 6. Under uniform convexity the optimal control is the Riccati feedback of Corollary 4.7. Section 6 removes uniform convexity: it regularizes the control weight to , takes the Riccati feedback control of each regularized problem, and shows that open-loop solvability of the original problem is exactly the convergence of along some sequence .
Timeline. Chen, Li and Zhou (SIAM J. Control Optim. 36 (1998)) introduced indefinite stochastic LQ problems. Ait Rami, Moore and Zhou (SIAM J. Control Optim. 40 (2002)) introduced the generalized Riccati equation with a pseudoinverse. Sun and Yong (SIAM J. Control Optim. 52 (2014)) characterized closed-loop solvability by regular solutions of that equation. In 2016 Sun, Li and Yong characterized uniform convexity by strongly regular solutions and open-loop solvability by the regularized feedback sequence treated here.
Fix a horizon and a probability space carrying a one-dimensional standard Brownian motion , with the augmented natural filtration of . For an initial pair and an admissible control , an -progressively measurable -valued process with , the state solves
The cost is
The coefficients and are deterministic, are random, and the integrability conditions are (H1)–(H2). The value function is . A control is open-loop optimal at if for every . Problem (SLQ) is the case , with cost .
For let be the strongly regular solution of the Riccati equation (5.7),
where for some and . Let be the adapted solution of the linear backward equation (4.11) for these data, and put
With the solution of the closed-loop system , , the regularized feedback sequence is
is a Hilbert space with inner product ; weak and strong convergence of controls refer to it.
Assume (H1)–(H2) and that is convex. For the following are equivalent:
and every weak or strong limit of such a subsequence is an open-loop optimal control at . The goal assumes convexity, not uniform convexity, and no finiteness.
Two further statements follow the goal: open-loop solvability is equivalent to (p. 2303), and Proposition 6.4: if , the Riccati equation (4.6) has a regular solution and Problem (SLQ) is closed-loop solvable.
Theorem 6.1 gives a minimizing sequence computed from Riccati and backward equations whenever the problem is finite. Theorem 6.2 turns it into a test for open-loop solvability that needs no uniform convexity and no regular solution of the original Riccati equation. When an optimal control exists, it is recovered as the limit of feedback controls. Proposition 6.4 converts a bound on the gains into closed-loop solvability of the homogeneous problem. Section 7 of the paper shows that open-loop solvability does not imply closed-loop solvability, so a criterion phrased directly in open-loop terms is needed.
All of these results are proved in the paper. None of them, nor the solution theory of stochastic LQ problems they rest on, had a machine-checked proof on Prove2Me or in Mathlib as of October 2026. A formal development needs the well-posedness of linear SDEs and BSDEs with integrable coefficients, the Riccati theory of Section 4, and the Hilbert-space structure of the space of admissible controls. Those parts are reusable for any stochastic LQ problem.
The obvious approach takes any minimizing sequence and extracts a weakly convergent subsequence. That fails without uniform convexity: a minimizing sequence need not be bounded, and boundedness is exactly what open-loop solvability provides in (6.7). The converse direction needs the limit of the regularized costs to identify the value, which requires both the minimizing property of (Theorem 6.1) and weak lower semicontinuity of . That in turn rests on convexity being transported from to through Corollary 3.4 and the zero extension. Upgrading weak to strong convergence uses the norm bound (6.7) with the limit itself as the optimal control. Every step depends on Corollary 4.7, the Riccati representation of the optimal control of the regularized problem, whose proof requires the theory of Section 4.
The probability basis is a probability space with a one-dimensional standard Brownian motion and its augmented natural filtration. Vectors are Fin k → ℝ and matrices Matrix (Fin k) (Fin l) ℝ. Time is ℝ≥0, and is the Euclidean dot product u ⬝ᵥ u. (H1)–(H2) are standing assumptions, with entrywise conditions on the matrix coefficients. The state from is a strong solution of the published SDE notion Peng1990.SMP.SolvesSDE whose coefficients are switched on at ; it has a.s. continuous paths and . The cost is evaluated along a chosen solution, which is unique. is an infimum in the extended reals. Limits in are taken as . "A subsequence" is a sequence with , and the limit control is required to be admissible. The backward equations use the published Peng1990.SMP.SolvesBSDE, and the pseudoinverse in (4.6) and (4.11) is the published HarmonicGames.Decomposition.pinv.
Theorem 6.1 prints the term in its backward equation. The equation (4.11) that its proof uses through Corollary 4.7 has , and the formalization uses (4.11). Corollary 3.4 is stated without its item (vi), which involves an operator that the paper quotes from another source.
The families , and are hypotheses pinned by their equations for every . The sequence is therefore the Riccati feedback sequence (6.2), never an arbitrary minimizing sequence or an arbitrary family of -optimal controls; with such a family the implication (ii) ⇒ (i) would be a different theorem.
Contributions are welcome at every level: the solution theory of linear SDEs and BSDEs, Itô's formula for quadratic forms, Riccati and Lyapunov equations in integral form, weak compactness in , and the milestones themselves.
In decentralized optimization, agents connected by a communication network jointly minimize a sum of private functions without a central coordinator: each agent sees only its own and talks only to its neighbours. Applications include sensor networks, distributed estimation, multi-agent control and learning over data spread across machines. The simplest method in this setting is decentralized gradient descent (DGD), in which every agent averages its neighbours' iterates and then takes a local gradient step. DGD and its relatives were analysed by Nedić and Ozdaglar (IEEE TAC 2009) and many later papers, almost always under the assumption that the (sub)gradients are bounded.
K. Yuan, Q. Ling and W. Yin (arXiv:1310.7063v3; SIAM J. Optim. 26(3), 2016) removed that assumption for DGD with a fixed stepsize. They showed that a stepsize bound depending on the spectrum of the mixing matrix keeps the gradients bounded, that the agents stay within of their mean, and that for convex smooth the objective error of the mean decreases at rate until it reaches a neighbourhood of size . This mission formalizes that last result, Theorem 2 of the paper, together with the lemmas its proof rests on.
Consider agents on a connected undirected graph . Agent holds a function , and the agents solve
with solution set , assumed nonempty.
A mixing matrix is symmetric and doubly stochastic, and only if or and are neighbours. Its eigenvalues are , and
Assumption 1 (p. 4): (a) each is convex, bounded below, and differentiable with an -Lipschitz gradient, ; (b) the network is connected and is symmetric, doubly stochastic, with .
DGD with stepsize , started from , is
Stacked vectors carry the Euclidean norm. Write , , , , , , , and
The paper reads DGD as unit-step gradient descent on the Lyapunov function
For a minimizer of and a solution , set
Let and . Then
and, for , if for every , then
The paper prints these as and . The constants are the ones its proof fixes: the recursion with (milestone below) and the threshold condition "", under which the error term absorbs half of the quadratic decrease. That gives , and " increases at " with this constant gives .
Theorem 2 is the convex, non-strongly-convex case of the paper's analysis. It says that DGD with a constant stepsize behaves like centralized gradient descent, with rate , until it reaches a floor of size . The floor shrinks with the stepsize and grows as the spectral gap of the network closes, which makes the trade-off between speed, accuracy and network connectivity explicit. The result is proved without bounded gradients; the boundedness comes out of the stepsize condition through the Lyapunov function. It is the baseline that exact methods such as EXTRA (Shi et al. 2015) were designed to improve on.
The paper's proof is complete in its main lines but informal in places: the rate is stated with , the constant is written with a -dependent , and the minimizer of is asserted to exist on grounds that do not suffice. To our knowledge no part of this analysis (DGD, mixing matrices with spectral bounds, the Lyapunov reformulation) has been machine-checked. A formal proof fixes the constants, records the needed hypotheses, and supplies decentralized-optimization infrastructure that Mathlib lacks.
The obvious approach treats the mean as gradient descent on with the exact gradient , which fails: by (15) the mean moves along , the average of gradients taken at different points. Controlling needs the consensus bound of Lemma 1, which in turn needs the gradients to be bounded, and no assumption bounds them. They are bounded only because DGD is unit-step gradient descent on and the stepsize condition makes that descent monotone (Theorem 1). Lemma 1 also needs the operator-norm identity for a symmetric doubly stochastic , a spectral fact about sorted eigenvalues. Finally, the recursion in needs a bound on that is uniform in , which comes from Fejér monotonicity of the iterates with respect to a minimizer of , not from anything about .
is EuclideanSpace ℝ (Fin p) and stacked vectors are PiLp 2 (fun _ : Fin n => ℝᵖ), so every stacked norm (, , ) is Euclidean on , not the sup norm. Gradients are Mathlib's gradient. DGD is a recursively defined sequence started at , not an arbitrary sequence with a property. and come from the eigenvalues of the symmetric sorted with multiplicity (eigenvalues₀). is , and is a supremum over the finite index set, i.e. a maximum.
Conventions and additions, each disclosed in the item statements:
Trivializing formalizations are ruled out. The iterates are the DGD recursion itself. The threshold in the rate is required at every earlier step, not only at step . does not depend on . The constants and are explicit, not an existential placed before the data. A sorry-free instance (, , constant ) shows that the goal's hypotheses can all hold together.
A complete development needs: the operator norm of via the spectral theorem, the descent lemma and co-coercivity for -smooth convex functions on Euclidean space, for -smooth functions bounded below, and Fejér monotonicity of gradient descent. These are reusable well beyond this mission. Contributions to any milestone are welcome; Lemmas 1–2 and (15) do not use convexity.
Liouville quantum gravity (LQG) equips a planar domain with a random area measure and a random boundary length measure . Both are built from an instance of the Gaussian free field (GFF). The Schramm–Loewner evolution is the conformally invariant random curve that describes interfaces in critical planar models. Sheffield's paper (arXiv:1012.4797, Ann. Probab. 44 (2016)) shows that the two are linked by a conformal welding. Zipping up a free boundary GFF by a reverse Loewner flow glues two boundary arcs of equal quantum length, and the glued seam is an curve.
This "quantum zipper" is the starting point of the mating-of-trees programme (Duplantier–Miller–Sheffield, arXiv:1409.7055). It is also the mechanism behind the conjectured, and partly proved, scaling limits of random planar maps decorated by statistical-physics models.
Timeline:
, and the free boundary Green's function is . Fix and put and .
which by Theorem 1.2 has the law of modulo additive constants.
as a vague limit. The area measure is the analogous limit with circle averages and exponent .
Almost surely, for every on and the two real points that maps to ,
The statement is scale free: it does not depend on the additive constant of .
Theorem 1.3 says that reverse SLE zipping is a welding by quantum length. Combined with the removability of for , it gives Theorem 1.4: the field determines the curve . The same equality of boundary lengths on the two sides of an SLE is the defining property of the quantum-zipper and mating-of-trees constructions, which build random surfaces by welding wedges together.
All results here are proved in the paper, and none has a machine-checked proof. The proofs are partly sketches: Proposition 5.5 ends with a limiting estimate, and the zero–one step of Theorem 1.8 is delegated to [DMS14a, Lemma 8.2]. A formal development would therefore check the most cited welding argument in random conformal geometry. The definitions it needs (arc averages of a GFF, , quantum wedges, conditionally Gaussian fields) are reusable for any LQG statement.
The obvious argument tries to compare the left and right boundary measures directly, ball by ball along the curve. It fails because the two measures depend on the field near the curve in the same way (5.1): nothing local distinguishes them, and nothing local forces them to agree. The paper instead builds a stationary picture (Lemma 5.6, Proposition 5.5, Figure 1.7). It shows that the curve splits a -wedge into two independent -wedges, and it uses the ergodic theorem with scale invariance to force the ratio of the two lengths to be a constant , which symmetry makes equal to . The last step transfers the result from the wedge to the field of Theorem 1.3 by absolute continuity. Every step uses Gaussian conditioning on random conformal images of the field, which current libraries lack.
Conventions committed to in Lean:
IsBrownianReal. Flows are pathwise ODE solutions, with no stochastic integrals.OAI.SLEExactGauge.IsOrdinaryChordalSLE.Disclosed readings of the text:
Contributions are welcome on any of the following:
A forward–backward stochastic differential equation (FBSDE) couples a forward diffusion with a backward equation for a pair whose terminal value depends on . Such systems arise from the stochastic maximum principle, from option pricing with large investors, and from stochastic differential games. Whether an FBSDE with Lipschitz coefficients has a unique solution on an arbitrary horizon is a classical question: small-time solvability is easy, but global solvability can fail even for linear equations.
J. Ma, Z. Wu, D. Zhang and J. Zhang, On well-posedness of forward–backward SDEs—a unified approach (arXiv:1110.4658v2, Ann. Appl. Probab. 25 (2015)), reduce well-posedness to the existence of bounded solutions of two deterministic dominating ordinary differential equations, obtained from the difference quotients of the coefficients. For linear FBSDEs with constant coefficients the two dominating ODEs coincide, and the authors give sharp criteria for global solvability. This mission formalizes the criterion in the case , where the dominating ODE has a rational right-hand side with a pole.
Earlier global results for coupled FBSDEs rested on the four-step scheme (Ma–Protter–Yong 1994) or on monotonicity conditions (Hu–Peng 1995); §7.4 of the paper compares the dominating-ODE approach with these methods.
The linear FBSDE (4.1) with constant coefficients is determined by nine reals and a terminal slope . Its dominating function is (3.9),
defined for . When it can be rewritten as (5.8),
for constants . The dominating ODE (5.3) is the backward integral equation
The paper needs a solution satisfying (5.9): both and are bounded on . Since , this forces (Remark 5.5).
The comparison tool is Lemma 5.1. For measurable it gives a unique solution of lying between a sub-solution and a super-solution of perturbed equations (5.2).
For and , the ODE (5.3) has a solution satisfying (5.9) for every if and only if one of the following holds:
The limit alternatives in cases 3 and 4 are not printed in the paper. Without them the equivalence is false. Take , , , all other coefficients , and . Then , and satisfies (5.9) on every horizon, yet none of the printed cases holds. The gap is in the Appendix (p. 48): it asserts that is positive on the closed interval when , which fails when the polynomial part vanishes at the pole. A companion item records the counterexample.
The milestones follow the paper's proof:
In the paper, Theorem 5.6 is the sharp solvability criterion for linear FBSDEs with constant coefficients and . The paper describes these sharp conditions as setting the "limits" for the solvability of general FBSDEs, and the nonlinear Theorems 5.9–5.11 and the main well-posedness Theorem 7.4 are modelled on them. Because the criterion is an equivalence, it also says when no regular decoupling field can be built from the dominating ODE, whatever the horizon.
The result is proved in the paper, but the printed statement is not correct as an equivalence (see above). The mission states and asks for a corrected version, a machine-checked counterexample to the printed one, and formal versions of each step of the proof. The deterministic parts (comparison for backward integral equations, finite-time blow-up of scalar autonomous ODEs, pole-reaching for rational vector fields) are basic real analysis with no current Lean library. They are reusable well beyond FBSDEs. No part of this paper has a machine-checked proof.
Each sufficiency case is an a priori bound: a comparison with a constant or explicitly solvable equation keeps the solution in a fixed interval away from the pole. The difficulty is on the necessity side, where three kinds of failure must be excluded:
The obvious argument for the last case, " is bounded below by a positive constant up to the pole", is exactly what fails when tends to at the pole. There the solution approaches the pole only asymptotically, and the right criterion is the corrected one above. A second subtlety is that is only locally Lipschitz off the pole, so comparison must be carried out on a band in which the solution provably stays.
Time is real, with and . The coefficients form a record Coeffs of nine reals, and Coeffs.F is (3.9) verbatim. A solution on is a function such that, for every , the integrand is integrable on and ; values outside are irrelevant. Condition (5.9) is a uniform bound on together with for some . "For arbitrary " is a universal quantifier over outside the existential.
Lean's conventions are total, so several trivializing formalizations are ruled out explicitly:
Coeffs.F a junk value at the pole. No statement evaluates there: every zero point, bound and limit in the statements lives strictly on one side of .The constants of (5.8) enter the necessity milestones only through the decomposition hypothesis, never through a formula.
The development needs a Picard–Lindelöf or comparison argument for backward scalar integral equations with locally Lipschitz right-hand sides, monotonicity of autonomous scalar solutions, and the intermediate value theorem. Contributions of a general comparison lemma for scalar integral equations would serve this mission and both other missions of the series.
A variational inequality asks for a point of a convex set at which a vector field points "inward" against every feasible direction. It covers constrained convex minimization (with ), saddle-point problems, Nash equilibria of convex games and complementarity problems, which is why projection methods for it are a standard topic in optimization and numerical analysis.
The classical methods for a monotone, -Lipschitz field (Korpelevich's extragradient method, Tseng's forward–backward–forward method, the subgradient extragradient method of Censor, Gibali and Reich) use a constant step or a backtracking search for one. Yu. Malitsky's paper (arXiv:1502.04968v1; SIAM J. Optim. 25(1), 2015, doi:10.1137/14097238X) introduces the projected reflected gradient method, which needs one projection and one evaluation of per iteration. Its constant-step version requires , and so requires knowing , which is rarely available in practice (§4, p. 8). Section 4 removes that requirement: Algorithm 4.2 chooses its step from local information only and corrects it when a computable test fails. This mission formalizes the paper's convergence theorem for that algorithm, Theorem 4.4.
Let be a real Hilbert space with inner product , nonempty, closed and convex, and . Write for the metric projection onto . The variational inequality (1.1) asks for with
and denotes its solution set. The standing conditions (p. 1) are (C1) ; (C2) is monotone, ; (C3) is -Lipschitz, , with .
Algorithm 4.2 (pp. 8–9) has parameters , and a cap , and adopts the convention . It starts from with , , and . For it uses the step rule
forms the trial values , , , and evaluates a test quantity built from these. If the trial is accepted. Otherwise, in step (4.i) () the step is replaced by some satisfying (4.2), and in step (4.ii) () the reflection is replaced by for some satisfying (4.3), with a step satisfying (4.4); is then recomputed. The values kept after iteration are the corrected ones. A sequence produced this way is a run of Algorithm 4.2. The Lipschitz constant appears nowhere in the algorithm.
Under (C1)–(C3), for every run of Algorithm 4.2 there is with
where is weak convergence in .
In the order the proof uses them:
The supporting lemmas 2.2 (Minty), 2.3 (Opial) and 2.7 are included as plain items, together with a statement that runs exist from every .
The result shows that the projected reflected gradient method keeps its weak convergence guarantee when the step is chosen adaptively, without knowledge of , at a cost of at most two projections per iteration (one in most iterations, per the experiments of §5). Adaptive step rules of this kind, based on the local ratio , recur in later work on reflected and golden-ratio methods for variational inequalities (e.g. Malitsky 2020, arXiv:1803.08832), so a formal treatment of the run predicate and its energy inequality is reusable beyond this paper.
The theorem is proved in the paper; it has no machine-checked proof that this mission knows of. The work here is to formalize the definitions of Algorithm 4.2, its well-definedness, the energy inequality and the closing weak-limit argument in a general Hilbert space. The proof as printed has a gap, described under Difficulty; a formal proof would either close it or show that the statement needs an extra hypothesis.
Lemma 4.3 is the bookkeeping core. It has five cases depending on how compares with and on the sign of a norm expression. In the case where the reflection is changed, the previous iterate must be reinterpreted as the projection of a point on a segment (via Lemma 2.4) before the estimate of the constant-step method applies.
The closing argument needs the step sizes to stay away from zero, so that the limit can be taken in the optimality inequality for the iterates. The paper asserts that is a lower bound of , "from Lemma 4.2" (p. 12). The proof of Lemma 4.2 shows only that the step rule is at least , and that only under . In step (4.ii) the algorithm allows any satisfying (4.3) and any , so an admissible run can take arbitrarily small at such steps. The step regrows by the factor at later steps, but the printed proof does not control this. The obvious first attempt, citing a uniform lower bound , does not work as stated.
All objects live in one definitions item. is a general real Hilbert space, never . The projection is a nearest point chosen by choice, with a junk value when none exists. Every theorem that uses it assumes closed and convex together with a nonemptiness source, so the junk branch is never reached. Weak convergence is for all . (C3) uses a real constant . The convention is encoded by omitting the ratio term from the minimum when its denominator is zero, never by Lean's .
A run is a relation: the corrections , range over all admissible values, and nothing selects the largest. The stopping rule of step 3 is not encoded. A run whose residual vanishes continues as a constant sequence through the branch . Indices are used only for , and is a separate parameter.
The goal assumes exactly (C1)–(C3), , and . It assumes neither nor any lower bound on . Adding such a bound would assume the unproved step of the paper's argument. The milestone on carries and as explicit, disclosed hypotheses. Lemma 4.3 and (4.10) are stated without (C1) and (C3), which their proofs do not use. A formalization that concluded norm convergence, specialized to finite dimension, or fixed one particular choice of corrections would be a different theorem.
The development needs the existence and characterization of the metric projection onto a closed convex set, Minty's lemma, Opial's inequality and weak sequential compactness of bounded sets in Hilbert space. These pieces are reusable for other projection methods. Contributions toward any milestone are welcome, as is a resolution of the lower-bound question for .
Networks of identical dynamical systems coupled along a directed graph model power grids, sensor and robot swarms, neural populations and coupled oscillators. A basic control question is how to steer every node of such a network onto a prescribed reference trajectory by acting directly on only a few nodes. This is pinning control: feedback is injected at a small set of pinned vertices, and the coupling has to carry the reference signal to the rest of the network.
For undirected or strongly connected networks, criteria for pinning synchronization go back to Wang and Chen (2002) and Chen, Liu and Lu (2007), and the first mission of this series treats the strongly connected case of Yu, Chen, Lü and Kurths (2013). Many networks of interest are not strongly connected: information flows down a hierarchy of groups, and the minimal requirement for the reference to reach every node is that the network, with the reference added as a virtual leader, contains a directed spanning tree rooted at the leader. Section 4 of that paper gives a criterion for this general case that splits into one condition per strongly connected component. This mission formalizes that criterion, Theorem 4.5, with the lemmas its proof uses and three corollaries.
There are vertices with states . The coupling configuration matrix has for , where records a connection from vertex to vertex , and zero row sums, . Given a function , a coupling strength , an inner coupling matrix and pinning gains (vertex is pinned when ), the controlled network is
where the reference solves . The network is globally synchronized when for every vertex and every pair of solutions.
The nonlinearity is controlled by Assumption 1: there is a matrix with for all and . Throughout §4 the paper also assumes that and commute, that is positive definite, and puts .
The vertices split into strongly connected components . In the Frobenius normal form the components are ordered so that no edge goes from a later component to an earlier one, which makes block lower triangular. For each component the mission uses three matrices:
In Lean, component membership is a map blk : Fin N → Fin M, and Fin M carries the Frobenius order.
If, for every component ,
then the controlled network with a directed spanning tree is globally synchronized.
Theorem 4.5 replaces a single matrix inequality for the whole network with inequalities, one of the size of each component. In practice the test runs component by component down the Frobenius order: decide which components need pinning, choose gains for each one separately, and get synchronization of the whole network. Corollary 4.7 makes this explicit in terms of the outer in-degrees: a component with no incoming edges from earlier components has to be pinned (Remark 4), while a component that receives enough weight from upstream needs no control. These conditions underlie the pinning scheme algorithm of §5 of the paper.
On the formal side, as far as a search of the platform and of Mathlib shows, none of these results is machine-checked. Mathlib has the positive semidefinite Schur complement and irreducible nonnegative matrices, but not the strict Schur complement, block-diagonal Lyapunov scaling, or Lyapunov arguments for networked ODEs with Kronecker-structured couplings. The mission produces, beyond the paper's theorem:
The obvious argument is to take one Lyapunov function weighted by a positive left null vector of the whole coupling matrix, as in the strongly connected case. Here it fails: the coupling matrix of a network that is not strongly connected has no positive left null vector, and condition (4.8) is local to each component. The central step is the passage from blockwise to global negative definiteness (Lemma 4.4). Condition (4.8) says nothing about the off-diagonal blocks that couple a component to earlier ones, and a block lower-triangular matrix whose symmetrized diagonal blocks are negative definite need not have a negative definite symmetric part; the component weights have to be found so that those couplings are dominated, which is a quantitative statement about Schur complements. Turning the resulting matrix inequality into convergence of the trajectories then needs a differential inequality on , a Kronecker-product definiteness argument with , and the commutation of and to reach the θ bound.
States are Fin n → ℝ and matrices are indexed by Fin N, Fin n, or the subtype of one component's vertices. Solutions are functions on ℝ that satisfy their ODE on through HasDerivWithinAt … (Set.Ici 0). "For any initial conditions" means for every pair of solutions ; existence of solutions is not claimed. Convergence is componentwise, which agrees with every norm on . "Positive definite" is Mathlib's Matrix.PosDef, which includes symmetry, and is (-X).PosDef. is the least Rayleigh bound, IsLamMax, never a supremum of a possibly empty set.
The vertices are not permuted into Frobenius form. The hypotheses say instead that:
The weights are tied to the paper's object by . The standing assumptions of p. 1402 (Assumption 1, , , ) are hypotheses of every goal-level statement. The goal does not assume the weights , the bound (4.10), or definiteness of a whole-network matrix; it assumes only (4.8) on each component, so it cannot be trivialized by assuming its own conclusion. For the hypothesis cannot be met, so that degenerate dimension is excluded.
The pages contain three misprints. (4.10) has "" in its third line and "" in its last; the last line, with a single , is formalized. Corollary 4.9 ranges "" where the component range is meant.
A complete development needs a Gronwall-type decay lemma on , the strict Schur complement, definiteness of Kronecker products, and the square root of a positive definite matrix commuting with matrices that commute with it. Each of these is reusable well beyond this mission, and contributions to any of them are welcome, as are proofs of the milestones in any order.
The stochastic block model is the basic random-graph model of a network with communities. It serves as a test bed for clustering algorithms in statistics, machine learning and theoretical computer science. In its sparse two-community form, each vertex has a constant expected degree, and the question is how much of the hidden partition a graph reveals. Using the cavity method of statistical physics, Decelle, Krzakala, Moore and Zdeborová (arXiv:1109.3041, 2011) conjectured a sharp threshold: one can label the vertices better than chance when the signal-to-noise ratio exceeds one, and not otherwise.
Timeline:
Fix and let be the number of vertices. In every vertex receives, independently and uniformly, a label . Then each unordered pair is an edge independently, with probability if and otherwise. Write
for the average degree and the signal strength; may be negative.
An estimator receives only the graph and outputs a labelling, possibly at random. Its overlap with the planted labelling is , with an absolute value because the two communities carry no names. A uniformly random guess has overlap of order .
The proof works with paths in the complete graph: consecutive vertices distinct. A path is non-backtracking if and self-avoiding if all its vertices are distinct. With and , the path sums and add over the non-backtracking, respectively self-avoiding, paths of length from to . An -tangle is a connected subgraph of diameter at most that contains two cycles.
For fixed with there are an estimator and an with
The goal fixes neither nor the algorithm, so it is the weakest form of the conjecture.
Together with the impossibility result for , Theorem 2.1 establishes as the detection threshold of the sparse two-community block model, a threshold first predicted by statistical physics. It equals the Kesten–Stigum bound for reconstruction on the Poisson Galton–Watson tree with the Ising channel, which locally describes the model. The non-backtracking and self-avoiding path statistics behind it led to the later spectral analyses of the non-backtracking matrix and to the multi-community theory.
The theorem is proved on paper. As far as is known, none of its ingredients is machine-checked: no formal statement of the block model, of path-count moments in sparse random graphs, or of tangle-freeness exists in Mathlib. The mission produces a faithful statement of the threshold theorem together with the first-moment, second-moment and combinatorial estimates the proof rests on. These can be attacked independently.
The obvious approach estimates by the sign of the number of length- paths between and , with . Its mean is right: it is of order . Its variance is not under control. With probability about a clique of size appears near and , and on that event the number of paths is so large that the expectation is dominated by a rare configuration. A plain second-moment argument therefore fails. The rare dense structures (tangles) must be excluded by conditioning, and the non-backtracking count must be compared with the self-avoiding one, whose moments can be computed. Even then, the second moment determines only with probability bounded away from . Turning many weakly correlated pairwise estimates into a globally correlated labelling is a separate step close to the threshold, where is barely above one.
Everything is a finite sum. Vertices are Fin n, graphs SimpleGraph (Fin n), labellings Fin n → Bool. The joint law of is written as an explicit weight. Conditioning on the labels of a vertex set is a weighted average with positive denominator . An estimator is a map from graphs to PMFs on labellings, so it never sees and may be randomized. Its success probability is the probability that the overlap, with absolute value, is at least , for an fixed before .
Asymptotic notation follows §1.3 of the paper. is for an explicit chosen before the vertices, sets and labellings it is uniform over. "Sets of size " in a hypothesis means: for every , all sets of size at most . Assumption 2.7 ( and ) and the preamble of Theorem 2.8 (, the choice of , ) are shared definitions, so the four displays of Theorem 2.8 cannot drift apart. Non-asymptotic statements assume , which is Definition 1.1's .
Three printed slips are corrected and disclosed. Theorem 2.8 (2) carries the square that the proof's display (17) gives. Theorem 2.8 (4) uses , since may be negative. Lemma 4.7 assumes distinct endpoints, as all its uses do.
The labelled branching tree of Lemma 3.7 is encoded by its generation counts: the numbers of and labelled vertices at depth form a two-type Poisson chain on , which has the same law by Poisson thinning and superposition. Lemma 3.7 assumes , the standing assumption of its section, and is stated for all sufficiently large , the range its proof covers.
The statements rule out the trivial readings: the estimator cannot see , the overlap carries its absolute value, does not depend on , antecedent bounds are universally quantified, and the model's weights are genuine probabilities for all large .
Reusable infrastructure includes the finite-sum stochastic block model, path edge-type counts, and tangle-freeness. The weights of independent-edge random graphs and the Poisson Galton–Watson tree with the Ising broadcast are also of independent use. Contributions are welcome on any milestone, on infrastructure lemmas such as normalisation of the model's weights and independence of distinct edges given the labels, and on the steps of §3 that connect Theorem 2.8 to the goal.
Unit commitment (UC) is the day-ahead decision of an electricity system operator: which generators to switch on in each hour of the next day, and how much each of them should produce. System operators solve UC problems every day, and their cost and reliability are first-order concerns of power-system operations. With a large share of wind and solar generation, the net load (demand minus renewable output) at each node is uncertain at commitment time, and robust optimization is one of the standard ways to commit units that remain operable for every load trajectory in an uncertainty set.
The robust UC literature first adopted the two-stage model (Jiang et al. 2012; Zhao and Zeng 2012; Bertsimas et al. 2013): commitments are chosen first, then the dispatch is chosen after the whole day's net loads are revealed. In reality the operator learns the loads hour by hour, so the dispatch at hour may only use what has been observed up to . Lorca, Sun, Litvinov and Zheng (2016) introduced the multistage robust UC model that imposes this non-anticipativity, and asked when the extra realism matters. Their answer is this mission's goal: it matters only through the ramping constraints.
There are generators , net-load nodes , lines and hours .
The two-stage robust UC (2) minimizes over
where the dispatch is chosen knowing the whole trajectory . The multistage robust UC (5) minimizes over
over policies that depend only on and satisfy the dispatch constraints for every .
With the ramping constraints deleted from both models,
and consequently the two problems have the same optimal value over .
Both sides are compared with problem (1P), whose objective is
On a two-bus, two-hour system with line limit and ramp rates equal to , the two-stage model is feasible (Proposition 1), yet under its commitment no causal dispatch policy is feasible (Proposition 2). These show that the hypothesis "without ramping constraints" cannot be dropped.
The theorem locates exactly where multistage robust UC differs from the two-stage model: in the inter-temporal coupling created by ramping. Without ramping, the hourly dispatch problems decouple and so does the uncertainty set, so seeing the future gives the dispatch no advantage. With ramping, Example 1 shows the two-stage model can certify a commitment that fails in real-time operation. The practical message drawn in the paper is that the multistage model is useful precisely when ramping capability is a scarce resource, which is the situation of systems with high renewable penetration.
The result is proved in the paper. As far as is known it has not been machine-checked. This mission produces a formal model of robust UC (commitment logic, network-constrained dispatch, budget uncertainty, non-anticipative policies) together with a checked proof of the equivalence and of the counterexample. The model is a reusable base for later formal work on robust and multistage power-system models, such as the affine-policy results of the same paper.
The two separability steps are short on paper but must be carried out in the extended reals, where infeasible dispatch problems have value and sums of extended reals are not well behaved in general; the argument has to show that no arises. The main gap is the multistage side. The paper passes from the policy formulation (5) to the nested max-min formulation (6) by a remark, without proof. Formally, the value of an optimization over non-anticipative policies, which are functions on the whole uncertainty set, has to be identified with a backward max-min recursion over the per-hour sets, in both directions and without any attainment of the minima. A tempting shortcut, defining the multistage model as the nested formula, would prove nothing about policies and is excluded.
Fin T, 0-based: Lean period is the paper's . Generators, nodes, buses and lines are Fin Ng, Fin Nd, Fin Nb, Fin Nl.EReal; an infimum over an empty set is , the paper's convention for infeasibility.Contributions welcome: proofs of the milestones and the goal, and lemmas on infima and suprema of sums over product sets in EReal, which are reusable beyond this mission.
Incidence bounds count how often points can lie on lines, planes or other simple objects. Over the reals the model result is the Szemerédi–Trotter theorem for points and lines in the plane (Szemerédi–Trotter 1983). Its proofs use the order or topology of (cuttings, crossing numbers, polynomial partitioning), so they say nothing over finite fields or fields of positive characteristic. These are the settings that matter for the sum–product problem in and for the finite-field versions of Erdős-type distance problems, where the absence of an incidence theorem was long the bottleneck.
M. Rudnev, On the number of incidences between points and planes in three dimensions (Combinatorica 38 (2018), doi:10.1007/s00493-016-3329-6), proves a point–plane incidence bound in valid over every field of characteristic , with a constraint only in terms of the characteristic. It became the standard tool for sum–product estimates in positive characteristic: for example, Roche-Newton, Rudnev and Shkredov and Stevens and de Zeeuw build their bounds on it.
Timeline:
Let be a field and the projective three-space over . A point and a plane are both nonzero vectors of up to scaling. The point lies on the plane, , when . A line of is a 2-dimensional subspace of . For finite sets of points and of planes, the incidence count is
The collinearity parameter is the largest number of planes of that contain a common line.
The proof works in the space of lines of . The line through and has Plücker vector , . These vectors fill the Klein quadric . A point defines its α-plane (the lines through ) and a plane its β-plane (the lines in ), both projective planes inside . Cutting with a hyperplane that is not tangent to it gives a three-quadric , and every α- and β-plane meets in a line.
There are absolute constants such that for every field of characteristic , every set of points and every set of planes in , with when has positive characteristic ,
In characteristic there is no constraint on .
The proof decomposes as: point–plane incidences in equal line–line incidences between two families of mutually skew lines in (Lemma 9), and those are bounded by
where now counts lines of in a three-dimensional section of . The supporting milestones are: the incidence criterion (9) for Plücker vectors, the intersection pattern of α- and β-planes, Lemma 6 on sections of , the generic projection from to , the existence of a low-degree vanishing polynomial, the bound of zeros on a line, and Salmon's theorem (Theorem 2) on surfaces with many lines.
Theorem 3 gives the incidence bound with no assumption on the field beyond characteristic. The paper shows that its main term is sharp in positive characteristic under the constraint alone (Remark 4), and that the bound is tight for , (§6.2). It yields the paper's applications (distinct bilinear products of a planar point set over , and a pinned Erdős distance bound in positive characteristic), and it is the incidence input to sum–product estimates over such as .
The theorem is proved and published; it is not open. As far as is known, neither it nor its ingredients (the Klein correspondence in Plücker coordinates, the Guth–Katz polynomial argument over an arbitrary field, Salmon's theorem) has a machine-checked proof. This mission's statements give a formal target for the whole chain. Several milestones (the Plücker incidence criterion, the vanishing polynomial, zeros on a line, the generic projection) are standard facts of projective geometry over arbitrary fields that are useful well beyond this paper.
The obvious route, cell decomposition by polynomial partitioning as over , fails over a general field: there is no ordering, so no cells. The Guth–Katz algebraic argument survives, but in it needs the hypothesis that few lines are concurrent, which point–plane arrangements violate. Rudnev's way out is to move the problem into the three-quadric . There the two line families are skew within themselves, and the collinearity parameter becomes a count of lines in a three-dimensional section of .
The hard step is Theorem 12. It needs the polynomial method over an arbitrary field together with Salmon's theorem on flecnodal surfaces. That theorem holds in characteristic only for degree , which is the source of the constraint . It also needs a structure theory of ruled surfaces to rule out many incidences inside non-quadric ruled components. Salmon's theorem alone has no formal proof anywhere.
Points and planes of are elements of Mathlib's ℙ F (Fin 4 → F). Finite sets of them are Finsets of projective classes, so they contain distinct points and planes. Incidence is Projectivization.orthogonal. Lines of , and are 2-dimensional subspaces. Two lines meet when their intersection is a nonzero subspace, and they are skew when it is zero. Plücker vectors are indexed in the order . A hyperplane of is given by its covector , and "not tangent to " is . A three-subspace of is a 4-dimensional subspace of .
Committed conventions:
Type. Bounds are stated in , and Salmon's threshold is computed in .Trivializing formalizations are excluded:
Finsets that would count one point twice are not used;A complete development needs Plücker coordinates and the Klein correspondence over arbitrary fields, homogeneous polynomials on and their zero sets, irreducible factorization, Salmon's theorem, and the Guth–Katz induction. Lemma 8 of the paper (generators of ruled surfaces as curves in ) is not posed. Proofs of any milestone are welcome, as are proofs of the projective-geometry milestones as standalone Mathlib-style lemmas.
First-order methods such as the gradient method, Nesterov's accelerated method and the Heavy-ball method are usually analysed one at a time, each with its own hand-built potential function. Lessard, Recht and Packard (SIAM J. Optim. 26(1), 2016; read here in arXiv:1408.3595v7) observed that such a method is a linear dynamical system in feedback with the gradient map, and that tools from robust control, the integral quadratic constraints (IQCs) of Megretski and Rantzer (IEEE TAC 42(6), 1997), turn the question "does this method converge linearly, and at what rate?" into the feasibility of a small semidefinite program. The size of that program depends on the algorithm, not on the dimension of the optimization problem.
The paper's main result, Theorem 4, is the certificate behind this approach. It has been the starting point of a line of work on automated and computer-aided analysis of optimization algorithms, including the design of new methods with provably optimal rates.
An iterative algorithm is a linear system with state , driven by an input and producing an output :
The loop is closed by a map from sequences to sequences, . For the gradient method, , , and .
Instead of itself, one uses a constraint that is known to satisfy. A filter is a second linear system with state , inputs and output :
Given a reference point , the pair is the fixed point of the filter: and . Assume (all eigenvalues of have modulus less than one) and let be a symmetric matrix. The map satisfies the -hard IQC defined by if, for every input sequence , with and ,
It satisfies the pointwise IQC if each term is nonnegative.
Eliminating , the systems and combine into one linear system with state :
The condition number of a symmetric positive definite is , and is the Euclidean norm.
Let be a fixed point of and (, , and the filter equations above), let , and suppose satisfies the -hard IQC defined by . If there are and with
then every trajectory of the interconnection, , satisfies
The milestones follow the paper's proof: the elimination (3.6) of ; the one-step inequality (3.10) obtained from the LMI at a fixed point of (3.7); its weighted telescoped sum; the decay in the -weighted norm; and the passage to the Euclidean norm with the factor . Two companion statements are included: a pointwise IQC implies the -hard IQC for every (the remark after Theorem 4), and Proposition 2 (for ), the Lyapunov characterisation .
Theorem 4 reduces a statement about all functions in a class, for instance all strongly convex functions with Lipschitz gradients in every dimension, to a semidefinite feasibility problem with a handful of variables. The paper uses it to recover the known rates of the gradient method and to compute numerically certified rates for Nesterov's method, and the same template underlies later rate certificates for proximal, operator-splitting and distributed methods. The pointwise remark is what lets the sector IQC of gradients be plugged in directly.
The theorem is proved in the paper; nothing about it is open. To our knowledge neither the IQC framework nor Theorem 4 has a machine-checked proof. A formal development gives the first verified version of the certificate, and with it a route by which a numerically found LMI solution, once checked exactly, yields a verified convergence rate for a concrete algorithm.
The argument is short; the difficulty is in the bookkeeping. The IQC is a statement about every input sequence, while the conclusion concerns one trajectory of the closed loop, so the proof has to instantiate the IQC at the trajectory's own output and match the filter state it produces with the -component of the combined state. The weights must line up with the telescoping of the one-step inequality, and the final step needs the eigenvalue bounds together with the fact that removes the filter state from the initial error. Block matrices indexed by sums of index types make each of these steps heavier in Lean than on paper.
Vectors are Fin n → ℝ, matrices are Matrix (Fin a) (Fin b) ℝ, and sequences are ℕ → Fin n → ℝ indexed from . The norm is written out as , because Mathlib's norm on Fin n → ℝ is the sup norm, under which the constant would be wrong. The combined state lives on Fin nξ ⊕ Fin nζ and the LMI on (Fin nξ ⊕ Fin nζ) ⊕ Fin d, assembled with Matrix.fromBlocks, fromRows and fromCols; "" is positive semidefiniteness of the negated matrix. is the largest over the smallest eigenvalue of the Hermitian matrix , and is stated over the complex spectrum.
The page allows ; since the weights are undefined at , every statement that uses them assumes . Proposition 2 is printed without a sign condition and is false for ; it is stated for . The IQC hypothesis quantifies over every input sequence and every , with the filter started at ; replacing it by the IQC along the single closed-loop trajectory, starting the filter at , or reading as the sup norm would each change the theorem, and none is the formalization. The trajectory in the goal is universally quantified ("for any "); its existence is not assumed. The hypotheses and are kept as on the page although the proof does not use them. A sanity instance outside the proposal (the scalar gradient method with the sector IQC, , , ) checks in Lean that all hypotheses of the goal can hold at once.
The development needs only Mathlib's linear algebra: block matrices, PosDef/PosSemidef, the spectral theorem for Hermitian matrices, and finite sums. The Euclidean-norm lemma (decay in a -norm implies decay in the Euclidean norm with factor ) and Proposition 2 are reusable beyond this mission. Proofs of any milestone, and of Proposition 2 in either direction, are welcome.
For a finite graph, the Cheeger constant measures how hard it is to cut the vertex set into two pieces, and the spectral gap of the graph Laplacian measures how fast random walks mix. The two Cheeger inequalities (Dodziuk 1984; Alon and Milman 1985; Alon 1986) bound each quantity by a function of the other, and they underlie the theory of expander graphs, with uses in derandomization, error-correcting codes and the analysis of Markov chains.
High-dimensional expanders extend this theory from graphs to simplicial complexes. Linial and Meshulam (2006) and Gromov (2010) introduced combinatorial and topological notions of expansion for complexes; the spectral side is Eckmann's discrete Hodge theory (1944), in which each dimension carries its own Laplacian. Parzanchevski, Rosenthal and Tessler (arXiv:1207.0638, Combinatorica 2015) defined a -dimensional Cheeger constant through partitions of the vertices into blocks and proved the analogue of the upper Cheeger inequality, , for complexes with a complete skeleton. This mission formalizes that theorem.
Let and . A finite -complex with a complete skeleton on consists of all subsets of with at most elements together with a set of -element subsets, the -cells. A set of vertices is a -cell; is therefore the set of all -element subsets.
Each cell is oriented by the increasing order of its vertices, with . The space of -forms consists of the real functions on -cells, with inner product
The co-boundary and the boundaries , are
where means that and is a cell, and equals times the increasingly oriented cell when has smaller vertices in . The upper Laplacian is on , and is the space of -cycles.
The spectral gap is the least eigenvalue of on the cycles (Definition 2.1):
For sets , let be the set of -cells with exactly one vertex in each . The Cheeger constant is (Definition 1.1)
the minimum over partitions of into nonempty sets . For , is the space of functions summing to zero, is the graph Laplacian, and is the usual Cheeger constant .
for every finite -complex with a complete skeleton on vertices.
Milestones 2 and 5–7 hold for every partition, not only a minimizing one.
The result. Theorem 1.2 shows that a large spectral gap forces every partition of the vertices into blocks to be crossed by many -cells, so spectral information certifies combinatorial expansion of a complex. The paper uses it with the spectral analysis of Gundert and Wagner to show that Linial–Meshulam random complexes have Cheeger constant of order for large (Corollary 1.3). The paper also shows that the converse direction fails: a triangulation of the Möbius strip has but , so no lower bound of the form holds.
Formalizing it. The theorem is proved in the paper; to our knowledge no machine-checked proof exists. A formal proof requires a signed simplicial chain complex with explicit orientations, the adjoint relation between boundary and co-boundary, and a Rayleigh-quotient bound for a symmetric operator on an invariant subspace. These are the basic tools for any further formal work on spectral high-dimensional expansion, including the Mixing Lemma of the same paper (the companion mission of this series).
The graph proof plugs a two-valued test function into the Rayleigh quotient. In dimension the test vector must be a -cycle, and an indicator of a block is not one. The paper's form (4.1) assigns to a -cell whose vertices meet distinct blocks the size of the missing block, with the sign of a permutation of the blocks. Showing that this form is a cycle and that its co-boundary has absolute value exactly on and elsewhere is a case analysis over how the vertices of a cell fall into blocks, and every case depends on the orientation signs. A convention error in any of the operators or in the form makes one of these identities fail. A second, smaller difficulty is that is a minimum over the spectrum on a subspace, so the Rayleigh bound must be proved for restricted to , which it preserves.
Fin n; a complex is a structure holding its -cells as Finset (Finset (Fin n)), each of size ; the complete skeleton is built into the type. Complexes without -cells are allowed.EuclideanSpace ℝ over the subtype of -element vertex sets, so no form is supported on sets of the wrong size. is modelled on all -element sets; vanishes off and ignores values there.Fin n; the sign of vertex in cell is . Boundary and co-boundary are both defined by their formulas; their adjointness is milestone 3.sInf. The goal states that some eigenvalue of on (a nonzero cycle with ) is at most the Cheeger ratio of every partition, which is equivalent to . A partition is a family A : Fin (d+1) → Finset (Fin n) of nonempty, pairwise disjoint sets covering the vertices.sInf (empty sets give ), unsigned boundaries (for which ), cocycles in place of cycles (on which is zero), and arbitrary disjoint families in place of partitions (empty blocks give ratio ).LinearMap.IsSymmetric), and counting cells by blocks of a partition. The chain-complex and adjointness lemmas are reusable in any formal development of simplicial Hodge theory; contributions there are welcome.Nonlinear filtering asks for the conditional law of an unobserved Markov process given noisy partial observations of it. It is the computational core of data assimilation in weather forecasting, oceanography and geophysics, of target tracking, and of inference in large networked systems. The standard numerical method, the particle filter, replaces the conditional law by a cloud of weighted samples. Its error is well understood in fixed dimension, but in practice it degrades exponentially in the dimension of the state: the number of particles needed for a fixed accuracy grows exponentially with the number of variables. This phenomenon, the curse of dimensionality of particle filters, has been documented empirically and analysed by Bickel, Li and Bengtsson and by Snyder et al. (Bickel–Li–Bengtsson 2008; Snyder et al. 2008), and it is a main obstacle to their use in high-dimensional data assimilation.
Rebeschini and van Handel (arXiv:1301.6585v2, Ann. Appl. Probab. 25(5), 2015) gave the first rigorous proof that a local variant of the particle filter, the block particle filter, has an approximation error that does not depend on the model dimension, for models with local interactions above a mixing threshold. The result is the standard theoretical reference for localization in sequential Monte Carlo.
Let be a finite graph with graph distance , and fix a neighbourhood size . The -neighbourhood of a vertex is , and the -inner boundary of is . Each vertex carries a Polish state space with a reference measure , and an observation space ; write and .
The hidden process is a Markov chain on with transition density with respect to , where each depends on only through (locality). The observation has density given . For a fixed observation sequence, the filter is the recursion
where applies the transition kernel and reweights by and renormalizes (the Bayes formula).
A partition of into blocks defines the blocking operator , which replaces a measure by the product of its block marginals. The block particle filter with particles is
where replaces a measure by the empirical measure of i.i.d. samples from it. The local quantities are , , and . The error is measured locally:
where is the class of measurable functions depending only on the coordinates in .
There is depending only on such that, if , , and , then for all , , , ,
with depending only on . The goal states the constants existentially, as the paper does, so that it survives any improvement of them.
The proof splits the error through the block filter :
Theorems 4.14 and 4.23 together give Theorem 2.1 by the triangle inequality.
The theorem shows that the error of a local particle filter can be controlled by quantities that are local in the graph: neither the assumptions nor the bound depend on the time horizon or on . On a square lattice, choosing blocks of side length of order balances the two terms and gives a local error, at most locations, that tends to zero as uniformly in time and in the lattice size (the paper's Corollary 2.5, which is not part of this mission): the number of particles needed for a given local accuracy does not grow with the dimension. The result identifies decay of correlations of the filter, established through the Dobrushin comparison theorem, as the mechanism that makes localization work, and it underlies later work on local particle filters and their spatial bias.
The result is proved on paper. No part of it is formalized, and the formal library has no nonlinear filter, no particle filter and no Dobrushin comparison theorem. The mission produces machine-checked statements of the main theorem and of the intermediate results of its proof, with explicit constants for the two halves; proofs of any milestone, or of the goal from Theorems 4.14 and 4.23, are the remaining work.
The obvious argument fails in two places. First, the standard particle filter error bound is uniform in time only through filter stability, and its constants are exponential in the dimension, because the reweighting step compares likelihoods over all of at once. Localizing the sampling (blocking) removes this, but introduces a bias at block boundaries that must not accumulate over time. Controlling that bias requires showing that the filter has decay of correlations uniformly in time, which is a statement about conditional distributions of a high-dimensional measure, not about its marginals. Second, the sampling error must be propagated through the block filter dynamics in a norm strong enough to compose: the weak norm does not contract under the block filter, which is why the paper measures one-step errors in total variation after one further step of dynamics.
The Lean development is in the namespace LocalPF.Block. Committed conventions:
Added or changed hypotheses, each disclosed in the item: strict positivity and integrability of in Theorem 4.14 and Proposition 4.17 (the paper assumes no bounds on there; without them the Bayes formula is undefined); explicit bounds in Lemma 4.2, whose clause is stated for Giry-measurable random probability measures; in Theorem 4.23, excluding only the case where the paper's bound is ; Lemma 4.19 and Proposition 4.22 are stated for every deterministic probability measure in place of the random previous estimate, which is stronger.
The statement admits no trivializing reading: the constants of Theorem 2.1 are quantified before the graph and the model, so they cannot depend on ; the goal and Theorem 4.23 assert that the particle-array law is a probability measure, so a zero law cannot make the expectation vanish; test functions are measurable and bounded, so the integrals are not junk values; excludes division by ; and the correction step's normalizer is positive and finite under the stated hypotheses.
Needed infrastructure: product measures over finite index sets and their marginals, the Giry monad and measurability of the maps it composes, conditional distributions on products of Polish spaces, and matrix Neumann series. The Dobrushin comparison theorem and the V-statistic bound (Lemma 4.20) are reusable beyond filtering. Proofs of any milestone are welcome, and so are formal statements of the remaining results of §4 (Propositions 4.4, 4.8, 4.9, Corollary 4.13).
Many problems in machine learning and statistics minimize an average of convex losses, one per data point or per block of data. Incremental methods such as SAG, SVRG, SAGA, SDCA, Finito and Katyusha exploit this finite-sum structure: each step touches one component instead of the whole average, and for smooth components the best of them reach accuracy with far fewer component evaluations than full-gradient methods. A natural question is how much of this improvement is possible at all, and whether access to stronger per-component information, such as a proximal step, could do better still.
B. Woodworth and N. Srebro, Tight Complexity Bounds for Optimizing Composite Objectives (NeurIPS 2016, arXiv:1605.08003), answer this with lower bounds on the number of component-oracle calls. Their oracle returns, for a requested component, its value, its gradient, and its exact proximal point. Earlier lower bounds covered only gradient access to smooth, strongly convex sums: Agarwal and Bottou (arXiv:1410.0723) for deterministic algorithms, and Lan (arXiv:1507.02000) for randomized algorithms that sample components from a fixed distribution and keep their iterates in the span of the gradients received (p. 2–3 of the paper). Woodworth and Srebro allow any algorithm, any sequence of gradient and prox queries, and iterates anywhere in , in all four combinations of Lipschitz or smooth components and bounded or strongly convex objectives. This mission formalizes the deterministic bound for smooth, not strongly convex components on a bounded domain (Theorem 3 of the paper).
Fix integers and , and write with the Euclidean inner product and norm . The domain is the ball . Given functions , the objective is
A component is -smooth on if it is differentiable and its gradient is -Lipschitz on : for . Each is also required to be convex on .
A query is a triple of a component index, a point and a parameter . The oracle answers it exactly with
A deterministic algorithm chooses its first query, and then each next query as a function of the ordered list of answers received so far. Running against an oracle produces a sequence of query points .
There are absolute constants such that for every and there is a dimension with the following property. For every deterministic algorithm there are convex, -smooth components on the -ball, an exact oracle for them, and a minimizer of over the ball, such that
In words: oracle calls are needed before any queried point is strictly -suboptimal. The constants are left unspecified, as in the paper's and .
The proof (Appendix B.3) builds the components adaptively from orthonormal directions and indicators . The milestones are the claims it states on the way:
The result. Running accelerated gradient descent on , with all component gradients computed at each step, finds an -suboptimal point with oracle calls (§2 and Table 1 of the paper). Theorem 3 shows that this is optimal among deterministic algorithms, up to a constant factor: neither incremental access to single components nor an exact prox oracle improves the order of the deterministic complexity. Randomized algorithms need only between and calls (Table 1, with the suboptimality of the point ), so Theorem 3 also measures the benefit of randomization in incremental methods such as accelerated SVRG: a factor of order in the dominant term.
Formalizing it. The theorem is proved in the paper; it has no machine-checked proof. A formal proof needs the adaptive adversary argument in full: the construction of directions orthogonal to all earlier queries, the consistency of answers given by partial functions, and the explicit linear-algebra of the tridiagonal quadratic. The paper's final count is false for some parameters (for even and ), and the large- construction needs a dimension of order that the stated bound does not allow when ; a complete formal proof settles both points.
The algorithm is arbitrary and adaptive, and it sees exact prox points, which in principle reveal far more about a component than a gradient. The construction must therefore be chosen after the algorithm, round by round, so that every answer the algorithm has received is consistent with the final functions, yet reveals at most one new direction per round. The naive argument, "the algorithm only explores the span of previous gradients", is not available: the algorithm is not restricted to linear spans, and its queries can lie anywhere. Instead, each new direction must be made orthogonal to every point queried so far, and one must show that the partial function used to answer a query has the same gradient and the same constrained prox as the final function at that point (Lemmas 4–5). The constrained prox over the ball is not covered by the paper's unconstrained computation and needs its own argument.
The space is EuclideanSpace ℝ (Fin d). Components are indexed by Fin m (0-based). A query is a structure carrying a component, a point and a parameter with a proof of ; the prox answer is described by the published minimizer predicate BoydADMM.Prox.IsProx, not by a choice function. A deterministic algorithm is a function from the list of earlier answers to the next query, and the oracle is a fixed function of the query, required to be exact on every query. The minimum is an explicit attained minimizer over the ball, never a real infimum.
Committed conventions, each disclosed in the item statements:
A trivializing formalization is ruled out: the goal mentions none of , , rounds, , or , so it cannot be discharged by assumptions about the construction, and the oracle must answer every query exactly.
A full development needs: the adversary construction (orthonormal vectors orthogonal to a finite set of earlier queries), smoothness of the quadratic hard functions (a Hessian bound ), existence of constrained prox points, and the arithmetic of the counts. The tridiagonal linear algebra of milestones 2–3 is reusable for other lower-bound constructions in the style of Nesterov's. Proofs of individual milestones, alternative constructions and a corrected explicit constant are all welcome.
In Wasserstein distributionally robust optimization (DRO) a decision is evaluated against the worst distribution within an optimal-transport ball around a nominal distribution . Every tractable reformulation rests on a strong duality theorem that replaces the supremum over distributions by a one-dimensional minimization over a multiplier and an expectation of a pointwise supremum. Zhang, Yang and Gao (arXiv:2205.00362v4) show (Theorem 1 of their paper) that this duality holds for every radius exactly when a single measure-theoretic property, the interchangeability principle (IP), holds for the functions . Earlier duality proofs (Blanchet and Murthy 2019, Gao and Kleywegt 2023) assumed a Polish space and semicontinuity of the loss and the cost; the interchangeability formulation removes those assumptions and isolates what is actually needed.
This mission formalizes the paper's §3 answer to the next question: when does (IP) hold? Proposition 1 characterizes it, for an entire class of functions, by two properties of the probability space alone: measurable projection and a weak measurable selection. Interchange of expectation and supremum is classical in stochastic programming (Shapiro, Dentcheva and Ruszczyński 2021, §9.3.4; Shapiro 2017) and measurable selection is classical in stochastic control (Bertsekas and Shreve 1978); Proposition 1 shows that, for the functions arising in Wasserstein DRO, the two are equivalent.
Let be a probability space, with no topology on . Write for the completion of under ; a function or set is -measurable if it is measurable for . Expectations take values in and are .
Let be the set of probability measures on whose first marginal is . For put .
Interchangeability principle (IP). An -measurable satisfies (IP) if is -measurable and
Diagonal dominance (Definition 1). A measurable is diagonally dominant if for all . A measurable set is diagonally dominant if implies . A set-valued map with measurable graph is diagonally dominant if implies . The functions with and a cost vanishing on the diagonal are exactly the diagonally dominant functions (Lemma 4).
(Proj) For every diagonally dominant , .
(Sel*) For every diagonally dominant with measurable graph there is with .
Combined with Theorem 1 of the paper, Proposition 1 and Lemma 4 reduce strong duality for Wasserstein DRO, for every measurable loss and every measurable cost vanishing on the diagonal, to two measurability properties of the nominal space. These properties hold, for instance, when is finitely supported, or when is a Polish or Suslin space with its Borel σ-algebra (Examples 1–3 of the paper, citing Aubin and Frankowska, Set-Valued Analysis, Thm 8.3.2 and Aliprantis and Border, Infinite Dimensional Analysis, Thm 18.26), which is how the paper covers the earlier duality results. The selection condition (Sel*) is weaker than the deterministic measurable selection used with the interchange formula of Rockafellar and Wets, Variational Analysis, Thm 14.60, and the necessity direction shows that nothing weaker than (Proj) and (Sel*) suffices for the whole class.
The result is published with a complete proof in the paper's e-companion. The work here is to formalize it: no machine-checked version of (Proj), (Sel*) or of this equivalence exists, in Mathlib or on the platform. The development yields a reusable interface between extended-real expectations, completions of probability spaces, and couplings with a fixed marginal.
The necessity direction is short: it tests (IP) on an indicator and on . The sufficiency direction is where the content lies. The inequality is immediate, but the reverse inequality requires building a single coupling that nearly attains simultaneously for -almost every , from a selection condition that only delivers couplings concentrated on graphs. The obvious idea, choosing a near-maximizer pointwise, fails because no measurable choice is available on an abstract measurable space; this is precisely why (Sel*) is stated for couplings rather than maps. The case , the null set where , and the passage between -measurable and -measurable sets all have to be handled.
MeasurableSpace; is Mathlib's product σ-algebra; is a Measure with IsProbabilityMeasure.EReal-valued with the side condition "never ".ModelRiskOT.Duality.extIntegral, with lower Lebesgue integrals. It agrees with the paper whenever one part is finite and assigns to the case , where the paper's expectation is undefined. The Bochner integral is never used.NullMeasurable / NullMeasurableSet (completion), never Measurable; the latter would turn (Proj) into a strictly stronger condition that fails on Polish spaces.map Prod.fst γ = P̂; without the probability requirement (Sel*) would hold trivially with .EReal product has ).A complete development needs: the transfer of lower Lebesgue integrals along the first marginal for null-measurable integrands, a characterization of null-measurability of EReal-valued functions through superlevel sets, and a countable gluing of couplings over a partition. These are reusable well beyond this mission, as is the (IP) interface, which the companion missions of this series also use. Contributions to any milestone, and to these general lemmas, are welcome.
Tensor decompositions express a multiway array as a sum of simple terms. The canonical polyadic decomposition (CPD) writes an -th order tensor as a sum of outer products of vectors; block term decompositions replace each rank-one term by a term of higher multilinear rank. These models are used in signal processing, blind source separation and telecommunications, and are computed numerically by minimizing a least-squares misfit.
Sorber, Van Barel and De Lathauwer (SIAM J. Optim. 23(2), 2013) introduce the (rank- rank-1) block term decomposition (BTD), which contains both the CPD and the rank- BTD as special cases, and develop optimization algorithms for it: nonlinear conjugate gradient and quasi-Newton methods built on the complex gradient, and Gauss–Newton and Levenberg–Marquardt methods built on the Jacobian. For the second family the central object is the Gramian of the Jacobian of the residual. Theorem 4.5 of the paper gives its exact block structure, and that structure is what lets the methods run without ever forming .
Fix modes with dimensions , a number of terms , and block sizes ; put . The BTD approximates by
where the inner sum runs over the columns of block . Here and .
The paper reads this as a structured CPD in rank-one terms. The first factor matrices are the , and the last are
where copies column of into the columns of block . The residual tensor is
and the unknowns are . The Jacobian is the complex (holomorphic) derivative: is a polynomial in , not in .
Three auxiliary matrices enter the answer. The first is , the Hadamard product of the Gramians of the factor matrices outside a mode set , with entries . The second is , which satisfies (Proposition 4.1). The third is the block diagonal .
For every tensor and every ,
The goal has two parts, and both are required. The first is that the Gramian of the CPD Jacobian equals the explicit block matrix. The second is the factorization through .
With Theorem 4.5, is determined by the factor matrices and the small Gramians . For a hypercubical CPD this takes extra memory instead of the of a dense Gramian. Theorem 4.6 of the paper then turns the same structure into a matrix–vector product in operations, which is what inexact Gauss–Newton and Levenberg–Marquardt steps solved by preconditioned conjugate gradients require. The block-diagonal part also gives the block Jacobi preconditioner of the paper's §4.2. For the CPD, expressions for the Gramian were already studied in chemometrics (the paper cites G. Tomasi's 2006 thesis for this); Theorem 4.5 states the block structure in closed form and extends it to the structured BTD through .
The result is proved in the paper. As far as a search of Prove2Me and Mathlib shows, nothing about CPD or BTD Jacobians has been formalized. This mission produces a machine-checked proof of the block structure, starting from an explicit model of the decomposition and an honest complex derivative. That model (outer products, the structured CPD, , , the Hadamard-Gramian products) can be reused for the paper's cogradient theorem and for other tensor algorithms.
The identity is finite-dimensional, but no single step reduces it to a known lemma. First, is a genuine derivative of a multilinear polynomial map in complex variables, so each entry has to be computed from the derivative of a sum of products. Second, is a sum over all multi-indices. Turning it into the product of Gramians in means exchanging a sum of products with a product of sums while one or two modes are held fixed, with the conjugates landing on crossed column indices (, ). Third, the structured factor matrices are not unknowns. The derivative with respect to has to go through the chain rule and the vec–Kronecker identity, and 's rows and columns are indexed by different sets.
All objects are defined in TensorBTD.Gramian.Setting, with the following conventions.
Fin P ⊕ Fin Q (mode is Sum.inl (p-1) and mode is Sum.inr (q-1)), so all indices are 0-based. The columns are Σ r : Fin R, Fin (L r) in lexicographic order, which is the order of (3.5).Matrix.vec. This is the paper's Definition 2.5 with its misprint corrected to . Kronecker products are Mathlib's ⊗ₖ.deriv of at . It is not defined by its closed form, and it is not a real derivative.There are no hypotheses. The paper's assumptions that and its qualifiers "nonzero" and "rank-" are not used in Section 4, so they are dropped. This is a generalization: gives the plain CPD in terms.
A goal that took the closed form of as the definition, or that defined entrywise by the outer-product formula of milestone 1, would only state a sum identity. Both are ruled out: is a derivative, and the goal asserts that the Gramian of the CPD Jacobian equals the closed form. A misprint in the proof's closing paragraph, for the block, is corrected in Lean to .
Useful Mathlib infrastructure includes Matrix.vec, Matrix.kroneckerMap, Matrix.blockDiagonal', Finset.prod_univ_sum and the derivative rules for finite products (HasDerivAt.finset_prod). General lemmas welcome as contributions: derivatives of multilinear maps along coordinate directions, the sum–product exchange over Fintype.piFinset, and the chain rule for a Jacobian composed with a linear map.
Distance covariance was introduced by Székely, Rizzo and Bakirov (2007) as a measure of dependence between random vectors in Euclidean spaces: it is zero exactly when the vectors are independent, and its empirical version gives a consistent test of independence that needs no moment beyond the first. Lyons (2013) asked for which metric spaces the same holds. His Theorem 3.11 shows that it holds whenever both spaces have strong negative type. This mission formalizes the complementary result, Proposition 3.15 of the same paper: the hypothesis on the space cannot be removed. Without negative type, distance covariance can even be negative; without strong negative type, it can vanish on a law that is not a product. Together with Theorem 3.11, the proposition locates the boundary of metric spaces on which distance covariance is a valid test of independence.
Timeline. 2007: Székely, Rizzo and Bakirov define distance covariance on and prove the independence characterization there. 2013: Lyons extends the theory to metric spaces of negative type, characterizes the spaces where it remains a test of independence as those of strong negative type, and proves Proposition 3.15. 2018 and 2021: two errata by the author correct several statements of the paper; the first of them adds the standing assumption that all metric spaces are separable. Proposition 3.15 is not affected by the corrections.
Let and be separable metric spaces, each with its Borel -field. A finite Borel measure on has a finite first moment if for some point . For such put
and define the doubly centred distance . For two probability measures with finite first moments, is the energy of their difference,
Let be a Borel probability measure on whose marginals on and on have finite first moments. Its distance covariance is
is a product measure if .
has negative type if for every , all points and all reals with ,
On such a space for all probability measures with finite first moments, and has strong negative type if moreover equality holds only when . Write for the point mass at .
Let have at least two points.
The space is arbitrary apart from having two points, so the statement fixes nothing about it.
The result. Theorem 3.11 of the paper shows that strong negative type of both spaces suffices for to characterize independence. Proposition 3.15 shows the hypothesis on each factor is necessary: a single failure of (3.1) already produces a law with negative distance covariance, so is not even a nonnegative quantity there, and a single pair of distinct laws with produces a dependent law that the test cannot detect. Consequently, any use of distance covariance on general metric data (graphs, spaces with , spaces of distributions under Wasserstein metrics) has to verify strong negative type first. Since the two-point space is arbitrary, the failure is a property of alone.
Formalizing it. The proposition is proved in the paper; no machine-checked proof of it, or of any result about distance covariance, is known to exist. The mission produces a formal definition of distance covariance on separable metric spaces, of negative and strong negative type in the paper's measure-theoretic form, and the computation of on two-point mixtures. These are the same objects as in the sibling mission on Theorem 3.11, so the two together give a formal account of when distance covariance characterizes independence.
The step the paper calls "a little algebra" is the bulk of the work: is a four-fold integral of a product of doubly centred distances, each of which is itself built from integrals against a marginal of , and every manipulation of it happens inside Bochner integrals over product measures whose integrability has to be derived from first moments alone. In a formal setting nothing about these integrals is automatic. The passage from a violation of the finite-sum condition (3.1) to two probability measures with is left implicit in the paper. The non-product claim also uses a fact the page does not state: that , which follows from and is false without it.
All metric spaces carry their Borel -field and are assumed second countable, which for metric spaces is separability; this is the author's own correction, Errata (i), which makes measurable on the product. Measures are Mathlib measures with values in ; mixture weights such as , and enter as extended nonnegative reals, and is always restricted to . Because Mathlib's Bochner integral does not integrate against signed measures, is defined as the bilinear energy expansion displayed above. "Not a product measure" means differs from the product of its own marginals, never from some other product.
Several formalizations of this statement would be trivially true and are excluded. A Bochner integral of a non-integrable function is in Lean, so every statement either assumes or concludes the finite first moments that make and genuine integrals. Negative type is the finite-sum condition (3.1) and strong negative type the measure condition of p. 11, never an embedding property. The product condition is tested against 's own marginals, not against free factors. is quantified before is chosen, and part 2's hypothesis is the full negation of strong negative type, which includes spaces of negative type.
A complete development needs integrability of under from first moments (Lemma 2.1 of the paper), linearity of the energy in each measure, push-forwards of mixtures of product measures, and the intermediate value theorem. The integrability and energy-bilinearity lemmas are reusable for any work on energy distance or distance covariance. Contributions of these general lemmas, as well as of proofs of the individual milestones, are welcome.
Polynomial optimization asks for the minimum of a polynomial over a set cut out by polynomial inequalities. Lasserre's moment relaxation (Lasserre 2001) replaces the minimization over points by a minimization over probability measures on , and then over linear functionals on polynomials that satisfy semidefinite constraints. The bridge between measures and semidefinite constraints is Putinar's theorem (Putinar 1993): on a compact basic semialgebraic set with an Archimedean description, a linear functional comes from a measure exactly when it is nonnegative on the quadratic module of the constraints.
Many problems of practical size are invariant under a group of linear transformations: permutations of variables, sign changes, rotations of a polygon. Gatermann and Parrilo (2004) showed how such symmetry block-diagonalizes sums-of-squares programs. Riener, Theobald, Jansson Andrén and Lasserre (arXiv:1103.0486, Math. Oper. Res. 2013) carry the reduction to the moment side. Their first step, Theorem 3.2, is a symmetric version of Putinar's theorem: for invariant data it suffices to consider functionals that are themselves invariant, and these are characterized by positivity of symmetrized localizing forms. This mission formalizes that theorem.
Write . Let be a finite subgroup of . A matrix acts on points by and on polynomials by
the linear substitution . A polynomial is -invariant if for every .
Fix and the feasible set
Assumption 2.1 requires to be compact and some polynomial , with sums of squares , to have a compact superlevel set . Put .
A linear map is -linear if for all and all . Its symmetrized localizing forms are
For a Borel measure on , is its image under , and is -invariant if for all . A measure on is one with .
If the are -invariant and Assumption 2.1 holds, then for a -linear :
The result. Theorem 3.2 turns the moment relaxation of a -invariant problem into one over -linear functionals. Such a functional is determined by its values on the invariant ring , so its moment variables are indexed by a basis of invariants instead of all monomials (Example 3.3 of the paper: five variables instead of fifteen for on in degree 2). The block-diagonalized relaxations and the convergence result of §3 (Theorems 3.4–3.7) rest on it.
Formalizing it. The theorem is proved in the paper, modulo Putinar's theorem, which is cited. Neither Putinar's theorem nor any Archimedean Positivstellensatz is in Mathlib or on the platform. A complete formalization therefore needs (i) Putinar's theorem itself, in its dual moment form, and (ii) the determinacy of compactly supported finite measures by polynomial moments in several variables. Both are reusable well beyond this paper: every moment-SOS hierarchy result in the literature cites them.
The group-theoretic steps (milestones 2–4) are finite averaging and change of variables. The weight of the theorem sits in two analytic facts. The first is Putinar's theorem: nonnegativity on the quadratic module is an algebraic condition, and producing a measure from it requires the Archimedean hypothesis of Assumption 2.1 in an essential way; without that hypothesis the statement is false in general. The second is that the measure Putinar's theorem returns has to be shown -invariant. Equality of the polynomial moments of and does not by itself identify two measures; it does so here because both are finite and carried by a compact set, where polynomials are dense in the continuous functions. A further detail: Putinar's theorem is stated for normalized functionals, and Theorem 3.2 is not normalized, so the degenerate case must be shown to force .
Polynomials are MvPolynomial (Fin n) ℝ, points Fin n → ℝ, and a Subgroup (GL (Fin n) ℝ) with a Fintype instance. The action on polynomials is the linear substitution aeval, so is an arbitrary finite matrix group, not only a permutation group. Sums of squares are Mathlib's IsSumSq. "psd" for the symmetric form means for every polynomial , with no degree truncation; () is included. Measures live on the Borel σ-algebra of , is Measure.map along the continuous (hence measurable) map , and "measure on " is .
Committed conventions and disclosed readings:
Trivializing formalizations are ruled out: integrals are taken only against finite measures carried by a compact set, so no statement holds because a Bochner integral of a non-integrable function is ; positivity is through the forms on all of , not replaced by pointwise nonnegativity; and the invariance of is a conclusion of milestone 5, never a hypothesis.
Contributions welcome: Putinar's theorem (milestone 1) and multivariate moment determinacy on compact sets are the reusable infrastructure; the averaging milestones are a natural first entry point.
Distance covariance is a statistic for testing whether two random variables are independent. Székely, Rizzo and Bakirov introduced it for Euclidean spaces (Ann. Statist. 2007): the population distance covariance of a joint law is exactly when is a product measure, so a consistent test of independence follows. Lyons (arXiv:1106.5758) extended the statistic to arbitrary metric spaces and showed that the characterization of independence holds on a pair of metric spaces precisely when both have strong negative type (his Theorem 3.11 and Proposition 3.15). That makes strong negative type the property a statistician has to check before using distance covariance on a given space. Functional data, the main case in practice, live in Hilbert spaces.
This mission formalizes Lyons's Theorem 3.16: every separable Hilbert space is of strong negative type. Kosorok (2009, cited by Lyons) had asked whether the characterization of independence extends to Hilbert spaces.
Timeline.
Let be a separable metric space with its Borel -field. A Borel probability measure has a finite first moment if for some . For two such measures write and
the integral of against the square of the signed measure .
The space has negative type if, for all , all and all real with ,
By approximation, negative type gives for all probability measures with finite first moments. The space has strong negative type if it has negative type and only when . Strict negative type is the same condition restricted to finitely supported measures.
The proof works on and uses the following objects. is the law on of an IID standard normal sequence ; is Lebesgue measure on ; . For put . The Gaussian Crofton embedding sends to the function
on . For probability measures on , its barycenter at is the function .
The goal has no constants. Each milestone states a claim of the paper in the paper's strength.
The result. With Theorem 3.11, Theorem 3.16 shows that for random elements of separable Hilbert spaces, zero distance covariance is equivalent to independence. Distance-covariance tests are therefore consistent for curves, images and other functional data. It also yields Corollary 3.18: if is a separable metric space of negative type, then has strong negative type, so a test of independence is available on every separable space of negative type after a change of metric. Remark 3.17 shows that separability cannot simply be dropped: a non-separable Hilbert space is of strong negative type exactly when its dimension is a cardinal of measure zero.
The formalization. The theorem is proved, and to our knowledge no proof of it, or of negative type of Hilbert spaces, is machine-checked. A complete development needs four things:
Measure.infinitePi and gaussianReal;Each of these is reusable outside distance covariance: the first in Gaussian measure theory, the last whenever laws on sequence spaces are compared.
The first idea is to approximate. Euclidean spaces have strict negative type, finite-dimensional projections of a Hilbert space are Euclidean, and probability measures are limits of finitely supported ones. Approximation preserves the inequality , but it does not preserve the equality case. A limit of strictly negative quantities may be even though . Remark 3.3 of the paper exhibits a space of strict but not strong negative type, so this gap is real.
The second idea is to transport the finite-dimensional Crofton embedding, in which is the measure of half-spaces separating and . It fails because has no rotation-invariant Lebesgue measure on its half-spaces. The Gaussian measure replaces it. But is defined only -almost surely, and its exceptional set depends on . As a result, " almost everywhere" does not immediately give information for every direction and level . That passage from almost every to every is the step the 2018 Errata had to justify.
Lean conventions, all disclosed in the items:
InnerProductSpace ℝ H with CompleteSpace H, as Errata (viii) prescribes; a complex space has the distances of its realification. Separability is SecondCountableTopology, which matches the standing separability of Errata (i). is lp (fun _ : ℕ => ℝ) 2 with the Borel -field, declared in the Setting file because Mathlib supplies none.Trivializing encodings are ruled out:
Contributions are welcome on any milestone. The reduction of a general separable to (by an isometry onto a closed subspace) is not posed separately and belongs to the goal's proof. Mathlib's Measure.ext_of_charFun, for finite measures on complete second-countable real inner product spaces, is a natural tool for milestone 5. Separability of lp is not yet an instance in Mathlib.