Re-package infinite sum via a partition

Stream: Is there code for X?

[Michael Stoll]

I am looking for something like (possibly with a more general target type than ℂ, of course)

import Mathlib

lemma HasSum.tsum_fibers {β γ : Type*} {f : β → ℂ} (g : β → γ) (a : ℂ) (hf : HasSum f a) :
    HasSum (fun c : γ ↦ tsum <| Set.restrict (g ⁻¹' {c}) f) a := sorry

but I'm unable to find anything close.

Any suggestions regarding where to look?

The finite version is there:

lemma Finset.sum.sum_fibers {β γ : Type*} [DecidableEq γ] (f : β → ℂ) (g : β → γ) (s : Finset β) :
    (s.image g).sum (fun c ↦ (s.filter (g · = c)).sum f) = s.sum f :=
  sum_fiberwise_of_maps_to (fun _ ↦ mem_image_of_mem g) f

Maybe one can use some filter magic to go from this to infinite sums, but I'm not an adept of the necessary yoga...

[Terence Tao]

docs#HasSum.sigma ?

[Michael Stoll]

Or docs#HasSum.prod_fiberwise (which comes right below it). I'll check it out. Thanks! @Terence Tao

[Yury G. Kudryashov]

(deleted)

[Junyan Xu]

Maybe you want to combine that with docs#Equiv.sigmaFiberEquiv and docs#Equiv.hasSum_iff

[Michael Stoll]

OK:

lemma HasSum.tsum_fibers {β γ : Type*} {f : β → ℂ} (g : β → γ) (a : ℂ) (hf : HasSum f a) :
    HasSum (fun c : γ ↦ tsum <| Set.restrict (g ⁻¹' {c}) f) a :=
  HasSum.sigma ((Equiv.hasSum_iff <| Equiv.sigmaFiberEquiv g).mpr hf) <|
    fun _ ↦ (Summable.hasSum_iff <| Summable.subtype hf.summable _).mpr rfl

Thanks everybody!