Donsker's invariance principle

DefinitionClamping to the unit interval#✓fully proved

For a real number \(x\), its clamp to \([0,1]\) is \(\min(\max(x, 0), 1)\).

noncomputable def donskerClamp (x : ℝ) : ℝ :=
  min (max x 0) 1

Used by 2

Used byPolygonal interpolation weight · Polygonal interpolation weight as a continuous function

DefinitionPolygonal interpolation weight#✓fully proved

For natural numbers \(n\) and \(i\) and \(t \in [0,1]\), the weight is \(w_{n,i}(t) = \min(\max(nt - i, 0), 1)\), the clamp of \(nt - i\) to \([0,1]\).

noncomputable def donskerWeight (n i : ℕ) (t : Set.Icc (0 : ℝ) 1) : ℝ :=
  donskerClamp ((n : ℝ) * t.val - (i : ℝ))

Uses 1 · Used by 2

Statement usesClamping to the unit interval

Used byExplicit formula for the polygonal partial-sum process · Polygonal interpolation weight as a continuous function

DefinitionPolygonal interpolation weight as a continuous function#✓fully proved

For natural numbers \(n\) and \(i\), this is the function \(t \mapsto \min(\max(nt - i, 0), 1)\) on \([0,1]\), regarded as an element of the space \(C([0,1], \mathbb{R})\) of continuous real functions on \([0,1]\).

noncomputable def donskerWeightCM (n i : ℕ) : C(Set.Icc (0 : ℝ) 1, ℝ) where
  toFun := donskerWeight n i
  continuous_toFun := by
    unfold donskerWeight donskerClamp
    have h_val : Continuous (fun t : Set.Icc (0 : ℝ) 1 => (t.val : ℝ)) :=
      continuous_subtype_val
    have h_lin : Continuous (fun t : Set.Icc (0 : ℝ) 1 => (n : ℝ) * t.val - (i : ℝ)) := by
      fun_prop
    have h_clamp : Continuous (fun x : ℝ => min (max x 0) 1) := by
      fun_prop
    exact h_clamp.comp h_lin

Uses 2 · Used by 3

Statement usesClamping to the unit interval · Polygonal interpolation weight

Used byDonsker's invariance principle · Polygonal partial-sum process · Explicit formula for the polygonal partial-sum process

DefinitionPolygonal partial-sum process#✓fully proved

Let \(X_0, X_1, \dots\) be real-valued functions on a set \(\Omega\). For \(n \in \mathbb{N}\) and \(\omega \in \Omega\), \(S_n(\omega)\) is the element of the space \(C([0,1], \mathbb{R})\) of continuous real functions on \([0,1]\) defined by \(S_0(\omega) = 0\) and, for \(n \ge 1\) and \(t \in [0,1]\),

\[S_n(\omega)(t) = \frac{1}{\sqrt{n}} \sum_{i=0}^{n-1} X_i(\omega) \min(\max(nt - i, 0), 1).\]

Thus for \(n \ge 1\), \(S_n(\omega)\) linearly interpolates the values \((X_0(\omega) + \dots + X_{k-1}(\omega))/\sqrt{n}\) at the times \(k/n\) for \(0 \le k \le n\).

noncomputable def donskerProcess {Ω : Type*} (n : ℕ) (X : ℕ → Ω → ℝ) (ω : Ω) :
    C(Set.Icc (0 : ℝ) 1, ℝ) :=
  if n = 0 then 0
  else
    let sqrtInv : ℝ := (Real.sqrt (n : ℝ))⁻¹
    sqrtInv • (Finset.sum (Finset.range n) fun i => (X i ω) • donskerWeightCM n i)

Uses 1 · Used by 2

Statement usesPolygonal interpolation weight as a continuous function

Used byDonsker's invariance principle · Explicit formula for the polygonal partial-sum process

TheoremExplicit formula for the polygonal partial-sum process#✓fully proved

Let \(X_0, X_1, \dots\) be real-valued functions on a set \(\Omega\) and let \(S_n\) be their polygonal partial-sum process. For \(n \ge 1\), \(\omega \in \Omega\) and \(t \in [0,1]\), write \(m = \lfloor nt \rfloor\). Then

\[S_n(\omega)(t) = \frac{1}{\sqrt{n}} \Big( \sum_{i=0}^{m-1} X_i(\omega) + c \Big),\]

where \(c = (nt - m) X_m(\omega)\) if \(m < n\) and \(c = 0\) otherwise.

public theorem donskerProcess_apply_eq {Ω : Type*} (n : ℕ) (X : ℕ → Ω → ℝ) (ω : Ω)
    (t : Set.Icc (0 : ℝ) 1) (hn : n ≠ 0) :
    donskerProcess n X ω t =
      ((∑ i ∈ Finset.range (Nat.floor ((n : ℝ) * t.1)), X i ω) +
        if Nat.floor ((n : ℝ) * t.1) < n then
          X (Nat.floor ((n : ℝ) * t.1)) ω *
            ((n : ℝ) * t.1 - Nat.floor ((n : ℝ) * t.1))
        else 0) / Real.sqrt (n : ℝ)

Uses 3 · Used by 1

Statement usesPolygonal partial-sum process

Proof usesPolygonal interpolation weight · Polygonal interpolation weight as a continuous function

Used byDonsker's invariance principle

DefinitionInclusion of the unit interval into the nonnegative reals#✓fully proved

This map sends \(t \in [0,1]\) to \(t\) regarded as a nonnegative real number.

