# mathlibdocumentation

topology.metric_space.holder

# 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 #

• holder_on_with: 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;
• holder_with: 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 holder_with {X : Type u_1} {Y : Type u_2} (C r : ℝ≥0) (f : X → Y) :
Prop

A function f : X → Y between two pseudo_emetric_spaces 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
def holder_on_with {X : Type u_1} {Y : Type u_2} (C r : ℝ≥0) (f : X → Y) (s : set X) :
Prop

A function f : X → Y between two pseudo_emeteric_spaces 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
@[simp]
theorem holder_on_with_empty {X : Type u_1} {Y : Type u_2} (C r : ℝ≥0) (f : X → Y) :
f
@[simp]
theorem holder_on_with_singleton {X : Type u_1} {Y : Type u_2} (C r : ℝ≥0) (f : X → Y) (x : X) :
f {x}
theorem set.subsingleton.holder_on_with {X : Type u_1} {Y : Type u_2} {s : set X} (hs : s.subsingleton) (C r : ℝ≥0) (f : X → Y) :
f s
theorem holder_on_with_univ {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} :
f set.univ r f
@[simp]
theorem holder_on_with_one {X : Type u_1} {Y : Type u_2} {C : ℝ≥0} {f : X → Y} {s : set X} :
f s s
theorem lipschitz_on_with.holder_on_with {X : Type u_1} {Y : Type u_2} {C : ℝ≥0} {f : X → Y} {s : set X} :
s f s

Alias of holder_on_with_one.

@[simp]
theorem holder_with_one {X : Type u_1} {Y : Type u_2} {C : ℝ≥0} {f : X → Y} :
1 f
theorem lipschitz_with.holder_with {X : Type u_1} {Y : Type u_2} {C : ℝ≥0} {f : X → Y} :
1 f

Alias of holder_with_one.

theorem holder_with_id {X : Type u_1}  :
1 id
theorem holder_with.holder_on_with {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} (h : r f) (s : set X) :
f s
theorem holder_on_with.edist_le {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} {s : set X} (h : f s) {x y : X} (hx : x s) (hy : y s) :
edist (f x) (f y) (C) * y ^ r
theorem holder_on_with.edist_le_of_le {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} {s : set X} (h : f s) {x y : X} (hx : x s) (hy : y s) {d : ℝ≥0∞} (hd : y d) :
edist (f x) (f y) (C) * d ^ r
theorem holder_on_with.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {s : set X} {Cg rg : ℝ≥0} {g : Y → Z} {t : set Y} (hg : rg g t) {Cf rf : ℝ≥0} {f : X → Y} (hf : rf f s) (hst : s t) :
holder_on_with (Cg * Cf ^ rg) (rg * rf) (g f) s
theorem holder_on_with.comp_holder_with {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {Cg rg : ℝ≥0} {g : Y → Z} {t : set Y} (hg : rg g t) {Cf rf : ℝ≥0} {f : X → Y} (hf : rf f) (ht : ∀ (x : X), f x t) :
holder_with (Cg * Cf ^ rg) (rg * rf) (g f)
theorem holder_on_with.uniform_continuous_on {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} {s : set X} (hf : f s) (h0 : 0 < r) :

A Hölder continuous function is uniformly continuous

theorem holder_on_with.continuous_on {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} {s : set X} (hf : f s) (h0 : 0 < r) :
theorem holder_on_with.mono {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} {s t : set X} (hf : f s) (ht : t s) :
f t
theorem holder_on_with.ediam_image_le_of_le {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} {s : set X} (hf : f s) {d : ℝ≥0∞} (hd : d) :
emetric.diam (f '' s) (C) * d ^ r
theorem holder_on_with.ediam_image_le {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} {s : set X} (hf : f s) :
emetric.diam (f '' s) (C) *
theorem holder_on_with.ediam_image_le_of_subset {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} {s t : set X} (hf : f s) (ht : t s) :
emetric.diam (f '' t) (C) *
theorem holder_on_with.ediam_image_le_of_subset_of_le {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} {s t : set X} (hf : f s) (ht : t s) {d : ℝ≥0∞} (hd : d) :
emetric.diam (f '' t) (C) * d ^ r
theorem holder_on_with.ediam_image_inter_le_of_le {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} {s t : set X} (hf : f s) {d : ℝ≥0∞} (hd : d) :
emetric.diam (f '' (t s)) (C) * d ^ r
theorem holder_on_with.ediam_image_inter_le {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} {s : set X} (hf : f s) (t : set X) :
emetric.diam (f '' (t s)) (C) *
theorem holder_with.edist_le {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} (h : r f) (x y : X) :
edist (f x) (f y) (C) * y ^ r
theorem holder_with.edist_le_of_le {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} (h : r f) {x y : X} {d : ℝ≥0∞} (hd : y d) :
edist (f x) (f y) (C) * d ^ r
theorem holder_with.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {Cg rg : ℝ≥0} {g : Y → Z} (hg : rg g) {Cf rf : ℝ≥0} {f : X → Y} (hf : rf f) :
holder_with (Cg * Cf ^ rg) (rg * rf) (g f)
theorem holder_with.comp_holder_on_with {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {Cg rg : ℝ≥0} {g : Y → Z} (hg : rg g) {Cf rf : ℝ≥0} {f : X → Y} {s : set X} (hf : rf f s) :
holder_on_with (Cg * Cf ^ rg) (rg * rf) (g f) s
theorem holder_with.uniform_continuous {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} (hf : r f) (h0 : 0 < r) :

A Hölder continuous function is uniformly continuous

theorem holder_with.continuous {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} (hf : r f) (h0 : 0 < r) :
theorem holder_with.ediam_image_le {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} (hf : r f) (s : set X) :
emetric.diam (f '' s) (C) *
theorem holder_with.nndist_le_of_le {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} (hf : r f) {x y : X} {d : ℝ≥0} (hd : y d) :
nndist (f x) (f y) C * d ^ r
theorem holder_with.nndist_le {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} (hf : r f) (x y : X) :
nndist (f x) (f y) C * y ^ r
theorem holder_with.dist_le_of_le {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} (hf : r f) {x y : X} {d : } (hd : dist x y d) :
dist (f x) (f y) (C) * d ^ r
theorem holder_with.dist_le {X : Type u_1} {Y : Type u_2} {C r : ℝ≥0} {f : X → Y} (hf : r f) (x y : X) :
dist (f x) (f y) (C) * dist x y ^ r