English
If two integral-curveOn objects γ and γ' are defined on overlapping Ioo intervals, then their piecewise combination on the union is again an integral-curveOn for the same velocity field, provided they agree on the overlap point.
Русский
Если γ и γ' заданы на перекрывающихся интервалах Ioo, их кусочно-замкнутая кривая на объединение — снова интегральная кривая того же поля скорости, при условии согласия на пересечении.
LaTeX
$$$\\text{IsMIntegralCurveOn}((Ioo a b).piecewise γ γ') v (Ioo a b \\cup Ioo a' b')$ under the stated hypotheses$$
Lean4
/-- For a family of integral curves `γ : ℝ → ℝ → M` with the same starting point `γ 0 = x` such that
each `γ a` is defined on `Ioo (-a) a`, the function `γ_ext := fun t ↦ γ (|t| + 1) t` is a global
integral curve. -/
theorem isMIntegralCurve_abs_add_one_of_isMIntegralCurveOn_Ioo [BoundarylessManifold I M]
(hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) {x : M} (γ : ℝ → ℝ → M)
(hγx : ∀ a, γ a 0 = x) (hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)) :
IsMIntegralCurve (fun t ↦ γ (|t| + 1) t) v := by
intro t
have ht : t ∈ Ioo (-(|t| + 1)) (|t| + 1) := by
rw [mem_Ioo, ← abs_lt]
exact lt_add_one _
apply HasMFDerivAt.congr_of_eventuallyEq (f := γ (|t| + 1))
· exact hγ (|t| + 1) (by positivity) _ ht |>.hasMFDerivAt (Ioo_mem_nhds ht.1 ht.2)
· rw [Filter.eventuallyEq_iff_exists_mem]
refine ⟨Ioo (-(|t| + 1)) (|t| + 1), ?_, eqOn_abs_add_one_of_isMIntegralCurveOn_Ioo hv γ hγx hγ⟩
have : |t| < |t| + 1 := lt_add_of_pos_right |t| zero_lt_one
rw [abs_lt] at this
exact Ioo_mem_nhds this.1 this.2
