Parametric families of functions on a manifold

Let F : 𝕜 → M → F' be a one-parameter family of functions from a manifold M to a normed space, jointly smooth on 𝕜 × M. This file proves the two facts needed to differentiate expressions built from F and its manifold differentials in the parameter:

• the parameter derivative y ↦ ∂ᵣ F (t, y) at a fixed parameter t loses one derivative of joint regularity, and so does the field of velocities of the curves of a two-parameter family of points of M;
• for a jointly C² family, the parameter derivative and the manifold differential commute: ∂ₜ (d (F t) x v) = d (∂ₜ F t) x v.

More generally, for a family G : P → M → F' parametrized by a manifold P and jointly C^n, the differential d (G r) x at a fixed point x, as a covector-valued function of the parameter r, loses one derivative of joint regularity. This is the regularity input for mixed second derivatives of functions on a product of manifolds.

The second fact is the manifold form of the symmetry of mixed partial derivatives. It is read in the extended chart at x, within the range of the model with corners, so it also holds at boundary points.

Main results

• TauCeti.Manifold.contDiffAt_extChartAt_family: a jointly C^n family of maps of M fixing x is jointly C^n when read in the chart at x.
• TauCeti.Manifold.eventuallyEq_extChartAt_family_of_eq_id: a family of maps which is the identity near x at time t is, read in the chart at x, the identity near the image of x.
• TauCeti.Manifold.contMDiffAt_deriv_of_contMDiffAt_uncurry: the parameter derivative of a jointly C^n family is C^m for m + 1 ≤ n.
• ContMDiffAt.contMDiffAt_curveVelocity_snd: for a jointly C^n map f : 𝕜 → 𝕜 → M, the velocities of the curves f q, as a map of both parameters to the tangent bundle, are C^m for m + 1 ≤ n.
• TauCeti.Manifold.hasDerivAt_mvfderiv_apply: the parameter derivative of the differential of a jointly C² family is the differential of its parameter derivative.
• TauCeti.Manifold.contMDiffAt_mvfderiv_of_contMDiffAt_uncurry: the differential at a fixed point of a jointly C^n family parametrized by a manifold is C^m in the parameter for m + 1 ≤ n.
• TauCeti.Manifold.contMDiff_mfderiv_apply_one_zero: the velocity q ↦ dΓ_q (1, 0) of a C^n map Γ out of 𝕜 × M is a C^m section along it for m + 1 ≤ n.

theorem TauCeti.Manifold.contDiffAt_extChartAt_family {𝕜 : 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] {t : 𝕜} {x : M} {n : WithTop ℕ∞} [I.Boundaryless] {ψ : 𝕜 → M → M} (hid : ψ t x = x) (hψ : ContMDiffAt ((modelWithCornersSelf 𝕜 𝕜).prod I) I n (Function.uncurry ψ) (t, x)) : ContDiffAt 𝕜 n (fun (p : 𝕜 × E) => ↑(extChartAt I x) (ψ p.1 (↑(extChartAt I x).symm p.2))) (t, ↑(extChartAt I x) x)

A family of maps ψᵤ of M which is jointly C^n at (t, x) and fixes x at time t is, read in the chart at x, a jointly C^n map of 𝕜 × E at (t, extChartAt I x x).

theorem TauCeti.Manifold.eventuallyEq_extChartAt_family_of_eq_id {𝕜 : 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] {t : 𝕜} {x : M} [I.Boundaryless] {ψ : 𝕜 → M → M} (hid : ∀ᶠ (y : M) in nhds x, ψ t y = y) : (fun (z : E) => ↑(extChartAt I x) (ψ t (↑(extChartAt I x).symm z))) =ᶠ[nhds (↑(extChartAt I x) x)] id

A family of maps which is the identity near x at time t, read in the chart at x, is the identity near the image of x at time t.

