English
A global integral curve is either injective or periodic with a positive period.
Русский
Глобальная интегральная кривая либо инъективна, либо периодична с положительным периодом.
LaTeX
$$$\mathrm{IsMIntegralCurve}(\gamma,w) \Rightarrow \mathrm{Xor'} (\exists T>0, \text{Periodic}(\gamma,T)) (\text{Injective}(\gamma)).$$$
Lean4
/-- A global integral curve is injective xor periodic with positive period. -/
theorem periodic_xor_injective [BoundarylessManifold I M] (hγ : IsMIntegralCurve γ 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
