Joint evaluation in the manifold weak Whitney topology

The weak Whitney topology controls coordinate derivatives on compact subsets of source charts. For a locally compact source model, local compactness gives a compact chart neighbourhood of each point, so a coordinate derivative of a map is continuous jointly in the map and the chart point: ContMDiffMap.tendsto_iteratedFDerivWithin_extChartAt. In order zero this is the continuity of evaluation jointly in the map and the source point, which is what the natural action of the diffeomorphism group on its manifold needs. In higher order it is the input for continuity of composition. On a compact subset of a chart target the convergence is uniform (ContMDiffMap.tendstoUniformlyOn_iteratedFDerivWithin_extChartAt, which needs no local compactness): every chartwise C^m neighbourhood of a map on a compact coordinate set, for m ≤ n, is a weak Whitney neighbourhood.

The compact-neighbourhood argument is the standard one for compact-open evaluation; see M. Hirsch, Differential Topology, Chapter 2, §1.

theorem ContinuousAt.eventually_mem_extChartAt_source {𝕜 : 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] {f : M → N} {x : M} {y : N} {w : E} (hfc : ContinuousAt f (↑(extChartAt I x).symm w)) (hw : w ∈ (extChartAt I x).target) (hf : f (↑(extChartAt I x).symm w) ∈ (extChartAt J y).source) : ∀ᶠ (v : E) in nhdsWithin w (extChartAt I x).target, f (↑(extChartAt I x).symm v) ∈ (extChartAt J y).source

A map continuous at a point and visible there in a target chart stays visible at the nearby points of a source chart target.

theorem ContMDiffMap.contDiffWithinAt_extChartAt {𝕜 : 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] (f : ContMDiffMap I J M N n) {x : M} {y : N} {w : E} (hw : w ∈ (extChartAt I x).target) (hf : f (↑(extChartAt I x).symm w) ∈ (extChartAt J y).source) : ContDiffWithinAt 𝕜 n (↑(extChartAt J y) ∘ ⇑f ∘ ↑(extChartAt I x).symm) (extChartAt I x).target w

The coordinate representative of a C^n map in any pair of extended charts is C^n within the source chart target, at every point where the map is visible in the target chart.

theorem TauCeti.continuousWithinAt_ftaylorSeriesWithin_extChartAt_comp_symm {𝕜 : 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] (x y : M) {z : E} (hz : z ∈ (extChartAt I x).target) (hys : ↑(extChartAt I x).symm z ∈ (extChartAt I y).source) {k : ℕ} (hk : ↑k ≤ n) : ContinuousWithinAt (fun (w : E) => ftaylorSeriesWithin 𝕜 (↑(extChartAt I y) ∘ ↑(extChartAt I x).symm) (extChartAt I x).target w k) (extChartAt I x).target z

The Taylor coefficients of order k ≤ n of the chart transition extChartAt y ∘ (extChartAt x).symm are continuous within the chart target (extChartAt x).target at any point z of it whose preimage lies in the source of the chart at y.

theorem ContMDiffMap.tendsto_iteratedFDerivWithin_extChartAt {𝕜 : 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] [LocallyCompactSpace E] {f₀ : ContMDiffMap I J M N n} {x : M} {y : N} {w₀ : E} (hw₀ : w₀ ∈ (extChartAt I x).target) (hf₀ : f₀ (↑(extChartAt I x).symm w₀) ∈ (extChartAt J y).source) {m : ℕ} (hm : ↑m ≤ n) : Filter.Tendsto (fun (p : ContMDiffMap I J M N n × E) => iteratedFDerivWithin 𝕜 m (↑(extChartAt J y) ∘ ⇑p.1 ∘ ↑(extChartAt I x).symm) (extChartAt I x).target p.2) (nhds f₀ ×ˢ nhdsWithin w₀ (extChartAt I x).target) (nhds (iteratedFDerivWithin 𝕜 m (↑(extChartAt J y) ∘ ⇑f₀ ∘ ↑(extChartAt I x).symm) (extChartAt I x).target w₀))

A coordinate derivative of a C^n map is continuous jointly in the map, for the manifold weak Whitney topology, and the point of the source chart target, provided the source model is locally compact. Derivatives are taken within the chart target, so boundary and corner points are included.

theorem ContMDiffMap.eventually_mem_extChartAt_source {𝕜 : 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] [LocallyCompactSpace E] {f₀ : ContMDiffMap I J M N n} {x : M} {y : N} {w₀ : E} (hw₀ : w₀ ∈ (extChartAt I x).target) (hf₀ : f₀ (↑(extChartAt I x).symm w₀) ∈ (extChartAt J y).source) : ∀ᶠ (p : ContMDiffMap I J M N n × E) in nhds f₀ ×ˢ nhdsWithin w₀ (extChartAt I x).target, p.1 (↑(extChartAt I x).symm p.2) ∈ (extChartAt J y).source

A map visible in a target chart at a point of a source chart stays visible there, jointly for nearby maps and nearby chart points, provided the source model is locally compact.

theorem ContMDiffMap.tendstoUniformlyOn_iteratedFDerivWithin_extChartAt {𝕜 : 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] {f₀ : ContMDiffMap I J M N n} {x : M} {y : N} {C : Set E} (hC : IsCompact C) (hCx : C ⊆ (extChartAt I x).target) (hCy : ∀ w ∈ C, f₀ (↑(extChartAt I x).symm w) ∈ (extChartAt J y).source) {m : ℕ} (hm : ↑m ≤ n) : TendstoUniformlyOn (fun (f : ContMDiffMap I J M N n) (w : E) => iteratedFDerivWithin 𝕜 m (↑(extChartAt J y) ∘ ⇑f ∘ ↑(extChartAt I x).symm) (extChartAt I x).target w) (fun (w : E) => iteratedFDerivWithin 𝕜 m (↑(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 derivatives of maps near f₀ converge uniformly to those of f₀. Derivatives are taken within the chart target, so boundary and corner points are included. No local compactness of the source model is needed.

theorem ContMDiffMap.continuous_eval_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] [LocallyCompactSpace E] : Continuous fun (p : ContMDiffMap I J M N n × M) => p.1 p.2

Evaluation of a C^n map is continuous jointly in the map and the source point for the manifold weak Whitney topology, provided the source model is locally compact.

theorem ContMDiffMap.eventually_forall_dist_lt {𝕜 : 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} [LocallyCompactSpace E] {X : Type u_8} [PseudoMetricSpace X] [ChartedSpace G X] [IsManifold J n X] (f₀ : ContMDiffMap I J M X n) {K : Set M} (hK : IsCompact K) {δ : M → ℝ} (hδ : Continuous δ) (hδ₀ : ∀ x ∈ K, 0 < δ x) : ∀ᶠ (f : ContMDiffMap I J M X n) in nhds f₀, ∀ x ∈ K, dist (f x) (f₀ x) < δ x

Uniform closeness of values on a compact set, up to a continuous tolerance which is positive there, is a neighbourhood condition for the manifold weak Whitney topology.

theorem ContMDiffMap.continuousEval_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] [LocallyCompactSpace E] : ContinuousEval (ContMDiffMap I J M N n) M N

Joint evaluation is continuous for the manifold weak Whitney topology.