Probability

Why stationary dependence matters

Classical central limit theorems begin with independent observations. Many stochastic models instead produce observations whose dependence persists across time: measurements from an equilibrium process, functions of a stationary Markov chain, and noise sequences in time-series models are standard examples. For such data, the variance of a long sum contains covariance terms from every lag, and independence cannot be used to discard them. Chapter 7, Section 3 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), gives a functional central limit theorem under a quantitative mixing condition. The conclusion is stronger than convergence of one normalized sum: the whole partial-sum path converges to Brownian motion.

Stationary sequences and mixing

Fix a probability space $(\Omega,\mathcal F,P)$ and a two-sided real sequence $(Y_k)_{k\in\mathbb Z}$. Strict stationarity means that shifting every integer index by the same amount leaves the joint law of the entire sequence unchanged. Each $Y_k$ is measurable and centered, so $E[Y_k]=0$.

For a nonnegative lag $m$, let the past be the sigma-algebra generated by all $Y_k$ with $k\le 0$, and let the future be generated by all $Y_k$ with $k\ge m$. For $p\ge 1$, the book's $L^p$ mixing coefficient $\varphi_p(m)$ is the supremum, over future events $A$, of

Thus $\varphi_p(m)$ measures how far events at least $m$ time units in the future remain from being independent of the complete past. The Lean definition constructs both coordinate-generated sigma-algebras explicitly and represents conditional probability as the conditional expectation of an indicator.

Formalization target

For $n\ge 1$, define the scaled partial-sum process

The Lean sequence uses the index $n+1$ because Lean's natural numbers begin at zero; this is only a reindexing of the same positive scaling sequence. Suppose there is $\delta>0$ such that every coordinate has a finite $(2+\delta)$ moment. Set

The target is Theorem 3.1: the ordered covariance series converges and

is nonnegative, while $X_n$ converges to centered Brownian motion with variance parameter $\sigma^2$. The variance is allowed to be zero. The covariance sum is encoded as convergence of its ordered partial sums, not as the stronger and unrequested assertion of absolute summability.

What the conclusion provides

The result identifies the macroscopic fluctuation process of a stationary dependent sequence. It supplies both the long-run variance, including every lag covariance, and a Brownian path limit. Consequently, continuous functionals of the accumulated process can be studied through the limiting Brownian motion rather than only through one-time normal approximations.

The formal statement preserves the book's functional interpretation. ConvergesToContinuousGaussian records the complete prelimit path laws, centered Gaussian finite-dimensional laws with covariance $\sigma^2\min(s,t)$, and convergence to a continuous limit through a common realization. This avoids weakening the theorem to convergence of a single terminal sum or to separate finite-dimensional marginals. The declaration is a statement-only formalization: the theorem remains an open Lean goal, while the mixing coefficient and partial-sum process are concrete definitions.

Where the difficulty lies

The usual independent-sum argument does not apply because blocks of observations are not independent and their covariance terms need not vanish. Merely showing that dependence becomes small at large lags is insufficient: the decay must interact with the available $(2+\delta)$ moment so that the total contribution of distant dependence is summable. A scalar central limit theorem would also leave tightness of the path sequence unresolved. The theorem packages both issues into the summability condition on the precise $L^p$ coefficient and concludes a path-level Brownian limit.

Formalization scope and conventions

The formalization uses a two-sided sequence indexed by $\mathbb Z$, matching the source's convenient stationary extension. Stationarity is equality of the laws of the whole shifted and unshifted sequence, which entails every finite-dimensional shift identity without adding Markov or independence assumptions. The probability measure is explicit, and every coordinate has an explicit measurability hypothesis.

stationaryLpMixing uses the past through zero and the future beginning at lag $m$. Its codomain is the extended nonnegative reals, so an infinite norm or supremum is not silently totalized to an ordinary real. The summability hypothesis is an extended-real infinite sum strictly below infinity. stationaryPartialSums embeds the real sum in one-dimensional Euclidean space so it can reuse the book-wide continuous-Gaussian path-convergence definition. The exact floor, positive indexing, square-root normalization, covariance order, and degenerate zero-variance case are retained. No interpolation, absolute covariance summability, positive-variance assumption, Markov property, or independence condition is introduced.

The expression-essential infrastructure consists of the two definitions introduced here and the compatible book-wide ConvergesToContinuousGaussian definition already staged for the preceding diffusion-limit mission. The latter is imported rather than duplicated under a conflicting name. Useful future work includes proving the theorem from martingale approximation and developing reusable results relating concrete mixing bounds to the required summability hypothesis.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 7, Section 3, Theorem 3.1, printed pp. 350–351; mixing convention in Section 2, printed pp. 345–346. Wiley DOI

Why diffusion limits matter

Many stochastic models are built from small random changes occurring at high frequency. Queue lengths, population counts, particle systems, and numerical schemes may be discrete or have jumps at every finite scale, yet their large-scale behavior is often described by a continuous diffusion. A diffusion approximation replaces the detailed microscopic model by a process whose drift and covariance depend on its current state. This can make asymptotic probabilities and qualitative behavior accessible without claiming that the original model itself has continuous paths.

Chapter 7 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, develops general limit theorems for this passage. The retained results in this mission are Theorem 1.4, a martingale functional central limit theorem with deterministic covariance, and Theorem 4.1, a state-dependent diffusion approximation from localized characteristics. They are related limit regimes, but the former is not presented here as a literal specialization of the latter: its covariance may vary deterministically with time, whereas the state-dependent theorem uses time-homogeneous coefficient fields evaluated along the evolving state.

The probabilistic setting

A càdlàg process is right-continuous and has a finite left limit at every positive time. For each index $n$, the state process $X_n$ and its finite-variation characteristic $B_n$ have càdlàg paths in $\mathbb R^d$. A symmetric matrix process $A_n$ has càdlàg entries and positive-semidefinite increments. The natural filtration records the histories of $X_n$, $B_n$, and $A_n$ jointly.

The centered process $M_n=X_n-B_n$ is required to be a local martingale coordinatewise. Its quadratic characteristic is represented by requiring every product

to be a local martingale as well. These conditions identify $B_n$ as the approximate drift and $A_n$ as the approximate covariance accumulation. They do not impose independence of the coordinates or of the prelimit processes.

Localization uses the first time $\tau_n^r$ at which either the current value $X_n(t)$ or its left limit $X_n(t-)$ reaches radius $r$. The jump and characteristic conditions are checked only up to $T\wedge\tau_n^r$, for each radius $r>0$ and time horizon $T>0$. This is essential when coefficients are controlled locally but not globally.

Formalization targets

State-dependent diffusion approximation

Let $a(x)$ be a continuous symmetric positive-semidefinite matrix field and let $b(x)$ be a continuous vector field. For smooth compactly supported $f$, define

Assume the continuous-path martingale problem for this operator is well posed for every initial probability law. The goal states that if the stopped squared jumps of $X_n$ and $B_n$ vanish in expected supremum, the stopped first-power jumps of each $A_n^{ij}$ vanish, and the stopped characteristics converge in probability to

then weak convergence of the initial laws implies convergence of the complete path laws to the unique continuous diffusion law.

Martingale functional central limit theorem

The retained milestone treats vector local martingales with deterministic limiting covariance $C(t)$. It preserves both alternatives in the source: either first-power martingale jumps vanish and $A_n$ is the actual cross variation, or the jumps of $A_n$ and the squared jumps of the martingale vanish while $M_n^iM_n^j-A_n^{ij}$ is locally martingale. Pointwise convergence in probability of $A_n^{ij}(t)$ to $C_{ij}(t)$ then yields the centered continuous Gaussian limit with covariance $C(\min(s,t))$.

Significance

The state-dependent theorem packages a common diffusion-limit argument into conditions on observable local characteristics. It separates model-specific work—identifying the drift, covariance, localization, and jump bounds—from the general conclusion that the entire trajectory converges. The martingale theorem records the important deterministic-covariance regime without erasing either of its two source alternatives.

For formalization, the mission provides concrete predicates for càdlàg paths, stopped maximum jumps, localized characteristic discrepancies, the diffusion generator, continuous martingale-problem laws, and Gaussian process convergence. The result is statement-only: the theorem bodies remain open with sorry, while every expression dependency is a concrete definition. No theorem proof, adapter-equivalence proof, or claim of completed formal verification is included.

Where the difficulty lies

Finite-dimensional convergence alone does not control whole trajectories. The central obstacle is simultaneous control of oscillations, jumps, and characteristics after localization. A naive argument that replaces $B_n$ and $A_n$ by their limiting integrals pointwise misses the uniform stopped discrepancies and does not justify tightness of path laws. Likewise, ignoring the left limit in the exit rule can miss a jump that crosses the localization boundary.

Well-posedness is also substantive. Identifying every subsequential limit with a solution of the martingale problem gives uniqueness only when that problem is well posed for the relevant initial law. The formal statement therefore retains existence and uniqueness for every initial probability law rather than silently assuming a distinguished solution.

Formalization scope

