The algebra of bounded Hölder functions

Bounded Hölder functions with values in a normed real algebra form a normed real algebra under pointwise multiplication. The existing supremum-plus-Hölder norm is submultiplicative with constant one. Completeness is inherited from HolderSpace, so Banach algebra valued functions give a Banach algebra. Commutativity and the normalization ‖1‖ = 1 are inherited when available; the latter requires a nonempty domain.

Constants, inclusion into bounded continuous functions, and evaluation are continuous algebra homomorphisms of operator norm at most one, with equality on nontrivial values and nonempty domains. This makes coefficient multiplication available within the Hölder spaces used in elliptic estimates.

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instMul {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NonUnitalNormedRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] : Mul (HolderSpace α X A)

Equations

• TauCeti.HolderSpace.instMul = { mul := fun (f g : TauCeti.HolderSpace α X A) => ((ContinuousLinearMap.mul ℝ A).compHolder₂ f) g }

@[simp]

theorem TauCeti.HolderSpace.mul_apply {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NonUnitalNormedRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] (f g : HolderSpace α X A) (x : X) : ↑(f * g).toHolderSubmodule x = ↑f.toHolderSubmodule x * ↑g.toHolderSubmodule x

@[simp]

theorem TauCeti.HolderSpace.toBoundedContinuousFunction_mul {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NonUnitalNormedRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] (f g : HolderSpace α X A) : (f * g).toBoundedContinuousFunction = f.toBoundedContinuousFunction * g.toBoundedContinuousFunction

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instNonUnitalRing {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NonUnitalNormedRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] : NonUnitalRing (HolderSpace α X A)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instNonUnitalNormedRing {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NonUnitalNormedRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] : NonUnitalNormedRing (HolderSpace α X A)

The supremum-plus-Hölder norm is submultiplicative, with no loss in the constant.

Equations

• TauCeti.HolderSpace.instNonUnitalNormedRing = { toNorm := inferInstance.toNorm, toNonUnitalRing := inferInstance, toMetricSpace := inferInstance.toMetricSpace, dist_eq := ⋯, norm_mul_le := ⋯ }

instance TauCeti.HolderSpace.instIsScalarTowerReal {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NonUnitalNormedRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] : IsScalarTower ℝ (HolderSpace α X A) (HolderSpace α X A)

instance TauCeti.HolderSpace.instSMulCommClassReal {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NonUnitalNormedRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] : SMulCommClass ℝ (HolderSpace α X A) (HolderSpace α X A)

@[simp]

theorem TauCeti.HolderSpace.const_mul {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NonUnitalNormedRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] (a b : A) : const (a * b) = const a * const b

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instOne {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] : One (HolderSpace α X A)

Equations

• TauCeti.HolderSpace.instOne = { one := TauCeti.HolderSpace.const 1 }

@[simp]

theorem TauCeti.HolderSpace.one_apply {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] (x : X) : ↑(toHolderSubmodule 1) x = 1

@[simp]

theorem TauCeti.HolderSpace.toBoundedContinuousFunction_one {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] : toBoundedContinuousFunction 1 = 1

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instNatCast {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] : NatCast (HolderSpace α X A)

Equations

• TauCeti.HolderSpace.instNatCast = { natCast := fun (n : ℕ) => TauCeti.HolderSpace.const ↑n }

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instIntCast {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] : IntCast (HolderSpace α X A)

Equations

• TauCeti.HolderSpace.instIntCast = { intCast := fun (n : ℤ) => TauCeti.HolderSpace.const ↑n }

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instPowNat {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] : Pow (HolderSpace α X A) ℕ

Equations

• TauCeti.HolderSpace.instPowNat = { pow := fun (f : TauCeti.HolderSpace α X A) (n : ℕ) => npowRec n f }

@[simp]

theorem TauCeti.HolderSpace.natCast_apply {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] (n : ℕ) (x : X) : ↑(↑n).toHolderSubmodule x = ↑n

@[simp]

theorem TauCeti.HolderSpace.intCast_apply {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] (n : ℤ) (x : X) : ↑(↑n).toHolderSubmodule x = ↑n

@[simp]

theorem TauCeti.HolderSpace.pow_apply {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] (f : HolderSpace α X A) (n : ℕ) (x : X) : ↑(f ^ n).toHolderSubmodule x = ↑f.toHolderSubmodule x ^ n

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instRing {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] : Ring (HolderSpace α X A)

Equations

• TauCeti.HolderSpace.instRing = Function.Injective.ring TauCeti.HolderSpace.toBoundedContinuousFunction ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instNormedRing {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] : NormedRing (HolderSpace α X A)

Bounded Hölder functions inherit the normed-ring structure from their values.

Equations