noncomputable def iccToNNReal (t : Set.Icc (0 : ℝ) 1) : ℝ≥0 :=
  ⟨t.val, t.2.1⟩

Used by 1

Used byDonsker's invariance principle

TheoremFinite-dimensional distributions determine laws on \(C((0,1))\)#✓fully proved

Probability measures on C([0,1], ℝ) are determined by their finite-dimensional distributions. Compatibility wrapper around MathlibExt.Probability.ContinuousPathConvergence.continuousPath_measure_ext_of_finset_eval at T = 1; the projective-limit argument lives there, not here.

public theorem continuousMap_measure_ext_of_finset_eval
    (μ ν : Measure C(Set.Icc (0 : ℝ) 1, ℝ))
    [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (h : ∀ I : Finset (Set.Icc (0 : ℝ) 1),
      μ.map (fun f => I.restrict (fun t => f t)) =
        ν.map (fun f => I.restrict (fun t => f t))) : μ = ν

Uses 1

Proof usesContinuous-path laws are determined by finite-dimensional marginals

TheoremEtemadi's maximal inequality#✓fully proved

Let \(X_0, X_1, \dots\) be independent real random variables on a probability space \((\Omega, P)\) and write \(S_k = X_0 + \dots + X_{k-1}\), so that \(S_0 = 0\). Then for every natural number \(n\) and every real number \(a\),

\[P\Big(\max_{0 \le k \le n} |S_k| \ge 3a\Big) \le 3 \max_{0 \le k \le n} P(|S_k| \ge a).\]

public theorem etemadi_maximal_inequality
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    (X : ℕ → Ω → ℝ) (hX : ∀ i, Measurable (X i))
    (hIndep : iIndepFun X P) (n : ℕ) (a : ℝ) :
    P {ω | ∃ k ∈ Finset.range (n + 1),
        3 * a ≤ |∑ i ∈ Finset.range k, X i ω|} ≤
      3 * (⨆ k ∈ Finset.range (n + 1),
        P {ω | a ≤ |∑ i ∈ Finset.range k, X i ω|})

Used by 1

Used byDonsker's invariance principle

TheoremDonsker's invariance principle#✓fully proved

Let \(X_0, X_1, \dots\) be independent, identically distributed, measurable real random variables on a probability space \((\Omega, P)\) such that \(X_0\) is integrable, \(\mathbb{E}[X_0^2] < \infty\), \(\mathbb{E}[X_0] = 0\) and \(\operatorname{Var}(X_0) = 1\). Let \((B_t)_{t \ge 0}\) be a real Brownian motion on a probability space \((\Omega', P')\): its finite-dimensional laws are those of Brownian motion and its paths are \(P'\)-almost surely continuous. For \(n \ge 1\) let \(S_n\) be the polygonal partial-sum process of the \(X_i\), the random element of \(C([0,1], \mathbb{R})\) that linearly interpolates the values \((X_0 + \dots + X_{k-1})/\sqrt{n}\) at the times \(k/n\) for \(0 \le k \le n\). Then there is a random element \(Y\) of \(C([0,1], \mathbb{R})\) defined on \(\Omega'\) such that \(P'\)-almost surely \(Y(t) = B_t\) for all \(t \in [0,1]\), and \(S_n\) converges in distribution to \(Y\) as \(n \to \infty\). Here \(C([0,1], \mathbb{R})\) carries the topology of uniform convergence and its Borel \(\sigma\)-algebra.

Proof: The route combines finite-dimensional convergence from the central limit theorem, tightness from a maximal inequality and a modulus-of-continuity criterion, Prokhorov's theorem, and uniqueness of laws on \(C([0,1], \mathbb{R})\) from finite-dimensional distributions.

MathlibExt.Probability.DonskerWanted.donsker_invariance_principle · 16 lines

public theorem donsker_invariance_principle
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {Ω' : Type*} [MeasurableSpace Ω'] {P' : Measure Ω'} [IsProbabilityMeasure P']
    (X : ℕ → Ω → ℝ)
    (hMeas : ∀ n, Measurable (X n))
    (hIndep : iIndepFun X P)
    (hIdent : ∀ i, IdentDistrib (X i) (X 0) P P)
    (hInt : Integrable (X 0) P)
    (hMemLp : MemLp (X 0) 2 P)
    (hMean : P[X 0] = 0)
    (hVar : Var[X 0; P] = 1)
    (B : ℝ≥0 → Ω' → ℝ) (hB : IsBrownianReal B P') :
    ∃ (Y : Ω' → C(Set.Icc (0 : ℝ) 1, ℝ)),
      (∀ᵐ ω' ∂P', ∀ t : Set.Icc (0 : ℝ) 1, (Y ω' t) = B (iccToNNReal t) ω') ∧
      TendstoInDistribution (fun n (ω : Ω) => donskerProcess n X ω) Filter.atTop Y
        (fun _ => P) P'

Sources

• M. D. Donsker, An invariance principle for certain probability limit theorems, Mem. Amer. Math. Soc. 6 (1951); extension Prohorov 1956 to Polish; textbook in Billingsley, Convergence of Probability Measures, 2nd ed., Kallenberg, Foundations of Modern Probability; Lean is C(Icc 0 1, ℝ) polygonal process with MemLp 2, mean-zero variance-one standardization.

Uses 6

Statement usesPolygonal partial-sum process · Inclusion of the unit interval into the nonnegative reals

Proof usesTightness plus finite-dimensional convergence gives weak convergence · Explicit formula for the polygonal partial-sum process · Polygonal interpolation weight as a continuous function · Etemadi's maximal inequality

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.