theorem TauCeti.Manifold.contMDiffAt_deriv_of_contMDiffAt_uncurry {𝕜 : 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'] {F : 𝕜 → M → F'} {t : 𝕜} {x : M} {m n : WithTop ℕ∞} (hF : ContMDiffAt ((modelWithCornersSelf 𝕜 𝕜).prod I) (modelWithCornersSelf 𝕜 F') n (Function.uncurry F) (t, x)) (hmn : m + 1 ≤ n) : ContMDiffAt I (modelWithCornersSelf 𝕜 F') m (fun (y : M) => deriv (fun (r : 𝕜) => F r y) t) x

Regularity of the parameter derivative. If a family F : 𝕜 → M → F' is jointly C^n at (t, x), then its parameter derivative y ↦ ∂ᵣ F (r, y) at r = t is C^m at x for every m with m + 1 ≤ n.

theorem ContMDiffAt.contMDiffAt_curveVelocity_snd {𝕜 : 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] {m n : WithTop ℕ∞} [IsManifold I 1 M] {f : 𝕜 → 𝕜 → M} {u v : 𝕜} (hf : ContMDiffAt (modelWithCornersSelf 𝕜 (𝕜 × 𝕜)) I n (fun (z : 𝕜 × 𝕜) => f z.1 z.2) (u, v)) (hmn : m + 1 ≤ n) : ContMDiffAt (modelWithCornersSelf 𝕜 (𝕜 × 𝕜)) I.tangent m (fun (z : 𝕜 × 𝕜) => ⟨f z.1 z.2, TauCeti.Manifold.curveVelocity I (f z.1) z.2⟩) (u, v)

Regularity of the velocity field of a two-parameter family. If f : 𝕜 → 𝕜 → M is jointly C^n at (u, v), then the velocities of its curves f q, as a map of both parameters to the tangent bundle, are C^m at (u, v) for every m with m + 1 ≤ n.

theorem TauCeti.Manifold.hasDerivAt_mvfderiv_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'] {F : 𝕜 → M → F'} {t : 𝕜} {x : M} [IsManifold I 1 M] (hF : ContMDiffAt ((modelWithCornersSelf 𝕜 𝕜).prod I) (modelWithCornersSelf 𝕜 F') (minSmoothness 𝕜 2) (Function.uncurry F) (t, x)) (v : TangentSpace I x) : HasDerivAt (fun (r : 𝕜) => (d% (F r) x) v) (((d% fun (y : M) => deriv (fun (r : 𝕜) => F r y) t) x) v) t

Mixed derivatives on a manifold. If a family F : 𝕜 → M → F' is jointly C² at (t, x) (analytic, over a field other than ℝ or ℂ), then the parameter derivative at t of the differential of F r at x, applied to v, is the differential at x of the parameter derivative y ↦ ∂ᵣ F (r, y) at r = t, applied to v.

theorem TauCeti.Manifold.contMDiffAt_mvfderiv_of_contMDiffAt_uncurry {𝕜 : 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'] {x : M} {m n : WithTop ℕ∞} [IsManifold I 1 M] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {P : Type u_8} [TopologicalSpace P] [ChartedSpace H' P] [IsManifold J 1 P] {G : P → M → F'} {p : P} (hG : ContMDiffAt (J.prod I) (modelWithCornersSelf 𝕜 F') n (Function.uncurry G) (p, x)) (hmn : m + 1 ≤ n) : ContMDiffAt J (modelWithCornersSelf 𝕜 (E →L[𝕜] F')) m (fun (r : P) => d% (G r) x) p

Regularity of the differential in a manifold parameter. If a family G : P → M → F' is jointly C^n at (p, x), then the differential d (G r) x, as a function of r with values in the covectors E →L[𝕜] F' on the model space of T_x M, is C^m at p for every m with m + 1 ≤ n.

theorem TauCeti.Manifold.contMDiff_mfderiv_apply_one_zero {𝕜 : 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] {m n : WithTop ℕ∞} [IsManifold I 1 M] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} {N : Type u_8} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] {Γ : 𝕜 × M → N} (hΓ : ContMDiff ((modelWithCornersSelf 𝕜 𝕜).prod I) J n Γ) (hmn : m + 1 ≤ n) : ContMDiff ((modelWithCornersSelf 𝕜 𝕜).prod I) J.tangent m fun (q : 𝕜 × M) => ⟨Γ q, (mfderiv% Γ q) (1, 0)⟩

The velocity q ↦ dΓ_q (1, 0) of a C^n map out of 𝕜 × M is a C^m section along it when m + 1 ≤ n.