Theorem: summation_by_parts'' (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
a b : ℕ → E
⊢ shift (cumsum (a * b)) = shift (cumsum a) * b - cumsum (shift (cumsum a) * nabla b)
Tactic:
ext n
State after:
case h
n✝ : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
a b : ℕ → E
n : ℕ
⊢ shift (cumsum (a * b)) n = (shift (cumsum a) * b - cumsum (shift (cumsum a) * nabla b)) n

State before:
case h
n✝ : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
a b : ℕ → E
n : ℕ
⊢ shift (cumsum (a * b)) n = (shift (cumsum a) * b - cumsum (shift (cumsum a) * nabla b)) n
Tactic:
apply summation_by_parts'
State after:
no goals