English
Suppose γ and γ' are integral curves on Ioo intervals with a common point; then the piecewise γ on their union is an integral curve with the same velocity field.
Русский
Пусть γ и γ' — интегральные кривые на интервалах Ioo с общей точкой; тогда кусочная кривая на их объединении является интегральной кривой с тем же полем скорости.
LaTeX
$$$IsMIntegralCurveOn(\\text{piecewise}(Ioo a b) γ γ') v (Ioo a b \\cup Ioo a' b')$$$
Lean4
/-- If there exists `ε > 0` such that the local integral curve at each point `x : M` is defined at
least on an open interval `Ioo (-ε) ε`, then every point on `M` has a global integral curve
passing through it.
See Lemma 9.15, [J.M. Lee (2012)][lee2012]. -/
theorem exists_isMIntegralCurve_of_isMIntegralCurveOn [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x}
(hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) {ε : ℝ} (hε : 0 < ε)
(h : ∀ x : M, ∃ γ : ℝ → M, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)) (x : M) :
∃ γ : ℝ → M, γ 0 = x ∧ IsMIntegralCurve γ v :=
by
let s := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
suffices hbdd : ¬BddAbove s by
rw [not_bddAbove_iff] at hbdd
rw [exists_isMIntegralCurve_iff_exists_isMIntegralCurveOn_Ioo hv]
intro a
obtain ⟨y, ⟨γ, hγ1, hγ2⟩, hlt⟩ := hbdd a
exact ⟨γ, hγ1, hγ2.mono <| Ioo_subset_Ioo (neg_le_neg hlt.le) hlt.le⟩
intro hbdd
set asup := sSup s with hasup
obtain ⟨a, ha, hlt⟩ :=
Real.add_neg_lt_sSup (⟨ε, h x⟩ : Set.Nonempty s) (ε := -(ε / 2)) (by rw [neg_lt, neg_zero]; exact half_pos hε)
rw [mem_setOf] at ha
rw [← hasup, ← sub_eq_add_neg] at hlt
obtain ⟨γ, h0, hγ⟩ := ha
obtain ⟨γ1_aux, h1_aux, hγ1⟩ := h (γ (-(asup - ε / 2)))
rw [isMIntegralCurveOn_comp_add (dt := asup - ε / 2)] at hγ1
set γ1 := γ1_aux ∘ (· + (asup - ε / 2)) with γ1_def
have heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2)) := by
simp [γ1_def, h1_aux]
-- integral curve starting at `asup - ε / 2` with radius `ε`
obtain ⟨γ2_aux, h2_aux, hγ2⟩ := h (γ (asup - ε / 2))
rw [isMIntegralCurveOn_comp_sub (dt := asup - ε / 2)] at hγ2
set γ2 := γ2_aux ∘ (· - (asup - ε / 2)) with γ2_def
have heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2) := by
simp [γ2_def, h2_aux]
-- rewrite shifted Ioo as Ioo
simp_rw [Set.mem_Ioo, ← sub_lt_iff_lt_add, ← lt_sub_iff_add_lt, ← Set.mem_Ioo] at hγ1
simp_rw [Set.mem_Ioo, lt_sub_iff_add_lt, sub_lt_iff_lt_add, ← Set.mem_Ioo] at hγ2
have hεle : ε ≤ asup :=
le_csSup hbdd
(h x)
-- extend `γ` on the left by `γ1` and on the right by `γ2`
set γ_ext : ℝ → M := piecewise (Ioo (-(asup + ε / 2)) a) (piecewise (Ioo (-a) a) γ γ1) γ2 with γ_ext_def
have heq_ext : γ_ext 0 = x := by
rw [γ_ext_def, piecewise, if_pos ⟨by linarith, by linarith⟩, piecewise, if_pos ⟨by linarith, by linarith⟩, h0]
-- `asup + ε / 2` is an element of `s` greater than `asup`, a contradiction
suffices hext : IsMIntegralCurveOn γ_ext v (Ioo (-(asup + ε / 2)) (asup + ε / 2)) from
(not_lt.mpr <| le_csSup hbdd ⟨γ_ext, heq_ext, hext⟩) <| lt_add_of_pos_right asup (half_pos hε)
apply
(isMIntegralCurveOn_piecewise (t₀ := asup - ε / 2) hv _ hγ2 ⟨⟨by linarith, hlt⟩, ⟨by linarith, by linarith⟩⟩
(by rw [piecewise, if_pos ⟨by linarith, hlt⟩, ← heq2])).mono
(Ioo_subset_Ioo_union_Ioo le_rfl (by linarith) (by linarith))
exact
(isMIntegralCurveOn_piecewise (t₀ := -(asup - ε / 2)) hv hγ hγ1
⟨⟨neg_lt_neg hlt, by linarith⟩, ⟨by linarith, by linarith⟩⟩ heq1.symm).mono
(union_comm _ _ ▸ Ioo_subset_Ioo_union_Ioo (by linarith) (by linarith) le_rfl)
