Currying in tsum_prod definition

Stream: maths

[Devon Tuma]

The current statement of ennreal.tsum_prod differs from the more general tsum_prod' lemma in that it doesn't curry the arguments to the sum function. This means it doesn't work in situations like this:

open_locale ennreal
-- Current version
lemma ennreal.tsum_prod₁ {α β : Type*} {f : α → β → ℝ≥0∞} :
  ∑' p : α × β, f p.1 p.2 = ∑' a b, f a b :=
tsum_prod' ennreal.summable $ λ _, ennreal.summable

lemma ennreal.tsum_prod₂ {α β : Type*} {f : α × β → ℝ≥0∞} :
  ∑' p : α × β, f p = ∑' a b, f (a, b) :=
tsum_prod' ennreal.summable $ λ _, ennreal.summable

example {α β γ : Type} (f : α → β) (g : β × γ → ℝ≥0∞) :
  ∑' x, g (prod.map f id x) = ∑' y z, g (f y, z) :=
by simp_rw [ennreal.tsum_prod₂, prod_map, id.def]

Is there any reason not to change this to use the second definition?

[Floris van Doorn]

The second version is also good to have. For sigma we have both: docs#ennreal.tsum_sigma docs#ennreal.tsum_sigma'
The first version is sometimes useful if you're picky about the exact form of the right-hand side, so it's better to just have both versions.

[Devon Tuma]

Sure, that makes sense. I'll open a PR to add the other version alongside it then

[Eric Wieser]

The first one is best for backwards rewrites, the second is best for forwards rewrites

[Eric Wieser]

A bit like docs#prod.exists vs docs#prod.exists'