α : Type ?u.1865526
β : Type ?u.1865529
ι : Type ?u.1865532
E : Type ?u.1865535
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n => ∑ x in Finset.range (n + 1), f x * (-1) ^ x
α : Type ?u.1865526
β : Type ?u.1865529
ι : Type ?u.1865532
E : Type ?u.1865535
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n => ∑ i in Finset.range (n + 1), (-1) ^ i * f i
simp_rw [mul_comm]
no goals
α : Type ?u.1865526
β : Type ?u.1865529
ι : Type ?u.1865532
E : Type ?u.1865535
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n => ∑ x in Finset.range (n + 1), f x * (-1) ^ x
exact hfa.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le