Probability

Martingales with partially ordered time

Optional sampling relates a process observed at two random times. A martingale has a conditional expectation at an earlier index equal to its value there, but this defining property initially concerns deterministic indices. Random indices require a separate theorem. In Chapter 2, Section 8, Ethier and Kurtz extend optional sampling to a partially ordered family of indices for use in the time changes of Chapter 6. The target is their Theorem 8.7, printed pages 87–88.

Metric lattices and information

A metric lattice is a partially ordered metric space I in which each pair of points has a greatest lower bound and a least upper bound. These are written as the meet and join. Both operations are jointly continuous. Points need not be comparable. The interval between u ≤ v consists of all points w with u ≤ w ≤ v.

A subset is separable from above if it contains a sequence aₙ that approximates each of its points w by the finite meets of those aᵢ with w ≤ aᵢ and i ≤ n. Each such meet is taken once this finite set is nonempty. The resulting sequence of meets must converge to w. The theorem assumes this condition for each interval.

Let Ω carry a probability measure P and an ambient sigma algebra. A filtration assigns a sub-sigma algebra Fᵤ to each index u, increasing with the order. A real-valued process X is a martingale if each X(u) is Fᵤ-measurable and integrable and, whenever u ≤ v,

$$E[X(v)\mid F_u]=X(u)\quad\text{almost surely}.$$

Right continuity here has a specific lattice meaning: for every u and every outcome ω, X(u ∨ v,ω) tends to X(u,ω) as v tends to u. A stopping time τ is a Borel-measurable I-valued random variable such that {τ ≤ u} belongs to Fᵤ for every u.

The optional-sampling target

Take stopping times τ₁ ≤ τ₂ pointwise. Suppose there are deterministic sequences uₙ and vₙ in I such that

$$P\{u_n\leq\tau_1\leq\tau_2\leq v_n\}\longrightarrow1,$$

and

$$E[|X(v_n)|\mathbf1_{\{\tau_2\leq v_n\}^{c}}]\longrightarrow0.$$

Assume also that X(τ₂) is integrable. The target is

$$E[X(\tau_2)\mid F_{\tau_1}]=X(\tau_1)\quad\text{almost surely}.$$

The sigma algebra Fτ consists of ambient-measurable events A for which A ∩ {τ ≤ u} belongs to Fᵤ for every u. This is the information used in the conclusion.

What the result provides

The conclusion extends the martingale identity to random lattice indices under explicit exhaustion and tail assumptions. Neither a deterministic bound on both stopping times nor a linear ordering of all indices is part of the statement. This is a known theorem in the cited book. The formal target retains the full conditional-expectation identity; its proof remains to be formalized.

Why the hypotheses matter

In a partially ordered space, the complement of {τ₂ ≤ vₙ} includes incomparable indices. Replacing this complement by {vₙ < τ₂} would change the tail assumption. Likewise, right continuity must use lattice joins, rather than a one-dimensional time convention. Controlling probabilities of the exhaustion events alone does not state the integrability control required by the second limit. Both limits belong to the theorem.

Mathematical scope and conventions

The index space has a metric and a lattice structure with continuous meet and join. No top, bottom, completeness of the metric, or linear order is required. The filtration need not be complete or right continuous. The stopping times are finite I-valued variables; their measurability is explicit. The sequences uₙ and vₙ need not be monotone. The nonnegative tail expectation uses extended nonnegative integration, avoiding a default value for a nonintegrable real integral. Indexwise integrability is retained explicitly, along with terminal integrability.

The two accompanying definitions express separation from above and the stopped sigma algebra. Together with the martingale and stopping-time conditions, they specify the single optional-sampling theorem. The target contains no additional supporting-theorem milestones.

Source

Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 2 §8, Theorem 8.7, printed pp. 87–88 (supplied PDF pp. 96–97); definitions and equation (8.6), printed p. 85 (PDF p. 94). Chapter 2.

Why two types change the limit

Critical branching is a basic scaling model for populations whose expected size neither grows nor decays at leading order. A single-type population has one macroscopic direction, but a two-type population has two coupled directions. In the critical regime considered by Ethier and Kurtz, one weighted population mode survives on the diffusive scale while a second mode is pulled rapidly toward zero. The rapid mode still leaves a random integrated contribution and an initial boundary layer, so discarding it would lose part of the limiting dynamics. The mission packages all of these conclusions from Chapter 9, Section 2, Theorem 2.1 of Ethier and Kurtz as one formal target.

The branching model

The state is a pair of natural numbers recording the numbers of particles of types 1 and 2. A type-$i$ particle lives for an exponential time with positive rate $\lambda_i$. At death it is replaced by a random pair of offspring with law $\rho_i$. The generator therefore applies the type-specific replacement rule at an intensity proportional to the current number of particles of that type. The formal predicate IsTwoTypeBranching records a measurable càdlàg process satisfying the corresponding natural-past martingale identities on finite-support tests, with an explicit integrability condition.

The offspring mean matrix has strictly positive entries. Its critical weighted rate matrix has a positive eigenvector $\nu$ with eigenvalue zero and an opposite-sign eigenvector $\mu$ with eigenvalue $-\eta$, where $\eta>0$. For the $n$th process, Lean consistently uses the positive index $n+1$. At accelerated time $(n+1)t$, the scaled modes are

$$X_n(t)=\frac{\nu_1 Z^{(n)}_1((n+1)t)+\nu_2 Z^{(n)}_2((n+1)t)}{n+1}, \qquad Y_n(t)=\frac{\mu_1 Z^{(n)}_1((n+1)t)+\mu_2 Z^{(n)}_2((n+1)t)}{n+1}.$$

The compensated fast coordinate is

$$W_n(t)=Y_n(t)+\int_0^t (n+1)\eta Y_n(s)\,ds.$$

Formalization target

The goal is the complete three-part statement of Theorem 2.1. First, $(X_n,W_n)$ converges jointly in path law to a continuous two-dimensional diffusion $(X,W)$. Its covariance matrix is built from the raw second moments of the two offspring replacement increments, and its generator has the form

$$Af(x,w)=\frac{x}{2}\left(a_{11}f_{xx}+2a_{12}f_{xw}+a_{22}f_{ww}\right)(x,w).$$

