English
If ∥r∥ < 1 and a sequence u(n) grows at most polynomially, then ∑ ∥u(n) r^n∥ converges (is summable).
Русский
Пусть ∥r∥ < 1 и последовательность u(n) растёт не быстрее полиномиального; тогда ∑ ∥u(n) r^n∥ сходится.
LaTeX
$$∥r∥ < 1 ∧ (fun n => (u n : ℝ)) =O[atTop] (fun n => ↑(n^k)) ⇒ Summable fun n => ∥u(n) r^n∥$$
Lean4
theorem summable_norm_mul_geometric_of_norm_lt_one {k : ℕ} {r : R} (hr : ‖r‖ < 1) {u : ℕ → ℕ}
(hu : (fun n ↦ (u n : ℝ)) =O[atTop] (fun n ↦ (↑(n ^ k) : ℝ))) : Summable fun n : ℕ ↦ ‖(u n * r ^ n : R)‖ :=
by
rcases exists_between hr with ⟨r', hrr', h⟩
rw [← norm_norm] at hrr'
apply summable_of_isBigO_nat (summable_geometric_of_lt_one ((norm_nonneg _).trans hrr'.le) h)
calc
fun n ↦ ‖↑(u n) * r ^ n‖
_ =O[atTop] fun n ↦ u n * ‖r‖ ^ n :=
by
apply (IsBigOWith.of_bound (c := ‖(1 : R)‖) ?_).isBigO
filter_upwards [eventually_norm_pow_le r] with n hn
simp only [norm_mul, Real.norm_eq_abs, abs_cast, norm_pow, abs_norm]
apply (norm_mul_le _ _).trans
have : ‖(u n : R)‖ * ‖r ^ n‖ ≤ (u n * ‖(1 : R)‖) * ‖r‖ ^ n := by gcongr; exact norm_cast_le (u n)
exact this.trans (le_of_eq (by ring))
_ =O[atTop] fun n ↦ ↑(n ^ k) * ‖r‖ ^ n := (hu.mul (isBigO_refl _ _))
_ =O[atTop] fun n ↦ r' ^ n := by
simp only [cast_pow]
exact (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO
