Skip to content

Commit

Permalink
feat: Integral curves are either injective or periodic (#9343)
Browse files Browse the repository at this point in the history
Integral curves are either injective, constant, or periodic and non-constant.

When we have notions of submanifolds, this'll be useful for showing that the image of an integral curve is a submanifold.

- [x] depends on: #8886


Co-authored-by: Yury G. Kudryashov <[email protected]>
Co-authored-by: Michael Rothgang <[email protected]>
  • Loading branch information
3 people committed Jan 30, 2024
1 parent b4d01dc commit 132e511
Show file tree
Hide file tree
Showing 2 changed files with 40 additions and 4 deletions.
5 changes: 5 additions & 0 deletions Mathlib/Algebra/Periodic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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`,
Expand Down
39 changes: 35 additions & 4 deletions Mathlib/Geometry/Manifold/IntegralCurve.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down Expand Up @@ -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]
Expand Down Expand Up @@ -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 _) _
Expand Down Expand Up @@ -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

0 comments on commit 132e511

Please sign in to comment.