English
For IsMIntegralCurveOn γ v defined on a time set s, scaling time by a real a yields IsMIntegralCurveOn (γ ∘ (·*a)) (a•v) on the scaled set {t | t*a ∈ s}. This describes how local integral curves transform under time dilation.
Русский
Для IsMIntegralCurveOn γ v на времени s масштабирование времени на a приводит к IsMIntegralCurveOn (γ ∘ (·*a)) (a•v) на множестве {t | t*a ∈ s}. Это описывает преобразование локальных интегральных кривых при временном замедлении/ускорении.
LaTeX
$$$IsMIntegralCurveOn(\\gamma, v, s) \\rightarrow IsMIntegralCurveOn(\\gamma \\circ (\\cdot * a), a \\cdot v, {t \\mid t * a \\in s})$$$
Lean4
theorem comp_mul (hγ : IsMIntegralCurveOn γ v s) (a : ℝ) : IsMIntegralCurveOn (γ ∘ (· * a)) (a • v) {t | t * a ∈ s} :=
by
intro t ht
rw [comp_apply, Pi.smul_apply, ← ContinuousLinearMap.smulRight_comp]
refine HasMFDerivWithinAt.comp t (hγ (t * a) ht) ⟨(continuous_mul_right _).continuousWithinAt, ?_⟩ subset_rfl
simp only [mfld_simps]
exact HasFDerivWithinAt.mul_const' (hasFDerivWithinAt_id _ _) _
