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 #
holder_on_with:f : X → Yis said to be Hölder continuous with constantC : ℝ≥0and exponentr : ℝ≥0on a sets, ifedist (f x) (f y) ≤ C * edist x y ^ rfor allx y ∈ s;holder_with:f : X → Yis said to be Hölder continuous with constantC : ℝ≥0and exponentr : ℝ≥0, ifedist (f x) (f y) ≤ C * edist x y ^ rfor allx 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}
[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
- holder_with C r f = ∀ (x y : X), has_edist.edist (f x) (f y) ≤ ↑C * has_edist.edist x y ^ ↑r
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
- holder_on_with C r f s = ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ s → has_edist.edist (f x) (f y) ≤ ↑C * has_edist.edist x y ^ ↑r
@[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) :
holder_on_with C r f ∅
@[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) :
holder_on_with C r f s
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} :
holder_on_with C r f set.univ ↔ holder_with C r f
@[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} :
holder_on_with C 1 f s ↔ lipschitz_on_with C f s
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} :
lipschitz_on_with C f s → holder_on_with C 1 f s
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} :
holder_with C 1 f ↔ lipschitz_with C f
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} :
lipschitz_with C f → holder_with C 1 f
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) :
holder_on_with C r f s
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) :
has_edist.edist (f x) (f y) ≤ ↑C * has_edist.edist x y ^ ↑r
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) :
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) :
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) :
@[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) :
continuous_on f s
@[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) :
holder_on_with C r f t
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) :
emetric.diam (f '' s) ≤ ↑C * emetric.diam s ^ ↑r
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) :
emetric.diam (f '' t) ≤ ↑C * emetric.diam t ^ ↑r
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) :
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) :
emetric.diam (f '' (t ∩ s)) ≤ ↑C * emetric.diam t ^ ↑r
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) :
has_edist.edist (f x) (f y) ≤ ↑C * has_edist.edist x y ^ ↑r
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) :
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) :
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) :
@[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) :
emetric.diam (f '' s) ≤ ↑C * emetric.diam s ^ ↑r
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) :
has_nndist.nndist (f x) (f y) ≤ C * has_nndist.nndist x y ^ ↑r
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) :
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) :
has_dist.dist (f x) (f y) ≤ ↑C * has_dist.dist x y ^ ↑r