A.e. limits with a common Hölder bound have a continuous representative

Proved

MeasureTheory.exists_holder_representative_of_ae_tendsto

by Mazecto · Oct 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

holder-spacesmeasure-theorymetric-spaces

Let $X$ and $Y$ be metric spaces with $Y$ complete, and let $\mu$ be a measure on $X$ that is positive on every nonempty open set. Suppose $v_j:X\to Y$ converges almost everywhere to $f$ , and for fixed $K\ge0$ and $\alpha>0$ every $v_j$ satisfies $d(v_j(x),v_j(y))\le Kd(x,y)^\alpha$ . Then $f$ has a continuous representative with the same Hölder bound. No measurability or continuity assumption on the approximating functions is required. The proof takes limits on the conull dense set and extends uniformly continuously.

Preamble

import Mathlib.Topology.MetricSpace.Holder
import Mathlib.Topology.UniformSpace.UniformEmbedding
import Mathlib.MeasureTheory.Measure.OpenPos

open MeasureTheory Filter Set
open scoped Topology NNReal ENNReal

Formal statement

theorem MeasureTheory.exists_holder_representative_of_ae_tendsto {X Y : Type*} [MetricSpace X] [MetricSpace Y] [CompleteSpace Y]
    [MeasurableSpace X] (μ : Measure X) [μ.IsOpenPosMeasure]
    (K : ℝ≥0) (α : ℝ) (hα : 0 < α) (v : ℕ → X → Y) (f : X → Y)
    (hv : ∀ j x y, dist (v j x) (v j y) ≤ (K : ℝ) * dist x y ^ α)
    (hf : ∀ᵐ x ∂μ, Tendsto (fun j => v j x) atTop (𝓝 (f x))) :
    ∃ u : X → Y, Continuous u ∧ u =ᵐ[μ] f ∧
      ∀ x y, dist (u x) (u y) ≤ (K : ℝ) * dist x y ^ α := by sorry

Source

Hunter, Notes on Partial Differential Equations (revised 6/18/2014), https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf, printed pp. 68–70, Theorems 3.36–3.37; homogeneous mollification and dense-set extension in the proof of Theorem 3.37.

View graph