All missions

Motivation

Chapter 7 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) asks when a limit of functions inherits the properties of its members. Pointwise convergence preserves almost nothing: Rudin's opening examples give continuous $f_n$ with discontinuous limit, and sequences where $\lim_n \int f_n \ne \int \lim_n f_n$. Uniform convergence is the hypothesis that repairs this, and the chapter's second half asks the converse question — which functions arise as uniform limits from a given family — answered by the Stone–Weierstrass theorem (Theorem 7.32): an algebra of continuous real functions on a compact set that separates points and vanishes nowhere is uniformly dense in all continuous functions there.

The classical Weierstrass approximation theorem (7.26) — polynomials are dense in $C[a,b]$ — is the special case that made the general theorem worth proving, and is used in Chapter 8 for Fourier series and in Chapter 11 for the density of continuous functions in $L^2$.

This mission is the seventh in a series formalizing Rudin Chapters 1–11; it uses the compactness results of Mission II, the continuity results of Mission IV and the Riemann–Stieltjes integral of Mission VI.

Setting

A sequence $f_n$ converges uniformly to $f$ on $E$ if for every $\varepsilon > 0$ there is $N$ with $|f_n(x) - f(x)| \le \varepsilon$ for all $n \ge N$ and all $x \in E$ — the same $N$ for every point. A family $\mathcal{F}$ is equicontinuous on $E$ if a single $\delta$ serves all its members in the definition of uniform continuity; it is pointwise bounded if each orbit $\{f(x) : f \in \mathcal{F}\}$ is bounded, and uniformly bounded if one bound works for all $f$ and all $x$.

A set $\mathcal{A}$ of real functions is an algebra if it is closed under addition, multiplication and multiplication by real scalars; it separates points on $K$ if for $x \ne y$ in $K$ some $f \in \mathcal{A}$ has $f(x) \ne f(y)$; it vanishes at no point of $K$ if for each $x \in K$ some $f \in \mathcal{A}$ has $f(x) \ne 0$. The uniform closure of $\mathcal{A}$ on $K$ is the set of uniform limits on $K$ of sequences from $\mathcal{A}$.

Formalization targets

Goal — Stone–Weierstrass (Theorem 7.32)

Let $K$ be compact and let $\mathcal{A}$ be an algebra of real continuous functions on $K$ which separates points on $K$ and vanishes at no point of $K$. Then

every continuous real function on $K$ is a uniform limit on $K$ of members of $\mathcal{A}$.

Milestones

Significance

Uniform convergence is the standard hypothesis under which limits commute with continuity, integration and (with an extra condition) differentiation, and Theorems 7.11, 7.12, 7.16 and 7.17 are used throughout the rest of the book; Chapter 8 in particular builds the exponential, trigonometric and Gamma functions as uniform limits and differentiates them term by term on the strength of 7.17. Theorem 7.18 shows how weak pointwise differentiability is as a consequence of continuity: a uniform limit of piecewise-linear functions can fail to be differentiable anywhere. Arzelà–Ascoli is the compactness criterion for families of functions, and it is the standard route to existence theorems for differential and integral equations.

Stone–Weierstrass is the structural theorem of the chapter: it replaces the combinatorial Bernstein-polynomial proof of Weierstrass's theorem with a statement about algebras of functions, applicable to trigonometric polynomials, polynomials in several variables, and Lipschitz algebras alike.

Mathlib contains a Stone–Weierstrass theorem for subalgebras of C(X, ℝ) on compact Hausdorff spaces, and a version of Arzelà–Ascoli. This mission states the results in Rudin's terms — plain sets of functions on a compact subset $K$ of a metric space, uniform closure defined by sequences — so that they can be used together with the Riemann–Stieltjes integral built in Mission VI, which is not part of the library.

Difficulty

Stone–Weierstrass is the one theorem in this mission whose proof is genuinely structural: from the algebra one first produces $|f|$ as a uniform limit of polynomials in $f$ (which needs the polynomial approximation of $\sqrt{t}$ on $[0,1]$ and so cannot be circular with Theorem 7.26), then maxima and minima of pairs, then functions matching prescribed values at two points, and only then the local-to-global patching over a finite subcover. Each step is short; keeping the uniform closure a lattice and an algebra simultaneously is the bookkeeping burden.

Two hypotheses are easy to lose and both are necessary: an algebra that vanishes at a point cannot approximate functions that do not, and one that fails to separate two points cannot approximate functions that distinguish them.

Formalization scope

Conventions fixed by this mission:

• Uniform convergence is Mathlib's TendstoUniformlyOn … atTop; complex-valued sequences are used where Rudin allows complex values.
• Algebras, separation, non-vanishing and uniform closure are the predicates Rudin.IsFunctionAlgebra, Rudin.SeparatesPointsOn, Rudin.VanishesAtNoPointOn, Rudin.UniformClosureOn, defined for sets of functions X → ℝ and a compact subset K. The goal's conclusion is membership in the uniform closure, i.e. the existence of an approximating sequence from the algebra.
• Equicontinuity and the two boundedness notions are Rudin.EquicontinuousOn, Rudin.PointwiseBoundedOn, Rudin.UniformlyBoundedOn, stated with explicit $\varepsilon$ and $\delta$ as in Definitions 7.19 and 7.22.
• Theorem 7.16 is stated for the Riemann–Stieltjes integral of Mission VI, not for a Mathlib integral, so the two missions compose.
• Theorem 7.26 is stated for complex-valued $f$ and polynomials with complex coefficients evaluated at real points, as in Rudin.

Selected references

• Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 7 (pp. 143–171).
• M. H. Stone, The generalized Weierstrass approximation theorem, Mathematics Magazine 21 (1948), 167–184 and 237–254. https://doi.org/10.2307/3029750

Motivation

The discrete-time Riccati equation is the central object of linear-quadratic optimal control — the design equation behind LQR/LQG controllers in every modern control stack. Proposition 4.4.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005, §4.1) packages its asymptotic theory: under controllability and observability the Riccati iteration converges to the unique positive semidefinite solution of the algebraic Riccati equation and the resulting closed loop is stable. Alongside it, Lemma 4.2.1 of §4.2 develops K-convexity, the analytical engine behind Scarf's optimality of $(s,S)$ inventory policies — a foundational result of operations research. Neither the Riccati asymptotics nor K-convexity exists in Mathlib.

Setting

Matrices $A \in \mathbb{R}^{n\times n}$, $B \in \mathbb{R}^{n\times m}$, $Q = C^\top C \succeq 0$, $R \succ 0$. The Riccati operator (BertsekasRiccatiMap)

$(A,B)$ is controllable if $[B, AB, \dots, A^{n-1}B]$ has rank $n$ (BertsekasControllablePair); $(A,C)$ is observable if $(A^\top, C^\top)$ is controllable (BertsekasObservablePair). Separately, $g : \mathbb{R} \to \mathbb{R}$ is $K$-convex (BertsekasKConvex, Def. 4.2.1) if $K + g(z+y) \ge g(y) + \tfrac{z}{b}(g(y) - g(y-b))$ for all $z \ge 0$, $b > 0$, $y$.

Target

with $L = -(B^\top P B + R)^{-1} B^\top P A$ — BertsekasDP.riccati_convergence_stability (goal). Milestones: Lemma 4.2.1(a)–(d) (kconvex_of_convex, kconvex_combination, kconvex_expectation, kconvex_sS_structure), culminating in the $(s,S)$ structure theorem for continuous coercive $K$-convex functions.

Significance

The Riccati result is the mathematical license behind steady-state LQR design: it guarantees the design equation has one meaningful solution, that iterating the finite-horizon recursion finds it, and that the resulting feedback is stabilizing. Formally it would seed a Mathlib-adjacent theory of matrix fixed-point iterations, positive semidefinite order, and spectral-radius stability. The K-convexity milestones are self-contained real analysis, each of independent reuse value for inventory theory; part (d) is the engine of $(s,S)$-policy optimality. All results are classical and proved in the book; the formal work is new.

Difficulty

The Riccati proof interleaves monotonicity of $F$ on the psd cone, boundedness from controllability (a steering argument), positivity from observability, and stability extracted from the fixed-point identity via a Lyapunov argument — several pieces of matrix analysis (psd order, congruence, Schur-type manipulations, spectral radius vs. convergence of powers) that must be built or located in Mathlib. The naive route of diagonalizing $A$ fails: nothing is symmetric about $A + BL$. For Lemma 4.2.1(d), the difficulty is that $g$ is not convex: the minimizer structure must come from the K-convexity inequality applied at carefully chosen points, plus continuity and coercivity.

