# Zulip Chat Archive

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

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

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