Almost-Sure Local Hölder Bounds on Unit Intervals

This is the almost-sure intervalwise Hölder estimate for a Kolmogorov process. Under the probability-space, process, and IsKolmogorovProcess assumptions above, let $\alpha>0$ satisfy $\alpha p<q-1$. Then for $P$-almost every $\omega$, every integer $j$ admits $K\ge0$ and $N\in\mathbb N$ such that for dyadic rationals $s,t\in[j,j+1]$ with $|s-t|\le(1/2)^N$,

The constants may depend on the path and on the interval index $j$.

Original Lean declaration header

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

lemma kc_ae_interval_holder
    (P : Measure Ω) [IsProbabilityMeasure P]
    (X : ℝ → Ω → ℝ) {p q : ℝ} {M : ℝ≥0}
    (hX : ProbabilityTheory.IsKolmogorovProcess X P p q M)
    {α : ℝ} (hα0 : 0 < α) (hαpq : α * p < q - 1) :
    ∀ᵐ ω ∂P, ∀ j : ℤ, ∃ (K : ℝ) (N : ℕ), 0 ≤ K ∧
      ∀ s ∈ dyadicRationals, ∀ t ∈ dyadicRationals,
        (j : ℝ) ≤ s → s ≤ (j : ℝ) + 1 → (j : ℝ) ≤ t → t ≤ (j : ℝ) + 1 →
        |s - t| ≤ (1 / 2 : ℝ) ^ N → |X s ω - X t ω| ≤ K * |s - t| ^ α

Module navigation

Module: LevyStochCalc/Brownian/ContinuityKolmogorovBounds.

Definition modules: LevyStochCalc/Brownian/ContinuityDyadicChaining.

Supporting theorems: dyadic_holder_chaining, kc_ae_increment_bound.

Previous: kc_ae_increment_bound · Next: kc_ae_nbhd_holder.

Source excerpt, lines 276–284 · Frozen source 408915f.