Time is nonnegative and the sequence is indexed from zero rather than one. Expectations of jump suprema take values in $\mathbb R_{\ge0}\cup\{\infty\}$, so no unmentioned integrability assumption is introduced. Matrix positivity is Matrix.PosSemidef, which includes the real symmetric positive-semidefinite condition used by the source. The exit time includes both the current value and the positive-time left limit, and an empty exit set gives infinity.

The diffusion law uses continuous canonical paths, smooth compactly supported tests, and bounded measurable functions of finitely many past states to express the natural-filtration martingale identities. Full process convergence is encoded by a joint realization that preserves every complete prelimit path law and converges almost surely uniformly on each compact interval to a continuous limit. This is the source-reviewed continuous-limit Skorohod representation convention, not merely convergence of finitely many observations.

The two shared definitions EthierKurtz.IsSourceLocalMartingale and EthierKurtz.HasCrossVariation are imported from the earlier book-wide stochastic-calculus package. All other definitions needed to state these two results are included here. Contributions should preserve the localization quantifiers, both central-limit jump alternatives, the full martingale-problem well-posedness hypothesis, and the complete path-law conclusions.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 7, Sections 1 and 4, Theorems 1.4 and 4.1. Wiley digital edition

Brownian equations as models of evolving systems

A Brownian stochastic equation describes a state that changes through a deterministic drift and random fluctuations. Such equations are basic models for diffusions and connect probabilistic sample paths with analytic operators. Chapter 5, Section 3 of Stewart Ethier and Thomas Kurtz's Markov Processes: Characterization and Convergence develops this connection in both directions and then separates three questions: whether a solution exists, whether it is unique when driven by fixed noise, and whether all solutions have the same distribution. The mission records four central results from that section as one coherent formalization target. The principal goal is the fixed-driver existence theorem, Theorem 3.11. Theorems 3.3, 3.6, and 3.10 retain the representation, uniqueness, and weak-existence variants without treating one as a consequence of another.

State space, coefficients, and solutions

Fix a dimension $d$. The state space is the Euclidean space $\mathbb R^d$, represented in Lean as EuclideanSpace ℝ (Fin d). A diffusion coefficient

controls the random fluctuations, and a drift coefficient

controls the finite-variation part. Given a $d$-dimensional Brownian motion $W$ and initial state $\xi$, a solution $X$ satisfies, componentwise,

The formal statement does not postulate an opaque stochastic-integral operator. The predicate HasBrownianItoIntegral uses bounded predictable dyadic step approximations, integrated squared-error convergence in probability, and convergence in probability of the corresponding stochastic sums. SolvesBrownianSDE requires continuous paths, adaptation to the completed natural past of $W$ and $\xi$, integrability of the drift, and one almost-sure equation holding for every time and coordinate.

A weak solution may choose its probability space, filtration, and Brownian driver. Its Brownian future increments are independent of the entire filtration past, its state process is adapted after completion, and its initial distribution is prescribed. Pathwise uniqueness compares two solutions on the same space with the same filtration and driver. Distribution uniqueness compares solutions that may live on different spaces and asks for equality of their whole coordinate-path laws.

Formalization targets

Theorem 3.3: martingale-problem representation

For locally bounded Borel coefficients, a given continuous solution of the diffusion martingale problem can be lifted to the completed product with an auxiliary Brownian space. On that specific extension there exists a Brownian motion making the lifted original process a weak solution of the stochastic equation. The generator is

This target retains the factor $1/2$, the complete drift term, possibly singular diffusion matrices, the given process, and the exact completed product filtration.

Theorem 3.6: uniqueness implication

For locally bounded Borel $\sigma$ and $b$ and any initial probability law $\mu$, pathwise uniqueness implies uniqueness in distribution. No existence, Lipschitz, ellipticity, or moment assumption is added.

Theorem 3.10: weak existence

When both coefficients are continuous and a constant $K$ satisfies

there is a weak solution for every initial probability law. The drift hypothesis is one-sided and does not bound $\lVert b(t,x)\rVert$.

Theorem 3.11: strong existence on fixed noise

The main goal assumes locally bounded Borel coefficients, the preceding one-sided growth condition locally in time, and local Lipschitz control on each bounded state ball. For every Brownian motion $W$ and every independent square-integrable initial variable $\xi$ already given on a probability space, there exists $X$ solving the equation with respect to the completed natural past of $W$ and $\xi$. The quantifier order preserves the fixed driver and original probability space.

Why these results matter

The representation theorem connects the analytic martingale problem with the pathwise stochastic-integral formulation while preserving a given process on a prescribed extension. The uniqueness theorem explains when the apparently stronger same-noise comparison controls the law of arbitrary weak solutions. The weak-existence theorem supplies solutions under continuity and one-sided growth without local Lipschitz assumptions. The strong-existence theorem supplies a solution driven by noise and initial data that are fixed in advance, under local Lipschitz regularity.

Formalizing the group creates reusable definitions for completed filtrations, Brownian drivers, local Itô integration, weak solutions, pathwise uniqueness, and time-dependent diffusion generators. The source results are classical theorems, and this proposal records their reviewed Lean statements as open proof obligations. It does not claim machine-checked proofs.

Main formalization difficulty

The central difficulty is keeping the probabilistic quantifiers and filtrations exact. Replacing the local stochastic integral by an unconstrained witness would make the equation too weak. Replacing weak existence by existence on a fixed space would make Theorem 3.10 too strong. Conversely, existentially choosing a new driver in Theorem 3.11 would lose its fixed-noise content. The representation theorem also cannot be reduced to equality in law: it must retain the original process through first projection and use the completed product past specified in the source.

Formalization scope

Time is ℝ≥0, states are finite-dimensional real Euclidean spaces, and diffusion matrices use the Frobenius norm. Brownian motion is represented by independent scalar Brownian coordinates with measurable evaluations and continuous paths. Completion adds every subset of an ambient measurable null set. The local Itô relation uses left-endpoint dyadic step functions, interval integrability, and convergence in probability. Equality of path laws is expressed on the coordinate function space; for continuous Euclidean paths this matches the usual continuous-path law.

The main theorem keeps Borel measurability, compact-set local boundedness, one-sided drift growth, squared diffusion growth, local Lipschitz bounds, independence of $\xi$ and $W$, and the second moment of $\xi$. The weak theorem keeps continuity and an arbitrary initial law. The representation target keeps compactly supported smooth tests and the exact covariance contraction. These conditions rule out vacuous solution predicates and default-valued integrals. Contributions may prove the four theorem statements or establish reusable lemmas for the concrete integral, completion, martingale, and path-law infrastructure.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 5, Section 3, Theorems 3.3, 3.6, 3.10, and 3.11. Wiley

Motivation

A continuous stochastic process may combine a finite-variation drift with a local martingale fluctuation. To understand a function of that process, one needs a change-of-variables rule that accounts for both parts and for their quadratic covariation. The ordinary chain rule has no term for covariation. The result here is the time-dependent, multidimensional Itô formula in Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), Chapter 5, Section 2, Theorem 2.9, printed page 287 (PDF page 296). It applies to arbitrary continuous semimartingales satisfying the stated decomposition; its input is not restricted to a particular stochastic differential equation.

Setting

Time is the nonnegative real half-line and the state has d real coordinates, indexed by Fin d. The sample space Ω has a complete probability measure P and a filtration ℱ. The initial sigma algebra contains every ambient measurable null set. For each coordinate i, V_i is a continuous adapted finite-variation process, zero at time zero; M_i is a continuous adapted local martingale, zero at time zero almost surely. The process X_i has an ℱ₀-measurable initial value and satisfies X_i(t)=X_i(0)+V_i(t)+M_i(t) for all times and samples.

The test function f(t,x) has a continuous first time derivative, continuous first spatial derivatives, and continuous second spatial derivatives. At time zero, the time derivative is taken within the nonnegative-time domain. The notation f_t, f_{x_i}, and f_{x_i x_j} denotes these derivative witnesses. The conclusion supplies processes representing the continuous cross variations and integrals; their existence is part of the theorem. The Stieltjes relations use pathwise left dyadic sums for continuous finite-variation integrators. Martingale integrals and cross variations use convergence in probability of their corresponding dyadic sums. The integral versions are continuous and adapted where the theorem requires those properties.

Formalization targets

Theorem 2.9 — time-dependent multidimensional Itô formula

For every t ≥ 0, outside one null set independent of t, the target is

The goal is EthierKurtz.ito_formula. It retains every term and both coordinate indices in the cross-variation sum. The bracket and integral witnesses are existential conclusions, so the statement does not require their existence as an extra hypothesis on X.

Significance

The formula identifies the effect of a smooth, time-dependent transformation on any process with the stated continuous semimartingale decomposition. In particular, it exposes the second-order correction that distinguishes stochastic change of variables from deterministic calculus. This makes it a general calculus result that can later be applied to diffusion equations, martingale problems, and transformed processes, independently of how the input process was constructed.

The cited theorem is established in the source book. This mission provides a compiled Lean statement and concrete expression dependencies; it does not provide a Lean proof. Formalizing the proof would require the stochastic-integral and covariation infrastructure to support the source's continuous local-martingale setting and version conventions. A solver's result should prove this full statement or develop reusable infrastructure that supports it without changing its hypotheses or conclusion.

