English
For a ≠ 0, IsMIntegralCurveAt γ v t0 is equivalent to IsMIntegralCurveAt (γ ∘ (·*a)) (a•v) (t0 / a). This captures how integral-curve behavior scales with a time rescaling around t0.
Русский
Для a ≠ 0 IsMIntegralCurveAt γ v t0 эквивалентно IsMIntegralCurveAt (γ ∘ (·*a)) (a•v) (t0 / a).
LaTeX
$$$IsMIntegralCurveAt(\\gamma, v, t_0) \\iff IsMIntegralCurveAt(\\gamma \\circ (\\cdot * a), a \\cdot v, t_0 / a)$$$
Lean4
theorem comp_mul_ne_zero (hγ : IsMIntegralCurveAt γ v t₀) {a : ℝ} (ha : a ≠ 0) :
IsMIntegralCurveAt (γ ∘ (· * a)) (a • v) (t₀ / a) :=
by
rw [isMIntegralCurveAt_iff'] at *
obtain ⟨ε, hε, h⟩ := hγ
refine ⟨ε / |a|, by positivity, ?_⟩
convert h.comp_mul a
ext t
rw [mem_setOf_eq, Metric.mem_ball, Metric.mem_ball, Real.dist_eq, Real.dist_eq, lt_div_iff₀ (abs_pos.mpr ha), ←
abs_mul, sub_mul, div_mul_cancel₀ _ ha]
