Continuous bilinear operations on Hölder spaces

A continuous bilinear map B : E →L[ℝ] F →L[ℝ] G acts pointwise on bounded Hölder functions. The resulting bilinear map has norm at most ‖B‖, and exactly ‖B‖ on a nonempty domain. This supplies multiplication and scalar multiplication in Hölder spaces with the usual supremum-plus-Hölder norm, without replacing the existing space or its norm.

The construction generalizes the scalar-multiplication operator boundedHolderSpaceSmu in DifferentialGeometry, Holder/Bilinear.lean. Keeping the supremum and Hölder terms separate improves its factor 3 to 1.

noncomputable def ContinuousLinearMap.compHolder₂ {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [MetricSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {α : NNReal} (B : E →L[ℝ] F →L[ℝ] G) : TauCeti.HolderSpace α X E →L[ℝ] TauCeti.HolderSpace α X F →L[ℝ] TauCeti.HolderSpace α X G

Pointwise application of a continuous bilinear map as a continuous bilinear map of bounded Hölder spaces.

Equations

• B.compHolder₂ = (ContinuousLinearMap.holderBilinearLinear✝ B).mkContinuous₂ ‖B‖ ⋯

@[simp]

theorem ContinuousLinearMap.compHolder₂_apply {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [MetricSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {α : NNReal} (B : E →L[ℝ] F →L[ℝ] G) (f : TauCeti.HolderSpace α X E) (g : TauCeti.HolderSpace α X F) (x : X) : ↑((B.compHolder₂ f) g).toHolderSubmodule x = (B (↑f.toHolderSubmodule x)) (↑g.toHolderSubmodule x)

theorem ContinuousLinearMap.norm_compHolder₂_le {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [MetricSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {α : NNReal} (B : E →L[ℝ] F →L[ℝ] G) : ‖B.compHolder₂‖ ≤ ‖B‖

Pointwise lifting to Hölder functions does not increase a bilinear map's operator norm.

@[simp]

theorem ContinuousLinearMap.norm_compHolder₂ {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [MetricSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {α : NNReal} [Nonempty X] (B : E →L[ℝ] F →L[ℝ] G) : ‖B.compHolder₂‖ = ‖B‖

On a nonempty domain, pointwise lifting preserves the bilinear operator norm.

@[simp]

theorem ContinuousLinearMap.compHolder₂_flip {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [MetricSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {α : NNReal} (B : E →L[ℝ] F →L[ℝ] G) : B.flip.compHolder₂ = B.compHolder₂.flip

@[simp]

theorem ContinuousLinearMap.compHolder₂_const {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [MetricSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {α : NNReal} (B : E →L[ℝ] F →L[ℝ] G) (e : E) (f : F) : (B.compHolder₂ (TauCeti.HolderSpace.const e)) (TauCeti.HolderSpace.const f) = TauCeti.HolderSpace.const ((B e) f)