Smooth dependence of the maximal integral curve near time zero

Let v be a vector field on a separated boundaryless C^1 manifold M modelled on a complete normed space. This file shows that if v is C^(n+1) at x₀, then the maximal flow (x, t) ↦ maximalIntegralCurve v x t is jointly C^(n+1) in the initial point and the time at (x₀, 0). Together with TauCeti.eventually_mem_maximalIntegralCurveInterval, which puts a neighbourhood of (x₀, 0) in the domain of the maximal flow, this is the local input to the smooth flow of a vector field, and in particular to the geodesic flow, which is the flow of the geodesic spray on the tangent bundle.

Main results

• contMDiffAt_maximalIntegralCurve: the maximal flow is C^(n+1) in the initial point and the time at (x₀, 0).

References

• [Lee, J. M. (2012). Introduction to Smooth Manifolds. Springer New York.][lee2012], Chapter 9, Theorem 9.12.
• Winston Yin, mathlib4#26394: Existence of local flows on manifolds, for the manifold local-flow formulation.

theorem TauCeti.contMDiffAt_maximalIntegralCurve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [BoundarylessManifold I M] [CompleteSpace E] [T2Space M] {v : (x : M) → TangentSpace I x} {x₀ : M} {n : ℕ∞} (hvx : ContMDiffAt I I.tangent (↑n + 1) (fun (y : M) => ⟨y, v y⟩) x₀) : ContMDiffAt (I.prod (modelWithCornersSelf ℝ ℝ)) I (↑n + 1) (fun (p : M × ℝ) => maximalIntegralCurve v p.1 p.2) (x₀, 0)

The maximal flow is C^(n+1) near time zero. Suppose v is C^(n+1) at x₀, for n finite or infinite, on a separated boundaryless manifold modelled on a complete normed space. Then the maximal flow (x, t) ↦ maximalIntegralCurve v x t is C^(n+1) jointly in the initial point and the time at (x₀, 0).