Hölder norm

This file defines the Hölder (semi-)norm for Hölder functions alongside some basic properties. The r-Hölder norm of a function f : X → Y between two metric spaces is the least non-negative real number C for which f is r-Hölder continuous with constant C, i.e. it is the least C for which WithHolder C r f is true.

Main definitions

• eHolderNorm r f: r-Hölder (semi-)norm in ℝ≥0∞ of a function f.
• nnHolderNorm r f: r-Hölder (semi-)norm in ℝ≥0 of a function f.
• MemHolder r f: Predicate for a function f being r-Hölder continuous.

Main results

• eHolderNorm_eq_zero: the Hölder norm of a function is zero if and only if it is constant.
• MemHolder.holderWith: The Hölder norm of a Hölder function f is a Hölder constant of f.

Tags

Hölder norm, Hoelder norm, Holder norm

noncomputable def eHolderNorm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (r : NNReal) (f : X → Y) : ENNReal

The r-Hölder (semi-)norm in ℝ≥0∞ of a function f is the least non-negative real number C for which f is r-Hölder continuous with constant C. This is ∞ if no such non-negative real exists.

Equations

• eHolderNorm r f = ⨅ (C : NNReal), ⨅ (_ : HolderWith C r f), ↑C

noncomputable def nnHolderNorm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (r : NNReal) (f : X → Y) : NNReal

The r-Hölder (semi)norm in ℝ≥0.

Equations

• nnHolderNorm r f = (eHolderNorm r f).toNNReal

