Zulip Chat Archive

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 _?

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

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: Dec 20 2023 at 11:08 UTC