Formalization scope

Real matrices over Fin n; Matrix.PosSemidef/PosDef; matrix inverse is Mathlib's total inverse (zero on singular input — harmless here since $B^\top P B + R \succ 0$ along the relevant iterates, which the proof must establish); convergence in the entrywise topology; eigenvalues via spectrum ℂ of the complexified matrix, all strictly inside the unit circle. Rank-based controllability exactly as Def. 4.1.1. K-convexity is stated for all real $K$; note $K \ge 0$ is forced whenever it is satisfiable ($z = 0$), and the expectation milestone is stated for finitely supported disturbances (integrability automatic).

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (Prop. 4.4.1, Def. 4.1.1, §4.2, Lemma 4.2.1.) http://www.athenasc.com/dpbook.html
• R. E. Kalman, Contributions to the theory of optimal control, Bol. Soc. Mat. Mexicana 5 (1960), 102–119.
• H. Scarf, The optimality of (S, s) policies in the dynamic inventory problem, in Mathematical Methods in the Social Sciences, Stanford Univ. Press, 1960.

Motivation

The Pontryagin Minimum (Maximum) Principle is the fundamental necessary condition of optimal control, in continuous use since 1956 across aerospace guidance, robotics, and mathematical economics. Chapter 3 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) develops it from the dynamic programming side: the HJB sufficiency theorem (Prop. 3.2.1), an envelope lemma (Lemma 3.3.1), the Minimum Principle itself (Prop. 3.3.1), and its discrete-time counterpart (Prop. 3.3.2). Mathlib's optimal-control coverage is currently near zero — no HJB equation, no adjoint equations, no maximum principle — which makes this the mission with the largest gap between textbook maturity and formal coverage in the series.

Setting

Minimize, over admissible pairs, the cost

with $f, g, h$ continuously differentiable (BertsekasCTModel). Admissible controls are piecewise continuous on $[0,T]$ — formalized as: bounded image and continuous off a finite set (BertsekasPiecewiseContinuousOn) — and state trajectories are continuous, satisfying the ODE off a finite set (BertsekasCTAdmissibleFrom, parametrized by an arbitrary start $(t_0, \xi)$). The Hamiltonian is $H(x,u,p) = g(x,u) + \langle p, f(x,u)\rangle$ (BertsekasHamiltonian).

Target

For an optimal admissible pair $(u^*, x^*)$: there exist an adjoint $p$ and a constant $c$ with

away from finitely many times — BertsekasDP.pontryagin_minimum_principle (goal). Milestones: Prop. 3.2.1 (hjb_sufficiency_of_continuous), Lemma 3.3.1 (envelope_gradient_lemma), Prop. 3.3.2 (discrete_minimum_principle).

The HJB milestone carries the hypotheses that $f$ and $g$ are jointly continuous — the consequence of the §3.1 standing assumptions that its proof uses. An earlier version without any regularity hypothesis was disproved: with a discontinuous running cost the cost integrand need not be integrable, and the library's integral of a non-integrable function is $0$.

Significance

The Minimum Principle converts an infinite-dimensional optimization into a two-point boundary value problem — the basis of shooting methods and of every "bang-bang" analysis. None of it exists in Mathlib; even the HJB verification theorem would be new. The discrete-time milestone is self-contained multivariable calculus and gives early value; the envelope lemma is reusable well beyond control theory. The results are classical (Pontryagin et al. 1962; the book's Chapter 3); the formal proof of Prop. 3.3.1 will need an honest variational argument — the book's own HJB-based derivation is explicitly informal.

Difficulty

For the goal: the classical proofs go through needle variations and a separation argument, or through regularity of the value function — neither is in Mathlib. The book's derivation assumes differentiability of the optimal value function, which is not a hypothesis of the statement; a formal proof must either supply a rigorous variational argument or add intermediate lemmas as new platform problems (sketching is encouraged). For the HJB milestone, the work is differentiating $t \mapsto V(t, x(t))$ along a trajectory that satisfies the ODE only off a finite set, then integrating.

Formalization scope

States and controls in EuclideanSpace ℝ (Fin n) / (Fin m); gradients in Mathlib's gradient; the ODE and adjoint via HasDerivAt off a finite exceptional set; costs via intervalIntegral. Piecewise continuity includes boundedness of the image, so the cost integrand of an admissible pair is genuinely integrable — the junk-value escape (non-integrable integrand ⇒ integral 0) is closed. Fixed initial state, fixed terminal time, free terminal state; time-independent dynamics (so the Hamiltonian is constant, per the book's remark that time-varying systems lose constancy). $U$ is an arbitrary set — no compactness or convexity is assumed in the goal.

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (Ch. 3.) http://www.athenasc.com/dpbook.html
• L. S. Pontryagin, V. G. Boltyanskii, R. V. Gamkrelidze, E. F. Mishchenko, The Mathematical Theory of Optimal Processes, Interscience, 1962.
• W. H. Fleming, R. W. Rishel, Deterministic and Stochastic Optimal Control, Springer, 1975. https://doi.org/10.1007/978-1-4612-6380-7

Motivation

Pontryagin's principle as presented by Luenberger is the decisive necessary condition in continuous-time optimal control. It converts an optimization over functions into a pointwise comparison of a Hamiltonian, coupled to the original state equation and a backward costate equation. Luenberger derives the minimum-Hamiltonian convention from vector-space multiplier ideas and a first-order comparison principle. Formalization is especially valuable here because the printed theorem contains a standard but consequential regularity oversight: it asserts a condition at every time even though controls are only piecewise continuous and the cost is an integral. This mission preserves the intended theorem while replacing that false pointwise claim by the mathematically canonical almost-everywhere statement.

Setting

Fix t₀ < t₁, a finite-dimensional Euclidean state space OCState n, a Euclidean control space OCControl m, and a permitted-control set Omega. A state-control pair (x,u) is admissible when x t₀ = xInit, the state is absolutely continuous on the interval, the control is almost everywhere strongly measurable and lies in Omega almost everywhere, the differential equation x' = F(x,u) holds almost everywhere in the interior, and the running cost is interval integrable. An optimal pair globally minimizes the interval integral among all admissible pairs.

The dynamics F and running cost ell are continuous jointly in state and control and continuously differentiable in the state variable. Their state derivatives Fx and ellx vary continuously. A global Lipschitz estimate controls changes of F in both state and control. Because an a.e. measurable control need not be bounded, the optimal control is explicitly assumed to have an a.e. norm bound on the compact interval, matching the boundedness inherited from the source's piecewise-continuous model. The operator-valued paths Fx (x₀ t) (u₀ t) and ellx (x₀ t) (u₀ t) are also assumed interval integrable along the optimum. Together these hypotheses provide the measure-theoretic regularity needed for the adjoint and state perturbations. The Hamiltonian uses Luenberger's minimum convention,

Formalization targets

The root VectorSpaceOpt.pontryagin_minimum_principle asserts the existence of an absolutely continuous costate lambda with terminal value lambda t₁ = 0. Almost everywhere it satisfies the weak inner-product form of

and almost everywhere on the control interval it satisfies

Two milestones capture source dependencies. control_state_lipschitz_estimate is the Grönwall stability estimate used on p. 263 to control the state response by the integral distance between controls; it explicitly assumes interval integrability of both the state-difference norm and the control-difference norm, so Mathlib's totalized integral cannot hide a nonintegrable input. adjoint_lagrangian_comparison formalizes §9.6, Proposition 1: under an implicit state equation, differentiability in the state, Lipschitz dependence of the state solution, and an adjoint identity, the objective difference agrees with a frozen-state Lagrangian difference up to an explicit filter-level little-o remainder.

Significance

This is the flagship analytic mission of the continuation. It connects finite-dimensional differential calculus, Bochner integration, absolute continuity, ODE constraints, adjoints, and localized control variations in one reusable theorem. The definitions form a minimal control framework that can support terminal costs, endpoint constraints, and alternative maximum-principle conventions later. The corrected a.e. conclusion also demonstrates a central benefit of formalization: informal conventions about representatives of controls and isolated time values must be resolved before a theorem can be accepted.