def MemHolder {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (r : NNReal) (f : X → Y) : Prop

A function f is MemHolder r f if it is Hölder continuous. Namely, f has a finite r-Hölder constant. This is equivalent to f having finite Hölder norm. c.f. memHolder_iff.

Equations

• MemHolder r f = ∃ (C : NNReal), HolderWith C r f

theorem HolderWith.memHolder {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {r : NNReal} {f : X → Y} {C : NNReal} (hf : HolderWith C r f) : MemHolder r f

@[simp]

theorem eHolderNorm_lt_top {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {r : NNReal} {f : X → Y} : eHolderNorm r f < ⊤ ↔ MemHolder r f

theorem eHolderNorm_ne_top {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {r : NNReal} {f : X → Y} : eHolderNorm r f ≠ ⊤ ↔ MemHolder r f

@[simp]

theorem eHolderNorm_eq_top {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {r : NNReal} {f : X → Y} : eHolderNorm r f = ⊤ ↔ ¬MemHolder r f

theorem MemHolder.eHolderNorm_lt_top {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {r : NNReal} {f : X → Y} : MemHolder r f → eHolderNorm r f < ⊤

Alias of the reverse direction of eHolderNorm_lt_top.

theorem MemHolder.eHolderNorm_ne_top {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {r : NNReal} {f : X → Y} : MemHolder r f → eHolderNorm r f ≠ ⊤

Alias of the reverse direction of eHolderNorm_ne_top.

theorem coe_nnHolderNorm_le_eHolderNorm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {r : NNReal} {f : X → Y} : ↑(nnHolderNorm r f) ≤ eHolderNorm r f

@[simp]

theorem eHolderNorm_const (X : Type u_1) {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (r : NNReal) (c : Y) : eHolderNorm r (Function.const X c) = 0

@[simp]

theorem eHolderNorm_zero (X : Type u_1) {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [Zero Y] (r : NNReal) : eHolderNorm r 0 = 0

@[simp]

theorem nnHolderNorm_const (X : Type u_1) {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (r : NNReal) (c : Y) : nnHolderNorm r (Function.const X c) = 0

@[simp]

theorem nnHolderNorm_zero (X : Type u_1) {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [Zero Y] (r : NNReal) : nnHolderNorm r 0 = 0

theorem eHolderNorm_of_isEmpty {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {r : NNReal} {f : X → Y} [hX : IsEmpty X] : eHolderNorm r f = 0

theorem HolderWith.eHolderNorm_le {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {r : NNReal} {f : X → Y} {C : NNReal} (hf : HolderWith C r f) : eHolderNorm r f ≤ ↑C

@[simp]

theorem memHolder_const {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {r : NNReal} {c : Y} : MemHolder r (Function.const X c)

See also memHolder_const for the version with the spelling fun _ ↦ c.

@[simp]

theorem memHolder_const' {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {r : NNReal} {c : Y} : MemHolder r fun (x : X) => c

Version of memHolder_const with the spelling fun _ ↦ c for the constant function.

@[simp]

theorem memHolder_zero {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {r : NNReal} [Zero Y] : MemHolder r 0

theorem eHolderNorm_eq_zero {X : Type u_1} {Y : Type u_2} [MetricSpace X] [EMetricSpace Y] {r : NNReal} {f : X → Y} : eHolderNorm r f = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂

theorem MemHolder.holderWith {X : Type u_1} {Y : Type u_2} [MetricSpace X] [EMetricSpace Y] {r : NNReal} {f : X → Y} (hf : MemHolder r f) : HolderWith (nnHolderNorm r f) r f

theorem memHolder_iff_holderWith {X : Type u_1} {Y : Type u_2} [MetricSpace X] [EMetricSpace Y] {r : NNReal} {f : X → Y} : MemHolder r f ↔ HolderWith (nnHolderNorm r f) r f

theorem MemHolder.coe_nnHolderNorm_eq_eHolderNorm {X : Type u_1} {Y : Type u_2} [MetricSpace X] [EMetricSpace Y] {r : NNReal} {f : X → Y} (hf : MemHolder r f) : ↑(nnHolderNorm r f) = eHolderNorm r f

theorem HolderWith.nnholderNorm_le {X : Type u_1} {Y : Type u_2} [MetricSpace X] [EMetricSpace Y] {C : NNReal} {r : NNReal} {f : X → Y} (hf : HolderWith C r f) : nnHolderNorm r f ≤ C

theorem MemHolder.comp {X : Type u_1} {Y : Type u_2} [MetricSpace X] [EMetricSpace Y] {r : NNReal} {s : NNReal} {Z : Type u_3} [MetricSpace Z] {f : Z → X} {g : X → Y} (hf : MemHolder r f) (hg : MemHolder s g) : MemHolder (s * r) (g ∘ f)

theorem MemHolder.nnHolderNorm_eq_zero {X : Type u_1} {Y : Type u_2} [MetricSpace X] [EMetricSpace Y] {r : NNReal} {f : X → Y} (hf : MemHolder r f) : nnHolderNorm r f = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂

theorem MemHolder.add {X : Type u_1} {Y : Type u_2} [MetricSpace X] [NormedAddCommGroup Y] {r : NNReal} {f : X → Y} {g : X → Y} (hf : MemHolder r f) (hg : MemHolder r g) : MemHolder r (f + g)

theorem MemHolder.smul {X : Type u_1} {Y : Type u_2} [MetricSpace X] [NormedAddCommGroup Y] {r : NNReal} {f : X → Y} {𝕜 : Type u_3} [NormedDivisionRing 𝕜] [Module 𝕜 Y] [BoundedSMul 𝕜 Y] {c : 𝕜} (hf : MemHolder r f) : MemHolder r (c • f)

theorem MemHolder.nsmul {X : Type u_1} {Y : Type u_2} [MetricSpace X] [NormedAddCommGroup Y] {r : NNReal} {f : X → Y} [Module ℝ Y] [BoundedSMul ℝ Y] (n : ℕ) (hf : MemHolder r f) : MemHolder r (n • f)

theorem MemHolder.nnHolderNorm_add_le {X : Type u_1} {Y : Type u_2} [MetricSpace X] [NormedAddCommGroup Y] {r : NNReal} {f : X → Y} {g : X → Y} (hf : MemHolder r f) (hg : MemHolder r g) : nnHolderNorm r (f + g) ≤ nnHolderNorm r f + nnHolderNorm r g

theorem eHolderNorm_add_le {X : Type u_1} {Y : Type u_2} [MetricSpace X] [NormedAddCommGroup Y] {r : NNReal} {f : X → Y} {g : X → Y} : eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g

theorem eHolderNorm_smul {X : Type u_1} {Y : Type u_2} [MetricSpace X] [NormedAddCommGroup Y] {r : NNReal} {f : X → Y} {α : Type u_3} [NormedDivisionRing α] [Module α Y] [BoundedSMul α Y] (c : α) : eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

theorem MemHolder.nnHolderNorm_smul {X : Type u_1} {Y : Type u_2} [MetricSpace X] [NormedAddCommGroup Y] {r : NNReal} {f : X → Y} {α : Type u_3} [NormedDivisionRing α] [Module α Y] [BoundedSMul α Y] (hf : MemHolder r f) (c : α) : nnHolderNorm r (c • f) = ‖c‖₊ * nnHolderNorm r f

theorem eHolderNorm_nsmul {X : Type u_1} {Y : Type u_2} [MetricSpace X] [NormedAddCommGroup Y] {r : NNReal} {f : X → Y} [Module ℝ Y] [BoundedSMul ℝ Y] (n : ℕ) : eHolderNorm r (n • f) = n • eHolderNorm r f

theorem MemHolder.nnHolderNorm_nsmul {X : Type u_1} {Y : Type u_2} [MetricSpace X] [NormedAddCommGroup Y] {r : NNReal} {f : X → Y} [Module ℝ Y] [BoundedSMul ℝ Y] (n : ℕ) (hf : MemHolder r f) : nnHolderNorm r (n • f) = n • nnHolderNorm r f