Second, on every finite time interval the fast mode is uniformly close in probability to its exponentially decaying initial layer $Y_n(0)e^{-(n+1)\eta t}$. On every interval $0<t_1<t_2$, its integrated drift converges weakly to $W(t_2)-W(t_1)$. Third, the first population coordinate is uniformly reconstructed from $X_n$ together with that same initial layer. The limit statement keeps the possibly nonzero initial fast coordinate and the separate nonnegativity conclusion for the slow coordinate.

What the result supplies

The theorem identifies both the persistent and collapsing directions of a critical multitype system. The slow direction produces population-scale diffusion, while the compensated fast direction records fluctuations that remain visible after the raw fast mode contracts. The reconstruction formula connects these mode coordinates back to the original particle count. Keeping the path limit, fast decay, integrated limit, and reconstruction together prevents an apparently simpler marginal statement from omitting the initial-layer behavior needed at time zero.

The textbook theorem is already mathematically proved. This mission asks for a Lean proof of the reviewed formal statement; the uploaded goal is intentionally a statement with a proof placeholder, not a claim of machine-checked completion. The concrete generator, branching-law predicate, scaling map, càdlàg condition, and diffusion martingale-problem predicate provide reusable vocabulary for related multitype limit theorems.

Where the formal difficulty lies

Coordinatewise convergence is insufficient. The result couples full path laws, a continuous diffusion martingale problem, compact-uniform control of an initial layer, and a positive-time integral of a rapidly changing mode. The naive step of simply setting the fast mode to zero fails at time zero and erases the exponential term needed in the population reconstruction. The covariance coefficients also come from replacement increments rather than centered offspring counts, so changing that convention alters the limiting operator.

Formalization scope and conventions

The state space is exactly $\mathbb N\times\mathbb N$; both offspring laws are probability measures, both coordinates have finite third moments under each parent law, and all four entries of the mean matrix are positive. Initial populations are deterministic floors of $(n+1)z_i$ for nonnegative densities $z_i$. The positive indexing avoids division by zero in every scaling, clock, and exponential. Natural-number subtraction in the generator is used only with a zero event intensity when the relevant population is empty.

Path convergence is represented by a joint probability-space realization carrying the correct complete prelimit path laws and almost-sure uniform convergence on compact intervals to a continuous limit. This is the continuous-limit Skorohod convention used in the reviewed development. The definitions are concrete: none contains the target theorem or assumes its conclusions. The mission includes only expression-essential dependencies, reusing exact private book-wide definitions for càdlàg paths and the continuous diffusion generator law. It does not add proof-only lemmas or split the three source conclusions into separate missions.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 9, Section 2, Theorem 2.1, printed pp. 392–393. DOI

Why infinite spin systems need a generation theorem

A spin-flip system models a countable collection of two-state components whose transition rates may depend on the entire current configuration. Such systems are basic examples of interacting particle processes: each local move is simple, but infinitely many possible moves may be active and their rates interact through the configuration. The central analytic question is whether the formal sum of local flip operators determines a genuine time evolution on continuous observables. Chapter 8, Section 3 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, answers this question under uniform rate and influence bounds Ethier--Kurtz, Theorem 3.5.

This mission states that result without replacing the countable system by a finite-state chain or assuming finite total jump intensity. It also retains the theorem's cylinder-function core, which identifies finitely coordinate-dependent observables as a sufficient starting class for recovering the closed generator.

Configuration space and coordinate variation

Let S be a countable type of sites. A configuration is a function η : S → Bool; false and true relabel the source spins -1 and 1. The product topology on these configurations is the one induced by the discrete topology on each coordinate. The Lean space C(S → Bool, ℝ) consists of real-valued continuous observables on this compact product space and carries its uniform norm.

For a site i, spinFlip i η agrees with η away from i and negates the Boolean value at i. For an observable f, its coordinate variation at i is

$$\operatorname{var}_i(f)=\sup_{\eta}\left|f(\operatorname{flip}_i\eta)-f(\eta)\right|.$$

The domain used in the theorem is the full class of continuous observables for which ∑ i, var_i(f) is summable. This is a one-coordinate variation domain: it measures the effect of changing one spin, rather than exchanging two occupied sites.

For every site i, the flip rate c i is itself a continuous function of the configuration. Rates are nonnegative and uniformly bounded in the uniform norm. Their dependence on other coordinates is controlled by a second uniform bound: for each i, the series ∑ j, var_j(c i) is summable, with a bound independent of i. These are the two clauses of equation (3.24).

Formalization target

The pre-generator graph implements equation (3.25). For every pair (f,g) in that graph, f has summable coordinate variation and

$$g(\eta)=\sum_i c_i(\eta)\bigl(f(\operatorname{flip}_i\eta)-f(\eta)\bigr).$$

The goal is Theorem 3.5 in full. It asserts that every function in the prescribed domain has a continuous image in the graph; the closure of the graph in the product uniform-norm topology is single-valued; and that closure is exactly the generator graph of a strongly continuous contraction semigroup. The semigroup is positive and preserves the constant function one, giving the conservative Feller conclusion used by the source.

The final clause retains the source's cylinder core. Restrict the initial graph to functions depending on a finite set of coordinates, expressed by the existence of a finite set F such that agreement on F forces equal function values. The closure of this restricted graph equals the full generator graph. Generation and the core are kept together because both are conclusions of the same theorem.

Significance of the result

The result turns an infinite formal sum of local moves into a closed, single-valued Markov generator. This is stronger than merely defining the pointwise series: it supplies the strongly continuous positive contraction evolution, conservativity, and the derivative characterization of the entire generator domain. The cylinder-core clause means that finite-coordinate observables are graph-norm dense enough to recover that generator, even though the state space and the total collection of possible flips are countable.

The theorem is already proved in the source. The formalization target is its precise Lean statement, including the infinite-site domain, the uniform influence hypothesis, generator closure, and core. The reusable infrastructure consists of the book-wide strongly continuous contraction-semigroup predicate and the mission-local flip, variation, and graph definitions.

Where the analytic difficulty lies

The naive finite-rate jump argument does not apply. A uniform bound on each individual rate does not bound the sum of rates over a countably infinite site set, so the system may have infinite total potential flip intensity. Pointwise notation for the generator also does not by itself show that its image is continuous or that its graph closure is single-valued. The coordinate-influence bound and summable-variation domain are therefore essential parts of the target rather than optional regularity decoration.

The neighboring exclusion-process theorem is not interchangeable with this one. A spin flip changes one coordinate and permits creation or destruction of occupation, whereas exclusion dynamics exchanges two coordinates and conserves particle number. Their domains and rate conditions are correspondingly different.