• TauCeti.HolderSpace.instNormedRing = { toNorm := inferInstance.toNorm, toRing := inferInstance, toMetricSpace := inferInstance.toMetricSpace, dist_eq := ⋯, norm_mul_le := ⋯ }

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instAlgebraReal {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] : Algebra ℝ (HolderSpace α X A)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.HolderSpace.algebraMap_apply {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] (c : ℝ) (x : X) : ↑((algebraMap ℝ (HolderSpace α X A)) c).toHolderSubmodule x = (algebraMap ℝ A) c

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instNormedAlgebraReal {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] : NormedAlgebra ℝ (HolderSpace α X A)

With the inherited scalar action and Hölder norm, pointwise operations give a normed algebra.

Equations

• TauCeti.HolderSpace.instNormedAlgebraReal = { toAlgebra := TauCeti.HolderSpace.instAlgebraReal, norm_smul_le := ⋯ }

instance TauCeti.HolderSpace.instNormOneClassOfNonempty {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] [Nonempty X] [NormOneClass A] : NormOneClass (HolderSpace α X A)

noncomputable def TauCeti.HolderSpace.constA {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] : A →A[ℝ] HolderSpace α X A

The continuous algebra homomorphism assigning a constant Hölder function to each value.

Equations

• TauCeti.HolderSpace.constA = { toFun := TauCeti.HolderSpace.const, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, cont := ⋯ }

@[simp]

theorem TauCeti.HolderSpace.constA_apply {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] (a : A) : constA a = const a

@[simp]

theorem TauCeti.HolderSpace.toContinuousLinearMap_constA {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] : constA.toContinuousLinearMap = constL

theorem TauCeti.HolderSpace.norm_constA_le_one {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] : ‖constA.toContinuousLinearMap‖ ≤ 1

The constant map has operator norm at most one.

theorem TauCeti.HolderSpace.norm_constA {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] [Nonempty X] [Nontrivial A] : ‖constA.toContinuousLinearMap‖ = 1

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

noncomputable def TauCeti.HolderSpace.toBoundedContinuousFunctionA {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] : HolderSpace α X A →A[ℝ] BoundedContinuousFunction X A

The continuous algebra homomorphism forgetting the Hölder seminorm.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.HolderSpace.toBoundedContinuousFunctionA_apply {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] (f : HolderSpace α X A) : toBoundedContinuousFunctionA f = f.toBoundedContinuousFunction

@[simp]

theorem TauCeti.HolderSpace.toContinuousLinearMap_toBoundedContinuousFunctionA {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] : toBoundedContinuousFunctionA.toContinuousLinearMap = toBoundedContinuousFunctionCLM

theorem TauCeti.HolderSpace.norm_toBoundedContinuousFunctionA_le_one {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] : ‖toBoundedContinuousFunctionA.toContinuousLinearMap‖ ≤ 1

The inclusion into bounded continuous functions has operator norm at most one.

theorem TauCeti.HolderSpace.norm_toBoundedContinuousFunctionA {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] [Nonempty X] [Nontrivial A] : ‖toBoundedContinuousFunctionA.toContinuousLinearMap‖ = 1

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

def TauCeti.HolderSpace.evalA {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] (x : X) : HolderSpace α X A →A[ℝ] A

Evaluation at a point as a continuous algebra homomorphism.

Equations

• TauCeti.HolderSpace.evalA x = { toFun := fun (f : TauCeti.HolderSpace α X A) => ↑f.toHolderSubmodule x, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, cont := ⋯ }

@[simp]

theorem TauCeti.HolderSpace.evalA_apply {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] (x : X) (f : HolderSpace α X A) : (evalA x) f = ↑f.toHolderSubmodule x

@[simp]

theorem TauCeti.HolderSpace.toContinuousLinearMap_evalA {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] (x : X) : (evalA x).toContinuousLinearMap = evalCLM x

theorem TauCeti.HolderSpace.norm_evalA_le_one {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] (x : X) : ‖(evalA x).toContinuousLinearMap‖ ≤ 1

Evaluation has operator norm at most one.

theorem TauCeti.HolderSpace.norm_evalA {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] [Nontrivial A] (x : X) : ‖(evalA x).toContinuousLinearMap‖ = 1

With nontrivial values, evaluation has operator norm one.

@[simp]

theorem TauCeti.HolderSpace.evalA_comp_constA {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedRing A] [NormedAlgebra ℝ A] (x : X) : (evalA x).comp constA = ContinuousAlgHom.id ℝ A

@[instance_reducible]

noncomputable instance TauCeti.HolderSpace.instNormedCommRing {X : Type u_1} {A : Type u_2} [MetricSpace X] {α : NNReal} [NormedCommRing A] [NormedAlgebra ℝ A] : NormedCommRing (HolderSpace α X A)

Equations

• TauCeti.HolderSpace.instNormedCommRing = { toNormedRing := inferInstance, mul_comm := ⋯ }