Difficulty

The ordinary deterministic chain rule cannot account for the double sum of cross variations. A statement limited to Brownian motion, an absolutely continuous bracket, or a fixed stochastic differential equation would omit cases covered by the source. The local-martingale integral also needs a continuous adapted version with a common almost-sure interpretation over all times; merely obtaining a separate fixed-time limit does not by itself supply that final identity. These requirements make the exact scope of the integral and bracket relations central to the formalization.

Formalization scope

The Lean declaration uses ℝ≥0 for time, Fin d → ℝ for state vectors, Measure Ω for the probability law, and Filtration ℝ≥0 for the filtration. It includes completeness of P, the initial-null-set condition on ℱ 0, continuity and adaptation of V and M, local bounded variation of V, stopping-time localization for M, the full decomposition of X, and continuous derivative witnesses for f. The final almost-everywhere quantifier precedes the universal time quantifier. There is no Brownian driver, global square-integrability requirement, right-continuity assumption on the filtration, or diagonal-only bracket simplification.

Five definitions are expression dependencies: IsSourceLocalMartingale, HasCrossVariation, itoStepSum, HasContinuousStieltjesIntegral, and HasContinuousMartingaleIntegral. Their staged declarations retain the reviewed source definitions under a consistent EthierKurtz namespace. The dyadic-sum definitions do not embed the change-of-variables identity, so the theorem cannot be discharged by unfolding a definition of the desired answer. The mission asks for a proof of the stated result, not a weakened special case. The empty-coordinate case is admitted consistently; no positive-dimensional source case is excluded.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986 (held reprint 1986/2005), Chapter 5, Section 2, Theorem 2.9, printed p. 287 (PDF p. 296), equations (2.40)–(2.41). Conventions: printed pp. 279–280 and 286 (PDF pp. 288–289 and 295). Cross variation: Chapter 2, equation (6.4), printed p. 79 (PDF p. 88).

Motivation

Continuous-time Markov processes are often studied through operators that describe how observables evolve. The generation question asks when an operator specified on a domain actually determines a strongly continuous family of contractions. Ethier and Kurtz place this question at the start of Markov Processes: Characterization and Convergence because the resulting semigroup language supports their later treatment of processes and convergence. This mission records the full generation characterization in Chapter 1, Theorem 2.6, and retains the related perturbation result in Theorem 7.1.

Setting

Let (E) be a real Banach space. A linear operator (A) has a linear domain (D(A)\subseteq E), which need not equal (E). A family (T(t)), for nonnegative real (t), consists of bounded linear maps (E\to E). It is a strongly continuous contraction semigroup when (T(0)) is the identity, (T(s+t)=T(s)T(t)), every (T(t)) has norm at most one, and (T(t)x\to x) as (t\downarrow0) for every (x\in E). Its infinitesimal generator has exactly those (x) for which the right-hand difference quotient (t^{-1}(T(t)x-x)) converges, and sends each such (x) to the limit.

An operator is dissipative here when

The range condition for a positive (r) says every vector in (E) is (rx-Ax) for some (x\in D(A)). Density means that vectors in (D(A)) approximate every vector in (E). These are independent requirements in the formal statement; neither the domain nor the operator is assumed closed or bounded.

For the related perturbation theorem, (A) and (B) may have different domains. Their sum uses the intersection of those domains. Closure is closure of the graph in (E\times E). A graph closure is required to be the graph of a single-valued operator before it can be called a generator.

Formalization targets

Theorem 2.6: generation characterization

The goal is the equivalence

The left side uses the full infinitesimal-generator domain, rather than agreement with a generator only on a smaller subdomain. The right side includes dissipativity for every positive parameter and full surjectivity for at least one positive parameter.

Theorem 7.1: relatively bounded perturbation

The retained related result assumes that the closure of (A) is single-valued and generates a strongly continuous contraction semigroup, (D(A)\subseteq D(B)), and (B) is dissipative. It further assumes

It concludes that the closure of (A+B) is single-valued and generates such a semigroup, and that its entire graph equals the sum of the graph closures of (A) and (B). This theorem is a related generation variant within the same mission, not a separate main goal.

Significance

The equivalence turns an existence question about a family of operators into conditions on a single potentially unbounded operator. In particular, it preserves the exact-domain requirement: proving only that a semigroup generator extends (A) would answer a weaker question. The perturbation theorem then identifies circumstances under which an already generating operator remains useful after adding a dissipative term that need not itself be bounded.

The textbook proves both statements. The Lean files supplied here are statements with intentional proof holes; they do not claim machine-checked proofs. A completed formalization would supply proofs of these source results while keeping the domain, range, closure, and relative-bound conditions shown in the statements.

Difficulty

The hypotheses describe a linear map on only part of the Banach space, while the conclusion requires bounded operators on all of (E) at every nonnegative time. Checking a semigroup law on a convenient subspace is insufficient unless the resulting operators and generator have the stated full domains. For perturbations, graph closure can enlarge a domain. An equality of formulas on (D(A)) alone would therefore omit the theorem's graph and domain conclusion.

Formalization scope

Lean uses NormedAddCommGroup E, NormedSpace ℝ E, and CompleteSpace E for the real Banach space; Submodule ℝ E for each domain; D →ₗ[ℝ] E for an operator that need not be bounded; and E →L[ℝ] E for each semigroup operator. Semigroup values at negative real times are unconstrained. The derivative is the right limit through positive times. Graph closure is topological closure in the ambient product, and graph sum requires a common input. The strict relative bound (\alpha<1) and positive resolvent parameter remain explicit.

The reusable definitions are the semigroup predicate, full generator predicate, operator graph, and graph sum. The mission welcomes proofs of the two stated theorems and genuinely source-based supporting lemmas. A model with an empty operator domain, an operator restricted from a larger generator, or a conclusion that drops the graph equality would not satisfy the target.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 1, Sections 2 and 7, Theorems 2.6 and 7.1. Book record.

Motivation

Minimum mean square error (MMSE) estimation — predicting a signal $x$ from a noisy observation $y$ by minimizing expected squared prediction error — underlies linear systems theory, linear regression, Kalman filtering, and multiple-input multiple-output signal processing. Its classical solution assumes the joint distribution of $(x,y)$ is known exactly; in practice it is estimated from data, and the estimator inherits sampling error and model risk. Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter shows that hedging the MMSE objective against every distribution in a Wasserstein ball around the empirical distribution — an infinite-dimensional worst case over an intractable set of measures, a priori — collapses to a tractable, finite-dimensional convex semidefinite program (Theorem 25, p. 29), building on the Gelbrich-hull machinery of Section 2.3. This mission formalizes that reduction.

Setting

Fix $m_x, m_y \in \mathbb{N}$ and let $\xi = (x,y) \in \mathbb{R}^{m_x} \times \mathbb{R}^{m_y}$ be a random vector: $x$ the signal to be estimated, $y$ the observation. An estimator is a measurable function $\psi : \mathbb{R}^{m_y} \to \mathbb{R}^{m_x}$; write $\Psi$ for the family of all estimators. The distribution of $\xi$ is only known to lie in a type-2 Wasserstein ball $B_{\varepsilon,2}(\hat P_N)$ centered at an elliptical nominal distribution $\hat P_N = E_g(\hat\mu,\hat\Sigma)$ with nominal mean $\hat\mu \in \mathbb{R}^m$ ($m=m_x+m_y$), nominal covariance $\hat\Sigma \in S^m_+$, and density generator $g$. The distributionally robust MMSE estimation problem is

Writing $\hat\Sigma = \begin{pmatrix}\hat\Sigma_{xx}&\hat\Sigma_{xy}\\\hat\Sigma_{yx}& \hat\Sigma_{yy}\end{pmatrix}$ blockwise, the nonlinear convex SDP

is the finite-dimensional relaxation the chapter builds toward.

Formalization targets

Goal (Theorem 25, distributionally robust MMSE estimator). If $\hat\Sigma \succ 0$, then the optimal value of problem (35) equals the optimal value of SDP (36). Moreover, if $S^\star$ is optimal in (36) with $S^\star_{yy}$ invertible, then the affine function

attains the outer infimum of (35) — it is a distributionally robust MMSE estimator, exhibited in closed form from an SDP optimizer.

Significance

Theorem 25 reduces an a priori infinite-dimensional, worst-case functional optimization problem (an infimum over all measurable estimators of a supremum over all distributions within a Wasserstein ball) to a finite convex program with one linear matrix inequality, one Loewner-order lower bound, and one trace/matrix-square-root constraint — solvable in polynomial time, with the optimal estimator recovered in closed form from the SDP's optimal block matrix. It shows that robustifying MMSE estimation against distributional ambiguity does not sacrifice tractability: the resulting estimator remains affine, the same functional form as the classical (non-robust) best linear unbiased estimator, only with its coefficients drawn from a regularized covariance estimate rather than the raw sample covariance. Formalizing it fixes, machine-checkably, the exact shape of that regularization — which SDP constraints are load-bearing (the Loewner lower bound in particular rules out a numerically unstable near-singular $S_{yy}$) and which conditions ($\hat\Sigma \succ 0$, $S^\star_{yy}$ invertible) the closed-form estimator formula actually needs.