Formalization scope

The Lean statement allows empty, finite, and countably infinite S; it does not impose nonemptiness or finiteness. Bool is an exact two-state relabeling, not a restriction to a special numerical spin convention. spinVariation uses a real supremum over the nonempty compact configuration space. Explicit Summable hypotheses prevent divergent real tsum expressions from receiving an unintended default interpretation.

The operator graph uses the actual pointwise series and requires a continuous output. Closure is taken in C(S → Bool, ℝ) × C(S → Bool, ℝ). The semigroup is indexed by real time, but every law and bound uses nonnegative times; negative-time values carry no mathematical requirement. No finite-total-rate hypothesis, finite-site approximation, two-site exchange dynamics, or weakened core statement is admitted.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 1, Section 3; Chapter 4; Chapter 8, Section 3, Theorem 3.5, equations (3.24)--(3.25), printed p. 381. Wiley DOI

Why nonlocal generators matter

Markov processes with jumps model changes that cannot be represented by continuous diffusion paths: arrivals in queueing systems, sudden failures, population events, and discontinuous changes in financial or physical systems. Their infinitesimal descriptions are nonlocal generators, because the value of the operator at a state depends on test-function values at displaced states rather than only on derivatives at the current point. Chapter 8, Section 3 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), treats three complementary regimes. Theorem 3.1 covers finite-rate jumps on a general locally compact state space. Theorem 3.4 treats homogeneous Lévy operators on Euclidean space, including infinite jump activity and degenerate covariance. Theorem 3.3 gives the main target here: well-posedness for a time- and state-dependent compensated Lévy-type martingale problem.

These results connect concrete jump kernels and integro-differential operators to two standard descriptions of stochastic dynamics. Autonomous operators are realized as generators of conservative Feller semigroups, while time-dependent operators are characterized through martingale identities. Keeping all three source results in one mission records the nonlocal-generator theme without claiming that their distinct hypotheses imply one another.

The setting

For the Euclidean results, the state space is $\mathbb R^d$, represented in Lean as EuclideanSpace ℝ (Fin d), with $d>0$. A covariance field $a(t,x)$ is a continuous linear endomorphism, a drift field $b(t,x)$ is a vector, and $\nu(t,x,dy)$ is a measure of jump displacements. For a smooth compactly supported test function $f$, the compensated Lévy-type operator is

$$L_t f(x)=\frac12\sum_{i,j}a_{ij}(t,x)\,\partial_{ij}f(x) +Df(x)[b(t,x)] +\int\!\left(f(x+y)-f(x)-\frac{Df(x)[y]}{1+\lVert y\rVert^2}\right)\nu(t,x,dy).$$

The denominator in the compensation term is part of the source convention. The covariance factor $1/2$ applies only to the second-order term; the drift is unscaled. The weighted moment $\lVert y\rVert^2/(1+\lVert y\rVert^2)$ permits measures with infinite total mass while controlling the compensated integral.

A solution of the Lévy-type martingale problem is a jointly measurable process with the prescribed initial pushforward law whose integrated-generator increments have zero expectation against every bounded continuous function of any finite history. Smooth compactly supported functions are the spatial tests. This definition imposes no path-continuity requirement.

The finite-rate model uses a locally compact, noncompact, separable metric space $E$, a nonnegative rate $\lambda(x)$, and a weakly continuous probability transition kernel $\mu(x,dy)$. Its operator is $Af(x)=\lambda(x)\int(f(y)-f(x))\mu(x,dy)$. Positive weights $\gamma$ and $\eta$ specify the graph domain and control behavior at infinity.

Formalization targets

Goal: nonautonomous Lévy-type well-posedness

The main target is Chapter 8, Section 3, Theorem 3.3. The covariance is continuous, symmetric, bounded, and strictly positive definite at every nonzero vector, without a uniform ellipticity constant. The drift is measurable and bounded. The weighted jump measure is integrable, and for every measurable set its weighted mass is a bounded continuous function of time and state.

For every initial probability measure, the conclusion asserts existence of a measurable-process solution on some probability space and uniqueness of all finite-dimensional distributions among every solution on every probability space. Setwise continuity is retained exactly; it is not replaced by weak convergence of measures or by finite total jump intensity.

Related target: homogeneous Lévy generation

Theorem 3.4 freezes the coefficients in time and space. The covariance may be degenerate but is symmetric and nonnegative, and the jump measure needs only the finite weighted integral. The full $\widehat C^2$ graph consists of functions, first derivatives, and second derivatives that vanish at infinity. Its closure is the exact generator of a positive conservative strongly continuous contraction semigroup on $C_0(\mathbb R^d)$, and smooth compactly supported functions form a core.

Related target: finite-rate jump generation

Theorem 3.1 retains the general-state-space jump model. The transition kernel is both setwise measurable and weakly continuous; the rate and weights satisfy the source's vanishing and signed integral bounds. The weighted graph closes to a single-valued conservative Feller generator, and compactly supported continuous functions form a core.

Significance

The main theorem says that the displayed nonlocal characteristics determine stochastic dynamics in distribution even when the drift is only measurable and jump activity need not be finite. The two autonomous theorems identify concrete domains whose closures are genuine Feller generators, including positivity, contraction, strong continuity, conservativity, and core statements. Together they distinguish finite-rate kernels, homogeneous compensated Lévy dynamics, and nonautonomous Lévy-type dynamics while sharing the same generator language.

The formal contribution is a machine-checkable statement layer, not a proof claim. It exposes the exact compensation, weighted-integrability, graph-domain, semigroup, and finite-history conventions on which later proofs depend. The common diffusion operator, bounded-pointwise closure, and strongly continuous contraction-semigroup predicate are reused from earlier private missions in the same textbook series rather than duplicated under conflicting identifiers.

Where the difficulty lies

The obvious finite-jump approximation does not by itself preserve the full conclusions. Infinite jump activity requires compensation near zero, and convergence of the associated operators must still identify the intended martingale problem or the exact closed Feller generator. In the nonautonomous theorem, setwise continuity of weighted jump masses must coexist with merely measurable drift, while uniqueness ranges over arbitrary probability-space realizations and all finite-dimensional laws. Strengthening to continuous drift, imposing finite total jump intensity, assuming uniform ellipticity, or comparing only continuous-path solutions would materially weaken or alter the source theorem.

Formalization scope and conventions

