simpa [shift] using Finset.sum_nonneg' ha
n✝ : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb✝ : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
n : ℕ
hb : b (n + 1) ≤ b n
⊢ 0 ≤ shift (cumsum a) n
no goals