Continuity of composition in the manifold weak Whitney topology

Composition C^n⟮J, N; I', P⟯ × C^n⟮I, M; J, N⟯ → C^n⟮I, M; I', P⟯ is continuous for the weak Whitney topologies, provided the models of the source and of the middle manifold are locally compact. No compactness of the manifolds themselves is needed.

The proof is local in the source. Reading g ∘ f in charts through a chart of N at the image point, the Faà di Bruno formula iteratedFDerivWithin_comp_of_eventually_mem expresses each coordinate derivative of g ∘ f through the coordinate derivatives of g and of f of no larger order (ContMDiffMap.iteratedFDerivWithin_extChartAt_comp). These depend continuously on the maps and the chart point jointly (ContMDiffMap.tendsto_iteratedFDerivWithin_extChartAt), and the Faà di Bruno composition depends continuously on them (Filter.Tendsto.taylorComp). A compactness argument over the compact set of a derivative test then gives continuity.

Main results

• ContMDiffMap.iteratedFDerivWithin_extChartAt_comp: the Faà di Bruno formula for coordinate derivatives of a composite, through any chart of the middle manifold.
• ContMDiffMap.continuous_comp_manifoldWeakWhitney: composition is jointly continuous.

The weak topology and the continuity properties of composition are treated in M. Hirsch, Differential Topology, GTM 33, Chapter 2; the coordinate computation is Mathlib's Faà di Bruno formula.

theorem ContMDiffMap.iteratedFDerivWithin_extChartAt_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I n M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J n N] {E' : Type u_8} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_9} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {P : Type u_10} [TopologicalSpace P] [ChartedSpace H' P] [IsManifold I' n P] (g : ContMDiffMap J I' N P n) (f : ContMDiffMap I J M N n) {x : M} {y : N} {z : P} {w : E} (hw : w ∈ (extChartAt I x).target) (hf : f (↑(extChartAt I x).symm w) ∈ (extChartAt J y).source) (hg : g (f (↑(extChartAt I x).symm w)) ∈ (extChartAt I' z).source) {m : ℕ} (hm : ↑m ≤ n) : iteratedFDerivWithin 𝕜 m (↑(extChartAt I' z) ∘ ⇑(g.comp f) ∘ ↑(extChartAt I x).symm) (extChartAt I x).target w = (ftaylorSeriesWithin 𝕜 (↑(extChartAt I' z) ∘ ⇑g ∘ ↑(extChartAt J y).symm) (extChartAt J y).target (↑(extChartAt J y) (f (↑(extChartAt I x).symm w)))).taylorComp (ftaylorSeriesWithin 𝕜 (↑(extChartAt J y) ∘ ⇑f ∘ ↑(extChartAt I x).symm) (extChartAt I x).target w) m

The Faà di Bruno formula in charts: a coordinate derivative of g ∘ f is the Taylor composition of the coordinate derivatives of g and of f, read through any chart of the middle manifold in which f is visible at the point.

theorem ContMDiffMap.continuous_comp_manifoldWeakWhitney {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I n M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J n N] {E' : Type u_8} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_9} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {P : Type u_10} [TopologicalSpace P] [ChartedSpace H' P] [IsManifold I' n P] [LocallyCompactSpace E] [LocallyCompactSpace F] : Continuous fun (p : ContMDiffMap J I' N P n × ContMDiffMap I J M N n) => p.1.comp p.2

Composition of C^n maps is jointly continuous for the manifold weak Whitney topologies, provided the models of the source and of the middle manifold are locally compact.