Derivatives on manifold chart domains

For a vector-valued smooth map on a manifold, differentiate its coordinate representative within the target of each extended source chart. These derivatives are continuous on that target, even when the manifold has boundary or corners: the model with corners supplies unique derivatives within the chart target.

This construction allows a source covered by many charts, rather than requiring one global chart. It supplies the vector-valued coordinate derivatives needed when treating maps between manifolds locally in the target.

The construction follows M. Hirsch, Differential Topology, GTM 33, Chapter 2, §1, and extends the global-chart construction in ContMDiffMap.WeakWhitney using Mathlib's extended charts and iterated derivatives within sets. No boundaryless or compactness assumption is needed here.

noncomputable def ContMDiffMap.chartIteratedFDeriv {𝕜 : 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] {n : WithTop ℕ∞} [IsManifold I n M] (f : ContMDiffMap I (modelWithCornersSelf 𝕜 F) M F n) (x : M) (m : ℕ) (hm : ↑m ≤ n) : C(↑(extChartAt I x).target, E [×m]→L[𝕜] F)

The derivative of order m of a vector-valued map in the source chart at x, as a continuous map on the extended chart target. Derivatives are taken within that target.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContMDiffMap.chartIteratedFDeriv_apply {𝕜 : 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] {n : WithTop ℕ∞} [IsManifold I n M] (f : ContMDiffMap I (modelWithCornersSelf 𝕜 F) M F n) (x : M) (m : ℕ) (hm : ↑m ≤ n) (y : ↑(extChartAt I x).target) : (f.chartIteratedFDeriv x m hm) y = iteratedFDerivWithin 𝕜 m (writtenInExtChartAt I (modelWithCornersSelf 𝕜 F) x ⇑f) (extChartAt I x).target ↑y

theorem ContMDiffMap.chartIteratedFDeriv_self_target_apply {𝕜 : 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] {n : WithTop ℕ∞} [IsManifold I n M] (f : ContMDiffMap I (modelWithCornersSelf 𝕜 F) M F n) (x : M) (m : ℕ) (hm : ↑m ≤ n) (y : ↑(extChartAt I x).target) : (f.chartIteratedFDeriv x m hm) y = iteratedFDerivWithin 𝕜 m (⇑f ∘ ↑(extChartAt I x).symm) (extChartAt I x).target ↑y

In a self-model target chart, the chart jet is the ordinary coordinate derivative.

@[simp]

theorem ContMDiffMap.chartIteratedFDeriv_zero_apply {𝕜 : 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] {n : WithTop ℕ∞} [IsManifold I n M] (f : ContMDiffMap I (modelWithCornersSelf 𝕜 F) M F n) (x : M) (y : ↑(extChartAt I x).target) (v : Fin 0 → E) : ((f.chartIteratedFDeriv x 0 ⋯) y) v = f (↑(extChartAt I x).symm ↑y)

Order zero of the chart jet recovers the map in source coordinates.

@[simp]

theorem ContMDiffMap.chartIteratedFDeriv_self_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (f : ContMDiffMap (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) E F n) (x : E) (m : ℕ) (hm : ↑m ≤ n) (y : ↑(extChartAt (modelWithCornersSelf 𝕜 E) x).target) : (f.chartIteratedFDeriv x m hm) y = (f.iteratedFDerivContinuousMap m hm) ↑y

For the identity chart of a normed space, the chart derivative is the ordinary iterated derivative, evaluated on the subtype representing the whole chart target.

The coercion type is spelled Set.univ ∩ Set.univ, the simp-normal form of the extended target of the identity chart: the chart target rewrites to Set.univ by chartAt_self_eq, while the intersection itself is not simplified inside a type.