prod_add_ordered — Mathlib

English

Let s be a finite set with a linear order. Then the product over i∈s of (f(i) + g(i)) equals the product over i∈s f(i) plus a sum over i∈s of g(i) times the product over j<i of (f(j) + g(j)) times the product over j>i of f(j).

Русский

Пусть s упорядчено; произведение по i∈s (f(i)+g(i)) равно произведению по i∈s f(i) плюс сумма по i∈s от g(i) раз произведение по j<i (f(j)+g(j)) и произведение по j>i f(j).

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_add_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
  refine Finset.induction_on_max s (by simp) ?_
  clear s
  intro a s ha ihs
  have ha' : a ∉ s := fun ha' => lt_irrefl a (ha a ha')
  rw [prod_insert ha', prod_insert ha', sum_insert ha', filter_insert, if_neg (lt_irrefl a), filter_true_of_mem ha, ihs,
    add_mul, mul_add, mul_add, add_assoc]
  congr 1
  rw [add_comm]
  congr 1
  · rw [filter_false_of_mem, prod_empty, mul_one]
    exact (forall_mem_insert _ _ _).2 ⟨lt_irrefl a, fun i hi => (ha i hi).not_gt⟩
  · rw [mul_sum]
    refine sum_congr rfl fun i hi => ?_
    rw [filter_insert, if_neg (ha i hi).not_gt, filter_insert, if_pos (ha i hi), prod_insert, mul_left_comm]
    exact mt (fun ha => (mem_filter.1 ha).1) ha'

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