prod_sub_ordered — Mathlib

English

Let s be finite with a linear order. Then the product over i∈s of (f(i) − g(i)) equals the product over i∈s f(i) minus a weighted sum over i∈s of g(i) times products over earlier and later indices, analogous to the unordered case.

Русский

Пусть s конечно и упорядочено; произведение (f(i)−g(i)) по i∈s равно произведению f(i) по i∈s минус взвешенная сумма по i∈s от g(i) умножить на произведения по предшествующим и последующим индексам.

LaTeX

$$$\\prod_{i\\in s} (f(i) - g(i)) = \\left(\\prod_{i\\in s} f(i)\\right) - \\sum_{i\\in s} g(i) \\left( \\prod_{j\\in s, j

Lean4

/-- `∏ i, (f i - g i) = (∏ i, f i) - ∑ i, g i * (∏ j < i, f j - g j) * (∏ j > i, f j)`. -/
theorem prod_sub_ordered [LinearOrder ι] (s : Finset ι) (f g : ι → R) :
    ∏ i ∈ s, (f i - g i) =
      (∏ i ∈ s, f i) - ∑ i ∈ s, g i * (∏ j ∈ s with j < i, (f j - g j)) * ∏ j ∈ s with i < j, f j :=
  by
  simp only [sub_eq_add_neg]
  convert prod_add_ordered s f fun i => -g i
  simp

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