sum_ite_eq_extract

Stream: Is there code for X?

[Chris Birkbeck]

Do we have the following in mathlib?

lemma sum_ite_eq_extract {α : Type*} {β : Type*} [add_comm_monoid β] [decidable_eq α]
 (s : finset α) (b : s) (f : α → β) :
  ∑ n in s, f n = f b + ∑ n in s, ite (n = b) 0 (f n) :=
begin
sorry,
end

We have a tsum_ite_eq_extract, but I can't seem to find a sum version.

[Yaël Dillies]

We have docs#finset.sum_boole and docs#finset.sum_ite, which are pretty close.

[Chris Birkbeck]

hmm yeah I saw those, but I can't seem to get this easily from them.

[Yaël Dillies]

You can rewrite the LHS using finset.sum_ite, finset.sum_ite_eq', add_comm.

[Yaël Dillies]

And of course you should turn (b : s) into {b : α} (hb : b ∈ s).

[Chris Birkbeck]

hmm I don't see how to rewrite the LHS using finset.sum_ite.

[Patrick Johnson]

You can also use docs#finset.filter_ne'

import algebra.big_operators.basic
open_locale big_operators

lemma sum_ite_eq_extract {α β : Type*} [add_comm_monoid β] [decidable_eq α]
  {s : finset α} {b : s} {f : α → β} :
  ∑ n in s, f n = f b + ∑ n in s, ite (n = b) 0 (f n) :=
begin
  cases b with b hb,
  simp [finset.sum_ite, finset.filter_ne'],
  rw add_comm,
  exact (finset.sum_erase_add _ _ hb).symm,
end

[Chris Birkbeck]

Patrick Johnson said:

You can also use docs#finset.filter_ne'

import algebra.big_operators.basic
open_locale big_operators

lemma sum_ite_eq_extract {α β : Type*} [add_comm_monoid β] [decidable_eq α]
  {s : finset α} {b : s} {f : α → β} :
  ∑ n in s, f n = f b + ∑ n in s, ite (n = b) 0 (f n) :=
begin
  cases b with b hb,
  simp [finset.sum_ite, finset.filter_ne'],
  rw add_comm,
  exact (finset.sum_erase_add _ _ hb).symm,
end

ah ok I hadn't seen filter_ne'. Thats nice.

[Eric Wieser]

it might be nice to have the function.update version too, which is how docs#tsum_ite_eq_extract is proved

[Chris Birkbeck]

You mean something like:

lemma sum_update_eq {α : Type*} {β : Type*} [add_comm_monoid β] [decidable_eq α] [has_sub β]
 (s : finset α) {a : α} (b : β) (hb : a ∈ s)  (f : α → β) :
  ∑ n in s, (update f a b) n = b + ∑ n in s, (f n) - (f a) :=

?

[Eric Wieser]

You'll need add_comm_group

[Eric Wieser]

Or the variant∑ n in s, update f a b n + f a = ∑ n in s, f n + b

[Chris Birkbeck]

Ok I made #13545 with these two things

[Yaël Dillies]

We already have docs#finset.sum_update_of_mem and docs#finset.sum_update_of_not_mem

[Chris Birkbeck]

oh damn I didnt see them. Well that cuts things in half :P

[Eric Wieser]

@Chris Birkbeck, is the lemma you actually want docs#finset.add_sum_erase?

[Chris Birkbeck]

Eric Wieser said:

Chris Birkbeck, is the lemma you actually want docs#finset.add_sum_erase?

Oh! that does actually work for what I want. Ok so I now don't have a use for this sum_ite_extract, but maybe its still worth having?

[Eric Wieser]

Personally I dislike tsum_ite_eq_extract, the name doesn't follow our naming conventions at all

[Johan Commelin]

My hunch is that finset.add_sum_erase is more practical to use, in most situations.

[Eric Wieser]

Maybe we should just add a comment to docs#tsum_ite_eq_extract indicating why the API is different to the finset case

[Eric Wieser]

(eg because "unlike finsets, this is indexed by a type not a set, so we can't use an API similar tofinset.add_sum_erase")