Difficulty

The paper's own remark (p. 29) names the two nontrivial steps: first, "establishing a minimax theorem for (35) and exploiting the properties of elliptical distributions" to show the outer infimum is attained by an affine estimator — a priori (35) ranges over all measurable $\psi$, and there is no obvious reason the worst case forces linearity. Second, "combining this structural insight with Theorem 16" (the SDP-representability result for indefinite quadratic losses under an elliptical nominal distribution, itself a nontrivial closed-form reduction of an infinite-dimensional worst-case risk) to convert the now-restricted problem over affine estimators into the finite SDP (36). Neither step is a routine consequence of the ambiguity-set definitions alone; each requires structural facts about elliptical distributions and quadratic losses proved earlier in the chapter.

Formalization scope

The signal-observation space is EuclideanSpace ℝ (Fin mx ⊕ Fin my), with $x$ and $y$ recovered as the two summand projections; the block matrix $S$ is Matrix (Fin mx ⊕ Fin my) (Fin mx ⊕ Fin my) ℝ, and Matrix.toBlocks₁₁/toBlocks₁₂/toBlocks₂₁/toBlocks₂₂ give its four blocks. The constraint "$S_{xy}=S_{yx}^\top$" is not stated as a separate hypothesis: it follows automatically once $S$ is symmetric (implied by S.PosSemidef), so encoding the feasible set from a single symmetric S rather than four independently-quantified blocks makes it structurally impossible to drop — see pitfall 4 of BRIEF.md. The outer infimum of problem (35) ranges only over measurable $\psi$ (Measurable ψ on the binder), matching the paper's own definition of $\Psi$ as "the family of all possible measurable estimators" (p. 29) exactly. λ_min(Σ̂) is taken as a hypothesis parameter characterized by the two properties that make it the minimum ("≤ every eigenvalue of Σ̂, and attained by some eigenvalue"), rather than invoking a specific Mathlib min-eigenvalue API by name. S_{yy}⁻¹ uses the ordinary matrix inverse (junk zero matrix when singular), matching the paper's literal notation; S^\star_{yy} invertible is stated as an added hypothesis, not present verbatim on the page, because the paper leaves the formula's well-definedness implicit — disclosed per pitfall 5 rather than silently assumed away. The paper's own "which is always solvable" clause is not asserted: Theorem 25 states, as part of itself, that SDP (36) attains its maximum (an unconditional existence claim for an optimal $S^\star$); this formalization states only the conditional consequences of such an $S^\star$ existing, not that one does — proving or asserting solvability is out of this mission's scope, so the Lean statement is strictly weaker than Theorem 25's own conclusion on this point, disclosed rather than silently dropped. All risk-style suprema are EReal-valued and Integrable-guarded, matching the series' convention. No milestone theorem is included: the paper's own proof sketch derives (33)'s and by extension (36)'s SDP "via Theorem 16", but Theorem 16 (indefinite quadratic loss and $p=2$, eq. 23) was itself judged too heavy to state faithfully in 02-gelbrich's time budget and is not redefined here either — see STATUS.md. Theorem 24 (the Wasserstein shrinkage estimator, this chapter's originally recommended goal) is out of scope: its closed-form eigenvalue transformation (eq. 34a/34b) requires transcribing nested square roots from a rendered PDF page that this session's time budget did not allow verifying to the standard the brief demands (pitfall 1); the brief's own documented fallback to Theorem 25 was taken instead.

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research. https://doi.org/10.1287/educ.2019.0198
• Nguyen, V. A., Shafieezadeh-Abadeh, S., Yue, M.-C., Kuhn, D., & Wiesemann, W. (2021). Optimistic distributionally robust optimization for nonparametric likelihood approximation. Advances in Neural Information Processing Systems, 32.
• Shafieezadeh-Abadeh, S., Nguyen, V. A., Kuhn, D., & Mohajerin Esfahani, P. (2018). Wasserstein distributionally robust Kalman filtering. Advances in Neural Information Processing Systems, 31.

Motivation

Every consistency guarantee for an empirical-risk-minimization procedure — the Lasso, kernel ridge regression, maximum likelihood — ultimately rests on relating an empirical average to its population expectation, uniformly over the class of candidate functions or parameters being searched. Chapter 4 established the classical form of this connection: a uniform law of large numbers, bounding $\sup_{f\in F}|\|f\|_n^2-\|f\|_2^2|$ by an absolute quantity governed by the (unlocalized) complexity of $F$. Such a bound is often wasteful: it treats a function with small population norm the same as one with large population norm, when intuitively the empirical and population norms of a small function should already agree closely. This mission formalizes the sharper, localized form of this uniform law — the same localization principle Chapter 13 used for nonparametric least squares, now applied directly to the empirical-versus-population norm comparison itself, giving relative rather than absolute control and recovering optimal convergence rates that the unlocalized theory misses.

Setting

Fix a probability distribution $P$ over a covariate space $X$ and $n$ i.i.d. samples $x_1,\dots,x_n\sim P$. For $f:X\to\mathbb R$, the population norm is $\|f\|_2^2:=\int_Xf(x)^2\,P(dx)$ and the empirical norm is $\|f\|_n^2:=\frac1n\sum_{i=1}^nf(x_i)^2$; by linearity of expectation, $\mathbb E[\|f\|_n^2]=\|f\|_2^2$, so the question is how tightly $\|f\|_n^2$ concentrates around $\|f\|_2^2$, uniformly over a function class $F$. A class $F$ is star-shaped around the origin if $f\in F,\alpha\in[0,1]\implies\alpha f\in F$, and $b$-uniformly bounded if $\|f\|_\infty\le b$ for every $f\in F$. The relevant complexity measure is the population localized Rademacher complexity

where $\varepsilon_1,\dots,\varepsilon_n$ are i.i.d. Rademacher signs independent of the samples — note that, unlike Chapter 13's Gaussian complexity for fixed design points, this expectation integrates out the randomness of the samples themselves, since this chapter treats $\{x_i\}$ as genuinely random throughout. A critical radius $\delta_n$ is any positive solution of $R_n(\delta;F)\le\delta^2/b$.

Formalization targets

Theorem 14.1 (goal). Given $F$ star-shaped and $b$-uniformly bounded, and $\delta_n$ solving the critical inequality, for any $t\ge\delta_n$,

with probability at least $1-c_1e^{-c_2nt^2/b^2}$; and if additionally $n\delta_n^2\ge\frac2{c_2}\log(4\log(1/\delta_n))$,

with probability at least $1-c_1'e^{-c_2'n\delta_n^2/b^2}$.

Significance

Theorem 14.1 is the technical engine behind two of the book's other sharp results: Example 14.2's derivation of the optimal $n^{-1/2}$ rate for bounded quadratic function classes (where the unlocalized analogue of this theorem only achieves the slower $n^{-1/4}$ rate), and, more broadly, every later argument in the book that needs to translate an empirical-norm guarantee (as produced directly by an M-estimator's optimality, e.g. Chapter 13's nonparametric least-squares bounds) into a population-norm guarantee, or vice versa. The gap between the "absolute" uniform law of Chapter 4 and the "relative" one here is exactly the difference between a bound that is only informative for functions of order-one population norm, and one that remains sharp arbitrarily close to the origin — which is precisely where a consistent estimator's error eventually lives. Formalizing the statement produces, for the first time on the platform, the localized-Rademacher-complexity vocabulary at the population level (as opposed to Chapter 13's fixed-design Gaussian-complexity version), reusable by any future mission needing to pass between empirical and population norms.

Difficulty

