α : Type ?u.1506622
β : Type ?u.1506625
ι : Type ?u.1506628
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
hfa' : Monotone fun n => -f n
⊢ CauchySeq fun n => ∑ i in Finset.range (n + 1), f i • z i
α : Type ?u.1506622
β : Type ?u.1506625
ι : Type ?u.1506628
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n => ∑ i in Finset.range (n + 1), f i • z i
have hfa' : Monotone fun n ↦ -f n := fun _ _ hab ↦ neg_le_neg <| hfa hab
α : Type ?u.1506622
β : Type ?u.1506625
ι : Type ?u.1506628
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
hfa' : Monotone fun n => -f n
hf0' : Tendsto (fun n => -f n) atTop (𝓝 0)
⊢ CauchySeq fun n => ∑ i in Finset.range (n + 1), f i • z i
α : Type ?u.1506622
β : Type ?u.1506625
ι : Type ?u.1506628
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
hfa' : Monotone fun n => -f n
⊢ CauchySeq fun n => ∑ i in Finset.range (n + 1), f i • z i
have hf0' : Tendsto (fun n ↦ -f n) atTop (𝓝 0) := by
  convert hf0.neg
  norm_num
case h.e'_5.h
α : Type ?u.1506622
β : Type ?u.1506625
ι : Type ?u.1506628
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
hfa' : Monotone fun n => -f n
hf0' : Tendsto (fun n => -f n) atTop (𝓝 0)
x✝ : ℕ
⊢ ∑ i in Finset.range (x✝ + 1), f i • z i = (-fun n => ∑ i in Finset.range (n + 1), -f i • z i) x✝
α : Type ?u.1506622
β : Type ?u.1506625
ι : Type ?u.1506628
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
hfa' : Monotone fun n => -f n
hf0' : Tendsto (fun n => -f n) atTop (𝓝 0)
⊢ CauchySeq fun n => ∑ i in Finset.range (n + 1), f i • z i
convert (hfa'.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0' hzb).neg
case h.e'_5.h
α : Type ?u.1506622
β : Type ?u.1506625
ι : Type ?u.1506628
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
hfa' : Monotone fun n => -f n
hf0' : Tendsto (fun n => -f n) atTop (𝓝 0)
x✝ : ℕ
⊢ ∑ i in Finset.range (x✝ + 1), f i • z i = (-fun n => ∑ i in Finset.range (n + 1), -f i • z i) x✝
case h.e'_5.h
α : Type ?u.1506622
β : Type ?u.1506625
ι : Type ?u.1506628
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
hfa' : Monotone fun n => -f n
hf0' : Tendsto (fun n => -f n) atTop (𝓝 0)
x✝ : ℕ
⊢ ∑ i in Finset.range (x✝ + 1), f i • z i = (-fun n => ∑ i in Finset.range (n + 1), -f i • z i) x✝
funext
no goals
case h.e'_5.h
α : Type ?u.1506622
β : Type ?u.1506625
ι : Type ?u.1506628
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
hfa' : Monotone fun n => -f n
hf0' : Tendsto (fun n => -f n) atTop (𝓝 0)
x✝ : ℕ
⊢ ∑ i in Finset.range (x✝ + 1), f i • z i = (-fun n => ∑ i in Finset.range (n + 1), -f i • z i) x✝
simp
case h.e'_5.h.e'_3
α : Type ?u.1506622
β : Type ?u.1506625
ι : Type ?u.1506628
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
hfa' : Monotone fun n => -f n
⊢ 0 = -0
α : Type ?u.1506622
β : Type ?u.1506625
ι : Type ?u.1506628
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
hfa' : Monotone fun n => -f n
⊢ Tendsto (fun n => -f n) atTop (𝓝 0)
convert hf0.neg
no goals
case h.e'_5.h.e'_3
α : Type ?u.1506622
β : Type ?u.1506625
ι : Type ?u.1506628
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
hfa' : Monotone fun n => -f n
⊢ 0 = -0
norm_num