Nonnegative real time is represented by ℝ≥0; Euclidean coordinates use Fin d. Fréchet derivatives express both gradient and Hessian terms. The jump measure is a measure of displacements $y$, so the operator evaluates $f(x+y)$. Integrable hypotheses prevent Lean's totalized integral from silently assigning zero to a divergent positive weighted moment. Positive dimension is explicit through [NeZero d].

The martingale predicate includes empty finite histories and repeated observation times. Its bounded continuous history tests determine the same finite-dimensional identities used by the source, and no sample-path regularity is inserted. The autonomous graphs live in $C_0\times C_0$; bounded-pointwise closure means closure under uniformly bounded pointwise sequential limits, not ordinary norm closure. The finite-rate theorem preserves its restriction of the additional integrability clause to states with positive rate. No vacuous solution predicate, unweighted moment assumption, hidden nonzero-rate condition, or proof-only theorem dependency is introduced.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 8, Section 3, Theorems 3.1, 3.3, and 3.4. Wiley DOI
• Stewart N. Ethier and Thomas G. Kurtz, same volume, Chapter 4, Sections 2–3 for Feller and martingale-problem conventions, and Appendix 3 for bounded-pointwise closure. Wiley DOI

Why simplex diffusions matter

Finite-dimensional simplices are the natural state spaces for proportions: allele frequencies, population shares, and other collections of nonnegative coordinates whose total cannot exceed one. A diffusion on such a space must do more than solve an unconstrained stochastic equation. Its covariance degenerates on the boundary, and its drift must respect every face so that the process remains in the simplex. Chapter 8 of Ethier and Kurtz develops generator results for this setting as part of the analytic foundation for Markov-process models with constrained state spaces Ethier and Kurtz, Chapter 8, §2.

This mission formalizes their Theorem 2.8, a known generation theorem rather than an open conjecture. The theorem treats arbitrary Lipschitz drift satisfying the inward boundary inequalities. It identifies the closed diffusion graph as a Feller generator and also states that polynomial restrictions form a core. The generality of the drift distinguishes this result from later population-model applications with particular mutation or selection coefficients.

The simplex and its boundary

For a positive integer $d$, the simplex state space is

$$K_d=\left\{x\in\mathbb R^d: x_i\ge 0\ \text{for every }i, \quad \sum_{i=1}^d x_i\le 1\right\}.$$

The missing mass $1-\sum_i x_i$ may be viewed as an additional coordinate. In Lean, WFState d is the subtype of functions Fin d → ℝ satisfying precisely nonnegativity and the upper bound on the coordinate sum. These conditions already imply $x_i\le 1$ for every coordinate.

Let $b:K_d\to\mathbb R^d$ be the drift. The boundary conditions say that $b_i(x)\ge 0$ whenever $x_i=0$, while $\sum_i b_i(x)\le 0$ whenever $\sum_i x_i=1$. Thus the drift cannot point outward through a coordinate face or through the top face. No mutation–selection formula or extra smoothness condition is imposed: global Lipschitz continuity and these face inequalities are the complete drift hypotheses retained here.

The operator and target theorem

The covariance matrix is

$$a_{ij}(x)=x_i(\delta_{ij}-x_j),$$

and the associated simplex diffusion operator is

$$Gf(x)=\frac12\sum_{i,j}x_i(\delta_{ij}-x_j) \,\partial_i\partial_j f(x)+\sum_i b_i(x)\,\partial_i f(x).$$

Only the second-order sum is multiplied by $1/2$. The covariance becomes singular on boundary faces, so this is not an immediate instance of a uniformly elliptic whole-space theorem.

The formal target asserts that the uniform graph closure of

$$\{(f,Gf):f\in C^2(K_d)\}$$

is single-valued and is exactly the generator graph of a positive, conservative, strongly continuous contraction semigroup on $C(K_d)$. Conservativity is expressed by preservation of the constant function $1$. The generator is identified by the right derivative at time zero, not merely by containment of a convenient operator restriction.

The final clause says that polynomials restricted to $K_d$ are a core: closing the graph obtained from polynomial first coordinates gives the same full generator graph. This is a graph-closure statement and is stronger than uniform density of polynomials as functions.

What the result provides

Single-valuedness shows that the closed graph behaves as an operator rather than a multivalued relation. Generation supplies a Feller semigroup whose positivity and preservation of constants give the Markov interpretation. The exact generator biconditional fixes the full infinitesimal domain, while the polynomial-core conclusion permits generator questions to be reduced to algebraically structured test functions without changing the closed operator.

The source theorem is already proved in the book. The formalization task is to recover its generator statement and core conclusion in Lean with all boundary, closure, and semigroup conventions explicit. The current mission contributes a source-reviewed statement and its expression-level definitions; it does not claim a completed Lean proof.

Why the formalization is delicate

The obvious route through standard elliptic diffusion generation does not apply because $a(x)$ degenerates as coordinates approach the boundary. It is also insufficient to prove only that the displayed differential operator is contained in some generator: the theorem identifies the closure of the entire $C^2(K_d)$ graph and separately asserts the polynomial core.

Boundary semantics create another source of possible weakening. Dropping either inward condition would permit outward drift at a face. Replacing the arbitrary Lipschitz drift by a special population-genetics formula would narrow the theorem. Replacing graph equality by inclusion, or polynomial graph density by ordinary function density, would lose a stated conclusion. These distinctions are all preserved in the target.

Formalization scope

The Lean development uses the book-wide namespace EthierKurtz. The compact space $C(K_d)$ is represented by real-valued bounded continuous functions on WFState d; compactness makes this the intended continuous-function space with the uniform norm. A $C^2(K_d)$ function is represented through a globally twice continuously differentiable extension on the ambient finite-coordinate space, following the book’s Appendix 6 extension convention for closed convex sets.

The operator uses Fréchet derivatives evaluated on coordinate vectors, which represent the first and second partial derivatives in the finite-dimensional ambient space. The graph is closed in the product uniform norm. IsStronglyContinuousContractionSemigroup records identity at zero, the nonnegative-time semigroup law, contraction, and strong right continuity at zero. The target additionally records positivity, preservation of one, and equality between its derivative graph and the closed diffusion graph.

The scope excludes the zero-dimensional case, as required by 0 < d. It does not introduce a continuous-path hypothesis, a special drift parameterization, or uniform ellipticity. The only packaged declarations beyond the goal are the state space, operator, graph, and the already published semigroup predicate needed to state it. Proof-only lemmas and unrelated Chapter 8 results are outside this mission.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 8, §2, Theorem 2.8, printed p. 375; equation (1.15), printed p. 368; Appendix 6, printed pp. 499–500. DOI

