English
A variant of the above: over the set where |t|+1 lies in an interval, the shifted integral-curve extensions agree with each other on that set.
Русский
Вариант выше: на множестве, где |t|+1 попадает в интервал, сдвинутые продолжения интегральных кривых совпадают.
LaTeX
$$$EqOn(\\gamma( |t|+1) , \\gamma'( |t|+1), Ioo(-a,a))$ under the assumptions$$
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 global curve `γ_ext := fun t ↦ γ (|t| + 1) t` agrees
with each `γ a` on `Ioo (-a) a`. This will help us show that `γ_ext` is a global integral curve. -/
theorem eqOn_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)) {a : ℝ} :
EqOn (fun t ↦ γ (|t| + 1) t) (γ a) (Ioo (-a) a) :=
by
intro t ht
by_cases hlt : |t| + 1 < a
· exact eqOn_of_isMIntegralCurveOn_Ioo hv γ hγx hγ (by positivity) hlt.le (abs_lt.mp <| lt_add_one _)
·
exact
eqOn_of_isMIntegralCurveOn_Ioo hv γ hγx hγ (neg_lt_self_iff.mp <| lt_trans ht.1 ht.2) (not_lt.mp hlt) ht |>.symm
