have l1 : ∀ᶠ n in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n := by
  filter_upwards [hbb] with n hb
  exact mul_nonneg (by simpa [shift] using Finset.sum_nonneg' ha) (sub_nonneg.mpr hb)
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)
⊢ Summable (a * b)
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)
l1 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
⊢ Summable (a * b)