The Banach space of global Hölder functions

This file equips bounded continuous Hölder functions with the norm

‖f‖_[C^α] = ‖f‖_∞ + [f]_α

and proves that this norm is complete when the codomain is complete. The supremum term controls the pointwise limit of a Cauchy sequence, while the Hölder term controls its increments uniformly. Thus the limiting function is again Hölder and convergence holds in both terms of the norm.

The resulting Banach space is the zeroth-order member of the C^{k,α} scale used for Schauder estimates. The definition uses Mathlib's MemHolder and nnHolderNorm rather than introducing a parallel notion of Hölder continuity.

Main declarations

• TauCeti.HolderSpace: bounded continuous globally α-Hölder functions.
• TauCeti.HolderSpace.instNormedAddCommGroup: the supremum-plus-Hölder normed group structure.
• TauCeti.HolderSpace.instCompleteSpace: completeness when the codomain is complete.
• TauCeti.HolderSpace.constL, TauCeti.HolderSpace.evalCLM, and TauCeti.HolderSpace.toBoundedContinuousFunctionCLM: continuous linear maps for constants, evaluation, and inclusion, with operator-norm bounds.

References

L. C. Evans, Partial Differential Equations, Section 5.1; D. Gilbarg and N. Trudinger, Elliptic Partial Differential Equations of Second Order, Section 4.1.

