Joint continuity of coordinate differentials

The first coordinate derivative varies continuously with the map and the chart point in the weak Whitney topology. The derivative is taken within the extended chart target, including boundary and corner points. This is the operator-valued form of joint chart-jet evaluation, used when inverting the differential of a diffeomorphism. The proof specializes ContMDiffMap.tendsto_iteratedFDerivWithin_extChartAt to order one and uses Mathlib's continuousMultilinearCurryFin1 to obtain a continuous linear operator.

First coordinate derivatives, as linear operators, and second coordinate derivatives, as bilinear operators, converge uniformly on compact subsets of the chart target (TauCeti.tendstoUniformlyOn_fderivWithin_extChartAt, TauCeti.tendstoUniformlyOn_fderivWithin_fderivWithin_extChartAt). This is the form of C² closeness used for the persistence of nondegenerate critical points.

theorem TauCeti.tendsto_fderivWithin_extChartAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [LocallyCompactSpace 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] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold J n N] {f₀ : ContMDiffMap I J M N n} {x : M} {y : N} {w₀ : E} (hn : 1 ≤ n) (hw₀ : w₀ ∈ (extChartAt I x).target) (hf₀ : f₀ (↑(extChartAt I x).symm w₀) ∈ (extChartAt J y).source) : Filter.Tendsto (fun (p : ContMDiffMap I J M N n × E) => fderivWithin 𝕜 (↑(extChartAt J y) ∘ ⇑p.1 ∘ ↑(extChartAt I x).symm) (extChartAt I x).target p.2) (nhds f₀ ×ˢ nhdsWithin w₀ (extChartAt I x).target) (nhds (fderivWithin 𝕜 (↑(extChartAt J y) ∘ ⇑f₀ ∘ ↑(extChartAt I x).symm) (extChartAt I x).target w₀))

Coordinate differentials vary continuously in the map and the chart point.

theorem TauCeti.tendstoUniformlyOn_fderivWithin_extChartAt {𝕜 : 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] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold J n N] {f₀ : ContMDiffMap I J M N n} {x : M} {y : N} {C : Set E} (hn : 1 ≤ n) (hC : IsCompact C) (hCx : C ⊆ (extChartAt I x).target) (hCy : ∀ w ∈ C, f₀ (↑(extChartAt I x).symm w) ∈ (extChartAt J y).source) : TendstoUniformlyOn (fun (f : ContMDiffMap I J M N n) (w : E) => fderivWithin 𝕜 (↑(extChartAt J y) ∘ ⇑f ∘ ↑(extChartAt I x).symm) (extChartAt I x).target w) (fun (w : E) => fderivWithin 𝕜 (↑(extChartAt J y) ∘ ⇑f₀ ∘ ↑(extChartAt I x).symm) (extChartAt I x).target w) (nhds f₀) C

On a compact subset of a source chart target which f₀ maps into a target chart, the coordinate differentials of maps near f₀ converge uniformly to those of f₀.

theorem TauCeti.tendstoUniformlyOn_fderivWithin_fderivWithin_extChartAt {𝕜 : 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] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold J n N] {f₀ : ContMDiffMap I J M N n} {x : M} {y : N} {C : Set E} (hn : 2 ≤ n) (hC : IsCompact C) (hCx : C ⊆ (extChartAt I x).target) (hCy : ∀ w ∈ C, f₀ (↑(extChartAt I x).symm w) ∈ (extChartAt J y).source) : TendstoUniformlyOn (fun (f : ContMDiffMap I J M N n) (w : E) => fderivWithin 𝕜 (fderivWithin 𝕜 (↑(extChartAt J y) ∘ ⇑f ∘ ↑(extChartAt I x).symm) (extChartAt I x).target) (extChartAt I x).target w) (fun (w : E) => fderivWithin 𝕜 (fderivWithin 𝕜 (↑(extChartAt J y) ∘ ⇑f₀ ∘ ↑(extChartAt I x).symm) (extChartAt I x).target) (extChartAt I x).target w) (nhds f₀) C

On a compact subset of a source chart target which f₀ maps into a target chart, the second coordinate derivatives of maps near f₀ converge uniformly to those of f₀.