[Merged by Bors] - feat: Integral curves are either injective or periodic

Mathlib/Algebra/Periodic.lean

@@ -349,6 +349,11 @@ theorem Periodic.lift_coe [AddGroup α] (h : Periodic f c) (a : α) :
   rfl
 #align function.periodic.lift_coe Function.Periodic.lift_coe
 
+/-- A periodic function `f : R → X` on a semiring (or, more generally, `AddZeroClass`)
+of non-zero period is not injective. -/
+lemma Periodic.not_injective {R X : Type*} [AddZeroClass R] {f : R → X} {c : R}
+    (hf : Periodic f c) (hc : c ≠ 0) : ¬ Injective f := fun h ↦ hc <| h hf.eq
+
 /-! ### Antiperiodicity -/
 
 /-- A function `f` is said to be `antiperiodic` with antiperiod `c` if for all `x`,

Mathlib/Geometry/Manifold/IntegralCurve.lean

@@ -60,7 +60,7 @@ integral curve, vector field, local existence, uniqueness
 
 open scoped Manifold Topology
 
-open Set
+open Function Set
 
 variable
   {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
@@ -193,8 +193,7 @@ section Translation
 lemma IsIntegralCurveOn.comp_add (hγ : IsIntegralCurveOn γ v s) (dt : ℝ) :
     IsIntegralCurveOn (γ ∘ (· + dt)) v { t | t + dt ∈ s } := by
   intros t ht
-  rw [Function.comp_apply,
-    ← ContinuousLinearMap.comp_id (ContinuousLinearMap.smulRight 1 (v (γ (t + dt))))]
+  rw [comp_apply, ← ContinuousLinearMap.comp_id (ContinuousLinearMap.smulRight 1 (v (γ (t + dt))))]
   apply HasMFDerivAt.comp t (hγ (t + dt) ht)
   refine ⟨(continuous_add_right _).continuousAt, ?_⟩
   simp only [mfld_simps, hasFDerivWithinAt_univ]
@@ -246,7 +245,7 @@ section Scaling
 lemma IsIntegralCurveOn.comp_mul (hγ : IsIntegralCurveOn γ v s) (a : ℝ) :
     IsIntegralCurveOn (γ ∘ (· * a)) (a • v) { t | t * a ∈ s } := by
   intros t ht
-  rw [Function.comp_apply, Pi.smul_apply, ← ContinuousLinearMap.smulRight_comp]
+  rw [comp_apply, Pi.smul_apply, ← ContinuousLinearMap.smulRight_comp]
   refine HasMFDerivAt.comp t (hγ (t * a) ht) ⟨(continuous_mul_right _).continuousAt, ?_⟩
   simp only [mfld_simps, hasFDerivWithinAt_univ]
   exact HasFDerivAt.mul_const' (hasFDerivAt_id _) _
@@ -501,4 +500,36 @@ theorem isIntegralCurve_Ioo_eq_of_contMDiff_boundaryless [BoundarylessManifold I
     (hγ : IsIntegralCurve γ v) (hγ' : IsIntegralCurve γ' v) (h : γ t₀ = γ' t₀) : γ = γ' :=
   isIntegralCurve_eq_of_contMDiff (fun _ ↦ BoundarylessManifold.isInteriorPoint I) hv hγ hγ' h
 
+/-- For a global integral curve `γ`, if it crosses itself at `a b : ℝ`, then it is periodic with
+period `a - b`. -/
+lemma IsIntegralCurve.periodic_of_eq [BoundarylessManifold I M]
+    (hγ : IsIntegralCurve γ v)
+    (hv : ContMDiff I I.tangent 1 (fun x => (⟨x, v x⟩ : TangentBundle I M)))
+    (heq : γ a = γ b) : Periodic γ (a - b) := by
+  intro t
+  apply congrFun <|
+    isIntegralCurve_Ioo_eq_of_contMDiff_boundaryless (t₀ := b) hv (hγ.comp_add _) hγ _
+  rw [comp_apply, add_sub_cancel'_right, heq]
+
+/-- A global integral curve is injective xor periodic with positive period. -/
+lemma IsIntegralCurve.periodic_xor_injective [BoundarylessManifold I M]
+    (hγ : IsIntegralCurve γ v)
+    (hv : ContMDiff I I.tangent 1 (fun x => (⟨x, v x⟩ : TangentBundle I M))) :
+    Xor' (∃ T > 0, Periodic γ T) (Injective γ) := by
+  rw [xor_iff_iff_not]
+  refine ⟨fun ⟨T, hT, hf⟩ ↦ hf.not_injective (ne_of_gt hT), ?_⟩
+  intro h
+  rw [Injective] at h
+  push_neg at h
+  obtain ⟨a, b, heq, hne⟩ := h
+  refine ⟨|a - b|, ?_, ?_⟩
+  · rw [gt_iff_lt, abs_pos, sub_ne_zero]
+    exact hne
+  · by_cases hab : a - b < 0
+    · rw [abs_of_neg hab, neg_sub]
+      exact hγ.periodic_of_eq hv heq.symm
+    · rw [not_lt] at hab
+      rw [abs_of_nonneg hab]
+      exact hγ.periodic_of_eq hv heq
+
 end ExistUnique