structure TauCeti.HolderSpace (α : NNReal) (X : Type u) (Y : Type v) [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : Type (max u v)

The space of bounded continuous globally α-Hölder functions, equipped below with the supremum-plus-Hölder norm. The wrapper separates this norm from the inherited supremum norm on the underlying submodule.

• toHolderSubmodule : ↥(holderSubmodule α)

  The underlying bounded continuous Hölder function.

@[instance_reducible]

instance TauCeti.HolderSpace.instCoeFunForall {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : CoeFun (HolderSpace α X Y) fun (x : HolderSpace α X Y) => X → Y

Equations

• TauCeti.HolderSpace.instCoeFunForall = { coe := fun (f : TauCeti.HolderSpace α X Y) => ⇑↑f.toHolderSubmodule }

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

The underlying bounded continuous function.

Equations

• f.toBoundedContinuousFunction = ↑f.toHolderSubmodule

def TauCeti.HolderSpace.ofBoundedContinuousFunction {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (f : BoundedContinuousFunction X Y) (hf : MemHolder α ⇑f) : HolderSpace α X Y

Promote a bounded continuous Hölder function to the Hölder space.

Equations

• TauCeti.HolderSpace.ofBoundedContinuousFunction f hf = { toHolderSubmodule := ⟨f, ⋯⟩ }

@[simp]

theorem TauCeti.HolderSpace.toBoundedContinuousFunction_ofBoundedContinuousFunction {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (f : BoundedContinuousFunction X Y) (hf : MemHolder α ⇑f) : (ofBoundedContinuousFunction f hf).toBoundedContinuousFunction = f

@[simp]

theorem TauCeti.HolderSpace.toBoundedContinuousFunction_apply {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (f : HolderSpace α X Y) (x : X) : f.toBoundedContinuousFunction x = ↑f.toHolderSubmodule x

@[simp]

theorem TauCeti.HolderSpace.coe_toBoundedContinuousFunction {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (f : HolderSpace α X Y) : ⇑f.toBoundedContinuousFunction = ⇑↑f.toHolderSubmodule

@[simp]

theorem TauCeti.HolderSpace.ofBoundedContinuousFunction_apply {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (f : BoundedContinuousFunction X Y) (hf : MemHolder α ⇑f) (x : X) : ↑(ofBoundedContinuousFunction f hf).toHolderSubmodule x = f x

theorem TauCeti.HolderSpace.continuous {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (f : HolderSpace α X Y) : Continuous ⇑↑f.toHolderSubmodule

Every element of the bounded Hölder space is continuous, including at exponent zero.

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

A Hölder-space element satisfies the global Hölder condition.

theorem TauCeti.HolderSpace.ext {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {f g : HolderSpace α X Y} (h : ∀ (x : X), ↑f.toHolderSubmodule x = ↑g.toHolderSubmodule x) : f = g

Two Hölder-space elements are equal when they agree pointwise.

theorem TauCeti.HolderSpace.ext_iff {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {f g : HolderSpace α X Y} : f = g ↔ ∀ (x : X), ↑f.toHolderSubmodule x = ↑g.toHolderSubmodule x

@[instance_reducible]

instance TauCeti.HolderSpace.instZero {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : Zero (HolderSpace α X Y)

Equations

• TauCeti.HolderSpace.instZero = { zero := { toHolderSubmodule := 0 } }

@[instance_reducible]

instance TauCeti.HolderSpace.instAdd {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : Add (HolderSpace α X Y)

Equations

• TauCeti.HolderSpace.instAdd = { add := fun (f g : TauCeti.HolderSpace α X Y) => { toHolderSubmodule := f.toHolderSubmodule + g.toHolderSubmodule } }

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instNeg {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : Neg (HolderSpace α X Y)

Equations

• TauCeti.HolderSpace.instNeg = { neg := fun (f : TauCeti.HolderSpace α X Y) => { toHolderSubmodule := -f.toHolderSubmodule } }

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instSub {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : Sub (HolderSpace α X Y)

Equations

• TauCeti.HolderSpace.instSub = { sub := fun (f g : TauCeti.HolderSpace α X Y) => { toHolderSubmodule := f.toHolderSubmodule - g.toHolderSubmodule } }

@[instance_reducible]

instance TauCeti.HolderSpace.instSMulReal {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : SMul ℝ (HolderSpace α X Y)

Equations

• TauCeti.HolderSpace.instSMulReal = { smul := fun (c : ℝ) (f : TauCeti.HolderSpace α X Y) => { toHolderSubmodule := c • f.toHolderSubmodule } }

@[instance_reducible]

instance TauCeti.HolderSpace.instSMulNat {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : SMul ℕ (HolderSpace α X Y)

Equations

• TauCeti.HolderSpace.instSMulNat = { smul := fun (n : ℕ) (f : TauCeti.HolderSpace α X Y) => { toHolderSubmodule := n • f.toHolderSubmodule } }

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instSMulInt {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : SMul ℤ (HolderSpace α X Y)

Equations

• TauCeti.HolderSpace.instSMulInt = { smul := fun (n : ℤ) (f : TauCeti.HolderSpace α X Y) => { toHolderSubmodule := n • f.toHolderSubmodule } }

@[simp]

theorem TauCeti.HolderSpace.toBoundedContinuousFunction_zero {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : toBoundedContinuousFunction 0 = 0

@[simp]

theorem TauCeti.HolderSpace.toBoundedContinuousFunction_add {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (f g : HolderSpace α X Y) : (f + g).toBoundedContinuousFunction = f.toBoundedContinuousFunction + g.toBoundedContinuousFunction

@[simp]

theorem TauCeti.HolderSpace.toBoundedContinuousFunction_neg {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (f : HolderSpace α X Y) : (-f).toBoundedContinuousFunction = -f.toBoundedContinuousFunction

@[simp]

theorem TauCeti.HolderSpace.toBoundedContinuousFunction_sub {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (f g : HolderSpace α X Y) : (f - g).toBoundedContinuousFunction = f.toBoundedContinuousFunction - g.toBoundedContinuousFunction

@[simp]

theorem TauCeti.HolderSpace.toBoundedContinuousFunction_smul {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (c : ℝ) (f : HolderSpace α X Y) : (c • f).toBoundedContinuousFunction = c • f.toBoundedContinuousFunction

@[simp]

theorem TauCeti.HolderSpace.toBoundedContinuousFunction_nsmul {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (n : ℕ) (f : HolderSpace α X Y) : (n • f).toBoundedContinuousFunction = n • f.toBoundedContinuousFunction

@[simp]

theorem TauCeti.HolderSpace.toBoundedContinuousFunction_zsmul {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (n : ℤ) (f : HolderSpace α X Y) : (n • f).toBoundedContinuousFunction = n • f.toBoundedContinuousFunction

@[simp]

theorem TauCeti.HolderSpace.zero_apply {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (x : X) : ↑(toHolderSubmodule 0) x = 0

@[simp]

theorem TauCeti.HolderSpace.add_apply {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (f g : HolderSpace α X Y) (x : X) : ↑(f + g).toHolderSubmodule x = ↑f.toHolderSubmodule x + ↑g.toHolderSubmodule x

@[simp]

theorem TauCeti.HolderSpace.smul_apply {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (c : ℝ) (f : HolderSpace α X Y) (x : X) : ↑(c • f).toHolderSubmodule x = c • ↑f.toHolderSubmodule x

theorem TauCeti.HolderSpace.toBoundedContinuousFunction_injective {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : Function.Injective toBoundedContinuousFunction

The underlying bounded continuous function determines a Hölder-space element.

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instAddCommGroup {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : AddCommGroup (HolderSpace α X Y)

Equations

• TauCeti.HolderSpace.instAddCommGroup = Function.Injective.addCommGroup TauCeti.HolderSpace.toBoundedContinuousFunction ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instModuleReal {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : Module ℝ (HolderSpace α X Y)

Equations

• TauCeti.HolderSpace.instModuleReal = Function.Injective.module ℝ { toFun := TauCeti.HolderSpace.toBoundedContinuousFunction, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instNorm {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : Norm (HolderSpace α X Y)

The supremum-plus-Hölder norm, combining uniform size with the global Hölder seminorm.

Equations

• TauCeti.HolderSpace.instNorm = { norm := fun (f : TauCeti.HolderSpace α X Y) => TauCeti.holderNorm α f.toBoundedContinuousFunction }

theorem TauCeti.HolderSpace.norm_eq_holderNorm {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (f : HolderSpace α X Y) : ‖f‖ = holderNorm α f.toBoundedContinuousFunction

The Hölder-space norm is the supremum-plus-Hölder norm of the underlying bounded continuous function.

theorem TauCeti.HolderSpace.norm_def {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (f : HolderSpace α X Y) : ‖f‖ = ‖f.toBoundedContinuousFunction‖ + ↑(nnHolderNorm α ⇑f.toBoundedContinuousFunction)

The Hölder-space norm is the sum of the supremum norm and the global Hölder seminorm.

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instNormedAddCommGroup {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : NormedAddCommGroup (HolderSpace α X Y)

The supremum-plus-Hölder norm makes HolderSpace α X Y a normed additive commutative group.

Equations

• TauCeti.HolderSpace.instNormedAddCommGroup = NormedAddCommGroup.ofCore ⋯

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instNormedSpace {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : NormedSpace ℝ (HolderSpace α X Y)

The supremum-plus-Hölder norm makes HolderSpace α X Y a normed space over ℝ.

Equations

• TauCeti.HolderSpace.instNormedSpace = { toModule := inferInstance, norm_smul_le := ⋯ }

theorem TauCeti.HolderSpace.norm_toBoundedContinuousFunction_le {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (f : HolderSpace α X Y) : ‖f.toBoundedContinuousFunction‖ ≤ ‖f‖

The supremum norm is controlled by the Hölder-space norm.

noncomputable def TauCeti.HolderSpace.toBoundedContinuousFunctionCLM {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : HolderSpace α X Y →L[ℝ] BoundedContinuousFunction X Y

Forgetting the Hölder bound is a continuous linear map to bounded continuous functions.

Equations

• TauCeti.HolderSpace.toBoundedContinuousFunctionCLM = { toFun := TauCeti.HolderSpace.toBoundedContinuousFunction, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

@[simp]

theorem TauCeti.HolderSpace.toBoundedContinuousFunctionCLM_apply {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (f : HolderSpace α X Y) : toBoundedContinuousFunctionCLM f = f.toBoundedContinuousFunction

theorem TauCeti.HolderSpace.norm_toBoundedContinuousFunctionCLM_le_one {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : ‖toBoundedContinuousFunctionCLM‖ ≤ 1

Forgetting the Hölder bound has operator norm at most one.

noncomputable def TauCeti.HolderSpace.evalCLM {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (x : X) : HolderSpace α X Y →L[ℝ] Y

Evaluation at a point as a continuous linear map on the Hölder space.

Equations

• TauCeti.HolderSpace.evalCLM x = BoundedContinuousFunction.evalCLM ℝ x ∘SL TauCeti.HolderSpace.toBoundedContinuousFunctionCLM

theorem TauCeti.HolderSpace.evalCLM_def {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (x : X) : evalCLM x = BoundedContinuousFunction.evalCLM ℝ x ∘SL toBoundedContinuousFunctionCLM

Evaluation factors through the inclusion into bounded continuous functions.

@[simp]

theorem TauCeti.HolderSpace.evalCLM_apply {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (x : X) (f : HolderSpace α X Y) : (evalCLM x) f = ↑f.toHolderSubmodule x

theorem TauCeti.HolderSpace.norm_evalCLM_le_one {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (x : X) : ‖evalCLM x‖ ≤ 1

Evaluation has operator norm at most one.

instance TauCeti.HolderSpace.instCompleteSpace {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y] : CompleteSpace (HolderSpace α X Y)

Bounded global α-Hölder functions form a Banach space when the codomain is Banach.

theorem TauCeti.HolderSpace.nnHolderNorm_le {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (f : HolderSpace α X Y) : ↑(nnHolderNorm α ⇑f.toBoundedContinuousFunction) ≤ ‖f‖

The Hölder seminorm is controlled by the Hölder-space norm.

def TauCeti.HolderSpace.const {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (c : Y) : HolderSpace α X Y

A constant function as an element of the bounded Hölder space.

Equations

• TauCeti.HolderSpace.const c = TauCeti.HolderSpace.ofBoundedContinuousFunction (BoundedContinuousFunction.const X c) ⋯

@[simp]

theorem TauCeti.HolderSpace.toBoundedContinuousFunction_const {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (c : Y) : (const c).toBoundedContinuousFunction = BoundedContinuousFunction.const X c

@[simp]

theorem TauCeti.HolderSpace.const_apply {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (c : Y) (x : X) : ↑(const c).toHolderSubmodule x = c

theorem TauCeti.HolderSpace.norm_const_le {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (c : Y) : ‖const c‖ ≤ ‖c‖

The Hölder norm of a constant is at most the norm of its value, even on an empty domain.

@[simp]

theorem TauCeti.HolderSpace.norm_const {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [Nonempty X] (c : Y) : ‖const c‖ = ‖c‖

On a nonempty domain, constant functions have exactly the norm of their value.

@[simp]

theorem TauCeti.HolderSpace.const_zero {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : const 0 = 0

@[simp]

theorem TauCeti.HolderSpace.const_add {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (c d : Y) : const (c + d) = const c + const d

@[simp]

theorem TauCeti.HolderSpace.const_smul {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (c : ℝ) (d : Y) : const (c • d) = c • const d

noncomputable def TauCeti.HolderSpace.constL {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : Y →L[ℝ] HolderSpace α X Y

The continuous linear map assigning a constant bounded Hölder function to each value.

Equations

• TauCeti.HolderSpace.constL = { toFun := TauCeti.HolderSpace.const, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

@[simp]

theorem TauCeti.HolderSpace.constL_apply {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (c : Y) : constL c = const c

theorem TauCeti.HolderSpace.norm_constL_le_one {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : ‖constL‖ ≤ 1

The constant map has operator norm at most one, including on an empty domain.

@[simp]

theorem TauCeti.HolderSpace.norm_constL {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [Nonempty X] [Nontrivial Y] : ‖constL‖ = 1

On a nonempty domain with nontrivial values, the constant map has operator norm one.

@[simp]

theorem TauCeti.HolderSpace.norm_toBoundedContinuousFunctionCLM {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [Nonempty X] [Nontrivial Y] : ‖toBoundedContinuousFunctionCLM‖ = 1

On a nonempty domain with nontrivial values, the inclusion has operator norm one.

@[simp]

theorem TauCeti.HolderSpace.norm_evalCLM {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [Nontrivial Y] (x : X) : ‖evalCLM x‖ = 1

With nontrivial values, evaluation has operator norm one.

@[simp]

theorem TauCeti.HolderSpace.evalCLM_comp_constL {α : NNReal} {X : Type u} {Y : Type v} [MetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (x : X) : evalCLM x ∘SL constL = ContinuousLinearMap.id ℝ Y