Global integral curves and the flow of a C^1 vector field on a compact manifold

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Geometry.Manifold.IntegralCurve).

Mathlib has local existence (exists_isMIntegralCurveAt_of_contMDiffAt), uniqueness (isMIntegralCurve_eq_of_contMDiff), and the uniform-time principle exists_isMIntegralCurve_of_isMIntegralCurveOn: if every point has a local integral curve on one and the same Ioo (-ε) ε, every point has a global one. What it does not have is the uniform ε itself. On a compact manifold it exists, and this module proves it:

• ★ exists_nhds_forall_exists_isMIntegralCurveOn_Ioo — uniform local existence time on a neighbourhood: around every point there is a neighbourhood U and an ε > 0 such that every x ∈ U has an integral curve on Ioo (-ε) ε with γ 0 = x. This is Mathlib's local proof with the ball of Picard–Lindelöf kept (ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt gives one ε for a whole closed ball of chart initial points), and the confinement of the chart solutions to the chart's target made uniform by shrinking the ball.
• ★★ exists_isMIntegralCurve_of_compactSpace — on a compact manifold every C^1 vector field has a global integral curve through every point (finite subcover, minimum ε, Mathlib's uniform-time principle).
• ★★ integralFlow hv — the flow ℝ → M → M (indexed by the existence proof hv, well-defined by uniqueness), with integralFlow hv 0 = id, integralFlow_add (the group law, from uniqueness applied to t ↦ φ (s + t) x), and isMIntegralCurve_integralFlow (each orbit is an integral curve); integralFlow_continuous_time (continuity in t) is what uniqueness plus the curves' continuity gives; joint continuity in (t, x) is not stated (see scope).

Honest scope

Against Mathlib's ODE API (checked 2026-09-17). The three flat lemmas are not duplicates of Mathlib's IsPicardLindelof.of_contDiffAt_one, IsPicardLindelof.exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt and ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt: each adds the confinement of the solutions to a prescribed neighbourhood (the closed Lipschitz ball inside a given s ∈ 𝓝 x₀, ∀ t, α t ∈ s), which Mathlib's statements do not provide and the manifold transport needs (the chart solutions must stay in the chart's target). They are the natural upstream strengthening of Mathlib's lemmas, not restatements of them; uniqueness and the uniform-time principle are Mathlib's own (isMIntegralCurve_eq_of_contMDiff, exists_isMIntegralCurve_of_isMIntegralCurveOn).

⚠️ The flow is not yet a Flow. Mathlib's Flow τ α needs joint continuity ℝ × M → M. Continuity in t for fixed x is here. Continuity in x needs continuous dependence of the integral curve on its initial point at manifold level; the flat Lipschitz dependence exists (IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith) and gluing it along the chart cover is the residue (Q29(a′), S–M). Nothing downstream consumes joint continuity until Q29(d′), which needs the time-t maps as homeomorphisms — that is where (a′) is spent.

⚠️ C^1, and x₀'s chart. The field is assumed C^1 as a section of the tangent bundle, the hypothesis Mathlib's local theorem takes; C^∞ fields qualify by ContMDiff.of_le. The transport in exists_nhds_forall_exists_isMIntegralCurveOn_Ioo works in the chart at x₀ and produces curves for initial points in a chart-neighbourhood of x₀; the neighbourhood is the preimage of a closed ball, a neighbourhood of x₀ in M by continuousAt_extChartAt.

Provenance and references. The generator-layer plan §11 (Q29); Mathlib/Geometry/Manifold/IntegralCurve/ (ExistUnique.lean, UniformTime.lean); Mathlib/Analysis/ODE/ExistUnique.lean (ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt).

Picard–Lindelöf with the confinement ball kept

theorem ContDiffAt.isPicardLindelof_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → E} {x₀ : E} (hf : ContDiffAt ℝ 1 f x₀) {s : Set E} (hs : s ∈ nhds x₀) : ∃ (ε : ℝ) (x : 0 < ε) (a : NNReal) (r : NNReal) (L : NNReal) (K : NNReal) (_ : 0 < r), Metric.closedBall x₀ ↑a ⊆ s ∧ ∀ (t₀ : ℝ), IsPicardLindelof (fun (x : ℝ) => f) ⟨t₀, ⋯⟩ x₀ a r L K

Picard–Lindelöf data for a C^1 field at x₀, with the Lipschitz ball inside a prescribed neighbourhood s. Mathlib's IsPicardLindelof.of_contDiffAt_one with one extra intersection.

