[Merged by Bors] - feat: uniqueness of integral curves of a vector field on a manifold

Mathlib/Analysis/ODE/Gronwall.lean

@@ -233,7 +233,7 @@ 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}
+theorem ODE_solution_unique_of_mem_set_Icc_right {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)
@@ -242,17 +242,116 @@ theorem ODE_solution_unique_of_mem_set {v : ℝ → E → E} {s : ℝ → Set E}
   have := dist_le_of_trajectories_ODE_of_mem_set 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_set_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_set_Icc_left {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 ∈ 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_set_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_set_Icc {v : ℝ → E → E} {s : ℝ → Set E} {K : ℝ≥0}
+    (hv : ∀ t, LipschitzOnWith K (v t) (s t))
+    {f g : ℝ → E} {a b t₀ : ℝ} (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_set_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_set_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_set_Icc` for uniqueness in an open interval. -/
+theorem ODE_solution_unique_of_mem_set_Ioo {v : ℝ → E → E} {s : ℝ → Set E} {K : ℝ≥0}
+    (hv : ∀ t, LipschitzOnWith K (v t) (s t))
+    {f g : ℝ → E} {a b t₀ : ℝ} (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_set_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_set_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_mem_set_eventually {v : ℝ → E → E} {s : ℝ → Set E} {K : ℝ≥0}
+    (hv : ∀ t, LipschitzOnWith K (v t) (s t)) {f g : ℝ → E} {t₀ : ℝ}
+    (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_set_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`. -/
+a given initial value provided that the 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) :
     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_set_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