theorem summable_real_norm_mul_geometric_of_norm_lt_one {k : ℕ} {r : ℂ} (hr : ‖r‖ < 1) {u : ℕ → ℂ} (hu : u =O[Filter.atTop] fun (n : ℕ) => ↑(n ^ k)) : Summable fun (n : ℕ) => ‖u n * r ^ n‖