Finset.univ.sum split

Stream: Is there code for X?

[Martin Dvořák]

Do we have anything close enough to either of the following lemmas?

import Mathlib.Data.Finset.Pointwise

lemma Finset.univ_sum_split {α β : Type} [Fintype α] [AddCommMonoid β]
    (f : α → β) (p : α → Prop) [DecidablePred p] :
    let fₚ : { a : α // p a } → β := (fun a => f a.val)
    let fₙ : { a : α // ¬(p a) } → β := (fun a => f a.val)
    Finset.univ.sum f = Finset.univ.sum fₚ + Finset.univ.sum fₙ := by
  sorry

lemma Finset.univ_sum_split_of_zero {α β : Type} [Fintype α] [AddCommMonoid β]
    {f : α → β} {p : α → Prop} [DecidablePred p]
    (hpf : ∀ a : α, ¬(p a) → f a = 0) :
    let fₚ : { a : α // p a } → β := (fun a => f a.val)
    Finset.univ.sum f = Finset.univ.sum fₚ := by
  rw [Finset.univ_sum_split f p]
  convert add_zero _
  apply Finset.sum_eq_zero
  intro x _
  apply hpf
  exact x.property

[Ruben Van de Velde]

I think you may have simplified too much. docs#Finset.sum_filter_add_sum_filter_not seems like a more sensible spelling for this kind of thing

[Eric Wieser]

A general hint when working with sums is to try stating your result over Finset first, rather than working with Fintype

[Martin Dvořák]

Can somebody help me with my todo please?

import Mathlib.Data.Finset.Pointwise

variable {α β : Type*}

lemma todo [Fintype α] (f : α → β) (p : α → Prop) [DecidablePred p] :
    Finset.univ.val.map (fun a : { a // p a } => f a.val) =
    (Finset.univ.filter p).val.map f := by
  sorry

lemma Finset.univ_sum_split [Fintype α] [AddCommMonoid β]
    (f : α → β) (p : α → Prop) [DecidablePred p] :
    let fₚ : { a : α // p a } → β := (fun a => f a.val)
    let fₙ : { a : α // ¬(p a) } → β := (fun a => f a.val)
    Finset.univ.sum f = Finset.univ.sum fₚ + Finset.univ.sum fₙ := by
  rw [←Finset.sum_filter_add_sum_filter_not (p := p)]
  apply congr_arg₂ <;>
  · rw [Finset.sum_filter, Finset.sum_ite, Finset.sum_const_zero, add_zero]
    unfold Finset.sum
    rw [todo]

lemma Finset.univ_sum_split_of_zero [Fintype α] [AddCommMonoid β]
    {f : α → β} {p : α → Prop} [DecidablePred p]
    (hpf : ∀ a : α, ¬(p a) → f a = 0) :
    let fₚ : { a : α // p a } → β := (fun a => f a.val)
    Finset.univ.sum f = Finset.univ.sum fₚ := by
  rw [Finset.univ_sum_split f p]
  convert add_zero _
  apply Finset.sum_eq_zero
  intro x _
  apply hpf
  exact x.property

I don't know any better way to finish my proof.

[Andrew Yang]

import Mathlib.Data.Finset.Pointwise

variable {α β : Type*}

lemma Finset.univ_sum_split_of_zero [Fintype α] [AddCommMonoid β]
    {f : α → β} {p : α → Prop} [DecidablePred p]
    (hpf : ∀ a : α, ¬(p a) → f a = 0) :
    Finset.univ.sum f = Finset.univ.sum fun a : { a : α // p a } ↦ f a.val := by
  classical
  trans (Finset.univ.filter p).sum f
  · exact (Finset.sum_subset_zero_on_sdiff (Finset.subset_univ _)
      (by simpa) (fun _ _ ↦ rfl)).symm
  · exact Finset.sum_subtype _ (by simp) _

[Richard Copley]

import Mathlib.Data.Finset.Pointwise

variable {α β : Type*}

lemma todo [Fintype α] (f : α → β) (p : α → Prop) [DecidablePred p] :
    Finset.univ.val.map (fun a : { a // p a } => f a.val) =
    (Finset.univ.filter p).val.map f := by
  rw [← Finset.subtype_map, Finset.map_val, Finset.subtype_univ,
    Function.Embedding.coe_subtype, Multiset.map_map, Function.comp_def]

(Fixing the defeq abuse is left as an exercise :)) [Edit: fixed] [Edit: rewrite rhs only]

[Martin Dvořák]

Andrew Yang said:

import Mathlib.Data.Finset.Pointwise

variable {α β : Type*}

lemma Finset.univ_sum_split_of_zero [Fintype α] [AddCommMonoid β]
    {f : α → β} {p : α → Prop} [DecidablePred p]
    (hpf : ∀ a : α, ¬(p a) → f a = 0) :
    Finset.univ.sum f = Finset.univ.sum fun a : { a : α // p a } ↦ f a.val := by
  classical
  trans (Finset.univ.filter p).sum f
  · exact (Finset.sum_subset_zero_on_sdiff (Finset.subset_univ _)
      (by simpa) (fun _ _ ↦ rfl)).symm
  · exact Finset.sum_subtype _ (by simp) _

Thank you very much!!
Also, I didn't know trans was a tactic! Good to know!

Do you mind that I cite you even know I ungolfed your proof (which I apologize for) for consistency of my codebase?
https://github.com/madvorak/vcsp/blob/05c22491cad415de64db587122d7cfe872215d85/VCSP/Basic.lean#L89

[Martin Dvořák]

Richard Copley said:

import Mathlib.Data.Finset.Pointwise

variable {α β : Type*}

lemma todo [Fintype α] (f : α → β) (p : α → Prop) [DecidablePred p] :
    Finset.univ.val.map (fun a : { a // p a } => f a.val) =
    (Finset.univ.filter p).val.map f := by
  show Finset.univ.val.map (f ∘ Subtype.val) = _
  rw [← Multiset.map_map, ← Finset.subtype_map, Finset.subtype_univ,
    Finset.map_val, Function.Embedding.coe_subtype]

The identity between subtype of univ and filter of univ go to Mathlib IMO.
Can we isolate it from the mapping done afterwards?
What name should the lemma have?

[Andrew Yang]

trans is called transitivity in the lean3 days. There is also symm which is useful at times.

[Andrew Yang]

Do you mind that I cite you

Not at all. (It's okay not to cite me as well)

[Martin Dvořák]

Andrew Yang said:

trans is called transitivity in the lean3 days. There is also symm which is useful at times.

Yeah, I use symm pretty often.
I must say that trans is nicer than apply proof.trans which I have been using until now.

[Richard Copley]

Martin Dvořák said:

The identity between subtype of univ and filter of univ go to Mathlib IMO.
Can we isolate it from the mapping done afterwards?
What name should the lemma have?

This part?

lemma todo' [Fintype α] (p : α → Prop) [DecidablePred p] :
    Finset.univ.val.map ((↑) : { a // p a } → α) = (Finset.univ.filter p).val := by
  rw [← Finset.subtype_map, Finset.map_val, Finset.subtype_univ,
    Function.Embedding.coe_subtype]

[Martin Dvořák]

I'm not sure. The version with mapping was probably more useful?

[Martin Dvořák]

Andrew Yang said:

It's okay not to cite me as well

I like to keep track of which parts of my repo are other people's work.
Eventually, if a paper comes out of it, you will get an acknowledgement like the one we wrote in the middle of the first page here:
https://arxiv.org/pdf/2302.06420

[Richard Copley]

Martin Dvořák said:

I'm not sure. The version with mapping was probably more useful?

It does seem pretty trivial when the non-injective map is not involved.

[Martin Dvořák]

Trivial enough for Lean's automation to take care of it? It doesn't seem to me.

[Richard Copley]

I think this would usually suffice. One wouldn't need to think about multisets.

lemma todo'' [Fintype α] (p : α → Prop) [DecidablePred p] :
    Finset.univ.map (Function.Embedding.subtype p) = Finset.univ.filter p := by
  rw [← Finset.subtype_map, Finset.subtype_univ]

[Richard Copley]

(aesop can do that one) [Edit: or ext; simp]

[Martin Dvořák]

Richard Copley said:

I think this would usually suffice. One wouldn't need to think about multisets.

lemma todo'' [Fintype α] (p : α → Prop) [DecidablePred p] :
    Finset.univ.map (Function.Embedding.subtype p) = Finset.univ.filter p := by
  rw [← Finset.subtype_map, Finset.subtype_univ]

Getting from todo'' to todo still feels nontrivial. Therefore, I think that todo should go Mathlib even tho todo'' is not useful per se.

[Richard Copley]

How would you motivate it, if you were writing a PR? It's probably my intuition that is failing me, but I don't see the usefulness.

[Martin Dvořák]

I think Mathlib users should be able to easily translate between filtering and subtyping.
Just because a task can be broken down to trivial parts does not mean the task is trivial.

[Richard Copley]

Fair enough!

Here's one way to get from one to another, just for fun:

lemma todo'' [Fintype α] (p : α → Prop) [DecidablePred p] :
    Finset.univ.map (Function.Embedding.subtype p) = Finset.univ.filter p := by
  rw [← Finset.subtype_map, Finset.subtype_univ]

lemma todo' [Fintype α] (p : α → Prop) [DecidablePred p] :
    Finset.univ.val.map ((↑) : { a // p a } → α) = (Finset.univ.filter p).val := by
  apply (Finset.map_val (Function.Embedding.subtype p) Finset.univ).symm.trans
  apply congrArg
  exact todo'' ..

lemma todo [Fintype α] (f : α → β) (p : α → Prop) [DecidablePred p] :
    Finset.univ.val.map (fun a : { a // p a } => f a.val) =
    (Finset.univ.filter p).val.map f := by
  rw [← todo', Multiset.map_map, Function.comp_def]

[Martin Dvořák]

May I PR your code in a form I find suitable?

[Richard Copley]

Be my guest.

[Martin Dvořák]

#12903