The naive approach — apply Hoeffding's inequality to $|\|f\|_n^2-\|f\|_2^2|$ for a fixed $f$, then union-bound (or apply the unlocalized Rademacher-complexity uniform law of Chapter 4) over $F$ — gives a bound whose complexity term does not shrink as $\|f\|_2\to0$, since it uses the complexity of all of $F$ regardless of a given function's own size. This is exactly the sub-optimality Example 14.2 exhibits concretely: the naive bound gives rate $n^{-1/4}$ where the truth is $n^{-1/2}$. The fix is not merely technical bookkeeping — it requires a genuine peeling argument over dyadic norm-scales (exactly as in Chapter 13's proof of Theorem 13.13), applying the localized complexity $R_n(\delta;F)$ at the scale $\delta=\|f\|_2$ appropriate to each individual $f$, and controlling the resulting geometric sum of tail probabilities across scales. A reader's first instinct — bound $\|f\|_2$ in terms of $\|f\|_n$ and substitute — is circular, since $\|f\|_n$ is itself the random quantity being controlled.

Formalization scope

The covariate space X carries an arbitrary MeasurableSpace structure (no topology needed for the statement); the sample sequence and the Rademacher signs are both represented as families of measurable functions on a shared probability space Ω, with their joint independence stated as a single IndepFun between the two vector-valued sequences (rather than building a combined-index iIndepFun), since it is the two sequences — not each pair of individual variables — whose independence the book invokes. The two conclusions of Theorem 14.1 are stated as a conjunction with the second gated behind its own extra hypothesis, never collapsed into a single implication, since the book's own statement keeps them syntactically and logically distinct (the second requires a strictly stronger and additional condition on top of the first's). The universal constants (c1,c2,c0,c1',c2') are quantified before every instance object, so they cannot secretly depend on the function class, sample size, or radius. Every f ∈ F is required measurable (hF_meas, added in revision): the book's own framing implicitly restricts to measurable, square-integrable f throughout (p. 454), and without this hypothesis the population norm popNormSq, which appears directly in the goal's conclusion, could silently take Mathlib's Bochner-integral junk value 0 for a non-measurable, pointwise-bounded member of a star-shaped, uniformly-bounded F. The trivializing formalization ruled out here is stating the localization constraint at the empirical rather than population norm in popRademacherComplexity — this chapter's whole point (contrast Chapter 13's Gn, correctly localized at the empirical norm since there the design is fixed) is that $R_n(\delta;F)$'s localization is a population-level object, precisely because the samples are random here. Welcome future contributions: Corollary 14.3's covering-number sufficient condition for the empirical version of the critical inequality, and Theorem 14.20's Lipschitz/strongly-convex cost-function uniform law, both deferred from this mission (see STATUS.md) as they need substantial additional apparatus (metric entropy integrals; cost functions and strong convexity) beyond what Theorem 14.1 itself requires.

Selected references

• M. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Chapter 14. https://doi.org/10.1017/9781108627771
• P. Bartlett, O. Bousquet and S. Mendelson, "Local Rademacher complexities," Annals of Statistics, 33(4):1497-1537, 2005. https://doi.org/10.1214/009053605000000282
• V. Koltchinskii, "Local Rademacher complexities and oracle inequalities in risk minimization," Annals of Statistics, 34(6):2593-2656, 2006. https://doi.org/10.1214/009053606000001019

Motivation

Many high-dimensional data sets — gene-expression profiles, sensor networks, social interactions — come with no natural ordering of variables, only pairwise dependencies whose structure is itself the object of interest. A graphical model encodes these dependencies as an undirected graph: vertices are variables, and edges mark direct (conditional) dependence. Recovering the graph from samples — graphical model selection — is a combinatorial problem masquerading as a statistical one: there are $2^{\binom{d}{2}}$ candidate graphs on $d$ vertices, far too many to search directly. For Gaussian data, however, graph structure is exactly the sparsity pattern of the inverse covariance (precision) matrix, which turns graph selection into $d$ coupled sparse-regression problems — one per vertex — each of which the Lasso theory of Chapter 7 already knows how to solve. This mission formalizes the theorem, due to Meinshausen and Bühlmann (2006), that shows this reduction actually works: solving $d$ independent Lasso problems and combining the results recovers the exact graph with high probability, at a sample complexity governed by the same kind of incoherence condition that governs Lasso support recovery itself.

Setting

An undirected graphical model on a finite vertex set $V$ pairs a graph $G=(V,E)$ with a random vector $X=(X_j)_{j\in V}$. Two equivalent structural properties connect $X$ to $G$ (Theorem 11.8, Hammersley-Clifford): $X$ factorizes according to $G$ if its density is a product of nonnegative functions, one per clique of $G$, each depending only on the variables in that clique (Definition 11.1); $X$ is Markov with respect to $G$ if, for every vertex cutset $S$ separating $V$ into disjoint pieces $A$ and $B$, the sub-vectors $X_A$ and $X_B$ are conditionally independent given $X_S$ (Definition 11.5). For a strictly positive density, these are the same condition.

For a zero-mean $d$-dimensional Gaussian vector with covariance $\Sigma^*$ and precision matrix $\Theta^*=(\Sigma^*)^{-1}$, the graph structure is exactly the support of $\Theta^*$: $(j,k)\in E \iff \Theta^*_{jk}\ne0$. The neighborhood $N(j):=\{k\mid(j,k)\in E\}$ of each vertex is itself a vertex cutset (separating $\{j\}$ from everything else), so the conditional independence $X_j\perp X_{V\setminus N^+(j)}\mid X_{N(j)}$ holds, and — by standard Gaussian conditioning — $X_j$ decomposes as a linear function of $X_{V\setminus\{j\}}$ plus independent Gaussian noise, with regression coefficients supported exactly on $N(j)$. Neighborhood regression exploits this directly: for each vertex $j$, solve the Lasso

read off $\hat N(j):=\{k\mid\hat\theta_{j,k}\ne0\}$, and combine the $d$ per-vertex estimates into a single edge set via the OR rule ($(j,k)\in\hat E_{\mathrm{OR}}$ iff $k\in\hat N(j)$ or $j\in\hat N(k)$) or the more conservative AND rule (iff both hold). The relevant incoherence condition, analogous to Chapter 7's, is stated for a positive definite matrix $\Gamma$ and subset $S$: $\Gamma$ is $\alpha$-incoherent with respect to $S$ if $\max_{k\notin S}\|\Gamma_{kS}(\Gamma_{SS})^{-1}\|_1\le1-\alpha$.

Formalization targets

Theorem 11.8 (Hammersley-Clifford). Factorizes G p ↔ IsMarkov G X P for any strictly positive density $p$.

Theorem 11.12 (goal — graph selection consistency). Suppose for every $j$, $\Sigma^*_{\setminus\{j\}}$ is $\alpha$-incoherent with respect to $N(j)$, and $|\!|\!|(\Sigma^*_{N(j),N(j)})^{-1}|\!|\!|_\infty\le b$. With $\lambda_n=c_0\frac1\alpha(\sqrt{\log d/n}+\delta)$, the neighborhood-Lasso estimate combined via either rule satisfies, with probability at least $1-c_2e^{-c_3n\min(\delta^2,1/m)}$:

Significance

Theorem 11.12 is the statistical justification for one of the two standard approaches to Gaussian graphical model selection (the other being the penalized-likelihood "graphical Lasso" of §11.2.1). Its significance is computational as much as statistical: rather than solving one $d$-dimensional penalized-likelihood problem, neighborhood regression solves $d$ independent, embarrassingly parallel Lasso problems, each of dimension $d-1$ — a substantial practical advantage at scale, with (as this theorem shows) no loss in statistical guarantee. Formalizing it produces, for the first time on the platform, statement-level infrastructure for undirected graphical models (Hammersley-Clifford, the Markov property via vertex cutsets, neighborhood structure) together with the random-design analogue of the Lasso support-recovery machinery — a genuinely different technical regime from Chapter 7's fixed-design Lasso theory, since here the "design matrix" $X_{\setminus\{j\}}$ is itself Gaussian and statistically coupled to the response $X_j$ through the very covariance structure being estimated. As with the other missions in this series, only the statements are formalized here; the proofs (an extension of the primal-dual witness technique to random design, per the book's own proof sketch) are left as the draft goal for future proof contributions.

Difficulty

The proof of Theorem 7.21 (Chapter 7's Lasso support-recovery guarantee) is for a deterministic design matrix, with all randomness confined to the additive noise. Here the "design" $X_{\setminus\{j\}}$ is itself random and Gaussian, and — critically — it is statistically dependent on the very quantity ($N(j)$, encoded in $\Theta^*$'s support) the Lasso is trying to recover, since $X_{\setminus\{j\}}$'s own covariance structure is exactly what the incoherence condition constrains. The naive approach of just conditioning on the realized design matrix and invoking Theorem 7.21 fails, because the deterministic-design incoherence condition would then need to hold for the sample covariance $\Gamma=\frac1n X_{\setminus\{j\}}^TX_{\setminus\{j\}}$, not the population covariance $\Sigma^*_{\setminus\{j\}}$ that is actually assumed — and controlling the gap between sample and population incoherence under the joint (not fixed) randomness of predictors and response is exactly the extra step the book's proof needs, handled via an extension of the primal-dual witness technique that tracks both sources of randomness together.

Formalization scope

The vertex set V is an arbitrary finite type; the covariate space for X is ℝ throughout (all variables jointly Gaussian). The Gaussian design is characterized via its one-dimensional projections (every linear combination is univariate Gaussian with the matching variance) rather than via Mathlib's multivariate-Gaussian machinery directly, to keep the definition self-contained. IsAlphaIncoherent's ambient index set is realized as a subset of the full vertex type rather than as a literal submatrix, since the book's condition never references an entry outside it. The theorem states the conclusion jointly for both the OR-rule and AND-rule estimated edge sets on one shared high-probability event, matching "based on either rule" literally rather than picking one. The trivializing formalization ruled out here is treating the neighborhood-Lasso estimate as a fixed-design Lasso problem (silently dropping the joint randomness of predictors and response) — every design realization in this formalization is the actual random vector Xdes i ω, not a deterministic parameter, and the Gaussian design hypothesis (IsIIDGaussianDesign) is stated over the same probability space Ω as the least-squares residual. Theorem 11.8 (Hammersley–Clifford) is formalized only for the continuous case — a random vector with a density with respect to Lebesgue measure — matching what the Gaussian goal (Theorem 11.12) actually needs; the book's own Definition 11.1 also permits a discrete (counting-measure) density, with the Ising model (Example 11.4) as a worked instance, which this mission does not cover. Contributions welcome: the graphical Lasso's own guarantees (Propositions 11.9, 11.10, deferred from this mission — see STATUS.md), and the proof of Theorem 11.12 itself via the primal-dual witness extension the book sketches.

