match n with
| 0 => simp [cumsum]
| 1 => specialize hg 0 ; specialize hf' 1 ; simp [cumsum, hf0] at hf' hg ⊢ ; positivity
| n + 2 => convert cancel_aux' hf hg hf' hg' (n + 2) using 1 ; simp [cumsum_succ] ; ring
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
⊢ cumsum (f * g) n ≤ C * cumsum g n
no goals