α : Type ?u.1232352
β : Type ?u.1232355
ι : Type ?u.1232358
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
h1 : Summable fun n => ‖x‖ ^ n
⊢ Summable fun n => x ^ n
α : Type ?u.1232352
β : Type ?u.1232355
ι : Type ?u.1232358
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ Summable fun n => x ^ n
have h1 : Summable fun n : ℕ ↦ ‖x‖ ^ n := summable_geometric_of_lt_1 (norm_nonneg _) h
α : Type ?u.1232352
β : Type ?u.1232355
ι : Type ?u.1232358
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
h1 : Summable fun n => ‖x‖ ^ n
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖x ^ i‖ ≤ ‖x‖ ^ i
α : Type ?u.1232352
β : Type ?u.1232355
ι : Type ?u.1232358
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
h1 : Summable fun n => ‖x‖ ^ n
⊢ Summable fun n => x ^ n
refine' summable_of_norm_bounded_eventually _ h1 _
α : Type ?u.1232352
β : Type ?u.1232355
ι : Type ?u.1232358
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
h1 : Summable fun n => ‖x‖ ^ n
⊢ ∀ᶠ (i : ℕ) in atTop, ‖x ^ i‖ ≤ ‖x‖ ^ i
α : Type ?u.1232352
β : Type ?u.1232355
ι : Type ?u.1232358
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
h1 : Summable fun n => ‖x‖ ^ n
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖x ^ i‖ ≤ ‖x‖ ^ i
rw [Nat.cofinite_eq_atTop]
no goals
α : Type ?u.1232352
β : Type ?u.1232355
ι : Type ?u.1232358
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
h1 : Summable fun n => ‖x‖ ^ n
⊢ ∀ᶠ (i : ℕ) in atTop, ‖x ^ i‖ ≤ ‖x‖ ^ i
exact eventually_norm_pow_le x