α : Type u_1
β : Type ?u.749948
ι : Type ?u.749951
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ dist (∑ x in Finset.range n, f x) a ≤ C * r ^ n / (1 - r)
α : Type u_1
β : Type ?u.749948
ι : Type ?u.749951
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ ‖∑ x in Finset.range n, f x - a‖ ≤ C * r ^ n / (1 - r)
rw [← dist_eq_norm]
case ha
α : Type u_1
β : Type ?u.749948
ι : Type ?u.749951
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ Tendsto (fun n => ∑ i in Finset.range n, f i) atTop (𝓝 a)
α : Type u_1
β : Type ?u.749948
ι : Type ?u.749951
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ dist (∑ x in Finset.range n, f x) a ≤ C * r ^ n / (1 - r)
apply dist_le_of_le_geometric_of_tendsto r C hr (dist_partial_sum_le_of_le_geometric hf)
no goals
case ha
α : Type u_1
β : Type ?u.749948
ι : Type ?u.749951
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ Tendsto (fun n => ∑ i in Finset.range n, f i) atTop (𝓝 a)
exact ha.tendsto_sum_nat