sum_range_by_parts — Mathlib

English

For the finite range, the Abel summation identity states

Русский

Для конечного диапазона формула Абеля для суммирования принимает вид:

LaTeX

$$$$ \\sum_{i=0}^{n-1} f(i) \\cdot g(i) = f(n-1) \\cdot G(n) - \\sum_{i=0}^{n-2} (f(i+1) - f(i)) \\cdot G(i+1). $$$$

Lean4

/-- **Summation by parts** for ranges -/
theorem sum_range_by_parts :
    ∑ i ∈ range n, f i • g i = f (n - 1) • G n - ∑ i ∈ range (n - 1), (f (i + 1) - f i) • G (i + 1) :=
  by
  by_cases hn : n = 0
  · simp [hn]
  · rw [range_eq_Ico, sum_Ico_by_parts f g (Nat.pos_of_ne_zero hn), sum_range_zero, smul_zero, sub_zero, range_eq_Ico]

Похожие утверждения