feat: uniqueness of integral curves of a vector field on a manifold (#8886)

We prove the uniqueness of integral curves of a vector field on a manifold using the uniqueness theorem for solutions to ODEs.



Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>

Author: winstonyin

Mathlib/Algebra/Order/Ring/Abs.lean

@@ -158,6 +158,12 @@ lemma sq_eq_sq_iff_abs_eq_abs (a b : α) : a ^ 2 = b ^ 2 ↔ |a| = |b| := by
   simpa only [one_pow, abs_one] using @sq_lt_sq _ _ 1 a
 #align one_lt_sq_iff_one_lt_abs one_lt_sq_iff_one_lt_abs
 
+lemma exists_abs_lt {α : Type*} [LinearOrderedRing α] (a : α) : ∃ b > 0, |a| < b := by
+  refine ⟨|a| + 1, lt_of_lt_of_le zero_lt_one <| by simp, ?_⟩
+  cases' le_or_lt 0 a with ht ht
+  · simp only [abs_of_nonneg ht, lt_add_iff_pos_right, zero_lt_one]
+  · simp only [abs_of_neg ht, lt_add_iff_pos_right, zero_lt_one]
+
 end LinearOrderedRing
 
 section LinearOrderedCommRing

Mathlib/Analysis/ODE/Gronwall.lean

@@ -144,19 +144,24 @@ theorem norm_le_gronwallBound_of_norm_deriv_right_le {f f' : ℝ → E} {δ K ε
     (fun x hx _r hr => (hf' x hx).liminf_right_slope_norm_le hr) ha bound
 #align norm_le_gronwall_bound_of_norm_deriv_right_le norm_le_gronwallBound_of_norm_deriv_right_le
 
+variable {v : ℝ → E → E} {s : ℝ → Set E} {K : ℝ≥0} {f g f' g' : ℝ → E} {a b t₀ : ℝ} {εf εg δ : ℝ}
+  (hv : ∀ t, LipschitzOnWith K (v t) (s t))
+
 /-- If `f` and `g` are two approximate solutions of the same ODE, then the distance between them
 can't grow faster than exponentially. This is a simple corollary of Grönwall's inequality, and some
 people call this Grönwall's inequality too.
 
 This version assumes all inequalities to be true in some time-dependent set `s t`,
 and assumes that the solutions never leave this set. -/
-theorem dist_le_of_approx_trajectories_ODE_of_mem_set {v : ℝ → E → E} {s : ℝ → Set E} {K : ℝ≥0}
-    (hv : ∀ t, LipschitzOnWith K (v t) (s t))
-    {f g f' g' : ℝ → E} {a b : ℝ} {εf εg δ : ℝ} (hf : ContinuousOn f (Icc a b))
+theorem dist_le_of_approx_trajectories_ODE_of_mem
+    (hf : ContinuousOn f (Icc a b))
     (hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t)
-    (f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf) (hfs : ∀ t ∈ Ico a b, f t ∈ s t)
-    (hg : ContinuousOn g (Icc a b)) (hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t)
-    (g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg) (hgs : ∀ t ∈ Ico a b, g t ∈ s t)
+    (f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf)
+    (hfs : ∀ t ∈ Ico a b, f t ∈ s t)
+    (hg : ContinuousOn g (Icc a b))
+    (hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t)
+    (g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg)
+    (hgs : ∀ t ∈ Ico a b, g t ∈ s t)
     (ha : dist (f a) (g a) ≤ δ) :
     ∀ t ∈ Icc a b, dist (f t) (g t) ≤ gronwallBound δ K (εf + εg) (t - a) := by
   simp only [dist_eq_norm] at ha ⊢
@@ -170,22 +175,25 @@ theorem dist_le_of_approx_trajectories_ODE_of_mem_set {v : ℝ → E → E} {s :
   refine this.trans ((add_le_add (add_le_add (f_bound t ht) (g_bound t ht)) hv).trans ?_)
   rw [add_comm]
 set_option linter.uppercaseLean3 false in
-#align dist_le_of_approx_trajectories_ODE_of_mem_set dist_le_of_approx_trajectories_ODE_of_mem_set
+#align dist_le_of_approx_trajectories_ODE_of_mem_set dist_le_of_approx_trajectories_ODE_of_mem
 
 /-- If `f` and `g` are two approximate solutions of the same ODE, then the distance between them
 can't grow faster than exponentially. This is a simple corollary of Grönwall's inequality, and some
 people call this Grönwall's inequality too.
 
 This version assumes all inequalities to be true in the whole space. -/
-theorem dist_le_of_approx_trajectories_ODE {v : ℝ → E → E} {K : ℝ≥0}
-    (hv : ∀ t, LipschitzWith K (v t)) {f g f' g' : ℝ → E} {a b : ℝ} {εf εg δ : ℝ}
-    (hf : ContinuousOn f (Icc a b)) (hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t)
-    (f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf) (hg : ContinuousOn g (Icc a b))
+theorem dist_le_of_approx_trajectories_ODE
+    (hv : ∀ t, LipschitzWith K (v t))
+    (hf : ContinuousOn f (Icc a b))
+    (hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t)
+    (f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf)
+    (hg : ContinuousOn g (Icc a b))
     (hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t)
-    (g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg) (ha : dist (f a) (g a) ≤ δ) :
+    (g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg)
+    (ha : dist (f a) (g a) ≤ δ) :
     ∀ t ∈ Icc a b, dist (f t) (g t) ≤ gronwallBound δ K (εf + εg) (t - a) :=
   have hfs : ∀ t ∈ Ico a b, f t ∈ @univ E := fun _ _ => trivial
-  dist_le_of_approx_trajectories_ODE_of_mem_set (fun t => (hv t).lipschitzOnWith _) hf hf'
+  dist_le_of_approx_trajectories_ODE_of_mem (fun t => (hv t).lipschitzOnWith _) hf hf'
     f_bound hfs hg hg' g_bound (fun _ _ => trivial) ha
 set_option linter.uppercaseLean3 false in
 #align dist_le_of_approx_trajectories_ODE dist_le_of_approx_trajectories_ODE
@@ -196,34 +204,37 @@ people call this Grönwall's inequality too.
 
 This version assumes all inequalities to be true in some time-dependent set `s t`,
 and assumes that the solutions never leave this set. -/
-theorem dist_le_of_trajectories_ODE_of_mem_set {v : ℝ → E → E} {s : ℝ → Set E} {K : ℝ≥0}
-    (hv : ∀ t, LipschitzOnWith K (v t) (s t))
-    {f g : ℝ → E} {a b : ℝ} {δ : ℝ} (hf : ContinuousOn f (Icc a b))
-    (hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t) (hfs : ∀ t ∈ Ico a b, f t ∈ s t)
+theorem dist_le_of_trajectories_ODE_of_mem
+    (hf : ContinuousOn f (Icc a b))
+    (hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t)
+    (hfs : ∀ t ∈ Ico a b, f t ∈ s t)
     (hg : ContinuousOn g (Icc a b)) (hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t)
     (hgs : ∀ t ∈ Ico a b, g t ∈ s t) (ha : dist (f a) (g a) ≤ δ) :
     ∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * exp (K * (t - a)) := by
   have f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0 := by intros; rw [dist_self]
   have g_bound : ∀ t ∈ Ico a b, dist (v t (g t)) (v t (g t)) ≤ 0 := by intros; rw [dist_self]
   intro t ht
   have :=
-    dist_le_of_approx_trajectories_ODE_of_mem_set hv hf hf' f_bound hfs hg hg' g_bound hgs ha t ht
+    dist_le_of_approx_trajectories_ODE_of_mem hv hf hf' f_bound hfs hg hg' g_bound hgs ha t ht
   rwa [zero_add, gronwallBound_ε0] at this
 set_option linter.uppercaseLean3 false in
-#align dist_le_of_trajectories_ODE_of_mem_set dist_le_of_trajectories_ODE_of_mem_set
+#align dist_le_of_trajectories_ODE_of_mem_set dist_le_of_trajectories_ODE_of_mem
 
 /-- If `f` and `g` are two exact solutions of the same ODE, then the distance between them
 can't grow faster than exponentially. This is a simple corollary of Grönwall's inequality, and some
 people call this Grönwall's inequality too.
 
 This version assumes all inequalities to be true in the whole space. -/
-theorem dist_le_of_trajectories_ODE {v : ℝ → E → E} {K : ℝ≥0} (hv : ∀ t, LipschitzWith K (v t))
-    {f g : ℝ → E} {a b : ℝ} {δ : ℝ} (hf : ContinuousOn f (Icc a b))
-    (hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t) (hg : ContinuousOn g (Icc a b))
-    (hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t) (ha : dist (f a) (g a) ≤ δ) :
+theorem dist_le_of_trajectories_ODE
+    (hv : ∀ t, LipschitzWith K (v t))
+    (hf : ContinuousOn f (Icc a b))
+    (hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t)
+    (hg : ContinuousOn g (Icc a b))
+    (hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t)
+    (ha : dist (f a) (g a) ≤ δ) :
     ∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * exp (K * (t - a)) :=
   have hfs : ∀ t ∈ Ico a b, f t ∈ @univ E := fun _ _ => trivial
-  dist_le_of_trajectories_ODE_of_mem_set (fun t => (hv t).lipschitzOnWith _) hf hf' hfs hg
+  dist_le_of_trajectories_ODE_of_mem (fun t => (hv t).lipschitzOnWith _) hf hf' hfs hg
     hg' (fun _ _ => trivial) ha
 set_option linter.uppercaseLean3 false in
 #align dist_le_of_trajectories_ODE dist_le_of_trajectories_ODE
@@ -233,26 +244,137 @@ a given initial value provided that the RHS is Lipschitz continuous in `x` withi
 and we consider only solutions included in `s`.
 
 This version shows uniqueness in a closed interval `Icc a b`, where `a` is the initial time. -/
-theorem ODE_solution_unique_of_mem_set {v : ℝ → E → E} {s : ℝ → Set E} {K : ℝ≥0}
-    (hv : ∀ t, LipschitzOnWith K (v t) (s t))
-    {f g : ℝ → E} {a b : ℝ} (hf : ContinuousOn f (Icc a b))
-    (hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t) (hfs : ∀ t ∈ Ico a b, f t ∈ s t)
-    (hg : ContinuousOn g (Icc a b)) (hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t)
-    (hgs : ∀ t ∈ Ico a b, g t ∈ s t) (ha : f a = g a) : EqOn f g (Icc a b) := fun t ht ↦ by
-  have := dist_le_of_trajectories_ODE_of_mem_set hv hf hf' hfs hg hg' hgs (dist_le_zero.2 ha) t ht
+theorem ODE_solution_unique_of_mem_Icc_right
+    (hf : ContinuousOn f (Icc a b))
+    (hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t)
+    (hfs : ∀ t ∈ Ico a b, f t ∈ s t)
+    (hg : ContinuousOn g (Icc a b))
+    (hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t)
+    (hgs : ∀ t ∈ Ico a b, g t ∈ s t)
+    (ha : f a = g a) :
+    EqOn f g (Icc a b) := fun t ht ↦ by
+  have := dist_le_of_trajectories_ODE_of_mem hv hf hf' hfs hg hg' hgs (dist_le_zero.2 ha) t ht
   rwa [zero_mul, dist_le_zero] at this
 set_option linter.uppercaseLean3 false in
-#align ODE_solution_unique_of_mem_set ODE_solution_unique_of_mem_set
+#align ODE_solution_unique_of_mem_set ODE_solution_unique_of_mem_Icc_right
+
+/-- A time-reversed version of `ODE_solution_unique_of_mem_Icc_right`. Uniqueness is shown in a
+closed interval `Icc a b`, where `b` is the "initial" time. -/
+theorem ODE_solution_unique_of_mem_Icc_left
+    (hf : ContinuousOn f (Icc a b))
+    (hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t)
+    (hfs : ∀ t ∈ Ioc a b, f t ∈ s t)
+    (hg : ContinuousOn g (Icc a b))
+    (hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t)
+    (hgs : ∀ t ∈ Ioc a b, g t ∈ s t)
+    (hb : f b = g b) :
+    EqOn f g (Icc a b) := by
+  have hv' t : LipschitzOnWith K (Neg.neg ∘ (v (-t))) (s (-t)) := by
+    rw [← one_mul K]
+    exact LipschitzWith.id.neg.comp_lipschitzOnWith (hv _)
+  have hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b) :=
+    fun _ ht ↦ ⟨le_neg.mp ht.2, neg_le.mp ht.1⟩
+  have hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b) :=
+    fun _ ht ↦ ⟨lt_neg.mp ht.2, neg_le.mp ht.1⟩
+  have hmt3 (t : ℝ) : MapsTo Neg.neg (Ici t) (Iic (-t)) :=
+    fun _ ht' ↦ mem_Iic.mpr <| neg_le_neg ht'
+  suffices EqOn (f ∘ Neg.neg) (g ∘ Neg.neg) (Icc (-b) (-a)) by
+    rw [eqOn_comp_right_iff] at this
+    convert this
+    simp
+  apply ODE_solution_unique_of_mem_Icc_right hv'
+    (hf.comp continuousOn_neg hmt1) _ (fun _ ht ↦ hfs _ (hmt2 ht))
+    (hg.comp continuousOn_neg hmt1) _ (fun _ ht ↦ hgs _ (hmt2 ht)) (by simp [hb])
+  · intros t ht
+    convert HasFDerivWithinAt.comp_hasDerivWithinAt t (hf' (-t) (hmt2 ht))
+      (hasDerivAt_neg t).hasDerivWithinAt (hmt3 t)
+    simp
+  · intros t ht
+    convert HasFDerivWithinAt.comp_hasDerivWithinAt t (hg' (-t) (hmt2 ht))
+      (hasDerivAt_neg t).hasDerivWithinAt (hmt3 t)
+    simp
+
+/-- A version of `ODE_solution_unique_of_mem_Icc_right` for uniqueness in a closed interval whose
+interior contains the initial time. -/
+theorem ODE_solution_unique_of_mem_Icc
+    (ht : t₀ ∈ Ioo a b)
+    (hf : ContinuousOn f (Icc a b))
+    (hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t)
+    (hfs : ∀ t ∈ Ioo a b, f t ∈ s t)
+    (hg : ContinuousOn g (Icc a b))
+    (hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t)
+    (hgs : ∀ t ∈ Ioo a b, g t ∈ s t)
+    (heq : f t₀ = g t₀) :
+    EqOn f g (Icc a b) := by
+  rw [← Icc_union_Icc_eq_Icc (le_of_lt ht.1) (le_of_lt ht.2)]
+  apply EqOn.union
+  · have hss : Ioc a t₀ ⊆ Ioo a b := Ioc_subset_Ioo_right ht.2
+    exact ODE_solution_unique_of_mem_Icc_left hv
+      (hf.mono <| Icc_subset_Icc_right <| le_of_lt ht.2)
+      (fun _ ht' ↦ (hf' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hfs _ (hss ht')))
+      (hg.mono <| Icc_subset_Icc_right <| le_of_lt ht.2)
+      (fun _ ht' ↦ (hg' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hgs _ (hss ht'))) heq
+  · have hss : Ico t₀ b ⊆ Ioo a b := Ico_subset_Ioo_left ht.1
+    exact ODE_solution_unique_of_mem_Icc_right hv
+      (hf.mono <| Icc_subset_Icc_left <| le_of_lt ht.1)
+      (fun _ ht' ↦ (hf' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hfs _ (hss ht')))
+      (hg.mono <| Icc_subset_Icc_left <| le_of_lt ht.1)
+      (fun _ ht' ↦ (hg' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hgs _ (hss ht'))) heq
+
+/-- A version of `ODE_solution_unique_of_mem_Icc` for uniqueness in an open interval. -/
+theorem ODE_solution_unique_of_mem_Ioo
+    (ht : t₀ ∈ Ioo a b)
+    (hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t)
+    (hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t)
+    (heq : f t₀ = g t₀) :
+    EqOn f g (Ioo a b) := by
+  intros t' ht'
+  rcases lt_or_le t' t₀ with (h | h)
+  · have hss : Icc t' t₀ ⊆ Ioo a b :=
+      fun _ ht'' ↦ ⟨lt_of_lt_of_le ht'.1 ht''.1, lt_of_le_of_lt ht''.2 ht.2⟩
+    exact ODE_solution_unique_of_mem_Icc_left hv
+      (ContinuousAt.continuousOn fun _ ht'' ↦ (hf _ <| hss ht'').1.continuousAt)
+      (fun _ ht'' ↦ (hf _ <| hss <| Ioc_subset_Icc_self ht'').1.hasDerivWithinAt)
+      (fun _ ht'' ↦ (hf _ <| hss <| Ioc_subset_Icc_self ht'').2)
+      (ContinuousAt.continuousOn fun _ ht'' ↦ (hg _ <| hss ht'').1.continuousAt)
+      (fun _ ht'' ↦ (hg _ <| hss <| Ioc_subset_Icc_self ht'').1.hasDerivWithinAt)
+      (fun _ ht'' ↦ (hg _ <| hss <| Ioc_subset_Icc_self ht'').2) heq
+      ⟨le_rfl, le_of_lt h⟩
+  · have hss : Icc t₀ t' ⊆ Ioo a b :=
+      fun _ ht'' ↦ ⟨lt_of_lt_of_le ht.1 ht''.1, lt_of_le_of_lt ht''.2 ht'.2⟩
+    exact ODE_solution_unique_of_mem_Icc_right hv
+      (ContinuousAt.continuousOn fun _ ht'' ↦ (hf _ <| hss ht'').1.continuousAt)
+      (fun _ ht'' ↦ (hf _ <| hss <| Ico_subset_Icc_self ht'').1.hasDerivWithinAt)
+      (fun _ ht'' ↦ (hf _ <| hss <| Ico_subset_Icc_self ht'').2)
+      (ContinuousAt.continuousOn fun _ ht'' ↦ (hg _ <| hss ht'').1.continuousAt)
+      (fun _ ht'' ↦ (hg _ <| hss <| Ico_subset_Icc_self ht'').1.hasDerivWithinAt)
+      (fun _ ht'' ↦ (hg _ <| hss <| Ico_subset_Icc_self ht'').2) heq
+      ⟨h, le_rfl⟩
+
+/-- Local unqueness of ODE solutions. -/
+theorem ODE_solution_unique_of_eventually
+    (hf : ∀ᶠ t in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t)
+    (hg : ∀ᶠ t in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t)
+    (heq : f t₀ = g t₀) : f =ᶠ[𝓝 t₀] g := by
+  obtain ⟨ε, hε, h⟩ := eventually_nhds_iff_ball.mp (hf.and hg)
+  rw [Filter.eventuallyEq_iff_exists_mem]
+  refine ⟨ball t₀ ε, ball_mem_nhds _ hε, ?_⟩
+  simp_rw [Real.ball_eq_Ioo] at *
+  apply ODE_solution_unique_of_mem_Ioo hv (Real.ball_eq_Ioo t₀ ε ▸ mem_ball_self hε)
+    (fun _ ht ↦ (h _ ht).1) (fun _ ht ↦ (h _ ht).2) heq
 
 /-- There exists only one solution of an ODE \(\dot x=v(t, x)\) with
-a given initial value provided that RHS is Lipschitz continuous in `x`. -/
-theorem ODE_solution_unique {v : ℝ → E → E} {K : ℝ≥0} (hv : ∀ t, LipschitzWith K (v t))
-    {f g : ℝ → E} {a b : ℝ} (hf : ContinuousOn f (Icc a b))
-    (hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t) (hg : ContinuousOn g (Icc a b))
-    (hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t) (ha : f a = g a) :
+a given initial value provided that the RHS is Lipschitz continuous in `x`. -/
+theorem ODE_solution_unique
+    (hv : ∀ t, LipschitzWith K (v t))
+    (hf : ContinuousOn f (Icc a b))
+    (hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t)
+    (hg : ContinuousOn g (Icc a b))
+    (hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t)
+    (ha : f a = g a) :
     EqOn f g (Icc a b) :=
   have hfs : ∀ t ∈ Ico a b, f t ∈ @univ E := fun _ _ => trivial
-  ODE_solution_unique_of_mem_set (fun t => (hv t).lipschitzOnWith _) hf hf' hfs hg hg'
+  ODE_solution_unique_of_mem_Icc_right (fun t => (hv t).lipschitzOnWith _) hf hf' hfs hg hg'
     (fun _ _ => trivial) ha
 set_option linter.uppercaseLean3 false in
 #align ODE_solution_unique ODE_solution_unique