theorem IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt_mem_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) {x : E} (hx : x ∈ Metric.closedBall x₀ ↑r) : ∃ (α : ℝ → E), α ↑t₀ = x ∧ (∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Set.Icc tmin tmax) t) ∧ ∀ (t : ℝ), α t ∈ Metric.closedBall x₀ ↑a

Picard–Lindelöf with the confinement of the solution made explicit (ODE.FunSpace.compProj_mem_closedBall).

theorem ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : E → E} {x₀ : E} (hf : ContDiffAt ℝ 1 f x₀) {s : Set E} (hs : s ∈ nhds x₀) : ∃ r > 0, ∃ ε > 0, ∀ x ∈ Metric.closedBall x₀ r, ∃ (α : ℝ → E), α 0 = x ∧ (∀ t ∈ Set.Ioo (-ε) ε, HasDerivAt α (f (α t)) t) ∧ ∀ (t : ℝ), α t ∈ s

★ C^1 at x₀: a uniform existence time ε for all initial points in a closed ball, with the solutions confined to a prescribed neighbourhood s of x₀, uniformly.

Uniform local existence time on a neighbourhood

theorem exists_nhds_forall_exists_isMIntegralCurveOn_Ioo {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] [CompleteSpace E] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) (x₀ : M) : ∃ U ∈ nhds x₀, ∃ ε > 0, ∀ x ∈ U, ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Set.Ioo (-ε) ε)

★ Uniform local existence time on a neighbourhood. For a C^1 vector field and a point x₀, there are a neighbourhood U of x₀ and an ε > 0 such that every x ∈ U is the initial point of an integral curve defined on Ioo (-ε) ε.

Mathlib's local theorem (exists_isMIntegralCurveAt_of_contMDiffAt) transported with the ball kept: the flat Picard–Lindelöf statement gives one ε for every chart initial point in a closed ball around φ x₀, and the chart solutions are confined, uniformly, to a ball inside interior φ.target (ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt_mem), so φ.symm ∘ f is an integral curve on the whole interval.

Global integral curves on a compact manifold

theorem exists_isMIntegralCurve_of_compactSpace {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] [CompleteSpace E] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} [CompactSpace M] [T2Space M] (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) (x : M) : ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurve γ v

★★ On a compact manifold every C^1 vector field has a global integral curve through every point. Cover by the neighbourhoods of exists_nhds_forall_exists_isMIntegralCurveOn_Ioo, take a finite subcover, the minimum of its εs is a uniform existence time, and Mathlib's exists_isMIntegralCurve_of_isMIntegralCurveOn extends every local curve to a global one.

The flow

noncomputable def integralFlow {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] [CompleteSpace E] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} [CompactSpace M] [T2Space M] (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) (t : ℝ) (x : M) : M

★★ The flow of a C^1 vector field on a compact manifold: integralFlow hv t x is the value at time t of the (unique) global integral curve through x at time 0.

Equations

• integralFlow hv t x = ⋯.choose t

theorem integralFlow_zero {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] [CompleteSpace E] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} [CompactSpace M] [T2Space M] (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) (x : M) : integralFlow hv 0 x = x

theorem isMIntegralCurve_integralFlow {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] [CompleteSpace E] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} [CompactSpace M] [T2Space M] (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) (x : M) : IsMIntegralCurve (fun (t : ℝ) => integralFlow hv t x) v

Each orbit of the flow is a global integral curve.

theorem integralFlow_eq_of_isMIntegralCurve {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] [CompleteSpace E] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} [CompactSpace M] [T2Space M] (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) {γ : ℝ → M} (hγ : IsMIntegralCurve γ v) {x : M} (h0 : γ 0 = x) : γ = fun (t : ℝ) => integralFlow hv t x

The flow is the unique global integral curve through x at 0.

theorem integralFlow_add {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] [CompleteSpace E] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} [CompactSpace M] [T2Space M] (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) (s t : ℝ) (x : M) : integralFlow hv (s + t) x = integralFlow hv s (integralFlow hv t x)

★★ The group law φ (s + t) = φ s ∘ φ t: u ↦ φ (u + t) x is an integral curve through φ t x at 0 (IsMIntegralCurve.comp_add), so by uniqueness it is u ↦ φ u (φ t x).

theorem continuous_integralFlow_time {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] [CompleteSpace E] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} [CompactSpace M] [T2Space M] (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) (x : M) : Continuous fun (t : ℝ) => integralFlow hv t x