# Hölder continuous functions #

In this file we define Hölder continuity on a set and on the whole space. We also prove some basic properties of Hölder continuous functions.

## Main definitions #

• HolderOnWith: f : X → Y is said to be Hölder continuous with constant C : ℝ≥0 and exponent r : ℝ≥0 on a set s, if edist (f x) (f y) ≤ C * edist x y ^ r for all x y ∈ s;
• HolderWith: f : X → Y is said to be Hölder continuous with constant C : ℝ≥0 and exponent r : ℝ≥0, if edist (f x) (f y) ≤ C * edist x y ^ r for all x y : X.

## Implementation notes #

We use the type ℝ≥0 (a.k.a. NNReal) for C because this type has coercion both to ℝ and ℝ≥0∞, so it can be easily used both in inequalities about dist and edist. We also use ℝ≥0 for r to ensure that d ^ r is monotone in d. It might be a good idea to use ℝ>0 for r but we don't have this type in mathlib (yet).

## Tags #

Hölder continuity, Lipschitz continuity

def HolderWith {X : Type u_1} {Y : Type u_2} (C : NNReal) (r : NNReal) (f : XY) :

A function f : X → Y between two PseudoEMetricSpaces is Hölder continuous with constant C : ℝ≥0 and exponent r : ℝ≥0, if edist (f x) (f y) ≤ C * edist x y ^ r for all x y : X.

Equations
Instances For
def HolderOnWith {X : Type u_1} {Y : Type u_2} (C : NNReal) (r : NNReal) (f : XY) (s : Set X) :

A function f : X → Y between two PseudoEMetricSpaces is Hölder continuous with constant C : ℝ≥0 and exponent r : ℝ≥0 on a set s : Set X, if edist (f x) (f y) ≤ C * edist x y ^ r for all x y ∈ s.

Equations
Instances For
@[simp]
theorem holderOnWith_empty {X : Type u_1} {Y : Type u_2} (C : NNReal) (r : NNReal) (f : XY) :
@[simp]
theorem holderOnWith_singleton {X : Type u_1} {Y : Type u_2} (C : NNReal) (r : NNReal) (f : XY) (x : X) :
HolderOnWith C r f {x}
theorem Set.Subsingleton.holderOnWith {X : Type u_1} {Y : Type u_2} {s : Set X} (hs : ) (C : NNReal) (r : NNReal) (f : XY) :
HolderOnWith C r f s
theorem holderOnWith_univ {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} :
HolderOnWith C r f Set.univ HolderWith C r f
@[simp]
theorem holderOnWith_one {X : Type u_1} {Y : Type u_2} {C : NNReal} {f : XY} {s : Set X} :
HolderOnWith C 1 f s
theorem LipschitzOnWith.holderOnWith {X : Type u_1} {Y : Type u_2} {C : NNReal} {f : XY} {s : Set X} :
HolderOnWith C 1 f s

Alias of the reverse direction of holderOnWith_one.

@[simp]
theorem holderWith_one {X : Type u_1} {Y : Type u_2} {C : NNReal} {f : XY} :
theorem LipschitzWith.holderWith {X : Type u_1} {Y : Type u_2} {C : NNReal} {f : XY} :
HolderWith C 1 f

Alias of the reverse direction of holderWith_one.

theorem holderWith_id {X : Type u_1} :
HolderWith 1 1 id
theorem HolderWith.holderOnWith {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} (h : HolderWith C r f) (s : Set X) :
HolderOnWith C r f s
theorem HolderOnWith.edist_le {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} {s : Set X} (h : HolderOnWith C r f s) {x : X} {y : X} (hx : x s) (hy : y s) :
edist (f x) (f y) C * edist x y ^ r
theorem HolderOnWith.edist_le_of_le {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} {s : Set X} (h : HolderOnWith C r f s) {x : X} {y : X} (hx : x s) (hy : y s) {d : ENNReal} (hd : edist x y d) :
edist (f x) (f y) C * d ^ r
theorem HolderOnWith.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {s : Set X} {Cg : NNReal} {rg : NNReal} {g : YZ} {t : Set Y} (hg : HolderOnWith Cg rg g t) {Cf : NNReal} {rf : NNReal} {f : XY} (hf : HolderOnWith Cf rf f s) (hst : Set.MapsTo f s t) :
HolderOnWith (Cg * NNReal.rpow Cf rg) (rg * rf) (g f) s
theorem HolderOnWith.comp_holderWith {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {Cg : NNReal} {rg : NNReal} {g : YZ} {t : Set Y} (hg : HolderOnWith Cg rg g t) {Cf : NNReal} {rf : NNReal} {f : XY} (hf : HolderWith Cf rf f) (ht : ∀ (x : X), f x t) :
HolderWith (Cg * NNReal.rpow Cf rg) (rg * rf) (g f)
theorem HolderOnWith.uniformContinuousOn {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} {s : Set X} (hf : HolderOnWith C r f s) (h0 : 0 < r) :

A Hölder continuous function is uniformly continuous

theorem HolderOnWith.continuousOn {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} {s : Set X} (hf : HolderOnWith C r f s) (h0 : 0 < r) :
theorem HolderOnWith.mono {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} {s : Set X} {t : Set X} (hf : HolderOnWith C r f s) (ht : t s) :
HolderOnWith C r f t
theorem HolderOnWith.ediam_image_le_of_le {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} {s : Set X} (hf : HolderOnWith C r f s) {d : ENNReal} (hd : ) :
EMetric.diam (f '' s) C * d ^ r
theorem HolderOnWith.ediam_image_le {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} {s : Set X} (hf : HolderOnWith C r f s) :
EMetric.diam (f '' s) C * ^ r
theorem HolderOnWith.ediam_image_le_of_subset {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} {s : Set X} {t : Set X} (hf : HolderOnWith C r f s) (ht : t s) :
EMetric.diam (f '' t) C * ^ r
theorem HolderOnWith.ediam_image_le_of_subset_of_le {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} {s : Set X} {t : Set X} (hf : HolderOnWith C r f s) (ht : t s) {d : ENNReal} (hd : ) :
EMetric.diam (f '' t) C * d ^ r
theorem HolderOnWith.ediam_image_inter_le_of_le {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} {s : Set X} {t : Set X} (hf : HolderOnWith C r f s) {d : ENNReal} (hd : ) :
EMetric.diam (f '' (t s)) C * d ^ r
theorem HolderOnWith.ediam_image_inter_le {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} {s : Set X} (hf : HolderOnWith C r f s) (t : Set X) :
EMetric.diam (f '' (t s)) C * ^ r
theorem HolderWith.edist_le {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} (h : HolderWith C r f) (x : X) (y : X) :
edist (f x) (f y) C * edist x y ^ r
theorem HolderWith.edist_le_of_le {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} (h : HolderWith C r f) {x : X} {y : X} {d : ENNReal} (hd : edist x y d) :
edist (f x) (f y) C * d ^ r
theorem HolderWith.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {Cg : NNReal} {rg : NNReal} {g : YZ} (hg : HolderWith Cg rg g) {Cf : NNReal} {rf : NNReal} {f : XY} (hf : HolderWith Cf rf f) :
HolderWith (Cg * NNReal.rpow Cf rg) (rg * rf) (g f)
theorem HolderWith.comp_holderOnWith {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {Cg : NNReal} {rg : NNReal} {g : YZ} (hg : HolderWith Cg rg g) {Cf : NNReal} {rf : NNReal} {f : XY} {s : Set X} (hf : HolderOnWith Cf rf f s) :
HolderOnWith (Cg * NNReal.rpow Cf rg) (rg * rf) (g f) s
theorem HolderWith.uniformContinuous {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} (hf : HolderWith C r f) (h0 : 0 < r) :

A Hölder continuous function is uniformly continuous

theorem HolderWith.continuous {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} (hf : HolderWith C r f) (h0 : 0 < r) :
theorem HolderWith.ediam_image_le {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} (hf : HolderWith C r f) (s : Set X) :
EMetric.diam (f '' s) C * ^ r
theorem HolderWith.nndist_le_of_le {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} (hf : HolderWith C r f) {x : X} {y : X} {d : NNReal} (hd : nndist x y d) :
nndist (f x) (f y) C * d ^ r
theorem HolderWith.nndist_le {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} (hf : HolderWith C r f) (x : X) (y : X) :
nndist (f x) (f y) C * nndist x y ^ r
theorem HolderWith.dist_le_of_le {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} (hf : HolderWith C r f) {x : X} {y : X} {d : } (hd : dist x y d) :
dist (f x) (f y) C * d ^ r
theorem HolderWith.dist_le {X : Type u_1} {Y : Type u_2} {C : NNReal} {r : NNReal} {f : XY} (hf : HolderWith C r f) (x : X) (y : X) :
dist (f x) (f y) C * dist x y ^ r