Regularity of the differential in fixed tangent charts

The differential of a C^n map f, read in the fixed source tangent chart at x₀ and target tangent chart at f x₀, is C^m throughout their overlap when m + 1 ≤ n. The source and target manifolds are C^(m+1); boundary and corners are allowed. Smooth and analytic orders are included, without shrinking separately for each finite differentiability order.

These operator families give the ranges whose quotients are the intrinsic normal fibres of an embedding. Their regularity on one chart overlap permits a single smooth family of fixed complementary coordinates for that normal bundle.

Reuse Mathlib's ContMDiffAt.mfderiv_const for regularity in charts centred at the evaluation point, and its smooth tangent-bundle transitions to change centres. Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, the normal-bundle construction preceding Theorem 6.24.

theorem ContMDiffAt.mfderiv_inTangentCoordinates {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {m n : WithTop ℕ∞} [IsManifold I (m + 1) M] [IsManifold I' (m + 1) M'] {f : M → M'} {x₀ x : M} (hf : ContMDiffAt I I' n f x) (hmn : m + 1 ≤ n) (hx : x ∈ (chartAt H x₀).source) (hy : f x ∈ (chartAt H' (f x₀)).source) : ContMDiffAt I (modelWithCornersSelf 𝕜 (E →L[𝕜] E')) m (inTangentCoordinates I I' id f (mfderiv% f) x₀) x

A C^n map f at x has a C^m differential in the fixed source tangent chart at x₀ and target tangent chart at f x₀, provided they contain x and f x, respectively, and m + 1 ≤ n. The source chart centre x₀ need not be x.

theorem ContMDiffOn.mfderiv_inTangentCoordinates {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {m n : WithTop ℕ∞} [IsManifold I (m + 1) M] [IsManifold I' (m + 1) M'] {f : M → M'} {s : Set M} (hf : ContMDiffOn I I' n f s) (hmn : m + 1 ≤ n) (hs : IsOpen s) (x₀ : M) : ContMDiffOn I (modelWithCornersSelf 𝕜 (E →L[𝕜] E')) m (inTangentCoordinates I I' id f (mfderiv% f) x₀) (s ∩ (chartAt H x₀).source ∩ f ⁻¹' (chartAt H' (f x₀)).source)

On an open domain, a C^n map f has a C^m coordinate differential on the overlap of the fixed source tangent chart at x₀ and target tangent chart at f x₀.

theorem ContMDiff.mfderiv_inTangentCoordinates {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {m n : WithTop ℕ∞} [IsManifold I (m + 1) M] [IsManifold I' (m + 1) M'] {f : M → M'} (hf : ContMDiff I I' n f) (hmn : m + 1 ≤ n) (x₀ : M) : ContMDiffOn I (modelWithCornersSelf 𝕜 (E →L[𝕜] E')) m (inTangentCoordinates I I' id f (mfderiv% f) x₀) ((chartAt H x₀).source ∩ f ⁻¹' (chartAt H' (f x₀)).source)

A globally C^n map f has a C^m differential on the overlap of the fixed source tangent chart at x₀ and target tangent chart at f x₀, including at smooth and analytic orders.