The flow of a C^1 vector field on a compact manifold is jointly continuous

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). Q29(a′) of specs/generator-layer-scoping.md.

GlobalFlow.lean built integralFlow (the flow of a C^1 field on a compact boundaryless manifold) with its group law and continuity in time. This file proves it is jointly continuous in (t, x):

• IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith_mem — Mathlib's Picard–Lindelöf local flow with Lipschitz dependence on the initial point (exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith), with the confinement of every solution to closedBall x₀ a made explicit;
• ★ ContDiffAt.exists_localFlow — a C^1 field has a local flow near x₀, jointly continuous on Icc (-ε) ε ×ˢ closedBall x₀ r (Lipschitz in the initial point, uniformly in time, plus continuity in time: continuousOn_prod_of_continuousOn_lipschitzOnWith'), confined to a prescribed neighbourhood;
• chartField, isMIntegralCurveOn_extChartAt_symm_comp — the chart-to-manifold transport of a confined chart solution, factored out of exists_nhds_forall_exists_isMIntegralCurveOn_Ioo;
• ★ exists_nhds_continuousOn_integralFlow — local joint continuity: near every point, for |t| < ε, the flow is the transported chart flow (uniqueness of integral curves on an open interval, isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless), hence continuous;
• exists_forall_continuous_integralFlow_of_abs_lt, integralFlow_nsmul, ★ continuous_integralFlow_point — continuity in the initial point at every time, by a uniform small time (compactness) and iteration of the group law;
• ★★ continuous_integralFlow — joint continuity, from the group law φ t x = φ (t − t₀) (φ t₀ x) and the local statement at (0, φ t₀ x₀).

What is not here: differentiable dependence on the initial point (the variational equation), which Mathlib lacks and which Q29(b′) needs.

Flat: Picard–Lindelöf with Lipschitz dependence on the initial point and confinement

theorem IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith_mem {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) : ∃ (α : E → ℝ → E), (∀ x ∈ Metric.closedBall x₀ ↑r, α x ↑t₀ = x ∧ (∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Set.Icc tmin tmax) t) ∧ ∀ (t : ℝ), α x t ∈ Metric.closedBall x₀ ↑a) ∧ ∃ (L' : NNReal), ∀ t ∈ Set.Icc tmin tmax, LipschitzOnWith L' (fun (x : E) => α x t) (Metric.closedBall x₀ ↑r)

Mathlib's exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith with the confinement of every solution to closedBall x₀ a made explicit.

theorem ContDiffAt.exists_localFlow {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, ∃ (α : E → ℝ → E), (∀ x ∈ Metric.closedBall x₀ r, α x 0 = x ∧ (∀ t ∈ Set.Ioo (-ε) ε, HasDerivAt (α x) (f (α x t)) t) ∧ ∀ (t : ℝ), α x t ∈ s) ∧ ContinuousOn (fun (p : ℝ × E) => α p.2 p.1) (Set.Icc (-ε) ε ×ˢ Metric.closedBall x₀ r)

★ A C^1 field has a local flow near x₀, jointly continuous, confined to a prescribed neighbourhood.

Manifold: joint continuity of the flow

noncomputable def chartField {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] (v : (x : M) → TangentSpace I x) (x₀ : M) : E → E

The vector field read in the chart at x₀: the second component of the tangent-bundle chart of the section.

Equations

• chartField v x₀ w = ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun (x : M) => ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) w).2

theorem isMIntegralCurveOn_extChartAt_symm_comp {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] {v : (x : M) → TangentSpace I x} (x₀ : M) {f : ℝ → E} {ε : ℝ} (hf2 : ∀ t ∈ Set.Ioo (-ε) ε, HasDerivAt f (chartField v x₀ (f t)) t) (hf3 : ∀ (t : ℝ), f t ∈ interior (extChartAt I x₀).target) : IsMIntegralCurveOn (↑(extChartAt I x₀).symm ∘ f) v (Set.Ioo (-ε) ε)

A chart solution confined to the interior of the chart target transports to an integral curve on the manifold (the transport step of exists_nhds_forall_exists_isMIntegralCurveOn_Ioo, factored out).

theorem exists_nhds_continuousOn_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) : ∃ U ∈ nhds x₀, IsOpen U ∧ ∃ ε > 0, ContinuousOn (fun (p : ℝ × M) => integralFlow hv p.1 p.2) (Set.Ioo (-ε) ε ×ˢ U)

★ Local joint continuity of the flow. Near every x₀ there are an open neighbourhood U and an ε > 0 on which (t, x) ↦ integralFlow t x is continuous, for |t| < ε: in the chart the flow is the Picard–Lindelöf local flow, jointly continuous by Lipschitz dependence on the initial point, and uniqueness of integral curves identifies it with integralFlow.

theorem exists_forall_continuous_integralFlow_of_abs_lt {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⟩) : ∃ ε₀ > 0, ∀ (t : ℝ), |t| < ε₀ → Continuous fun (x : M) => integralFlow hv t x

Continuity of the flow at time t in the initial point, for |t| below a uniform time.

theorem integralFlow_nsmul {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 : ℝ) (k : ℕ) (x : M) : integralFlow hv (↑k * s) x = (fun (y : M) => integralFlow hv s y)^[k] x

The flow at time k • s is the k-th iterate of the flow at time s.

theorem continuous_integralFlow_point {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 : ℝ) : Continuous fun (x : M) => integralFlow hv t x

★ For every time t, x ↦ integralFlow t x is continuous (iterate a small time).

theorem continuous_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⟩) : Continuous fun (p : ℝ × M) => integralFlow hv p.1 p.2

★★ The flow of a C^1 vector field on a compact manifold is jointly continuous.