English
Let F be a normed ring with identity, k a natural number, and r ∈ F with ||r|| < 1. If u : N → F satisfies u =O_{atTop}(n^k), then the series ∑_{n≥0} ||u(n) r^n|| converges (is summable).
Русский
Пусть F — нормированное кольцо с единицей, k ∈ N и r ∈ F такое, что ||r|| < 1. Если последовательность u : N → F растет не быстрее чем n^k, то ряд ∑_{n≥0} ||u(n) r^n|| сходится.
LaTeX
$$$ \\|r\\| < 1,\\quad u =O_{\\mathrm{atTop}}(n^k) \\;\Rightarrow\\; \\sum_{n=0}^\infty \\|u(n) r^n\\| < \\infty. $$$
Lean4
/-- This is a version of `summable_norm_mul_geometric_of_norm_lt_one` for more general codomains. We
keep the original one due to import restrictions. -/
theorem summable_norm_mul_geometric_of_norm_lt_one' {F : Type*} [NormedRing F] [NormOneClass F] [NormMulClass F] {k : ℕ}
{r : F} (hr : ‖r‖ < 1) {u : ℕ → F} (hu : u =O[atTop] fun n ↦ ((n ^ k : ℕ) : F)) :
Summable fun n : ℕ ↦ ‖u n * r ^ n‖ :=
by
rcases exists_between hr with ⟨r', hrr', h⟩
apply summable_of_isBigO_nat (summable_geometric_of_lt_one ((norm_nonneg _).trans hrr'.le) h).norm
calc
fun n ↦ ‖(u n) * r ^ n‖
_ =O[atTop] fun n ↦ ‖u n‖ * ‖r‖ ^ n :=
by
apply (IsBigOWith.of_bound (c := ‖(1 : ℝ)‖) ?_).isBigO
filter_upwards [eventually_norm_pow_le r] with n hn
simp
_ =O[atTop] fun n ↦ ‖((n : F) ^ k)‖ * ‖r‖ ^ n := by
simpa [Nat.cast_pow] using
(isBigO_norm_left.mpr (isBigO_norm_right.mpr hu)).mul (isBigO_refl (fun n ↦ (‖r‖ ^ n)) atTop)
_ =O[atTop] fun n ↦ ‖r' ^ n‖ :=
by
convert
isBigO_norm_right.mpr
(isBigO_norm_left.mpr (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO)
simp only [norm_pow, norm_mul]