Selected references

• M. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Chapter 11. https://doi.org/10.1017/9781108627771
• N. Meinshausen and P. Bühlmann, "High-dimensional graphs and variable selection with the Lasso," Annals of Statistics, 34(3):1436-1462, 2006. https://doi.org/10.1214/009053606000000281
• J. Hammersley and P. Clifford, "Markov fields on finite graphs and lattices," unpublished manuscript, 1971.

Motivation

A striking fact discovered by Dvoretzky in the 1960s (conjectured by Grothendieck, and sharpened into its modern quantitative form by Milman in 1971) is that every high-dimensional convex body, however irregular, contains a round slice: a random low-dimensional section (or projection) of any bounded convex set in $\mathbb R^n$ is, with high probability, close to a Euclidean ball — provided the dimension of the slice is small enough relative to a single geometric parameter of the body. This is remarkable because it holds for every bounded set, arbitrarily irregular; no special structure is assumed beyond boundedness. This chapter proves the theorem in its Gaussian form, as a culmination of every geometric and probabilistic tool the book develops: chaining and Dudley's inequality (Chapter 8), the matrix deviation inequality (Chapter 9), and Gaussian width and the stable dimension (Chapter 7) all combine into a single closing argument.

Setting

Fix a subset $T\subseteq\mathbb R^n$. For a standard Gaussian vector $g\sim N(0,I_n)$, the Gaussian width of $T$ is $w(T) := \mathbb E\sup_{x\in T}\langle g,x\rangle$ (Chapter 7), and the stable dimension of a bounded $T$ is $d(T) := w(T)^2/\mathrm{diam}(T)^2$ up to an absolute constant factor (Definition 7.6.2) — a robust substitute for the ordinary linear-algebraic dimension of $T$, which can jump discontinuously under a small perturbation of $T$, unlike $d(T)$.

An $m\times n$ Gaussian random matrix with i.i.d. $N(0,1)$ entries is a random matrix $A$ each of whose $mn$ entries is an independent standard normal random variable.

Formalization targets

Goal (Theorem 11.3.3, Dvoretzky-Milman's theorem, Gaussian form)

for every $m\times n$ Gaussian random matrix $A$ with i.i.d. $N(0,1)$ entries, every bounded $T\subseteq\mathbb R^n$ containing the origin, and every $\varepsilon\in(0,1)$, where $B$ is the Euclidean ball of radius $w(T)$ centered at the origin. The probability $0.99$ is the book's own literal numeral, not a free parameter — this is the theorem the book actually states, not a family of theorems indexed by a confidence level.

Significance

Dvoretzky-Milman's theorem is one of the foundational results of the local theory of Banach spaces (asymptotic geometric analysis): it says every $n$-dimensional normed space contains an almost-Euclidean subspace of dimension proportional to (a geometric invariant closely related to) $\log n$ in the worst case, and much larger for spaces whose unit ball is already well-behaved (the stable dimension of the cube $[-1,1]^n$, for instance, is proportional to $n$ itself — Example 11.3.6). This underlies results throughout convex geometry, compressed sensing, and high-dimensional statistics wherever a random low-dimensional projection needs to be shown to preserve geometric structure. The book's own framing makes clear why this chapter is placed last: the theorem's proof is a genuine capstone, invoking Chevet's inequality (itself built from the matrix deviation inequality of Chapter 9, which is built from chaining, Chapter 8) as its main technical tool.

The theorem and its proof are classical (Milman 1971; this book's specific route via Chevet's inequality is a standard modern exposition). This mission formalizes the goal theorem's statement — including its two supporting geometric quantities, Gaussian width and stable dimension, and the notion of a Gaussian random matrix — as a complete, faithful target for a solver, in the book's own sub-namespace built for this chapter (no dependency here is reusable from an earlier chunk, since none of this book series' Chapter 7 or Chapter 9 definitions has yet been published).

Difficulty

The natural first idea — bound $\mathrm{conv}(AT)$ directly using concentration of $\|Ax\|_2$ for each fixed $x\in T$ — runs into exactly the uniform-supremum obstacle the whole book has been building tools to overcome: a bound that holds for one $x$ at a time, even with a union bound over a net of $T$, does not obviously extend to the full convex hull without first controlling $\sup_{x\in T}|\langle Ax,y\rangle - w(T)\|y\|_2|$ uniformly over both $x\in T$ and $y$ on the unit sphere of the target space — a two-parameter supremum. The book's actual route goes through Chevet's inequality, itself proved using the matrix deviation inequality's own chaining-based argument, to control this two-sided supremum, and then converts the resulting inequality into the containment $(1-\varepsilon)B\subseteq\mathrm{conv}(AT)\subseteq(1+\varepsilon)B$ via a support- function duality argument (a convex body is pinned down by its support function, so bounding $\sup_{x\in T}\langle Ax,y\rangle$ uniformly over $y$ on the sphere is exactly what is needed).

Formalization scope

A is Ω → Matrix (Fin m) (Fin n) ℝ with an explicit IsGaussianMatrix hypothesis (entries i.i.d. $N(0,1)$, formalized entrywise with joint independence). conv(AT) is convexHull ℝ of the image of T under A's mulVec, round-tripped through EuclideanSpace's continuous linear equivalence with the underlying function type. w(T) reuses this mission series' ExpSup/GaussianWidth convention (redefined locally, per the drafts-cannot-import-drafts rule, following the same ProbabilityTheory.stdGaussian-based realization of a standard Gaussian vector as 08-matrix-deviation). The stable dimension $d(T)$ is formalized directly as $w(T)^2/ \mathrm{diam}(T)^2$ rather than via the book's literal (but only asymptotically equivalent, per Exercise 7.6.1) definition through a squared Gaussian width $h(T-T)^2$ — the goal theorem's own proof uses only the inequality direction of that equivalence, and the goal's hypothesis already carries an unpinned absolute constant that absorbs the equivalence constant, so this substitution preserves the theorem's exact truth content (see StableDimension's own doc-comment and MODERATION_NOTES.md for the full argument) rather than approximating it.

Ball-center deviation, disclosed. The book's printed theorem statement carries no hypothesis that $T$ contains the origin; its proof opens by translating $T$ so that it does ("Translating $T$ if necessary, we can assume that $T$ contains the origin"), and Remark 11.3.4 then confirms the ball is centered at the origin in that case. This mission states the WLOG-reduced case directly — adding $0\in T$ as an explicit hypothesis — rather than also formalizing the translation argument that recovers the fully general (untranslated) statement. This is disclosed as a genuine narrowing of the literal printed statement, though not of what the book's own proof actually establishes.

This mission covers Theorem 11.3.3 only, with no milestones: BRIEF.md explicitly instructs that if the chapter's full proof chain (general matrix deviation inequality, Chevet's inequality, random projections of sets — Theorems 11.1.5, 11.2.4, 11.3.1) proves too heavy for the session, milestones should be cut rather than the goal substituted. All three are left out, not approximated, given this chapter's five from-scratch definitions already needed for the goal's own statement. ExpSup, GaussianWidth, StableDimension and IsGaussianMatrix are reusable by any later development needing Gaussian width, the stable dimension, or a Gaussian random matrix. Solvers' contributions are welcome on the goal theorem itself and, beyond this mission's current scope, on the three named milestones.

Selected references

• A. Dvoretzky, Some results on convex bodies and Banach spaces, Proc. Internat. Sympos. Linear Spaces (Jerusalem, 1960), 123–160.
• V. D. Milman, A new proof of A. Dvoretzky's theorem on cross-sections of convex bodies, Funkcional. Anal. i Priložen. 5 (1971), 28–37.
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 11. https://doi.org/10.1017/9781108231596

Motivation

Most stochastic programs cannot be solved exactly: the expectation defining the objective is an integral over a continuous or high-dimensional random parameter, and evaluating it exactly is as hard as the optimization itself. The standard remedy is Monte Carlo: draw a sample of size ν from the random parameter, replace the true expectation by the sample average, and solve the resulting finite-dimensional "sample average approximation" (SAA) instead. This only helps if the SAA's optimal value and optimal solution actually converge to the true problem's as ν → ∞, and if that convergence is fast enough to be useful with a sample size one can actually draw and solve. Birge & Louveaux's Chapter 9, §9.5, states the two central asymptotic results that justify this approach for a general (not necessarily linear, not necessarily two-stage) stochastic program: a central limit theorem describing the SAA optimal value's fluctuations around the truth (Theorem 6, after Shapiro [1991]), and an exponential-rate large-deviation bound on how quickly both the SAA value and the SAA solution concentrate near their true counterparts as the sample grows (Theorem 7, after Dai, Chen & Birge [2000]). This mission formalizes both statements.

Setting

Fix a feasible set X ⊆ ℝⁿ of first-stage decisions and an outcome space Ξ carrying a σ-algebra. The book considers the general stochastic program

z* = inf_{x ∈ X} ∫_Ξ g(x,ξ) P(dξ),                                                        (5.1)

