Kolmogorov continuity theorem

DefinitionDyadic rationals#✓fully proved

The set of dyadic rationals: real numbers of the form k / 2 ^ n for some integer k and natural number n.

def dyadicRationals : Set ℝ :=
  {x : ℝ | ∃ k : ℤ, ∃ n : ℕ, x = k / (2 : ℝ) ^ n}

Used by 5

Used byDeterministic chaining · Kolmogorov continuous-modification theorem for real-valued processes · Almost sure Hölder bound on the dyadic rationals · Hölder bound on dyadics for a Kolmogorov process · Kolmogorov continuity theorem

TheoremDeterministic chaining#✓fully proved

If every adjacent dyadic increment at level m is at most D * 2^{-mγ}, then f is γ-Hölder on the dyadic rationals of [0, 1], with an explicit constant.

theorem dyadic_holder_of_increment_bound {f : ℝ → ℝ} {γ D : ℝ} (hγ : 0 < γ) (hD : 0 < D)
    (hf : ∀ m : ℕ, ∀ k : ℕ, k < 2 ^ m →
      |f ((k + 1 : ℝ) / (2 : ℝ) ^ m) - f ((k : ℝ) / (2 : ℝ) ^ m)| ≤
        D * (2 : ℝ) ^ (-(m : ℝ) * γ))
    {q r : ℝ} (hq : q ∈ dyadicRationals ∩ Set.Icc 0 1)
    (hr : r ∈ dyadicRationals ∩ Set.Icc 0 1) :
    |f q - f r| ≤ D * (4 + 2 * (2 : ℝ) ^ (-γ) / (1 - (2 : ℝ) ^ (-γ))) * |q - r| ^ γ

Uses 1 · Used by 1

Statement usesDyadic rationals

Used byAlmost sure Hölder bound on the dyadic rationals

TheoremAlmost sure Hölder bound on the dyadic rationals#✓fully proved

A single full-measure set carries a Hölder bound for the original process on the dyadic rationals of [0, 1]. The moment-integrability correction in the module docstring is required for this Bochner formulation.

theorem kolmogorov_ae_holder_on_dyadics {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
    [IsProbabilityMeasure μ] {X : ℝ → Ω → ℝ} {α β K : ℝ} (_hα : 0 < α) (hβ : 0 < β)
    (hK : 0 ≤ K)
    (hX_int : ∀ s t : ℝ, Integrable (fun ω => |X s ω - X t ω| ^ β) μ)
    (hkolm : ∀ s t : ℝ, ∫ ω, |X s ω - X t ω| ^ β ∂μ ≤ K * |s - t| ^ (1 + α)) :
    ∀ γ : ℝ, γ < α / β → γ > 0 →
      ∀ᵐ ω ∂μ, ∃ C : ℝ, 0 < C ∧
        ∀ q r : ℝ, q ∈ dyadicRationals ∩ Set.Icc 0 1 →
          r ∈ dyadicRationals ∩ Set.Icc 0 1 →
          |X q ω - X r ω| ≤ C * |q - r| ^ γ

Uses 2 · Used by 2

Statement usesDyadic rationals

Proof usesDeterministic chaining

Used byHölder bound on dyadics for a Kolmogorov process · Kolmogorov continuity theorem

TheoremKolmogorov continuity theorem#✓fully proved

Kolmogorov continuity theorem, in the original modification formulation. The direct dyadic bound permits choosing Y = X. See the module docstring for the necessary moment-integrability correction to the archived v1 statement.

theorem kolmogorov_continuity_theorem {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
    [IsProbabilityMeasure μ] {X : ℝ → Ω → ℝ} {α β K : ℝ} (_hα : 0 < α) (hβ : 0 < β)
    (hK : 0 ≤ K)
    (hX_int : ∀ s t : ℝ, Integrable (fun ω => |X s ω - X t ω| ^ β) μ)
    (hkolm : ∀ s t : ℝ, ∫ ω, |X s ω - X t ω| ^ β ∂μ ≤ K * |s - t| ^ (1 + α)) :
    ∀ γ : ℝ, γ < α / β → γ > 0 →
      ∃ Y : ℝ → Ω → ℝ,
        (∀ t, ∀ᵐ ω ∂μ, Y t ω = X t ω) ∧
        (∀ᵐ ω ∂μ, ∃ C : ℝ, 0 < C ∧
          ∀ q r : ℝ, q ∈ dyadicRationals ∩ Set.Icc 0 1 →
            r ∈ dyadicRationals ∩ Set.Icc 0 1 →
            |Y q ω - Y r ω| ≤ C * |q - r| ^ γ)

Uses 2

Statement usesDyadic rationals

Proof usesAlmost sure Hölder bound on the dyadic rationals

TheoremHölder bound on dyadics for a Kolmogorov process#✓fully proved

The canonical Kolmogorov-process condition implies a common a.e. Hölder bound for X on the dyadics of [0, 1]. Its measurable-pair and finite lintegral fields supply the Bochner hypotheses internally, including when M = 0. No claim is made about the raw paths at every real time.

theorem kolmogorov_ae_holder_on_dyadics_of_isKolmogorovProcess
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    {X : ℝ → Ω → ℝ} {α β : ℝ} {M : NNReal} (hα : 0 < α)
    (hX : ProbabilityTheory.IsKolmogorovProcess X μ β (1 + α) M) :
    ∀ γ : ℝ, γ < α / β → γ > 0 →
      ∀ᵐ ω ∂μ, ∃ C : ℝ, 0 < C ∧
        ∀ q r : ℝ, q ∈ dyadicRationals ∩ Set.Icc 0 1 →
          r ∈ dyadicRationals ∩ Set.Icc 0 1 →
          |X q ω - X r ω| ≤ C * |q - r| ^ γ

Uses 2 · Used by 1

Statement usesDyadic rationals

Proof usesAlmost sure Hölder bound on the dyadic rationals

Used byKolmogorov continuous-modification theorem for real-valued processes

TheoremKolmogorov continuous-modification theorem for real-valued processes#✓fully proved

A real-valued Kolmogorov process on NNReal whose time exponent is greater than one has one modification with measurable coordinates and continuous paths on every sample. The same modification agrees exactly at time zero and preserves every closed set containing an original sample path. Fixed-time almost-everywhere equality is asserted separately at each time; no indistinguishability claim is made for the raw process.

theorem exists_continuous_modification {Ω : Type*} [MeasurableSpace Ω]
    {P : Measure Ω} [IsProbabilityMeasure P] {X : NNReal → Ω → ℝ}
    {p q : ℝ} {M : NNReal}
    (hX : ProbabilityTheory.IsKolmogorovProcess X P p q M) (hq : 1 < q) :
    ∃ Y : NNReal → Ω → ℝ,
      (∀ t, Measurable (Y t)) ∧
      (∀ ω, Continuous fun t => Y t ω) ∧
      (∀ t, Y t =ᵐ[P] X t) ∧
      (∀ ω, Y 0 ω = X 0 ω) ∧
      (∀ S : Set ℝ, IsClosed S → ∀ ω, (∀ s, X s ω ∈ S) → ∀ t, Y t ω ∈ S)

Uses 2 · Used by 1

Proof usesDyadic rationals · Hölder bound on dyadics for a Kolmogorov process

Used byContinuous modification selected by Kolmogorov's theorem

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.