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 → 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;HolderWith: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
HolderWith
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(C r : NNReal)
(f : X → Y)
:
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.
Instances For
def
HolderOnWith
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(C r : NNReal)
(f : X → Y)
(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.
Instances For
@[simp]
theorem
holderOnWith_empty
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(C r : NNReal)
(f : X → Y)
:
HolderOnWith C r f ∅
@[simp]
theorem
holderOnWith_singleton
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(C r : NNReal)
(f : X → Y)
(x : X)
:
HolderOnWith C r f {x}
theorem
Set.Subsingleton.holderOnWith
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{s : Set X}
(hs : s.Subsingleton)
(C r : NNReal)
(f : X → Y)
:
HolderOnWith C r f s
theorem
holderOnWith_univ
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
:
HolderOnWith C r f Set.univ ↔ HolderWith C r f
@[simp]
theorem
holderOnWith_one
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C : NNReal}
{f : X → Y}
{s : Set X}
:
HolderOnWith C 1 f s ↔ LipschitzOnWith C f s
theorem
LipschitzOnWith.holderOnWith
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C : NNReal}
{f : X → Y}
{s : Set X}
:
LipschitzOnWith C f s → 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}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C : NNReal}
{f : X → Y}
:
HolderWith C 1 f ↔ LipschitzWith C f
theorem
LipschitzWith.holderWith
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C : NNReal}
{f : X → Y}
:
LipschitzWith C f → HolderWith C 1 f
Alias of the reverse direction of holderWith_one.
theorem
HolderWith.holderOnWith
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
(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}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{s : Set X}
(h : HolderOnWith C r f s)
{x y : X}
(hx : x ∈ s)
(hy : y ∈ s)
:
theorem
HolderOnWith.edist_le_of_le
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{s : Set X}
(h : HolderOnWith C r f s)
{x y : X}
(hx : x ∈ s)
(hy : y ∈ s)
{d : ENNReal}
(hd : edist x y ≤ d)
:
theorem
HolderOnWith.comp
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
[PseudoEMetricSpace Z]
{s : Set X}
{Cg rg : NNReal}
{g : Y → Z}
{t : Set Y}
(hg : HolderOnWith Cg rg g t)
{Cf rf : NNReal}
{f : X → Y}
(hf : HolderOnWith Cf rf f s)
(hst : Set.MapsTo f s t)
:
HolderOnWith (Cg * Cf ^ ↑rg) (rg * rf) (g ∘ f) s
theorem
HolderOnWith.comp_holderWith
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
[PseudoEMetricSpace Z]
{Cg rg : NNReal}
{g : Y → Z}
{t : Set Y}
(hg : HolderOnWith Cg rg g t)
{Cf rf : NNReal}
{f : X → Y}
(hf : HolderWith Cf rf f)
(ht : ∀ (x : X), f x ∈ t)
:
HolderWith (Cg * Cf ^ ↑rg) (rg * rf) (g ∘ f)
theorem
HolderOnWith.uniformContinuousOn
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{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}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{s : Set X}
(hf : HolderOnWith C r f s)
(h0 : 0 < r)
:
ContinuousOn f s
theorem
HolderOnWith.mono
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{s 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}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{s : Set X}
(hf : HolderOnWith C r f s)
{d : ENNReal}
(hd : EMetric.diam s ≤ d)
:
EMetric.diam (f '' s) ≤ ↑C * d ^ ↑r
theorem
HolderOnWith.ediam_image_le
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{s : Set X}
(hf : HolderOnWith C r f s)
:
EMetric.diam (f '' s) ≤ ↑C * EMetric.diam s ^ ↑r
theorem
HolderOnWith.ediam_image_le_of_subset
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{s t : Set X}
(hf : HolderOnWith C r f s)
(ht : t ⊆ s)
:
EMetric.diam (f '' t) ≤ ↑C * EMetric.diam t ^ ↑r
theorem
HolderOnWith.ediam_image_le_of_subset_of_le
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{s t : Set X}
(hf : HolderOnWith C r f s)
(ht : t ⊆ s)
{d : ENNReal}
(hd : EMetric.diam t ≤ d)
:
EMetric.diam (f '' t) ≤ ↑C * d ^ ↑r
theorem
HolderOnWith.ediam_image_inter_le_of_le
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{s t : Set X}
(hf : HolderOnWith C r f s)
{d : ENNReal}
(hd : EMetric.diam t ≤ d)
:
theorem
HolderOnWith.ediam_image_inter_le
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{s : Set X}
(hf : HolderOnWith C r f s)
(t : Set X)
:
EMetric.diam (f '' (t ∩ s)) ≤ ↑C * EMetric.diam t ^ ↑r
theorem
HolderWith.edist_le
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
(h : HolderWith C r f)
(x y : X)
:
theorem
HolderWith.edist_le_of_le
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
(h : HolderWith C r f)
{x y : X}
{d : ENNReal}
(hd : edist x y ≤ d)
:
theorem
HolderWith.comp
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
[PseudoEMetricSpace Z]
{Cg rg : NNReal}
{g : Y → Z}
(hg : HolderWith Cg rg g)
{Cf rf : NNReal}
{f : X → Y}
(hf : HolderWith Cf rf f)
:
HolderWith (Cg * Cf ^ ↑rg) (rg * rf) (g ∘ f)
theorem
HolderWith.comp_holderOnWith
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
[PseudoEMetricSpace Z]
{Cg rg : NNReal}
{g : Y → Z}
(hg : HolderWith Cg rg g)
{Cf rf : NNReal}
{f : X → Y}
{s : Set X}
(hf : HolderOnWith Cf rf f s)
:
HolderOnWith (Cg * Cf ^ ↑rg) (rg * rf) (g ∘ f) s
theorem
HolderWith.uniformContinuous
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
(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}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
(hf : HolderWith C r f)
(h0 : 0 < r)
:
theorem
HolderWith.ediam_image_le
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
(hf : HolderWith C r f)
(s : Set X)
:
EMetric.diam (f '' s) ≤ ↑C * EMetric.diam s ^ ↑r
theorem
HolderWith.const
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{y : Y}
:
HolderWith C r (Function.const X y)
theorem
HolderWith.zero
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
[Zero Y]
:
HolderWith C r 0
theorem
HolderWith.of_isEmpty
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
[IsEmpty X]
:
HolderWith C r f
theorem
HolderWith.mono
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{C' : NNReal}
(hf : HolderWith C r f)
(h : C ≤ C')
:
HolderWith C' r f
theorem
HolderWith.nndist_le_of_le
{X : Type u_1}
{Y : Type u_2}
[PseudoMetricSpace X]
[PseudoMetricSpace Y]
{C r : NNReal}
{f : X → Y}
(hf : HolderWith C r f)
{x y : X}
{d : NNReal}
(hd : nndist x y ≤ d)
:
theorem
HolderWith.nndist_le
{X : Type u_1}
{Y : Type u_2}
[PseudoMetricSpace X]
[PseudoMetricSpace Y]
{C r : NNReal}
{f : X → Y}
(hf : HolderWith C r f)
(x y : X)
:
theorem
HolderWith.dist_le_of_le
{X : Type u_1}
{Y : Type u_2}
[PseudoMetricSpace X]
[PseudoMetricSpace Y]
{C r : NNReal}
{f : X → Y}
(hf : HolderWith C r f)
{x y : X}
{d : ℝ}
(hd : dist x y ≤ d)
:
theorem
HolderWith.dist_le
{X : Type u_1}
{Y : Type u_2}
[PseudoMetricSpace X]
[PseudoMetricSpace Y]
{C r : NNReal}
{f : X → Y}
(hf : HolderWith C r f)
(x y : X)
:
@[simp]
theorem
holderWith_zero_iff
{X : Type u_1}
{Y : Type u_2}
[PseudoMetricSpace X]
[MetricSpace Y]
{r : NNReal}
{f : X → Y}
:
HolderWith 0 r f ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂
theorem
HolderWith.add
{X : Type u_1}
{Y : Type u_2}
[PseudoMetricSpace X]
[SeminormedAddCommGroup Y]
{C C' r : NNReal}
{f g : X → Y}
(hf : HolderWith C r f)
(hg : HolderWith C' r g)
:
HolderWith (C + C') r (f + g)
theorem
HolderWith.smul
{X : Type u_1}
{Y : Type u_2}
[PseudoMetricSpace X]
[SeminormedAddCommGroup Y]
{C r : NNReal}
{f : X → Y}
{α : Type u_4}
[NormedDivisionRing α]
[Module α Y]
[BoundedSMul α Y]
(a : α)
(hf : HolderWith C r f)
:
HolderWith (C * ‖a‖₊) r (a • f)