Bilinear operations on bounded Hölder functions

A continuous bilinear map sends two bounded Hölder functions of the same exponent to a Hölder function. The estimate keeps the uniform bounds separate from the Hölder constants, so it also applies to restrictions and yields the product estimate for the supremum-plus-Hölder norm.

The argument is adapted from holderWith_bilinear_of_norm_le in DifferentialGeometry, Holder/Bilinear.lean. Here the map may be semilinear over arbitrary nontrivially normed fields, the spaces are seminormed, the domain is a pseudo-emetric space, and the operator norm is explicit.

theorem ContinuousLinearMap.holderOnWith_comp₂ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {X : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [PseudoEMetricSpace X] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜₂ F] [SeminormedAddCommGroup G] [NormedSpace 𝕜₃ G] {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomIsometric σ₁₃] [RingHomIsometric σ₂₃] (B : E →SL[σ₁₃] F →SL[σ₂₃] G) {α Kf Kg Mf Mg : NNReal} {f : X → E} {g : X → F} {s : Set X} (hf : HolderOnWith Kf α f s) (hg : HolderOnWith Kg α g s) (hfnorm : ∀ x ∈ s, ‖f x‖ ≤ ↑Mf) (hgnorm : ∀ x ∈ s, ‖g x‖ ≤ ↑Mg) : HolderOnWith (‖B‖₊ * (Mf * Kg + Mg * Kf)) α (fun (x : X) => (B (f x)) (g x)) s

A bilinear map preserves Hölder continuity on a set when both input functions are bounded there. The constant is ‖B‖ * (Mf * Kg + Mg * Kf).

theorem ContinuousLinearMap.holderWith_comp₂ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {X : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [PseudoEMetricSpace X] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜₂ F] [SeminormedAddCommGroup G] [NormedSpace 𝕜₃ G] {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomIsometric σ₁₃] [RingHomIsometric σ₂₃] (B : E →SL[σ₁₃] F →SL[σ₂₃] G) {α Kf Kg Mf Mg : NNReal} {f : X → E} {g : X → F} (hf : HolderWith Kf α f) (hg : HolderWith Kg α g) (hfnorm : ∀ (x : X), ‖f x‖ ≤ ↑Mf) (hgnorm : ∀ (x : X), ‖g x‖ ≤ ↑Mg) : HolderWith (‖B‖₊ * (Mf * Kg + Mg * Kf)) α fun (x : X) => (B (f x)) (g x)

A bilinear map preserves global Hölder continuity for uniformly bounded functions.