Smooth finite-dimensional families of continuous linear maps

A family of continuous linear maps with finite-dimensional domain is smooth exactly when all its evaluations are smooth. The source may be a manifold with corners. These criteria recover joint Christoffel regularity from smooth contractions.

Formal sources

The finite-dimensional identification follows Mathlib's contDiffWithinAt_clm_apply, by Sébastien Gouëzel and Floris van Doorn; the proof uses the same continuous linear equivalence.

theorem TauCeti.contMDiffWithinAt_clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 G H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {f : M → E →L[𝕜] F} {s : Set M} {x : M} : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (E →L[𝕜] F)) n f s x ↔ ∀ (v : E), ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F) n (fun (y : M) => (f y) v) s x

A family of continuous linear maps on a finite-dimensional space is smooth within a set exactly when its applications to every fixed vector are smooth within that set.

theorem TauCeti.contMDiffAt_clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 G H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {f : M → E →L[𝕜] F} {x : M} : ContMDiffAt I (modelWithCornersSelf 𝕜 (E →L[𝕜] F)) n f x ↔ ∀ (v : E), ContMDiffAt I (modelWithCornersSelf 𝕜 F) n (fun (y : M) => (f y) v) x

A family of continuous linear maps on a finite-dimensional space is smooth at a manifold point exactly when its applications to every fixed vector are smooth there.