English
If along every point x in M there exists a local integral curve defined on some symmetric interval Ioo(−ε, ε) with uniform hv, then there exists a global integral curve γ with γ(0)=x through that point.
Русский
Если для каждой точки x в M существует локальная интегральная кривая на некотором симметричном интервале Ioo(−ε, ε) с общим hv, то существует глобальная интегральная кривая γ, проходящая через x в точке 0.
LaTeX
$$$\\exists \\gamma: \\mathbb{R}\\to M, \\gamma(0)=x \\land IsMIntegralCurve(\\gamma, v)$ given the local existence hypothesis$$
Lean4
/-- Let `γ` and `γ'` be integral curves defined on `Ioo a b` and `Ioo a' b'`, respectively. Then,
`piecewise (Ioo a b) γ γ'` is equal to `γ` and `γ'` in their respective domains.
`Set.piecewise_eqOn` shows the equality for `γ` by definition, while this lemma shows the equality
for `γ'` by the uniqueness of integral curves. -/
theorem eqOn_piecewise_of_isMIntegralCurveOn_Ioo [BoundarylessManifold I M]
(hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) {a b a' b' : ℝ}
(hγ : IsMIntegralCurveOn γ v (Ioo a b)) (hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')) (ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b')
(h : γ t₀ = γ' t₀) : EqOn (piecewise (Ioo a b) γ γ') γ' (Ioo a' b') :=
by
intro t ht
suffices H : EqOn γ γ' (Ioo (max a a') (min b b'))
by
by_cases hmem : t ∈ Ioo a b
· rw [piecewise, if_pos hmem]
apply H
simp [ht.1, ht.2, hmem.1, hmem.2]
· rw [piecewise, if_neg hmem]
apply
isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless _ hv
(hγ.mono (Ioo_subset_Ioo (le_max_left ..) (min_le_left ..)))
(hγ'.mono (Ioo_subset_Ioo (le_max_right ..) (min_le_right ..))) h
exact ⟨max_lt ht₀.1.1 ht₀.2.1, lt_min ht₀.1.2 ht₀.2.2⟩
