sum_Ioc_by_parts — Mathlib

English

Let m < n and f,g be sequences with G the partial sum of g. Then

Русский

Пусть m < n и последовательности f, g с G(n) = ∑_{k<n} g(k). Тогда для Ioc выполняется формула Абеля:

LaTeX

$$$$ \\sum_{i \in \\mathrm{Ioc}(m,n)} f(i) \\cdot g(i) = f(n) \\cdot G(n+1) - f(m+1) \\cdot G(m+1) - \\sum_{i \\in \\mathrm{Ioc}(m, n-1)} (f(i+1) - f(i)) \\cdot G(i+1). $$$$

Lean4

theorem sum_Ioc_by_parts (hmn : m < n) :
    ∑ i ∈ Ioc m n, f i • g i =
      f n • G (n + 1) - f (m + 1) • G (m + 1) - ∑ i ∈ Ioc m (n - 1), (f (i + 1) - f i) • G (i + 1) :=
  by
  simpa only [← Ico_add_one_add_one_eq_Ioc, Nat.sub_add_cancel (Nat.one_le_of_lt hmn), add_tsub_cancel_right] using
    sum_Ico_by_parts f g (Nat.succ_lt_succ hmn)

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