sum of products

Stream: Is there code for X?

[Floris van Doorn]

What is the lemma in mathlib that is closest to the following pseudo-Lean goal involving finset.prod?

i : ι
f g h : ι → α
h1 : f i = g i + h i
h2 : ∀ j ≠ i, f i = g i = h i
⊢ ∏ i, f i = (∏ i, g i) + (∏ i, h i)

[Floris van Doorn]

I think this didn't exist yet, so I'll PR this soon:

lemma prod_split {α β} [decidable_eq α] [comm_monoid β] (s t : finset α) (f : α → β) :
  (∏ x in s, f x) = (∏ x in s ∩ t, f x) * (∏ x in s \ t, f x) :=
by { convert s.prod_piecewise t f f, simp [finset.piecewise] }

lemma prod_split_single {α β} [decidable_eq α] [comm_monoid β] {s : finset α} {i : α} (h : i ∈ s)
  (f : α → β) : (∏ x in s, f x) = f i * (∏ x in s \ {i}, f x) :=
by { convert s.prod_split {i} f, simp [h] }

lemma prod_add_single {α β} [comm_semiring β] {s : finset α} {i : α} {f g h : α → β}
  (hi : i ∈ s) (h1 : f i = g i + h i) (h2 : ∀ j ∈ s, j ≠ i → f j = g j)
  (h3 : ∀ j ∈ s, j ≠ i → f j = h j) : ∏ i in s, f i = ∏ i in s, g i + ∏ i in s, h i :=
by { simp [prod_split_single hi, h1, right_distrib], congr' 2; apply prod_congr rfl; simpa }

lemma prod_univ_add_single {α β} [fintype α] [comm_semiring β] (i : α) {f g h : α → β}
  (h1 : f i = g i + h i) (h2 : ∀ j ≠ i, f j = g j) (h3 : ∀ j ≠ i, f j = h j) :
  ∏ i, f i = ∏ i, g i + ∏ i, h i :=
prod_add_single (mem_univ i) h1 (λ j _, h2 j) (λ j _, h3 j)

[Kenny Lau]

import data.fintype.basic algebra.big_operators

open_locale classical big_operators

lemma prod_add_single {α β} [comm_semiring β] (s : finset α) (i : α) {f g h : α → β}
  (h1 : f i = g i + h i) (h2 : ∀ j ≠ i, f j = g j) (h3 : ∀ j ≠ i, f j = h j) (h4 : i ∈ s) :
  ∏ i in s, f i = ∏ i in s, g i + ∏ i in s, h i :=
by { rw ← finset.insert_erase h4, simp_rw finset.prod_insert (finset.not_mem_erase i s),
     rw [h1, add_mul], congr' 2; apply finset.prod_congr rfl; intros j hj,
     exacts [h2 j (finset.ne_of_mem_erase hj), h3 j (finset.ne_of_mem_erase hj)] }

lemma prod_univ_add_single {α β} [fintype α] [comm_semiring β] (i : α) {f g h : α → β}
  (h1 : f i = g i + h i) (h2 : ∀ j ≠ i, f j = g j) (h3 : ∀ j ≠ i, f j = h j) :
  ∏ i, f i = ∏ i, g i + ∏ i, h i :=
prod_add_single _ i h1 h2 h3 (finset.mem_univ i)

[Yury G. Kudryashov]

There is a file about multilinear functions.

[Yury G. Kudryashov]

Not sure if it has this lemma.