## Stream: maths

### Topic: sensitivity project lemmas

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

#### Johan Commelin (Oct 14 2019 at 14:31):

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

#### 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.

#### 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.

#### 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)

#### Johan Commelin (Oct 14 2019 at 14:45):

@[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 :=


#### 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.

#### 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 = _

#### 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


#### Rob Lewis (Oct 14 2019 at 15:24):

Does this exist already/where does it belong?

#### 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.

#### Patrick Massot (Oct 14 2019 at 16:11):

That one drove me crazy last summer.

#### Patrick Massot (Oct 14 2019 at 16:12):

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

#### Mario Carneiro (Oct 14 2019 at 18:15):

I think decidable_mem_of_fintype should go

#### 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.

#### 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

#### Mario Carneiro (Oct 14 2019 at 19:07):

it can of course stick around as a def

#### 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