Zulip Chat Archive

Stream: Is there code for X?

Topic: sum of products


view this post on Zulip Floris van Doorn (Aug 06 2020 at 20:50):

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)

view this post on Zulip Floris van Doorn (Aug 06 2020 at 21:12):

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)

view this post on Zulip Kenny Lau (Aug 07 2020 at 00:01):

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)

view this post on Zulip Yury G. Kudryashov (Aug 08 2020 at 01:58):

There is a file about multilinear functions.

view this post on Zulip Yury G. Kudryashov (Aug 08 2020 at 01:58):

Not sure if it has this lemma.


Last updated: May 16 2021 at 05:21 UTC