Stream: maths

Topic: product of 0s and 1s

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?

Mario Carneiro (Oct 24 2019 at 00:35):

I think that should be exists instead of forall?

Mario Carneiro (Oct 24 2019 at 00:35):

or 0 and 1 should be swapped

Reid Barton (Oct 24 2019 at 00:37):

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

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

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

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

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.

Mario Carneiro (Oct 24 2019 at 00:41):

at some point it becomes theorem-local reasoning though

Mario Carneiro (Oct 24 2019 at 00:41):

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

Reid Barton (Oct 24 2019 at 00:42):

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

Kenny Lau (Oct 24 2019 at 00:42):

finset.prod_filter, finset.prod_const, zero_pow / pow_zero

Mario Carneiro (Oct 24 2019 at 00:42):

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

Mario Carneiro (Oct 24 2019 at 00:42):

these are all equalities

Mario Carneiro (Oct 24 2019 at 00:44):

I think I just rationally reconstructed mathlib

Reid Barton (Oct 24 2019 at 00:47):

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

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.

Mario Carneiro (Oct 24 2019 at 00:48):

I think that's the right conclusion

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


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