have l2 n : ‖cumsum u n‖ = cumsum u n := by simpa using cumsum_nonneg hu n
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
l2 : ∀ (n : ℕ), ‖cumsum u n‖ = cumsum u n
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)