chore: rename IsIntegralCurve to IsMIntegralCurve (leanprover-community#26563)

I rename all the existing `IsIntegralCurve` series of definitions and lemmas for manifolds to `IsMIntegralCurve` in preparation for reusing `IsIntegralCurve` for the vector space version.

- [x] depends on: leanprover-community#26533

Author: winstonyin

Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean

@@ -23,16 +23,20 @@ This is the first of a series of files, organised as follows:
 ## Main definitions
 
 Let `v : M → TM` be a vector field on `M`, and let `γ : ℝ → M`.
-* `IsIntegralCurve γ v`: `γ t` is tangent to `v (γ t)` for all `t : ℝ`. That is, `γ` is a global
+* `IsMIntegralCurve γ v`: `γ t` is tangent to `v (γ t)` for all `t : ℝ`. That is, `γ` is a global
   integral curve of `v`.
-* `IsIntegralCurveOn γ v s`: `γ t` is tangent to `v (γ t)` for all `t ∈ s`, where `s : Set ℝ`.
-* `IsIntegralCurveAt γ v t₀`: `γ t` is tangent to `v (γ t)` for all `t` in some open interval
+* `IsMIntegralCurveOn γ v s`: `γ t` is tangent to `v (γ t)` for all `t ∈ s`, where `s : Set ℝ`.
+* `IsMIntegralCurveAt γ v t₀`: `γ t` is tangent to `v (γ t)` for all `t` in some open interval
   around `t₀`. That is, `γ` is a local integral curve of `v`.
 
-For `IsIntegralCurveOn γ v s` and `IsIntegralCurveAt γ v t₀`, even though `γ` is defined for all
+For `IsMIntegralCurveOn γ v s` and `IsMIntegralCurveAt γ v t₀`, even though `γ` is defined for all
 time, its value outside of the set `s` or a small interval around `t₀` is irrelevant and considered
 junk.
 
+## TODO
+
+* Implement `IsMIntegralCurveWithinAt`.
+
 ## Reference
 
 * [Lee, J. M. (2012). _Introduction to Smooth Manifolds_. Springer New York.][lee2012]
@@ -52,51 +56,66 @@ variable
   {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
 
 /-- If `γ : ℝ → M` is $C^1$ on `s : Set ℝ` and `v` is a vector field on `M`,
-`IsIntegralCurveOn γ v s` means `γ t` is tangent to `v (γ t)` within `s` for all `t ∈ s`. The value
-of `γ` outside of `s` is irrelevant and considered junk. -/
-def IsIntegralCurveOn (γ : ℝ → M) (v : (x : M) → TangentSpace I x) (s : Set ℝ) : Prop :=
+`IsMIntegralCurveOn γ v s` means `γ t` is tangent to `v (γ t)` for all `t ∈ s`. The value of `γ`
+outside of `s` is irrelevant and considered junk. -/
+def IsMIntegralCurveOn (γ : ℝ → M) (v : (x : M) → TangentSpace I x) (s : Set ℝ) : Prop :=
   ∀ t ∈ s, HasMFDerivWithinAt 𝓘(ℝ, ℝ) I γ s t ((1 : ℝ →L[ℝ] ℝ).smulRight <| v (γ t))
 
-/-- If `v` is a vector field on `M` and `t₀ : ℝ`, `IsIntegralCurveAt γ v t₀` means `γ : ℝ → M` is a
+@[deprecated (since := "2025-08-12")] alias IsIntegralCurveOn := IsMIntegralCurveOn
+
+/-- If `v` is a vector field on `M` and `t₀ : ℝ`, `IsMIntegralCurveAt γ v t₀` means `γ : ℝ → M` is a
 local integral curve of `v` in a neighbourhood containing `t₀`. The value of `γ` outside of this
-neighbourhood is irrelevant and considered junk. -/
-def IsIntegralCurveAt (γ : ℝ → M) (v : (x : M) → TangentSpace I x) (t₀ : ℝ) : Prop :=
+interval is irrelevant and considered junk. -/
+def IsMIntegralCurveAt (γ : ℝ → M) (v : (x : M) → TangentSpace I x) (t₀ : ℝ) : Prop :=
   ∀ᶠ t in 𝓝 t₀, HasMFDerivAt 𝓘(ℝ, ℝ) I γ t ((1 : ℝ →L[ℝ] ℝ).smulRight <| v (γ t))
 
-/-- If `v : M → TM` is a vector field on `M`, `IsIntegralCurve γ v` means `γ : ℝ → M` is a global
+@[deprecated (since := "2025-08-12")] alias IsIntegralCurveAt := IsMIntegralCurveAt
+
+/-- If `v : M → TM` is a vector field on `M`, `IsMIntegralCurve γ v` means `γ : ℝ → M` is a global
 integral curve of `v`. That is, `γ t` is tangent to `v (γ t)` for all `t : ℝ`. -/
-def IsIntegralCurve (γ : ℝ → M) (v : (x : M) → TangentSpace I x) : Prop :=
+def IsMIntegralCurve (γ : ℝ → M) (v : (x : M) → TangentSpace I x) : Prop :=
   ∀ t : ℝ, HasMFDerivAt 𝓘(ℝ, ℝ) I γ t ((1 : ℝ →L[ℝ] ℝ).smulRight (v (γ t)))
 
+@[deprecated (since := "2025-08-12")] alias IsIntegralCurve := IsMIntegralCurve
+
 variable {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} {s s' : Set ℝ} {t₀ : ℝ}
 
-lemma IsIntegralCurve.isIntegralCurveOn (h : IsIntegralCurve γ v) (s : Set ℝ) :
-    IsIntegralCurveOn γ v s := fun t _ ↦ (h t).hasMFDerivWithinAt
+lemma IsMIntegralCurve.isMIntegralCurveOn (h : IsMIntegralCurve γ v) (s : Set ℝ) :
+    IsMIntegralCurveOn γ v s := fun t _ ↦ (h t).hasMFDerivWithinAt
 
-lemma isIntegralCurve_iff_isIntegralCurveOn : IsIntegralCurve γ v ↔ IsIntegralCurveOn γ v univ :=
-  ⟨fun h ↦ h.isIntegralCurveOn _, fun h t ↦ (h t (mem_univ _)).hasMFDerivAt Filter.univ_mem⟩
+@[deprecated (since := "2025-08-12")] alias IsIntegralCurve.isIntegralCurveOn :=
+  IsMIntegralCurve.isMIntegralCurveOn
 
-lemma isIntegralCurveAt_iff :
-    IsIntegralCurveAt γ v t₀ ↔ ∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s := by
+lemma isMIntegralCurve_iff_isMIntegralCurveOn :
+    IsMIntegralCurve γ v ↔ IsMIntegralCurveOn γ v univ :=
+  ⟨fun h ↦ h.isMIntegralCurveOn _, fun h t ↦ (h t (mem_univ _)).hasMFDerivAt Filter.univ_mem⟩
+
+@[deprecated (since := "2025-08-12")] alias isIntegralCurve_iff_isIntegralCurveOn :=
+  isMIntegralCurve_iff_isMIntegralCurveOn
+
+lemma isMIntegralCurveAt_iff :
+    IsMIntegralCurveAt γ v t₀ ↔ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s := by
   constructor
   · intro h
-    rw [IsIntegralCurveAt, Filter.eventually_iff_exists_mem] at h
+    rw [IsMIntegralCurveAt, Filter.eventually_iff_exists_mem] at h
     obtain ⟨s, hs, h⟩ := h
     exact ⟨s, hs, fun t ht ↦ (h t ht).hasMFDerivWithinAt⟩
   · rintro ⟨s, hs, h⟩
-    rw [IsIntegralCurveAt, Filter.eventually_iff_exists_mem]
+    rw [IsMIntegralCurveAt, Filter.eventually_iff_exists_mem]
     obtain ⟨s', h1, h2, h3⟩ := mem_nhds_iff.mp hs
     refine ⟨s', h2.mem_nhds h3, ?_⟩
     intro t ht
     apply (h t (h1 ht)).hasMFDerivAt
     rw [mem_nhds_iff]
     exact ⟨s', h1, h2, ht⟩
 
+@[deprecated (since := "2025-08-12")] alias isIntegralCurveAt_iff := isMIntegralCurveAt_iff
+
 /-- `γ` is an integral curve for `v` at `t₀` iff `γ` is an integral curve on some interval
 containing `t₀`. -/
-lemma isIntegralCurveAt_iff' :
-    IsIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε) := by
-  rw [isIntegralCurveAt_iff]
+lemma isMIntegralCurveAt_iff' :
+    IsMIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε) := by
+  rw [isMIntegralCurveAt_iff]
   constructor
   · intro ⟨s, hs, h⟩
     rw [Metric.mem_nhds_iff] at hs
@@ -105,61 +124,95 @@ lemma isIntegralCurveAt_iff' :
   · intro ⟨ε, hε, h⟩
     exact ⟨Metric.ball t₀ ε, Metric.ball_mem_nhds _ hε, h⟩
 
-lemma IsIntegralCurve.isIntegralCurveAt (h : IsIntegralCurve γ v) (t : ℝ) :
-    IsIntegralCurveAt γ v t :=
-  isIntegralCurveAt_iff.mpr ⟨univ, Filter.univ_mem, fun t _ ↦ (h t).hasMFDerivWithinAt⟩
+@[deprecated (since := "2025-08-12")] alias isIntegralCurveAt_iff' := isMIntegralCurveAt_iff'
+
+lemma IsMIntegralCurve.isMIntegralCurveAt (h : IsMIntegralCurve γ v) (t : ℝ) :
+    IsMIntegralCurveAt γ v t :=
+  isMIntegralCurveAt_iff.mpr ⟨univ, Filter.univ_mem, fun t _ ↦ (h t).hasMFDerivWithinAt⟩
+
+@[deprecated (since := "2025-08-12")] alias IsIntegralCurve.isIntegralCurveAt :=
+  IsMIntegralCurve.isMIntegralCurveAt
 
-lemma isIntegralCurve_iff_isIntegralCurveAt :
-    IsIntegralCurve γ v ↔ ∀ t : ℝ, IsIntegralCurveAt γ v t :=
-  ⟨fun h ↦ h.isIntegralCurveAt, fun h t ↦ by
-    obtain ⟨s, hs, h⟩ := isIntegralCurveAt_iff.mp (h t)
+lemma isMIntegralCurve_iff_isMIntegralCurveAt :
+    IsMIntegralCurve γ v ↔ ∀ t : ℝ, IsMIntegralCurveAt γ v t :=
+  ⟨fun h ↦ h.isMIntegralCurveAt, fun h t ↦ by
+    obtain ⟨s, hs, h⟩ := isMIntegralCurveAt_iff.mp (h t)
     exact h t (mem_of_mem_nhds hs) |>.hasMFDerivAt hs⟩
 
-lemma IsIntegralCurveOn.mono (h : IsIntegralCurveOn γ v s) (hs : s' ⊆ s) :
-    IsIntegralCurveOn γ v s' := fun t ht ↦ (h t (hs ht)).mono hs
+@[deprecated (since := "2025-08-12")] alias isIntegralCurve_iff_isIntegralCurveAt :=
+  isMIntegralCurve_iff_isMIntegralCurveAt
 
-lemma IsIntegralCurveAt.hasMFDerivAt (h : IsIntegralCurveAt γ v t₀) :
+lemma IsMIntegralCurveOn.mono (h : IsMIntegralCurveOn γ v s) (hs : s' ⊆ s) :
+    IsMIntegralCurveOn γ v s' := fun t ht ↦ (h t (hs ht)).mono hs
+
+@[deprecated (since := "2025-08-12")] alias IsIntegralCurveOn.mono :=
+  IsMIntegralCurveOn.mono
+
+lemma IsMIntegralCurveAt.hasMFDerivAt (h : IsMIntegralCurveAt γ v t₀) :
     HasMFDerivAt 𝓘(ℝ, ℝ) I γ t₀ ((1 : ℝ →L[ℝ] ℝ).smulRight (v (γ t₀))) :=
-  have ⟨_, hs, h⟩ := isIntegralCurveAt_iff.mp h
+  have ⟨_, hs, h⟩ := isMIntegralCurveAt_iff.mp h
   h t₀ (mem_of_mem_nhds hs) |>.hasMFDerivAt hs
 
-lemma IsIntegralCurveOn.isIntegralCurveAt (h : IsIntegralCurveOn γ v s) (hs : s ∈ 𝓝 t₀) :
-    IsIntegralCurveAt γ v t₀ := isIntegralCurveAt_iff.mpr ⟨s, hs, h⟩
+@[deprecated (since := "2025-08-12")] alias IsIntegralCurveAt.hasMFDerivAt :=
+  IsMIntegralCurveAt.hasMFDerivAt
+
+lemma IsMIntegralCurveOn.isMIntegralCurveAt (h : IsMIntegralCurveOn γ v s) (hs : s ∈ 𝓝 t₀) :
+    IsMIntegralCurveAt γ v t₀ := isMIntegralCurveAt_iff.mpr ⟨s, hs, h⟩
+
+@[deprecated (since := "2025-08-12")] alias IsIntegralCurveOn.isIntegralCurveAt :=
+  IsMIntegralCurveOn.isMIntegralCurveAt
 
 /-- If `γ` is an integral curve at each `t ∈ s`, it is an integral curve on `s`. -/
-lemma IsIntegralCurveAt.isIntegralCurveOn (h : ∀ t ∈ s, IsIntegralCurveAt γ v t) :
-    IsIntegralCurveOn γ v s := by
+lemma IsMIntegralCurveAt.isMIntegralCurveOn (h : ∀ t ∈ s, IsMIntegralCurveAt γ v t) :
+    IsMIntegralCurveOn γ v s := by
   intros t ht
   apply HasMFDerivAt.hasMFDerivWithinAt
   obtain ⟨s', hs', h⟩ := Filter.eventually_iff_exists_mem.mp (h t ht)
   exact h _ (mem_of_mem_nhds hs')
 
-lemma isIntegralCurveOn_iff_isIntegralCurveAt (hs : IsOpen s) :
-    IsIntegralCurveOn γ v s ↔ ∀ t ∈ s, IsIntegralCurveAt γ v t :=
-  ⟨fun h _ ht ↦ h.isIntegralCurveAt (hs.mem_nhds ht), IsIntegralCurveAt.isIntegralCurveOn⟩
+@[deprecated (since := "2025-08-12")] alias IsIntegralCurveAt.isIntegralCurveOn :=
+  IsMIntegralCurveAt.isMIntegralCurveOn
+
+lemma isMIntegralCurveOn_iff_isMIntegralCurveAt (hs : IsOpen s) :
+    IsMIntegralCurveOn γ v s ↔ ∀ t ∈ s, IsMIntegralCurveAt γ v t :=
+  ⟨fun h _ ht ↦ h.isMIntegralCurveAt (hs.mem_nhds ht), IsMIntegralCurveAt.isMIntegralCurveOn⟩
 
-lemma IsIntegralCurveOn.continuousWithinAt (hγ : IsIntegralCurveOn γ v s) (ht : t₀ ∈ s) :
+@[deprecated (since := "2025-08-12")] alias isIntegralCurveOn_iff_isIntegralCurveAt :=
+  isMIntegralCurveOn_iff_isMIntegralCurveAt
+
+lemma IsMIntegralCurveOn.continuousWithinAt (hγ : IsMIntegralCurveOn γ v s) (ht : t₀ ∈ s) :
     ContinuousWithinAt γ s t₀ := (hγ t₀ ht).1
 
-@[deprecated (since := "2025-06-29")] alias IsIntegralCurveOn.continuousAt :=
-  IsIntegralCurveOn.continuousWithinAt
+@[deprecated (since := "2025-08-12")] alias IsIntegralCurveOn.continuousAt :=
+  IsMIntegralCurveOn.continuousWithinAt
+@[deprecated (since := "2025-08-12")] alias IsIntegralCurveOn.continuousWithinAt :=
+  IsMIntegralCurveOn.continuousWithinAt
 
-lemma IsIntegralCurveOn.continuousOn (hγ : IsIntegralCurveOn γ v s) :
+lemma IsMIntegralCurveOn.continuousOn (hγ : IsMIntegralCurveOn γ v s) :
     ContinuousOn γ s := fun t ht ↦ (hγ t ht).continuousWithinAt
 
-lemma IsIntegralCurveAt.continuousAt (hγ : IsIntegralCurveAt γ v t₀) :
+@[deprecated (since := "2025-08-12")] alias IsIntegralCurveOn.continuousOn :=
+  IsMIntegralCurveOn.continuousOn
+
+lemma IsMIntegralCurveAt.continuousAt (hγ : IsMIntegralCurveAt γ v t₀) :
     ContinuousAt γ t₀ :=
-  have ⟨_, hs, hγ⟩ := isIntegralCurveAt_iff.mp hγ
+  have ⟨_, hs, hγ⟩ := isMIntegralCurveAt_iff.mp hγ
   hγ.continuousWithinAt (mem_of_mem_nhds hs) |>.continuousAt hs
 
-lemma IsIntegralCurve.continuous (hγ : IsIntegralCurve γ v) : Continuous γ :=
-  continuous_iff_continuousAt.mpr fun t ↦ (hγ.isIntegralCurveAt t).continuousAt
+@[deprecated (since := "2025-08-12")] alias IsIntegralCurveAt.continuousAt :=
+  IsMIntegralCurveAt.continuousAt
+
+lemma IsMIntegralCurve.continuous (hγ : IsMIntegralCurve γ v) : Continuous γ :=
+  continuous_iff_continuousAt.mpr fun t ↦ (hγ.isMIntegralCurveAt t).continuousAt
+
+@[deprecated (since := "2025-08-12")] alias IsIntegralCurve.continuous :=
+  IsMIntegralCurve.continuous
 
 variable [IsManifold I 1 M]
 
 /-- If `γ` is an integral curve of a vector field `v`, then `γ t` is tangent to `v (γ t)` when
 expressed in the local chart around the initial point `γ t₀`. -/
-lemma IsIntegralCurveOn.hasDerivWithinAt (hγ : IsIntegralCurveOn γ v s) {t : ℝ} (ht : t ∈ s)
+lemma IsMIntegralCurveOn.hasDerivWithinAt (hγ : IsMIntegralCurveOn γ v s) {t : ℝ} (ht : t ∈ s)
     (hsrc : γ t ∈ (extChartAt I (γ t₀)).source) :
     HasDerivWithinAt ((extChartAt I (γ t₀)) ∘ γ)
       (tangentCoordChange I (γ t) (γ t₀) (γ t) (v (γ t))) s t := by
@@ -175,10 +228,10 @@ lemma IsIntegralCurveOn.hasDerivWithinAt (hγ : IsIntegralCurveOn γ v s) {t : 
     mfderiv_chartAt_eq_tangentCoordChange hsrc]
   rfl
 
-@[deprecated (since := "2025-06-29")] alias IsIntegralCurveOn.hasDerivAt :=
-  IsIntegralCurveOn.hasDerivWithinAt
+@[deprecated (since := "2025-08-12")] alias IsIntegralCurveOn.hasDerivWithinAt :=
+  IsMIntegralCurveOn.hasDerivWithinAt
 
-lemma IsIntegralCurveAt.eventually_hasDerivAt (hγ : IsIntegralCurveAt γ v t₀) :
+lemma IsMIntegralCurveAt.eventually_hasDerivAt (hγ : IsMIntegralCurveAt γ v t₀) :
     ∀ᶠ t in 𝓝 t₀, HasDerivAt ((extChartAt I (γ t₀)) ∘ γ)
       (tangentCoordChange I (γ t) (γ t₀) (γ t) (v (γ t))) t := by
   apply eventually_mem_nhds_iff.mpr
@@ -194,3 +247,6 @@ lemma IsIntegralCurveAt.eventually_hasDerivAt (hγ : IsIntegralCurveAt γ v t₀
     ← ContinuousLinearMap.one_apply (R₁ := ℝ) a, ← ContinuousLinearMap.smulRight_apply,
     mfderiv_chartAt_eq_tangentCoordChange hsrc]
   rfl
+
+@[deprecated (since := "2025-08-12")] alias IsIntegralCurveAt.eventually_hasDerivAt :=
+  IsMIntegralCurveAt.eventually_hasDerivAt