Why couple sums to Brownian motion

Independent sums are a basic model for accumulated random fluctuation. A central limit theorem describes their distribution at one large time, and a functional limit theorem describes weak convergence of a rescaled path. Strong approximation asks for substantially more: construct the sums and a Brownian motion on one probability space so that their paths remain close, with an explicit error bound that holds simultaneously over all earlier integer times. Such a coupling turns Brownian path estimates into quantitative information about random walks and independent sums.

Chapter 7, Section 5 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986) states this strong approximation result as Theorem 5.1. Its estimate has logarithmic deterministic error and a strictly exponential tail. The theorem is known as a Komlós–Major–Tusnády type approximation, but the mission follows the exact formulation and hypotheses printed by Ethier and Kurtz.

Probability law and common space

Let $\mu$ be a probability measure on $\mathbb R$. The hypothesis requires an $\alpha_0>0$ such that

$$\int_{\mathbb R} e^{\alpha x}\,\mu(dx)<\infty \qquad\text{whenever }|\alpha|\leq \alpha_0.$$

Thus the moment-generating integral is finite on a neighborhood of zero. No centering, symmetry, bounded-support, or positive-variance assumption is made.

The conclusion constructs one probability space carrying an iid sequence $(\xi_i)_{i\geq1}$ with common law $\mu$ and a Brownian motion $W$. The Brownian motion has drift and variance chosen to match one summand:

$$E[W(1)]=E[\xi_1]=m, \qquad \operatorname{var}(W(1))=\operatorname{var}(\xi_1)=\sigma^2.$$

Writing $S_k=\sum_{i=1}^k\xi_i$, both $S_k$ and $W(k)$ are evaluated on this same space. The theorem does not require the iid sequence to be independent of the Brownian coordinate; their dependence is precisely what permits a close coupling.

Formalization target

There are positive constants $C$, $K$, and $\lambda$, depending only on $\mu$, such that for every integer $n\geq1$ and every real $x>0$,

$$P\left\{\max_{1\leq k\leq n}|S_k-W(k)|>C\log n+x\right\} <K e^{-\lambda x}.$$

Both inequalities are strict: the discrepancy event uses $>$ and its probability is $<K e^{-\lambda x}$. The constants and the entire coupling are chosen before $n$ and $x$. The logarithmic term is retained at $n=1$, where $\log 1=0$.

The Lean statement uses sequence coordinates indexed from zero, so coordinate $i$ represents the source variable $\xi_{i+1}$ and Finset.range k is exactly the sum of the first $k$ variables. An existential index $k$ with $1\leq k\leq n$ expresses the finite maximum event without replacing either strict inequality.

What the theorem provides

Weak convergence compares distributions after rescaling and does not place a prelimit sum and its limiting process on the same sample point. This theorem instead supplies a simultaneous pathwise comparison through a common-space construction. The exponential tail quantifies the chance that the uniform error up to time $n$ exceeds the logarithmic scale by an additional amount $x$.

The formal statement records the complete coupling rather than only its consequence for normalized terminal sums. It exposes the iid coordinate laws, mutual independence of those coordinates, the Brownian law, the moment-matched affine scaling, the positivity and quantifier order of the constants, and the exact maximal-error event. This is a statement-only formalization: the theorem remains an open Lean goal, and no proof claim is made.

Where the difficulty lies

Matching a single sum to a Gaussian random variable is not enough. The construction must coordinate every partial sum with one Brownian path, uniformly over all $k\leq n$, while keeping the error logarithmic and the excess probability exponentially small. Independent coupling at each time would destroy consistency across times, while an ordinary invariance principle gives convergence in distribution without the stated finite-$n$ tail. The difficulty is therefore the joint construction with all of these quantitative requirements at once.

Formalization scope and conventions

The common carrier is the product of a real sequence space with the subtype of continuous functions from nonnegative real time to $\mathbb R$. A probability measure $Q$ on that carrier is the joint law. iIndepFun asserts mutual independence of all sequence coordinates, and HasLaw gives each coordinate the law $\mu$. IsBrownianReal specifies the standard Brownian second coordinate.

The Brownian motion appearing in the estimate is defined from that standard coordinate by

$$W(t)=mt+\sqrt{\operatorname{var}_\mu(X)}\,B(t).$$

This representation covers the zero-variance case: then the scaled Brownian fluctuation vanishes and $W$ is deterministic, while the auxiliary standard Brownian coordinate may still be present on the common carrier. The exponential-moment hypothesis supplies the intended finite first and second moments. Probabilities use extended nonnegative reals, and the finite positive real bound $K e^{-\lambda x}$ is embedded with ENNReal.ofReal.

No local auxiliary definition is expression-essential: all objects in the theorem are provided by Mathlib. The mission intentionally excludes the section's rescaling observations and Poisson corollaries, which do not form separate capstone goals in the accepted grouping. Useful future contributions include the proof of this exact common-space theorem and reusable coupling infrastructure that preserves strict tail estimates.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 7, Section 5, Theorem 5.1, equation (5.1), printed p. 356. Wiley DOI