Almost-Sure Equality of a Continuous Modification

This is the fixed-time modification-identification lemma. Let $P$ be a probability measure on $\Omega$, let $X:\mathbb R\to\Omega\to\mathbb R$ satisfy IsKolmogorovProcess X P p q M, and let $Y:\mathbb R\to\Omega\to\mathbb R$. Assume that $Y(\cdot,\omega)$ is continuous for $P$-almost every $\omega$, and that for every dyadic rational $s$, $Y(s,\omega)=X(s,\omega)$ almost surely. Then for every $t\in\mathbb R$,

The conclusion is pointwise in the time parameter; it is not a single exceptional null set uniform over all $t$.

Original Lean declaration header

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

lemma kolmogorov_modification_ae_eq
    (P : Measure Ω) [IsProbabilityMeasure P]
    (X : ℝ → Ω → ℝ) {p q : ℝ} {M : ℝ≥0}
    (hX : ProbabilityTheory.IsKolmogorovProcess X P p q M)
    (Y : ℝ → Ω → ℝ)
    (h_continuous : ∀ᵐ ω ∂P, Continuous (fun t => Y t ω))
    (h_dyadic_eq : ∀ s ∈ dyadicRationals, ∀ᵐ ω ∂P, Y s ω = X s ω) :
    ∀ t : ℝ, ∀ᵐ ω ∂P, Y t ω = X t ω

Module navigation

Module: LevyStochCalc/Brownian/ContinuityKolmogorovBounds.

Definition modules: LevyStochCalc/Brownian/ContinuityDyadicChaining.

Supporting theorems: dense_dyadicRationals, kolmogorov_markov_bound.

Previous: kc_ae_nbhd_holder.

Source excerpt, lines 419–426 · Frozen source 408915f.