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?
Balanced truncation is the standard method for reducing the state dimension of a linear control system while keeping its input–output behaviour: states that are both hard to reach and hard to observe are discarded. Its justification rests on two Gramians, the solutions and of a pair of Lyapunov equations, whose quadratic forms measure how much input energy a state costs to reach and how much output energy it produces. For linear systems the facts are classical: the image of the controllability Gramian is the reachable subspace, and the kernel of the observability Gramian is the unobservable subspace.
Bilinear systems, in which the input multiplies the state, are the simplest nonlinear extension of linear control systems. Their generalized Lyapunov equations have the same form as the Lyapunov equations of linear stochastic systems with multiplicative noise, which is why Benner and Damm treat the two classes together. Balanced truncation was extended to them using the solutions of generalized Lyapunov equations (Al-Baiyat and Bettayeb, 1993; Gray and Mesko, 1998, both as cited by Benner and Damm). Benner and Damm, in Lyapunov Equations, Energy Functionals, and Model Order Reduction of Bilinear and Stochastic Systems (SIAM J. Control Optim. 49(2), 2011, doi:10.1137/09075041X), examine which of the linear-system energy interpretations survive for bilinear systems. Their Theorem 3.1 is the structural result that does survive: the kernels of the Gramians still identify states that are unreachable from the origin and states that produce no output, so these states can be eliminated without changing the transfer behaviour.
Fix and real matrices , , . The bilinear control system (3.1)–(3.2) is
with state , input and output . The homogeneous system (3.5) drops the term : , . The same indexes the bilinear terms and the columns of . Write for a solution with input and initial state , and .
An admissible input is a function that is integrable on every interval . A solution with is a continuous satisfying
The generalized Lyapunov equations (3.6) are
A solution of the first is a controllability Gramian and a solution of the second an observability Gramian. "" means is symmetric nonnegative definite; and are its image and kernel.
(a) If solves the first equation of (3.6), then for every admissible input
(b) If solves the second equation of (3.6) and , then for the homogeneous system (3.5) and every admissible input
The result. Part (a) says that a state outside cannot be reached from the origin by any input, so its controllability energy is infinite; part (b) says that a state in is indistinguishable from the origin at the output, so its observability energy is zero. Together they justify the first step of balanced truncation for bilinear systems (Remark 3.2 of the paper): the system can be restricted to and projected along without changing its input–output map, after which the Gramians are nonsingular and can be balanced. The theorem needs neither stability of nor uniqueness of the Gramians, so it applies to every nonnegative definite solution of (3.6). The rest of §3 of the paper shows that the finer, quantitative energy estimates of the linear case fail for bilinear systems; this qualitative statement is what remains exact.
Formalizing it. The theorem is proved in the paper; no machine-checked version is known. A formal proof yields a reusable invariance principle: a subspace that is invariant under every vector field is invariant under the flow of the input-driven system, for merely integrable inputs. It also yields the linear-algebra lemmas relating kernels of nonnegative definite solutions of generalized Lyapunov equations to the system matrices, which are used throughout model reduction and stochastic stability theory.
The algebraic part (milestones 1, 2, 4) rests on the fact that for a nonnegative definite matrix , forces , applied to the terms of the Lyapunov equation tested against a kernel vector. The passage from the vector field to trajectories is where care is needed. The paper's sentence " whenever , so is invariant" is not by itself an argument: tangency of a vector field to a subspace implies invariance only together with a uniqueness or Gronwall-type estimate, and here the field depends on time through an input that is only integrable, so is merely absolutely continuous and exists only almost everywhere. A pointwise "the derivative points into the subspace" argument therefore does not apply as stated, and the step needs an estimate on the component of orthogonal to the subspace.
The Lean development uses states Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, the matrix–vector product *ᵥ, and indices as Fin m. and are LinearMap.range and LinearMap.ker of Matrix.toLin' P; "" is Matrix.PosSemidef, which includes symmetry. Admissible inputs are integrable on every (this contains , the input space of the paper's energy functionals). A solution is a function continuous on whose integrand is integrable on every and which satisfies the integral equation for all ; no uniqueness of solutions is presupposed, and the theorem is asserted for every such solution.
Two reading decisions are fixed. First, part (b) is stated for every admissible input , not only for as printed in the theorem: the paper's proof concludes " for all , implying ", and the theorem's clause "i.e., " (with a maximum over inputs) needs this form. The statement contains the printed one. Second, the clauses "i.e., " and "i.e., ", which restate the conclusions through the energy functionals (3.3)–(3.4), are not formalized.
The statements must not be trivialized: assuming positive definite makes (a) empty (), assuming stable or the Gramians unique adds hypotheses the paper does not have, and a solution notion requiring trajectories for integrable inputs would make the solution set empty. None of these is used. A local check confirms the hypotheses have content: for , , , the matrix is a nonnegative definite solution of (3.6) with .
A complete development needs Mathlib's facts on nonnegative definite matrices, interval integrals of vector-valued functions, and a Gronwall inequality with an integrable coefficient. The flow-invariance lemma for input-driven linear-in-state systems is reusable beyond this mission. Contributions welcome: proofs of the five milestones, and the passage from vector-field invariance to trajectory invariance.
Treewidth measures how closely a graph resembles a tree. Many problems that are NP-hard on general graphs can be solved in time linear in the number of vertices once a tree decomposition of bounded width is available, so computing such decompositions quickly is a basic task in algorithmic graph theory. Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (SIAM J. Comput. 45(2), 2016) gave an algorithm that, for a graph on vertices and an integer , either reports that the treewidth of exceeds or returns a tree decomposition of width at most , in time .
The paper's headline is that algorithm, a statement about pseudo-code and running times. This mission does not formalize it. It formalizes one of the paper's combinatorial lemmas, Lemma 6.5 (p. 369), which the algorithm's data structure uses to answer its balanced-separator query: it turns the search for a small balanced separator into two maximization problems that a dynamic program can solve.
Timeline. Robertson and Seymour (Graph Minors II, J. Algorithms 7, 1986) proved that graphs of treewidth have balanced separators of size (Lemma 2.1 of the paper). Robertson and Seymour (Graph Minors XIII, 1995) used it in an approximation algorithm, Reed (1992) improved the dependence on to , and Bodlaender et al. (2016) reached linear time with a single-exponential dependence on .
All graphs are finite and simple. For , is the graph obtained by deleting ; its components are the vertex sets of its connected components.
A separation of is a partition of (parts may be empty) such that no edge of joins to . Its order is . It is -balanced if .
For and sets of terminals , a terminal separation of the induced subgraph of order (Definition 6.4) is a partition of with
It is left-pushed if is maximum, and right-pushed if is maximum, among all terminal separations of of order with the same terminals.
The treewidth is the least width of a tree decomposition of (Definition 1.1), where the width is the largest bag size minus one.
Let and let be a separation of with . Then there are a partition of and integers with such that, for with terminals ,
In the order of the proof, the milestones are: Lemma 2.1 (balanced -separators of size , cited from Graph Minors II); the packing step of the proof sketch of Lemma 2.2 (components holding at most of each split into two sides holding at most each); the folklore -balanced separation of order ; the restriction of that separation to , which gives part (i); four lower bounds on , ; the dichotomy that two opposite "quadrants" have at least vertices each; the comparison of pushed separations with the restricted one; and the gluing step of part (ii).
Lemma 6.5 is what makes the paper's balanced-separator query computable: given a bag that splits a component in a balanced way, a left-pushed and a right-pushed terminal separation are each the solution of a maximization problem, and the lemma guarantees that gluing them gives a separator of order whose sides are bounded away from . The constant feeds into the approximation ratio of the whole algorithm.
The proof is complete in the paper and elementary given Lemma 2.1. No part of it is formalized in Lean's Mathlib or, as far as a search of the Prove2Me catalog shows, on the platform. Lemma 2.1 itself, Robertson and Seymour's balanced-separator theorem for bounded treewidth, is not in Mathlib; a machine-checked proof of it would be reusable wherever treewidth separators are used (divide-and-conquer on tree decompositions, Lipton–Tarjan style arguments, grid-minor theorems).
Everything after Lemma 2.1 is counting with partitions, but the bookkeeping is the obstacle: the two separations and cut into nine pieces, the induced subgraphs overlap on , and pushedness is a maximum over a family of partitions of a subset, not of .
Lemma 2.1 is the hard milestone. It is a statement about tree decompositions, and any proof has to relate subtrees of the decomposition tree to components of for a bag , infrastructure that does not yet exist in Mathlib.
V : Type with decidable equality; vertex sets are Finset V, is Finset.univ, is Fintype.card V. Universe 0 matches the published definition of treewidth.RobertsonSeymour1986.GM5.TreewidthLE G k: a decomposition tree on a finite type whose bags have at most vertices. Definition 1.1 roots the tree; rooting does not change the width.avoidComp G X u: the vertices reachable from by a walk of none of whose vertices, endpoints included, lies in .Part (i) is part of the goal: without it, left- and right-pushed separations of the chosen orders might not exist and part (ii) would hold vacuously. Choosing does not trivialize the goal, because the size bound and the budget must hold simultaneously.
Welcome contributions: a proof of Lemma 2.1 from tree decompositions (reusable on its own), the packing lemma, and the counting milestones of the proof of Lemma 6.5.
How should a set of indivisible items (courses, shifts, inherited objects) be divided among people who have different entitlements but no money to transfer? A classical answer for divisible goods is the competitive equilibrium from equal incomes (CEEI): give every agent a budget of artificial currency, find prices at which every agent can afford her favourite bundle and the market clears. The resulting allocation is Pareto optimal and fair. With indivisible items a CEEI can fail to exist already for one item and two agents with equal budgets: at any price, either both agents can afford the item or neither can.
Babaioff, Nisan and Talgam-Cohen (arXiv:1703.08150; Math. Oper. Res. 2021, doi:10.1287/moor.2020.1062) study this Fisher market with indivisible goods when budgets are generic: unequal budgets, with a measure-zero set of exceptional budget pairs excluded. Their main result is for two agents with almost equal budgets. This mission formalizes the companion result for two agents with identical additive preferences and arbitrary unequal budgets (Theorem 8.1 of the paper, its informal Theorem 1.4). With identical preferences the division problem is a discrete claims (bankruptcy) problem: one cake of fixed value is split between claimants with different entitlements .
Timeline of the relevant results:
There are indivisible items and two agents. Agent has a valuation that is additive, normalized (), non-negative, monotone and strict (different bundles have different values), and a budget , with . An allocation gives every item to exactly one agent. Item prices price a bundle at .
A bundle is demanded by agent at prices if and for every bundle with . A competitive equilibrium (CE) is a pair in which each is demanded by agent . An allocation is Pareto optimal (PO) if every other allocation is strictly worse for some agent. It is budget-proportional if for both agents, and anti-proportional if for both, strictly for one.
The truncated share of agent is
the best she can get in a PO allocation that gives her at most her budget share; an allocation gives her the truncated share if . The exceptional set (Definition 6.2) consists of the budget pairs for which two PO allocations , consecutive in agent 's order of preference, satisfy . It is finite. The rectangle (Definition 6.1) is a set of allocations between the truncated-share maximizers of the two agents.
In Lean all objects live in GenericBudgets.IdenticalPrefs: bundle, price, IsDemanded, IsCE, IsPO, IsStandardValuation, IsBudgetProportional, IsAntiProportional, GetsTruncatedShare, IsTruncMaximizer, InRectT, InR.
If , , and for some agent , then
Theorem 8.1 shows that the non-existence of CEEI for identical preferences is a knife-edge phenomenon: for every market with identical strict additive preferences, every unequal budget pair outside a finite set admits a CE, and the CE allocation is as close to budget-proportional as indivisibility allows. It gives a market-based solution to the indivisible claims problem with unequal entitlements, and its CE inherits Pareto optimality from the first welfare theorem (Theorem 2.4 of the paper).
The formalization targets three things on top of the paper. First, a machine-checked proof of the paper's main technical tool, Lemma 6.3, which also drives the paper's main Theorem 7.1 (mission 1 of this series), where it is applied to almost equal budgets instead of identical preferences. Second, precise definitions of the truncated share, the rectangle and the exceptional set , whose informal versions leave conventions implicit (the maximization runs over PO allocations only; is indexed by consecutive PO allocations). Third, verification of the proof chain Proposition 5.1 → Lemma 6.3 → Lemma 8.2 → Theorem 8.1. The statements compile, but none of these results has a machine-checked proof yet.
The reduction of Theorem 8.1 to Lemma 8.2 and the proof of Lemma 8.2 from Proposition 5.1 and Lemma 6.3 are short. The substance is in Lemma 6.3, which must exhibit prices supporting a PO allocation when no allocation gives both agents their budget shares. Demand is a condition over all bundles, so a candidate price vector has to be checked against every bundle each agent prefers, and the paper's construction breaks down on the exceptional budget pairs , which is why they are excluded; the argument is a case analysis over the finite Pareto frontier. The easy case, Proposition 5.1, covers only markets with a budget-proportional or anti-proportional PO allocation; with identical preferences and unequal budgets neither typically exists (no allocation is ever anti-proportional), so Lemma 6.3 cannot be avoided.
Items are Fin m; agents are Fin 2, with indices for the paper's agents , so is b 1 < b 0. Valuations are functions Finset (Fin m) → ℝ bundled with the standing assumptions in IsStandardValuation; identical preferences are the hypothesis v 0 = v 1. An allocation is a map Fin m → Fin 2, so every item is allocated exactly once. Budgets are positive reals summing to . All quantities are real.
Committed conventions and disclosed restrictions:
max: for every PO with .Trivializing formalizations are ruled out: the demand condition quantifies over every bundle with strict inequality, allocations must assign every item, prices are non-negative, the truncated share is maximized over PO allocations only (not over all allocations), and the budget hypothesis excludes only the finite set for one agent, never all unequal budgets.
Proposition 5.1 and Lemma 6.3 are posed with the same statement as in mission 1 of this series; a proof of either transfers verbatim. Contributions welcome: the finite-frontier infrastructure (existence and uniqueness of the truncated-share maximizer), Proposition 5.1 through budget-exhausting combination pricing, and Lemma 6.3.
The electroweak interaction is the unified description of electromagnetism and the weak nuclear force in the Standard Model of particle physics. Glashow, Salam and Weinberg shared the 1979 Nobel Prize in Physics for this unification, and its central predictions — neutral weak currents (Gargamelle, 1973) and the massive and bosons (UA1/UA2, 1983) — have been confirmed experimentally. The algebraic core of the theory is short: an gauge theory whose symmetry is broken by the vacuum value of a Higgs doublet, after which the neutral gauge fields are rotated by the weak mixing angle into the photon and the , and the masses satisfy .
This mission formalizes those tree-level algebraic facts as they are stated in the Wikipedia article Electroweak interaction (revision 1360331872), sections Formulation and Lagrangian.
Timeline (as recounted in the article). After the Wu experiment (1956) exposed parity violation, Glashow combined a chiral and an achiral symmetry and predicted a boson; Salam and Ward (1964) proposed a massless photon and three massive gauge bosons with manually broken symmetry; Weinberg (1967) used spontaneous symmetry breaking (Englert–Brout, Higgs, Guralnik–Hagen–Kibble, 1964) and predicted rough and masses; 't Hooft (1971) proved that spontaneously broken gauge theories are renormalizable. Neutral currents were observed in 1973 and the , in 1983.
Fix the weak isospin coupling and the weak hypercharge coupling . The gauge fields at a spacetime point, for one Lorentz component, are real numbers (weak isospin) and (weak hypercharge).
For all real ,
which is the mass part of in the article. The photon field does not appear: it stays massless.
These identities are the content behind the article's statements that "the axes ... have been rotated by the angle ", that , that , and that is unbroken because it does not couple to the Higgs. The formal library produced here (Pauli matrices, the Higgs doublet, the mixing rotation, the mass formulas) can be reused by later missions on the full electroweak Lagrangian, on the Yukawa sector, or on the custodial relation .
All statements are classical tree-level results. None is open; the work is to formalize them.
The mathematics is finite-dimensional linear algebra and trigonometry. The main pitfalls are conventions: the factor in front of the Pauli matrices, the hypercharge normalization (so the Higgs has ), and the sign conventions in the rotation matrix. The goal also requires handling complex doublets, factors and the inverse trigonometric definition of at the same time.
All fields are real numbers at one spacetime point and for one Lorentz component; the Lorentz contraction and the kinetic (derivative) terms are not modeled. The Higgs doublet is a function Fin 2 → ℂ, and its squared norm is written out as (not the sup norm of the product type). The Pauli matrices are defined explicitly. The angle is ; with this agrees with the triangle. The standing convention is a hypothesis wherever appears. The goal is stated as an equation in so that the product appears exactly as in .
All declarations live in the namespace ElectroweakWiki.
In ordinary quantum mechanics, and in quantum field theory on a fixed spacetime, events happen in a definite causal order: an operation either precedes another, follows it, or the two are spacelike separated. Attempts to combine quantum theory with general relativity call this assumption into question. In general relativity the causal structure is dynamical, and a quantum theory of gravity may allow it to be indefinite. Oreshkov, Costa and Brukner (Nat. Commun. 3, 1092 (2012), arXiv:1105.4464) turned this question into a precise mathematical one. They assume that quantum mechanics holds locally in each laboratory and make no assumption about any global causal order. Within that framework they ask which correlations between two laboratories are possible. They find correlations that no definite causal order can produce: these correlations violate a causal inequality, which every causally ordered scenario satisfies.
Timeline.
Alice's laboratory has an input system and an output system , and Bob's has and . All four are finite-dimensional, with dimensions , and operators on are complex matrices indexed by .
A local operation of Alice is described by its Choi–Jamiołkowski (CJ) matrix . The operation is a completely positive trace-preserving (CPTP) map exactly when
A process matrix is a matrix satisfying
(Eqs. (4)–(5) of the source). The probability of a pair of local outcomes is (Eq. (3)).
The task (Eq. (1)). Alice, Bob and a second bit for Bob receive independent uniform bits , and . Alice uses an instrument to produce a guess , and Bob uses to produce a guess . If Bob must communicate to Alice, and if Alice must communicate to Bob:
Causal separability (Eq. (6)). A process matrix of the form allows no signalling from Alice to Bob, written . One of the form allows none from Bob to Alice. is causally separable if for some .
The goal states only that a violation exists, with no hard-coded value. The specific value is a milestone.
is a process matrix. 3. Eq. (8): with the instruments of Eqs. (20)–(23), this gives , for every state that Bob may prepare. 4. p. 5: the matrix of Eq. (7) is not causally separable. 5. Appendix F: every process matrix that is diagonal in a product basis (a classical process) is causally separable. 6. Appendix C, Fig. 3: for Hermitian , the normalization condition (5) holds if and only if and has no Hilbert–Schmidt component of type , , , , , , or . 7. Appendix E, Eq. (26): , and .
The result. Milestones 1 and 3 together show that quantum mechanics, applied locally in each laboratory, does not by itself imply a definite causal order. The causal inequality is a device-independent test of causal order, analogous to a Bell inequality for local realism. Milestone 5 shows that indefinite causal order disappears in the classical limit, and the source reads this as a hint that spacetime causal structure may emerge in a quantum-to-classical transition. The process-matrix framework has since become standard for indefinite causal order. Milestone 6 is the characterization that later work on witnesses and causal inequalities relies on.
Formalizing it. All seven milestones and the goal are proved in the source; none are open mathematics. This mission produces machine-checked versions in a common vocabulary: process matrices, CJ instruments, causal separability and Hilbert–Schmidt type analysis. That vocabulary can be reused for later results such as witnesses of causal nonseparability, multipartite causal separability and the quantum switch.
Status honesty. The formal statements are about matrices. Whether causal-inequality violations can occur in nature is not settled. Laboratory realizations of the quantum switch certify causal nonseparability with witnesses, not with a causal-inequality violation, and the source leaves open whether is the largest possible violation.
The violation itself (milestones 2, 3 and 7) is finite linear algebra on matrices, but the irrational entries rule out a purely computational check. Positivity of is the nontrivial part of milestone 2. The two Pauli strings in anticommute, which fixes its spectrum, but this has to be turned into a positive-semidefiniteness proof.
Milestone 1 needs more than inspecting the definitions. The bound has to be shown for each no-signalling form separately and then carried through convex mixtures, with instruments of arbitrary dimension.
Milestone 4 is a non-existence statement over all decompositions. A direct search is hopeless; it follows from milestones 1 and 3.
Milestone 5 (Appendix F) is the deepest: it builds the two positive parts of the decomposition by an eigenvalue-shifting procedure.
Milestone 6 needs orthogonality computations with arbitrary Hilbert–Schmidt bases on four tensor factors.
⊗ₖ with tensor order . Local operations are represented directly by their CJ matrices, so the transpose in the source's CJ convention never enters the statements. Bits are Bool (false ↦ 0). Probabilities are real parts of traces, which are real whenever all inputs are positive semidefinite.OCB2012_defs: partial trace ptrace₂, IsCPTP_CJ, IsProcessMatrix, prob, IsAliceInstrument, IsBobInstrument, pSucc, the no-signalling forms, IsCausallySeparable, the Pauli matrices, W7, the instruments ξ and η, the structure HSBasis and the predicate AllowedType. Density matrices come from the published PeresTerno.IsDensityMatrix.The Wheeler–DeWitt equation is the quantum version of the Hamiltonian constraint of general relativity. In the canonical formulation, a spacetime is described by the evolution of the metric of a spatial slice, and Einstein's equations include a constraint: the Hamiltonian density vanishes at every point of space. Quantizing this constraint, as DeWitt did (Phys. Rev. 160, 1967), gives a second-order functional differential equation for a wavefunctional with no external time parameter.
Three structural facts make the equation distinctive:
A fourth issue is not settled: consistency. In the continuum, the Poisson bracket of two Hamiltonian constraints is a combination of the momentum constraints, so imposing all constraints is consistent (Dirac's first-class condition). Any regularization of the quantum equation, a lattice for instance, must reproduce this. Generic lattice discretizations do not: the constraints become second class (Bander 1987; Dittrich 2008; Bahr–Dittrich 2009). Whether, and with which anomaly, the Hamiltonian-constraint commutators close as the lattice is refined was singled out as an open question by Loll (Living Rev. Rel. 1998, §2.12).
The first three facts are the standard entry points of quantum geometrodynamics, as reviewed by Kiefer (arXiv 0812.0295): Section 2 for the constraints and their quantization, eqs. (3)–(8), and Section 3 for the Hamilton–Jacobi equation, eq. (10), and the semiclassical approximation, eq. (11).
A spatial metric at a point is a symmetric positive-definite matrix . Write . The DeWitt supermetric is
It is a quadratic form on symmetric momenta. Its inverse acts on velocities.
Space is represented by a finite set of sites; this is a lattice regularization. A configuration assigns to each site a matrix . All nine entries are coordinates, so configuration space is , and physical configurations are those that are symmetric and positive definite at every site. A wavefunction is a function from configurations to . The functional derivative is the partial derivative with respect to the coordinate , with the cell volume normalized to one.
The Wheeler–DeWitt operator at site , with gravitational coupling , cosmological constant , and a supplied potential playing the role of the spatial scalar curvature, is
Write for the potential at site . On the classical phase space of pairs , with conjugate to , the lattice constraints are
with the canonical Poisson bracket. They are first class if each bracket vanishes wherever all constraints vanish.
The supermetric stands to the left of both derivatives (Kiefer, eq. (7), vacuum case; the coupling is , so as in Kiefer's eq. (10)). The kinetic term involves only derivatives at the same site, as in the continuum; it is ultralocal. The potential may couple neighbouring sites.
For with and :
For every real function and :
The -independent part is the Einstein–Hamilton–Jacobi functional of Kiefer's eq. (10), Hamiltonian part, with the eikonal of the WKB form (11) (amplitude ). This is the weakest statement exhibiting the classical limit, and it holds for every potential.
For and sites :
If every depends only on , then identically.
If the symmetric part of is nonzero at a physical , for some , then there is a point of the constraint surface over at which .
Every finite-difference curvature couples neighbouring sites, so the goal applies to every such discretization. It is the weakest statement that the discretized constraint algebra is inconsistent, and it holds uniformly in the discretization.
Tendsto statement.The signature theorem is the mathematical content behind two physical facts: the hyperbolic character of the Wheeler–DeWitt equation, and the instability of the conformal mode (the "conformal factor problem" of Euclidean quantum gravity). DeWitt's cone form identifies the local volume as an intrinsic clock. On this rests the reading of the equation as a wave equation in superspace, with as time. The conformal-sector reduction shows explicitly how the timelike direction appears in the operator, with the sign opposite to the traceless modes. The WKB identity is the precise sense in which the quantum constraint contains classical general relativity: its leading order is the Hamilton–Jacobi form of the Einstein constraint (Peres 1962; Kiefer, eq. (10)), and its next order is the one used in derivations of the Schrödinger equation from quantum gravity.
All of these are classical computations. The drafter knows of no machine-checked version. A formalization fixes conventions that the literature handles loosely:
It does so with genuine derivatives in place of formal symbols.
The constraint-algebra part turns a phenomenon described qualitatively in the literature into a theorem with exact hypotheses. Lattice constraints are second class as soon as curvature couples sites, and the quantum commutator is given in closed form. It also isolates precisely what a consistent discretization would have to cancel. The continuum-limit target addresses an open question in canonical quantum gravity.
The supermetric statements are finite-dimensional, but none is a single computation. The signature requires a positivity argument for on an -traceless subspace. The cone form requires separating the trace part of a velocity in a non-orthonormal frame.
The analytic targets require second derivatives of compositions through the determinant and the matrix inverse. The derivative of at in the direction of a single entry is , and the derivative of produces terms like ; a sign or index slip changes the constant . Treating the nine entries as independent coordinates, rather than the six symmetric ones, changes the numerical coefficients; the conventions below fix this.
For the constraint algebra, the quantum commutator involves up to fourth derivatives of , which cancel only by the symmetry of mixed partials. The classical goal needs a point on the constraint surface where the bracket is nonzero. Each constraint fixes the value of an indefinite quadratic form in the momenta, and the bracket is linear in them, so the proof must use the Lorentzian signature to show that the bracket is not constant on that quadric.
A naive formalization that replaces by an abstract linear map reduces every target to ring arithmetic, and is ruled out by the definitions.
Def_WheelerDeWittSuperspace):
Fin 3 → Fin 3 → ℝ, so that configuration space X → Fin 3 → Fin 3 → ℝ with X a Fintype is a normed space;Matrix.of;fderiv ℝ Ψ h applied to the coordinate direction of ;Real.sqrt of the determinant;Matrix.PosDef includes symmetry);At high energies (, the Regge limit) scattering amplitudes of gauge theories simplify and organise into towers of logarithms . For the four-gluon amplitude of super-Yang–Mills theory with gauge group , the colour structure is what makes the nonplanar (subleading in ) amplitude hard to control. Naculich (2020) builds a basis of colour factors adapted to the Regge limit at every loop order, writes the -loop amplitude in that basis, and uses one of its coefficients, , to motivate a conjectured all-loop relation with the Regge limit of the supergravity four-graviton amplitude. The physics conjecture itself is not a mathematical statement; what is exact and checkable is the colour algebra underlying it — finite-dimensional linear algebra over polynomials in .
Trace basis. Four-gluon colour factors are expanded in six single and double traces of fundamental generators (eq. (2.1)). A colour vector is a column of polynomials in , with complex coefficients.
Colour operators. The -channel Casimir and the crossing-odd combination act on colour vectors as the explicit matrices of eq. (4.15) (entries in ). The tree-level -channel colour factor is . Crossing (exchange of legs 2 and 3) is the permutation : , .
Regge colour factors. With ,
each with exactly operators. The admissible pairs are , , and for .
Extended trace basis. At loops, for and for , giving elements (eq. (2.3)). The colour-ordered amplitudes of an amplitude are its coordinates in this basis (eq. (2.4)).
Regge-basis amplitude. Eq. (4.24):
Null vectors. Four vectors per loop order (eqs. (2.10), (2.12), extended by prepending zeros) encode the group-theory relations among the .
For every even ,
and for , . The paper obtains the even- formula by guessing from explicit results through ; a proof for all is not given there.
The result. Eq. (4.26) is the input to the paper's analysis of the infrared behaviour of (at most , manifest for even because only most-subleading-colour amplitudes appear), and hence to the conjectured all-orders relation between and the Regge limit of supergravity (Sec. 6). An all- proof replaces an extrapolation from nine loop orders by a theorem.
Formalizing it. The low-loop tables (4.16), (4.20), (4.18), (4.22) are finite computations; the goal and milestones 3, 4, 7, 8 are statements for every loop order and need genuine arguments (induction on , structure of the operators on the extended basis).
The coefficient is defined through the whole -element basis: a formula for it must vanish on every other , including the nested commutators and whose components grow in complexity with . Checking the formula loop order by loop order does not give a proof; one needs to control how and act on the two most-subleading slots of the extended basis uniformly in .
Fin 6 → ℂ[X], with the polynomial variable X; operators are Matrix (Fin 6) (Fin 6) ℂ[X] acting by Matrix.mulVec. Coefficients and the prefactor are arbitrary complex numbers; is a function ℕ × ℕ → ℂ of which only the admissible pairs matter.LinearIndependent, finite sums) is used.In February 1998 Witten's paper Anti de Sitter Space and Holography made precise Maldacena's proposal that large- conformal field theories in dimensions are described by gravity on -dimensional anti de Sitter space . The dictionary it proposes identifies boundary values of bulk fields with sources of boundary operators, and reads correlation functions off the dependence of the bulk action on those boundary values. Its most quoted quantitative consequence is the mass–dimension relation: a scalar of mass on corresponds to a boundary operator of conformal dimension
Behind this physics statement sits a piece of classical analysis on hyperbolic space: the Dirichlet-type problem for the operator with prescribed boundary asymptotics, solved by an explicit Poisson-type integral (Section 2 of the paper, eqs. (2.15)–(2.44)). This mission formalizes that analytic core.
Timeline. Maldacena 1997 (hep-th/9711200) conjectured the correspondence; Gubser–Klebanov–Polyakov (hep-th/9802109) and Witten (hep-th/9802150, both February 1998) proposed the precise dictionary; the Euclidean black-hole thermodynamics used in Section 3 goes back to Hawking–Page 1983.
Euclidean is modelled as the upper half space with the hyperbolic metric
Its Laplace–Beltrami operator is
A massive scalar of squared mass solves (eqs. (2.34), (2.37)). The conformal dimension is (eq. (2.44)), the bulk-to-boundary kernel is
and the Poisson-type integral of a boundary datum is (eqs. (2.20), (2.41)).
For there is a constant such that for every bounded continuous on ,
is a solution of on the upper half space and as , i.e. at the boundary (eq. (2.36) with ).
The goal is the analytic statement underlying the mass–dimension relation of the AdS/CFT dictionary: it shows that the boundary datum of a massive field is naturally a density of weight , which is how the paper identifies the dimension of the dual operator. The same kernel is the starting point for the two-point function (2.42). The result is classical mathematics (scattering theory on hyperbolic space), proved informally in the paper; this mission produces a machine-checked version together with reusable infrastructure for the hyperbolic Laplacian in half-space coordinates.
The pointwise identities (milestones 1, 2, 6, 7, 8) are calculus. The substance is analytic: differentiating the Poisson-type integral twice under the integral sign with only boundedness of , and proving the approximate-identity limit with the right normalisation; the scaling integral requires , and the endpoint (where and the kernel is not integrable) must be excluded.
Points are pairs ; partial derivatives are one-variable derivs, so the solution predicate also demands regularity on , which rules out junk values of deriv. Real powers are Real.rpow; integrals are Bochner integrals for Lebesgue measure. Boundary data are bounded continuous functions. All declarations live in the namespace WittenAdSHolography, with the shared definitions in one definition file.
A coupling constant is the number that fixes the strength of an interaction: in the modern formulation it is the parameter weighting the interaction part of a Lagrangian against its kinetic part. In a quantum field theory such a parameter is not constant. Probing a process at a higher energy resolves more of the virtual activity that dresses the interaction, and the value one measures depends on the energy scale at which the measurement is made. This scale dependence is called the running of the coupling, and it is the organising phenomenon behind two of the best-known qualitative facts about the Standard Model: the electromagnetic coupling grows with energy ( at low energy, at the mass, about 90 GeV) and apparently diverges at a finite energy — the Landau pole — while the strong coupling decreases logarithmically at high energy, the asymptotic freedom found by Gross, Politzer and Wilczek and recognised by the 2004 Nobel Prize.
The source treats the running through the beta function, defined there by
and through the one-loop strong coupling
Everything in this mission is the mathematics of those two formulas: an autonomous scalar ordinary differential equation in the logarithm of the energy, and the behaviour of its solutions according to the sign of the one-loop coefficient.
Write for the energy scale of a process and , or , for a real-valued coupling as a function of that scale. The beta function in the energy scale is the logarithmic derivative used by the source,
a function of built from ; a theory whose beta function vanishes identically is scale-invariant, since its coupling then takes the same value at every scale.
A coupling is said to be one-loop running with coefficient on a set of scales when it satisfies, at every ,
equivalently . Here is the asymptotically free sign (QCD) and the sign the source attributes to QED. The equation is the one-loop truncation written in rather than in : both forms appear in the source, and the first milestone is precisely their agreement.
The one-loop strong coupling with one-loop coefficient and QCD scale is the explicit function
the formula the source quotes for . It is defined by an existing platform definition, which this mission reuses rather than restates.
For every reference scale and every positive reference value of the coupling at that scale:
The negative-coefficient half is asymptotic freedom together with the uniqueness of the solution; the positive-coefficient half is the Landau pole, stated as the non-existence of any solution up to the pole scale rather than as a divergence of one chosen formula. The pole scale is the one the one-loop equation itself predicts.
The milestones below range from the definitional identity , through the three qualitative readings of the sign of that the source states in words (vanishing beta function means scale invariance; positive beta function means the coupling grows with energy; negative means it falls), to the identification of the quoted QCD formula as an exact solution of the one-loop equation and the determination of from a single measured value.
The dichotomy is the mathematical content of two physical statements that the source presents side by side. Asymptotic freedom is what makes perturbative QCD predictive at high energy; the Landau pole is the reason the source warns that the perturbative beta function cannot be trusted at strong coupling, since the one-loop equation has no solution reaching the pole scale at all. Formalizing the uniqueness half also pins down what "the" running coupling means: the explicit formula is not merely one solution of the renormalization-group equation but the only one through a given data point.
An earlier public mission on the same source ("Coupling Constant: One-Loop Running, Asymptotic Freedom and the Landau Pole") formalized the one-loop flow in the logarithmic variable with a cubic beta function , and its statements are proved. This mission is stated in the other variable the source uses — the energy scale itself, with the quadratic one-loop equation for — and adds the parts of the source that the earlier mission does not cover: the defining identity between the two forms of the beta function, the sign-to-monotonicity statements for an arbitrary (not necessarily one-loop) coupling, the explicit pole scale, and the determination of the QCD scale from a measurement. Where the earlier mission already settles a statement in the quoted formula's variables, this proposal references the published theorem instead of restating it.
The equation is elementary, and the difficulty is entirely in what the statements quantify over. The negative-coefficient half asserts that every function satisfying the equation on is the explicit one, so it needs a uniqueness argument for a nonlinear scalar ordinary differential equation rather than a verification that a formula works; the substitution that makes the equation linear is legitimate only while is known not to vanish, which is part of what has to be proved. The positive-coefficient half is a non-existence statement on a closed interval reaching the pole, so no local solution can be extended to it; the naive attempt — differentiate the explicit formula and observe that it blows up — proves nothing about the other candidate solutions.
Couplings are total functions , and every statement restricts to the scales it is about: the positive half-line for the beta-function statements, for the explicit QCD formula, or a closed interval for the one-loop flow. Outside those ranges nothing is claimed — in particular at , where the logarithm in the quoted formula vanishes or is negative and the reciprocal returns a junk value. Differentiability is a hypothesis where it is needed, written as a two-sided derivative at each scale of the set, so that a statement cannot be satisfied by a one-sided artefact at an endpoint. The one-loop property is phrased as an exact differential equation, never as an asymptotic approximation, and the Landau-pole milestone is a non-existence claim rather than a divergence claim, so it cannot be discharged by exhibiting a formula with a singularity.
A complete development needs the mean value theorem, Gronwall- or uniqueness-type arguments for scalar ordinary differential equations, and the standard logarithm and exponential API; the uniqueness lemma for and the reciprocal substitution are reusable beyond this mission. Contributions of a general scalar-ODE uniqueness lemma, usable by both this mission and the earlier one, are especially welcome.
The Polyakov action is the standard action for the worldsheet of a bosonic string. It was introduced by Deser and Zumino and independently by Brink, Di Vecchia and Howe in 1976, and is associated with Polyakov after he used it to quantize the string in 1981. Its value over the Nambu–Goto (area) action is that it is quadratic in the embedding fields, which makes quantization tractable, while being classically equivalent to the area action. This mission formalizes the classical facts collected in the Wikipedia article Polyakov action.
A string sweeps out a two-dimensional worldsheet with coordinates . Its embedding in a -dimensional target is ; the target carries a metric , and the worldsheet carries an independent (auxiliary) metric with inverse and determinant . With the induced metric and string tension , the Polyakov and Nambu–Goto actions are
The stress–energy tensor is . Signature convention: timelike , spacelike .
If the auxiliary metric satisfies its equation of motion (with ), then
These are the classical foundations of bosonic string theory: the symmetries (Poincaré, diffeomorphism, Weyl) are what make the conformal gauge reachable, and the equivalence with Nambu–Goto justifies using the quadratic action. All statements are textbook results; the work here is to formalize them with explicit hypotheses (differentiability, integrability, positivity of ) that the physics presentation leaves implicit.
The algebraic statements are matrix identities. The diffeomorphism invariance needs the change-of-variables formula; the infinitesimal Lorentz statement needs care with integrability; the wave-equation milestone needs the fundamental lemma of the calculus of variations; and the light-cone solution is d'Alembert's theorem.
Worldsheet (coordinates Fin 2 → ℝ, index ), target . Actions are Bochner integrals over a region . The inverse metric is Mathlib's matrix inverse. Quantization, Virasoro operators, the Liouville action and string boundary conditions are out of scope.
Whether the many-worlds (Everett) interpretation of quantum mechanics is local in the sense of Bell is a recurring question in the foundations of physics. A number of authors have argued that Everett's theory escapes Bell-type nonlocality theorems because it drops the assumption that each measurement has a single outcome. A. Drezet's paper arXiv:2306.07794 (2023) argues against this claim by revisiting the Greenberger–Horne–Zeilinger (GHZ) nonlocality theorem, which, unlike Bell's inequality, uses only probability-one (perfect) correlations. Its central mathematical step, stated in Section II, is that no locally causal beable model can reproduce the quantum predictions for the GHZ state. The paper's argument is that this step makes no assumption about completeness or hidden variables, and so applies to Everett's theory as well.
Timeline:
Three spin-½ particles are sent to three distant observers, Alice, Bob and Charlie. Each one measures the spin of their particle along a direction and records an outcome . The particles are prepared in the GHZ state
and quantum mechanics predicts the joint outcome probabilities through the Born rule, . Here denotes the eigenvector of with eigenvalue . In Lean this is bornProb n₁ n₂ n₃ α β γ.
A locally causal (Bell-local) model consists of
Such a model predicts
In Lean the model is a LocalCausalModel Λ and its prediction is M.predict. The beables are arbitrary: may be a hidden variable, or the quantum state itself as in the Beltrametti–Bugajski representation, Eq. (15).
No locally causal model reproduces the quantum predictions on the four GHZ settings , , , :
The goal theorem is the mathematical core of the paper's conclusion that any beable account of the GHZ correlations, including one where is just the quantum state, violates Bell's local causality. Milestones 6–8 formalize the paper's separation of notions of locality: non-signalling holds both in quantum mechanics and in every locally causal model, so it cannot tell them apart; and dropping statistical independence (Eq. (18)) is enough to reproduce the correlations. The GHZ theorem itself has been known since 1989. As far as the drafter is aware it has no machine-checked formalization on this platform, and this mission provides one, stated for general measurable beable spaces.
The combinatorial core (milestone 3) is a parity argument. The substance lies in the steps that connect it to probability: showing that perfect correlations force determinism almost surely when is an arbitrary probability measure (null sets, measurability, integrals of nonnegative functions), and computing the Born probabilities exactly in Lean from explicit matrices and eigenvectors.
ℤˣ (exactly ). Settings form a two-element type Setting with values x and y. Qubit index 0 is and index 1 is . Three-qubit operators are Kronecker products.LocalCausalModel Λ has a probability measure ρ on a measurable space Λ and measurable response functions P j λ n α with values in that sum to one over . The fixed state is left implicit. Predictions are Bochner integrals, and all integrands are bounded and measurable.In emergent gravity proposals, spacetime and gravity are macroscopic descriptions of an underlying quantum system. In Verlinde (2016) it is argued that in de Sitter space (a universe with positive dark energy) the entanglement entropy has, besides the usual area-law part, a thermal volume-law part, and that matter displaces this volume-law entropy. The elastic response of the medium to this displacement produces an extra gravitational pull, which the paper proposes as the origin of the effects usually ascribed to dark matter in galaxies and clusters.
The physical derivation is heuristic, but it ends in explicit mathematical relations between the baryonic (visible) mass profile and the apparent dark matter mass profile of a spherically symmetric, isolated system. The central one is the integral relation (7.40),
where is Newton's constant and is the Hubble acceleration scale. For a point mass it reproduces Milgrom's empirical acceleration relation and the baryonic Tully-Fisher relation with .
All quantities are real numbers or real functions of the radius . and are constants. and are the baryonic and apparent dark masses inside radius . The Newtonian accelerations are and (7.42). The averaged density inside radius is (7.45), and the slope parameter is (7.46). A local density gives (7.39).
The paper also uses two purely mathematical facts about elastic strain in spatial dimensions: a bound (7.30) on the largest principal strain of a traceless symmetric strain tensor, and the integration-by-parts identity (7.31) between the squared Hessian and the squared Laplacian.
If is constant and (7.40) holds for every , then for every
The point-mass relation (7.43) is what connects the paper to the observed flat rotation curves and the baryonic Tully-Fisher law; (7.47) is its extension to extended mass profiles, which the paper uses to discuss galaxy clusters. The formal content checked here is the mathematics that turns the stated relation (7.40) into these observable consequences, plus the two elasticity lemmas used on the way to (7.40). The physical steps that lead to (7.40) (the entropy-displacement picture, the elastic interpretation, the identification (7.35)) are not mathematical statements and are outside the scope of this mission. None of these relations is known to have been machine-checked before.
The algebra is short once one may differentiate; the work is in the analysis. (7.40) is an integral identity with a singular weight at the origin, so recovering pointwise information requires the fundamental theorem of calculus on with only continuity there, and care with integrability at . (7.31) is a double integration by parts in that must be justified for the chosen decay class. (7.30) needs the spectral theorem for symmetric matrices, or an equivalent argument.
All statements live in the namespace Verlinde2016. Radial profiles are functions , with hypotheses only on . The integral in (7.40) is Lean's interval integral over ; since it would be for a non-integrable integrand, the positivity of the right-hand side forces integrability. Continuity of (and of densities) on is taken as a standing physical convention. In (7.31) the paper's condition that " falls off rapidly enough" is formalized as smooth with compact support. Spatial dimension is in (7.30); (7.40)–(7.51) use as in Section 7.2. Definitions: avgDensity, slopeParam, partialDeriv.
Liouville field theory is a two-dimensional conformal field theory whose classical equation of motion generalizes Liouville's equation. It is one of the few interacting conformal field theories with a continuous spectrum that has been solved: its three-point function on the sphere is given by the DOZZ formula (Dorn–Otto 1994; Zamolodchikov–Zamolodchikov 1996), proved rigorously from a probabilistic construction of the path integral by Kupiainen–Rhodes–Vargas (2017), with the conformal bootstrap established by Guillarmou–Kupiainen–Rhodes–Vargas (2020). It appears in two-dimensional quantum gravity, non-critical string theory, and log-correlated random energy models.
This mission is the first in a series following the Wikipedia article on Liouville field theory. It formalizes the kinematic layer of the theory: the algebraic relations between the coupling constant, the background charge, the central charge, the conformal dimensions and the reflection coefficient, on which every later statement (the spectrum, the DOZZ formula, the bootstrap) is phrased.
Fix a complex number , the coupling constant. Define
with sign if and otherwise.
Two symmetries act on these data: the reflection and the duality . The spectrum of the theory is the set of dimensions , parametrized by momenta , .
For every , the map is a bijection
These identities are the dictionary between the parameters used in the physics literature (, , , , , ) and fix the conventions for later missions in the series: the DOZZ formula, the pole structure of correlation functions, and the reflection and duality covariance of structure constants are all stated in these variables. None of these statements is open; the value of the mission is a vetted, reusable definition layer with machine-checked consistency of the conventions.
The individual statements are elementary algebra over , together with the non-vanishing of the Gamma function away from its poles. The care needed is in conventions: total functions in Lean (, principal-branch complex powers, Gamma at its poles) must be handled by explicit hypotheses exactly where the source implicitly excludes degenerate values.
All quantities are complex-valued functions of , defined in the namespace LiouvilleFieldTheory. is Lean's inverse (so gives junk values , ; statements that need assume it). is taken to be . The condition is encoded as . is the principal-branch complex power. The analytic content of the article (Virasoro representations, conformal blocks, the special function , the path integral, the DOZZ formula) is out of scope for this mission.
Optimal transport compares two distributions by finding the least expensive way to move mass between them. For finite histograms, the resulting linear program is precise but its optimal coupling can be sparse. In applications where the coupling represents traffic, matching, or a differentiable loss, a sparse plan may be undesirable or expensive to compute repeatedly. Peyré and Cuturi describe how adding an entropy term selects a diffuse coupling and leads to matrix scaling algorithms that can be used on large finite problems (Peyré and Cuturi, 2019, Chapter 4).
The entropic dual gives a second view of the same regularized problem. Its variables are real vectors attached to the two marginal constraints. Unlike the ordinary Kantorovich dual, the objective has no explicit feasibility constraints and is smooth. This permits calculations in the log domain, which the book introduces because direct scaling with exponentials can suffer from numerical overflow or underflow when the regularization parameter is small relative to the costs (Peyré and Cuturi, 2019, §4.4). This mission targets the exact relationship between the regularized minimum, the smooth dual maximum, and the scaling factors.
Fix positive integers . A histogram is a vector with nonnegative entries summing to one; is defined similarly. Strict positivity is required for the attained dual maximum and log-domain updates; the primal scaling and Kantorovich-feasibility statements also cover zero-entry histograms. A coupling is an matrix with nonnegative entries, row sums , and column sums . A real matrix assigns cost to each transfer from row to column , and is its transport cost.
The book uses the entropy , with . For , the regularized cost is . The Gibbs kernel has entries . Given potentials and , the smooth dual objective is . These are the finite-dimensional objects of (4.1), (4.2), and (4.30) in the source (Peyré and Cuturi, 2019, pp. 425, 428, 448).
The goal is Proposition 4.4. There are an optimal coupling and potentials at which the dual reaches its maximum, with the common value
For every maximizing pair , the same optimal coupling satisfies
Thus the dual potentials determine the scaling vectors and in (4.12). The maximum is an attained maximum of a real function, as stated in the book, rather than an unrestricted real infimum or supremum that might take a default value on a bad input (Peyré and Cuturi, 2019, Proposition 4.4).
The milestones follow the source's statements. Proposition 4.3 gives existence, uniqueness, and the Gibbs scaling of the primal optimizer. Remark 4.21 gives the two partial-gradient formulas and the closed log-domain block updates. Proposition 4.5 states that an entropic dual maximizer is a feasible pair of ordinary Kantorovich potentials, so its linear objective is bounded above by the unregularized cost (Peyré and Cuturi, 2019, pp. 432, 449, 452–453).
The equality establishes that the matrix scaling variables and the dual potentials describe the same optimal coupling. It lets a computation based on scaling be interpreted as maximizing a smooth objective, and it gives exact marginal-error expressions through the dual gradients. Feasible Kantorovich potentials obtained at the optimum also provide a lower bound on the ordinary transport cost. These statements explain why log-domain updates represent the same mathematical problem as entropic transport, even when direct exponentiation is numerically fragile (Peyré and Cuturi, 2019, §§4.4–4.5).
The results are established in the textbook; the open work here is their Lean formalization. A completed development would provide reusable finite coupling, entropy, Gibbs-kernel, and smooth-dual interfaces, together with the existence and differentiability results needed to connect them. It would also distinguish a primal optimum, a dual maximum, and a feasible potential without relying on informal convention. The mission does not assert that these textbook results are new, and no machine-checked proof of these exact statements is claimed here.
The unconstrained dual objective has a symmetry: shifting every coordinate of by one constant and every coordinate of by its negative leaves the value unchanged. Consequently, the set of maximizers is not bounded in the ordinary product space. Positivity of the marginals matters for attaining a maximum with finite real potentials; if a marginal entry is zero, the corresponding potential can escape toward negative infinity. On the primal side, the entropy formula must be valid at zero entries even though optimality links it to strictly positive exponential scalings. The formal argument must connect these boundary conventions and the finite-dimensional optimization statements without turning the maximum into a junk real supremum (Peyré and Cuturi, 2019, Proposition 4.4 and Remark 4.21).
The Lean development represents indices by Fin n and Fin m, matrices by Matrix (Fin n) (Fin m) ℝ, and histograms by Mathlib's stdSimplex. Positive dimensions and appear throughout. Strictly positive marginal entries are required for the attained dual maximum and log-domain updates; the other statements permit zero entries. The book assumes positive weights for discrete measures in Remark 2.1; the marginal positivity is also required for the attained dual maximum and the logarithmic updates. The cost matrix itself may have arbitrary real entries. Entropy uses Real.negMulLog, which implements on the nonnegative couplings where it is applied.
The primal optimum is a predicate on a coupling and its objective, rather than a chosen matrix. The unregularized is a real infimum used only when simplex marginals make its feasible set nonempty and bounded. The dual objective is a finite sum. Its gradients are stated as one-variable derivatives in each coordinate, and each block update is characterized as the unique maximizer with the other block fixed. The complete development needs Mathlib's finite sums, real exponential and logarithm, calculus, finite-dimensional topology, and optimization facts. Contributions that establish these shared interfaces or the four milestone statements are in scope.
Propositions 4.7 and 4.8 are excluded from this proposal because their printed bounds compare a dual linear objective with where the accompanying arguments instead support a comparison with the unregularized ; (4.47) also has a sign discrepancy. The milestone list therefore avoids encoding a false inequality (Peyré and Cuturi, 2019, pp. 453–454).
The discrete optimal transport problem of Kantorovich asks for the cheapest way to move a probability histogram onto a histogram when moving a unit of mass from to costs . Its optimal couplings are vertices of a polytope and are typically sparse: they rely on a few routes. Two communities have reasons to blur them. In transportation planning, observed traffic is more diffuse than linear-programming predictions, which led to the "gravity" model of Wilson (1969) and Erlander (1980), as recounted in Peyré and Cuturi, §4.1. In machine learning and statistics, adding an entropy term to the objective turns the linear program into a strictly convex problem that Sinkhorn's matrix-scaling algorithm solves at scale (Cuturi, 2013).
Every use of the entropic problem raises the same question: what does the regularized solution approximate? Chapter 4 of Peyré and Cuturi's Computational Optimal Transport answers it in Proposition 4.1 for the two extreme regimes of the regularization strength .
Timeline. Cominetti and San Martín (1994) studied the convergence of entropic penalties for linear programs, including first-order expansions near and . Peyré and Cuturi (2019) record the transport case as Proposition 4.1, with a short compactness proof.
Fix sizes . A histogram is a vector of the probability simplex . Given , , the set of couplings is
nonnegative matrices with row sums and column sums . For a cost matrix write . The Kantorovich problem is .
The discrete entropy of a coupling is
with . For the entropic problem is
whose unique minimizer is . The maximum-entropy optimal coupling is the optimal coupling of the Kantorovich problem with the largest entropy. The Gibbs kernel is and the Kullback–Leibler divergence between matrices is .
In Lean these are couplings, frob and IsOptimalCoupling in CompOT.Assignment, and entropy, entObjective, IsEntropicOptimal, IsMaxEntropyOptimal, gibbs and klMat in CompOT.EntropicLimit.
For , and any cost matrix ,
The result. Proposition 4.1 justifies the entropic regularization as an approximation scheme: for small the regularized plan converges to an exact optimal plan, and specifically to a canonical one, the most diffuse among all optimal couplings, so the limit does not depend on any tie-breaking. The value converges to the transport cost, which is what makes Sinkhorn-based estimates of transport distances meaningful. For large the plan becomes the independent coupling , which explains the interpolation between optimal transport and maximum mean discrepancy studied later in the book. The KL projection identity (4.7) is the starting point of Sinkhorn's algorithm, so this mission also supplies the bridge to the next missions of the series.
Formalizing it. The proposition is a known result with a complete proof in the source; the work is formalizing it in Lean 4 with Mathlib. To our knowledge none of these statements, nor the discrete entropic transport problem itself, has a machine-checked proof in Mathlib or on the platform. A formal proof also pins down the convention for zero entries, on which the statement silently depends.
The obvious argument passes to the limit in the optimality of , but this only shows that limit points are optimal for the Kantorovich problem; it does not identify which optimal coupling is the limit when the optimal set is a face of the polytope rather than a vertex. Identifying it requires a second-order argument at the level of the entropy, and the convergence of the whole family (not just a subsequence) rests on the uniqueness of the maximum-entropy optimal coupling, which in turn needs strict concavity of on a set that may contain matrices with zero entries, where the logarithm is singular. Existence and uniqueness of face the same boundary issue: the minimizer may a priori sit on the boundary of the polytope.
Indices are 0-based (Fin n, Fin m); histograms are functions Fin n → ℝ in Mathlib's stdSimplex; matrices are Matrix (Fin n) (Fin m) ℝ with the product topology, so convergence is entrywise. Entropy uses (Real.negMulLog); the book's remark that at a zero entry is not used, since it would contradict the continuity of invoked in the book's proof and make (4.3) degenerate. Optimality is expressed by predicates (a minimizer over ), never by a real infimum, so no junk value of an empty infimum appears. The limit is taken from the right. The values and appear as the objectives at and .
In the goal, and are given by hypotheses (any family solving (4.2) for every , any solution of (4.3)). This is not a vacuous formalization: milestones 1 and 2 assert that such objects exist and are unique, so the hypotheses are satisfiable and determine them. Standing assumptions are exactly those of the book: , , ; no positivity of , or is assumed.
A complete development needs: compactness of the transport polytope, continuity and strict concavity of on , and the Gibbs inequality on finite sums. These are reusable for the Sinkhorn and entropic-duality missions of this series. Proofs of any milestone are welcome independently.
Statistical learning algorithms fit hypotheses to data that are available during training, while their performance is judged on new data. A rule that minimizes training loss can fit peculiarities of the sample, so its training loss and population loss need not agree. Xu and Raginsky study this difference through information quantities associated with the sample and the algorithm's output. Their Gibbs example shows how a probability distribution chosen before seeing the data can guide a randomized learner and yield a population-risk guarantee with explicit dependence on the sample size and the prior's mass at a good hypothesis. This mission formalizes their countable-hypothesis result, Corollary 2, and the steps of Section 4.3 and Appendix D that support it. Xu and Raginsky, 2017
Let be an instance space and a hypothesis space, each with a measurable structure. A probability measure on generates a sample of independent observations. A loss measures the cost of hypothesis on instance . Its population risk is ; its empirical risk on a realized sample is . These definitions match equations (1)–(3) of the paper. Xu and Raginsky, 2017, p. 2
A randomized learning rule is a Markov kernel : for each observed sample , it gives a probability distribution for an output hypothesis . Together with the sample law , it determines the joint law of . The expected generalization error is , as in equation (4). A probability distribution on serves as a prior. The Gibbs rule at inverse temperature weights a hypothesis by its prior mass times , then normalizes across the hypothesis space. Thus it favors low empirical risk without discarding the prior. Xu and Raginsky, 2017, pp. 2, 6
The associated optimization problem balances expected empirical risk against the conditional Kullback–Leibler divergence from the learning kernel to : . This penalty measures how much the output distribution changes from the prior after observing the sample. The paper's Theorem 5 identifies the Gibbs kernel as an optimizer of this relaxed problem. Xu and Raginsky, 2017, p. 6
For nonnegative loss, Theorem 5 asserts that the Gibbs kernel is a Markov learning rule, has the normalized exponential distribution at each sample, and minimizes the relaxed objective over learning kernels:
The milestone list also records the Appendix D empirical-risk comparison with a fixed hypothesis, its identity when the prior has positive mass at , and the Gibbs generalization bound quoted in equation (28). Xu and Raginsky, 2017, pp. 6–7, 13
The goal is Corollary 2. If is countable, , achieves the minimum population risk, and , then
The first excess term reflects the prior mass on a population-risk minimizer; the second is controlled by sample size and inverse temperature. The target keeps the infimum over the whole hypothesis space and the constants of equation (29). Xu and Raginsky, 2017, p. 7
Corollary 2 gives a quantitative way to choose a prior and temperature: a prior that puts more mass on a good hypothesis reduces the logarithmic term, while changing changes both terms in opposite directions. It also connects the optimization characterization of a randomized algorithm to the population risk that matters for learning. Without the empirical-risk comparison and the separate generalization estimate, optimizing the training objective alone would not give this population statement. Xu and Raginsky, 2017, pp. 6–7, 13
The cited paper proves Corollary 2 and Theorem 5; the present task is to supply machine-checked proofs of their faithful Lean statements. The Donsker–Varadhan inequality and a tilted-measure identity are already published and proved on the platform, and the basic sample-law and risk definitions are already published. The Gibbs optimization, the Appendix D comparisons, and the quoted bound (28) are posed here as new targets. This work would leave reusable definitions for randomized learning kernels, their Gibbs specialization, and objectives with potentially infinite divergence.
The Gibbs rule is defined separately at every sample, but a learning algorithm must be a measurable kernel on the entire sample space. Establishing the normalized density pointwise does not by itself establish this kernel property. The relaxed objective also combines an integral of empirical risk with a conditional divergence, either of which can be infinite before bounded-loss assumptions are imposed. Equation (28), which the paper attributes to earlier work, needs a sharp constant; the looser information bound discussed immediately before it has a different dependence on . These are separate mathematical obligations even though the final displayed inequality is short. Xu and Raginsky, 2017, pp. 6–7, 13
The Lean development represents a sample as Fin n → Z, its law as Measure.pi, and a randomized learner as Kernel (Fin n → Z) W. Population and empirical risks come from the published LearnStability.Characterization.Setting definition. The Gibbs kernel is built by a normalized density over the probability prior ; Theorem 5 explicitly asserts it is a Markov kernel. The relaxed objective takes values in , so an infinite KL cost is not lost through real conversion. Generalization error remains the real expectation of the population-risk minus empirical-risk difference. The stated loss bounds ensure those real expectations are meaningful in the bounded-loss results.
The paper assumes a nonnegative loss in its general setting and requires for the later bounds. The Lean statements add joint measurability of and explicitly. Corollary 2 also makes the named minimizer's defining property and positive prior mass explicit: countability alone does not ensure an attained infimum, and a zero prior mass makes the printed logarithmic bound infinite. Theorem 5 retains its general measurable hypothesis space and nonnegative loss; countability appears only where the paper invokes it. Theorem 5 states optimality over all Markov kernels, the displayed Gibbs formula, and, for each sample, uniqueness of the Gibbs distribution as the minimizer of the samplewise problem (C.12) of Appendix C. The goal concerns the Gibbs kernel's actual population risk, rather than only the existence of a minimizer of the relaxed objective.
Useful contributions include probability-kernel measurability, control of conditional divergence and its finite conversions, the fixed-hypothesis comparison, and the sharp bounded-loss generalization estimate. The point-mass KL identity and the extended objective can be reused in other Gibbs and PAC-Bayesian formalizations. Xu and Raginsky, 2017, pp. 2, 6–7, 13
Large optimization models often split their variables into blocks that can be handled separately. A method can then solve one smaller approximation problem per iteration instead of the full problem. The block successive convex approximation (BSCA) method of Razaviyayn, Hong and Luo allows the block approximation to guide the search without requiring it to be a global upper bound on the original objective. This matters when an upper bound is awkward to construct but a locally accurate convex model is available. The question is what such a run can approach: a small objective value by itself does not certify first-order optimality.
The paper develops this result after its successive upper-bound minimization methods. Theorem 4 of the pinned preprint gives the limit-point guarantee for BSCA with an Armijo step search. The mission records that result and the numbered relations (31)–(34) and (39) that organize the argument, using the 2012 preprint as the sole source for statement indices and page numbers.
The decision vector is a block vector , with block in a nonempty, closed, convex set . The feasible set is . A continuously differentiable objective assigns each feasible vector a real value. A point is stationary when for every direction whose full step lies in . For a smooth objective, is the derivative of in direction .
For block , the function approximates the objective as the trial block varies around a current point . Its directional derivative at agrees with the objective derivative in the corresponding one-block direction, as in equation (30). Each is strictly convex on , and varies continuously with its trial block and feasible base point. Strict convexity is a condition in the trial block for each fixed ; it does not say that is jointly convex in both arguments.
At iteration , a cyclic schedule chooses one block . A minimizer of over replaces that block in ; all other blocks of equal those of . The search direction is . With and an initial trial length , the Armijo rule chooses the largest member of satisfying
then sets . The selected minimizer can be any one of the block minimizers; the definition does not prescribe a hidden tie-breaking rule.
The first targets identify descent and line-search existence. Equation (31) says the chosen block direction has a nonpositive derivative. Equation (32) says a strict descent direction admits a trial index. The later milestones state the vanishing scaled derivative (33), a subsequence with vanishing search directions (34), and limiting block optimality following (39).
The goal is Theorem 4: for every limit point of the sequence generated by cyclic BSCA,
This is a limit-point assertion. It does not assert convergence of the entire iterate sequence, a convergence rate, or global optimality of a stationary point.
Theorem 4 identifies what an accumulation point of BSCA must satisfy even though its block models need only local first-order agreement rather than global upper bounds. In a nonconvex problem, stationarity is a meaningful first-order conclusion but need not be a global minimum. The exact role of the step search is important: accepting some Armijo step gives decrease, whereas the theorem's limit-point claim uses the largest acceptable member of the geometric trial sequence.
This mission asks solvers to supply machine-checked proofs for a known paper theorem and its stated supporting relations. The draft statements compile as open theorems; they are not proofs. The reusable output includes a block run predicate, an explicit first-order agreement predicate, and a bridge between feasible-direction stationarity and an extended-real objective on the full block space. These objects also make subsequent variants of cyclic block methods easier to state precisely.
A simple decrease argument shows that objective values do not increase, but the accepted step sizes may approach zero. Therefore decrease alone does not imply or that a limit point minimizes every block model. The paper's key limit statement singles out a convergent subsequence on which a fixed block is updated and finds a further subsequence with vanishing directions. Passing block optimality to the limit then requires continuity of the approximation and feasible limit points. The cyclic schedule is needed to cover all blocks, while first-order agreement turns block optimality into stationarity for the original smooth objective.
Lean uses the published TsengBCD.Stationary.X for the finite product of Euclidean block spaces, its extended-real lower directional derivative, and its stationary-point predicate. The product has the sup norm rather than the paper's Euclidean product norm; in finite dimension the notions of convergence used here agree. Blocks and iterations are indexed from zero. The paper's cyclic choice is reindexed so the step from to updates block . The existence of the schedule already rules out zero blocks.
The objective is a real function on the full block space, with ContDiff ℝ 1 expressing the paper's continuous differentiability. This makes the Fréchet derivative used in the Armijo test equal to the paper's lower directional derivative at the points in question. For stationarity, the objective is extended by outside , so infeasible directions cannot silently become admissible. The approximation derivative remains extended-real because the paper assumes only convexity for that function. ContinuousOn is taken on the product of a feasible trial block and a feasible base point.
Two points are explicit in the formalization. First, ensures that a convex combination of and stays in ; the paper prints only positivity. Whether Theorem 4 holds without this restriction under a different global interpretation of and remains a separate question. Second, Figure 4 mixes and in the approximation, direction, and update lines. The run follows the adjacent prose and proof, all of which construct the direction at the current iterate. For (33), the existence of a limit point makes explicit the proof's standing situation and gives the decreasing objective a finite limit. An arbitrary unrelated sequence, an Armijo step that is not the largest accepted trial, or an objective extension that gives a default zero derivative off is outside this scope.
The remaining proof work includes feasibility of every iterate, first-order agreement along the selected block, the Armijo existence statement, the subsequence claim, passage of block minimization to the limit, and the final stationary-point equivalence. The finite-dimensional convex analysis and topology involved are reusable beyond this one algorithm.
Let be an -dimensional vector space over the finite field . Viewed over the subfield , has dimension , and its one-dimensional -subspaces form the Desarguesian spread. An -subspace of is scattered if it meets every element of this spread in an -subspace of dimension at most one. Scattered subspaces define scattered -linear sets in . Through these linear sets they are connected to projective two-weight codes, strongly regular graphs and maximum rank distance (MRD) codes. In 2000 Blokhuis and Lavrauw proved that a scattered subspace has dimension at most , and a sequence of papers showed that this bound is attained whenever .
Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590v2; Combinatorica 41, 2021) replace the one-dimensional spread elements by all -dimensional -subspaces. This gives a hierarchy of conditions, the -scattered subspaces, that refines the scattered case. For and dimension these subspaces had already been identified with -linear MRD codes by Sheekey and Van de Voorde. This mission formalizes the paper's main theorem, the dimension bound for -scattered subspaces.
Timeline.
Let be finite fields, so , and let be a vector space over of dimension . Every -subspace of is also an -subspace. For an -subspace of , denotes its -span.
Definition 1.1. Let . An -subspace of is -scattered if and every -dimensional -subspace of satisfies . In Lean this is HScattered.Bound.IsHScattered F K h U, with F , K , and = Module.finrank K V.
An -subspace defines a subgeometry of if some -basis of is also an -basis of (HScattered.Construction.DefinesSubgeometry F K U, a definition shared with the other missions of this series). In coordinates, is then inside .
A rank distance code of , , is a set of -linear maps from an -dimensional to an -dimensional -space, with distance .
If is an -scattered -subspace of , then either , defines a subgeometry and is -scattered, or
The disjunction is inclusive. The statement holds for every in the range , including .
The result. Theorem 2.3 is the upper end of the theory of -scattered subspaces. It shows that the bound decreases with : a stronger intersection condition forces a smaller subspace. Every subspace reaching the bound is a maximum -scattered subspace. The rest of the paper builds on such subspaces. Its constructions show the bound is sharp when . Its intersection numbers with hyperplanes lie in . Its Delsarte-type duality sends maximum -scattered subspaces to maximum -scattered ones. Each of these statements presupposes the bound. For , the bound is the geometric counterpart of the Singleton bound for MRD codes.
Formalizing it. The theorem is proved in the paper; it has no machine-checked proof. A formalization would provide a Lean model of -scattered subspaces over a field tower and a rank-metric Singleton bound, and the bound itself as a reusable lemma for the companion missions on constructions, hyperplane intersections and duality. The case is attributed in the paper to Blokhuis–Lavrauw and is not reproved there, so a complete formal proof must also supply that case.
The obvious approach is to count. Every -dimensional -subspace meets in at most vectors. But these subspaces overlap heavily, and a double count of incidences between vectors of and -dimensional subspaces does not produce a bound of the form . The -scattered condition must be used on subspaces of every dimension at once, which is the content of Proposition 2.1. The argument for does not carry over directly either: the paper treats , with , and as separate cases. The case rests on a coding-theoretic input (Result 4.6), and the middle case needs auxiliary subspaces whose existence (Lemma 2.2) holds only when .
F, K with [Algebra F K]. is a finite-dimensional K-module with a compatible F-module structure ([IsScalarTower F K V]). The parameters are = Fintype.card F, = Module.finrank F K and = Module.finrank K V.Submodule F V and -subspaces are Submodule K V. The intersection is S.restrictScalars F ⊓ U.IsHScattered.Finset of linear maps. The minimum distance enters as a lower bound on all pairwise rank distances, with .Ruling out trivial readings. Without the range , every spanning subspace would be "-scattered" for , and of dimension would refute the goal. Without the spanning condition, would satisfy the bound vacuously. Both conditions are part of the definition, and the goal is the inclusive disjunction for every -scattered .
Cited inputs. Result 4.6 is Delsarte's theorem [13], numbered in this paper and posed here with sorry. The case of the goal is the Blokhuis–Lavrauw bound [4], which the paper cites without proof and says can be obtained by adapting its argument (Zullo's thesis [30]). It is not an item: a complete proof of the goal must cover it.
Infrastructure. A proof needs: dimension arithmetic for restriction of scalars in a tower; the rank–nullity theorem for -linear maps; the count of roots of a -polynomial , for Lemma 2.2; and a rank-metric Singleton bound. The Singleton bound and Lemma 2.2 are reusable beyond this mission. Contributions are welcome on any milestone, on the case, and on the reduction for .
Peaceman–Rachford splitting separates the minimization of a sum into two proximal computations. That matters when each summand has a tractable proximal map but the sum does not. Douglas–Rachford splitting is its half-relaxed instance, and related iterations appear in the analysis of ADMM. Davis and Yin study how regularity of the two summands changes the rate at which a relaxed Peaceman–Rachford iteration approaches a fixed point. Their Section 4 distinguishes two arrangements: one summand may carry both strong convexity and a Lipschitz gradient, or the two properties may be shared between summands. The mixed case of Theorem 4.3 is the target of this mission. The authors describe it as a new result in the preprint version used here. Davis and Yin, §4, pp. 13–16.
Let be a real Hilbert space and let be proper, closed, convex functions. For a step size , the proximal map takes a point to the minimizer of ; define similarly. The reflection associated with a proximal map is . The Peaceman–Rachford operator is . Its relaxed iteration, Algorithm 1 of the paper, is
The analysis fixes a point satisfying and writes . It also uses the two proximal points and . Their selected proximal subgradients are and . Lemma 1.1 states that they belong to the respective convex subdifferentials and relates them to the iteration. These are selected subgradients, rather than arbitrary members of a set-valued subdifferential. Davis and Yin, §1.2 and Lemma 1.1, pp. 4–7.
A function is -strongly convex when its convexity inequality improves by the quadratic term . A -Lipschitz gradient means the function is real valued, differentiable, and , with . Section 1.10 also permits the parameters and to be zero when a property is unavailable. Its auxiliary term is the maximum of a squared-point-distance term weighted by and a squared-selected-subgradient-distance term weighted by . The one-step bound (2.1) controls the sum of the corresponding terms for and . Davis and Yin, (1.13)–(1.14) and (2.1), pp. 7–8.
Suppose . The goal covers both arrangements: is -strongly convex while has a -Lipschitz gradient, and the arrangement with and exchanged. In either case the target is
The factor is the paper's explicit factor, for . It is strictly below one for with fixed positive regularity parameters; at it equals one. A uniform geometric rate therefore requires relaxation parameters to remain in a range where these factors have a uniform upper bound below one. Davis and Yin, Theorem 4.3, p. 16.
Theorems 4.1 and 4.2 give the explicit factors when , or respectively , supplies both properties. Proposition 4.1 translates a fixed-point contraction sequence into bounds on the proximal points, selected subgradients, fixed-point residual, and objective error. These are companion items in the proposal. The milestone list follows Lemma 1.1, the auxiliary bound (2.1), and the displayed estimates (4.6) and (4.7) from the proof of the mixed case. Davis and Yin, Proposition 4.1 and Theorems 4.1–4.3, pp. 13–16.
Theorem 4.3 identifies a rate available when neither summand alone carries both regularity properties. The explicit dependence on , , , and lets a reader compare choices of step size and relaxation without hiding them in an unspecified constant. Proposition 4.1 explains what a contraction in the auxiliary fixed-point variable says about the quantities used to judge an optimization method: proximal point error, residual, and objective error. The distinction between a per-step bound and a uniform geometric rate is part of the mathematical result.
The inequalities are proved in the source paper; the remaining work here is to give their statements and eventual proofs a machine-checked account. The shared setting makes the proximal operator, selected subgradients, and regularity terms explicit, so the same formal definitions can be used across this mission's estimates. The two external platform definitions cited by this development already provide the closed proper convex class, proximal-map predicate, smooth convex class, and subdifferential. The results in this proposal are open Lean statements until solvers supply proofs.
Strong convexity and Lipschitz smoothness control different quantities in the mixed case. The decrease inequality directly bounds distances between proximal points and between gradients, whereas the desired conclusion concerns . Treating merely as a nonexpansive operator yields no factor below one. The displayed estimate (4.7) expresses the fixed-point distance through the quantities controlled by (4.6). The proof must also identify the proximal subgradient of the smooth summand with its ordinary gradient, rather than assume that identity as part of the goal. Davis and Yin, proof of Theorem 4.3, p. 16.
The Lean carrier is a complete real inner-product space, including the zero space. The functions take values in EReal to represent outside their effective domains. The published IsProperClosedConvex, IsProx, IsSmoothConvex, and subgrad definitions supply the common function and operator conventions. A proximal map is passed as a function together with a proof that it minimizes the defining objective; under the standing assumptions it is uniquely determined. Every result involving a proximal map assumes . Run statements require , and the mixed theorem requires . The goal has no hypothesis asserting any of its decrease estimates or a contraction; those are results to establish.
The contraction factors use Real.sqrt. For the mixed and -regular factors, the radicands are positive throughout the relaxation range. For the -regular factor, its nonnegativity follows from the compatibility of positive strong convexity and gradient Lipschitz parameters on a nonzero space; the zero space makes the contraction statement trivial even if that radicand is negative. Objective errors use real values only at proximal points where both summands are finite. The milestone (2.1) uses the paper's selected proximal subgradients. Proving the link between smooth gradients and those subgradients, and reusable proximal-map inequalities, are welcome contributions beyond the four named milestones.
Many large optimization problems in signal processing, statistics and machine learning have a variable that splits naturally into blocks, and are solved by updating one block at a time. The classical method of this kind, block coordinate descent (BCD), minimises the objective exactly in one block while the others are held fixed. In practice the exact block subproblem is often too expensive, and one minimises instead a simpler function that upper-bounds the objective and touches it at the current point. The EM algorithm, DC (difference of convex) programming, proximal and linearised block updates and several alternating schemes for matrix factorisation and transceiver design are all of this form.
Razaviyayn, Hong and Luo (arXiv:1209.2385, SIAM J. Optim. 23 (2013)) gave one convergence analysis for this whole family, the block successive upper-bound minimization (BSUM) method, without convexity or smoothness of the objective. This mission formalizes the block part of that analysis: the cyclic BSUM method (Theorem 2) and its maximum-improvement variant MISUM (Theorem 3).
Timeline. Bertsekas (Nonlinear Programming, 1999, Prop. 2.7.1) proved that limit points of cyclic BCD are stationary for continuously differentiable objectives over a product of closed convex sets when each block minimiser is unique. Tseng (J. Optim. Theory Appl. 109, 2001) treated nondifferentiable objectives using regularity and coordinatewise minima. Chen, He, Li and Zhang (SIAM J. Optim. 22, 2012) introduced maximum block improvement, which drops the uniqueness assumption. The 2013 paper extends these results from exact block minimisation of to minimisation of block upper bounds.
The problem is
where each is a closed convex set and is a continuous real function on . A point is with . The directional derivative is , a value in . A point is stationary for (12) if for every with . The function is regular at if holds for every such that for every block . A point is coordinatewise stationary if for every with , for every .
For each block an approximation function is given, with and . Assumption 2 requires:
The BSUM algorithm (Fig. 2) starts at and, at each iteration, picks a block by the cyclic rule, replaces by any minimiser of over , and keeps the other blocks. The MISUM algorithm (Fig. 3) instead updates a block attaining .
If each is quasi-convex in , Assumption 2 holds and every block subproblem , , has a unique solution, then every limit point of the cyclic BSUM iterates satisfies
and is a stationary point of (12) if is regular at .
The proof passes through the monotonicity (14); the limit at a limit point (15); the claim that forces ; block minimality for all and every ; and the first-order condition for feasible (22).
Theorem 2(b): if the level set is compact, block minimisers are unique in at least blocks and is regular on , then , where is the set of stationary points. Theorem 3: under Assumption 2 alone, every limit point of the MISUM iterates is coordinatewise stationary, and stationary where is regular.
Theorem 2 is the stationarity guarantee for every method that can be written as cyclic block minimisation of tight upper bounds: block EM, alternating DC iterations, proximal block updates, and the matrix-factorisation and beamforming schemes of Section VIII of the paper. Each such method needs only a check of (B1)–(B4) to inherit it. Theorem 3 shows that the uniqueness assumption, which part (a) needs and BCD needs too, can be traded for a greedy block choice.
The results are proved in the paper. As far as the platform's catalogue shows, none of them has been formalized; the related published work is the formalization of Tseng's 2001 setting (directional derivative, stationarity, regularity, cyclic rule), which this mission reuses. Formalizing the analysis checks the "without loss of generality" and "by further restricting to a subsequence" steps, which carry most of the argument, and gives reusable statements about limit points of block methods.
The obvious argument shows that decreases and that a limit point satisfies the block optimality condition for the block updated along the convergent subsequence. It does not say anything about the other blocks: consecutive iterates may stay a fixed distance apart, so the next iterate need not converge to , and then nothing is known about in the next block. Showing that is the central step, and it is exactly where quasi-convexity and uniqueness of the block minimisers are used. Without uniqueness, limit points of even exact cyclic BCD need not be stationary (Powell's examples, which the paper cites), which is why Theorem 2(b) needs compactness and Theorem 3 needs a different update rule.
The step from block minimality to stationarity is a second gap: (B3) only matches derivatives in coordinate directions, and passing to all directions requires regularity of .
The space is the dependent product X n of the referenced Tseng setting, with blocks indexed (paper block is index ). It carries the sup norm over blocks, which matters only for distances; convergence statements do not depend on the norm. The block sets are closed and convex, is a real function continuous on , and ; these standing hypotheses of Section IV appear in every statement.
The paper assumes . Accordingly is extended by off , and stationarity and regularity are those of the extension. Directional derivatives are extended-real liminfs, never real-valued limits with a junk value. A run is a predicate on a sequence: each new block is a minimiser of the block subproblem, but existence of minimisers is not assumed. The cyclic rule updates block on the step , a relabelling of Fig. 2's . Limit points are cluster points of the sequence.
Deviations from the printed statements, each disclosed in the items:
Trivializing formalizations are ruled out: hypotheses on are required on all of , not just along the run; uniqueness is required at every ; and a sorry-free check shows that all hypotheses of Theorem 2(a) hold together for a one-block instance.
Not formalized: Proposition 2 (a sufficient condition for (B3)), Corollaries 2 and 3 (essentially cyclic and overlapping rules) and the applications of Section VIII. Contributions of reusable lemmas about cluster points of block methods and first-order conditions for constrained minimisers in a single block are welcome.
Manufacturers increasingly sell directly to consumers through their own stores and websites, alongside the independent retailers that carry their products. This practice is called supply chain encroachment. Retailers routinely resent it, and examples range from beer brewers to personal computers. Arya, Mittendorf and Sappington (Marketing Science, 2007) showed that, when product quality is fixed, encroachment can benefit the retailer too: the manufacturer lowers the wholesale price to keep the retailer channel competitive, and this wholesale price effect can outweigh the lost sales.
Ha, Long and Nasiry (Manufacturing & Service Operations Management, 2016; authors' manuscript SSRN 3970373) ask what changes when the manufacturer also chooses product quality. Their first result, formalized in this mission, is that the win–win outcome disappears: with endogenous quality and a single product sold in both channels, encroachment always helps the manufacturer and always hurts the retailer.
Consumers have a quality sensitivity uniformly distributed on , and a consumer who buys a product of quality at price obtains surplus . When one product of quality is sold in total quantity , the market-clearing price is . The manufacturer's unit production cost for quality is , with the cost of quality. Selling one unit through her own direct channel costs her an additional ; the retailer's selling cost is .
Benchmark (no direct channel). The manufacturer chooses a wholesale price and a quality ; after observing them the retailer orders . The profits are
Encroachment with uniform quality. The game has three stages and perfect information:
Both channels sell the same product at the price , so
The solution concept is subgame perfect equilibrium: at every decision node, on or off the equilibrium path, the mover's rule picks a feasible action that no feasible alternative beats. The manufacturer encroaches when on the equilibrium path.
In the Lean development these are the structures Outcome and Profile, the payoffs retailerPayoff and mfrPayoff k c, and the predicate IsSPE k c σ of the definition QualityEncroach.Uniform.Game, with the benchmark counterparts BenchProfile and IsBenchSPE k τ.
In the benchmark, every equilibrium has and profits , . The goal states that, for every , and every subgame perfect equilibrium of the encroachment game in which the manufacturer encroaches,
The statement fixes no threshold value, and it holds for every equilibrium.
The milestones follow the paper's backward induction:
The mission also contains:
The result separates two regimes that look alike. With quality fixed, a retailer facing an encroaching manufacturer is better off exactly when condition (6) holds. With quality chosen by the manufacturer, that region disappears. The manufacturer distorts quality, upward when is small and downward when it is large, and so relies less on the wholesale price to steer the retailer's order. The retailer then loses in every equilibrium in which encroachment occurs. The paper's later sections (quality differentiation, a fixed cost of quality, no quality commitment, a general cost function) all measure against this base case.
The result is proved on paper, by backward induction with closed-form profits, an envelope-theorem convexity argument in , and a numerically located threshold . None of it is formalized. A machine-checked proof would certify:
Each step of the backward induction is a one-variable concave problem, but the steps do not compose into a single smooth problem. The retailer's best order depends on whether his order leaves room for direct sales. As a result the manufacturer's profit given is the piecewise function . Its middle piece describes a retailer who orders exactly enough to keep the manufacturer out, and that piece is not a stationary point of anything. The global optimum over switches between the first piece and the other two at a threshold that the paper locates only numerically.
The goal compares the optimum of this piecewise problem with a constant, for every equilibrium. The natural first idea, comparing the reduced profits with the benchmark ones pointwise in , does not work for the retailer: for a fixed quality his encroachment profit exceeds the benchmark profit on part of the range, which is exactly condition (6). The comparison has to use the quality the manufacturer actually chooses, and that quality is known only through the case analysis above.
All quantities are real numbers. The following conventions are fixed:
Subgame perfection is written in one-shot-deviation form at every history, which in this three-stage game with perfect information is subgame perfection. It constrains the retailer's rule at every and the manufacturer's stage-3 rule at every , not only on the path.
The benchmark profits in the goal are the paper's constants and . The milestone benchmark_equilibrium proves that a benchmark equilibrium exists and that these are its profits.
Two formalizations would trivialize the goal, and both are ruled out:
The encroachment threshold of Proposition 1(i) is stated in both directions, with chosen before . The boundary point is left open, because the paper's statements disagree there.
The closed forms , , , , , , , , , and are definitions that cite their page. Every statement that uses one with in a denominator assumes .
A complete development needs:
The game definitions are reusable for the other missions of this series, which keep this cost structure. Proofs of any milestone are welcome, as are alternative arguments for the goal that bypass the threshold computation.
Best subset selection with ridge shrinkage, the -regularized least squares problem
is a mixed integer program. Exact solvers for it rely on branch-and-bound: at every node of the search tree a convex relaxation is solved, and the node is discarded if a lower bound on that relaxation already exceeds the best objective value found so far. Hazimeh, Mazumder and Saab (arXiv:2004.06152v2, Mathematical Programming 2022) build such a solver, L0BnB, for instances with in the millions. Its relaxations are solved only approximately, by first-order methods, and an approximate primal solution does not by itself certify a lower bound. The bound has to come from a dual feasible point. Theorem 2 of the paper supplies the duals of the node relaxation in closed form, together with explicit formulas for the optimal dual variables as functions of the primal optimum. Everything the paper later proves about the quality of its dual bounds (Section 3.2, Theorem 3) starts from these formulas.
Data are a matrix with columns , a response , and parameters , where bounds the coefficients. Write and . The reverse Huber penalty is for and for . Define
and let if and if . The reduced relaxation (5) is
By Theorem 1 of the paper it is the interval relaxation of the perspective formulation, projected onto .
The two dual objectives of Theorem 2 are, for and ,
where is maximized over all of (problem (20)) and subject to for (problem (22)). For an optimal of (5), with residual , the candidate dual variables are
In the Lean development these objects are F, box, h1, v, h2, Feas22, alphaStar, gammaStar, rhoStar, muStar in the namespace L0BnB.Duality.
Let minimize over .
This is "(20), respectively (22), is a dual of (5), and (23), respectively (24), are optimal dual variables", with the paper's remark that strong duality holds.
The result. Theorem 2 turns the node relaxation of L0BnB into a pair of explicit concave maximization problems, one per regime of versus . The dual (20) is unconstrained, so any gives a valid lower bound; the paper's dual bounds (25)–(28) evaluate or at built from an inexact primal solution , with the remaining variable chosen in closed form. The formulas (23)–(24) explain why this choice is right: at the exact optimum it recovers the primal value. Theorem 3 of the paper, which bounds the loss of this dual bound by a quantity depending on the support size rather than on , compares to term by term and therefore depends on (23).
Formalizing it. The paper proves the case in Appendix A and omits the proof of the case ("follows along the lines similar to what was shown above"). The appendix also contains an intermediate formula for the coordinate minimum, , that is incorrect when is large; the final dual (49) = (20) is nevertheless correct. A machine-checked proof supplies the omitted case and settles the correct statement. To our knowledge neither half has been formalized.
The dual objective (20) hides the box constraint inside the term and the penalty inside , and the reverse Huber penalty is piecewise, so even the weak-duality half has to handle both pieces of and the junction . The attainment half is where the work lies: it needs the optimality conditions of a nonsmooth convex problem over a box, at coordinates where (where is not differentiable), where (where the box is active), and where both may interact with the regime boundary . The natural first idea, to read (23) off the Lagrangian derivation in the paper, does not yield a proof: that derivation assumes a dual optimum exists and relates it to by complementary slackness, whereas the theorem asserts an identity for the explicit built from alone.
Data are X : Matrix (Fin n) (Fin p) ℝ, y : Fin n → ℝ and reals lam0 lam2 M with 0 < lam0, 0 < lam2, 0 < M as hypotheses; is Fin p. Norms and inner products are explicit sums: , , , , and is for every . The regime split is written versus . sign is Real.sign, with ; where it is evaluated in (23) the argument is nonzero at an optimum. The optimal solution is a hypothesis (feasible and minimizing over the box); its existence is not part of the statements. The coordinate milestones (45) and (47) are stated for a scalar standing for and a multiplier . No normalization of or is assumed: the unit-norm convention that opens Section 3 is not used by Theorem 2. The paper writes no in these results, so no constants are instantiated.
"A dual is given by" is formalized as weak duality over all dual-feasible points together with equality at the explicit dual variables. Weak duality alone would not be Theorem 2, and neither would the equality alone; the goal requires both in both regimes. Uniqueness of the dual optimum is not claimed.
A complete development needs elementary convex analysis of the scalar penalty (its conjugate and subdifferential), first-order optimality conditions for a convex function over a box in , and finite-sum bookkeeping. The scalar facts about the reverse Huber penalty are reusable in the companion missions on the reduced relaxation and on dual-bound quality. Contributions to any milestone, or a direct proof of the goal, are welcome.
Minimizing a convex function on a real Hilbert space by first-order methods has a continuous-time counterpart: second-order differential equations whose trajectories descend . Su, Boyd and Candès (20) showed that Nesterov's accelerated gradient method is a discretization of with , along which . Two modifications of this equation have been studied separately because each adds a property the plain system lacks.
Boţ, Csetnek and László (arXiv:1911.12845v2, 2020) combine both terms and ask which properties of the two parent systems survive. This mission covers the first of their answers: when decays fast enough, the fast rates and the weak convergence of trajectories are preserved.
Timeline. 2016 (published 2018): weak convergence of trajectories of for (Attouch, Chbani, Peypouquet, Redont, Math. Program. 168). 2016: the same with Hessian-driven damping, (Attouch, Peypouquet, Redont). 2018: Tikhonov regularization of that system, with the rate kept and strong convergence to the minimum-norm minimizer under slow decay of (Attouch, Chbani, Riahi). 2020: both terms together (Boţ, Csetnek, László, this paper).
Fix a real Hilbert space , a starting time , parameters and , and initial data . The General assumption of the paper is:
The dynamical system is
A global -solution is a twice continuously differentiable satisfying (5) for every . The decay of is controlled by together with one of two conditions:
A curve converges weakly to if for every . The Lean development lives in the namespace TikhonovHDD.Weak, with IsSolution, GenAssumptionG, GenAssumptionEps, CondA, CondB, argmin, minVal and WeakTendstoAtTop for these objects.
Under the General assumption, and (a) or (b), if then every global -solution of (5) satisfies
In the order the argument uses them:
The result. Theorem 3.5 shows that the Tikhonov term, when it decays at least as fast as requires, does not disturb the asymptotics of the Hessian-damped system: values converge at rate and trajectories converge weakly to a minimizer. With it recovers the corresponding results for the regularized system without Hessian damping, and with those for the Hessian-damped system. It is also the boundary case of the paper's second half, where slower decay of is shown to give strong convergence to the minimum-norm minimizer instead.
Formalizing it. The results are proved in the paper; none of them is machine-checked. A formal development would produce reusable pieces: a Lyapunov-energy analysis of second-order systems with time-dependent coefficients, the asymptotic Lemmas A.2 and A.3, and the bridge from "the distance to every minimizer converges and weak cluster points are minimizers" to weak convergence of a curve (the continuous Opial lemma).
The obvious approach, a single Lyapunov function that decreases along trajectories, fails here: the Tikhonov term makes the natural energy only almost nonincreasing, with an error that must be integrated, and the Hessian term produces a cross term that is controlled only by condition (a) or (b). The step from to and to the existence of cannot be read off a single bounded energy: boundedness of gives rates in , not in , and says nothing directly about . Weak convergence then requires Opial's lemma, which is not in Mathlib in continuous form. Existence of solutions is itself nontrivial in infinite dimension: the right-hand side involves , so the system has to be rewritten as a first-order system before the Cauchy–Lipschitz theorem applies.
InnerProductSpace ℝ H, CompleteSpace H); nothing is finite-dimensional, so weak convergence is genuinely weaker than norm convergence. It is stated through inner products with every ; stating it as norm convergence, or testing only some , would change the theorem.Asymptotics relations at .InertialAVD.Traj.lemma_A_2 (same hypotheses: nonempty, exists for every , every weak sequential limit point lies in ; same conclusion). It is a reference milestone of this mission; its weak convergence InertialAVD.Traj.WeakTendstoAtTop has the same body as TikhonovHDD.Weak.WeakTendstoAtTop.HessianDamping.DINAVD.Setting concerns a different equation (no term) and is not reused.Thompson sampling (TS) chooses each action with the posterior probability that it is optimal. Its practical success in online advertising, recommendation and experimentation raised the question of why it works and when it does not. The tutorial of Russo, Van Roy, Kazerouni, Osband and Wen (Found. Trends Mach. Learn. 11(1), 2018) answers part of that question in §8.1 with an information-theoretic regret bound due to Russo and Van Roy (JMLR 17, 2016). The bound applies to every algorithm, not only TS. It reduces the analysis of a particular algorithm to one quantity, the information ratio: the squared expected regret of a period divided by the information the period yields about the optimal action.
Timeline:
An agent acts in periods . In each period it selects an action from a finite set and observes an outcome from a finite set . An unknown parameter , taking values in a measurable space , has a prior distribution . Given and the action , the outcome is drawn from a probability vector that depends measurably on . The agent receives the reward for a known function . The mean reward of action is
and the optimal action is a measurable selector of . Ties may be broken in any measurable way, and every result holds for every selector.
The history is the list . An algorithm assigns to every history a probability vector over , from which the next action is drawn. The joint law of is , and every expectation below is taken under it. The expected cumulative regret, or Bayesian regret, is
The entropy of the prior distribution of is . The conditional mutual information is the expected information that the period- observation carries about given the past, averaged over the past. The information ratio of period is (8.7):
For every model and every algorithm, every horizon and every with for ,
When every mutual information is positive, the least such is , which is the tutorial's . A companion theorem states that literal form under the positivity hypothesis.
BanditAlgorithm.information_ratio_cumulative_bound_signed. It states the step in the form the proof uses, with the entropy budget as a hypothesis.The result. (8.8) separates the regret analysis of an algorithm into two independent problems. One is a per-period bound on the information ratio, which depends on the structure of the problem and the algorithm. The other is the entropy of the optimal action, which depends only on the prior. Combined with the bound that Russo and Van Roy (2016) prove for TS on -armed bandits, and with , it gives . On the shortest-path problem of p. 76, makes the regret depend on the number of edges and on , not on the exponentially large number of paths. The same inequality is the design criterion of information-directed sampling, which chooses actions to minimise the ratio.
Formalizing it. The bound and its proof are known. The work here is to make the probabilistic model explicit, with a general parameter space, an outcome kernel and randomized algorithms; to formalize the per-period decomposition of the regret and the chain-rule argument behind the entropy budget, which the tutorial cites rather than proves; and to obtain (8.8) for every algorithm in one statement. The Proved platform results for Lattimore and Szepesvári's Bayesian adversarial bandit (Theorem 36.5 and its chain-rule lemmas) are about a different model: one algorithm (TS), the best arm in hindsight of a reward matrix, and the budget . To our knowledge, (8.8) itself has not been formalized.
The Cauchy–Schwarz step is elementary and already proved on the platform. Milestone 1 is bookkeeping: the cumulative regret integrates over histories of length , while the period- term integrates over histories of length , and later periods must be integrated out.
The substance is the entropy budget. The obvious attempt bounds each period's information by , which loses a factor . The bound is uniform in only because the per-period informations telescope: their sum is the information that the whole history carries about , which is at most the entropy of . Each step requires conditional distributions of given histories, where lives in a general measurable space and is integrated against the prior. Zero-probability histories must also be handled consistently with the convention .
InformationTheory.kernel_average_categorical_kl_le_marginal_entropy and its _general variant (average KL to the mixture is at most the mixture's entropy), and the adversarial-bandit lemmas BanditAlgorithm.bayesian_ts_conditional_information_gain_chain_rule and bayesian_history_mutualInformation_endpoint_bound, are related tools. A chain-rule library for this history model would be reusable beyond this mission, for example for information-directed sampling. Proofs of auxiliary lemmas are welcome.The tutorial's argument is on pp. 75–76. The tutorial cites Russo and Van Roy (2016) for the original results, including the entropy budget.
The Kalman filter estimates the hidden state of a linear system from noisy observations. At every step it solves a minimum mean square error (MMSE) estimation problem: given a joint normal distribution of a signal and an observation , find the estimator minimizing . The answer, the conditional mean, is optimal only if the model distribution is correct, and in practice the system matrices and noise covariances are estimated and misspecified.
Shafieezadeh-Abadeh, Nguyen, Kuhn and Mohajerin Esfahani (arXiv:1809.08830, NeurIPS 2018) replace the single model by a set of plausible models: all normal distributions within type-2 Wasserstein distance of a nominal normal distribution. The estimator is then chosen to minimize the worst-case mean square error over this set. Their Theorem 2.5 shows that this robust estimation problem, although posed over an infinite-dimensional space of estimators and a nonconvex set of distributions, has the same value as a finite convex program over covariance matrices, and that the robust estimator is affine. Applied at every time step, this yields the Wasserstein distributionally robust Kalman filter of the paper's §4.
This mission formalizes Theorem 2.5 together with the minimax theorem (Theorem 2.3) and the lemmas of its proof.
Let and . A point of is with signal and observation . A symmetric matrix is partitioned as . () denotes the positive semidefinite (definite) matrices, means , , and is the positive semidefinite square root of .
Normal distributions. is the normal distribution on with mean and covariance ; singular is allowed. is the set of all of them.
Wasserstein distance. For distributions on ,
the infimum ranging over all distributions on with marginals and .
Ambiguity set. Fix , , the nominal distribution and a radius . The Wasserstein ambiguity set is
Robust estimation. Let be the set of all measurable functions . The distributionally robust MMSE problem is
and a distributionally robust MMSE estimator is a attaining the outer infimum. Nature's problem exchanges the two optimizations; a attaining its outer supremum is a least favorable prior.
The finite program. With , program (5) maximizes over (with , ) subject to
is a distributionally robust MMSE estimator. 3. For the same , lies in and is a least favorable prior.
Existence and uniqueness of an optimal are not part of the statement.
The result. Theorem 2.5 gives the robust estimator in closed form from one optimal covariance matrix, and identifies the least favorable distribution as a normal distribution with the nominal mean. Together with Theorem 2.3 it shows that the pair is a saddle point: the robust estimator is the Bayesian estimator for the least favorable prior. For the program has the single feasible point and the estimator reduces to the classical conditional mean, so the theorem contains the Kalman update as a special case. The finite program is what makes the robust filter of §4 computable; the paper's §3 (formalized in the companion mission of this series) solves it with a Frank–Wolfe method.
Formalizing it. The result is proved in the paper; nothing here is open. No part of it is machine-checked yet. The Gelbrich formula for normal distributions (Proposition 2.2) is cited from the literature and has no formal proof in Mathlib; neither does Lemma A.1, cited from earlier work of the same authors. A closely related statement for a Wasserstein ball over all distributions around an elliptical nominal (Kuhn et al. 2019, Theorem 25) is posed on the platform as WassersteinDRO.Shrinkage.distributionally_robust_mmse_estimator; it is a different theorem, since the ambiguity set there is convex and contains non-normal distributions.
The ambiguity set is not convex, because a mixture of normal distributions is generally not normal. The standard route to a minimax equality, Sion's theorem, needs convexity on nature's side and therefore does not apply to (2) directly; the obvious attempt to interchange the infimum and the supremum fails at this step. The space of measurable estimators is infinite-dimensional, and the Wasserstein constraint is an infimum over couplings, so a proof must pass to finite-dimensional descriptions on both sides (means and covariances for , affine maps for ) and justify each passage. The matrix-analytic parts involve the nonlinear map , for which Mathlib has square roots but little calculus.
EuclideanSpace ℝ (Fin n ⊕ Fin m); the Sum.inl coordinates are , the Sum.inr coordinates are , and the blocks of a matrix are toBlocks₁₁, toBlocks₁₂, toBlocks₂₁, toBlocks₂₂.multivariateGaussian c S with S.PosSemidef; only the nominal is required to be positive definite.WassersteinDRO.Shrinkage.wassersteinDistance 2 in . The ambiguity set is defined through it, not through the Gelbrich formula; the formula is Proposition 2.2, a milestone.sdpValue in EReal, and the two are compared through the coercion.A complete development needs the Gelbrich formula for (possibly degenerate) normal distributions, conditional means of jointly normal vectors, a minimax theorem for convex–concave functions on compact sets, Lagrangian duality for a convex semidefinite program, and calculus of the positive semidefinite square root. The first three are reusable well beyond this mission, and contributions of any of them as separate results are welcome.