Hölder functions: a dist criterion and extension from a dense set

A Hölder bound stated with dist is equivalent to HolderOnWith, which Mathlib phrases with edist.

A function which is Hölder continuous, with positive exponent, on a dense subset s of a pseudo-emetric space and takes values in a complete emetric space extends to a function which is Hölder continuous on the whole space, with the same constant and exponent.

The extension is the uniformly continuous extension along the dense inclusion s → X, and the Hölder inequality passes from s × s to its closure because both of its sides are continuous.

This is how an almost-everywhere Hölder estimate becomes a Hölder continuous representative: a set of full measure for a measure that is positive on open sets is dense.

Main declarations

• HolderOnWith.of_dist_le: a Hölder bound stated with dist gives HolderOnWith; the converse is Mathlib's HolderOnWith.dist_le.
• holderOnWith_iff_dist_le: HolderOnWith is equivalent to the Hölder bound stated with dist.
• HolderOnWith.extend_of_dense: a Hölder function on a dense set extends to a Hölder function on the whole space.

theorem HolderOnWith.extend_of_dense {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [EMetricSpace Y] [CompleteSpace Y] {C r : NNReal} {f : X → Y} {s : Set X} (hf : HolderOnWith C r f s) (hr : 0 < r) (hs : Dense s) : ∃ (g : X → Y), HolderWith C r g ∧ Set.EqOn f g s

Hölder functions extend from dense sets. If f is Hölder continuous with constant C and positive exponent r on a dense set s, and the target is complete, then some function which is Hölder continuous with constant C and exponent r on the whole space agrees with f on s. Compare LipschitzOnWith.extend_real, which needs no density but only applies to real values.

theorem HolderOnWith.of_dist_le {X : Type u_3} {Y : Type u_4} [PseudoMetricSpace X] [PseudoMetricSpace Y] {C r : NNReal} {f : X → Y} {s : Set X} (h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑C * dist x y ^ ↑r) : HolderOnWith C r f s

A Hölder bound stated with dist gives HolderOnWith, which is phrased with edist. This is the converse of HolderOnWith.dist_le.

theorem holderOnWith_iff_dist_le {X : Type u_3} {Y : Type u_4} [PseudoMetricSpace X] [PseudoMetricSpace Y] {C r : NNReal} {f : X → Y} {s : Set X} : HolderOnWith C r f s ↔ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑C * dist x y ^ ↑r

HolderOnWith is equivalent to the Hölder bound stated with dist. Compare lipschitzOnWith_iff_dist_le_mul.