finset.extend_by_zero variant

Stream: Is there code for X?

[Kyle Miller]

Is something like this already somewhere? I didn't see anything in algebra.big_operators.basic.

lemma finset.sum_extend_by_zero' {α β : Type*} [fintype α] [add_comm_monoid β]
  (s : finset α) [decidable_pred (∈ s)] (f : α → β) :
  ∑ i in s, f i = ∑ (i : α), if i ∈ s then f i else 0 :=
begin
  classical,
  convert finset.sum_add_sum_compl s _,
  have : filter (λ (i : α), i ∈ s) sᶜ = ∅,
  { ext, simp, },
  simp [finset.sum_ite, this],
end

[Yaël Dillies]

Yes there is something close

[Yaël Dillies]

!docs#finset.sum_extend_by_zero

[Yaël Dillies]

Argh! Not on Discord.

[Yaël Dillies]

Is this what you were looking for?

[Kyle Miller]

That lemma's why this got a ' -- I want to change the bounds of the sum to finset.univ

[Kyle Miller]

I guess it could also be a finset.sum_subset_extend, where you can extend the bound while introducing an ite.

[Yaël Dillies]

Ah yeah I assume not then.

[Eric Wieser]

Does it exist if you phrase it in terms of docs#set.indicator?

[Kyle Miller]

I'd forgotten about that function, but I don't see anything.

Maybe another question is whether there's something pre-existing for the following finset.sum_subset_extend:

lemma finset.sum_subset_extend {α β : Type*} [add_comm_monoid β]
  {s t : finset α} [decidable_pred (∈ s)]
  (h : s ⊆ t) (f : α → β) :
  ∑ i in s, f i = ∑ i in t, if i ∈ s then f i else 0 :=
begin
  rw [←finset.sum_subset h, ←finset.sum_attach],
  swap, exact λ x ht hs, by simp [hs],
  nth_rewrite 1 ←finset.sum_attach,
  congr,
  ext,
  simp,
end

lemma finset.extend_by_zero' {α β : Type*} [fintype α] [add_comm_monoid β]
  (s : finset α) [decidable_pred (∈ s)] (f : α → β) :
  ∑ i in s, f i = ∑ (i : α), if i ∈ s then f i else 0 :=
by rw sum_subset_extend (subset_univ s)

[Eric Wieser]

docs#set.sum_indicator_subset?

[Kyle Miller]

Thanks, sum_extend_by_zero' is equivalent to the following dance:

rw set.sum_indicator_subset _ (subset_univ _),
simp_rw [set.indicator_apply, mem_coe],

[Eric Wieser]

Is refl not enough to close the goal after the rw?

[Kyle Miller]

It's mid-proof. I wanted finset.sum_extend_by_zero' specifically to get a sum into a particular form.

[Kyle Miller]

https://github.com/leanprover-community/mathlib/blob/7d8fc747f273c0be4f7a3f384c43cb69320daeec/src/combinatorics/simple_graph/adj_matrix.lean#L183

[Eric Wieser]

import algebra.indicator_function

open_locale big_operators

lemma finset.sum_extend_by_zero' {α β : Type*} [fintype α] [add_comm_monoid β]
  (s : finset α) [decidable_pred (∈ s)] (f : α → β) :
  ∑ i in s, f i = ∑ (i : α), if i ∈ s then f i else 0 :=
begin
  convert set.sum_indicator_subset _ (finset.subset_univ _),
  ext i,
  congr,
end

was what I was thinking of

[Eric Wieser]

I guessset.indicator is unpleasant here because it has the wrong decidable instance

[Eric Wieser]

So I guess we should rewrite every proof in the file about set.indicator to be about ite, and then reprove the indicator / classical.decidable version as a special case?

[Kyle Miller]

Another pain point is that set.indicator is for sets, but these are finsets. @Eric Wieser Have you thought about making finset a set_like? Then indicator could be generalized for any set_like, and the set.indicator_apply lemma could put things in terms of the correct has_mem.

[Oliver Nash]

Eric Wieser said:

I guessset.indicator is unpleasant here because it has the wrong decidable instance

I was just using set.indicator and discovered that it contains classical decidability instances in its definition. This should be fixed, right?

[Eric Wieser]

classical decidability instances in definitions are a deliberate design choice

[Eric Wieser]

They just should never appear directly in lemmas

[Eric Wieser]

If a decidability instance in a definition is tripping you up, then either:

• Your use case requires definitional equality and you're probably in for a bad time anyway
• You're unfolding when you should be using API

[Oliver Nash]

OK thanks, let me see if I can resolve my situation with this useful guide.

[Oliver Nash]

FWIW I just used the same pattern as your example above: convert, ext, congr instead of exact: https://github.com/leanprover-community/mathlib/pull/9629/files#diff-ece920d3095b577efda5ca995226b64d018390dfbefdb264722220712d38682bR727