Finite sum over two disjoint sets

Stream: Is there code for X?

[Michael Rothgang]

I want to use the following lemma - which is so basic that mathlib "surely has it, right"? I cannot find it --- what's the right term to search for? Where can I read about the different kinds of sums and their behaviour, for instance?

import Mathlib
open Classical in
lemma foo {X : Type*} [Fintype X] {g : X → ℂ} {s t : Set (X)} (hst : Disjoint s t) :
    ∑ p ∈ {p | p ∈ s ∪ t}, g p = ∑ p ∈ {p | p ∈ s}, g p + ∑ p ∈ {p | p ∈ t}, g p := by
  sorry

[Kenny Lau]

@Michael Rothgang is there a reason why you're using Set instead of Finset?

[Michael Rothgang]

This is minimized from the Carleson project, so... I don't know. Probably, this can be changed.

[Michael Rothgang]

Next non-expert question: what's the difference between these two/where should I read up about that?

[Kenny Lau]

we only have sum over Finset, which makes sense even when the universe (i.e. the Type) is infinite; when you used Set here, the compiler implicitly converts it to Finset in the first place

[Kenny Lau]

import Mathlib
open Classical in
lemma foo {X : Type*} {g : X → ℂ} {s t : Finset X} (hst : Disjoint s t) :
    ∑ p ∈ s ∪ t, g p = ∑ p ∈ s, g p + ∑ p ∈ t, g p :=
  Finset.sum_union hst

@Michael Rothgang

[Kenny Lau]

this is the "correct" version

[Kenny Lau]

like, mathematically, sum only makes sense over a finite set

[Kenny Lau]

(infinite sums, which exist in maths, is an abuse of notation: it's really the limit of finite sums)

[Sabbir Rahman]

There is tsum for sum over sets, finite and infinite. but that is only absolute convergence I think

[Sabbir Rahman]

the lemma in question can be converted to finsets. Though like Kenny said, starting with Finset makes more sense.

import Mathlib

open Classical in
lemma foo {X : Type*} [Fintype X] {g : X → ℂ} {s t : Set (X)} (hst : Disjoint s t) :
    ∑ p ∈ {p | p ∈ s ∪ t}, g p = ∑ p ∈ {p | p ∈ s}, g p + ∑ p ∈ {p | p ∈ t}, g p := by
  convert_to ∑ p ∈ (s.toFinset ∪ t.toFinset), g p = ∑ p ∈ s.toFinset, g p + ∑ p ∈ t.toFinset, g p
  any_goals (
    congr <;> (ext x; simp)
  )
  apply  Finset.sum_union
  simpa