Deterministic Dyadic Hölder Chaining

This is the deterministic dyadic Hölder-chaining lemma. Let $f:\mathbb R\to\mathbb R$, $\alpha,C\in\mathbb R$, and $N\in\mathbb N$, with $\alpha>0$ and $C\ge0$. Assume that for every $n\ge N$, every integer $k$ with $0\le k$ and $k+1\le2^n$, the consecutive dyadic increment satisfies

Then there exists $K\ge0$ such that for all dyadic rationals $s,t\in[0,1]$ with $|s-t|\le(1/2)^N$,

This supplies the deterministic pathwise estimate used after obtaining eventual dyadic increment bounds.

Original Lean declaration header

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

lemma dyadic_holder_chaining {f : ℝ → ℝ} {α C : ℝ} {N : ℕ}
    (hα : 0 < α) (hC : 0 ≤ C)
    (hf : ∀ n, N ≤ n → ∀ k : ℤ, 0 ≤ k → k + 1 ≤ 2 ^ n →
      |f ((k + 1 : ℤ) / 2 ^ n) - f ((k : ℤ) / 2 ^ n)| ≤ C * ((1 / 2 : ℝ) ^ α) ^ n) :
    ∃ K : ℝ, 0 ≤ K ∧ ∀ s ∈ dyadicRationals, ∀ t ∈ dyadicRationals,
      0 ≤ s → s ≤ 1 → 0 ≤ t → t ≤ 1 → |s - t| ≤ (1 / 2 : ℝ) ^ N →
      |f s - f t| ≤ K * |s - t| ^ α

Module navigation

Module: LevyStochCalc/Brownian/ContinuityDyadicChaining.

Supporting theorems: dyadicTrunc_eventually_eq, dyadicTrunc_near_step, dyadicTrunc_telescope, exists_dyadic_scale, rpow_half_pow_le.

Previous: kc_exponent_identity.

Source excerpt, lines 407–413 · Frozen source 408915f.