Documentation

Mathlib.Topology.MetricSpace.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 #

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 : NNReal) (r : NNReal) (f : XY) :

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.

Equations
Instances For
    def HolderOnWith {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (C : NNReal) (r : NNReal) (f : XY) (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.

    Equations
    Instances For
      @[simp]
      theorem holderOnWith_empty {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (C : NNReal) (r : NNReal) (f : XY) :
      @[simp]
      theorem holderOnWith_singleton {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (C : NNReal) (r : NNReal) (f : XY) (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 : NNReal) (r : NNReal) (f : XY) :
      HolderOnWith C r f s
      theorem holderOnWith_univ {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {C : NNReal} {r : NNReal} {f : XY} :
      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 : XY} {s : Set X} :
      theorem LipschitzOnWith.holderOnWith {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {C : NNReal} {f : XY} {s : Set X} :
      LipschitzOnWith C f sHolderOnWith 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 : XY} :
      theorem LipschitzWith.holderWith {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {C : NNReal} {f : XY} :

      Alias of the reverse direction of holderWith_one.

      theorem HolderWith.holderOnWith {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {C : NNReal} {r : NNReal} {f : XY} (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 : NNReal} {r : NNReal} {f : XY} {s : Set X} (h : HolderOnWith C r f s) {x : X} {y : X} (hx : x s) (hy : y s) :
      edist (f x) (f y) C * edist x y ^ r
      theorem HolderOnWith.edist_le_of_le {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {C : NNReal} {r : NNReal} {f : XY} {s : Set X} (h : HolderOnWith C r f s) {x : X} {y : X} (hx : x s) (hy : y s) {d : ENNReal} (hd : edist x y d) :
      edist (f x) (f y) C * d ^ r
      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 : NNReal} {rg : NNReal} {g : YZ} {t : Set Y} (hg : HolderOnWith Cg rg g t) {Cf : NNReal} {rf : NNReal} {f : XY} (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 : NNReal} {rg : NNReal} {g : YZ} {t : Set Y} (hg : HolderOnWith Cg rg g t) {Cf : NNReal} {rf : NNReal} {f : XY} (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 : NNReal} {r : NNReal} {f : XY} {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 : NNReal} {r : NNReal} {f : XY} {s : Set X} (hf : HolderOnWith C r f s) (h0 : 0 < r) :
      theorem HolderOnWith.mono {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {C : NNReal} {r : NNReal} {f : XY} {s : Set X} {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 : NNReal} {r : NNReal} {f : XY} {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 : NNReal} {r : NNReal} {f : XY} {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 : NNReal} {r : NNReal} {f : XY} {s : Set X} {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 : NNReal} {r : NNReal} {f : XY} {s : Set X} {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 : NNReal} {r : NNReal} {f : XY} {s : Set X} {t : Set X} (hf : HolderOnWith C r f s) {d : ENNReal} (hd : EMetric.diam t d) :
      EMetric.diam (f '' (t s)) C * d ^ r
      theorem HolderOnWith.ediam_image_inter_le {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {C : NNReal} {r : NNReal} {f : XY} {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 : NNReal} {r : NNReal} {f : XY} (h : HolderWith C r f) (x : X) (y : X) :
      edist (f x) (f y) C * edist x y ^ r
      theorem HolderWith.edist_le_of_le {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {C : NNReal} {r : NNReal} {f : XY} (h : HolderWith C r f) {x : X} {y : X} {d : ENNReal} (hd : edist x y d) :
      edist (f x) (f y) C * d ^ r
      theorem HolderWith.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [PseudoEMetricSpace Z] {Cg : NNReal} {rg : NNReal} {g : YZ} (hg : HolderWith Cg rg g) {Cf : NNReal} {rf : NNReal} {f : XY} (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 : NNReal} {rg : NNReal} {g : YZ} (hg : HolderWith Cg rg g) {Cf : NNReal} {rf : NNReal} {f : XY} {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 : NNReal} {r : NNReal} {f : XY} (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 : NNReal} {r : NNReal} {f : XY} (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 : NNReal} {r : NNReal} {f : XY} (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 : NNReal} {r : NNReal} {y : Y} :
      theorem HolderWith.zero {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {C : NNReal} {r : NNReal} [Zero Y] :
      theorem HolderWith.of_isEmpty {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {C : NNReal} {r : NNReal} {f : XY} [IsEmpty X] :
      theorem HolderWith.mono {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {C : NNReal} {r : NNReal} {f : XY} {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 : NNReal} {r : NNReal} {f : XY} (hf : HolderWith C r f) {x : X} {y : X} {d : NNReal} (hd : nndist x y d) :
      nndist (f x) (f y) C * d ^ r
      theorem HolderWith.nndist_le {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {C : NNReal} {r : NNReal} {f : XY} (hf : HolderWith C r f) (x : X) (y : X) :
      nndist (f x) (f y) C * nndist x y ^ r
      theorem HolderWith.dist_le_of_le {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {C : NNReal} {r : NNReal} {f : XY} (hf : HolderWith C r f) {x : X} {y : X} {d : } (hd : dist x y d) :
      dist (f x) (f y) C * d ^ r
      theorem HolderWith.dist_le {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {C : NNReal} {r : NNReal} {f : XY} (hf : HolderWith C r f) (x : X) (y : X) :
      dist (f x) (f y) C * dist x y ^ r
      @[simp]
      theorem holderWith_zero_iff {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [MetricSpace Y] {r : NNReal} {f : XY} :
      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 : NNReal} {C' : NNReal} {r : NNReal} {f : XY} {g : XY} (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 : NNReal} {r : NNReal} {f : XY} {α : Type u_4} [NormedDivisionRing α] [Module α Y] [BoundedSMul α Y] (a : α) (hf : HolderWith C r f) :
      HolderWith (C * a‖₊) r (a f)