Almost-Everywhere Dyadic Increment Bound

This is the almost-sure dyadic increment estimate for a Kolmogorov process. Let $(\Omega,P)$ be a probability space, $X:\mathbb R\to\Omega\to\mathbb R$, $p,q\in\mathbb R$, $M\in\mathbb R_{\ge0}$, and assume IsKolmogorovProcess X P p q M. If $\alpha p<q-1$, then for $P$-almost every $\omega$ there exists $N\in\mathbb N$ such that for every $n\ge N$ and every integer $k$ with $0\le k$ and $k+1\le2^n$,

This is the probabilistic input for dyadic_holder_chaining_readable.

Original Lean declaration header

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

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

Module navigation

Module: LevyStochCalc/Brownian/ContinuityKolmogorovBounds.

Supporting theorems: kc_level_bad_measure.

Previous: exists_tendsto_of_local_holder · Next: kc_ae_interval_holder.

Source excerpt, lines 227–234 · Frozen source 408915f.