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 A b : ℕ → E
ha : a = nabla A
n : ℕ
⊢ cumsum (a * b) (n + 1) = A (n + 1) * b n - A 0 * b 0 - cumsum (shift A * fun i => b (i + 1) - b i) n
Tactic:
have l1 : ∑ x in Finset.range (n + 1), A (x + 1) * b x = ∑ x in Finset.range n, A (x + 1) * b x + A (n + 1) * b n :=
  Finset.sum_shift_back
State after:
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 A b : ℕ → E
ha : a = nabla A
n : ℕ
l1 : ∑ x ∈ Finset.range (n + 1), A (x + 1) * b x = ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n
⊢ cumsum (a * b) (n + 1) = A (n + 1) * b n - A 0 * b 0 - cumsum (shift A * fun i => b (i + 1) - b i) n

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 A b : ℕ → E
ha : a = nabla A
n : ℕ
l1 : ∑ x ∈ Finset.range (n + 1), A (x + 1) * b x = ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n
⊢ cumsum (a * b) (n + 1) = A (n + 1) * b n - A 0 * b 0 - cumsum (shift A * fun i => b (i + 1) - b i) n
Tactic:
have l2 : ∑ x in Finset.range (n + 1), A x * b x = A 0 * b 0 + ∑ x in Finset.range n, A (x + 1) * b (x + 1) :=
  Finset.sum_shift_front
State after:
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 A b : ℕ → E
ha : a = nabla A
n : ℕ
l1 : ∑ x ∈ Finset.range (n + 1), A (x + 1) * b x = ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n
l2 : ∑ x ∈ Finset.range (n + 1), A x * b x = A 0 * b 0 + ∑ x ∈ Finset.range n, A (x + 1) * b (x + 1)
⊢ cumsum (a * b) (n + 1) = A (n + 1) * b n - A 0 * b 0 - cumsum (shift A * fun i => b (i + 1) - b i) n

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 A b : ℕ → E
ha : a = nabla A
n : ℕ
l1 : ∑ x ∈ Finset.range (n + 1), A (x + 1) * b x = ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n
l2 : ∑ x ∈ Finset.range (n + 1), A x * b x = A 0 * b 0 + ∑ x ∈ Finset.range n, A (x + 1) * b (x + 1)
⊢ cumsum (a * b) (n + 1) = A (n + 1) * b n - A 0 * b 0 - cumsum (shift A * fun i => b (i + 1) - b i) n
Tactic:
simp [cumsum, shift, ha, nabla, sub_mul, mul_sub, l1, l2]
State after:
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 A b : ℕ → E
ha : a = nabla A
n : ℕ
l1 : ∑ x ∈ Finset.range (n + 1), A (x + 1) * b x = ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n
l2 : ∑ x ∈ Finset.range (n + 1), A x * b x = A 0 * b 0 + ∑ x ∈ Finset.range n, A (x + 1) * b (x + 1)
⊢ ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n - (A 0 * b 0 + ∑ x ∈ Finset.range n, A (x + 1) * b (x + 1)) =
    A (n + 1) * b n - A 0 * b 0 - (∑ x ∈ Finset.range n, A (x + 1) * b (x + 1) - ∑ x ∈ Finset.range n, A (x + 1) * b x)

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 A b : ℕ → E
ha : a = nabla A
n : ℕ
l1 : ∑ x ∈ Finset.range (n + 1), A (x + 1) * b x = ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n
l2 : ∑ x ∈ Finset.range (n + 1), A x * b x = A 0 * b 0 + ∑ x ∈ Finset.range n, A (x + 1) * b (x + 1)
⊢ ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n - (A 0 * b 0 + ∑ x ∈ Finset.range n, A (x + 1) * b (x + 1)) =
    A (n + 1) * b n - A 0 * b 0 - (∑ x ∈ Finset.range n, A (x + 1) * b (x + 1) - ∑ x ∈ Finset.range n, A (x + 1) * b x)
Tactic:
abel
State after:
no goals