Zulip Chat Archive

Stream: maths

Topic: sensitivity project lemmas


view this post on Zulip Rob Lewis (Oct 14 2019 at 14:29):

I'm trying to move the sensitivity formalization to mathlib and need to locate one or two lemmas.

lemma finset.sum_ite' {α : Type*} [decidable_eq α] {β : Type*} [semiring β] (s : finset α)
  (P : set α) [decidable_pred P] [fintype P] (f : α  β) :
  s.sum (λ a, (f a) * (if P a then 1 else 0)) = (s  P.to_finset).sum f :=

feels like it belongs in algebra.big_operators but also needs a data.fintype import. Also, I'm not at all sure that this is the ideal way to state this. Opinions?

view this post on Zulip Johan Commelin (Oct 14 2019 at 14:31):

Why do you need the fintype? Can't we filter s by P?

view this post on Zulip Johan Commelin (Oct 14 2019 at 14:35):

This statement doesn't really seem to know whether it wants to treat P as a set or as a predicate.

view this post on Zulip Chris Hughes (Oct 14 2019 at 14:36):

I think this is so easy to prove with sum_subset that it might not be worth stating.

view this post on Zulip Mario Carneiro (Oct 14 2019 at 14:36):

I would prefer if P a then f a else 0 in the statement of this theorem, with another lemma expressing a * boole p = (if p then a else 0)

view this post on Zulip Johan Commelin (Oct 14 2019 at 14:45):

FYI: there is already https://github.com/leanprover-community/mathlib/blob/494132e1ebdba300a43d66e19ddc5b724fd20129/src/algebra/big_operators.lean#L453

@[simp] lemma sum_mul_boole [decidable_eq α] (s : finset α) (f : α  β) (a : α) :
  s.sum (λ x, (f x * ite (a = x) 1 0)) = ite (a  s) (f a) 0 :=

view this post on Zulip Rob Lewis (Oct 14 2019 at 14:46):

It isn't a direct application of sum_subset, is it? f changes. sum_mul_boole might be helpful.

view this post on Zulip Johan Commelin (Oct 14 2019 at 14:47):

Well, it's a bit restrictive. I would want sum_mul_boole to use a more general predicate than a = _

view this post on Zulip Rob Lewis (Oct 14 2019 at 15:24):

Aha. Here's the missing lemma. With this, finset.sum_ite' is unnecessary.

@[simp] lemma mul_ite {α} [semiring α] (P : Prop) [decidable P] (a : α) :
  a * (if P then 1 else 0) = if P then a else 0 :=
by split_ifs; simp

view this post on Zulip Rob Lewis (Oct 14 2019 at 15:24):

Does this exist already/where does it belong?

view this post on Zulip Rob Lewis (Oct 14 2019 at 15:43):

An issue with another lemma from the sensitivity project.

This has come up a few times (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/fintype.2Ecard, https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60decidable_mem_of_fintype.60.20problem): there's a type class loop. With A : Type, fintype A, s : set A, a search for fintype ↥s loops. subtype.fintype directs it to find decidable_pred s, and then decidable_mem_of_fintype directs it to find fintype ↥s.

view this post on Zulip Patrick Massot (Oct 14 2019 at 16:11):

That one drove me crazy last summer.

view this post on Zulip Patrick Massot (Oct 14 2019 at 16:12):

About mul_ite: library_search doesn't find it before timing out.

view this post on Zulip Mario Carneiro (Oct 14 2019 at 18:15):

I think decidable_mem_of_fintype should go

view this post on Zulip Rob Lewis (Oct 14 2019 at 19:03):

I think decidable_mem_of_fintype should go

It does seem like the less essential of the two, but it doesn't look inherently bad.

view this post on Zulip Mario Carneiro (Oct 14 2019 at 19:07):

My reasoning is that it is a rather expensive way to decide a predicate, so it should be opt in

view this post on Zulip Mario Carneiro (Oct 14 2019 at 19:07):

it can of course stick around as a def

view this post on Zulip Johan Commelin (Oct 15 2019 at 12:11):

@Rob Lewis Thanks a lot for your efforts in "archiving" this project.


Last updated: May 14 2021 at 18:28 UTC