The weak inner-product adjoint equation avoids introducing a coordinate transpose and remains invariant under the Euclidean-space representation. That choice makes the result immediately reusable in later vector-space treatments of transversality and endpoint multipliers.

Difficulty

The difficulty is very high. Mathlib supplies finite-dimensional calculus, interval integration, absolute continuity, measure-theoretic almost-everywhere statements, and Grönwall tools, but not an assembled Pontryagin framework. The mission must coordinate a state-solution stability estimate, state differentiability of the dynamics and cost, existence and regularity of the backward costate, and Hamiltonian comparison against arbitrary admissible values. The control is measurable rather than globally continuous, so every pointwise expression must be placed under an a.e. quantifier where appropriate. The proposition milestone additionally requires a precise little-o interface instead of an unnamed asymptotic remainder.

Formalization scope

The proposal covers §9.6, Proposition 1 and Theorem 1, with the regularity inherited from the surrounding discussion made explicit. Both the optimal state and the costate are absolutely continuous. Admissible controls are a.e. strongly measurable, which is a broader measure-theoretic proxy for the source's piecewise-continuous controls and is compatible with integral objectives; the root additionally requires the optimal control to be essentially norm bounded on Icc t₀ t₁, restoring the compact-interval boundedness used by the source. The maps F, ell, Fx, and ellx are jointly continuous; state derivatives are supplied by HasFDerivAt; a uniform Lipschitz bound is stated; and both derivative coefficients along the optimal path are interval integrable. The separate Grönwall milestone requires its state and control norm differences to be interval integrable. The interval is required to have positive length.

There is a documented source erratum. The sentence on printed p. 263 states Hamiltonian minimality for every t, while the proof on p. 264 chooses a neighborhood on which a purported strict violation persists. That step requires continuity at the selected time. Moreover, changing a piecewise-continuous control at a single isolated time changes neither its a.e. class, the state equation, nor the integral cost. Therefore no condition can be forced at an arbitrary jump value. The Lean root uses an a.e. conclusion on Icc t₀ t₁; an alternative source-faithful repair would assert the inequality at every continuity point of u₀. The mission does not claim existence of an optimal pair, compactness of Omega, endpoint constraints, nonsmooth dynamics, or a sufficiency theorem.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, Wiley, 1969, Chapter 9, §9.6, Proposition 1 and Theorem 1, pp. 262–264, including the printed all-times wording and its proof context. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf
• Lean community, Mathlib documentation, continuously updated: https://leanprover-community.github.io/mathlib4_docs/ (interval integration, absolute continuity, Euclidean spaces, Fréchet derivatives, ODE estimates, and a.e. measurability).

AI generated but i think correct. I think the milestones make it really annoying but the central theorem looks correct.

Motivation

The matrix-multiplication exponent measures the asymptotic number of field operations needed to multiply two square matrices. A bound $\omega<c$ means that, for every $\varepsilon>0$, two $n\times n$ matrices can be multiplied using $O(n^{c+\varepsilon})$ arithmetic operations. Matrix multiplication is a central benchmark in algebraic complexity and a primitive for many algorithms in linear algebra, graph theory, and symbolic computation.

After Strassen showed that $\omega<3$, a sequence of tensor constructions reduced the exponent further. Schönhage's asymptotic sum inequality made it possible to exploit simultaneous matrix products rather than a single square product. In 1990, Don Coppersmith and Shmuel Winograd combined an explicit low-border-rank tensor with a block extraction argument based on Salem--Spencer sets. Their basic analysis gave $\omega<2.38719$; coupling the random weights in the tensor square sharpened this to $\omega<2.375477$, hence the exact rational consequence $\omega<2.376$.

This mission formalizes that historical Coppersmith--Winograd result. It follows the source tensor and its actual block restrictions, while excluding placeholder “laser values” that are not backed by extracted direct sums of matrix-multiplication tensors.

Setting

For a field $K$, an order-three tensor is represented by three finite-dimensional $K$-vector spaces and an element of their tensor product. The matrix-multiplication tensor

encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix. A restriction applies one linear map to each tensor leg. A degeneration permits those maps to depend polynomially on a formal parameter and selects their first nonzero coefficient. Thus a degeneration from the diagonal tensor $I_r$ is a border-rank certificate $\underline R(T)\le r$.

The Coppersmith--Winograd tensor with parameter $q$ is

It has border rank at most $q+2$. Its coordinates carry three classes, indexed by $0,1,2$, and its six nonzero block types are

The first three blocks are matrix-multiplication tensors with dimensions $(1,1,q)$, $(q,1,1)$, and $(1,q,1)$; the other three are scalar products. Tensor powers therefore contain many typed rectangular matrix products. The laser method selects a large family with disjoint coordinate blocks and applies Schönhage's asymptotic sum inequality to all surviving products simultaneously.

Formalization targets

Goal: the 1990 Coppersmith--Winograd bound

For every field $K$,

The Lean goal has the same quantified proposition and the same matMulExp definition as the existing Schönhage-bound mission; only the theorem identifier and rational endpoint change.

Tensor and block foundations

The development records the characteristic-free order-three degeneration

and the exact matrix-product dimensions associated with every supported type sequence in $T_q^{\otimes N}$. These statements identify the algebraic input before any asymptotic counting is used.

Coupled-weight extraction

For $q=6$, the tensor-square grading and the coupled-weight pruning must produce the direct sums and asymptotic inequality stated in Section 8 and in the coupled-constituent lemma on journal pp. 270--272. The final numerical milestone certifies the rational endpoint $297/125$ from exact inequalities, rather than treating the decimal $2.375477$ as a proof object.

Significance

The result was the strongest matrix-multiplication bound for roughly two decades and introduced the tensor family that underlies the classical laser-method line of work. A formal proof supplies a checked bridge from an explicit border-rank identity to an exponent bound whose combinatorial extraction is substantially more delicate than the earlier Schönhage examples.

The formalization also produces reusable infrastructure. The order-three CW degeneration is an explicit polynomial-family test case over arbitrary fields. The six block identifications and type-count formulas can be reused in analyses of tensor powers. A faithful extraction predicate, stated through actual restrictions to direct sums of MMObj tensors, separates sound laser arguments from formulas that count incompatible or coordinate-sharing blocks as independent.

The mathematical bound is known. The open work is its machine-checked reconstruction in Lean. The border-rank theorem, per-type matrix-product restriction layer, tensor-square support invariant, balanced block calculation, Salem--Spencer set theorem, and exact $q=6$ numerical endpoint are already proved. The unrestricted value/rank bridge, the coupled-constituent extraction, and the full Section 8 auxiliary inequality remain the substantive frontier.

Difficulty

The main difficulty is not expanding $T_q$ or evaluating a decimal logarithm. A tensor power contains exponentially many typed terms, but most share variables. They cannot all be placed in a direct sum, and counting all joint type sequences overestimates the usable matrix products. The source hashes coordinate blocks into a large progression-free set and prunes collisions so that the surviving blocks are genuinely independent.

The $2.376$ improvement adds a second layer. It begins with $T_q^{\otimes2}$, regroups variables into five classes, couples weights that were independent in the simpler analysis, and estimates a nontrivial central block by a further extraction. A formal proof must track the direction of every restriction, the exact multiplicities of all block types, and the loss introduced by pruning. Replacing exponential surviving-block counts by a polynomial number of blocks, or using joint entropy without the marginal compatibility constraints, changes the mathematical claim and is outside the mission.

Formalization scope

The mission uses the existing TensorObj, MMObj, TensorObj.Restrict, Degenerates, tensorAsymptoticRank, matMulExp, and matMulExp_strassen declarations in the Mathlib environment pinned by the earlier matrix-multiplication mission. Tensor dimensions and type counts are natural numbers; exponent and optimization inequalities are real-valued. All top-level bounds quantify over an arbitrary field, matching the integral polynomial identities used by the construction.

Laser statements must exhibit, directly or through a faithful reusable predicate, restrictions from a tensor power to a finite direct sum of concrete matrix-multiplication tensors. The number and dimensions of the summands remain part of the witness. A constant-valued “laser functional,” a vacuous witness hypothesis, or a capacity definition that discards the exponential number of surviving blocks does not satisfy the mission.

