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}
:
@[simp]
theorem
holderOnWith_one
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C : NNReal}
{f : X → Y}
{s : Set X}
:
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}
:
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)
:
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)
:
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)
:
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)
:
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)
:
theorem
HolderOnWith.interpolate
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{r : NNReal}
{f : X → Y}
{C₁ C₂ s t₁ t₂ : NNReal}
{A : Set X}
(hf₁ : HolderOnWith C₁ r f A)
(hf₂ : HolderOnWith C₂ s f A)
(ht : t₁ + t₂ = 1)
:
If a function is (C₁, r)-Hölder and (C₂, s)-Hölder, then it is
(C₁ ^ t₁ * C₂ ^ t₂, r * t₁ + s * t₂)-Hölder for all t₁ t₂ : ℝ≥0 such that
t₁ + t₂ = 1.
theorem
HolderOnWith.holderOnWith_zero_of_bounded
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{r : NNReal}
{f : X → Y}
{C D : NNReal}
{A : Set X}
(hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ ↑D)
(hf : HolderOnWith C r f A)
:
HolderOnWith (C * D ^ ↑r) 0 f A
If a function is Hölder over a bounded set, then it is bounded.
theorem
HolderOnWith.of_le
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{r : NNReal}
{f : X → Y}
{C D s : NNReal}
{A : Set X}
(hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ ↑D)
(hf : HolderOnWith C r f A)
(hsr : s ≤ r)
:
HolderOnWith (C * D ^ (↑r - ↑s)) s f A
If a function is r-Hölder over a bounded set, then it is also s-Hölder when s ≤ r.
theorem
HolderOnWith.mono_const
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{r : NNReal}
{f : X → Y}
{C₁ C₂ : NNReal}
{A : Set X}
(hf : HolderOnWith C₁ r f A)
(hC : C₁ ≤ C₂)
:
HolderOnWith C₂ r f A
theorem
HolderOnWith.interpolate_const
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{r : NNReal}
{f : X → Y}
{C s t₁ t₂ : NNReal}
{A : Set X}
(hf₁ : HolderOnWith C r f A)
(hf₂ : HolderOnWith C s f A)
(ht : t₁ + t₂ = 1)
:
HolderOnWith C (r * t₁ + s * t₂) f A
If a function is (C, r)-Hölder and (C, s)-Hölder,
then it is (C, r * t₁ + s * t₂)-Hölder for all t₁ t₂ : ℝ≥0 such that
t₁ + t₂ = 1.
theorem
convex_setOf_holderOnWith
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(f : X → Y)
(C : NNReal)
(A : Set X)
:
For fixed f : X → Y, A : Set X and C : ℝ≥0, the set of all parameters r : ℝ≥0 such that
f is (C, r)-Hölder on A is convex.
theorem
HolderOnWith.of_le_of_le
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{r : NNReal}
{f : X → Y}
{C₁ C₂ s t : NNReal}
{A : Set X}
(hf₁ : HolderOnWith C₁ r f A)
(hf₂ : HolderOnWith C₂ s f A)
(hrt : r ≤ t)
(hts : t ≤ s)
:
HolderOnWith (max C₁ C₂) t f A
theorem
HolderWith.restrict_iff
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{s : Set X}
:
theorem
HolderOnWith.holderWith
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{s : Set X}
:
HolderOnWith C r f s → HolderWith C r (s.restrict f)
Alias of the reverse direction of HolderWith.restrict_iff.
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)
:
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.interpolate
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{r : NNReal}
{f : X → Y}
{C₁ C₂ s t₁ t₂ : NNReal}
(hf₁ : HolderWith C₁ r f)
(hf₂ : HolderWith C₂ s f)
(ht : t₁ + t₂ = 1)
:
If a function is (C₁, r)-Hölder and (C₂, s)-Hölder, then it is
(C₁ ^ t₁ * C₂ ^ t₂, r * t₁ + s * t₂)-Hölder for all t₁ t₂ : ℝ≥0 such that
t₁ + t₂ = 1.
theorem
HolderWith.holderWith_zero_of_bounded
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{r : NNReal}
{f : X → Y}
{C D : NNReal}
(h : ∀ (x y : X), edist x y ≤ ↑D)
(hf : HolderWith C r f)
:
HolderWith (C * D ^ ↑r) 0 f
If a function is Hölder over a bounded space, then it is bounded.
theorem
HolderWith.of_le
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{r : NNReal}
{f : X → Y}
{C D s : NNReal}
(h : ∀ (x y : X), edist x y ≤ ↑D)
(hf : HolderWith C r f)
(hsr : s ≤ r)
:
HolderWith (C * D ^ (↑r - ↑s)) s f
If a function is r-Hölder over a bounded space, then it is also s-Hölder when s ≤ r.
theorem
HolderWith.interpolate_const
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{r : NNReal}
{f : X → Y}
{C s t₁ t₂ : NNReal}
(hf₁ : HolderWith C r f)
(hf₂ : HolderWith C s f)
(ht : t₁ + t₂ = 1)
:
HolderWith C (r * t₁ + s * t₂) f
If a function is (C, r)-Hölder and (C, s)-Hölder,
then it is (C, r * t₁ + s * t₂)-Hölder for all t₁ t₂ : ℝ≥0 such that
t₁ + t₂ = 1.
theorem
convex_setOf_holderWith
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(f : X → Y)
(C : NNReal)
:
For fixed f : X → Y and C : ℝ≥0, the set of all parameters r : ℝ≥0 such that
f is (C, r)-Hölder is convex.
theorem
HolderWith.of_le_of_le
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{r : NNReal}
{f : X → Y}
{C₁ C₂ s t : NNReal}
(hf₁ : HolderWith C₁ r f)
(hf₂ : HolderWith C₂ s f)
(hrt : r ≤ t)
(hts : t ≤ s)
:
HolderWith (max C₁ C₂) t f
theorem
HolderOnWith.nndist_le_of_le
{X : Type u_1}
{Y : Type u_2}
[PseudoMetricSpace X]
[PseudoMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{s : Set X}
{x y : X}
(hf : HolderOnWith C r f s)
(hx : x ∈ s)
(hy : y ∈ s)
{d : NNReal}
(hd : nndist x y ≤ d)
:
theorem
HolderOnWith.nndist_le
{X : Type u_1}
{Y : Type u_2}
[PseudoMetricSpace X]
[PseudoMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{s : Set X}
{x y : X}
(hf : HolderOnWith C r f s)
(hx : x ∈ s)
(hy : y ∈ s)
:
theorem
HolderOnWith.dist_le_of_le
{X : Type u_1}
{Y : Type u_2}
[PseudoMetricSpace X]
[PseudoMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{s : Set X}
{x y : X}
(hf : HolderOnWith C r f s)
(hx : x ∈ s)
(hy : y ∈ s)
{d : ℝ}
(hd : dist x y ≤ d)
:
theorem
HolderOnWith.dist_le
{X : Type u_1}
{Y : Type u_2}
[PseudoMetricSpace X]
[PseudoMetricSpace Y]
{C r : NNReal}
{f : X → Y}
{s : Set X}
{x y : X}
(hf : HolderOnWith C r f s)
(hx : x ∈ s)
(hy : y ∈ s)
:
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}
:
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}
[SeminormedAddCommGroup α]
[SMulZeroClass α Y]
[IsBoundedSMul α Y]
(a : α)
(hf : HolderWith C r f)
:
HolderWith (C * ‖a‖₊) r (a • f)
theorem
HolderWith.smul_iff
{X : Type u_1}
{Y : Type u_2}
[PseudoMetricSpace X]
[SeminormedAddCommGroup Y]
{C r : NNReal}
{f : X → Y}
{α : Type u_4}
[SeminormedRing α]
[Module α Y]
[NormSMulClass α Y]
(a : α)
(ha : ‖a‖₊ ≠ 0)
: