Smoothness of continuous-linear-map coproducts on manifolds

Two families of continuous linear maps g : M → F₁ →L[𝕜] F₃ and f : M → F₂ →L[𝕜] F₃ on a manifold combine into the family x ↦ (g x).coprod (f x) on F₁ × F₂ by composing (g, f) with the continuous linear equivalence ContinuousLinearMap.coprodEquivL. Consequently, C^n regularity is preserved at a point within a set, at a point, on a set, and globally.

Main results

• ContMDiffWithinAt.clm_coprod, ContMDiffAt.clm_coprod, ContMDiffOn.clm_coprod, ContMDiff.clm_coprod: C^n regularity of x ↦ (g x).coprod (f x).

Formal sources

These lemmas parallel ContMDiffWithinAt.clm_prodMap in Mathlib.Geometry.Manifold.ContMDiff.NormedSpace, by Sébastien Gouëzel and Floris van Doorn, replacing ContinuousLinearMap.prodMapL by ContinuousLinearMap.coprodEquivL.

theorem ContMDiffWithinAt.clm_coprod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_5} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_7} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {s : Set M} {x : M} {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₃} (hg : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g s x) (hf : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n f s x) : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₁ × F₂ →L[𝕜] F₃)) n (fun (x : M) => (g x).coprod (f x)) s x

Taking the coproduct (g x).coprod (f x) of two operator families that are C^n within s at x yields an operator family that is C^n within s at x.

theorem ContMDiffAt.clm_coprod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_5} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_7} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {x : M} {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₃} (hg : ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g x) (hf : ContMDiffAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n f x) : ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ × F₂ →L[𝕜] F₃)) n (fun (x : M) => (g x).coprod (f x)) x

Taking the coproduct (g x).coprod (f x) of two operator families that are C^n at x yields an operator family that is C^n at x.

theorem ContMDiffOn.clm_coprod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_5} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_7} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {s : Set M} {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₃} (hg : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g s) (hf : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n f s) : ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ × F₂ →L[𝕜] F₃)) n (fun (x : M) => (g x).coprod (f x)) s

Taking the coproduct (g x).coprod (f x) of two operator families that are C^n on s yields an operator family that is C^n on s.

theorem ContMDiff.clm_coprod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F₁ : Type u_5} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type u_6} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {F₃ : Type u_7} [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₃} (hg : ContMDiff I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g) (hf : ContMDiff I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n f) : ContMDiff I (modelWithCornersSelf 𝕜 (F₁ × F₂ →L[𝕜] F₃)) n fun (x : M) => (g x).coprod (f x)

Taking the coproduct (g x).coprod (f x) of two C^n operator families yields a C^n operator family.