rw [← summable_nat_add_iff N, summable_iff_bounded (fun n => hu _ <| Nat.le_add_left N n), e2]
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
e2 : (cumsum fun i => u (i + N)) = fun n => cumsum u (n + N) - cumsum u N
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
e2 : (cumsum fun i => u (i + N)) = fun n => cumsum u (n + N) - cumsum u N
⊢ (atTop.BoundedAtFilter fun n => cumsum u (n + N) - cumsum u N) ↔ atTop.BoundedAtFilter (cumsum u)