- gaussian_increments (n : ℕ) (t : Fin (n + 1) → NNReal) : StrictMono t → t 0 = 0 → ∀ (j : Fin n), ProbabilityTheory.HasLaw (fun (ω : Ω) => B (t j.succ) ω - B (t j.castSucc) ω) (ProbabilityTheory.gaussianReal 0 (t j.succ - t j.castSucc)) P
Instances For
- gaussian_process : ProbabilityTheory.IsGaussianProcess B P
Instances For
- indep : ProbabilityTheory.iIndepFun a P
- std_gaussian (k : ℕ) : ProbabilityTheory.HasLaw (a k) (ProbabilityTheory.gaussianReal 0 1) P
Instances For
Instances For
Instances For
Instances For
Instances For
If $X$ has law $\mathcal{N}(0, v)$ under $P$, then $\operatorname{Var}[X; P] = v$.
If $X$ has law $\mathcal{N}(0, v)$ under $P$, then $\mathbb{E}[X] = \int_\Omega X \,\mathrm{d}P = 0$.
If $X$ has law $\mathcal{N}(0, v)$ under $P$, then $X$ has a Gaussian law under $P$.
A real-valued Gaussian random variable with law $\mathcal{N}(0, v)$ lies in $L^2(P)$.
The partial sum $S_n = \sum_{k < n} X_k$ of Gaussian random variables lies in $L^2(P)$.
The partial sum $S_n = \sum_{k < n} X_k$ viewed as an element of $L^2(P)$.
Instances For
For a centered $L^2$ random variable $f$ on a probability space, $\|f\|_{L^2}^2 = \operatorname{Var}(f)$.
For independent Gaussian random variables $X_k \sim \mathcal{N}(0, v_k)$, the variance of the block sum $\sum_{k \in [n, m)} X_k$ equals $\sum_{k \in [n, m)} v_k$.
For a summable nonnegative sequence $v$, the block sum is bounded by the tail of the series: $\sum_{k \in [n, m)} v_k \leq \sum_{k \geq 0} v_{k + n}$.
The $L^2$-distance between partial sums $S_n$ and $S_m$ (with $n \leq m$) is bounded by $\sqrt{\sum_{k \geq 0} v_{k + n}}$, the square root of the tail of the variance series.
If $\sum_k v_k < \infty$, then the partial sums $S_n = \sum_{k < n} X_k$ form a Cauchy sequence in $L^2(P)$.
Existence of the $L^2$-limit: completeness of $L^2(P)$ gives an $S \in L^2(P)$ such that the partial sums $S_n = \sum_{k < n} X_k$ converge to $S$ in $L^2(P)$.
The partial sum of independent Gaussian random variables has a Gaussian law: if each $X_k \sim \mathcal{N}(0, v_k)$ and the $X_k$ are independent, then $\sum_{k < n} X_k$ has a Gaussian law on $\mathbb{R}$.
Identification of the law of the partial sum: if $X_k \sim \mathcal{N}(0, v_k)$ are independent, then $\sum_{k < n} X_k \sim \mathcal{N}\bigl(0, \sum_{k < n} v_k\bigr)$.
The $L^2$-limit $S$ inherits the Gaussian law: if $S_n = \sum_{k < n} X_k \to S$ in $L^2(P)$, then $S \sim \mathcal{N}\bigl(0, \sum_k v_k\bigr)$. The proof uses convergence in measure $\Rightarrow$ convergence in distribution together with continuity of the characteristic function $\mathcal{N}(0, \sum_{k<n} v_k) \to \mathcal{N}(0, \sum_k v_k)$.
Proposition 1 (Brownian Motion). Let $(X_k)_{k \geq 0}$ be independent real-valued Gaussian random variables on a probability space $(\Omega, P)$ with $X_k \sim \mathcal{N}(0, v_k)$ and $\sigma^2 := \sum_k v_k < \infty$. Then there exists a random variable $S$ such that the partial sums $\sum_{k < n} X_k$ converge to $S$ in $L^2(P)$ and $S \sim \mathcal{N}(0, \sigma^2)$.
Predicate characterizing a Rademacher-type random variable $R : Ω → ℝ$ on $(Ω, P)$: $R$ is measurable, has mean zero $\mathbb{E}[R] = \int R\,\mathrm{d}P = 0$, and unit variance $\mathbb{E}[R^2] = \int R^2\,\mathrm{d}P = 1$. The canonical example is the symmetric $\pm 1$ Bernoulli (Rademacher) variable.
- measurable : Measurable R
Instances For
The Donsker-scaled increment of the random walk between indices $k_{\text{prev}}$ and $k_{\text{next}}$: $$\frac{S_{k_{\text{next}}}(ω) - S_{k_{\text{prev}}}(ω)}{\sqrt{n}}.$$ This is the basic building block whose distribution converges to a Gaussian as $n \to \infty$.
Instances For
The discrete grid index associated with a continuous time $t_j$ at scale $n$: $\lfloor n \cdot t_j \rfloor$. Converts a continuous time partition into the nearest discrete step on the random walk.
Instances For
The vector of variances $\sigma_j^2 = t_{j+1} - t_j$ for $j = 0, \dots, m-1$ associated with a strictly increasing time partition $t : \mathrm{Fin}(m+1) \to ℝ$. These are the variances of the limiting independent Gaussian increments in Brownian finite-dimensional distribution convergence.
Instances For
Monotonicity of the grid index: for a strictly monotone time partition $t$ and fixed scale $n$, the discrete grid indices $j \mapsto \lfloor n \cdot t_j \rfloor$ form a monotone sequence.
The block size $\lfloor n \cdot t_{j+1} \rfloor - \lfloor n \cdot t_j \rfloor$ tends to infinity as $n \to \infty$, since $t_{j+1} - t_j > 0$. This is what allows the central limit theorem to apply on each block.
Rewrite the scaled increment as a normalized sum over a block: $\dfrac{S_{k_{\text{next}}} - S_{k_{\text{prev}}}}{\sqrt{n}} = \dfrac{1}{\sqrt{n}} \sum_{i \in [k_{\text{prev}}, k_{\text{next}})} R_i(ω)$.
The ratio of block size to total scale converges to the time difference: $$\frac{\lfloor n \cdot t_{j+1} \rfloor - \lfloor n \cdot t_j \rfloor}{n} \;\longrightarrow\; t_{j+1} - t_j \quad (n \to \infty).$$ This is the key asymptotic that lets the rescaled increments carry the correct Brownian variance in the limit.
Central Limit Theorem with variable block sizes. For iid mean-zero unit-variance random variables $(R_i)$, if a block of length $m_n$ starting at $a_n$ satisfies $m_n \to \infty$ and $m_n / n \to \sigma^2$, then the normalized block sum $$\frac{1}{\sqrt{n}} \sum_{i=a_n}^{a_n + m_n - 1} R_i$$ converges in distribution to a centered Gaussian with variance $\sigma^2$.
For iid Rademacher variables, the single scaled increment between grid points $t_j$ and $t_{j+1}$ converges in distribution to a Gaussian with mean $0$ and variance $\sigma_j^2 = t_{j+1} - t_j$. This is the one-dimensional marginal of the Brownian FDD convergence, obtained by applying the variable-block CLT to the block $[\lfloor n t_j \rfloor, \lfloor n t_{j+1} \rfloor)$.
Independence of $\sigma$-algebras indexed by disjoint families. Given an $ι$-indexed independent family of $\sigma$-algebras $(m_i)$ and a $κ$-indexed family of pairwise disjoint subsets $(S_j) \subseteq ι$, the bundled $\sigma$-algebras $\bigvee_{i \in S_j} m_i$ are independent across $j$.
The collection of scaled increments $\bigl(\mathrm{scaledIncrement}\,R\,n\,\lfloor n t_j \rfloor\,\lfloor n t_{j+1} \rfloor\bigr)_{j \in \mathrm{Fin}\,m}$ is jointly independent, because each increment is measurable with respect to the $\sigma$-algebra generated by $(R_i)$ on a disjoint block of indices.
Joint convergence from marginal convergence for independent coordinates. If for each $j$ the marginal sequence $X_n(j)$ converges in distribution to $Z(j)$, and if the coordinates $(X_n(j))_j$ are jointly independent for every $n$ (and the limit coordinates $(Z(j))_j$ are independent), then the full vector $X_n(\cdot)$ converges in distribution to $Z(\cdot)$.
Brownian FDD convergence (discrete version). For iid Rademacher random
variables $(R_i)$, the vector of scaled increments on a partition
$0 \le t_0 < t_1 < \cdots < t_m$ converges jointly in distribution to a vector of
independent Gaussians with variances $\sigma_j^2 = t_{j+1} - t_j$. This combines
the one-dimensional CLT on each block (increment_tendstoInDistribution_gaussianReal)
with the joint-from-marginal-with-independence principle
(indep_marginal_tendstoInDistribution_product).
The Donsker-scale piecewise linear interpolation $f_n(t)$ of the random walk: between integer scaled times $k/n$ and $(k+1)/n$, the function interpolates linearly between $S_k/\sqrt{n}$ and $S_{k+1}/\sqrt{n}$. Explicitly, with $k = \lfloor n t \rfloor$ and fractional part $\{nt\} = nt - k$, $$f_n(t)(ω) = \frac{S_k(ω)}{\sqrt{n}} + \{nt\} \cdot \frac{R_k(ω)}{\sqrt{n}}.$$ This is the continuous-time process whose finite-dimensional distributions converge to those of Brownian motion.
Instances For
Decomposition of the continuous-time increment of $f_n$ into the discrete scaled increment plus a small fractional error: $$f_n(t_{\text{next}}) - f_n(t_{\text{prev}}) = \mathrm{scaledIncrement},R,n,\lfloor n t_{\text{prev}} \rfloor,\lfloor n t_{\text{next}} \rfloor
- \frac{1}{\sqrt{n}}\Bigl({n t_{\text{next}}} R_{\lfloor n t_{\text{next}} \rfloor}
- {n t_{\text{prev}}} R_{\lfloor n t_{\text{prev}} \rfloor}\Bigr).$$
The error term is uniformly bounded by $2/\sqrt{n}$ (provided $|R_i| \le 1$) and so
vanishes in the limit; this is the basis of the Slutsky argument for
brownian_fdd_convergence.
Slutsky's theorem for deterministic perturbations. If $X_n \Rightarrow Z$ in distribution and $Y_n$ is uniformly close to $X_n$, with $\sup_ω \mathrm{dist}(Y_n(ω), X_n(ω)) \le \varepsilon_n \to 0$, then $Y_n \Rightarrow Z$ in distribution as well. This is the standard tool for transferring distributional convergence across a vanishing additive error term.
Theorem 1 — Brownian Motion (finite-dimensional distribution convergence).
Let $(R_i)$ be iid Rademacher random variables with $|R_i| \le 1$. Then for any
strictly increasing time partition $0 \le t_0 < t_1 < \cdots < t_m$, the vector of
continuous-time increments
$$\bigl(f_n(t_1) - f_n(t_0),\; \dots,\; f_n(t_m) - f_n(t_{m-1})\bigr)$$
of the piecewise linear interpolation $f_n$ converges in distribution to a vector
of independent centered Gaussians with variances $\sigma_j^2 = t_j - t_{j-1}$.
Equivalently, the finite-dimensional distributions of $f_n$ converge to those of a
standard Brownian motion. The proof combines the discrete FDD convergence
(brownian_fdd_convergence_discrete) with Slutsky's theorem applied to the bounded
fractional error $\le 2/\sqrt{n}$ from fnIncrement_eq_scaledIncrement_add_error.
Instances For
Instances For
Closed-form decomposition of the coefficient pairing $\sum_k c_k(s)\,c_k(t)$ into the constant-mode term $st/\pi$ and the sine-series tail $\tfrac{2}{\pi}\sum_{k\ge 1}\sin(ks)\sin(kt)/k^2$, where $c_k$ are the Wiener basis coefficients.
Bilinear-Parseval expansion of the Wiener-process covariance: for i.i.d. standard Gaussian coefficients $(a_k)$ the expectation $\mathbb{E}(W_s W_t)$ equals $st/\pi$ plus the Fourier sine tail $\tfrac{2}{\pi}\sum_{k\ge 1}\sin(ks)\sin(kt)/k^2$.
Helper: evaluate the second Bernoulli polynomial under the $\mathbb{Q}\to\mathbb{R}$ algebra map, giving $B_2(x) = x^2 - x + 1/6$.
Closed-form for the Fourier cosine series with $1/k^2$ coefficients on $[0,2\pi]$: $\sum_{n\ge 1} \cos(n\theta)/n^2 = \theta^2/4 - \pi\theta/2 + \pi^2/6$. This is the classical Bernoulli evaluation of the second Bernoulli polynomial.
Closed-form evaluation of the sine cross-product series on $[0,\pi]$: for $0 \le s \le t \le \pi$, $\sum_{k\ge 1}\sin(ks)\sin(kt)/k^2 = s(\pi-t)/2$. This is the off-diagonal Fourier expansion that yields the Brownian covariance $s \wedge t$.
The Brownian-motion covariance identity for the Wiener construction: for $s, t \in [0,\pi]$, the expectation of $W_s W_t$ equals $s \wedge t$ under any distribution of i.i.d. standard Gaussian coefficients.
Cauchy-Schwarz on intervals: the square of an interval integral is bounded by the length times the integral of the square, $\bigl(\int_0^L g\bigr)^2 \le L\int_0^L g^2$.
Bessel's inequality on the circle of radius $r<1$: for any finite truncation $u$, $\sum_{k\in u}|a_{k+1}(\omega)|^2 r^{2k} \le \tfrac{1}{2\pi}\int_0^{2\pi}\|f'(re^{it})\|^2\,dt$, where $f'$ denotes the formal derivative of the random power series.
The squared norm $\|f'(re^{it})\|^2$ of the random-power-series derivative is interval-integrable on $[0, 2\pi]$ for any $r \in (0,1)$.
The fourth-power norm $\|f'(re^{it})\|^4$ of the random-power-series derivative is interval-integrable on $[0, 2\pi]$ for any $r \in (0,1)$; needed later for the Cauchy-Schwarz step in the gradient bound.
Bessel-type $\ell^2$ bound on the random Fourier coefficients: if the weighted gradient integral $\int (1-r)^{\beta}\|f'(re^{it})\|^2$ is bounded by $C$, then the sequence $\|a_{k+1}(\omega)\|^2$ is summable with sum at most $4\sqrt{(|C|+1)/(2\pi)} + 1$.
Uniform partial-sum bound: every finite Parseval partial sum of the squared random Fourier coefficients is bounded by $4\sqrt{(|C|+1)/(2\pi)} + 1$, given the weighted gradient integral bound $C$.
Parseval $\ell^2$-summability: if the weighted gradient integral is finite, the squared random Fourier coefficients $\|a_{k+1}(\omega)\|^2$ form a summable sequence.
AM-GM bridge: if $(\|a_{k+1}(\omega)\|^2)$ is summable, then so is $(\|a_{k+1}(\omega)\|/(k+1))$, since $|a|/(k+1) \le \tfrac12(|a|^2 + 1/(k+1)^2)$ and the $1/(k+1)^2$ series converges.
Summability of the random-power-series coefficients $\|a_{k+1}(\omega)\|/(k+1)$, granted a finite weighted gradient integral. This gives uniform convergence of $f(z) = \sum a_{k+1}(\omega) z^{k+1}/(k+1)$ on $\overline{\mathbb{D}}$.
Area-mean-value-property tsum bound: at any interior point $z\in\mathbb{D}$, the coefficient sum $\sum\|a_{k+1}(\omega)\|/(k+1)$ is dominated by $\tfrac12\max(1,|C_\star|+1)\,(1-\|z\|)^{\min((\beta-1)/4,1)}$, a quantitative local Hardy-space estimate.
Cauchy-type derivative bound: dividing the coefficient sum by the radius $(1-\|z\|)/2$ produces a quantitative upper bound on the derivative norm at $z$, $\max(1,|C_\star|+1)(1-\|z\|)^{-1+\min((\beta-1)/4,1)}$.
Submean-area gradient bound: the Frechet derivative of the random power series at $z\in\mathbb{D}$ satisfies $\|\nabla f(z)\| \le \max(1,|C_\star|+1)(1-\|z\|)^{-1+\min((\beta-1)/4,1)}$. This is Lemma 4 of the textbook, combining Cauchy's estimate with the area MVP.
Restatement of submean_area_gradient_bound as a named pointwise gradient
estimate, suitable for use in subsequent boundary-regularity proofs.
Continuity on the closed disk: granted a finite weighted gradient integral, $z\mapsto f(z) = \sum a_{k+1}(\omega)z^{k+1}/(k+1)$ is continuous on $\overline{\mathbb{D}}$ by Weierstrass M-test.
Real differentiability inside the disk: under the same finite weighted gradient hypothesis, $f$ is real-differentiable on the open disk $\mathbb{D}$, obtained via complex differentiability of a uniformly convergent power series.
Repackaging the submean gradient bound as a SatisfiesGradientBound
predicate with constants $(\max(1,|C_\star|+1),\min((\beta-1)/4,1))$, the
hypothesis needed for the abstract Hardy-Littlewood boundary-Hölder argument.
Lemma 4 packaged: if the weighted gradient integral is finite, the random power series $f$ is continuous on $\overline{\mathbb{D}}$, real-differentiable on $\mathbb{D}$, and satisfies a quantitative gradient bound for some $(C_g,\alpha)$ with $0<\alpha\le 1$ -- precisely the hypotheses of the abstract boundary-Hölder lemma.
Transfer step (Lemma 5): a Hölder estimate on the boundary trace $t\mapsto f(e^{it})$ implies continuity of the Wiener process $t\mapsto W_t$ on $[0,\pi]$. The imaginary part of the boundary values recovers the sine series defining $W_t$.
Almost-sure continuity (the crux of Theorem 2): for $P$-almost every sample path $\omega$, the Wiener process $t\mapsto W_t(\omega)$ is continuous on $[0,\pi]$. The proof chains the a.s. finiteness of the weighted gradient integral, the gradient bound, the boundary Hölder lemma, and the boundary transfer to the imaginary part of the random power series.
Main theorem of the chapter (Theorem 2): the Wiener construction $W(t) = c_0 a_0 t + c_1 \sum_{k\ge 1} a_k \sin(kt)/k$, with $(a_k)$ i.i.d. standard Gaussian, is a Brownian motion on $[0,\pi]$, i.e. satisfies the four defining properties: starts at $0$, has mean $0$, is a Gaussian process with $\mathbb{E}(W_s W_t) = s\wedge t$, and has a.s. continuous sample paths.