Documentation

Mathlib.Topology.MetricSpace.HolderNorm

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) :

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

Instances For

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

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

Equations

nnHolderNorm r f = (eHolderNorm r f).toNNReal

Instances For

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

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

Instances For

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) :

@[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] :

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 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 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 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} [SeminormedRing 𝕜] [Module 𝕜 Y] [IsBoundedSMul 𝕜 Y] {c : 𝕜} (hf : MemHolder r f) :

MemHolder r (c • f)

theorem MemHolder.smul_iff {X : Type u_1} {Y : Type u_2} [MetricSpace X] [NormedAddCommGroup Y] {r : NNReal} {f : X → Y} {𝕜 : Type u_3} [SeminormedRing 𝕜] [Module 𝕜 Y] [NormSMulClass 𝕜 Y] {c : 𝕜} (hc : ‖c‖₊ ≠ 0) :

MemHolder r (c • f) ↔ MemHolder r f

theorem MemHolder.nsmul {X : Type u_1} {Y : Type u_2} [MetricSpace X] [NormedAddCommGroup Y] {r : NNReal} {f : X → Y} [NormedSpace ℝ 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 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 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} [NormedRing α] [Module α Y] [NormSMulClass α 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} [NormedRing α] [Module α Y] [NormSMulClass α 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} [NormedSpace ℝ 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} [NormedSpace ℝ Y] (n : ℕ) (hf : MemHolder r f) :

nnHolderNorm r (n • f) = n • nnHolderNorm r f