Kolmogorov–Chentsov Continuous Modification

This is the Kolmogorov–Chentsov continuous-modification theorem. Let $P$ be a probability measure and let $X:\mathbb R\to\Omega\to\mathbb R$ satisfy IsKolmogorovProcess X P p q M. If $1<q$, then there exists $Y:\mathbb R\to\Omega\to\mathbb R$ such that

and, for every $t\in\mathbb R$, $Y(t)=X(t)$ almost surely. The theorem uses the exponent $\alpha=(q-1)/(2p)$ internally, but the conclusion asserts only existence of the continuous modification.

Original Lean declaration header

Within namespace LevyStochCalc.Brownian.Continuity. Shown in its original module context. Proof omitted.

theorem kolmogorovChentsov_modification
    (P : Measure Ω) [IsProbabilityMeasure P]
    (X : ℝ → Ω → ℝ) {p q : ℝ} {M : ℝ≥0}
    (hX : ProbabilityTheory.IsKolmogorovProcess X P p q M)
    (hq : 1 < q) :
    ∃ Y : ℝ → Ω → ℝ,
      (∀ᵐ ω ∂P, Continuous (fun t => Y t ω)) ∧
      (∀ t : ℝ, ∀ᵐ ω ∂P, Y t ω = X t ω)

Module navigation

Module: LevyStochCalc/Brownian/Continuity.

Supporting theorems: dense_dyadicRationals, exists_tendsto_of_local_holder, kc_ae_nbhd_holder, kolmogorov_modification_ae_eq.

Source excerpt, lines 51–58 · Frozen source 408915f.