mathlib3 documentation

topology.metric_space.holder

Hölder continuous functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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} [pseudo_emetric_space X] [pseudo_emetric_space Y] (C r : nnreal) (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} [pseudo_emetric_space X] [pseudo_emetric_space Y] (C r : nnreal) (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} [pseudo_emetric_space X] [pseudo_emetric_space Y] (C r : nnreal) (f : X Y) :
@[simp]
theorem holder_on_with_singleton {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] (C r : nnreal) (f : X Y) (x : X) :
holder_on_with C r f {x}
theorem set.subsingleton.holder_on_with {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {s : set X} (hs : s.subsingleton) (C r : nnreal) (f : X Y) :
theorem holder_on_with_univ {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} :
@[simp]
theorem holder_on_with_one {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C : nnreal} {f : X Y} {s : set X} :
theorem lipschitz_on_with.holder_on_with {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C : nnreal} {f : X Y} {s : set X} :

Alias of the reverse direction of holder_on_with_one.

@[simp]
theorem holder_with_one {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C : nnreal} {f : X Y} :
theorem lipschitz_with.holder_with {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C : nnreal} {f : X Y} :

Alias of the reverse direction of holder_with_one.

@[protected]
theorem holder_with.holder_on_with {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} (h : holder_with C r f) (s : set X) :
theorem holder_on_with.edist_le {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} {s : set X} (h : holder_on_with C r f s) {x y : X} (hx : x s) (hy : y s) :
theorem holder_on_with.edist_le_of_le {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} {s : set X} (h : holder_on_with C r f s) {x y : X} (hx : x s) (hy : y s) {d : ennreal} (hd : has_edist.edist x y d) :
has_edist.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} [pseudo_emetric_space X] [pseudo_emetric_space Y] [pseudo_emetric_space Z] {s : set X} {Cg rg : nnreal} {g : Y Z} {t : set Y} (hg : holder_on_with Cg rg g t) {Cf rf : nnreal} {f : X Y} (hf : holder_on_with Cf rf f s) (hst : set.maps_to f 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} [pseudo_emetric_space X] [pseudo_emetric_space Y] [pseudo_emetric_space Z] {Cg rg : nnreal} {g : Y Z} {t : set Y} (hg : holder_on_with Cg rg g t) {Cf rf : nnreal} {f : X Y} (hf : holder_with Cf rf f) (ht : (x : X), f x t) :
holder_with (Cg * Cf ^ rg) (rg * rf) (g f)
@[protected]
theorem holder_on_with.uniform_continuous_on {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} {s : set X} (hf : holder_on_with C r f s) (h0 : 0 < r) :

A Hölder continuous function is uniformly continuous

@[protected]
theorem holder_on_with.continuous_on {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} {s : set X} (hf : holder_on_with C r f s) (h0 : 0 < r) :
@[protected]
theorem holder_on_with.mono {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} {s t : set X} (hf : holder_on_with C r f s) (ht : t s) :
theorem holder_on_with.ediam_image_le_of_le {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} {s : set X} (hf : holder_on_with C r f s) {d : ennreal} (hd : emetric.diam s d) :
theorem holder_on_with.ediam_image_le {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} {s : set X} (hf : holder_on_with C r f s) :
theorem holder_on_with.ediam_image_le_of_subset {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} {s t : set X} (hf : holder_on_with C r f s) (ht : t s) :
theorem holder_on_with.ediam_image_le_of_subset_of_le {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} {s t : set X} (hf : holder_on_with C r f s) (ht : t s) {d : ennreal} (hd : emetric.diam t d) :
theorem holder_on_with.ediam_image_inter_le_of_le {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} {s t : set X} (hf : holder_on_with C r f s) {d : ennreal} (hd : emetric.diam t 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} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} {s : set X} (hf : holder_on_with C r f s) (t : set X) :
theorem holder_with.edist_le {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} (h : holder_with C r f) (x y : X) :
theorem holder_with.edist_le_of_le {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} (h : holder_with C r f) {x y : X} {d : ennreal} (hd : has_edist.edist x y d) :
has_edist.edist (f x) (f y) C * d ^ r
theorem holder_with.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [pseudo_emetric_space X] [pseudo_emetric_space Y] [pseudo_emetric_space Z] {Cg rg : nnreal} {g : Y Z} (hg : holder_with Cg rg g) {Cf rf : nnreal} {f : X Y} (hf : holder_with Cf 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} [pseudo_emetric_space X] [pseudo_emetric_space Y] [pseudo_emetric_space Z] {Cg rg : nnreal} {g : Y Z} (hg : holder_with Cg rg g) {Cf rf : nnreal} {f : X Y} {s : set X} (hf : holder_on_with Cf rf f s) :
holder_on_with (Cg * Cf ^ rg) (rg * rf) (g f) s
@[protected]
theorem holder_with.uniform_continuous {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} (hf : holder_with C r f) (h0 : 0 < r) :

A Hölder continuous function is uniformly continuous

@[protected]
theorem holder_with.continuous {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} (hf : holder_with C r f) (h0 : 0 < r) :
theorem holder_with.ediam_image_le {X : Type u_1} {Y : Type u_2} [pseudo_emetric_space X] [pseudo_emetric_space Y] {C r : nnreal} {f : X Y} (hf : holder_with C r f) (s : set X) :
theorem holder_with.nndist_le_of_le {X : Type u_1} {Y : Type u_2} [pseudo_metric_space X] [pseudo_metric_space Y] {C r : nnreal} {f : X Y} (hf : holder_with C r f) {x y : X} {d : nnreal} (hd : has_nndist.nndist x y d) :
has_nndist.nndist (f x) (f y) C * d ^ r
theorem holder_with.nndist_le {X : Type u_1} {Y : Type u_2} [pseudo_metric_space X] [pseudo_metric_space Y] {C r : nnreal} {f : X Y} (hf : holder_with C r f) (x y : X) :
theorem holder_with.dist_le_of_le {X : Type u_1} {Y : Type u_2} [pseudo_metric_space X] [pseudo_metric_space Y] {C r : nnreal} {f : X Y} (hf : holder_with C r f) {x y : X} {d : } (hd : has_dist.dist x y d) :
has_dist.dist (f x) (f y) C * d ^ r
theorem holder_with.dist_le {X : Type u_1} {Y : Type u_2} [pseudo_metric_space X] [pseudo_metric_space Y] {C r : nnreal} {f : X Y} (hf : holder_with C r f) (x y : X) :