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

Mathlib/Algebra/Periodic.lean

@@ -349,6 +349,13 @@ 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 any semiring of non-zero period is not injective. -/
+lemma Periodic.not_injective {R X : Type*} [Semiring R] {f : R → X} {c : R}
+    (hf : Periodic f c) (hc : c ≠ 0) : ¬ Injective f := by
+  rw [Injective]
+  push_neg
+  exact ⟨0, c, by rw [← hf 0, zero_add], hc.symm⟩
+
 /-! ### 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,33 @@ 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
 
+/-- A (global) integral curve is injective iff it is not periodic. -/
+lemma IsIntegralCurve.periodic_iff_not_injective [BoundarylessManifold I M]
+    (hγ : IsIntegralCurve γ v)
+    (hv : ContMDiff I I.tangent 1 (fun x => (⟨x, v x⟩ : TangentBundle I M))) :
+    (∃ T > 0, Periodic γ T) ↔ ¬Injective γ := by
+  constructor
+  · exact fun ⟨T, hT, hf⟩ ↦ hf.not_injective (ne_of_gt hT)
+  · intro h
+    rw [Injective] at h
+    push_neg at h
+    obtain ⟨t₁, t₂, heq, hne⟩ := h
+    refine ⟨|t₁ - t₂|, ?_, ?_⟩
+    · rw [gt_iff_lt, abs_pos, sub_ne_zero]
+      exact hne
+    · apply congrFun
+      by_cases hle : t₁ - t₂ < 0
+      · apply isIntegralCurve_Ioo_eq_of_contMDiff_boundaryless (t₀ := t₁) hv (hγ.comp_add _) hγ
+        simp [abs_of_neg hle, heq]
+      · apply isIntegralCurve_Ioo_eq_of_contMDiff_boundaryless (t₀ := t₂) hv (hγ.comp_add _) hγ
+        rw [not_lt] at hle
+        simp [abs_of_nonneg hle, heq]
+
+/-- A global integral curve is injective xor periodic. -/
+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 γ) :=
+  xor_iff_iff_not.mpr (hγ.periodic_iff_not_injective hv)
+
 end ExistUnique