prod_ite_eq

Stream: Is there code for X?

[Scott Morrison]

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]

split_ifs then use prod_single etc

[Scott Morrison]

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

[Kenny Lau]

right

[Kenny Lau]

or rather the LHS

[Anne Baanen]

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]

That looks very promising!

[Anne Baanen]

I'll see if I can make a quick PR

[Kenny Lau]

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]

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]

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