Regularity of tangent-bundle-valued maps and directional derivatives

This file records reusable regularity facts for maps into a tangent bundle and for applying the manifold differential of a function to tangent vectors whose base point varies.

Main results

• contMDiff_tangentBundle_mk_zero: smoothness of the zero tangent vector over a varying point.
• contMDiff_tangentBundle_mk_constBase: smoothness of a varying model vector over a fixed point.
• mvfderiv_apply_eq_mfderiv_apply: identifies mvfderiv with mfderiv when the target is a normed vector space.
• ContMDiff.contMDiff_mvfderiv_apply: applying the differential of a C^n function on the tangent bundle is C^m when m + 1 ≤ n.
• ContMDiffOn.contMDiffOn_mvfderiv_apply: the derivative of a C^n function along a C^m vector field is C^m on an open set, when m + 1 ≤ n.
• ContMDiffOn.contMDiffOn_totalSpaceMk_mfderiv_apply: the lifted directional derivative z ↦ (f z, df_z ξ) of a C^n map from an open subset of a normed space into a manifold is C^m into the tangent bundle, when m + 1 ≤ n.
• TauCeti.mdifferentiableWithinAt_vectorSpace_iff_differentiableWithinAt and its At and On forms: a vector field on a normed space is differentiable in the manifold sense exactly when it is differentiable as a map of the space.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The infinitesimal adjoint".

theorem contMDiff_tangentBundle_mk_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {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] {f : N → M} (hf : ContMDiff J I n f) : ContMDiff J I.tangent n fun (p : N) => ⟨f p, 0⟩

The zero tangent vector over a smoothly varying manifold point varies smoothly.

theorem contMDiff_tangentBundle_mk_constBase {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {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] {v : N → E} (hv : ContMDiff J (modelWithCornersSelf 𝕜 E) n v) (x : M) : ContMDiff J I.tangent n fun (p : N) => ⟨x, v p⟩

A model-space vector placed in the tangent fiber over a fixed point varies smoothly.

@[simp]

theorem mvfderiv_apply_eq_mfderiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] (f : M → F) (x : M) (v : TangentSpace I x) : (d% f x) v = (mfderiv% f x) v

For a normed vector-space target, the tangent-space identification in mvfderiv is the canonical one, so evaluating it agrees with evaluating mfderiv.

theorem ContMDiff.contMDiff_mvfderiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n m : WithTop ℕ∞} {f : M → F} (hf : ContMDiff I (modelWithCornersSelf 𝕜 F) n f) (hmn : m + 1 ≤ n) : ContMDiff I.tangent (modelWithCornersSelf 𝕜 F) m fun (p : TangentBundle I M) => (d% f p.proj) p.snd

The map that applies the differential of a C^n function to tangent vectors is C^m on the tangent bundle when m + 1 ≤ n.

theorem ContMDiffOn.contMDiffOn_mvfderiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n m : WithTop ℕ∞} {f : M → F} {s : Set M} {A : (y : M) → TangentSpace I y} (hf : ContMDiffOn I (modelWithCornersSelf 𝕜 F) n f s) (hs : IsOpen s) (hA : ContMDiffOn I I.tangent m (fun (y : M) => ⟨y, A y⟩) s) (hmn : m + 1 ≤ n) : ContMDiffOn I (modelWithCornersSelf 𝕜 F) m (fun (y : M) => (d% f y) (A y)) s

The derivative of a C^n function along a C^m vector field is C^m on an open set, when m + 1 ≤ n. This is the set-local form of ContMDiff.contMDiff_mvfderiv_apply: only the germ of f on the open set s enters, so it applies to functions built from sections that are smooth on a chart domain only.

theorem ContMDiffOn.contMDiffOn_totalSpaceMk_mfderiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n m : WithTop ℕ∞} {f : F → M} {U : Set F} (hf : ContMDiffOn (modelWithCornersSelf 𝕜 F) I n f U) (hmn : m + 1 ≤ n) (hU : IsOpen U) (ξ : F) : ContMDiffOn (modelWithCornersSelf 𝕜 F) I.tangent m (fun (z : F) => ⟨f z, (mfderiv% f z) ξ⟩) U

The lifted directional derivative of a C^(m+1) map is C^m. If f is C^n on an open set U of a normed space and m + 1 ≤ n, then for every fixed direction ξ the map z ↦ (f z, df_z ξ) into the tangent bundle is C^m on U. This is the regularity input for composing df_z ξ with C^m maps on the tangent bundle, such as a Riemannian metric.

theorem TauCeti.mdifferentiableWithinAt_vectorSpace_iff_differentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V : (x : E) → TangentSpace (modelWithCornersSelf 𝕜 E) x} {s : Set E} {x : E} : (MDiffAt[s] fun (x : E) => ⟨x, V x⟩) x ↔ DifferentiableWithinAt 𝕜 V s x

A vector field on a normed space is differentiable in the manifold sense iff it is differentiable in the vector space sense. This is the differentiable counterpart of Mathlib's contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt.

theorem TauCeti.mdifferentiableAt_vectorSpace_iff_differentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V : (x : E) → TangentSpace (modelWithCornersSelf 𝕜 E) x} {x : E} : (MDiffAt fun (x : E) => ⟨x, V x⟩) x ↔ DifferentiableAt 𝕜 V x

A vector field on a normed space is differentiable in the manifold sense iff it is differentiable in the vector space sense.

theorem TauCeti.mdifferentiableOn_vectorSpace_iff_differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V : (x : E) → TangentSpace (modelWithCornersSelf 𝕜 E) x} {s : Set E} : (MDiff[s] fun (x : E) => ⟨x, V x⟩) ↔ DifferentiableOn 𝕜 V s

A vector field on a normed space is differentiable in the manifold sense iff it is differentiable in the vector space sense.