Why endpoint classification matters

A one-dimensional diffusion is governed in the interior by a second-order differential operator, but the interior coefficients alone do not determine what happens when the process approaches the edge of its state space. An endpoint may be reachable from the interior or inaccessible; after arrival it may absorb, reflect, or retain the process according to a boundary parameter. The same issue persists when an endpoint is infinite. Chapter 8 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), organizes these alternatives through scale and speed integrals and identifies the exact operator domain that generates the corresponding Feller evolution. This mission formalizes Chapter 8, Section 1, Theorem 1.1, printed page 367.

The setting

Let $-\infty\le r_0<r_1\le\infty$. The real state interval is $I=[r_0,r_1]\cap\mathbb R$, its interior is $I^\circ=(r_0,r_1)$, and $\bar I$ is the closed interval in the extended real line. A function in $C(\bar I)$ is represented by a continuous function on that compact extended interval, so finite endpoint limits are part of the object even when an endpoint is infinite.

The interior diffusion operator is

$$Gf(x)=\frac{a(x)}2 f''(x)+b(x)f'(x),$$

where $a$ and $b$ are continuous on $I^\circ$ and $a(x)>0$ there. Choose an interior reference point $r$. Define

$$B(x)=\int_r^x \frac{2b(y)}{a(y)}\,dy, \qquad p(x)=\int_r^x e^{-B(y)}\,dy, \qquad m(x)=\int_r^x \frac{2e^{B(y)}}{a(y)}\,dy.$$

The corresponding endpoint tests $u$ and $v$ are nonnegative extended-real integrals. Their values may be $+\infty$; preserving that possibility is essential because the four boundary classes are distinguished precisely by which of the two tests are finite.

Formalization target

Theorem 1.1 — one-dimensional boundary diffusion generation

At either endpoint, the pair $(u,v)$ gives the Feller boundary class:

$$\begin{array}{c|cc} \text{class} & u & v\\ \hline \text{regular} & <\infty & <\infty\\ \text{exit} & <\infty & =\infty\\ \text{entrance} & =\infty & <\infty\\ \text{natural} & =\infty & =\infty. \end{array}$$

Entrance and natural endpoints are inaccessible, so the generator domain imposes no boundary equation there. At an exit endpoint the limiting generator value must be zero. At a regular endpoint $r_i$, a parameter $q_i\in[0,1]$ determines the boundary condition

$$q_i\lim_{x\to r_i}Gf(x) =(-1)^i(1-q_i)\lim_{x\to r_i}e^{B(x)}f'(x).$$

The target states that the graph consisting of $f\in C(\bar I)$ that are twice continuously differentiable in the interior, whose $Gf$ extends continuously to $\bar I$, and that satisfy the applicable condition at both endpoints is exactly the infinitesimal generator of a Feller semigroup on $C(\bar I)$. The conclusion includes the semigroup law, contraction, strong right continuity at zero, positivity, preservation of the constant function $1$, and a biconditional identifying the complete generator graph rather than merely an included core or its closure.

Significance

The theorem translates local coefficients into a global Markov evolution while retaining every possible finite or infinite endpoint type. The endpoint tests determine which boundary behavior is available, and the regular-boundary parameter records absorbing, reflecting, and intermediate behavior in one equation. Without the classification, writing down the differential expression does not specify a unique Feller generator because distinct domains can encode different stochastic behavior at the same endpoint.

The formal contribution is a machine-checkable statement layer for the source theorem. It makes the compactified state space, improper endpoint integrals, one-sided endpoint filters, and exact generator graph explicit. The theorem itself remains an open proof obligation in this statement-only mission. The definitions can also support later formal work on hitting distributions, killed or reflected diffusions, and comparison of boundary regimes.

Where the difficulty lies

The main difficulty is that the classification cannot be reduced to ordinary finite integrals or to boundary values at finite real points. Infinite endpoints and divergent scale or speed tests carry mathematical information; replacing extended-real integrals by totalized real integrals would collapse boundary classes. A second difficulty is identifying the full closed generator domain. Showing that the differential expression is meaningful on smooth interior functions is insufficient: the proof must connect its endpoint asymptotics to positivity, conservativity, strong continuity, and exact generation on the uniform-norm space.

Formalization scope and conventions

Endpoints use EReal, and the state space is Set.Icc r₀ r₁ in the extended line. Coefficients are constrained only on the open real interior; no boundedness or uniform ellipticity is added. The drift primitive and scale/speed tests use oriented interval integrals internally and ENNReal endpoint integrals externally, retaining $+\infty$. Absolute values correct the orientation on the left of the reference point.

The graph stores continuous endpoint extensions of both $f$ and $Gf$. Interior $C^2$ regularity is expressed by ContDiffOn ℝ 2, and endpoint limits use the one-sided neighborhood filter induced from the extended interval. The regular parameter is required to lie in $[0,1]$ only when both boundary tests are finite. The mission does not replace the four cases by an opaque classifier, assume finite endpoints, add a pathwise stochastic differential equation, or weaken exact generation to graph inclusion. The shared book definition of a strongly continuous contraction semigroup is reused from the earlier semigroup-generation mission rather than redeclared.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 8, Section 1, Theorem 1.1 and equations (1.1)–(1.11), printed pp. 366–367. Wiley DOI
• Stewart N. Ethier and Thomas G. Kurtz, same volume, Chapter 4, printed p. 166, for the Feller semigroup convention used in the conclusion. Wiley DOI

Why whole-space diffusion generators matter

Diffusion processes connect stochastic differential equations, partial differential equations, and Markov semigroups. On Euclidean space, their local behavior is encoded by a second-order operator built from a covariance field and a drift field. A central question is whether those local coefficients determine an actual Markov evolution, and whether the resulting evolution is unique. Ethier and Kurtz organize these questions through generator graphs and martingale problems, which allow the same language to cover smooth elliptic diffusions, degenerate models, and coefficients that vary measurably with time. This mission formalizes three complementary whole-space regimes from Chapter 8 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), principally Theorems 1.6, 1.7, and 2.5.

The setting

