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
n : ℕ
⊢ cumsum (a * b) (n + 1) = cumsum a (n + 1) * b n - cumsum (shift (cumsum a) * nabla b) n
Tactic:
simpa using summation_by_parts (a := a) (b := b) (A := cumsum a) (by simp [Finset.sum_shift_back])
State after:
no goals

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
n : ℕ
⊢ a = nabla (cumsum a)
Tactic:
simp [Finset.sum_shift_back]
State after:
no goals