Welcome contributions include restriction composition lemmas, tensor-power block equivalences, multinomial and entropy estimates with all marginal constraints, formal Salem--Spencer pruning, exact real-inequality certificates, and the coupled central-block value lemma. Every milestone should cite the corresponding equation, table, or lemma in the primary paper.

Selected references

• Don Coppersmith and Shmuel Winograd, Matrix Multiplication via Arithmetic Progressions, Journal of Symbolic Computation 9, 1990, pp. 251--280. ScienceDirect.
• Arnold Schönhage, Partial and Total Matrix Multiplication, SIAM Journal on Computing 10(3), 1981, pp. 434--455. DOI 10.1137/0210032.
• Avi Wigderson and Jeroen Zuiddam, Asymptotic Spectra: Theory, Applications and Extensions, 2023, for the tensor restriction and asymptotic-rank framework used by the Lean development. Author manuscript.

Motivation

The whole series so far lived in discrete time on finite state spaces. Chapters 20–21 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) lift both restrictions. Running the jumps of a chain at the arrivals of a rate-one Poisson clock produces the continuous-time chain, whose transition semigroup — the heat kernel — converges to stationarity for every irreducible chain, with no aperiodicity hypothesis: continuous time washes out periodicity. On countable state spaces, existence of a stationary distribution is no longer automatic, and the trichotomy of transience, null recurrence, and positive recurrence replaces it; the convergence theorem survives exactly on the positive-recurrent class. The chapter's crown jewel — and this mission's goal — is Pólya's theorem: simple random walk on the lattice $\mathbb Z^d$ is recurrent in dimensions one and two and transient in dimension three and higher. "A drunk man will find his way home, but a drunk bird may get lost forever."

Setting

Continuous time (Ch. 20). For a finite chain $P$, the heat kernel at time $t\ge0$ is defined by Poissonization,

the law at time $t$ of a walk taking $P$-steps at Poisson arrival times ($=e^{t(P-I)}$ as a matrix exponential). With $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$, the continuous distance and mixing time are $d^{\mathrm{cont}}(t)=\max_x\|H_t(x,\cdot)-\pi\|_{TV}$ and $t^{\mathrm{cont}}_{\mathrm{mix}}(\varepsilon)=\inf\{t\ge0:d^{\mathrm{cont}}(t)\le\varepsilon\}$. The lazy version of a discrete chain is $\tfrac12(I+P)$; from Mission VII, the spectral gap $\gamma$ is $1-\lambda_2$ with $\lambda_2$ the largest eigenvalue $\ne1$. The product chain on a product of $n$ coordinate spaces picks a uniform coordinate and updates it by that coordinate's chain.

Countable state spaces (Ch. 21). A chain on a countable state space $V$ is a function $P$ with nonnegative entries and rows summing to one (as convergent series); $t$-step probabilities $P^t(x,y)$ are defined recursively, and trajectory probabilities are countable sums of path weights. The first return time to $x$ is $\tau_x^+=\min\{t\ge1:X_t=x\}$; a state is recurrent when $\mathbb P_x\{\tau_x^+<\infty\}=1$ (tails tend to zero), positive recurrent when moreover $\mathbb E_x(\tau_x^+)<\infty$ (tails summable), and null recurrent when recurrent but not positive recurrent. A stationary distribution is a nonnegative $\pi$ summing to one with $\pi P=\pi$ (as convergent series). Simple random walk on $\mathbb Z^d$ steps from $x$ to one of its $2d$ nearest neighbours uniformly at random.

Formalization targets

Goal

Pólya's theorem (§21.2, Examples 21.8–21.9), the capstone of Chapters 20–21:

1. for $d\le2$, simple random walk on $\mathbb Z^d$ is recurrent — it returns to its starting point with probability one;
2. for $d\ge3$, it is transient — with positive probability it never returns.

Milestones

• Theorem 20.1 — for any irreducible finite chain, aperiodic or not, the heat kernel converges: $d^{\mathrm{cont}}(t)\to0$ as $t\to\infty$.
• Theorem 20.3 — the two-way comparison between lazy discrete and continuous mixing: eventual $\varepsilon$-mixing of the lazy chain at time $k$ gives $2\varepsilon$-mixing of the heat kernel at time $k$, and $\varepsilon$-mixing of the heat kernel at time $m$ gives $2\varepsilon$-mixing of the lazy chain at time $4m$.
• Theorem 20.6 — the spectral bound for reversible chains: $\bigl|H_t(x,y)-\pi(y)\bigr|\le\sqrt{\pi(y)/\pi(x)}\;e^{-\gamma t}$.
• Theorem 20.7 — mixing of continuous-time product chains: with all coordinate gaps $\ge\gamma$ and coordinate stationary masses bounded below, $t^{\mathrm{cont}}_{\mathrm{mix}}(\varepsilon)\le(2\gamma)^{-1}n\log n+\gamma^{-1}n\log(1/(c_0\varepsilon))$, with a matching $\tfrac{n}{2\gamma}\log n$ lower bound when the gaps are equal — the $n\log n$ product-chain phenomenon.
• Proposition 21.3 — the recurrence dichotomy on countable spaces: a state is recurrent exactly when its Green's function $\sum_tP^t(x,x)$ diverges, and for an irreducible chain one recurrent state makes all states recurrent.
• Theorem 21.12 — an irreducible countable chain is positive recurrent if and only if it has a stationary distribution.
• Lemma 21.13 (Kac) — for an irreducible chain with stationary distribution $\pi$ and any nonempty set $S$: $\sum_{x\in S}\pi(x)\,\mathbb E_x(\tau_S^+)=1$; in particular $\mathbb E_x(\tau_x^+)=1/\pi(x)$.
• Theorem 21.14 — the convergence theorem on countable spaces: an irreducible, aperiodic, positive recurrent chain has a unique stationary distribution $\pi$, and $\|P^t(x,\cdot)-\pi\|_{TV}\to0$ from every start.
• Theorem 21.17 — in the null recurrent case, $P^t(x,y)\to0$ for all pairs of states: no stationary profile is approached.

Significance

The results. Theorem 20.1 explains why laziness and aperiodicity pervade the discrete theory — periodicity is an artifact of the discrete clock. The product-chain theorem 20.7 is the cleanest instance of the $n\log n$ paradigm (independent coordinates mix in relaxation time $\times\log(\text{number of coordinates})$) and the template for the hypercube cutoff of Mission XI. Chapter 21's trichotomy is the backbone of applied Markov chain theory — queueing, branching, renewal — and Kac's lemma with the convergence theorem 21.14 is the standard equipment of any probability course. Pólya's theorem is one of the most celebrated results of twentieth-century probability, the birth of the random-walk-in-dimension-$d$ paradigm.

Formalizing them. Mathlib has no continuous-time Markov chains, no Poissonization, and no recurrence/transience theory (its PMF random walks stop far short). The countable-state layer built here — summable stationary equations, tail-sum return times, the recurrence dichotomy — is the missing infrastructure for formalized applied probability; Pólya's theorem is a famous target in its own right, and the $d\ge3$ half has never been formalized in any assistant to our knowledge.

Difficulty

The heat kernel is an infinite series of matrices: convergence (dominated by the Poisson weights), the semigroup property, and the interchange of the series with matrix products and limits must all be established by hand over tsum. Theorem 20.1 avoids aperiodicity by the number-theoretic fact that the Poisson distribution smears over residue classes — formally, the continuous chain is automatically aperiodic because $H_t(x,x)>0$ for $t>0$. The product-chain bounds need the $\ell^2$ machinery of Mission VII applied coordinatewise and a careful union bound; the lower bound is a Gaussian-free second-moment argument. On the countable side, everything is series bookkeeping in the absence of Fintype: the recurrence dichotomy is a generating-function (renewal) identity $G(x,x)=1/\mathbb P_x\{\tau_x^+=\infty\}$ handled through partial sums; Kac's lemma is a mass-transport double-count over trajectories; and Theorem 21.14 needs an aperiodicity-based coupling on a countable product space, the technical summit of the mission. Pólya's theorem itself combines a local central-limit-type estimate for the return probabilities ($P^{2t}(0,0)\asymp t^{-d/2}$, obtained by Stirling in $d=1,2$ and by a comparison argument in higher dimension) with the dichotomy of Proposition 21.3.

Formalization scope