The state space is the finite-dimensional Euclidean space $\mathbb R^d$, represented in Lean as EuclideanSpace ℝ (Fin d), with $d>0$. A covariance operator $a(t,x)$ is a continuous linear endomorphism of this space, while a drift $b(t,x)$ is a vector. For a smooth scalar test function $f$, the diffusion operator is

$$G_t f(x)=\frac12\sum_{i,j} a_{ij}(t,x)\,\partial_{ij}f(x) + Df(x)[b(t,x)].$$

The factor $1/2$ multiplies only the covariance-weighted second-order term. The formalization uses Fréchet derivatives evaluated in the standard coordinate directions. In the time-homogeneous cases, the smooth compactly supported graph consists of pairs $(f,Gf)$ viewed in $C_0(\mathbb R^d)\times C_0(\mathbb R^d)$, and its uniform closure is the candidate generator.

For time-dependent coefficients, a measurable process solves the time-inhomogeneous martingale problem when its initial pushforward law is prescribed and the integrated generator identity holds against every smooth compactly supported spatial test and every bounded continuous finite-history test. This formulation records the natural-past moment identities without imposing continuity of sample paths as an extra hypothesis.

Formalization targets

Goal: measurable-drift nonautonomous well-posedness

The main target is Chapter 8, Section 1, Theorem 1.7. The covariance and drift are jointly Borel measurable and locally bounded. The covariance is symmetric and nonnegative. At each fixed spatial point it is uniformly elliptic over every bounded positive time interval, and its spatial continuity is uniform over that interval. A common quadratic bound controls the covariance norm and the one-sided radial drift quantity $\langle x,b(t,x)\rangle$.

For every initial probability measure, the conclusion asserts existence of a measurable-process solution on some probability space and uniqueness of all finite-dimensional distributions among every such solution on any probability space. The drift is not assumed continuous, and no stronger norm-growth condition on the drift or moment condition on the initial law is inserted.

Related target: uniformly elliptic Feller generation

Chapter 8, Section 1, Theorem 1.6 treats bounded Hölder continuous time-homogeneous coefficients with symmetric, globally uniformly elliptic covariance. It concludes that the closure of the smooth compactly supported graph is single-valued and is exactly the generator of a positive, strongly continuous contraction semigroup on $C_0(\mathbb R^d)$. Conservativity is retained through membership of the constant graph pair $(1,0)$ in the bounded-pointwise closure.

Related target: degenerate smooth-core generation

Chapter 8, Section 2, Theorem 2.5 permits degenerate and unbounded covariance fields. Its assumptions are symmetry, nonnegativity, twice continuous differentiability of the matrix entries, bounded second partial derivatives, and a globally Lipschitz drift. Its conclusion is the same full Feller generation and conservativity statement. This regime is related to, but not implied by, the bounded uniformly elliptic regime.

Significance

Together the three statements separate distinct mechanisms for obtaining Markov dynamics from local diffusion data. The two autonomous theorems identify when a concrete smooth core closes to a Feller generator, including positivity, contraction, strong continuity, and conservativity. The nonautonomous theorem establishes existence and uniqueness in distribution under substantially rougher temporal behavior and merely measurable drift. Keeping the regimes together exposes the common operator while preserving their incompatible regularity hypotheses.

The formal contribution is a machine-checkable statement layer for these source results and their expression-essential definitions. It does not claim proofs of the theorems. The definitions make explicit the coordinate form of the generator, the $C_0$ graph, the bounded-pointwise closure convention, and the complete finite-history martingale identities. These components can support later formal proofs and other diffusion or martingale-problem developments.

Where the difficulty lies

The source conclusions are not consequences of a single elementary continuity argument. In the Feller cases, identifying the closure of a graph with the generator requires simultaneous control of the operator domain, the semigroup properties, positivity, and conservativity. In the time-dependent case, measurability of the drift is deliberately weaker than continuity, while uniqueness must cover all measurable-process realizations and all finite collections of observation times. Replacing that conclusion by uniqueness only among continuous processes, or strengthening the drift hypotheses until a standard smooth theory applies, would change the theorem.

Formalization scope and conventions

The development uses nonnegative real time and finite-dimensional real Euclidean space. Covariance matrices act as continuous linear maps; their entries are recovered in the standard orthonormal basis. Smoothness is expressed with ContDiff, compact support with HasCompactSupport, and autonomous generator graphs in C₀. The bounded-pointwise closure is the smallest set closed under uniformly bounded pointwise sequential limits, not merely the set of one-step limits.

The martingale-problem predicate requires joint measurability of the process, equality of the initial pushforward measure, and all bounded continuous finite-history identities. Empty histories and repeated observation times are included. The goal compares the complete finite-dimensional laws of any two solutions. No vacuous solution predicate, arbitrary extension of the generator, chosen matrix square root, hidden path-continuity assumption, or proof-only theorem dependency is used.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 8, Theorems 1.6, 1.7, and 2.5. Wiley DOI
• Stewart N. Ethier and Thomas G. Kurtz, same volume, Chapter 4 for martingale-problem well-posedness and Feller conventions, and Appendix 3 for bounded-pointwise closure. Wiley DOI

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

$$\left\|P(A\mid\text{past})-P(A)\right\|_p.$$

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

$$X_n(t)=\frac{1}{\sqrt n}\sum_{k=1}^{\lfloor nt\rfloor}Y_k, \qquad t\ge 0.$$

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

$$p=\frac{2+\delta}{1+\delta}, \qquad \sum_{m=0}^{\infty}\varphi_p(m)^{\delta/(1+\delta)}<\infty.$$

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

$$\sigma^2=E[Y_1^2]+2\sum_{k=2}^{\infty}E[Y_1Y_k]$$

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

$$M_n^i M_n^j-A_n^{ij}$$

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

$$Gf(x)=\frac12\sum_{i,j}a_{ij}(x)\,\partial_i\partial_jf(x) +\sum_i b_i(x)\,\partial_i f(x).$$

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

$$\int_0^t b_i(X_n(s))\,ds \quad\text{and}\quad \int_0^t a_{ij}(X_n(s))\,ds,$$

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

$$\sigma:[0,\infty)\times\mathbb R^d\longrightarrow\mathbb R^{d\times d}$$

controls the random fluctuations, and a drift coefficient

$$b:[0,\infty)\times\mathbb R^d\longrightarrow\mathbb R^d$$

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

$$X(t)=X(0)+\int_0^t \sigma(s,X(s))\,dW(s)+\int_0^t b(s,X(s))\,ds.$$

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

