English
If a function tends to infinity along a filter, multiplying by a positive constant on the left preserves the Tendsto to infinity.
Русский
Если функция растет до бесконечности вдоль фильтра, умножение слева на положительную константу сохраняет тенденцию к бесконечности.
LaTeX
$$$\text{If } hr>0 \text{ and } \mathrm{Tendsto}\ f\ l\ \mathrm{atTop},\; \mathrm{Tendsto}(x \mapsto r \cdot f(x))\ l\ \mathrm{atTop}$$$
Lean4
/-- If a function tends to infinity along a filter, then this function multiplied by a positive
constant (on the left) also tends to infinity. The archimedean assumption is convenient to get a
statement that works on `ℕ`, `ℤ` and `ℝ`, although not necessary (a version in ordered fields is
given in `Filter.Tendsto.const_mul_atTop`). -/
theorem const_mul_atTop' (hr : 0 < r) (hf : Tendsto f l atTop) : Tendsto (fun x => r * f x) l atTop :=
by
refine tendsto_atTop.2 fun b => ?_
obtain ⟨n : ℕ, hn : 1 ≤ n • r⟩ := Archimedean.arch 1 hr
rw [nsmul_eq_mul'] at hn
filter_upwards [tendsto_atTop.1 hf (n * max b 0)] with x hx
calc
b ≤ 1 * max b 0 := by {
rw [one_mul]
exact le_max_left _ _
}
_ ≤ r * n * max b 0 := by gcongr
_ = r * (n * max b 0) := by rw [mul_assoc]
_ ≤ r * f x := by gcongr