with g : ℝⁿ × Ξ → ℝ an abstract integrand — no longer specialized to the two-stage recourse cost Q(x,ξ) of Chapters 3–7, matching the book's own level of generality at this point in §9.5 — and ξ a random element of (Ξ, 𝓑, P). Given an i.i.d. sample ξ₁, ξ₂, … from P, the sample average approximation of size ν is

zν = inf_{x ∈ X} (1/ν) Σᵢ₌₁^ν g(x,ξᵢ) .                                                    (5.2)

Both z* and zν are attained (an optimal solution x* of (5.1); a random optimal solution xν(ω) of (5.2) at each sample outcome ω). The two chapter results describe, in different regimes, how (zν, xν) relates to (z*, x*) as ν → ∞.

Formalized in this mission: X sits in EuclideanSpace ℝ (Fin n); the sample is a sequence ξ : ℕ → Ω → Ξ on an ambient probability space (Ω, P), independent and identically distributed (Mathlib's iIndepFun/IdentDistrib); z*, x*, zν, xν are given as hypotheses that pin them down as the optimal value and an optimal point of (5.1)/(5.2) (a lower bound over X plus attainment at the named point), rather than computed via sInf/sSup of an image set — Real's extended-real infimum returns the junk value 0 on an unbounded-below or empty set, which would silently misstate the theorems if X, g are only assumed as loosely as the book states them.

Formalization targets

Goal — Chapter 9, Theorem 7 (p. 412)

∀ ε>0, ∃ α>0, ∃ β>0,
  (∀ ν>0, P[|zν − z*| ≥ ε] ≤ α·e^{−βν})
  ∧ (x* the unique optimal solution of (5.1) → ∀ ν≥1, P[‖xν − x*‖ ≥ ε] ≤ α·e^{−βν})

under the moment hypothesis: there exist a>0, θ₀>0, η : Ξ → ℝ with |g(x,ξ)| ≤ a·η(ξ) for all x ∈ X, and E[e^{θ·η(ξ)}] < ∞ for every θ ∈ [0,θ₀]. This is the mission's goal because it is a clean, self-contained existential-constants statement — no algorithm to define, unlike most of the chapter's other convergence results — and because, like Chunk 03's Theorem 6(a), the book's own proof cites an external paper (Dai, Chen & Birge [2000], Theorems 3.1–3.2) and gives no in-text derivation: the statement itself, not a derivation from a preceding numbered result of this book, is the mission's content.

Milestone — Chapter 9, Theorem 6 (p. 411)

X compact, g(x,·) measurable ∀x∈X, g Lipschitz in x with an L²(μ) envelope a,
x0 the unique minimizer of x ↦ E g(x) over X
  ⟹ √ν·[zν − E g(x0)] converges in distribution to N(0, Var g(x0))

Included as a milestone (not used in Theorem 7's proof, which the book does not give — see above) because it is the chapter's other general SAA convergence result, standing on the same setup (5.1)–(5.2), and because Mathlib's MeasureTheory.Function.ConvergenceInDistribution (the TendstoInDistribution predicate) plus Probability.Distributions.Gaussian.Real (gaussianReal) and Mathlib's own i.i.d. central limit theorem (ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub) supply exactly the vocabulary needed to state — not prove — a faithful weak-convergence-to-Gaussian conclusion. Chunk 09's BRIEF.md flagged this as a milestone to attempt "only if your workspace has enough of a weak-convergence/CLT toolkit in Mathlib to state it faithfully"; the toolkit is present (verified directly, not assumed from substrate.md, which predates this rev's addition of ConvergenceInDistribution.lean), so it is included.

Significance

Every practical Monte Carlo solution method for stochastic programming — every discretization, every scenario-reduction heuristic, every "solve on a sample and hope" approach used throughout the rest of the book and the wider literature — rests on exactly these two results: that the SAA converges at all (Theorem 6's CLT gives the asymptotic distribution of the error) and that it converges fast enough to bound the error at a finite, computable sample size (Theorem 7's exponential rate). Formalizing them gives Prove2Me a first foothold in convergence-rate theory for stochastic optimization under sampling, a genre distinct from the concentration-of-measure results already reachable via Mathlib's sub-Gaussian machinery (Probability/Moments/SubGaussian.lean): sub-Gaussian concentration bounds a fixed-size sample's deviation from its own mean, not the rate-in-ν convergence of a nested sequence of optimization problems' values and solutions to a limiting problem's — the object Theorem 7 is actually about.

Difficulty

Theorem 6 needs a functional/uniform argument over the whole feasible set X (not the plain i.i.d. CLT at the single point x0) to control the interaction between sampling noise and the optimization over x; the book states it without proof, citing Shapiro [1991]. Theorem 7's constants α, β are produced by a large-deviation argument specific to the exponential-moment condition, again cited rather than derived in the book. Both are left as sorry; the value of this mission is the faithful statement, matching the difficulty pattern already established for Chunk 03's Theorem 6(a) (a result the book itself only cites).

Formalization scope

• Existential constants left abstract, never sharpened or weakened. Theorem 7's α, β are ∃-bound exactly as the book leaves them (trap 8 of reference/FAITHFULNESS_TRAPS.md: the existentials sit outside every quantifier they must be uniform over — in particular outside the ∀ ν). No closed form for α, β in terms of a, θ0, ε is invented.
• The book's own typo is corrected, and the correction is flagged. The printed (5.8) reads P[E[zν − z*)] ≥ ε] ≤ αe^{−βν} — an unmatched parenthesis and a stray E[·] around a quantity that is already deterministic. milestones.yaml/MODERATION_NOTES.md quote the typo verbatim; the Lean and natural_language_statement use the unambiguous P[|zν − z*| ≥ ε] the surrounding prose (and every other occurrence of this quantity in the section) plainly intends.
• g is left fully abstract, not specialized to the two-stage recourse cost Q(x,ξ) of Chunks 03–07, matching §9.5's own generality and keeping this mission independent of every other chunk's namespace (no cross-chunk import, per missions/README.md's "Prior art" column for this chunk: "none expected").
• z*, x*, zν, xν are hypothesis-characterized, not sInf/sSup-defined, to avoid the real extended-value junk-value trap (trap 5) discussed under Setting above.
• Measurability of zν, xν is an added hypothesis (hzSAA_meas/hxSAA_meas/hzSAA_meas in Theorem 6), not derivable from the other hypotheses since g is abstract; the book is silent on this technical point, standard for an applied convergence theorem, but Lean's P {ω | …} needs it for the displayed probability to be the actual measure of the event rather than an outer-measure value on a possibly non-measurable set.
• Convergence in distribution (Theorem 6) is formalized via Mathlib's TendstoInDistribution, with the limiting Gaussian supplied as an explicit random variable Y on a separate probability space with HasLaw Y (gaussianReal 0 σ²) P' — the same pattern Mathlib's own CLT (tendstoInDistribution_inv_sqrt_mul_sum_sub) uses for its own conclusion.
• Trivialization risk (this chapter's own, beyond paper.md's book-wide list item 5). A formalization that quantifies α, β universally, or with an invented closed form, would assert something the book's proof (cited, not given) does not establish; a formalization of Theorem 7 that used a computable sInf-defined zν on a set that is not shown bounded below would let the conclusion hold vacuously via the junk value 0, independent of the genuine large-deviation content — both are excluded by the choices above.

Selected references

• Birge, J.R., Louveaux, F. Introduction to Stochastic Programming, 2nd ed., Springer 2011, Chapter 9, §9.5 (pp. 409–412).
• Shapiro, A. "Asymptotic properties of statistical estimators in stochastic programming." Annals of Statistics 19 (1991), 1463–1466 — proof of Theorem 6 (their Theorem 3.3).
• Dai, L., Chen, C.-H., Birge, J.R. "Convergence properties of two-stage stochastic programming." Journal of Optimization Theory and Applications 106 (2000), 489–509 — proof of Theorem 7 (their Theorems 3.1–3.2).
• King, A.J., Rockafellar, R.T. "Asymptotic theory for solutions in statistical estimation and stochastic programming." Mathematics of Operations Research 18 (1993), 148–162 — the general theory of §9.5's opening (Theorem 5), the chapter's third general result, not formalized here (see STATUS.md for why it is out of scope).

Motivation

The central limit theorem says that $S_n/\sqrt n$ converges to a normal random variable. Donsker's theorem says something much stronger: the whole rescaled path of the random walk converges to the whole path of a Brownian motion, as a random element of $C[0,1]$.

The payoff is a machine. Once $S(n\cdot)/\sqrt n\Rightarrow B(\cdot)$ in $C[0,1]$, every functional of the path that is continuous — or merely continuous at almost every Brownian path — transfers automatically. The maximum of the walk converges to the maximum of Brownian motion; the fraction of time the walk spends above a level converges to the corresponding occupation time; the last zero before time $n$ converges to the last Brownian zero before time $1$, which is how the arcsine law escapes the simple random walk it was proved for. This is the invariance principle of Erdős and Kac: the asymptotic behaviour of a functional of $S_n$ should not depend on the step distribution, as long as the central limit theorem applies.

Chapter 8 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) proves this by embedding rather than by the usual tightness argument. Skorokhod's representation theorem puts a mean-zero, finite-variance random variable inside a Brownian motion as the value at a stopping time; iterating puts the whole walk inside one Brownian motion at a sequence of stopping times whose gaps are i.i.d.; and the law of large numbers then forces the embedded walk to be uniformly close to the Brownian path.

Setting

Let $X_1,X_2,\dots$ be i.i.d. with mean $0$ and variance $1$, and $S_m=X_1+\dots+X_m$. Define $S(u)$ to be $S_m$ at integer $u=m$ and linear in between, and set

a random element of $C[0,1]$, the continuous functions on the unit interval with the uniform norm and its Borel $\sigma$-algebra.

On the Brownian side, let $B$ be a Brownian motion, and write $B(\cdot)$ for its restriction to $[0,1]$, again a random element of $C[0,1]$.

Formalization targets

Goal — Theorem 8.1.4, Donsker's theorem

that is, the laws of $W_n$ on $C[0,1]$ converge weakly to the law of Brownian motion. This is a statement about measures on a function space, not about finite-dimensional marginals: it is exactly the extra content over the central limit theorem.

Supporting levels

Theorem 8.1.1, Skorokhod's representation theorem: a mean-zero, square-integrable law is the law of $B_T$ for a stopping time $T$ with $\mathbb ET=\mathbb EX^2$; Theorem 8.1.2, the embedding of the whole walk, giving stopping times $T_0=0,T_1,\dots$ with $(B(T_n))_n$ distributed as the walk and with i.i.d. gaps; Theorem 8.1.5, the continuous mapping theorem for almost surely continuous functionals; and its two workhorse instances, Example 8.1.6 on maxima and Example 8.1.8 on occupation times of half-lines.

Significance

The results themselves. Donsker's theorem is the reason the arcsine law, the distribution of the maximum, and the occupation-time law are universal rather than artefacts of the simple random walk for which they were first computed. It is also the prototype for every later functional limit theorem — for martingales in Durrett's section 8.2, for stationary sequences in 8.3, for the empirical process converging to a Brownian bridge in 8.4.

Skorokhod's embedding deserves separate billing. It says any centred law with finite variance sits inside Brownian motion, which is what makes the path-space comparison possible at all, and it is the tool behind the law of the iterated logarithm in Durrett's section 8.5. The construction is a two-point mixture: write the law as a mixture of two-point laws $\mu_{u,v}$ with mean zero, use the exit time of $(u,v)$ for each, and the exit-time identity $\mathbb ET_{a,b}=-ab$ integrates to $\mathbb EX^2$.

Formalizing them. Mathlib has the i.i.d. central limit theorem, convergence in distribution for random elements of an arbitrary topological space (TendstoInDistribution, with the continuous mapping theorem and Slutsky), Brownian motion as a process with its invariances, and the machinery of stopping times for filtered spaces. It has no functional limit theorem of any kind, no Wiener measure on $C[0,1]$, no Skorokhod embedding, and no continuous-time optional stopping. Nothing in the library relates a random walk to a Brownian path.

Difficulty

The goal is the hardest item in this series, and the embedding route is the reason the mission is stated the way it is. Durrett's proof: with $X_{n,m}=X_m/\sqrt n$ and stopping times $\tau^n_m$ realizing $(S_{n,1},\dots,S_{n,n})$ as $(B(\tau^n_1),\dots,B(\tau^n_n))$, Lemma 8.1.9 says that if $\tau^n_{\lfloor ns\rfloor}\to s$ in probability for each $s\in[0,1]$, then $\|S_{n,(n\cdot)}-B(\cdot)\|_\infty\to0$ in probability. The hypothesis is the weak law applied to the i.i.d. gaps of Theorem 8.1.2 after Brownian scaling; the conclusion plus the converging-together lemma gives the theorem. The work is uniform control of the Brownian path over shrinking time windows — the modulus of continuity — together with the bookkeeping of the polygonal interpolation.

Skorokhod's theorem needs the two exit-time facts for Brownian motion, Durrett's Theorems 7.5.3 and 7.5.5: $B_{T_{a,b}}$ takes the values $a$ and $b$ with probabilities $b/(b-a)$ and $-a/(b-a)$, and $\mathbb ET_{a,b}=-ab$. Both come from optional stopping applied to $B_t$ and $B_t^2-t$, and continuous-time optional stopping is itself not in the library. The mixture identity,

is elementary but needs Fubini and the two expressions for $c$.

Theorem 8.1.5 is the Mann–Wald theorem in the form that allows a discontinuous $\psi$: Mathlib's TendstoInDistribution.continuous_comp handles genuinely continuous maps, and the extension to maps continuous almost everywhere with respect to the limit law is the milestone. Given it, the two examples are short — the maximum is continuous outright, and the occupation-time functional is continuous at every path spending no time at the level $a$, which Fubini shows is almost every Brownian path.

Formalization scope

$C[0,1]$ is C(Set.Icc (0:ℝ) 1, ℝ), whose compact-open topology is the uniform one because the domain is compact, with the Borel $\sigma$-algebra — Mathlib has no measurable-space instance on a space of continuous maps, so the mission supplies it, and a BorelSpace instance with it.

The polygonal interpolation is written as a finite sum,

which agrees with $S_m$ at integer $m\le n$ and is linear in between, and is manifestly continuous, so walkPath is a genuine element of $C[0,1]$ with no side condition. Both properties were proved in Lean before publishing rather than assumed. Indexing is from zero, so $S_m=X_0+\dots+X_{m-1}$.

The Brownian limit is brownianPath B, the restriction of the path to $[0,1]$. Restriction is a total function: it returns the zero path for a discontinuous argument. That junk branch is never reached, because every statement assumes every path of $B$ is continuous, not merely almost every one — one may always modify a Brownian motion on a null set to achieve this, and Durrett's canonical construction on $C[0,\infty)$ has it by definition. Without it there would be no $C[0,1]$-valued random variable to speak of.

Weak convergence is Mathlib's TendstoInDistribution, the same predicate mission II used for the Lindeberg–Feller theorem, instantiated at $C[0,1]$ rather than at $\mathbb R$.

Skorokhod's theorem and the embedding of the walk are stated as existence of a probability space carrying the Brownian motion, a filtration and the stopping times. This is how Durrett states them — the construction needs an independent pair $(U,V)$ alongside the Brownian motion, and he notes himself that $T_{U,V}$ is a stopping time only for the enlarged filtration. The filtration is therefore an explicit family $F_t$ that is increasing, sits inside the ambient $\sigma$-field, and contains $\sigma(B_s:s\le t)$ — the pastSigma of mission V, which this mission imports as a reference. The stopping-time property is {T ≤ t} ∈ F_t, stated directly rather than through a bundled filtration structure.

Theorem 8.1.2's conclusion "$S_n=_d B(T_n)$" is read as equality of the laws of the whole processes: the push-forward of $\omega\mapsto(n\mapsto B(T_n\omega))$ equals the law of the partial-sum process of an i.i.d. sequence with step law $\mu$, taken on the infinite product measure. The gaps are required to be independent and identically distributed, as the book says.

The counting in Example 8.1.8 is a sum of indicators rather than a filtered cardinality, to keep a decidability side condition out of the statement, and the limit is the Lebesgue measure of $\{t\in[0,1]:B_t>a\}$ as a real number. Example 8.1.6 takes the maximum over $0\le m\le n$, which includes $S_0=0$, and the limit is the supremum of $B$ over $[0,1]$, attained because the path is continuous on a compact interval.

Existence of a Brownian motion is a hypothesis, not a claim, exactly as in mission V, except in Theorems 8.1.1 and 8.1.2 where the existence of a suitable space is the content of the statement and a Brownian motion must be produced; that is Durrett's Theorem 7.1.1, which the library does not yet have, so those two items subsume it.

Contributions welcome beyond the listed items: Lemma 8.1.9 on its own; Theorem 8.1.3, the CLT derived from the embedding; Example 8.1.7, the last zero before time $n$ and the arcsine law; continuous-time optional stopping and the exit identities 7.5.3 and 7.5.5 that Skorokhod's theorem rests on; the extension to $C[0,\infty)$; and the martingale, stationary-sequence and empirical-process versions of sections 8.2 to 8.4.

Selected references

• Rick Durrett, Probability: Theory and Examples, Version 5 (11 January 2019), chapter 8, section 8.1 (pp. 389–395); Theorems 8.1.1, 8.1.2, 8.1.4, 8.1.5, Examples 8.1.6 and 8.1.8. Published as the 5th edition, Cambridge University Press, 2019, DOI 10.1017/9781108591034
• M. D. Donsker, An invariance principle for certain probability limit theorems, Memoirs of the American Mathematical Society 6 (1951).
• A. V. Skorokhod, Studies in the Theory of Random Processes, Addison-Wesley, 1965.
• P. Erdős and M. Kac, On certain limit theorems of the theory of probability, Bulletin of the American Mathematical Society 52 (1946), 292–302. DOI 10.1090/S0002-9904-1946-08560-2
• P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999, chapters 2 and 8. DOI 10.1002/9780470316962