$$Gf(t,x)=\frac12\sum_{i,j}(\sigma\sigma^{\mathsf T})_{ij}(t,x)\,\partial_i\partial_j f(x)+\sum_i b_i(t,x)\,\partial_i f(x).$$

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

$$\lVert\sigma(t,x)\rVert^2\le K(1+\lVert x\rVert^2),\qquad x\cdot b(t,x)\le K(1+\lVert x\rVert^2),$$

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

$$\begin{aligned} f(t,X(t))-f(0,X(0))={}&\int_0^t f_t(s,X(s))\,ds\\ &+\sum_i\int_0^t f_{x_i}(s,X(s))\,dV_i(s)\\ &+\sum_i\int_0^t f_{x_i}(s,X(s))\,dM_i(s)\\ &+\frac12\sum_{i,j}\int_0^t f_{x_i x_j}(s,X(s))\,d\langle M_i,M_j\rangle_s. \end{aligned}$$

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

$$r\lVert x\rVert\leq\lVert rx-Ax\rVert \quad(x\in D(A),\ r>0).$$

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

$$A\text{ generates a strongly continuous contraction semigroup} \quad\Longleftrightarrow\quad \overline{D(A)}=E,\quad A\text{ is dissipative},\quad \operatorname{Ran}(rI-A)=E\text{ for some }r>0.$$

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

$$\lVert Bx\rVert\leq\alpha\lVert Ax\rVert+\beta\lVert x\rVert \quad(x\in D(A)),\qquad 0\leq\alpha<1,\quad\beta\geq0.$$

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

$$\inf_{\psi \in \Psi} \sup_{Q \in B_{\varepsilon,2}(\hat P_N)} E_Q\big[\|x-\psi(y)\|_2^2\big]. \tag{35}$$

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

$$\max_S f(S) = \mathrm{Tr}[S_{xx} - S_{xy}S_{yy}^{-1}S_{yx}] \quad \text{s.t.} \quad S = \begin{pmatrix}S_{xx}&S_{xy}\\S_{yx}&S_{yy}\end{pmatrix} \succeq 0,\; S_{xx} \succeq 0,\; S_{yy} \succeq 0,\; \mathrm{Tr}[S+\hat\Sigma-2(\hat\Sigma^{1/2}S\hat\Sigma^{1/2})^{1/2}] \le \varepsilon^2,\; S \succeq \lambda_{\min}(\hat\Sigma) I \tag{36}$$

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

$$\psi^\star(y) = S^\star_{xy}(S^\star_{yy})^{-1}(y-\hat\mu_y) + \hat\mu_x$$

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

Distributionally robust optimization (DRO) hedges a decision against every distribution within some ambiguity set around an estimated (nominal) distribution, rather than trusting the estimate exactly. When the ambiguity set is a ball of radius $\varepsilon$ around the empirical distribution $\hat P_N$ in the type-$p$ Wasserstein metric, the resulting worst-case risk problem inherits attractive statistical guarantees (Mohajerin Esfahani & Kuhn 2018) but is, in general, an optimization problem over an infinite-dimensional space of measures. Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter surveys when this problem becomes computationally tractable. One route — the subject of this mission — discards everything about the nominal distribution except its mean vector and covariance matrix and replaces the Wasserstein ball with a set built only from these two moments, the Gelbrich hull. The construction is due to Gelbrich (1990), who first bounded the Wasserstein distance between two distributions using only their means and covariances.

Setting

Fix $\Xi \subseteq \mathbb{R}^m$, a nominal distribution $\hat P_N \in \mathcal{P}(\Xi)$, a radius $\varepsilon > 0$ and an exponent $p \ge 1$. The type-$p$ Wasserstein distance between two probability measures $Q, Q'$ on $\mathbb{R}^m$ is

$$W_p(Q,Q') = \Big(\inf_{\pi \in \Pi(Q,Q')} \int \|\xi-\xi'\|^p \, d\pi(\xi,\xi')\Big)^{1/p},$$

