sensitivity project lemmas

Stream: maths

[Rob Lewis]

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]

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

[Johan Commelin]

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

[Chris Hughes]

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

[Mario Carneiro]

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]

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]

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

[Johan Commelin]

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

[Rob Lewis]

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]

Does this exist already/where does it belong?

[Rob Lewis]

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]

That one drove me crazy last summer.

[Patrick Massot]

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

[Mario Carneiro]

I think decidable_mem_of_fintype should go

[Rob Lewis]

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]

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

[Mario Carneiro]

it can of course stick around as a def

[Johan Commelin]

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