Limit Existence from Local Hölder Control

Let A ⊆ ℝ be dense, f : ℝ → ℝ, α > 0, and t : ℝ. Suppose there exist ρ > 0 and K ≥ 0 such that for all s, s′ ∈ A lying in (t−ρ,t+ρ),

Then there exists y : ℝ such that f tends to y along the neighborhood filter 𝓝[A] t:

The lemma exists_tendsto_of_local_holder_readable is a deterministic extension ingredient: local Hölder control on a dense set ensures existence of the limit needed to define a continuous extension.

Original Lean declaration header

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

lemma exists_tendsto_of_local_holder {A : Set ℝ} (hA : Dense A) {f : ℝ → ℝ}
    {α : ℝ} (hα : 0 < α) (t : ℝ)
    (hloc : ∃ K ρ : ℝ, 0 < ρ ∧ 0 ≤ K ∧ ∀ s ∈ A, ∀ s' ∈ A,
      s ∈ Set.Ioo (t - ρ) (t + ρ) → s' ∈ Set.Ioo (t - ρ) (t + ρ) →
        |f s - f s'| ≤ K * |s - s'| ^ α) :
    ∃ y, Filter.Tendsto f (𝓝[A] t) (nhds y)

Module navigation

Module: LevyStochCalc/Brownian/ContinuityKolmogorovBounds.

Previous: kc_level_bad_measure · Next: kc_ae_increment_bound.

Source excerpt, lines 148–153 · Frozen source 408915f.