## Stream: Is there code for X?

### Topic: prod_ite_eq

#### Scott Morrison (Jun 18 2020 at 14:21):

I need a variant of src#prod_ite_eq, that says:

lemma prod_dite_eq [decidable_eq α] (s : finset α) (a : α) (b : Π x : α, a = x → β) :
(∏ x in s, (if h : a = x then b x h else 1)) = ite (a ∈ s) (b a rfl) 1 :=


but it seems tricky to prove from the available API. Any ideas?

#### Kenny Lau (Jun 18 2020 at 14:22):

split_ifs then use prod_single etc

#### Scott Morrison (Jun 18 2020 at 14:34):

So as an intermediate step in the a ∈ s branch, the RHS will become ∏ x in {a}, b x _?

right

#### Kenny Lau (Jun 18 2020 at 14:35):

or rather the LHS

#### Anne Baanen (Jun 18 2020 at 14:36):

Perhaps this modification of prod_ite will help? (Works for me in algebra/big_operators.lean)

@[to_additive] lemma prod_dite {s : finset α} {p : α → Prop} {hp : decidable_pred p}
(f : Π (x : α), p x → γ) (g : Π (x : α), ¬p x → γ) (h : α → γ → β) :
s.prod (λ x, h x (if b : p x then f x b else g x b)) =
(s.filter p).attach.prod (λ x, h x (f x.1 (mem_filter.mp x.2).2)) *
(s.filter (λ x, ¬ p x)).attach.prod (λ x, h x (g x.1 (mem_filter.mp x.2).2)) :=
by {letI := classical.dec_eq α,
calc s.prod (λ x, h x (if b : p x then f x b else g x b))
= (s.filter p ∪ s.filter (λ x, ¬ p x)).prod (λ x, h x (if b : p x then f x b else g x b)) :
by rw [filter_union_filter_neg_eq]
... = (s.filter p).prod (λ x, h x (if b : p x then f x b else g x b)) *
(s.filter (λ x, ¬ p x)).prod (λ x, h x (if b : p x then f x b else g x b)) :
prod_union (by simp [disjoint_right] {contextual := tt})
... = (s.filter p).attach.prod (λ x, h x.1 (f x.1 (mem_filter.mp x.2).2)) *
(s.filter (λ x, ¬ p x)).attach.prod (λ x, h x.1 (g x.1 (mem_filter.mp x.2).2)) :
begin
apply congr_arg2;
apply @prod_bij _ _ _ _ (s.filter _) (s.filter _).attach _ _
(λ a ha, subtype.mk a ha)
(λ a ha, mem_attach _ ⟨a, ha⟩),
{ intros a ha, congr, rw dif_pos },
{ intros a b ha hb, apply subtype.mk.inj },
{ intros a ha, use a.1, use a.2, finish },
{ intros a ha, congr, rw dif_neg },
{ intros a b ha hb, apply subtype.mk.inj },
{ intros a ha, use a.1, use a.2, finish }
end}


#### Scott Morrison (Jun 18 2020 at 14:37):

That looks very promising!

#### Anne Baanen (Jun 18 2020 at 14:38):

I'll see if I can make a quick PR

#### Kenny Lau (Jun 18 2020 at 14:42):

import algebra.big_operators

open_locale classical big_operators

variables {α β : Type*} [comm_monoid β]

lemma prod_dite_eq (s : finset α) (a : α) (b : Π x : α, a = x → β) :
(∏ x in s, (if h : a = x then b x h else 1)) = ite (a ∈ s) (b a rfl) 1 :=
begin
split_ifs with h,
{ rw [finset.prod_eq_single a, dif_pos rfl],
{ intros, rw dif_neg, cc },
{ cc } },
{ rw finset.prod_eq_one,
intros, rw dif_neg, intro, cc }
end


#### Scott Morrison (Jun 18 2020 at 14:46):

Looks good. Right now I'm going to copy-and-paste Kenny's proof into my branch which will eventually turn into PRs, but @Anne Baanen yours seems like a good thing to have in big_operators.lean too.

#### Anne Baanen (Jun 18 2020 at 15:14):

prod_apply_dite and prod_dite are #3110 and I will let you PR prod_dite_eq :)

Last updated: May 17 2021 at 15:13 UTC