Zulip Chat Archive

Stream: maths

Topic: product of 0s and 1s


view this post on Zulip Reid Barton (Oct 24 2019 at 00:33):

Is there already a lemma like s.prod (\lam i, if p i then 0 else 1) = if (\forall i \in s, p i) then 0 else 1?

view this post on Zulip Mario Carneiro (Oct 24 2019 at 00:35):

I think that should be exists instead of forall?

view this post on Zulip Mario Carneiro (Oct 24 2019 at 00:35):

or 0 and 1 should be swapped

view this post on Zulip Reid Barton (Oct 24 2019 at 00:37):

Yes exists, sorry, or any other similar but correct statement

view this post on Zulip Mario Carneiro (Oct 24 2019 at 00:37):

I would prefer to see that factored into s.prod (\lam i, if p i then f i else 0) = (s.filter p).prod f and s.prod (\lam _, 1) = if s != \empty then 1 else 0

view this post on Zulip Mario Carneiro (Oct 24 2019 at 00:38):

I'm not a big fan of if statements in conclusions though; I would probably state the latter as two lemmas

view this post on Zulip Mario Carneiro (Oct 24 2019 at 00:39):

It might also make sense to add an additional step that connects s.prod (\lam _, a) to a ^ card s first

view this post on Zulip Reid Barton (Oct 24 2019 at 00:40):

In the intended application (https://en.wikipedia.org/wiki/Chevalley%E2%80%93Warning_theorem#Proof_of_Warning's_theorem) you do kind of want the if ... then 1 else 0 form though, since another lemma connects the sum of that to the cardinality of a set.

view this post on Zulip Mario Carneiro (Oct 24 2019 at 00:41):

at some point it becomes theorem-local reasoning though

view this post on Zulip Mario Carneiro (Oct 24 2019 at 00:41):

I would just use funext and split_ifs to get the if back

view this post on Zulip Reid Barton (Oct 24 2019 at 00:42):

You people don't like if and only if statements, do you

view this post on Zulip Kenny Lau (Oct 24 2019 at 00:42):

finset.prod_filter, finset.prod_const, zero_pow / pow_zero

view this post on Zulip Mario Carneiro (Oct 24 2019 at 00:42):

I'm a big fan of iff statements, what do you mean?

view this post on Zulip Mario Carneiro (Oct 24 2019 at 00:42):

these are all equalities

view this post on Zulip Mario Carneiro (Oct 24 2019 at 00:44):

I think I just rationally reconstructed mathlib

view this post on Zulip Reid Barton (Oct 24 2019 at 00:47):

Each term is the product of the indicator functions of fi(x)=0f_i(x) = 0, which is the indicator function of i,fi(x)=0\forall i, f_i(x) = 0, and summing that gives the number of solutions. I don't want to separately argue when all fi(x)f_i(x) are zero and when some fi(x)f_i(x) is not zero.

view this post on Zulip Reid Barton (Oct 24 2019 at 00:47):

Maybe I am just arguing that the function we talked about in #1472 should exist, and not fall under the general rule about ifs in conclusions.

view this post on Zulip Mario Carneiro (Oct 24 2019 at 00:48):

I think that's the right conclusion

view this post on Zulip Kenny Lau (Oct 24 2019 at 00:48):

import data.finsupp

universes u v

example (α : Type u) (β : Type v) [comm_ring β] (s : finset α) (p : α  Prop) [decidable_pred p] :
  s.prod (λ i, if p i then 0 else 1) = if  i  s, p i then 0 else 1 :=
by rw [ finset.prod_filter, finset.prod_const]
-- ⊢ 0 ^ finset.card (finset.filter (λ (a : α), p a) s) = ite (∃ (i : α) (H : i ∈ s), p i) 0 1

view this post on Zulip Kenny Lau (Oct 24 2019 at 00:49):

maybe 0 ^ finset.card (finset.filter (λ (a : α), p a) s)?


Last updated: May 11 2021 at 15:12 UTC