Hölder spaces

This file records the carrier and canonical norm estimates for the zeroth-order global Hölder space. The carrier is a submodule of bounded continuous maps, using Mathlib's existing MemHolder predicate and nnHolderNorm seminorm. The Banach-space completion of this carrier is the next step in the C^{k,α} lane of TauCetiRoadmap/PDE/README.md.

Main declarations

• holderNorm: the supremum-plus-Hölder norm on bounded continuous maps;
• holderSubmodule: the ℝ-submodule of bounded continuous Hölder functions;
• holderNorm_nonneg, norm_le_holderNorm, and nnHolderNorm_le_holderNorm: basic bounds;
• holderNorm_add_le, holderNorm_smul, and holderNorm_sub_le_holderNorm_sub_add_holderNorm_sub: norm estimates.

noncomputable def TauCeti.holderNorm {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] (α : NNReal) (f : BoundedContinuousFunction X Y) : ℝ

The supremum-plus-Hölder norm on bounded continuous maps.

Equations

• TauCeti.holderNorm α f = ‖f‖ + ↑(nnHolderNorm α ⇑f)

def TauCeti.holderSubmodule {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (α : NNReal) : Submodule ℝ (BoundedContinuousFunction X Y)

The ℝ-submodule of bounded continuous α-Hölder functions.

Equations

• TauCeti.holderSubmodule α = { carrier := {f : BoundedContinuousFunction X Y | MemHolder α ⇑f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem TauCeti.mem_holderSubmodule_iff {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {α : NNReal} (f : BoundedContinuousFunction X Y) : f ∈ holderSubmodule α ↔ MemHolder α ⇑f

Membership in holderSubmodule is exactly the global Hölder predicate.

theorem TauCeti.holderNorm_def {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] (α : NNReal) (f : BoundedContinuousFunction X Y) : holderNorm α f = ‖f‖ + ↑(nnHolderNorm α ⇑f)

The defining formula for holderNorm.

@[simp]

theorem TauCeti.holderNorm_zero {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] (α : NNReal) : holderNorm α 0 = 0

The zero function has zero supremum-plus-Hölder norm.

theorem TauCeti.holderSubmodule.memHolder {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {α : NNReal} (f : ↥(holderSubmodule α)) : MemHolder α ⇑↑f

theorem TauCeti.holderSubmodule.holderWith {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {α : NNReal} (f : ↥(holderSubmodule α)) : HolderWith (nnHolderNorm α ⇑↑f) α ⇑↑f

theorem TauCeti.holderSubmodule.memHolder_sub {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {α : NNReal} (f g : ↥(holderSubmodule α)) : MemHolder α (⇑↑f - ⇑↑g)

theorem TauCeti.holderNorm_nonneg {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] {α : NNReal} (f : BoundedContinuousFunction X Y) : 0 ≤ holderNorm α f

The supremum-plus-Hölder norm is nonnegative.

theorem TauCeti.norm_le_holderNorm {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] {α : NNReal} (f : BoundedContinuousFunction X Y) : ‖f‖ ≤ holderNorm α f

The supremum norm is bounded by the supremum-plus-Hölder norm.

theorem TauCeti.nnHolderNorm_le_holderNorm {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] {α : NNReal} (f : BoundedContinuousFunction X Y) : ↑(nnHolderNorm α ⇑f) ≤ holderNorm α f

The Hölder seminorm is bounded by the supremum-plus-Hölder norm.

theorem TauCeti.holderNorm_add_le {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] {α : NNReal} (f g : BoundedContinuousFunction X Y) (hf : MemHolder α ⇑f) (hg : MemHolder α ⇑g) : holderNorm α (f + g) ≤ holderNorm α f + holderNorm α g

Subadditivity of the supremum-plus-Hölder norm for Hölder maps.

@[simp]

theorem TauCeti.holderNorm_smul {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {α : NNReal} (c : ℝ) (f : BoundedContinuousFunction X Y) (hf : MemHolder α ⇑f) : holderNorm α (c • f) = ‖c‖ * holderNorm α f

Scalar homogeneity of the supremum-plus-Hölder norm for Hölder maps.

theorem TauCeti.holderNorm_sub_le_holderNorm_sub_add_holderNorm_sub {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {α : NNReal} (f g h : ↥(holderSubmodule α)) : holderNorm α (↑f - ↑h) ≤ holderNorm α (↑f - ↑g) + holderNorm α (↑g - ↑h)

Triangle inequality for the norm of a difference through an intermediate Hölder map.