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.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The second part of Hilbert's 16th problem (Paris, 1900) asks for the maximal number and the relative position of the limit cycles of a planar polynomial differential system
where are real polynomials of degree at most . Smale listed it in 1998 among the mathematical problems for the next century and remarked that, apart from the Riemann hypothesis, it seems the hardest of Hilbert's problems (Smale 1998). Even for it is not known whether the number of limit cycles is uniformly bounded.
J. Llibre's survey Sobre el problema 16 de Hilbert (La Gaceta de la RSME 18 (2015), 543–554) organises the question into seven problems and concentrates on a more tractable restriction: algebraic limit cycles, i.e. limit cycles contained in a real algebraic curve. For this restriction there is an explicit conjecture for the maximal number (Conjecture 1 of the survey, first stated in Llibre–Ramírez–Sadovskaia 2010). This mission formalizes that conjecture as its goal, together with the results of the survey on which it rests.
Timeline (as reported in the survey):
A polynomial vector field is a pair of real polynomials in ; its degree is . A solution is a differentiable curve with for all . A periodic orbit is the image of a non-constant periodic solution. A limit cycle is a periodic orbit that is isolated among periodic orbits: some open set contains no periodic orbit other than .
A limit cycle is algebraic if it is contained in the zero set of a non-zero real polynomial . The algebraic Hilbert number is the supremum, over all polynomial vector fields of degree at most , of the number of algebraic limit cycles (a value in ).
A curve is invariant with cofactor if . A family of irreducible curves is generic if (i) no curve is singular, (ii) the top-degree homogeneous part of each curve is square-free, (iii) distinct curves meet transversally, (iv) no three distinct curves share a point, and (v) the top-degree homogeneous parts of distinct curves are coprime.
The equality asserts both that the number of algebraic limit cycles is bounded by the right-hand side for every field of degree at most , and that the bound is attained.
A proof of the goal would settle Problems 6 and 7 of the survey: it would give a uniform bound, depending only on the degree, for the number of algebraic limit cycles, and identify the sharp value. The conjecture is consistent with every example known to the survey: the generic bound of Theorem 4 is sharp for even , and the known non-generic examples exceed the generic bound only in odd degree and by one. Conjecture 2 () is its first open case.
On the formal side, the milestones require a reusable library of planar dynamics that is currently absent from Mathlib: periodic orbits and limit cycles of planar vector fields, hyperbolicity via the divergence integral, inverse integrating factors, invariant algebraic curves and Darboux-type arguments, and topological configurations of Jordan curves. Theorems 1, 2, 4 and 5, Proposition 3 and the cubic example are proved in the literature but, as far as the proposal author knows, not formalized; the goal and Conjecture 2 are open.
The obvious route bounds the number of ovals of the invariant curve (Harnack's theorem) and relates the degree of the curve to the degree of the field. This fails because a field of degree can have invariant curves of arbitrarily high degree, so no a-priori degree bound on the curve is available; Theorem 4 obtains one only under the genericity conditions (i)–(v), and the degree-3 example shows that non-generic curves behave differently. On the formal side, the dynamical milestones (Theorems 2 and 5, the cubic example) need Poincaré–Bendixson-type planar topology and uniqueness of solutions, which Mathlib does not yet provide.
MvPolynomial (Fin 2) ℝ with variable 0 as and 1 as ; points are ℝ × ℝ. The degree of a field is the maximum of the total degrees of and , and ranges over fields of degree at most , matching equation (1) of the survey.Set.encard values in ℕ∞, so an infinite family is , never silently ; is an iSup in ℕ∞, so the goal also asserts finiteness.HasDerivAt at every real time). A limit cycle is isolated among periodic orbits contained in a neighbourhood. An algebraic limit cycle lies in the zero set of some non-zero polynomial, with no degree restriction on the curve.ℕ∞, not an inequality over a possibly empty family.Contributions welcome: a planar ODE library (uniqueness, flows, Poincaré–Bendixson), Darboux theory of integrability, and proofs of the classical milestones.
A base-stock (order-up-to) policy orders, in every period, exactly enough to bring the inventory position (stock on hand plus stock on order minus backorders) up to a target level. It is the policy used in practice for repairable and consumable service parts, and the analysis of every later chapter of Muckstadt's book assumes it. Its optimality is therefore a foundational question, and there are three classical ways to prove it.
This mission formalizes the third approach, in the finite-horizon single-location form presented in Section 2.2.1 of Muckstadt (2005).
A single item is reviewed in periods . An exogenous, time-homogeneous Markov chain on a finite set is observed at the start of period ; given , the demand has law and is independent of . Excess demand is backordered.
Every unit of demand is a customer, and customers are indexed in arrival order, the initially waiting customers first. A customer's distance is once served, while waiting, and for future customers in the order they will arrive. Units are indexed by location: (used), (on hand), (in transit) and (at the supplier, which holds countably many units). The state is
with the location of unit and the distance of customer . In period : units in transit move one location closer and the released units move from to (so an order is on hand periods later); the demand brings the customers at distances to distance and moves the others steps closer; units on hand serve waiting customers, lowest indices first; then is charged per unit on hand and per waiting customer, with . The criterion is the expected cost over the periods, discounted by .
A policy for the whole system chooses a finite set of units at the supplier to release. It is monotone if it releases lower-indexed units first, and committed if unit only ever serves customer . The subsystem is unit with customer under commitment, with state and actions Release and Hold. The set contains the optimal actions of a subsystem whose unit is at the supplier and whose customer is at distance , and the critical distance is
Every policy that, in each period and Markov state , releases the lowest-indexed units at the supplier to raise the inventory position to
is optimal for among all policies, from every starting state. Such a policy exists. The levels are not fixed numbers but the critical distances of the single-unit problem, so the goal asserts the structure of an optimal policy and identifies its levels, without committing to any constant.
and managing every subsystem independently and optimally is optimal for . 3. Lemma 2 (p. 28): implies . 4. Section 2.2.1.2.2 (p. 29): the critical distance policy, release if and only if , is optimal for every subsystem.
The result shows that under Markov-modulated demand a single-location system is optimally run by a state-dependent base-stock policy. The same unit–customer argument gives echelon base-stock optimality in serial systems with noncrossing stochastic lead times (Sections 2.2.2–2.2.3). The decomposition also yields the levels themselves: they are the critical distances of a two-action problem, which can be solved one customer at a time.
The theorems are proved in the literature (Muharremoglu and Tsitsiklis 2008) and in the book. To our knowledge no machine-checked proof of any base-stock optimality theorem exists, by dynamic programming or by decomposition. The book's proof is informal in three places a formalization has to settle:
A formal development makes each of these precise.
The obvious argument says that costs are linear, so the cost of is the sum of unit–customer costs and everything decouples. That is only half of Theorem 4. The pairing of unit with customer holds only under monotone policies, and a general policy for observes the whole infinite state , not just . The lower bound therefore needs Lemma 1 together with the fact that extra information about the demand history does not help a Markov decision problem. The upper bound needs the lowest-index matching to cost no more than committed matching.
The second difficulty is that the threshold structure is not the obvious consequence of Lemma 2. The set of distances at which releasing is optimal must be shown to be an initial segment when ties are allowed. Unbounded demand makes that set possibly unbounded (it is, in the last periods). Finally, the release decisions of the subsystems must be counted to recover an inventory position, which uses the invariant that future customers occupy consecutive distances.
Everything is in the namespace ServiceParts.UnitDecomp, with three definition files.
Model. Model bundles the chain, the demand law, , , and with the standing assumptions , , , together with the per-unit and per-customer motions and a generic finite-horizon expected-cost recursion. Costs are in .
Subsystem. Subsystem defines a subsystem, its optimal cost, , and the critical distance policy.
System. System defines with lowest-index matching, its policies (finite release sets), monotone and committed policies, starting states, the inventory position and the order-up-to release.
Conventions and pinnings:
Corrections to the book:
Out of scope: stochastic noncrossing lead times (Section 2.2.2), serial systems (Section 2.2.3; compare the disproved platform statement SupplyChainTheory.clark_scarf_sequential), and continuous review (Section 2.2.4, which the book calls intuitive).
Proofs of any milestone are welcome. A reusable by-product would be a general lemma that Markov policies are optimal among history-dependent ones for finite-horizon problems with countable randomness and costs in .
The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission extends the best possible constant for complex diagonal matrices from to every real . The result is proved in Lean. The constant and its formula are unchanged from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. For each exponent, it works for every triple of diagonal matrices, whatever their size, and no smaller constant does.
The mission started from a supplied pen-and-paper proof. Lowering the cutoff took more than replacing 256 with 90: several estimates in the original argument had to be strengthened. The research note proves the bound for real entries first, then transfers it to complex entries and shows that the constant cannot be improved. The goal theorem below gives the exact formula and statement.
This is the second step of the sharp diagonal Hlawka campaign, and it reuses the foundation's definitions and supporting results. The campaign invites further improvements below 90, keeping the same formula.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryA Markov chain Monte Carlo sampler is often assembled from simpler parts. A practitioner who has several proposal mechanisms for a Metropolis–Hastings sampler can combine them in two ways. Either each drives its own Metropolis–Hastings kernel and the sampler picks kernel with probability at each step, or the mixture is used as a single proposal inside one Metropolis–Hastings kernel. Both samplers leave the target invariant, so the choice is about efficiency.
Section 4 of Tierney (1998) settles the comparison: when both samplers use the maximal acceptance probability, the second never does worse in terms of asymptotic variances of sample-path averages. The statement that carries this is Proposition 5, an ordering of kernels in Peskun's off-diagonal order; the variance comparison then follows from Theorem 4 of the same paper, the general-state-space extension of Peskun (1973).
Timeline. Peskun (1973) introduced off-diagonal domination for finite state spaces and showed that the Metropolis–Hastings acceptance probability is maximal in that order. A version of Proposition 5 for discrete chains appears in the appendix of Tierney (1991) and in the rejoinder of Besag, Green, Higdon and Mengersen (1995). Tierney (1998) states and proves it for general state spaces, using the measure-theoretic description of Metropolis–Hastings kernels from §2 of the same paper.
Let be a measurable space and a probability measure on it, the target. A proposal kernel is a Markov kernel on . Given a measurable acceptance probability , the Metropolis–Hastings kernel is
where is the point mass at (mhKernel Q α).
Put and . With and (canonDensity), let
(canonR, canonRatio). The set is symmetric, and are mutually absolutely continuous on and mutually singular off it (Proposition 1 of the paper). The Metropolis–Hastings acceptance probability is
(alphaMH π Q), and the kernel with is the maximal Metropolis–Hastings kernel for (maxMHKernel π Q).
For kernels on , dominates off the diagonal, (OffDiagDominates π P₁ P₂), if for -almost every , for all . For a countable family of kernels and weights , the mixture is the kernel (mixKernel β K).
Let be a finite or countable family of proposal kernels and with . Let be the maximal Metropolis–Hastings kernel for and the maximal Metropolis–Hastings kernel for . Then
Both sides use maximal kernels: uses of the mixture proposal, each its own , and the same weights form both mixtures.
A companion item states the maximality of (§3, p. 7): every measurable acceptance probability whose kernel is reversible satisfies -a.e., so the maximal kernel dominates every reversible Metropolis–Hastings kernel with the same proposal.
The result. Proposition 5, combined with Theorem 4 of the paper (off-diagonal domination orders asymptotic variances of reversible kernels), shows that for every function with finite variance the asymptotic variance of under the mixture-proposal sampler is at most that under the mixture of samplers. Per-iteration cost can be higher for the mixture proposal, since then needs the densities of all components; Proposition 5 isolates the statistical side of that trade-off. The maximality companion states the fact behind the name "maximal kernel": is the largest acceptance probability that keeps a Metropolis–Hastings kernel reversible.
Formalizing it. The paper's proof is a computation of about six lines with Radon–Nikodym densities. A formal version must make explicit what the computation leaves implicit: that , defined from one dominating measure, has the same density form for every symmetric dominating measure; that the measure inequality on passes to the kernel-level statement with one null set for all ; and that the mixture proposal and the mixture of kernels are handled as countable sums of kernels. As of September 2026 neither Mathlib nor this platform has a machine-checked version of Proposition 5, of the maximality of , or of reversibility of the Metropolis–Hastings kernel on a general state space; only finite-state Metropolis chains have been formalized on the platform.
The obvious argument works pointwise with densities: write every kernel as a density against a common reference measure and compare of sums with sums of minima. On a general state space there is no common reference measure given in advance, and is only defined up to -null sets, through a Radon–Nikodym derivative with respect to , a measure that differs for and for each . The step that needs care is relating these different versions: the densities of the against a common symmetric , the density of , and the transpose densities , which are densities of only because is symmetric.
The second difficulty is the passage from measures to kernels. The inequality between measures on gives, for each fixed , the kernel inequality for -almost every , with a null set that depends on . The order requires one null set for all , and the diagonal must be removed, which needs the diagonal to be measurable.
The formalization is in Lean 4 with Mathlib, in the namespace TierneyMH.Mixture. The state space is a type E with a σ-algebra; π is a probability measure; proposal kernels are Markov kernels Kernel E E. Acceptance probabilities and densities take values in (ℝ≥0∞); a general is assumed measurable with . is π ⊗ₘ Q, its image under Prod.swap, detailed balance is Kernel.IsReversible. Mixtures are indexed by a countable type ("a sequence", which includes finite families), with weights in ℝ≥0 and HasSum β 1.
Added hypotheses, both labelled in the statements: singletons are measurable (implicit in the paper's and ), on the goal and the maximality companion; and, on the goal only, the σ-algebra of is countably generated. The second is an addition to the paper: it is what makes the exceptional null set in uniform over in the passage from the measure inequality to the kernels. It is not assumed in the measure-level milestones.
is one fixed version, built from Mathlib's rnDeriv exactly as in the proof of Proposition 1 (with , not an arbitrary dominating measure), and all statements are insensitive to the version. The ratio is set to 1 on the null subset of where is infinite, so that and hold everywhere, as Proposition 1 asks.
Trivializations ruled out: is the indicator of times , never an arbitrary acceptance function or a single shared by all components; compares , not (on the rejection masses differ and the comparison is false); and the conclusion is about the Metropolis–Hastings kernels themselves, not about the measure identity alone. All hypotheses are satisfiable, for instance on = Bool with uniform, two proposals and and weights .
Needed infrastructure, reusable for other Metropolis–Hastings results: Radon–Nikodym calculus for product measures and their transposes, countable sums of kernels, and a monotone-class argument over a countable generating family. The Metropolis–Hastings kernel, , and off-diagonal domination are defined identically in the companion missions I (detailed balance, Theorem 2) and II (Peskun ordering, Theorem 4) of this series. Proofs of milestones in any order, and proofs of the goal from the milestones, are welcome.
The discrete logarithm problem modulo a prime asks, given a prime , a generator of the multiplicative group modulo , and a nonzero residue , for the exponent with . Its presumed classical hardness underlies Diffie–Hellman key exchange, ElGamal encryption and the Digital Signature Algorithm. The best classical algorithm known when Shor wrote, Gordon's adaptation of the number field sieve, runs in time .
In §6 of Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer (SIAM J. Comput. 26(5), 1997; doi:10.1137/S0097539795293172, arXiv:quant-ph/9508027), Shor gave a quantum algorithm that uses two modular exponentiations and two quantum Fourier transforms and outputs, with constant probability, a pair from which can be computed. The quantitative core of that analysis is a single number: the circuit produces a "good" output with probability at least . This mission formalizes that bound and the three estimates it is assembled from.
Let be a prime and a generator of , so that are all the nonzero residues. Fix the unknown with and put . Let be the power of with .
The Fourier matrix is the matrix with entries for (§4, eq. (4.1)). Rows index input basis vectors and columns output basis vectors.
The algorithm uses three registers: two holding numbers and one holding a nonzero residue modulo . It starts from the state
(preFourierState), applies to each of the first two registers (finalState), and measures all three registers. The probability of observing is the squared modulus of its amplitude (outcomeProb).
For integers and , the symmetric residue is the residue of modulo in (symmRes). Put
An observed state is good (IsGood) when
Goodness depends only on .
The constant is the one the page carries forward. The goal fixes no threshold on : it is stated for every prime that admits a power of two strictly between and .
The result. The bound is what turns the circuit into an algorithm. Repeating the circuit times in expectation yields a good output, and from a good pair one reads off an equation that determines modulo divisors of (§6, eqs. (6.18)–(6.20)). Together with the quantum Fourier transform circuit and reversible modular exponentiation, this places the discrete logarithm modulo a prime in quantum polynomial time. Every later analysis of quantum attacks on discrete-logarithm cryptography starts from this success probability or a sharpened version of it.
Formalizing it. The result has been proved since 1994–1997 and is textbook material; it is not open. As far as is known, no machine-checked proof of Shor's discrete-logarithm analysis exists. The paper's proof of eq. (6.17) replaces a sum by an integral with an error term whose constant is not given, yet states for every prime. A formal proof must therefore either control that error explicitly or find another argument, and so settles a point the paper leaves informal. Numerically, the smallest value of over good states is about for all primes , so the unconditional claim is not in doubt for small . The page also contains two small slips, recorded under Formalization scope; a complete development pins down exactly what is true.
The exponential sum (6.4) runs over pairs satisfying a congruence modulo , while the phases are taken modulo . The two moduli are unrelated: is a power of two and is arbitrary. Eliminating through the congruence introduces a floor function , and the resulting phase is not linear in . The obvious estimate treats the sum as a geometric series in and bounds it by its first-order phase; this fails because the floor term perturbs every phase by an amount of size up to . Condition (6.11) only keeps this perturbation within of the main phase; it does not remove it. The per-state bound must survive this perturbation uniformly in , and , including small primes where the paper's integral approximation gives no explicit control.
The count of good pairs needs a separate argument about how often a multiple lies within of a multiple of when is large.
Fin q × Fin q × (ZMod p)ˣ → ℂ. The first two registers range over ; the third over the units modulo .finalState is defined this way from (6.1) and . It is not typed in as the closed form (6.3) or (6.4). A formalization that defined the final state by (6.4) directly would make milestone 1 trivial, and is ruled out.Fact p.Prime). The generator is encoded as orderOf g = p - 1. is a parameter, with . is given by q = 2 ^ l together with . No large- threshold is added anywhere.x⁻¹ ^ b in the unit group. is computed in and inside and the congruences, and as natural-number subtraction only where makes it exact. is real.Needed infrastructure: finite exponential sums and their modulus, the symmetric residue and its basic properties, and counting multiples in residue classes of . The exponential-sum estimates of milestones 1 and 2 are reusable in the order-finding analysis of §5 of the same paper. Proofs of any milestone, of the normalization , and of auxiliary lemmas about symmRes are welcome.
Feedback laws in engineering are applied with a lag: sensors, actuators and communication channels introduce a time delay between the measurement of a state and the control that reacts to it. For finite-dimensional systems small delays are usually harmless. For distributed systems such as the wave equation they need not be: Datko, Lagnese and Polis (SIAM J. Control Optim. 24, 1986) and Datko (SIAM J. Control Optim. 26, 1988) showed, for one-dimensional examples, that an arbitrarily small delay in a stabilizing feedback can destroy stability. The question matters to anyone who designs boundary or internal controllers for vibrating structures and wants to know whether a stabilizing law is robust to delay.
Nicaise and Pignotti (SIAM J. Control Optim. 45 (2006)) study the wave equation on a bounded domain of with a damping term that combines an instantaneous and a delayed velocity feedback, with coefficients and . They show that the system is exponentially stable when (Theorems 1.1 and 1.3), and that when stability can fail (Theorems 1.2 and 1.4). This mission is Theorem 1.4, the internal-damping instability result, in the case the paper proves.
Let and let be a bounded open set with boundary of class , split as with and . Write for the outer unit normal and for the normal derivative. Let , and let be the delay. With damping coefficient the problem is
with initial data , and a history on . The standard energy of a solution is
The condition is the paper's assumption (1.8). The paper's problem (1.12)–(1.16) carries a general coefficient with and near ; is one such coefficient.
If (1.8) fails, i.e. , then
and the same holds with "" replaced by "", for every . The goal asserts only non-decay, not a rate of growth or the value of the energy, so it survives any sharpening of the examples.
The result shows that the stability threshold of Theorem 1.3 is sharp in the sense that matters for design: at or beyond the threshold there is no delay margin, since delays as small as desired already produce solutions whose energy does not decay. Together with Theorem 1.3 it gives a complete dichotomy in the coefficients for the internally damped wave equation with delay, in any dimension, and it identifies the mechanism (roots of the characteristic equation on or to the right of the imaginary axis) that later work on delayed stabilization has had to avoid.
The result is proved in the paper; to the best of current knowledge it has not been machine-checked. The mission's product is a formal proof of the case together with its algebraic core: the reduction of the transcendental characteristic equation, the analysis of both cases, and the two-sided bounds on the delays. The spectral input it needs, an unbounded sequence of eigenvalues of the mixed Dirichlet–Neumann Laplacian with regular eigenfunctions, is reusable well beyond this paper.
The scalar part is elementary. The difficulty is the spectral input. The small delays come from with , so the proof needs infinitely many eigenvalues of the Laplacian with mixed Dirichlet–Neumann conditions on a domain, with eigenfunctions that are inside and up to the boundary. This requires compactness of the embedding , the spectral theorem for compact self-adjoint operators, and elliptic regularity for a mixed problem, none of which is available in Mathlib for domains in . A single eigenpair gives only the large delays (letting ); it does not give the small ones.
A second point: the paper's own bound bounds only from below, so it does not by itself give ; the upper bound of milestone 6 is needed.
EuclideanSpace ℝ (Fin n) with . The boundary is given by a global defining function (, , on ); ; the surface measure is pinned by the Gauss–Green formula for all fields.Boundary feedback stabilization of the wave equation asks whether a damping term placed on part of the boundary drives the energy of every solution to zero. Without delay the answer is classical: the feedback on a part of the boundary gives exponential energy decay under geometric conditions (Chen, Lagnese, Lasiecka–Triggiani, Komornik–Zuazua). In practice a feedback is applied with a lag, and a small lag can destroy stability. Datko, Lagnese and Polis (doi:10.1137/0324007) and Datko (doi:10.1137/0326040) showed, in one space dimension, that a purely delayed boundary feedback destabilizes the system for arbitrarily small delays.
Nicaise and Pignotti (doi:10.1137/060648891) study a feedback made of an instantaneous part and a delayed part, with weights and , in any space dimension. Their Theorem 1.1 gives exponential decay when . This mission formalizes the converse, Theorem 1.2: when , some delays admit solutions whose energy does not decay at all.
Timeline.
Let and let be a bounded open set with boundary of class . The boundary is split as , with and . Write for the outer unit normal and for the surface measure. Together these data form a mixed domain (MixedDomain n in Lean).
Fix and a delay . The problem (1.1)–(1.3) is
with initial data , and a history on (1.4)–(1.5). The standard energy of a solution is (3.7)
Condition (1.8) of the paper is . This mission concerns the complementary case .
For real functions on , (5.11) defines and .
If , there exist delays and, for each , a classical solution of (1.1)–(1.3) with delay and a constant such that
The statement fixes no formula for the delays and no value of the energy. It asserts only the existence of infinitely many delays for which the energy does not decay.
The result. Theorem 1.2 shows that the threshold of Theorem 1.1 is sharp in the following sense: once the delayed weight reaches the instantaneous one, no geometric assumption restores asymptotic stability for every delay. Together, Theorems 1.1 and 1.2 separate robust from non-robust boundary feedbacks by a single inequality between the two gains. The explicit delays of case (a), , become arbitrarily small or large. So even an arbitrarily short lag in an equally weighted feedback can remove decay.
The formalization. The paper proves the result. It has not been formalized, and Mathlib has no wave equation on domains, no mixed eigenvalue problems and no Sobolev spaces on domains. This mission produces:
Milestones 1 and 2 are calculus and trigonometry. The difficulty sits in producing . The goal needs a nonzero function that is in and up to the boundary and solves an eigenvalue problem with mixed Dirichlet and Neumann (case (a)) or Dirichlet and Robin-type (case (b)) boundary conditions. Existence requires compactness of and of the trace into , followed by elliptic regularity up to a boundary. None of these is in Mathlib.
A shortcut does not work: in case (b) the frequency enters the boundary condition, so is not an eigenfunction of a fixed self-adjoint operator. The page instead minimizes a non-quadratic functional, and its first-variation computation (5.18)–(5.19) needs care: the functional is not 2-homogeneous, so the normalization by does not literally give , although the first-order condition is right.
Taking real parts does not give a real-valued solution with constant energy: in case (b) the energy of oscillates.
A complete development needs the following:
These pieces are reusable well beyond this mission. Contributions of any of them, or of an alternative route to a with the required properties, are welcome.
Many problems in statistics, signal processing and machine learning minimize a sum of a smooth loss and a nonsmooth regularizer: least squares with an or penalty, and constrained problems in which the regularizer is the indicator of a nonconvex set. The proximal gradient method (also called forward–backward splitting) is the standard first-order algorithm for such problems. Each step takes a gradient step on the smooth part and then applies the proximal mapping of the nonsmooth part, which for many nonconvex regularizers (hard thresholding, projection onto sparse vectors) has a closed form.
For a smooth part whose gradient is -Lipschitz, the classical analysis allows any constant step size , and every cluster point of the iterates is stationary; Li and Pong cite Bredies and Lorenz (Minimization of non-convex, non-smooth functionals by iterative thresholding, preprint, 2009) for this. Attouch, Bolte and Svaiter (Math. Program., 2013) added convergence of the whole sequence when has the Kurdyka–Łojasiewicz property. When is nonconvex, however, is governed by the most negative curvature of as much as by the most positive one, and the admissible step sizes can be much smaller than the convex part of alone would require.
Li and Pong (SIAM J. Optim., 2015; preprint arXiv:1407.0753v6) show that the concave part of imposes no restriction on the step size: it suffices to bound the curvature of after it has been offset by a convex function. This mission formalizes that result, Theorem 4 of their paper. It is the fourth mission of a series on the paper; the first three treat its results on the alternating direction method of multipliers.
Work in with the Euclidean inner product and norm . The problem is
under the paper's standing assumptions: is twice continuously differentiable with a bounded Hessian ; is proper (never , finite somewhere) and closed (lower semicontinuous); and for every and the proximal problem has a minimizer. Neither nor is assumed convex.
A vector is a regular subgradient of at (with ) if for all near , for every . The limiting subdifferential collects the limits of regular subgradients at points with . A point is stationary if
Given a step size and an arbitrary starting point , the proximal gradient method generates by
Any minimizer may be selected. A cluster point of is the limit of a subsequence .
The step-size condition involves a convex function and a constant with
where is the Loewner order on symmetric linear maps.
Suppose is twice continuously differentiable and convex, , (44) holds, and is generated by (43) with . Then
and every cluster point of , if one exists, satisfies .
The goal does not assert that a cluster point exists, nor that the whole sequence converges; both are false without further assumptions.
In the order of the paper's proof:
The result. For a difference of convex functions with being -Lipschitz, (44) holds with and , so the step size may be taken in whatever the curvature of . For an indefinite quadratic the admissible range becomes instead of , and for a concave quadratic every positive step size is admissible. Because the method is a descent method under this rule, its iterates stay in a sublevel set of , so the sequence is bounded whenever is coercive. The same estimates feed the whole-sequence convergence argument for Kurdyka–Łojasiewicz functions.
Formalizing it. The theorem is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it requires the limiting subdifferential of an extended-real-valued function, its closedness property (3), and a Fermat rule for a smooth-plus-nonsmooth sum, none of which is in Mathlib. These are reusable for any nonconvex first-order method analysed through cluster points.
The descent part rests on (45), a descent inequality for whose Lipschitz constant is read off from a two-sided Hessian bound; the familiar descent lemma is stated for alone and does not apply, since may have a much larger Lipschitz constant than .
The stationarity part is where the naive argument fails. Passing to the limit in (47) needs not only but also , because the limiting subdifferential is closed only under -attentive convergence. Lower semicontinuity gives one inequality; the other must come from the minimizing property (43) compared against . The objective may be at , so summability of the steps has to be extracted without assuming a finite starting value.
The space is EuclideanSpace ℝ (Fin n). and are real-valued; takes values in EReal, and every objective value is compared in EReal, never through EReal.toReal. The Hessian is the derivative of the gradient map, a continuous linear self-map; the Loewner order is Mathlib's partial order A ≤ B ↔ (B - A).IsPositive, and both sides of (44) are kept. The regular subgradient is encoded in its -neighbourhood form, and the limiting subdifferential requires all three convergences , , . Stationarity is . The update (43) is a relation on sequences: minimizes the bracket over all of , with no uniqueness and a free starting point. A cluster point is the limit of for a strictly increasing .
Trivializing formalizations are ruled out: (44) is not replaced by " is -Lipschitz", which is the classical special case ; , boundedness of the sequence and existence of a cluster point are not assumed; and a limiting subdifferential without is not used, since that would make stationarity a weaker statement.
Contributions welcome: the closedness (3) and the Fermat rule behind (47) for the limiting subdifferential, a descent lemma from a two-sided Hessian bound, and the telescoping and limit arguments of the proof.
The alternating direction method of multipliers (ADMM) is a standard method for problems of the form , in which a smooth loss is composed with a structured, possibly nonsmooth regularizer through a linear map . Its convergence theory was developed for convex problems, yet it is routinely run on nonconvex ones: sparse recovery with the constraint, low-rank matrix problems, and total-variation-type models with nonconvex penalties. For such problems a practitioner wants a guarantee about the iterates actually produced, not only about the existence of good subsequences.
Li and Pong (arXiv:1407.0753v6, SIAM J. Optim. 25(4), 2015) gave the first such guarantee for the classical ADMM on nonconvex composite problems with a surjective . Their Theorem 1 shows that cluster points of the (proximal) ADMM are stationary; their Theorem 3, the subject of this mission, shows that for semi-algebraic data the whole sequence converges. The argument adapts the Kurdyka–Łojasiewicz (KL) framework of Attouch, Bolte and Svaiter (Math. Program. 137, 2013) to a setting where the ADMM only decreases its merit function in the -block.
Fix linear, twice continuously differentiable with bounded Hessian, and proper (finite somewhere) and closed (lower semicontinuous). For the augmented Lagrangian is
The ADMM produces from arbitrary by
Assumption 1 with asks for , and symmetric maps with , and for all , , and .
The limiting subdifferential of consists of limits of regular subgradients at points with . A point is stationary if .
A set in is semi-algebraic if it is a finite union of sets cut out by finitely many polynomial equations and strict inequalities ; a function is semi-algebraic if its graph is. A proper has the KL property at if there are , a neighbourhood of and a continuous concave with , , , such that whenever and . A KL function is proper, closed, and KL at every point of .
In the Lean development is augLag h P M β x y z, and also augLagX h P M β as a single function on the triple space with the Euclidean inner product.
Under the standing assumptions and Assumption 1 with , if and are semi-algebraic and the ADMM sequence has a cluster point , then
No constants are fixed: every parameter is quantified exactly as in the paper.
Milestones 6, 7 and 8 together imply the goal.
The result. Theorem 3 upgrades subsequential convergence to convergence of the whole iterate sequence, with finite length of the -trajectory, for a nonconvex ADMM without any convexity of or . Semi-algebraicity covers the paper's applications: polynomial losses, the constraint, and indicators of polyhedral or algebraic sets. Remark 4(1) isolates the only property actually used, the KL property of , so the result extends to any class of functions for which that property is known (for instance, globally subanalytic or o-minimal definable data).
Formalizing it. The result is proved in the paper and, as far as is known, formalized nowhere. The mission produces a machine-checked version of the paper's convergence argument, a Lean definition of the KL property with the correct convention for empty subdifferentials, and a semi-algebraic set predicate over MvPolynomial. Milestone 8 is a published theorem of real algebraic geometry and nonsmooth analysis (Bolte–Daniilidis–Lewis 2007) that the paper quotes without proof; it is part of what a complete development of the goal requires.
The obvious route is to invoke the abstract convergence theorem of Attouch–Bolte–Svaiter for descent methods. It does not apply: its sufficient-decrease hypothesis requires to drop by a multiple of , while the ADMM only guarantees a drop proportional to (Remark 4(2)). The relative-error bound (35) is likewise in terms of the -step alone, and relating the - and -blocks back to the -block uses the surjectivity of and the specific structure of the multiplier update. The neighbourhood on which the KL inequality holds is a neighbourhood of the full triple, whereas the trajectory is controlled only in .
The semi-algebraic part has a separate difficulty: showing that is semi-algebraic needs closure of semi-algebraic sets under projection (the Tarski–Seidenberg theorem), and the KL property of semi-algebraic functions needs the Łojasiewicz inequality for subanalytic or semi-algebraic functions. Mathlib has neither.
Spaces are EuclideanSpace ℝ (Fin n); is a continuous linear map and its adjoint. and take values in EReal, never passed through toReal except where the value is provably finite. is Mathlib's Loewner order on self-maps; the Hessian is fderiv ℝ (gradient h). The ADMM is the proximal-ADMM relation with ; argmin steps are "value at most the value anywhere", with no uniqueness; is unconstrained. The triple space is the nested product, so its inner product is the sum of the block inner products.
The KL inequality is stated for every , which encodes . Writing it with Metric.infDist 0 (∂f x) would give and make the KL property fail at every point with empty subdifferential, so that "semi-algebraic implies KL" becomes false and the goal becomes a statement about a different notion. The KL property is required only at points of , only on a neighbourhood and only for values in ; is differentiable only on the open interval. Semi-algebraicity of an extended-valued function is that of its graph over its real values. is a positive real, which is equivalent to the paper's .
The hypotheses and are part of the theorem, not a simplification: the analogous statement for the proximal ADMM is open (Remark 4(3)). The cluster point is assumed, not derived.
Needed infrastructure: calculus of the limiting subdifferential (a smooth-plus-separable sum rule), the Tarski–Seidenberg theorem, and the Łojasiewicz/KL inequality for semi-algebraic functions. The last two are reusable far beyond this mission; contributions toward them, and toward the analytic core (milestones 1–6), are welcome.
The alternating direction method of multipliers (ADMM) splits a problem of the form into a sequence of simpler subproblems, one in which the nonsmooth term enters only through its proximal map and one in which only the smooth term appears. For convex problems its convergence theory is classical. In signal processing and statistics, however, the method is routinely run on nonconvex models, such as - or -regularized least squares, where is nonconvex and possibly discontinuous and convex theory does not apply.
Li and Pong (arXiv:1407.0753, SIAM J. Optim. 25(4), 2015) gave a convergence analysis of a proximal variant of the ADMM for this nonconvex setting. Their Theorem 1 shows that every cluster point of the iterates is a stationary point. That statement is only informative if cluster points exist. Theorem 2, the subject of this mission, gives conditions on , and under which the whole sequence of iterates is bounded, so that cluster points exist and Theorem 1 applies.
Let . The data are:
The augmented Lagrangian is
and the Bregman distance of is . A sequence is generated by the proximal ADMM if, from arbitrary ,
For a linear self-map , write , and write , for the semidefinite and definite order of symmetric maps. Assumption 1 asks for with (so is surjective), bounds , maps with , with , a bound , and with
Suppose Assumption 1 holds and, with the same and , there is with
Suppose that either (i) is invertible and , or (ii) and . Then
The milestones are the numbered displays of the paper's proof:
The result. Theorem 2 supplies the existence of cluster points that Theorem 1 assumes. The two together give an unconditional statement: under Assumption 1, (29) and either coercivity condition, the proximal ADMM has a cluster point and every one of them is stationary. The hypotheses cover the models that motivate the paper. Least squares with a coercive nonconvex regularizer falls under case (i) with , and a strongly convex quadratic with a regularizer that is bounded below and a general surjective falls under case (ii) (Examples 4–6 of the paper). Boundedness is also a standing hypothesis of the paper's Theorem 3, the Kurdyka–Łojasiewicz argument for convergence of the whole sequence.
Formalizing it. The result has been proved since 2015. As far as a search of the platform shows, neither it nor the underlying Lyapunov-type estimates for the ADMM has been machine-checked. This mission formalizes the known proof. The estimates (20), (30) and (31) are shared with the stationarity analysis of the same algorithm, so they serve any later formal work on nonconvex ADMM variants.
The obvious approach is to bound the iterates by the monotone quantity of Eq. (30). That quantity involves , which contains and is not bounded below a priori, so its decrease alone does not bound anything. The dual term has to be absorbed. It is controlled through and the last primal step, and the part involving is then paid for out of itself. Condition (29) exists to make exactly this trade possible, which is why it couples to the of Assumption 1. The two cases then extract boundedness in opposite orders: (i) goes from through to using invertibility of , and (ii) goes from through to . In case (i) the lower bound on that the argument needs is not assumed and must itself be derived from coercivity and lower semicontinuity.
EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), and is a continuous linear map with Mathlib's adjoint. , and every inequality containing them live in EReal, stated additively so that no extended-real subtraction occurs.Ruling out trivial versions. A formalization that bounds only , fixes or to an example's values, lets (29) use a fresh , adds a lower bound on in case (i), or assumes minimizers that make the sequence constant proves a different, weaker theorem, and is not the target.
Definitions needed. Proper and closed extended-valued functions, the Hessian as fderiv of gradient, the augmented Lagrangian, the Bregman distance, the proximal-ADMM relation and Assumption 1 are all provided. They mirror the definitions of the companion mission on cluster points of the same algorithm. A solver will need standard facts beyond them: first-order optimality for a differentiable function, the mean-value bound from the Hessian sandwich, and strong convexity of the -subproblem. Proofs of individual milestones are welcome independently.
Approximate policy iteration and policy-gradient methods stop when they can no longer find a direction of improvement. Kakade and Langford (ICML 2002) asked what such a stopping point guarantees. Their algorithm, conservative policy iteration, halts at a policy for which no policy can improve much on as measured under a restart distribution ; the quantity that is small is the optimal policy advantage . Theorem 6.2 of the paper translates this local condition into a global statement: the performance of is close to optimal, with a loss controlled by how well covers the states an optimal policy visits.
The bound is the origin of the distribution mismatch coefficient , which reappears in the analysis of approximate dynamic programming (concentrability coefficients, Munos 2003), of conservative and trust-region methods, and of the convergence of policy gradient methods (Agarwal, Kakade, Lee, Mahajan 2021), where it governs the rate. The performance difference lemma (Lemma 6.1) used in its proof has become a standard tool of reinforcement learning theory.
A finite Markov decision process has a finite nonempty state set , a finite nonempty action set , transition probabilities (for each a probability distribution over ), a reward function with , and a discount factor . A stochastic policy is, for each state , a probability distribution over actions. A state distribution is a probability vector on .
The normalized value function is , where , and . The state–action value is and the advantage is . The discounted future state distribution from is
and the performance of from is .
The policy advantage of with respect to and is : the expected advantage of over on the states itself visits. Its maximum over all stochastic policies is (Definition 4.3). An optimal policy satisfies for every policy and every state . For nonnegative on , (p. 5).
If and is optimal, then for every state distribution
The goal states both inequalities and the outer bound. The evaluation distribution is arbitrary and unrelated to the restart distribution ; taking , the start distribution, gives Corollary 4.5 (p. 5).
For any policies , and any starting distribution ,
The states are weighted by the future state distribution of the new policy , the advantage is that of the old policy .
Theorem 6.2 is the quality guarantee for conservative policy iteration: combined with the paper's Theorem 4.4 (the algorithm stops with after polynomially many calls), it bounds the suboptimality of the returned policy for any target distribution, independently of the size of the state space except through the mismatch coefficient. It also explains the role of the restart distribution: a more uniform makes small. Lemma 6.1 is used throughout later theory, from trust-region policy optimization to the global convergence of policy gradient methods.
Both results are proved in the paper, with short arguments. The contribution of this mission is a machine-checked version of the infinite-horizon discounted statement in the paper's normalization, with the ratios handled exactly, including states where a denominator vanishes. Neither the discounted performance difference lemma for stochastic policies nor the distribution mismatch bound is known to be formalized in Mathlib; a finite-horizon performance difference identity has been formalized separately and is a different statement.
The mathematics is short; the difficulty is in the infinite-horizon bookkeeping. The value function and are infinite series, and Lemma 6.1 relates the series of two different policies: its natural one-line argument uses the Bellman equation for , which is not the definition here, together with interchanges of infinite sums over time with finite sums over states and actions, each of which needs summability. Theorem 6.2 then needs two facts that are not stated as results in the paper: that equals (the supremum over policies is attained by a greedy policy, and ), and that . Reading the ratio with real division would give a false statement when a denominator is zero; the statement avoids this.
States and actions are finite nonempty types; policies and kernels are real-valued functions π s a (the paper's ) and P s a s' (the paper's ), with their distribution properties as explicit hypotheses. The published definitions IsTransitionKernel, IsPolicy, InducedTransition, OccupationDist, InducedReward and PolicyValue from the Foundations of Machine Learning series are reused; is times PolicyValue, the defining series. is the supremum of the policy advantages over stochastic policies, which is the paper's maximum. Optimality of is relative to stationary stochastic policies, the paper's policy class; the existence of an optimal policy (the paper's "well known result", p. 2) is not part of this mission.
Every hypothesis is explicit: rewards in with , , a kernel, and stochastic policies, and state distributions. Each bound is stated multiplicatively: "" is " for every with for all ". When some no such exists and the bound is empty, which matches ; no full-support assumption is made on or . The hypothesis is on the supremum itself, not on the closed form , which is a step of the proof; a formalization that assumed the closed form, or that divided by in real arithmetic, would not be this theorem. The proof of the theorem uses only that is a policy; optimality is kept as a hypothesis because the paper states it.
The proof on p. 7 twice writes ; the inequality it uses, and the one stated on p. 5, is . This slip is in the proof, not in the statement. Pages are PDF pages; the paper has no printed page numbers.
Useful reusable infrastructure: summability and Bellman equations for the normalized discounted value, as a probability distribution with , and attainment of by a greedy policy. Contributions of any of these as separate lemmas are welcome.
Johnson's 1954 paper in Naval Research Logistics Quarterly is the starting point of machine scheduling theory. Its first section solves the two-machine flow shop: items must pass through machine 1 and then machine 2, and an explicit ordering rule minimizes the total elapsed time. Its second section treats three machines. There the problem "loses some of the nice structure of the two-stage case" (p. 65), and the general three-machine problem was later shown to be strongly NP-hard (Garey, Johnson and Sethi, 1976). Johnson nevertheless identifies a restricted case, in which the middle machine is dominated by the first (or the last), where the two-machine rule still gives an optimal schedule. That case, and the structural facts behind it, are the content of this mission.
The three-machine results are still the reference point for polynomially solvable flow shops and for lower bounds in branch-and-bound methods for the general problem.
Timeline.
There are items and three machines. Item needs processing time on machine 1, on machine 2 and on machine 3, in that order. Each machine handles at most one item at a time, and processing is not interrupted.
A schedule assigns each item start times . It is feasible when all start times are at least on machine 1, the processing intervals of distinct items on the same machine do not overlap, and , . The three machines may process the items in different orders. The total elapsed time (makespan) is .
An ordering lists the items, being the item in position . Its as-soon-as-possible schedule processes the items in the order on every machine and starts each item on each machine as early as the rules allow. For an ordering, with positions , Johnson defines
the sums running over the items in the first (resp. ) positions.
Johnson's three-stage rule says that item definitely precedes item when
and calls them indifferent under equality. An ordering is consistent with (IV) when no item placed later is definitely preferred to an item placed earlier.
If every is at least every , then an ordering consistent with (IV) exists, and for every such ordering the as-soon-as-possible schedule of is feasible and satisfies
the "maximum walk" of p. 68. 3. Special case (p. 67). If then , so the makespan is . 4. (III) (IV) (p. 67). Interchanging the items in positions changes and only at , and the interchange is strictly worse for the diagonal terms exactly when (IV) holds. 5. Lemma 4 (p. 67). Relation (IV) is transitive, except when the middle item is indifferent to both others. 6. Mirror case (p. 68). The conclusion of Theorem 2 also holds when every is at least every .
The result. Theorem 2 gives an exact method for a class of three-machine flow shops, in a problem that is strongly NP-hard in general. Lemma 3 says that, for three machines, permutation schedules are dominant; Johnson's example on p. 65 shows this fails for four machines. The closed form of milestone 2 expresses the makespan of any ordering as a longest path in a grid, the device behind most later flow-shop lower bounds.
Formalizing it. All results are proved on paper, some tersely: Lemma 3's proof is two lines and cites the wrong lemma, Lemma 4 is proved by reference to Lemma 2, and the mirror case is asserted without proof. A search of Mathlib and of the platform catalog found no machine-checked proof of any of them. The mission produces a checked account of the three-machine flow shop, including the comparison against all feasible schedules rather than only permutation schedules, and pins down the exact form of the hypotheses (see below).
The interchange argument of the two-machine case does not transfer directly. For a general ordering the makespan involves , and interchanging adjacent items changes terms that depend on everything placed earlier; the page notes that "the decision is not independent of what precedes the interchanged elements". The hypothesis is what makes nondecreasing along the ordering, collapsing the double maximum to the diagonal. A second obstacle is that (IV) is not a total preorder: ties break transitivity, so passing from "no adjacent pair can be improved" to "optimal" needs the all-pairs consistency and the tie exception of Lemma 4. Finally, Lemma 3 is a statement about arbitrary start-time schedules, so the reduction to orderings must handle machines whose orders differ.
Items are Fin n; processing times are real-valued functions A B C : Fin n → ℝ, assumed positive in each theorem that is about schedules (the paper's standing assumption, p. 61). A schedule is three start-time functions; feasibility is spelled out as above with non-overlap written as a disjunction of inequalities. The makespan is the maximum of the machine-3 completion times together with , so the empty instance has makespan . An ordering is an Equiv.Perm (Fin n) with σ k the item in position k; positions are 0-based, so the Lean K u, H v are the paper's , . Statements with maxima over positions assume .
Hypotheses made explicit or corrected:
Optimality in the goal is against every feasible schedule. A formalization that compares only orderings with each other, or that defines the objective as the closed form , would drop Lemma 3's content and is ruled out: the makespan is the latest completion time of a start-time schedule. The existence clause keeps the optimality clause from being vacuous.
A complete development needs finite sums over initial segments of Fin n, Finset.sup', and permutation manipulations (adjacent transpositions, bubble-sort arguments). The feasibility model and the closed form are reusable for other flow-shop results; contributions of general lemmas on adjacent interchanges of permutations are welcome.
Federated learning combines information from several clients without pooling their raw training records. A client may later request removal of its contribution. Retraining on the retained records supplies a natural comparison model, but repeating the training process can be costly. Jin, Chen, Zhang, and Li introduce a linearized learning pipeline and a server-side removal procedure in Forgettable Federated Linear Learning with Certified Data Unlearning, arXiv:2306.02216v3. Their linearization makes the training objective quadratic, so the distinction between an exact Newton correction and an approximate correction can be studied explicitly.
This mission formalizes a corrected finite-run error bound motivated by that analysis. It is not a transcription or validation of the printed Theorem 2. The source audit found that the supplementary argument drops a finite-training term when passing to a limit, uses an invalid general inverse-perturbation inequality, and does not justify its three-term squared-norm constant. The draft preserves the removal problem while stating its error factors explicitly. The source anchors are Section III-C, Theorem 2, PDF pp. 5–6, and supplementary Section C5, PDF p. 16. The preprint first appeared in 2023; this mission fixes the revised May 2026 version so later source changes cannot silently alter its meaning.
A parameter is a vector . Record has a fixed linear feature map , an offset , and a target . Its prediction is . This represents the fixed linearization in the paper's equation (3); arbitrary real targets are permitted, and one-hot classification targets are a special case. Neither approximation accuracy for a nonlinear neural network nor an infinite-width limit is asserted.
Let be the full finite dataset and a nonempty subset of retained indices. Client removal is represented by retaining precisely the indices whose owner differs from the removed client. More general record removals are also allowed. For a fixed regularization parameter , define
Write , , and . Define and let use the full dataset. These reference parameters are computed from the data. The accepted child proofs establish the Hessian positivity and invertibility needed for the error bound; the broader unique-minimizer theorem is a separate supporting statement. The construction comes from Section III-A, PDF pp. 3–4, equations (3)–(5).
A separate nonempty server dataset has Gram operator and regularized Hessian . All operator norms below are Euclidean operator norms. The datasets and feature maps are fixed throughout the probability calculation.
Let be the trained parameter, the parameter returned by retraining on , and an approximate removal correction. The removed parameter is . Their joint probability model has finite outcome space , with masses summing to one. They may be dependent. This covers the outputs of finite randomized runs on finite data with fixed initialization; no independence assumption is used.
For each trained parameter , define the server removal objective and its exact minimizer by
This is the quadratic surrogate in Section III-B, PDF p. 5, equation (6). Define
The corrected goal is
The two completed milestones used by the accepted proof are the surrogate gap bound and the corrected signed removal-error identity:
The broader ridge-structure, exact-Newton-removal and inverse-perturbation statements remain available as separate open theorems. Their milestone entries were removed because the accepted proof does not depend on their full statements.
Formalization note: the completed root is a corrected, paper-derived error bound. Its formal bridge uses the two source-backed child theorems above, anchored to Section III-B (Section 3), PDF p. 5, equation (6), and Section III-C (Section 3), PDF p. 5 and PDF p. 6, Theorem 2; supplementary C5, PDF p. 16, unnumbered displays. The coefficients in the boxed goal are conservative; no optimality claim is made.
The result connects the removal solver's objective gap, the difference between the server and retained Hessians, and the actual optimization errors to an observable parameter discrepancy. Exact Hessian matching sets . Exact removal optimization sets , but finite retraining error still remains. This distinguishes exact optimization of the retained objective from reproducing an unfinished retraining run.
The original paper motivates the comparison; the displayed corrected bound is a new formulation derived from its quadratic setting. The root Lean theorem and its two dependency milestones are now Proved. Their accepted proofs match the original formal statements exactly; the three separate supporting statements remain open. The requested OpenProblem classification describes the formalization task and does not assert that the elementary corrected inequality is an unresolved research conjecture.
An approximate server Hessian cannot be substituted for the retained Hessian without a sensitivity term. A bound on the difference of the Gram operators alone does not bound its action on every parameter vector. Likewise, a small training error relative to the full-data optimum does not imply that the full and retained optima coincide. The displacement therefore remains visible. Formalization must respect the normalization of each empirical objective, the sign of the correction, and the operator norm used in the perturbation estimate.
The model uses finite-dimensional real Euclidean spaces, continuous linear maps and adjoints, finite index sets, a total ring inverse, and finite weighted expectations. Positive regularization must justify every use of the inverse; it is not an invertibility assumption hidden inside the dataset. Nonempty retained and server data exclude division by an empty sample count. Zero-dimensional feature or parameter spaces are permitted and harmless. A finite law on an empty outcome type has no inhabitant because its masses cannot sum to one.
The root theorem quantifies over arbitrary output maps . It is an error-propagation theorem in terms of their actual errors and surrogate gap, not a convergence theorem for a particular implementation. Obtaining algorithm-specific bounds on those quantities is separate future work. In particular, the draft does not import the source's unsupported all-smaller-learning-rates FedAvg contraction claim. It also makes no differential-privacy, distributional indistinguishability, nonlinear-network, or empirical accuracy assertion.
The Lasso (Tibshirani 1996, doi:10.1111/j.2517-6161.1996.tb02080.x) is -penalized least squares regression, one of the standard estimators of statistics and machine learning because it selects sparse coefficient vectors. Explaining why a learned Lasso predictor generalizes is less routine than it looks. The two classical routes are uniform convergence over the hypothesis class and algorithmic stability (Bousquet and Elisseeff 2002, JMLR 2:499–526). The stability route is closed for the Lasso: Xu, Caramanis and Mannor (IEEE Trans. Inf. Theory 56(7), 2010, doi:10.1109/TIT.2010.2048503) showed that its uniform stability bound does not decrease with the sample size, a fact reproduced as Theorem 7 of Xu and Mannor (2012).
Xu and Mannor, Robustness and Generalization (Mach Learn 86 (2012) 391–423, doi:10.1007/s10994-011-5268-1), propose a third route, algorithmic robustness: if the sample space can be split into cells such that a test point in the same cell as a training point has nearly the same loss, then the algorithm generalizes (their Theorem 1). Their Example 6 shows that the Lasso is robust in this sense, with a number of cells given by a covering number and a robustness level depending on the training responses. This mission formalizes Example 6 together with the general criterion it rests on (Theorem 6) and the Lipschitz estimate for the Lasso loss (Lemma 3).
A sample is a point with a response and a feature vector , so the samples live in . The sample space is a compact set, and carries the norm . A training set is .
A learning algorithm maps each training set to a hypothesis ; with a loss , it is -robust (Definition 2, p. 396) if can be partitioned into disjoint sets , fixed independently of the data, such that for every , every training point , every and every ,
For a metric on and , a set is an -cover of if every point of is within distance of a point of ; the covering number is the least cardinality of such a cover (Definition 1, p. 394).
For a coefficient vector let . Given , the Lasso is
a Lasso algorithm returns a minimizer of (5) for each , and the loss is the absolute prediction error . Finally .
For every compact , every , every Lasso algorithm and every ,
The statement holds for every selection of a minimizer, since (5) need not have a unique solution.
Combined with Theorem 1 of the same paper, Example 6 yields a generalization bound for the Lasso of the form with a covering number of the sample space, a bound that uses no stability of the algorithm and no uniqueness of the minimizer. Theorem 6 is the reusable part: it converts any data-dependent local Lipschitz or continuity estimate of the loss into robustness, and the paper derives its examples for the SVM, the Lasso, neural networks and PCA from it. The authors note (p. 404) that the resulting bound is weaker than VC-dimension bounds for linear predictors, since it depends exponentially on the dimension; the value of the example is the method, not the rate.
The results are proved in the paper, with short arguments. No machine-checked version of Theorem 6, Lemma 3 or Example 6 is known to exist. The formal work is to connect Mathlib's covering numbers to partitions of a set, to handle the / pairing on , and to state robustness so that later missions of this series (the generalization bound of Theorem 1, mission I) can consume it.
The constant in the robustness level depends on the training set through , while the partition in Definition 2 must be chosen before the training set is seen. A formalization that lets the cells depend on proves a much weaker, nearly empty statement, so the data dependence has to be carried entirely by and the cells must depend only on and . A cover by balls is not a partition, and the radius of the cover () and the closeness threshold in Theorem 6 () differ by the factor that the diameter of a cell requires. The Lipschitz estimate must bound a Lasso solution without any information beyond optimality, and the pairing between and is the one that makes the constant come out as printed; a Euclidean norm on either side gives a different constant.
ℝ × (Fin m → ℝ), a point being (z^{(y)}, z^{(x)}). Lean's norm on this product is the maximum of the absolute values of all coordinates, which is exactly . is written out as , since the default norm on Fin m → ℝ is the sup norm; is dotProduct w x.Z with IsCompact Z. Robustness (IsRobustOn) asks for cells C : Fin K → Set α that lie in Z, cover Z and are pairwise disjoint (empty cells allowed), chosen before the universally quantified training set; training sets are maps Fin n → α with all points in Z. No measurability is involved anywhere in this mission.Metric.coveringNumber at radius Real.toNNReal (γ / 2): closed balls, centres in Z (the metric space of Definition 1 is itself), value in ℕ∞, converted with toNat. Theorem 6 assumes its finiteness, as the paper does; without that hypothesis toNat would return and the statement would be false for nonempty Z. Example 6 does not assume it: it follows from compactness.A with ∀ s, IsLassoSolution c s (A s); it is not defined by a choice of minimizer. The regularization parameter satisfies , which the paper leaves implicit. The factor is a real division; for it is in Lean, the objective reduces to , and all statements remain true.Useful infrastructure beyond this mission: a lemma turning a finite cover of a set into a partition of it with cells of diameter at most twice the radius, and finiteness of Mathlib's internal covering number for compact sets. Contributions of either as separate theorems are welcome.
Classical generalization bounds control the gap between the expected loss of a learned hypothesis and its average loss on the training sample. The average is sensitive to outliers: when a non-negligible fraction of the sample is corrupted, the mean loss stops describing the quality of a solution, and quantile-type summaries such as the median become the natural measurement. Quantile losses have long been used for this reason in statistics and econometrics (Koenker and Bassett 1978; Huber 1981). The standard tools for proving generalization bounds — symmetrization, Rademacher and VC arguments — are built around the expected loss and do not extend to quantiles in any direct way.
Xu and Mannor (Mach Learn 86 (2012) 391–423) introduced algorithmic robustness: an algorithm is robust if the sample space can be partitioned into finitely many cells such that a test point falling in the same cell as a training point incurs a similar loss. Because the argument works cell by cell and needs no symmetrization, it transfers to loss functionals other than the mean. Sect. 4.1 of the paper uses this to bound the quantile value and the truncated mean of the testing error, and Sect. 5 relaxes robustness to pseudo robustness, which only asks the cell condition for a subset of the training samples. This mission formalizes the resulting Theorem 5 (p. 402), whose proof is Appendix C (pp. 415–418).
Let be a measurable sample space, a set of hypotheses and a loss, with each measurable. A training set consists of i.i.d. draws from a probability measure on ; its empirical distribution is . A learning algorithm is a map , and is the hypothesis learned from .
For a real random variable and a level , the -quantile value is
and, writing , the -truncated mean is
where the second term vanishes when . It is the contribution to of the leftmost fraction of the distribution. For a hypothesis and a measure on put and with .
The algorithm is pseudo robust, with and , if can be partitioned into disjoint sets , fixed in advance, such that every training set has a subset of samples with: whenever and lie in a common cell, . With this is -robustness.
Let and . If is pseudo robust, and , then with probability at least : whenever and ,
The constants are the paper's, and , , , , , and the algorithm are arbitrary.
The result. Theorem 5 shows that any pseudo-robust algorithm has a testing-error quantile and truncated mean that are bracketed by the empirical ones at levels shifted by , up to the robustness tolerance . The quantile of the testing error can therefore be estimated from training data for every algorithm to which the robustness framework applies — among them majority voting, SVMs, Lasso and principal component analysis (Sect. 6 of the paper) — without a separate complexity analysis of the loss class. The pseudo-robust form covers algorithms that are robust only away from a small set of training samples, which is the typical situation in the presence of outliers. The robust case is the paper's Theorem 2 (p. 400).
Formalizing it. The paper states Theorem 5 and proves it in Appendix C; no machine-checked proof exists. The appendix contains misprints (see Formalization scope) and the argument uses minimizers of the loss over each cell, which need not exist; a formal proof settles which steps are sound as written. The definitions of quantile value and truncated mean of a law on developed here are reusable beyond this mission.
The concentration step is the same as for the expected loss: on the event the empirical cell frequencies are close to the cell probabilities. The difficulty is converting this into a statement about quantiles. Quantile values are not linear in the distribution and are discontinuous in the level, so the triangle-inequality argument that bounds the mean-loss gap does not apply. Mass that moves between cells shifts every level of the quantile function, and the up to samples outside carry no guarantee at all, so an arbitrary fraction of the empirical law is uncontrolled. For the truncated mean this must be done for the whole lower tail up to level , not just at one point, and the atoms of the loss distribution (the second branch of the definition) have to be accounted for exactly.
XuMannorRobust.Quantile. is a type with a measurable space structure, an arbitrary type, a training set a function Fin n → Z, and the i.i.d. law the product measure Measure.pi (fun _ => μ).Most generalization guarantees in statistical learning theory bound the gap between training error and expected error through a complexity measure of the hypothesis class: VC dimension, Rademacher complexity, covering numbers. Such bounds are sufficient conditions, and they say little about why a particular algorithm, run on a particular data stream, does or does not generalize. Xu and Mannor (Mach Learn 86 (2012) 391–423) proposed algorithmic robustness as an alternative: an algorithm is robust if a test sample "close to" a training sample incurs a loss close to that training sample's loss. Their first results show that robustness implies generalization (Theorem 1 of the paper, the subject of the first mission in this series).
Section 8 of the paper asks the converse question: is some form of robustness also necessary? The answer is Theorem 8. For a learning method trained on a fixed, growing sequence of samples, generalization is equivalent to a weaker property, weak robustness. The authors present this as evidence that robustness is "an essential property of successful learning", and contrast it with the characterization of learnability by stability (Remark 5 of the paper, citing Shalev-Shwartz et al. 2009; journal version JMLR 11 (2010)): learnability is uniform over all distributions, whereas the generalization studied here is for one distribution and one training sequence.
Let be a measurable space of samples, drawn from an unknown probability measure . Let be a set of hypotheses and a loss with for all (the paper's standing assumption, Sect. 1.1).
expectedLoss).avgLoss).firstN).The method generalizes w.r.t. (Definition 8) if
It is weakly robust w.r.t. (Definition 9) if there are sets with and
A set can be read as a family of perturbed copies of the training set that carries almost all of the probability of the test sample.
for every probability measure , every loss measurable in with values in , every learning method and every training sequence .
Milestones 1–2 give the sufficiency direction; milestones 3–4 give necessity.
Theorem 8 is a characterization, not a bound. The sufficiency half says a quantitative robustness property yields generalization. The necessity half says every method that generalizes along a sequence is weakly robust along it, so no generalization argument can avoid something of this shape. The paper remarks that -robustness for every implies weak robustness, which places Theorem 1's condition inside this characterization. Corollary 6, the almost-sure version (generalization with probability 1 iff almost-sure weak robustness), follows from Theorem 8 applied sequence by sequence.
The result is proved in the paper; no machine-checked proof of it is known. This mission contributes a formal statement of Definitions 8 and 9 in Lean, the two directions of the proof as reusable finite- and asymptotic lemmas, and a place to formalize the bounded-loss law of large numbers for a hypothesis that changes with (Eq. (9)), which Mathlib states for a fixed random variable.
The sufficiency direction is a direct estimate once the expectation of the average test loss is identified with the expected loss; the formal work is in handling the product measure and a set that need not be measurable.
The necessity direction is where care is needed. Eq. (9) is not the weak law of large numbers for a fixed function: the hypothesis changes with , so the concentration must be uniform in the hypothesis, which holds only because the loss is uniformly bounded. Lemma 2 negates a statement with an existential over sequences of sets and a limit; the naive reading "for each some works eventually" does not by itself produce a single sequence satisfying (6) with one limit.
MeasurableSpace, a Measure with IsProbabilityMeasure, an arbitrary type. The learning method is A : (n : ℕ) → (Fin n → Z) → H, the training sequence sStar : ℕ → Z, and Measure.pi (fun _ : Fin n => μ). Indices start at .ℝ≥0∞). The sets need not be measurable; their probability is the outer measure. "For infinitely many " is ∃ᶠ n in atTop.Measure.pi of coordinate functions, a Chebyshev or Hoeffding bound for averages of bounded i.i.d. variables uniform over a family of functions, and a diagonal-sequence construction. The uniform concentration lemma is reusable beyond this mission. Proofs of the milestones, and alternative routes to Eq. (9), are welcome.A learning algorithm maps a training set to a hypothesis. It generalizes when the loss it incurs on the training set is close to its expected loss on fresh data. The classical way to certify this bounds the complexity of the whole hypothesis class the algorithm may output, through its VC dimension, covering numbers or Rademacher complexity. A second approach, algorithmic stability (Bousquet and Elisseeff 2002), looks instead at how the output changes when one training point is replaced.
Huan Xu and Shie Mannor proposed a third notion, algorithmic robustness. An algorithm is robust if the sample space can be cut into finitely many cells such that a test point falling in the same cell as a training point incurs nearly the same loss as that training point. The notion came out of their earlier analyses of support vector machines and the Lasso as robust optimization problems (Xu, Caramanis and Mannor 2009). The conference version appeared at COLT 2010, and the journal version, which this mission follows, is Xu and Mannor, Machine Learning 86 (2012) 391–423.
Robustness is a property of the algorithm and not of its hypothesis class, so it applies to algorithms whose class has infinite VC dimension. The paper's main result for i.i.d. data is Theorem 1 (p. 396). This mission formalizes Theorem 1 together with the steps of its proof.
Throughout, is a measurable space of samples and is an arbitrary set of hypotheses. A loss satisfies for a constant . A training set is , and a learning algorithm is a map , written .
For a probability measure on , the expected error and the training error of the learned hypothesis are
Definition 2 (p. 396). For and , the algorithm is -robust if can be partitioned into disjoint sets such that for every ,
The partition is chosen once, before the training set. Only the tolerance may depend on .
For a partition , the cell count is the number of training points in . The Lean development uses expectedLoss, empiricalLoss, cellCount and IsRobust in the namespace XuMannorRobust.Standard.
Let be -robust and let consist of i.i.d. draws from . Then for every , with probability at least ,
The constants are the paper's and are kept as printed. , , , , , and the algorithm are all universally quantified.
Theorem 1 is the base result of the robustness framework. The later results of the same paper are extensions of it:
Its complexity term depends only on the number of cells , not on any capacity measure of . This is why it gives bounds for algorithms such as support vector machines, Lasso, feed-forward networks and principal component analysis (Sect. 6 of the paper). For those, is a covering number of the sample space. Section 8 of the paper shows that a weak form of robustness is also necessary for generalization.
Theorem 1 is a published result with a short proof. What a formalization adds:
A search of the platform (2026-09-26) found no formal statement of Theorem 1, Definition 2, or the Bretagnolle–Huber–Carol inequality for multinomial vectors. Hoeffding's inequality is already available there in proved form.
The deterministic step, Eq. (4), splits the expected loss over the cells. It then compares the loss within each cell with the loss at the training points in that cell. This needs integration over a partition and some care with cells of -measure zero, where the conditional expectation in the paper's chain is undefined.
The main obstacle is the probabilistic step. The quantity is an deviation of a multinomial vector. A coordinate-wise Hoeffding bound followed by a union bound over the coordinates gives a bound whose deviation level grows linearly in . That is not , and it does not give the constant of Theorem 1. The difficulty is to obtain the exact exponential rate for the deviation as a whole, with no loss in the constant.
Samples are a type Z with a MeasurableSpace, training sets are Fin n → Z, the algorithm is a function (Fin n → Z) → H, and the loss is H → Z → ℝ. The partition is a family C : Fin K → Set Z that is pairwise disjoint, measurable, and covers Z. Empty cells are allowed, as in the paper. The i.i.d. sample law is Measure.pi (fun _ => μ) with μ a probability measure, and enters as a real number.
"With probability at least " is encoded as an upper bound on the outer measure, under , of the set of training sets where the inequality fails. This needs no measurability of .
The paper ignores measurability. The formalization restores it: every is measurable and every cell is a measurable set. Together with this makes the expected error a genuine expectation.
The theorems assume . The Bretagnolle–Huber–Carol step assumes , because the printed inequality is false for . No upper bound on is imposed: for the radicand is negative, the square root evaluates to , and the statements remain true.
Two trivializing readings of Definition 2 are ruled out:
IsRobust the existential over the partition precedes the universal over training sets. If the order were swapped, every algorithm with a -valued loss would be -robust, since it could take the two level sets of its own learned loss as cells. Theorem 1 would then fail for a memorizing classifier.Beyond the paper's text, a complete development needs the integral over a finite measurable partition, a Hoeffding bound for indicator averages, and a union bound over the subsets of Fin K. The multinomial concentration inequality is reusable beyond this mission, in histogram estimators, discretization arguments and the covering-number examples of the paper. Contributions are welcome at every level: proofs of the milestones, and alternative proofs of the Bretagnolle–Huber–Carol step (for instance via the method of types).
Traffic information systems (TIS) such as navigation apps send drivers private, noisy signals about the state of the road network: incidents, weather, closures. When several such systems coexist, their subscribers act on different information, and the congestion each population experiences depends on how all of them route. A question then arises for transport planners and for the information providers themselves: if travelers are free to choose which system to subscribe to, which market shares of the competing systems are stable?
Wu, Amin and Ozdaglar (Operations Research 69(1):148–163, 2021; preprint arXiv:1808.10590) model this situation as a Bayesian routing game with heterogeneous information and answer the question exactly: the equilibrium adoption rates are the minimizers of a convex function of the population sizes, the equilibrium value of a weighted potential. This mission formalizes that characterization (Theorem 4 of the paper) together with the results its proof rests on. A companion mission (Value of Information in Bayesian Routing Games I) formalizes the paper's other main result, the sign and monotonicity of the relative value of information between two populations.
A Bayesian routing game has a single origin–destination pair, a finite set of edges and a finite nonempty set of routes (each route a set of edges), and a finite set of network states . Travelers of total demand are split into populations , one per TIS; population has size , where the size vector lies in the simplex . Each population receives a signal (its type) from a finite set ; states and type profiles are drawn from a common prior . Edge in state has cost at load , positive, strictly increasing and differentiable.
A strategy profile assigns to each population and type a split of its demand over routes, with ; these form the polytope . It induces route flows and edge loads . A traveler of population with signal forms the belief and evaluates the expected route cost . A Bayesian Wardrop equilibrium (BWE) is a in which every type uses only routes of minimal expected cost. The equilibrium population cost is
The weighted potential is , and is its equilibrium value. In route-flow form, is the same expression in terms of ; route flows satisfy linear constraints (14a)–(14c) (a separability condition across populations, total demand , nonnegativity) and one information impact constraint per population, , where measures how much of the demand reacts to population 's signal. Let be the set of minimizers of subject to (14a)–(14c) only, and
In the two-stage game, travelers first choose a TIS, inducing , and then play . A size vector is a vector of equilibrium adoption rates if no traveler gains by switching TIS:
For every and every BWE of ,
With the existence of a BWE for every , this is the paper's statement that the set of equilibrium adoption rates is .
A separate item states the existence of a BWE for every .
The result. Theorem 4 reduces a question about a two-stage game with a continuum of travelers and private signals to the minimization of one convex function over a simplex. It shows that the stable market shares form a convex set, generally not a single point, so each system's equilibrium adoption rate ranges over an interval; and that this set is determined by the joint information environment of all systems, not by each system's signal alone. On the equilibrium edge load does not depend on the shares at all, which identifies when changes in market shares leave congestion unchanged.
Formalizing it. The proofs of Theorem 1, Proposition 2 and Proposition 5 are in the paper's online e-companion, and Lemma 5 relies on sensitivity results for parametric convex programs cited from the literature. No part of this development has, to our knowledge, been machine-checked. A complete formalization would produce a verified potential-game characterization of Bayesian Wardrop equilibria with heterogeneous information and a verified directional-derivative formula for the optimal value of a parametric convex program; nothing comparable is currently on the platform (the existing Wardrop development covers complete information only).
The direction " implies (31)" is not a pointwise statement about costs: it follows from being the argmin of together with the formula linking directional derivatives of to cost differences. Both are hard. The derivative formula (26) is a statement about the optimal value of a convex program whose feasible set moves with ; its standard proofs pass through uniqueness of Lagrange multipliers, which fails exactly at the degenerate size vectors () that Theorem 4 must cover, since an unused TIS is a legitimate outcome. The identity needs the route-flow reformulation (Proposition 2), in which the size vector enters only through the information impact constraints, and the uniqueness of the minimizing edge load. The natural first idea, comparing population costs directly at a given equilibrium, gives no handle on which size vectors make them equal.
The Lean development lives in the namespace BayesRouting.Adoption. Populations, types, states, edges and routes are finite types; type spaces and the route set are nonempty; routes are edge sets. The game is a structure whose fields include the paper's standing assumptions: the prior is a probability distribution, , and each cost is positive on nonnegative loads, strictly increasing and differentiable (on all of , which loses no generality). One assumption is added: every type profile has positive probability. Without it the equilibrium edge load need not be unique and the beliefs can be undefined; it excludes the paper's Example 2(i) (perfectly correlated signals).
Conventions: size vectors range over the probability simplex; is the infimum of over and is only compared at points of the simplex (outside it the feasible set can be empty and the value is a default); is the last form of the paper's (7), well defined when ; is the maximum over reference profiles, which equals the paper's value on flows satisfying (14a); equilibrium statements are made for every BWE rather than for "the" equilibrium; and similar sets are argmin sets. Lemma 5 is stated for the directions with (otherwise leaves the simplex); is allowed.
A trivializing formalization is ruled out: the existence of a BWE is its own item, so "for every BWE" is not vacuous, and is defined by (30) from the flow problem (28), not as the argmin of , so the goal is not a restatement of Proposition 5.
Infrastructure a complete development needs: KKT conditions for convex programs with linear constraints, convexity of integrals of increasing functions, compactness arguments for existence of minimizers, and one-sided directional derivatives of optimal-value functions. The last two are reusable well beyond this mission. Proofs of any item, and of auxiliary lemmas such as Proposition 1 of the paper (feasible route flows form the polytope ), are welcome.
A two-stage stochastic linear program with fixed recourse chooses a first-stage decision before a random vector is observed, and then pays for a cheapest corrective action once is known. It is the basic model of planning under uncertainty in operations research: capacity expansion, production planning with random demand, and energy dispatch are all written in this form, and every decomposition algorithm of the field (L-shaped, stochastic decomposition, progressive hedging) works on it.
Roger J.-B. Wets' survey Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program (SIAM Review, 1974) collected the structural theory of this model: where the problem is feasible (§4), what the expected cost looks like as a function of (§7), and when the resulting convex program is well behaved (§8). This mission formalizes the second chain, from the polyhedral structure of the recourse function to the stability of the deterministic equivalent program: the existence of an optimal Lagrange multiplier for the first-stage constraints. Stability is what makes the optimal value react at a bounded rate to perturbations of the first-stage right-hand side, and it is the hypothesis under which dual and decomposition methods have something to converge to.
The data are a random element with , , and an matrix, distributed according to a probability measure . The recourse matrix (), the first-stage matrix () and are fixed. The recourse function is
equal to if the second-stage program is infeasible and if it is unbounded.
The weak covariance condition (Definition 2.2) requires , and to be integrable for all indices; it does not require , or themselves to be integrable. The paper also assumes throughout that has full row rank (p. 312).
Expectations use the paper's integral: positive part minus negative part, with each part infinite if its integral diverges or the integrand is infinite on a set of positive measure, and . The expected recourse is and the objective is
The induced constraints are , where and is the support of the distribution of . The fixed constraints are , and . The deterministic equivalent program (8.2) is to minimize over .
A convex program of the form with finite value is stable (Definition 8.1(iv)) if there is with for all , . Equivalently, the dual obtained by perturbing is solvable and has no duality gap.
If the weak covariance condition holds, has full row rank, is a polyhedron and the program is finite, , then
Stability of (8.2) is the regularity property that the dual and sensitivity theory of two-stage programs relies on. It gives a finite Lagrange multiplier for the first-stage constraints, a supporting hyperplane of the perturbation function at , and hence a bounded rate of change of the optimal value under perturbations of . The route through Theorems 7.6 and 7.7 also yields facts that are used on their own: the objective is a convex function that is either finite or identically on the feasible region, and it is Lipschitz with a constant controlled by the weak covariance moments.
The results have been proved since 1974, and Lemma 8.9 is cited there to Walkup and Wets (1969). As far as the platform's catalog shows, none of them is formalized for a general distribution. The platform has finite-scenario versions of related facts from Birge and Louveaux's textbook, Chapter 3: StochasticProg.Recourse.thm6a_Q_lipschitz_convex_finite (the expected recourse is finite, convex and Lipschitz on for finitely many scenarios) and StochasticProg.Recourse.thm5a_K2_closed_convex. A complete development would supply the general-distribution versions, with the paper's own extended integral.
The obvious argument for Theorem 7.7 integrates a pointwise Lipschitz constant of . It fails unless that constant is integrable, and the weak covariance condition, not integrability of , is what has to deliver this, uniformly over the finitely many second-stage bases.
For the goal, convexity and finiteness of the program are not enough. The paper's Example 8.5 has a finite convex deterministic equivalent with an infinite duality gap, and the counterexample under Formalization scope has a finite value and no multiplier. When the domain of has curved boundary, the perturbation function can have infinite slope at ; the polyhedral hypothesis on is what excludes this.
Fin n → ℝ; matrices are Matrix (Fin _) (Fin _) ℝ; row vectors of the paper (, , ) enter through dotProduct. The law is a probability measure on (Fin n → ℝ) × (Fin n̄ → ℝ) × (Fin m̄ → ℝ) × (Fin m̄ → Fin n → ℝ). is the platform definition KallMayer.Recourse.PointwiseRecourse, an EReal-valued infimum. Supports are MeasureTheory.Measure.support.lintegral of the positive part minus lintegral of the negative part, with whenever the positive part is . This is the paper's ; Mathlib's EReal subtraction resolves the other way. A Bochner integral of toReal would be for non-integrable integrands and make every expected-cost statement trivial, and it is not used. is a Bochner integral, legitimate because Definition 2.2 makes each integrable.Integrable.ConvexOn of toReal on the finite branch.PointedCone.FG/DualFG in Mathlib), LP duality with values, the paper's extended integral, and a Kuhn–Tucker theorem for convex programs with polyhedral constraints (Rockafellar, Convex Analysis, Thm 28.2). Corollary 7.3 and Lemma 8.9 contain no probability and are reusable across convex analysis. Proofs of any milestone, and lemmas on the paper's extended integral (monotonicity, subadditivity), are welcome.A two-stage stochastic program with recourse is a linear program in which a decision is taken before a random vector is observed, and a corrective (recourse) decision is taken afterwards at a cost. It is the basic model of planning under uncertainty in operations research: capacity expansion, production planning, energy dispatch and inventory models are routinely written this way. Before any algorithm can be applied, the model has to be reduced to a deterministic equivalent program in alone, and the first question is which are admissible at all: the random second-stage constraints induce constraints on that are not written down anywhere in the data.
Roger J.-B. Wets's survey (SIAM Review 16(3), 1974) settled this question for fixed recourse (the recourse matrix is not random) under a weak moment condition on the data. Its §4 shows that the natural definitions of the induced feasibility region agree, that the region is always closed and convex, and that it is a polyhedron, described by finitely many deterministic linear inequalities, whenever the technology matrix is fixed. The last fact is what makes decomposition methods such as the L-shaped method of Van Slyke and Wets (1969) terminate with finitely many feasibility cuts.
Timeline: Dantzig (1955) and Beale (1955) introduce linear programs under uncertainty, under assumptions that make every feasible (relatively complete recourse). Wets (1966) and Kall (1966) begin studying the feasibility region without that assumption; Wets (1966c) introduces the polar matrix used for the polyhedrality result. Walkup and Wets (1967) treat random . The 1974 survey collects these results in the form formalized here.
The data are a fixed real matrix and a random vector with , , and an matrix. The law of is a probability measure on the product space, and its support is the smallest closed set of measure one. The recourse function is
equal to when the program is infeasible and when it is unbounded below. The expected recourse uses the paper's integral: the sum of the positive part and the negative part , with .
The weak covariance condition (Definition 2.2) asks that , and be integrable for all . Write . The candidate feasibility sets for the induced constraints are
A convex polyhedron is a set given by finitely many linear inequalities; and are polyhedra.
If is fixed and satisfies the weak covariance condition, then
so is a closed convex polyhedron. The number of inequalities is not fixed in advance, and may be empty.
Theorem 4.1 and Corollary 4.5 show that three different notions of second-stage feasibility (almost sure, on the support, finite expected cost) coincide, and that feasibility depends only on the distribution of . This justifies computing the feasibility region from the support alone, which is what feasibility-cut algorithms do. Theorem 4.7 guarantees that the deterministic equivalent program is a convex program over a closed convex set, with no moment condition. Theorem 4.10 shows that with a fixed technology matrix the induced constraints are finitely many linear inequalities, even when has an unbounded continuous distribution, so the deterministic equivalent program has a polyhedral feasible region.
The results are classical and proved in the paper. None of them is formalized on Prove2Me for a general distribution. The platform has the finite-scenario analogue of Theorem 4.7's first part, StochasticProg.Recourse.thm5a_K2_closed_convex (Birge and Louveaux, Ch. 3, Thm 5(a)), for finitely many scenarios; it is related work, not a special case in the Lean sense, because its model differs. The mission produces a machine-checked account of the measure-theoretic part (supports, pushforwards, an extended-valued integral with a nonstandard convention) and of the polyhedral part (Minkowski–Weyl for cones).
Two steps resist the obvious approach. First, needs an integrable upper bound for the positive part of on the whole support. is only piecewise linear in , can equal , and , , are not assumed integrable separately, so no single dominating function is at hand; only the products controlled by the weak covariance condition are integrable. Second, Theorem 4.10 intersects infinitely many polyhedra , and an infinite intersection of polyhedra is in general only closed and convex (Theorem 4.7). Showing that finitely many inequalities suffice without any assumption on the shape of the support of is the content of the goal, and the resulting system may be inconsistent, in which case .
Vectors are Fin k → ℝ and matrices are Matrix (Fin m) (Fin n) ℝ; the paper's row vectors and suppressed transposes become Matrix.mulVec. The data space is with its Borel structure, and is a probability measure on the whole space (the paper's sample space only carries ). Readings fixed by the formalization:
Integrable with respect to .EReal subtraction () and the Bochner integral of toReal (zero for non-integrable functions) would both make wrong and are not used.Measure.support; is the support of the pushforward under the (continuous, hence measurable) projection onto .A trivializing formalization is ruled out: a polyhedron indexed by an arbitrary type or by the support would make Theorem 4.10 a restatement of the first part of Theorem 4.7, and a Bochner-integral would make . Neither is used.
A complete development needs Minkowski–Weyl for finitely generated cones (available in Mathlib as PointedCone.FG / DualFG), closedness of finitely generated cones, supports of pushforward measures, and simplicial covers of (Carathéodory). The support and integral lemmas are reusable for every result about recourse functions with general distributions; contributions of such lemmas as separate theorems are welcome.
The periodic-review inventory model with a fixed ordering cost is one of the basic models of operations research. When every order incurs a set-up cost in addition to holding and shortage costs, the optimal replenishment rule over an infinite horizon is, under standard convexity assumptions, a stationary policy: whenever the stock falls below the reorder point , order up to the level . Existence of such an optimal policy goes back to Scarf (1960) and Iglehart (1963). Knowing that an optimal policy exists does not say how to find one, and the average cost of an policy is neither convex nor unimodal in .
Veinott and Wagner (Management Science 11 (1965) 525–552) gave an exact algorithm. It proceeds in three steps: (i) compute integers bounding an optimal policy; (ii) find the set of all policies within those bounds that minimize the cost for starting stocks below ; (iii) choose from a policy that is optimal for every starting stock. This mission formalizes the theory behind Step iii. It is the third mission of a series on the paper: mission I treats the renewal closed form of the discounted cost, mission II the bounds of Step i.
Demands are independent non-negative integer random variables with common distribution and finite mean. Following the paper's Eq. (2), the unit purchase cost and the holding and penalty costs are combined into a single function , assumed convex with as ; the set-up cost is and is the discount factor.
A stationary policy, with integers , sets the stock after ordering to
and the stock evolves as from . Its discounted cost is
where for and , and its equivalent average cost is .
A policy is optimal for a set of integers if, for each , it minimizes over all policies; it is optimal if it is optimal for every integer . Under a fixed policy, is accessible from if for some .
Below the reorder point the cost does not depend on the starting stock; its value is written with . The bounds are: the smallest minimizer of ; the smallest integer with (21); the smallest integer with (22); the smallest integer with (23). The candidate set consists of the policies with , that minimize among such policies.
For and : if is optimal and every with
is accessible from under , then is optimal.
Theorem 2 turns the final selection step of the algorithm into a reachability check on the demand distribution: a policy of is certified optimal without comparing average costs at every starting stock. Its corollaries give checkable sufficient conditions; for example (Corollary 2.2) if for , the policy of with the largest reorder point is optimal, which covers Poisson and negative binomial demand. Theorem 1 separately reduces the comparison of two policies to finitely many starting stocks.
The results are proved in the paper (Section 4 and Appendix §3). No machine-checked version is known: the platform has no discrete inventory chain, no discounted cost of a stationary policy on , and no accessibility notion for such a chain. The mission produces these objects together with the paper's selection theory on top of them.
Theorem 1 needs a renewal decomposition at the first passage of the stock below , carried out for expectations over an unbounded integer state space with a discounted infinite sum. Lemma 1 is the delicate step. The paper's argument compares the policy with a hybrid policy that follows until the stock first reaches and then switches to an optimal policy; the inequality "the hybrid cannot be better than the optimal policy" requires that some stationary policy is optimal among all ordering policies, including non-stationary ones. That existence result is cited by the paper (Section 2), not proved there. A proof of Lemma 1 within the class of policies alone does not go through, because the hybrid policy is not an policy.
All objects live in the namespace VeinottWagnerSS.Selection. The model is the structure Model: the demand distribution φ : PMF ℕ with finite mean, K ≥ 0, and G : ℤ → ℝ convex (non-decreasing forward differences) and tending to at both ends. The unit cost , the function and the lead time do not appear (the paper's own reduction, Eq. (2), p. 529). Stock levels are integers. stateLaw is the law of , obtained by iterated PMF.bind; fCost is the expected discounted cost of that chain as a real series, which converges absolutely for because every lies in . aCost is times fCost. Accessible uses the law of with strictly. Optimality is among policies (p. 536); the class of general ordering policies is not formalized.
The bounds are infima of sets of integers; under the standing assumptions and these sets are nonempty and bounded below, so each bound is the least integer the paper describes. is defined as , the cost at the starting stock just below ; that this is the common value for every is milestone 1.
The standing assumptions are kept in every statement, including Theorem 1 and milestone 1, which do not need them; Lemma 1 and Theorem 2 are true only because of them. No printed slip was found in the three results.
Trivializing formalizations are excluded: is the expected cost of the stock process, not a closed formula or a fixed point of a recursion, so milestone 1 is not definitional; the bounds are the least integers of (21)–(23), not arbitrary integers, so is determined by the data; the goal does not assume that is optimal below , and Lemma 1 assumes optimality only at the single starting stock .
Useful contributions beyond the milestones: summability lemmas for fCost, the Markov (one-step) equation for fCost, the first-passage decomposition, and, for Lemma 1, a formalization of general ordering policies with the existence of an optimal stationary policy. The chain and cost definitions are reusable for other results of the paper (Theorem 3, Corollaries 2.1 and 2.2).
The periodic-review inventory problem with a fixed ordering cost is one of the basic models of operations research. A firm reviews its stock once per period, may order at a cost per order plus a unit cost, and then faces a random demand; unmet demand is backlogged. Scarf (1960) and Iglehart (1963) showed that for this model an policy is optimal: order up to whenever the stock falls below , and otherwise do nothing. That result tells a manager what shape a good policy has, but not which pair to use.
Veinott and Wagner, Computing Optimal (s, S) Inventory Policies (Management Science 11 (1965) 525–552), gave the first practical algorithm for computing an optimal pair when demand is discrete. The algorithm rests on a closed form, their Eq. (11), for the discounted cost of an arbitrary stationary policy, obtained by a renewal argument in their Section 3. The same closed form, in the undiscounted limit, is the classical expression of the long-run average cost of an policy used throughout inventory theory textbooks.
Timeline:
Demands are independent random variables on with common distribution , . Write for the -fold convolution of ( is the point mass at ) and for its distribution function, so .
In period the stock before ordering is and the stock after ordering is ; then . With the unit purchase cost eliminated as in the paper's Eq. (2), the cost of period is , where is the set-up cost, , for , and is the one-period cost. Period is discounted by with .
A stationary policy, for integers , sets if and otherwise. Its total expected discounted cost from is
and its equivalent cost per period is .
The renewal quantities are
the latter being the discount renewal function,
If is the first period in which cumulative demand exceeds , then is the expected discounted one-period cost over periods from stock without ordering, and .
With ,
Eq. (11) turns the cost of an policy, an infinite series over the trajectories of a controlled Markov chain, into a finite expression in , and the renewal sequence , which the paper computes by a one-line recursion. Everything in the paper's Section 4 builds on it: the search for an optimal pair minimizes over a finite box, and the undiscounted limit gives the long-run average cost .
The result is classical and proved in the paper. What this mission adds is a machine-checked derivation from the definition of the policy's expected cost, including the renewal step, which the paper states in one sentence ("a renewal of the process takes place"). It also produces a reusable Lean layer: discrete convolution powers, the discount renewal function, and the law of an -controlled inventory chain. To the best of our knowledge none of these is formalized in Mathlib or on the platform.
The paper's argument conditions on the random time at which the process renews and uses the strong Markov property at that time. In the formalization, is defined as a sum over periods of expectations under the law of . Relating that sum to one that splits at the random time requires either a stopping-time decomposition of the chain or an explicit accounting of the law of before and after the first order. Neither is a direct computation. A second difficulty is the interchange of the infinite sum over periods with the sum over states , which has infinitely many states reachable (demand is unbounded below). The renewal equation (milestone 4) alone does not determine without the fact that for , which comes from (9).
VeinottWagnerSS.RenewalCost. Stock levels are integers, demands natural numbers; and enter , , through Int.toNat, which is exact because the statements assume or .tsums. is defined by the series (7) and by the first line of (9), i.e. through the law ; the paper's derivations of these series from are not formalized. For all series converge for every , because after period the stock after ordering lies in the finite set .Contributions welcome: proofs of the milestones, general lemmas on discrete renewal sequences and convolution powers, and a first-passage decomposition for integer-valued Markov chains, which is reusable beyond this mission.
Markov chain Monte Carlo (MCMC) estimates an expectation by the average of along a Markov chain whose invariant distribution is . Many chains share the same : every Metropolis–Hastings acceptance rule that satisfies detailed balance, every mixture of such kernels, every choice of proposal. Practitioners need a criterion for preferring one of them. The standard yardstick is the asymptotic variance of the ergodic average, the constant in the Markov chain central limit theorem. A smaller asymptotic variance means fewer iterations for the same Monte Carlo error.
Peskun (1973) compared chains on a finite state space through a partial order on transition matrices: if one reversible matrix moves off the diagonal at least as much as another, entry by entry, its asymptotic variances are no larger, for every function. That result justifies the Metropolis–Hastings acceptance probability as the best possible among reversible acceptance rules. It covers only finite state spaces, while MCMC is used almost exclusively on continuous or mixed ones.
Tierney (1998) extended Peskun's theorem to general state spaces, using the spectral approach of Kipnis and Varadhan (1986) for reversible chains. The theorem is the one usually cited when an MCMC paper argues that one sampler dominates another; Mira (2001) surveys orderings built on it.
Let be a measurable space in which singletons are measurable, and let be a probability measure on . A Markov kernel assigns to each a probability measure , measurably in . It acts on functions by . The measure is invariant for if for every . The kernel is reversible with respect to (satisfies detailed balance) if
that is, for all . Reversibility implies invariance.
Write , for the square-integrable functions and .
Off-diagonal domination. For kernels , (OffDiagDominates π P₁ P₂) if for -almost every ,
So from almost every state moves to every region at least as readily as , and the kernels differ only in the probability of staying put.
The chain and its asymptotic variance. For a Markov kernel , let be the Markov chain with initial distribution and transition kernel (chainMeasure π H, a measure on paths ). For put (pathSum f n) and
The lag inner products are (lagInner π H f k), and for the regularized variance is (vLam π H f lam).
Let be Markov kernels reversible with respect to , , and . Then both asymptotic variances exist in and
No rate, constant or regularity of the kernels is fixed. The statement is the ordering itself, valid for every reversible pair and every .
The result. Theorem 4 turns a pointwise, one-step comparison of kernels, which is easy to check, into a comparison of the quantity that governs Monte Carlo error. Its main consequence, drawn in §3 of the paper, is that the Metropolis–Hastings acceptance probability gives the maximal kernel in the off-diagonal order among reversible Metropolis–Hastings kernels with a given proposal. It is therefore optimal in asymptotic variance, on arbitrary state spaces. Proposition 5 of the same paper (a separate mission in this series) combines with it to show that a single Metropolis–Hastings kernel built on a mixture proposal beats the mixture of the component kernels. Later orderings of samplers (Mira 2001; Andrieu and Livingstone 2021) take this theorem as their base case.
Formalizing it. The theorem has been proved since 1998. No machine-checked version exists for general state spaces, and none of its milestones is on the platform. The formalization produces reusable infrastructure: the asymptotic variance of a stationary chain as an extended-real limit on Mathlib's Ionescu–Tulcea path measure, the facts for reversible kernels (self-adjointness, contraction, the covariance formula for path sums), and the positivity of under off-diagonal domination. Each of these is used again in any formal treatment of MCMC efficiency or the Markov chain central limit theorem.
The direct approach compares the two finite- variances. This fails, and not just technically: the paper exhibits two doubly stochastic, symmetric matrices with for which the variance of is 15.4 under and 14.8 under (p. 7). Off-diagonal domination orders the lag-one covariances, but higher-order correlations "need not be ordered" (p. 5). The ordering appears only in the limit, and only for reversible kernels. The comparison must pass through an object that sees all lags at once and is monotone along the segment , and that object involves resolvents of operators on . The limit may be infinite, so every comparison must be made in . Mathlib has neither the spectral measure of a self-adjoint operator nor the Kipnis–Varadhan theory.
The state space is {E : Type*} [MeasurableSpace E] with [MeasurableSingletonClass E] wherever off-diagonal domination appears. This is an assumption the paper leaves implicit: must be an event. is a probability measure and all kernels are Markov kernels. Reversibility is Mathlib's Kernel.IsReversible, invariance is Kernel.Invariant. The function is measurable with MemLp f 2 π and, for , ∫ f ∂π = 0; measurability picks a representative of the class and costs nothing. The chain is Kernel.trajMeasure started from . The sum runs over , not . Variances are Mathlib's evariance in , and is a Tendsto limit in ℝ≥0∞, so an infinite asymptotic variance is represented. The goal asserts the existence of both limits rather than assuming it, so it cannot hold vacuously. Neither it nor any milestone specializes to finite , to Metropolis–Hastings kernels, or to a chain started from a point. Lemma 3 assumes invariance only, and the theorem requires reversibility, as printed.
Two statements depart in form from the page. The finite- variance identity and are written through the moments (a Neumann series) instead of through the spectral measure and the resolvent . The two forms agree for a self-adjoint contraction, and this is noted in each item. The paper's appeal to the spectral theorem and to Kipnis and Varadhan (1986) is not restated as an item: a complete development needs it, or an equivalent argument, as part of the proof. Proofs of any milestone, and reusable lemmas on the path measure (stationarity and the marginal laws of ), are welcome.
The Metropolis–Hastings algorithm (Metropolis et al. 1953; Hastings 1970) is the basic construction of Markov chain Monte Carlo. It turns a target probability distribution , known only up to a constant, into a Markov chain that has as its invariant distribution. Bayesian computation depends on it, and a sampler is usually designed by proving one property: reversibility, or detailed balance, with respect to .
For discrete state spaces, or when every measure involved has a density with respect to a common reference measure, the condition on the acceptance probability is the familiar . Samplers used in practice often do not fit this setting: deterministic involutive proposals, mixtures of proposals with different supports, and Green's dimension-changing moves for model selection (Green 1995) have no common density. Each of these was treated separately in the literature. Tierney (1998) gives one necessary and sufficient condition that covers all of them, on an arbitrary measurable state space. This mission formalizes that condition.
Let be a measurable space, with no topological or countability assumption. Let be a probability measure on , the target. Let be a Markov transition kernel on , the proposal, and let be a measurable function, the acceptance probability. From the current state , a candidate is drawn from and accepted with probability ; otherwise the chain stays at . The resulting Metropolis–Hastings kernel (mhKernel Q α) is
A kernel satisfies detailed balance with respect to if the two measures and on are equal (Eq. (2)). Equivalently, for all measurable , which is Mathlib's Kernel.IsReversible P π.
Put (π ⊗ₘ Q), and let be its image under the swap . A symmetric split (IsSymmetricSplit) is a measurable set with , such that and are mutually absolutely continuous on and mutually singular on its complement . Informally, consists of the pairs between which the proposal can move in both directions. A ratio version (IsRatioVersion) is a measurable that is a density of (the restriction of to ) with respect to , and satisfies at every point.
For every , , as above and every symmetric split and ratio version for :
The paper phrases the left side as condition (4), , which its text identifies with (2) for the kernel (1). The goal states it for the kernel itself.
that is, the rejection mass on the diagonal does not affect reversibility.
§2, special case 1 (pp. 3–4). If and for a -finite , then is a symmetric split, is a density of with respect to , and detailed balance is equivalent to the two conditions holding -almost everywhere.
Theorem 2 lets reversibility be checked in the same way for every Metropolis–Hastings variant: compute and for the proposal, then verify (i) and (ii). The paper derives from it the reversibility of the standard acceptance probability on (and off ), and the three special cases of §2 are instances. Together with Mathlib's Kernel.IsReversible.invariant, it yields that is invariant for the sampler. This is the correctness statement of every MCMC method built on the Metropolis–Hastings kernel. Missions II and III of this series (Peskun ordering; mixture proposals) take reversible Metropolis–Hastings kernels as their objects.
The result is proved in the paper. The mission adds a machine-checked proof at the paper's full generality: no densities, no dominating measure, no countability of . The platform currently has only finite-state statements (MarkovMixing.metropolis_stationary, a sufficiency direction on a Fintype state space with a matrix proposal), so neither the general kernel nor the converse direction is formalized there.
The obvious argument works with densities: write both sides of (3) as densities with respect to one reference measure and compare them pointwise. On a general space no such reference is given for and together, and even yields densities only up to null sets. Pointwise comparison of densities is therefore not available, and the statement mixes three kinds of almost-everywhere claim (-a.e., -a.e., and a.e. for the restrictions to and ). The Lean statement also has to hold for every version of and , not one convenient choice. Milestone 2 has its own content: the diagonal part of is a measure concentrated on the diagonal, which need not be a measurable set, and its symmetry has to be shown without that measurability.
{E : Type*} [MeasurableSpace E] with nothing else: no measurable singletons, no topology, no countable generation. π : Measure E with [IsProbabilityMeasure π] and Q : Kernel E E with [IsMarkovKernel Q].α : E × E → ℝ≥0∞ with the hypotheses Measurable α and ∀ p, α p ≤ 1, which is the paper's measurable . The kernel is Q.withDensity (fun x y => α (x, y)) + Kernel.withDensity Kernel.id (fun x _ => ∫⁻ u, (1 - α (x, u)) ∂(Q x)). The measurability hypothesis rules out the junk zero kernel that Kernel.withDensity returns for a non-measurable density.Kernel.IsReversible. It agrees with the measure identity (2) because rectangles determine a finite measure on .IsSymmetricSplit and IsRatioVersion (a symmetric Lebesgue-type decomposition of a measure against its transpose) are reusable for any reversibility argument on product spaces. Lemmas on Measure.map Prod.swap of compProd and withDensity, and on the symmetry of measures carried by the diagonal, are also welcome contributions.A variational inequality asks for a point of a convex set at which a vector field points "inward" against every feasible direction. The format covers the first-order optimality conditions of constrained optimization, nonlinear complementarity problems, traffic and economic equilibria (Wardrop, Walrasian, Nash–Cournot), and systems of nonlinear equations; see Harker and Pang's survey (Math. Programming 48, 1990) and Facchinei and Pang's monograph (Springer, 2003).
When the map has no special structure (not strongly monotone, not Lipschitz with known constant, not affine) and the feasible set is a general closed convex set, the practical algorithms are projection methods. The oldest is Korpelevich's extragradient method (1976). Without a known Lipschitz constant, extragradient-type methods need a linesearch in which every trial point costs one projection onto the feasible set, and projection onto a general convex set is itself an optimization problem.
Solodov and Svaiter (SIAM J. Control Optim. 37 (1999) 765–776) proposed a method that spends exactly two projections per iteration, whatever the linesearch does, and proved global convergence under only continuity of the map and a generalized monotonicity condition weaker than pseudomonotonicity. The method, often called the hyperplane projection method, is a standard reference point for later projection and extragradient-type algorithms.
Timeline:
Work in with the Euclidean inner product and norm . Let be closed and convex and continuous. The problem is to find with
Its solution set is . The projection onto a nonempty closed convex set is . The projected residual is ; its zeros are exactly the points of .
Condition (1.2) requires, for every ,
It holds when is monotone or pseudomonotone, and in cases where is neither.
Algorithm 2.1. Fix and . Given : if , stop. Otherwise let be the smallest nonnegative integer with
set , , , and
The hyperplane separates from .
If is closed and convex, is continuous, and (1.2) holds, then every sequence generated by Algorithm 2.1 converges to a single point of :
The theorem fixes no rate and no constant; it asserts convergence of the whole sequence, not only of a subsequence.
Theorem 2.1 gives global convergence of a projection method for variational inequalities with no Lipschitz constant, no monotonicity and no knowledge of the problem beyond continuity and (1.2), at a fixed cost of two projections per iteration. Condition (1.2) covers pseudomonotone maps, which arise as gradients of pseudoconvex functions and in equilibrium models where monotonicity fails. The separating-hyperplane-and-project template of the proof is reused throughout the later literature on projection, proximal and hybrid methods for monotone inclusions.
The result has been proved since 1999. To the best of available knowledge no machine-checked proof of it, or of any convergence theorem for a projection method for variational inequalities, exists in Lean or Mathlib. This mission produces the statement and the supporting layer: a Euclidean projection onto closed convex sets with its standard inequalities, variational inequality solution sets, the projected residual, and a formal model of an Armijo-type linesearch algorithm with termination.
The Fejér-type inequality (2.6) quickly gives bounded iterates and . The obvious next step, concluding , fails: nothing prevents the stepsizes from tending to zero, and in that regime the product going to zero says nothing about the residual. This regime is where the minimality of and the continuity of enter, and it is the step a naive formalization (for instance one that drops minimality, or fixes the stepsize) cannot reach. A second subtlety is that (1.2) is needed at an accumulation point that is only known to lie in at the end of the argument, which is why the condition must hold for every . Finally, subsequential convergence must be upgraded to convergence of the whole sequence to one solution; convergence of a subsequence, or of the distance to , is strictly weaker.
EuclideanSpace ℝ (Fin n) (not Fin n → ℝ, whose norm is the sup norm). The accumulation-point step needs finite dimension; no Hilbert-space generalization is intended.projOnto K x is a nearest point of to when one exists, chosen by Classical.choose, and the junk value otherwise. On nonempty closed convex sets it is exactly ; the paper only projects onto such sets (, , ), so the junk value is never reached under the hypotheses.x : ℕ → ℝⁿ with Armijo indices k : ℕ → ℕ (predicate IsAlg21Run). If the method has stopped and the run stalls, ; otherwise is the least index satisfying (2.1) and . A stalled point is a solution, so finitely terminating runs are included in the goal.exists_norm_eq_iInf_of_complete_convex and norm_eq_iInf_iff_real_inner_le_zero), firm nonexpansiveness, the explicit projection onto a halfspace, and a bounded-sequence subsequence argument in . The projection lemmas are reusable for any projection-type method; contributions proving them as standalone lemmas are welcome.