Stochastic Systems

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.

Motivation

A stochastic linear program is a linear optimization problem whose coefficients depend on a random parameter. Even when the model is feasible and bounded almost surely, its optimal value is itself a random quantity. Knowing only its expectation can hide the probability of unusually favorable or unfavorable outcomes; its full distribution supports threshold probabilities, quantiles, and later risk-sensitive decisions. Chapter II of Peter Kall's Stochastic Linear Programming develops a finite-dimensional method for determining that distribution when the constraint matrix, right-hand side, and objective coefficients depend affinely on the same random vector. Theorem 8, printed p. 29 / PDF35, is the chapter's general distribution formula. This mission asks for that known theorem to be proved in Lean from its reviewed statement.

Setting

Fix a finite parameter vector $t\in\mathbb R^r$. An affine random linear program supplies a matrix $A(t)\in\mathbb R^{m\times n}$, a right-hand side $b(t)\in\mathbb R^m$, and costs $c(t)\in\mathbb R^n$, each affine in $t$. Its optimal value is the extended-real infimum

$$\gamma(t)=\inf\{c(t)^\top x:A(t)x=b(t),\ x\ge 0\}.$$

The parameter has a probability law $\mu$, supported almost surely on a measurable set $T$, with a nonnegative extended-real density $f$ relative to Lebesgue measure. The extended-real value records infeasibility as $+\infty$ and unboundedness as $-\infty$; the target distribution deliberately restricts to the finite-value event $-\infty<\gamma(t)\le\xi$.

A candidate basis is an increasing selection $\sigma:\operatorname{Fin}(m)\to\operatorname{Fin}(n)$. Its basis matrix $B_\sigma(t)$ consists of the selected columns of $A(t)$. Kall enumerates exactly those candidate bases whose determinant is nonzero at some point of $T$. For each one, its raw optimality region consists of the parameters for which $B_\sigma(t)^{-1}b(t)\ge0$ and the reduced costs $c(t)^\top-c_B(t)^\top B_\sigma(t)^{-1}A(t)$ are nonnegative. Matrix inversion is totalized to zero at singular matrices, matching the source convention. The ordered basis regions remove every earlier raw region, so overlapping optimal bases are assigned to the first enumerated basis. On a basis region the associated value is

$$\gamma_\sigma(t)=c_B(t)^\top B_\sigma(t)^{-1}b(t).$$

Assumption A1 is explicit in Lean: the density and support clauses above, both almost-sure feasibility/boundedness implications from Theorem 4, and the existence of one full-row-rank column minor at a point of $T$. The basis enumeration is injective and exhaustive for the almost nonsingular increasing selections.

Formalization targets

Theorem 8: distribution by basis regions

For the ordered regions $B_i$, the theorem states

$$\mu\!\left(\bigcup_i B_i\right)=\sum_i\mu(B_i)=1.$$

For every real threshold $\xi$, it further identifies the finite optimal-value distribution by

$$\mu\{t\in T:-\infty<\gamma(t)\le\xi\} =\sum_i\int_{\{t\in B_i:\gamma_i(t)\le\xi\}} f(t)\,dt.$$

The normalization and distribution identity are the two clauses of the same source theorem and remain one goal. Determinant facts, special stochastic models, and examples elsewhere in the chapter are context rather than additional mission targets.

Significance

The result turns the distribution of a random optimization value into a finite sum of ordinary density integrals over explicitly described parameter regions. It connects parametric linear programming geometry with probabilistic questions about the optimum and provides the chapter's foundation for studying particular stochastic models and derived distributional quantities. Without the coverage and normalization clauses, the integral expression could omit positive-probability parameter regimes; without the finite-value event, extended-real exceptional outcomes would be conflated with a real-valued distribution function.

The theorem is established in the 1976 source, but the staged Lean declaration contains a proof placeholder. Completing it would produce a machine-checked account of the basis-region decomposition under the source's full hypotheses. The reusable content includes the affine model, basis matrix, raw-region inequalities, ordered disjointification, basis value, and the referenced extended-real linear-program value.

Difficulty

The natural pointwise argument chooses an optimal basis and substitutes its basic solution. That alone does not prove a measurable probability decomposition: several bases may be optimal at the same parameter, bases may become singular on exceptional sets, and the optimal value may be infinite. The ordered subtraction of earlier regions resolves overlap only after one proves exhaustive coverage under A1. The final equality must also connect the extended-real infimum to the real basis value on each region and justify the density integrals on the threshold sets. Treating the raw regions as automatically disjoint or silently assuming every parameter has a unique nonsingular optimizer would bypass the central issues.

Formalization scope

All dimensions and basis lists are finite. The law is a probability measure on $\operatorname{Fin}(r)\to\mathbb R$, represented as volume.withDensity f; $T$ is measurable and carries the law almost surely. The density is ENNReal-valued and the displayed integrals are nonnegative lintegrals. No integrability or finite-moment hypothesis is imposed on the optimal value. LPValue is an existing referenced platform definition using EReal.sInf; the book-local declarations remain in the shared Kall1976 namespace. Mathlib's nonsingular inverse supplies the source's zero value at singular matrices.

The formal target must retain both almost-sure implications, the one-point full-rank condition, increasing and exhaustive basis enumeration, region ordering, probability-one normalization, the strict lower bound by $-\infty$, and the weak upper threshold $\le\xi$. Removing any of these clauses would change the reviewed theorem rather than simplify its proof. Contributions may develop measurable-region, finite-basis coverage, LP optimality, and density-integration lemmas, provided they preserve these conventions.

Selected references

• Peter Kall, Stochastic Linear Programming, Springer, 1976, Chapter II §1: Theorem 4 printed p. 25 / PDF31; model (5) printed p. 27 / PDF33; Assumption A1 printed p. 28 / PDF34; Theorem 8 printed p. 29 / PDF35. DOI.

Motivation

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

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

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

Setting

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

$$W_n(t)\ =\ \frac{S(nt)}{\sqrt n},\qquad t\in[0,1],$$

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

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

Formalization targets

Goal — Theorem 8.1.4, Donsker's theorem

$$\frac{S(n\cdot)}{\sqrt n}\ \Longrightarrow\ B(\cdot)\qquad\text{in }C[0,1],$$

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

Supporting levels

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

Significance

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

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

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

Difficulty

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

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

$$\int\varphi\,dF=c^{-1}\int_0^\infty dF(v)\int_{-\infty}^0 dF(u)\,(v-u) \Bigl[\tfrac{v}{v-u}\varphi(u)+\tfrac{-u}{v-u}\varphi(v)\Bigr], \qquad c=\int_0^\infty v\,dF(v),$$

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

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

Formalization scope

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

The polygonal interpolation is written as a finite sum,

$$S(u)=\sum_{k<n}X_k\cdot\operatorname{clamp}(u-k),\qquad \operatorname{clamp}(x)=\max(0,\min(1,x)),$$

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

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

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

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

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

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

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

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

Selected references

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