the infimum over couplings $\pi$ (probability measures on $\mathbb{R}^m \times \mathbb{R}^m$ with marginals $Q$ and $Q'$) of the $p$-th root of the expected $p$-th power of Euclidean distance. The Wasserstein ambiguity set is $B_{\varepsilon,p}(\hat P_N) = \{Q \in \mathcal{P}(\Xi) : W_p(Q,\hat P_N) \le \varepsilon\}$, and the worst-case risk of a loss function $\ell$ is $R_{\varepsilon,p}(\hat P_N,\ell) = \sup_{Q \in B_{\varepsilon,p}(\hat P_N)} E_Q[\ell(\xi)]$.

Suppose $\hat P_N$ has mean vector $\hat\mu$ and covariance matrix $\hat\Sigma \in S^m_+$ (the positive semidefinite $m\times m$ matrices). The mean-covariance uncertainty set is

$$U_\varepsilon(\hat\mu,\hat\Sigma) = \Big\{(\mu,\Sigma) \in \mathbb{R}^m \times S^m_+ : \|\hat\mu-\mu\|_2^2 + \mathrm{Tr}\big[\hat\Sigma+\Sigma-2(\hat\Sigma^{1/2}\Sigma\hat\Sigma^{1/2})^{1/2}\big] \le \varepsilon^2\Big\},$$

where $\Sigma^{1/2}$ is the positive-semidefinite square root. The Gelbrich hull is $G_\varepsilon(\hat\mu,\hat\Sigma) = \{Q \in \mathcal{P}(\Xi) : (E_Q[\xi],\mathrm{Cov}_Q[\xi]) \in U_\varepsilon(\hat\mu,\hat\Sigma)\}$: the distributions on $\Xi$ whose own mean and covariance lie in $U_\varepsilon(\hat\mu,\hat\Sigma)$. An elliptical distribution $E_g(\mu,\Sigma)$ has density $f(\xi) = C \cdot \det(\Sigma)^{-1} g\big((\xi-\mu)^\top\Sigma^{-1}(\xi-\mu)\big)$ for a density generator $g$ and normalizing constant $C$; two elliptical distributions "have the same density generator" when their $g$ coincide (e.g. both Gaussian, both Student-$t_\nu$ for the same $\nu$).

Formalization targets

Goal (Theorem 13, Gelbrich hull). For every $p \ge 2$,

$$B_{\varepsilon,p}(\hat P_N) \subseteq G_\varepsilon(\hat\mu,\hat\Sigma).$$

This is an outer approximation: every distribution within $\varepsilon$ of $\hat P_N$ in Wasserstein distance has a mean and covariance inside $U_\varepsilon(\hat\mu,\hat\Sigma)$, so optimizing over the Gelbrich hull instead of the Wasserstein ball can only enlarge the feasible set, never shrink it below the truth.

Supporting results. Theorem 4 (Gelbrich bound) gives the moment-only lower bound on $W_2$ that Theorem 13 is built from, with equality for elliptical distributions sharing a generator. Proposition 1 sharpens the goal's containment to an equality on the mean-covariance projection itself, under the same two conditions ($\Xi = \mathbb{R}^m$, $\hat P_N$ elliptical). Corollary 1 propagates the goal's set containment to the risk level: $R_{\varepsilon,p}(\hat P_N,\ell) \le R_\varepsilon(\hat\mu,\hat\Sigma,\ell)$ for every $\ell$, where $R_\varepsilon(\hat\mu,\hat\Sigma,\ell) = \sup_{Q \in G_\varepsilon(\hat\mu,\hat\Sigma)} E_Q[\ell(\xi)]$ is the Gelbrich risk.

Significance

Theorem 13 is the hinge between an intractable infinite-dimensional worst-case-risk problem and a tractable one: the paper goes on (Theorem 16, outside this mission's scope) to show that for quadratic loss functions and elliptical nominal distributions the Gelbrich risk itself equals the optimal value of a semidefinite program with two linear matrix inequality constraints — and that, under those same conditions, the Wasserstein worst-case risk, the Gelbrich risk and the SDP value all coincide. Corollary 1 is what makes the Gelbrich risk usable as a conservative surrogate even outside that special case: it upper-bounds the true worst-case risk for any loss function and any $p \ge 2$, at the cost of discarding all but first- and second-order information about the nominal distribution. Formalizing the goal and Corollary 1 gives the exact scope in which this moment-relaxation is licensed — the $p \ge 2$ restriction and the outer-approximation direction are both easy to get backwards, and this mission's Lean encoding fixes both irreversibly.

Difficulty

The obvious first argument is to prove containment pointwise: fix $Q \in B_{\varepsilon,p}(\hat P_N)$ and show its mean and covariance land in $U_\varepsilon(\hat\mu,\hat\Sigma)$. That reduces Theorem 13 to Proposition 1's containment half, which in turn reduces to the Gelbrich bound (Theorem 4) applied to the pair $(Q,\hat P_N)$ — the inequality direction of Theorem 4 suffices for containment; only the sharper equality direction (needed for Proposition 1's own equality clause) requires the elliptical hypothesis. The non-obvious step is Theorem 4 itself: bounding $W_2(Q,Q')$ below by a closed-form expression in the two distributions' first two moments only, for arbitrary $Q,Q'$ with those moments, requires an argument that survives every coupling $\pi$ — the paper's proof goes through a lower bound on the coupling's cross-covariance term via the eigenvalues of $\Sigma^{1/2}\Sigma'\Sigma^{1/2}$, not a direct manipulation of $W_2$'s definition.

Formalization scope

$\mathbb{R}^m$ is EuclideanSpace ℝ (Fin m); a "distribution" is a MeasureTheory.Measure on it constrained by Q Set.univ = 1 (probability) and Q Ξᶜ = 0 (support in Ξ). The Wasserstein distance is ENNReal-valued (Definition 1's infimum over couplings, matching 01-duality's convention); the worst-case and Gelbrich risks are EReal-valued suprema restricted to loss functions integrable under the candidate distribution, avoiding Mathlib's junk value for a non-integrable Bochner integral. $\Sigma^{1/2}$ is the positive-semidefinite matrix square root, picked by choice from its defining existential and applied in this mission only to matrices hypothesized (or, per Section 2.3's standing assumption, given) positive semidefinite. Elliptical distributions (IsElliptical) are represented by the paper's own density formula (a measure equal to volume.withDensity of C·det(Σ)⁻¹·g((ξ-μ)ᵀΣ⁻¹(ξ-μ)) for some C>0), together with the mean/covariance facts every theorem in this chunk reads off directly; an earlier draft kept only the latter, under which "same density generator" held vacuously for any moment-matched pair — corrected after moderation flagged it (see STATUS.md). Because 01-duality (Wasserstein distance, ambiguity set, worst-case risk) is not yet a published mission, this chunk redefines those objects locally in its own namespace rather than importing an unpublished draft, per the series' definition-reuse policy; a future upload can retire the duplication once 01-duality is live. A formalization that dropped Theorem 4's "same density generator" condition from its equality clause, or that stated the goal's containment for all $p\ge 1$ rather than $p \ge 2$, would be trivializing or simply false — both are explicit hypotheses in the Lean statements. Matrix.PosSemidef and its Loewner order carry the $S^m_+$ constraints; no elliptical-distribution or Gelbrich-hull infrastructure exists elsewhere on the platform, so this mission's definitions are original contributions reusable by any later extension (Theorem 16/17, Lemma 1/2's SDP representations) of this series.

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
• Gelbrich, M. (1990). On a formula for the L2 Wasserstein metric between measures on Euclidean and Hilbert spaces. Mathematische Nachrichten, 147(1), 185–203.
• Mohajerin Esfahani, P., & Kuhn, D. (2018). Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations. Mathematical Programming, 171(1), 115–166.

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

$$R_n(\delta;F) := \mathbb E_{\varepsilon,x}\Big[\ \sup_{f\in F,\ \|f\|_2\le\delta}\ \Big| \tfrac1n\sum_{i=1}^n\varepsilon_if(x_i)\Big|\ \Big],$$

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$,

$$\Big|\|f\|_n^2-\|f\|_2^2\Big|\le\frac12\|f\|_2^2+\frac{t^2}2 \qquad\text{for all }f\in F,$$

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))$,

$$\big|\|f\|_n-\|f\|_2\big|\le c_0\delta_n \qquad\text{for all }f\in F,$$

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

$$\hat\theta_j \in \arg\min_{\theta\in\mathbb R^{d-1}}\ \frac1{2n}\|X_j-X_{\setminus\{j\}}\theta\|_2^2 +\lambda_n\|\theta\|_1,$$

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)}$:

$$\hat E\subseteq E \qquad\text{and}\qquad \forall (j,k):\ |\Theta^*_{jk}|\ge7b\lambda_n \implies (j,k)\in\hat E.$$

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.