Chapter 20 lives on finite state spaces: the heat kernel is a tsum over $k$ of Poisson weights times matrix powers (summability is provable, not assumed), continuous distance is a supremum over states, and the continuous mixing time is an sInf over nonnegative reals (junk $0$ if the set were empty — excluded under the theorems' hypotheses). Discrete-vs-continuous comparison (Theorem 20.3) is stated with eventual thresholds ($\exists K,\forall k\ge K$), matching the book's asymptotic phrasing. Chapter 21 lives on a Countable type: stochasticity and stationarity are HasSum statements, $t$-step powers are defined recursively with tsum convolutions, return-time tails are countable sums of path weights over finite horizons, and recurrence/positive recurrence are the tail-limit and tail-summability conditions above — measure theory never enters. Pólya's theorem is stated for the origin of $\mathbb Z^d$ with the walk defined by nearest-neighbour steps; the $d\le2$ and $d\ge3$ halves are separate conjuncts of one statement.

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• G. Pólya, Über eine Aufgabe der Wahrscheinlichkeitsrechnung betreffend die Irrfahrt im Straßennetz, Math. Ann. 84 (1921). https://doi.org/10.1007/BF01458701
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. I, 3rd ed., Wiley, 1968.
• D. Aldous, J. A. Fill, Reversible Markov Chains and Random Walks on Graphs, 2002. https://www.stat.berkeley.edu/~aldous/RWG/book.html

Motivation

How fast does a Markov chain forget its starting point? For a reversible chain the complete answer is coded in the eigenvalues of its transition matrix: the largest eigenvalue is always $1$, and the size of the gap between $1$ and the rest of the spectrum is the chain's fundamental time constant — a large gap means fast mixing, a small gap means slow mixing. Chapters 12–13 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develop this spectral theory and culminate in the discrete Cheeger inequality of Jerrum–Sinclair and Lawler–Sokal, which says that the spectral gap $\gamma$ (an analytic quantity, defined below) and the bottleneck constant $\Phi_\star$ (a geometric quantity from Mission IV, also recalled below) control each other:

A chain mixes rapidly exactly when its state space has no bottleneck. This inequality is the backbone of the Markov-chain approach to approximate counting and of spectral graph theory at large; alongside it the chapters provide Wilson's method — the sharpest general technique for mixing-time lower bounds — and the comparison machinery that transfers spectral estimates between chains.

Setting

All chains live on a finite state space $V$. A chain with transition matrix $P$ and stationary distribution $\pi$ is reversible when the detailed balance equations $\pi(x)P(x,y)=\pi(y)P(y,x)$ hold; reversibility is the standing assumption of both chapters. The yardsticks of the series are the total variation distance $\|\mu-\nu\|_{TV}=\max_{A\subseteq V}|\mu(A)-\nu(A)|$, the worst-case distance to stationarity $d(t)=\max_x\|P^t(x,\cdot)-\pi\|_{TV}$, and the mixing time $t_{\mathrm{mix}}(\varepsilon)=\min\{t: d(t)\le\varepsilon\}$, with $t_{\mathrm{mix}}=t_{\mathrm{mix}}(1/4)$; we write $\pi_{\min}=\min_x\pi(x)$.

The spectral vocabulary: an eigenfunction of $P$ is a nonzero $f:V\to\mathbb R$ with $Pf=\lambda f$, where $(Pf)(x)=\sum_yP(x,y)f(y)$; the number $\lambda$ is then an eigenvalue. Out of the spectrum one forms

• $\lambda_2$, the largest eigenvalue different from $1$, and the spectral gap $\gamma=1-\lambda_2$;
• $\lambda_\star$, the largest absolute value of an eigenvalue different from $1$, the absolute gap $\gamma_\star=1-\lambda_\star$, and the relaxation time $t_{\mathrm{rel}}=1/\gamma_\star$.

Functions on $V$ carry the weighted inner product $\langle f,g\rangle_\pi=\sum_xf(x)g(x)\pi(x)$ — the geometry, denoted $\ell^2(\pi)$, in which a reversible $P$ is self-adjoint — and the Dirichlet form

the average squared variation of $f$ along the chain's transitions. Finally, from Mission IV: the bottleneck ratio of a set $S$ of states is $\Phi(S)=\sum_{x\in S,\,y\notin S}\pi(x)P(x,y)\,/\,\pi(S)$, the conditional probability at stationarity of escaping $S$ in one step, and the bottleneck constant is $\Phi_\star=\min\{\Phi(S):\varnothing\ne S,\ \pi(S)\le\tfrac12\}$.

Formalization targets

Goal

Theorem 13.14, the discrete Cheeger inequality: for a reversible irreducible chain,

Milestones

• Lemma 12.1 — every eigenvalue satisfies $|\lambda|\le1$; for an irreducible chain the eigenfunctions of the eigenvalue $1$ are the constant functions; an irreducible aperiodic chain does not have $-1$ as an eigenvalue.
• Lemma 12.2 — the spectral representation: a reversible chain admits eigenfunctions $f_1,\dots,f_{|V|}$, orthonormal with respect to $\langle\cdot,\cdot\rangle_\pi$, with eigenvalues $\lambda_j$, such that $P^t(x,y)/\pi(y)=\sum_jf_j(x)f_j(y)\lambda_j^t$ for all $t,x,y$.
• Theorem 12.3 — mixing is at most relaxation times a log factor: $t_{\mathrm{mix}}(\varepsilon)\le\log\bigl(1/(\varepsilon\,\pi_{\min})\bigr)\,t_{\mathrm{rel}}+1$.
• Theorem 12.4 — mixing is at least the relaxation time: $t_{\mathrm{mix}}(\varepsilon)\ge(t_{\mathrm{rel}}-1)\log\bigl(1/(2\varepsilon)\bigr)$.
• §12.3.1 — the model computation: simple random walk on the $n$-cycle has the numbers $\cos(2\pi j/n)$, $j=0,\dots,n-1$, among its eigenvalues.
• Theorem 13.1 — if every pair of states admits a coupling of the two one-step distributions that contracts some metric $\rho$ on $V$ by a factor $\theta$ in expectation, then $\lambda_\star\le\theta$.
• Theorem 13.5, Wilson's method — an eigenfunction $\Phi$ with eigenvalue $\lambda\in(\tfrac12,1)$ whose one-step increments have second moment at most $R$ yields the explicit lower bound $t_{\mathrm{mix}}(\varepsilon)\ge\bigl[2\log(1/\lambda)\bigr]^{-1}\bigl[\log\bigl((1-\lambda)\Phi(x)^2/(2R)\bigr)+\log\bigl((1-\varepsilon)/\varepsilon\bigr)\bigr]$.
• Lemmas 13.11–13.12 — the variational characterization: $\gamma$ is the minimum of $\mathcal E(f)$ over functions with mean zero ($\sum_xf(x)\pi(x)=0$) and unit norm ($\langle f,f\rangle_\pi=1$), and the minimum is attained.
• Lemma 13.22 — the comparison method: if a second reversible chain $\tilde P$ on the same space, with stationary distribution $\tilde\pi$, Dirichlet form $\tilde{\mathcal E}$, and gap $\tilde\gamma$, satisfies $\tilde{\mathcal E}(f)\le B\,\mathcal E(f)$ for every $f$, then $\tilde\gamma\le\bigl[\max_x\pi(x)/\tilde\pi(x)\bigr]B\,\gamma$.

Significance

The results. Theorems 12.3–12.4 sandwich the mixing time between $t_{\mathrm{rel}}$ and $t_{\mathrm{rel}}\log(1/\pi_{\min})$ — the fundamental equivalence of spectral and mixing estimates for reversible chains, prerequisite for the cutoff criterion of Mission XI. The Cheeger inequality converts isoperimetry into spectral bounds; it is the mathematical core of the Jerrum–Sinclair program of polynomial-time approximate counting, and its graph version underlies expander theory. Wilson's method produced the sharp lower bounds for adjacent transpositions and hypercube-type chains; the comparison lemma is the engine behind the shuffle bounds cited in Mission V (§16.1).

Formalizing them. Mathlib has the spectral theorem for symmetric matrices but nothing connecting spectra to Markov chains: no spectral gap, no relaxation time, no Dirichlet forms, no Cheeger inequality in any form. A formalized discrete Cheeger inequality would be a landmark reusable well outside this series (spectral graph theory, expanders); the eigenvalue and Rayleigh-quotient layer built here is what Missions IX (tree relaxation, block dynamics) and XI (cutoff criterion) consume.

Difficulty

Everything routes through one change of basis: conjugating $P$ by the diagonal matrix with entries $\sqrt{\pi(x)}$ produces a matrix that is symmetric precisely because the chain is reversible, so Mathlib's spectral theorem applies — but transporting the resulting eigenbasis back to $\ell^2(\pi)$, keeping track of orthonormality with respect to the weighted inner product, is a genuine formal-linear-algebra project; nothing about it is deep, all of it is fussy. The definitions of $\lambda_2$ and $\lambda_\star$ as suprema over the set of non-unit eigenvalues (finite, and nonempty once $|V|\ge2$) must be reconciled with the eigenbasis enumeration before any variational argument runs. The upper half of Cheeger is direct from the variational characterization — test it on the indicator function of a bottleneck set $S$, recentred to have mean zero; the lower half is the hard half: the standard proof takes an optimal $f$, decomposes it over its level sets $\{f>c\}$, and applies Cauchy–Schwarz twice, and formalizing that level-set sweep is the main effort of the mission. Wilson's method needs a supermartingale-style iteration of the eigenfunction estimate; its constants are exact, so the inequalities cannot be rounded.

Formalization scope

Eigenvalues are defined by real eigenvectors ($\exists f\ne0,\ Pf=\lambda f$); for reversible chains this captures the whole spectrum, and all statements assume reversibility wherever the book does. $\lambda_2$ and $\lambda_\star$ are suprema of explicit sets of reals; on a one-point space these sets are empty and the supremum takes a junk value, so the affected statements carry the explicit hypothesis $|V|\ge2$, matching the book's implicit assumption of a non-degenerate chain. $t_{\mathrm{rel}}=(1-\lambda_\star)^{-1}$ with total inverse. Theorem 12.3 carries an explicit $+1$ absorbing the rounding of a real-valued bound to an integer time. The cycle eigenvalue statement exhibits eigenvalues (existence of eigenfunctions); completeness of that list is not asserted. The variational characterization asserts both the minimization identity and its attainment, so it can be used in either direction.

Welcome contributions: the symmetrization API (conjugation by $\mathrm{diag}(\sqrt{\pi})$), Rayleigh-quotient lemmas, level-set (layer-cake) infrastructure — all reused by Missions IX and XI.

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• M. Jerrum, A. Sinclair, Approximating the permanent, SIAM J. Comput. 18 (1989). https://doi.org/10.1137/0218077
• G. F. Lawler, A. D. Sokal, Bounds on the L² spectrum for Markov chains and Markov processes, Trans. Amer. Math. Soc. 309 (1988). https://doi.org/10.1090/S0002-9947-1988-0930082-9
• D. B. Wilson, Mixing times of lozenge tiling and card shuffling Markov chains, Ann. Appl. Probab. 14 (2004). https://doi.org/10.1214/aoap/1042765669

Motivation

Missions II–III produce upper bounds on mixing times. Whether such a bound is sharp is a different question: an $O(n^2)$ bound on a chain that actually mixes in $n\log n$ steps hides the truth. Chapter 7 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develops the standard toolkit of lower bounds: the counting and diameter bounds (a chain cannot spread faster than its transition graph allows), the bottleneck ratio (a chain cannot mix faster than it crosses its worst cut), and distinguishing statistics (a chain is far from stationarity as long as some statistic separates $P^t(x,\cdot)$ from $\pi$ by several standard deviations). The bottleneck bound — closely related to the conductance of the chain and, via Mission VII, to the Cheeger inequality — is the single most important obstruction result in the subject: it is how slow mixing (torpid mixing of Ising at low temperature, in Mission IX) is proved.

Setting

For a chain $P$ with stationary distribution $\pi$, the edge measure is $Q(x,y)=\pi(x)P(x,y)$, the bottleneck ratio of a set $S$ of states is

and the bottleneck ratio of the chain is $\Phi_\star=\min\{\Phi(S):\pi(S)\le\tfrac12,\ S\neq\varnothing\}$. The maximal one-step out-degree is $\Delta=\max_x|\{y:P(x,y)>0\}|$; the diameter is measured in the graph joining $x\ne y$ when $P(x,y)+P(y,x)>0$. For a statistic $f:V\to\mathbb R$ and distribution $\mu$, $\mathbb E_\mu(f)$ and $\operatorname{Var}_\mu(f)$ are the finite-sum expectation and variance, and $\mu f^{-1}$ denotes the pushforward of $\mu$ under $f$.

Formalization targets

Goal

This is Theorem 7.3, the bottleneck-ratio lower bound, the chapter's central theorem.

Milestones

The counting bound $t_{\mathrm{mix}}(\varepsilon)\ge\log\bigl(|V|(1-\varepsilon)\bigr)/\log\Delta$ for chains with uniform stationary distribution (§7.1.1, display (7.2)); the diameter bound: any two states satisfy $\mathrm{dist}(x_0,y_0)\le 2\,t_{\mathrm{mix}}(\varepsilon)$ for $\varepsilon<1/2$ (§7.1.2, display (7.3)); Proposition 7.8 (a statistic separating means by $r$ standard deviations forces $\|\mu-\nu\|_{\mathrm{TV}}\ge1-4/(4+r^2)$); Lemma 7.9 (projection under a statistic does not increase TV distance); Proposition 7.13 (the lazy hypercube walk satisfies $d(\tfrac12 n\log n-\alpha n)\ge 1-8e^{1-2\alpha}$); and Proposition 7.14 (the top-to-random shuffle needs $n\log n-O(n)$ shuffles, matching the upper bound of Mission III).

Significance

The results. Together with Mission III this pins the top-to-random shuffle at $n\log n\pm O(n)$ — the first sharp mixing result of the series, and the prototype of the cutoff phenomenon formalized in Mission XI. Proposition 7.13 similarly matches the hypercube upper bound and feeds the cutoff analysis. The bottleneck bound is used in Mission IX to prove exponentially slow mixing of the mean-field Ising model at low temperature, and its two-sided refinement is the Cheeger inequality of Mission VII.

Formalizing them. Mathlib has no notion of conductance/bottleneck ratio of a chain, no distinguishing-statistic method, and no mixing-time lower bound of any kind. The pushforward and variance infrastructure over finitely supported distributions is elementary but new, and reusable wherever second-moment methods appear (Wilson's method in Mission VII).

Difficulty

The bottleneck theorem's proof is short but exact: it hinges on the identity $\pi(S)\|\mu_S P-\mu_S\|_{\mathrm{TV}}=Q(S,S^c)$ for $\pi$ conditioned on $S$, followed by a telescoping estimate of $\|\mu_S P^t-\mu_S\|_{\mathrm{TV}}$; the formal cost is manipulating conditioned measures and one-sided TV sums (Remark 4.3 from Mission II). For Proposition 7.8, the second-moment argument runs through Chebyshev on both distributions plus optimization of a threshold — the constants $4/(4+r^2)$ are exact, not asymptotic, so the formal inequalities must be done carefully. Proposition 7.13 requires the binomial mean/variance computation for Hamming weight under both $\pi$ and $P^t(\mathbf 1,\cdot)$, including the negative-correlation bound for unrefreshed coordinates. The naive route to a lower bound — "the chain has not left a small set, so it is far from $\pi$" — is precisely the counting bound and is too weak for the sharp results; the statistics method is what closes the gap.

Formalization scope

$\Phi_\star$ is an infimum over the subtype of nonempty sets with $\pi(S)\le\tfrac12$; on a one-point space this subtype is empty and the infimum takes a junk value, making the goal trivially true there (the bound carries content only for $|V|\ge2$, as in the book). The counting bound divides by $\log\Delta$ with total division ($\Delta\le1$ gives a trivially true statement). The diameter bound is stated for arbitrary pairs of states through SimpleGraph.dist of the transition graph, which subsumes the book's diameter formulation. Propositions 7.13 and 7.14 are stated for all integer times $t\le\frac12 n\log n-\alpha n$ (resp. $t\le n\log n-\alpha n$), using monotonicity of $d$ instead of evaluating at a real-valued time — this avoids floor artifacts while keeping the book's content. Proposition 7.14 quantifies "$\alpha$ large, then $n$ large" exactly as the book's iterated limit.

Welcome contributions: monotonicity of $d(t)$ in $t$; conditioned-measure lemmas; variance API for distExp/distVar.

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• M. Jerrum, A. Sinclair, Approximating the permanent, SIAM J. Comput. 18 (1989). https://doi.org/10.1137/0218077
• D. Aldous, P. Diaconis, Shuffling cards and stopping times, Amer. Math. Monthly 93 (1986). https://doi.org/10.1080/00029890.1986.11971821

Motivation

The Convergence Theorem of Mission II says an irreducible aperiodic chain mixes geometrically, but with constants coming from a crude Doeblin decomposition — useless for actual chains, whose state spaces are exponentially large. Chapters 5–6 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develop the two classic probabilistic techniques that give useful upper bounds: coupling — run two copies of the chain jointly so that they meet quickly, and read a TV bound off the meeting time — and strong stationary times — random times at which the chain is exactly stationary, independent of the time. The flagship application is the top-to-random shuffle: repeatedly take the top card of a deck of $n$ cards and reinsert it at a uniform position; the deck is well mixed after $n\log n + cn$ shuffles, with error at most $e^{-c}$.

Setting

A Markovian coupling of a chain $P$ (with the stay-together convention (5.2)) is a chain $Q$ on pairs whose coordinate marginals are both $P$ and which moves diagonal states to diagonal states. The coupling time $\tau_{\mathrm{couple}}$ is the hitting time of the diagonal; its tails are expressed with the trajectory calculus of Mission I.

A randomized stopping time is presented by its stopping rule: for each time $t$ and trajectory prefix $\omega$, a number $s_t(\omega)\in[0,1]$, the conditional probability of stopping at $t$ given the trajectory so far and no earlier stop. A strong stationary time for the chain started at $x$ is an almost surely finite such $\tau$ with

i.e. $X_\tau\sim\pi$ independent of $\tau$. The separation distance is $s_x(t)=\max_y\,[1-P^t(x,y)/\pi(y)]$.

The mission also fixes the concrete chains it bounds: the lazy walk on the discrete torus $\mathbb Z_n^d$, the Metropolis chain on proper $q$-colorings of a graph, the Glauber dynamics of the hardcore model with fugacity $\lambda$, and the top-to-random shuffle on decks of $n$ cards (states are arrangements, i.e. permutations; position $0$ is the top).

Formalization targets

Goal

Let $d(t)= \max_x\|P^t (x,\cdot)−\pi\|_{TV}$,

for the top-to-random shuffle on $n\ge2$ cards — display (6.16) of the book, the chapter's flagship bound, proved by combining the strong stationary time $\tau_{\mathrm{top}}$ with the coupon collector tail of Mission I.

Milestones

Theorem 5.2 and Corollary 5.3 (the coupling bound: $\|P^t(x,\cdot)-P^t(y,\cdot)\|_{\mathrm{TV}}\le\mathbb P_{x,y}\{\tau_{\mathrm{couple}}>t\}$, hence $d(t)\le\max_{x,y}\mathbb P_{x,y}\{\tau_{\mathrm{couple}}>t\}$); Theorem 5.5 ($t_{\mathrm{mix}}(\varepsilon)\le c(d)\,n^2\log_2\varepsilon^{-1}$ for the lazy torus walk); Theorem 5.7 (Metropolis colorings, $q>3\Delta$: mixing in $O(n\log n)$); Theorem 5.8 (hardcore Glauber, $\lambda<(\Delta-1)^{-1}$: mixing in $O(n\log n)$); Proposition 6.1 with Example 6.7 ($\tau_{\mathrm{top}}$ is a strong stationary time); Lemma 6.11 ($s_x(t)\le\mathbb P_x\{\tau>t\}$); Lemma 6.13 ($\|P^t(x,\cdot)-\pi\|_{\mathrm{TV}}\le s_x(t)$); Proposition 6.10 ($d(t)\le\max_x\mathbb P_x\{\tau>t\}$).

Significance

The results. The coupling bound is the single most used upper-bound technique in the subject: Missions VIII (path coupling), IX (Ising) and XI (cutoff examples) all instantiate it. Strong stationary times and separation distance return in Mission XI (separation cutoff) and underlie perfect sampling in Mission XIII. The three concrete bounds (torus, colorings, hardcore) are the standard first applications and give the first polynomial mixing results of the series; the colorings and hardcore chains are the objects of intense ongoing research on sampling thresholds.

Formalizing them. Nothing here exists in Mathlib. The novel infrastructure is the stopping-rule formalization of randomized stopping times over trajectory prefixes — measure-theory-free, but expressive enough for the strong stationarity identity — and the Markovian-coupling predicate on pair chains. Both are reused later in the series (Matthews method, cutoff, CFTP).

Difficulty

The coupling bound itself is short once Proposition 4.7 (Mission II) is available; the work is in the applications. For the torus, the coordinatewise coupling requires assembling $d$ one-dimensional couplings and bounding the coupling time by a sum of one-dimensional meeting times — the formal bookkeeping of "couple coordinate by coordinate" is the real cost, and the constant $c(d)$ absorbs it. For Theorem 5.7 and 5.8 the argument is a grand coupling over all colorings/configurations simultaneously; the formal statements quantify only over the resulting bound, but a solver must build the coupling. For Proposition 6.1, the crux is the induction "given $k$ cards under the original bottom card, all $k!$ orders are equally likely" — an exchangeability argument that must be carried through the stopping-rule encoding. Lemma 6.11 is where the definition of strong stationarity does its work; the naive attempt to prove Proposition 6.10 directly from the coupling characterization fails, which is exactly why separation distance is introduced.

Formalization scope

Couplings of chains are transition matrices on $V\times V$ with marginal conditions stated row by row; the stay-together convention is part of the predicate, matching (5.2). Stopping rules take the trajectory prefix (which includes the starting state), so times "depending on the starting position" are covered; strong stationarity packages the stopping rule bounds, almost-sure finiteness ($\sum_t\mathbb P_x\{\tau=t\}=1$), and the product identity. The colorings chain lives on the subtype of proper colorings; the hardcore chain is the Glauber dynamics of Mission II restricted to the subtype of hardcore configurations (transitions never leave it). Mixing-time upper bounds carry an explicit $+1$ for integer rounding where the book's real-valued display would otherwise be false for the integer-valued $t_{\mathrm{mix}}$. The torus statement fixes $\varepsilon\le 1/2$; for $\varepsilon$ near $1$ the display is false as stated in the book.

Welcome contributions: interface lemmas between setAvoidTailProb of the pair chain and the two coordinates; the taboo-matrix form of coupling-time tails; exchangeability infrastructure for the deck chains (reused in Mission V).

Selected references

• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
• D. Aldous, P. Diaconis, Shuffling cards and stopping times, Amer. Math. Monthly 93 (1986). https://doi.org/10.1080/00029890.1986.11971821
• P. Diaconis, J. A. Fill, Strong stationary times via a new form of duality, Ann. Probab. 18 (1990). https://doi.org/10.1214/aop/1176990628

Two quadratic functions can be compared losslessly. The S-procedure says that, when the constraint is strictly feasible, the implication

holds if and only if a single nonnegative multiplier certifies it as a matrix inequality, $\lambda \begin{bmatrix} F_1 & g_1 \\ g_1^{T} & h_1\end{bmatrix} \succeq \begin{bmatrix} F_2 & g_2 \\ g_2^{T} & h_2\end{bmatrix}$ for some $\lambda \ge 0$. It is a cornerstone of control theory, trust-region methods and robust optimization, and a rare case in which a nonconvex problem has zero duality gap. The route runs through the theory this mission builds from Boyd & Vandenberghe §5.8–5.9 and Appendix B: strong alternatives for convex inequality systems, cone-program strong duality under a generalized Slater condition, semidefinite programming duality, the LMI theorems of alternatives, and the hidden convexity of the joint range of two quadratic forms.

Log-concave functions are the meeting point of convex analysis and probability: densities of Gaussian, exponential, uniform and Wishart distributions are all log-concave, and countless facts of applied probability flow from one structural theorem — integrating out variables preserves log-concavity. This mission builds the convex-analysis spine of Boyd & Vandenberghe's Convex Optimization (Chapters 2–3) — separation and supporting hyperplanes, dual cones, the first- and second-order differential characterizations of convexity, Fenchel conjugacy — and climbs to Prékopa's theorem via the Prékopa–Leindler inequality, a landmark of Brunn–Minkowski theory absent from Mathlib.

Value decomposition — approximating the value of a joint state by a sum of per-agent local values — is a staple of multi-agent dynamic programming and reinforcement learning, from index policies for restless bandits to modern MARL architectures, yet it is normally used without justification. Chen and Peng (arXiv:2506.02385) supply one. They show a multi-agent MDP admits an exact value decomposition precisely when its transition matrix is not entangled — a notion built in direct analogy with quantum entanglement — and then turn that qualitative characterisation into a quantitative one: a measure of Markov entanglement bounds the decomposition error in general. This mission formalizes that core theory. The goal is Theorem 6, the general N-agent bound in the occupancy-weighted norm; the milestones are the equivalence between separability and exact decomposition, the perturbation machinery that carries a one-step transition error into a value-function error, and the extensions to shared global state and shared rewards. The paper's restless-bandit application, which needs mean-field machinery of its own, is left to a second mission in the series.

The Monge optimal transport problem on the real line with the classical distance cost $|x-y|$ famously fails to have a unique solution. Juillet (2019) restored uniqueness by considering the strictly concave power costs $|x-y|^p$ with $p<1$ and letting $p\to 1^-$: the limit selects a distinguished optimal plan, the excursion coupling, built from the level sets of the difference $F_\sigma=F_\mu-F_\nu$ of the cumulative distribution functions. This mission formalizes the completed-graph construction, the generalized Banach indicatrix identities of Bertoin-Yor, the alternating crossing structure of almost every level, and the marginal identities for the crossing counting measures. It culminates in Propositions 3.5-3.6: every monotone transport plan is concentrated on the paired routes, and the marginals uniquely determine the coupling carried by those routes, including in the presence of atoms.

This mission formalizes the key implication 3=>4 in Juillet's Main Theorem.

How much flow can be sent from a source $s$ to a sink $t$ through a network with arc capacities $u_{ij}\in(0,\infty]$ — and what certifies that no more is possible? This mission formalizes §7.4-7.5 of Bertsimas & Tsitsiklis. The circulation calculus of §7.4 supplies the two structural tools: the flow decomposition theorem (Lemma 7.1 — every nonzero nonnegative circulation is a positive combination $\mathbf{f}=\sum_i a_i\mathbf{f}^i$ of simple circulations with only forward arcs, with integer $a_i$ when $\mathbf{f}$ is integer) and the optimality criterion for the minimum cost network flow problem (Theorem 7.6 — a feasible flow is optimal if and only if there is no unsaturated cycle with negative cost). Section 7.5 then formulates the maximum flow problem ($\max b_s$ s.t. $\mathbf{A}\mathbf{f}=\mathbf{b}$, $b_t=-b_s$, $b_i=0$ for $i\ne s,t$, $0\le\mathbf{f}\le\mathbf{u}$), defines augmenting paths (Definition 7.2: $f_{ij}<u_{ij}$ on forward arcs, $f_{ij}>0$ on backward arcs) and the Ford–Fulkerson algorithm, and proves integer invariance and finite termination for integer capacities (Theorem 7.8). The goal is Theorem 7.10:

(a) if the Ford–Fulkerson algorithm terminates because no augmenting path can be found, the current flow is optimal;

(b) the value of the maximum flow equals the minimum cut capacity

— the archetypal combinatorial min-max theorem, which the book notes can also be read as LP duality (pp. 311-312).

Sometimes reward during learning is irrelevant — a pharmaceutical company running phase-II trials only cares about identifying the best treatment, as quickly and as reliably as possible. Chapter 33 of Lattimore–Szepesvári formalizes fixed-confidence best-arm identification: a policy together with a stopping time $\tau$ and a recommendation must be sound (wrong with probability at most $\delta$) while minimizing $\mathbb{E}[\tau]$. The information-theoretic complexity is $c^*(\nu)^{-1} = \sup_{\alpha\in\mathcal{P}_{k-1}} \inf_{\nu'\in\mathcal{E}_{alt}(\nu)} \sum_i \alpha_i D(\nu_i, \nu_i')$: every sound strategy needs $\mathbb{E}[\tau] \ge c^*(\nu)\log\frac{1}{4\delta}$, and the Track-and-Stop algorithm — the goal theorem — achieves $\lim_{\delta\to 0} \mathbb{E}[\tau]/\log(1/\delta) = c^*(\nu)$ exactly. The mission also covers the fixed-budget counterpart, sequential halving.

When rewards are binary — a click or no click, a cure or no cure — the subgaussian machinery of Missions I–III is not tight: the variance of a Bernoulli arm degrades near the boundary of $[0,1]$, and the correct exponential rate is governed by the binary relative entropy $d(p,q) = p\log\frac{p}{q} + (1-p)\log\frac{1-p}{1-q}$ rather than a squared distance. Chapter 10 of Lattimore–Szepesvári develops Chernoff's tail bound in its information-theoretic form and the KL-UCB algorithm, whose upper confidence bounds are level sets of $d$. The goal theorem shows KL-UCB attains

— asymptotic optimality with exactly the constant demanded by the lower bound of Mission VII, strictly improving subgaussian UCB on every Bernoulli instance.

Every lower bound in bandit theory rests on one question: how hard is it to tell two probability measures apart from a sample? The answer is quantified by the relative entropy $D(P,Q)$, and the sharpest elementary tool is the Bretagnolle–Huber inequality: for any event $A$, $P(A) + Q(A^c) \ge \frac{1}{2}\exp(-D(P,Q))$ — no test can distinguish $P$ from $Q$ with total error probability below $\frac{1}{2}e^{-D(P,Q)}$. This mission formalizes Chapter 14 of Lattimore–Szepesvári: the Bretagnolle–Huber inequality (the goal theorem, proved via Le Cam's inequality $\int p \wedge q \ge \frac{1}{2}(\int\sqrt{pq})^2$), Pinsker's inequality $\delta(P,Q) \le \sqrt{D(P,Q)/2}$, and the closed-form divergences between Gaussians and Bernoullis. These half-page inequalities power every impossibility result in Missions VII, XI and beyond.

Motivation

Large language models are now deployed as decision aids next to human decision-makers, and a basic empirical question is whether the pair does better than either party alone. Baek, Fu, Ma and Peng (arXiv:2602.12631v2) study this question for inventory control: they build a benchmark of multi-period inventory problems, compare operations-research policies, LLM agents and their hybrids, and run a classroom experiment in which students manage inventory with and without an AI assistant.

The experiment raises a statistical issue that is independent of inventory control. Average gains at the population level do not show that any individual benefits: if weak decision-makers simply adopt the AI's recommendation and strong ones ignore it, the average collaborative performance can exceed both stand-alone averages while no single person improves on the better of their own and the AI's performance. The quantity of interest is therefore the fraction of individuals who benefit, and it is not identified: each person is observed in only one condition (alone or with the AI), so the joint law of the two outcomes is unknown and only their marginal laws can be estimated.

Section 6.1 of the paper answers this with a distribution-free lower bound on the fraction of individuals whose gain exceeds a threshold, computed from the two marginal distributions alone, and shows that the bound cannot be improved. The bound is an instance of the classical bounds on the distribution of a difference of two random variables with given marginals (Makarov, 1981; Rüschendorf, 1982; Frank, Nelsen and Schweizer, 1987), applied to the identification problem of a human–AI experiment.

Setting

A person $i$ is drawn from a population. Write $y_H^{(i)}$ for their performance alone, $y_{AI}$ for the AI's performance, and $y_{H+AI}^{(i)}$ for their performance with the AI. The individual complementarity effect is

Set $a(i) = \max(y_H^{(i)}, y_{AI})$ and $b(i) = y_{H+AI}^{(i)}$, so that $\mathrm{CE}_i = b(i) - a(i)$. In the formal development the population is a probability space $(\Omega, P)$ and $a, b : \Omega \to \mathbb R$ are measurable functions.

The cumulative distribution function of a probability law $\mu$ on $\mathbb R$ is the right-continuous function $F(t) = \mu((-\infty, t])$; $F_a$ and $F_b$ denote those of $a$ and $b$. A joint law (coupling) of $(a, b)$ with marginals $\mu_a, \mu_b$ is a probability measure $\pi$ on $\mathbb R^2$ whose first and second marginals are $\mu_a$ and $\mu_b$. For a threshold $\delta \ge 0$ the bound is