Summable for functions on product

Stream: Is there code for X?

[Michael Stoll]

I'll need something along the lines of the following.

lemma Summable.prod_of_nonneg_of_summable_tsum {β γ : Type*} {f : β × γ → ℝ} (h₁ : ∀ x, 0 ≤ f x)
    (h₂ : ∀ b, Summable fun c ↦ f (b, c)) (h₃ : Summable fun b ↦ ∑' c, f (b, c)) :
    Summable f := by
  sorry

I found docs#HasSum.of_sigma, but this a) uses a Sigma type instead of a product type, and b) has a condition (h : CauchySeq fun (s : Finset ((b : β) × γ b)) => ∑ i ∈ s, f i), which is a bit unwieldy (and I had problems translating this to the corresponding statement for the product type: it seems that there is no lemma allowing to transfer docs#CauchySeq via an equivalence).

There surely must be a better approach?

[Sébastien Gouëzel]

Would docs#HasProd.prod_fiberwise help?

[Michael Stoll]

I don't think so; it requires f to be summable (for docs#HasSum.prod_fiberwise), which is what I want to prove.

[Sébastien Gouëzel]

No, sorry, I misread.

[Sébastien Gouëzel]

Well, you could lift everything to ENNReal using the positivity, use my lemma there to see that the sum of f coincides with the sum in h_3, so that it is finite, and then come back to the reals. Not completely direct, but not unnatural because nonnegativity is crucial for your lemma.

[Michael Stoll]

Which one is "your lemma there"?

[Michael Stoll]

@Sébastien Gouëzel :up:

[Eric Wieser]

Michael Stoll said:

it seems that there is no lemma allowing to transfer docs#CauchySeq via an equivalence).

This sounds like it would be a good result to PR, irrespective of whether it's the right thing to do here

[Eric Wieser]

Though maybe it's docs#CauchySeq.comp_injective ?

[Michael Stoll]

That is restricted to functions on Nat and has an annoying Nonempty assumption.

[Michael Stoll]

What I would need is something that works for functions defined on Finset <something>.

[Chris Birkbeck]

does summable_prod_of_nonneg help?

[Chris Birkbeck]

wait maybe that what you want?

[Chris Birkbeck]

Oh yeah thats it:

lemma Summable.prod_of_nonneg_of_summable_tsum {β γ : Type*} {f : β × γ → ℝ} (h₁ : ∀ x, 0 ≤ f x)
    (h₂ : ∀ b, Summable fun c ↦ f (b, c)) (h₃ : Summable fun b ↦ ∑' c, f (b, c)) :
    Summable f := by
    rw [summable_prod_of_nonneg]
    exact ⟨h₂, h₃⟩
    apply h₁

[Michael Stoll]

docs#summable_prod_of_nonneg

I wonder why loogle doesn't find it:
@loogle ⊢ Summable _, ?α × ?β, 0 ≤ _

[loogle]

:search: Summable.mul_of_nonneg

[Michael Stoll]

@Joachim Breitner :up:

[Sébastien Gouëzel]

@loogle Summable, ?_ × ?_, 0 ≤ ?_

[loogle]

:search: summable_prod_of_nonneg, Summable.mul_of_nonneg

[Sébastien Gouëzel]

@loogle Summable _, ?α × ?β, 0 ≤ _

[loogle]

:search: summable_prod_of_nonneg, Summable.mul_of_nonneg

[Sébastien Gouëzel]

I copied your exact command, and now it works. Weird.

[Sébastien Gouëzel]

Ah no, it's not your exact command, I omitted ⊢.

[Sébastien Gouëzel]

It's because the conclusion of the lemma is not that something is summable, it's an equivalence.

[Michael Stoll]

import Mathlib.Topology.Algebra.InfiniteSum.Real

lemma Summable.prod_of_nonneg_of_summable_tsum {β γ : Type*} {f : β × γ → ℝ} (h₁ : ∀ x, 0 ≤ f x)
    (h₂ : ∀ b, Summable fun c ↦ f (b, c)) (h₃ : Summable fun b ↦ ∑' c, f (b, c)) :
    Summable f :=
  (summable_prod_of_nonneg h₁).mpr ⟨h₂, h₃⟩

Short enough to be inlined...

[Michael Stoll]

@Joachim Breitner Could loogle be taught to match ⊢ blah also when the conclusion is an "iff" statement with blah on one side?

[Joachim Breitner]

Michael Stoll said:

Joachim Breitner Could loogle be taught to match ⊢ blah also when the conclusion is an "iff" statement with blah on one side?

Plausible, but I’m reluctant to add too much heuristics and special cases. Should it do the same for =?

You can find it this way as well (but you’d have to try both variants I guess).

@loogle ⊢ Summable _ ↔ _ , ?α × ?β, 0 ≤ _

Maybe once apply does this for you I am more likely convinced that loogle should do this :-)

Anyways, noted down as https://github.com/nomeata/loogle/issues/23.

[loogle]

:search: summable_prod_of_nonneg

[Michael Stoll]

Joachim Breitner said:

Maybe once apply does this for you I am more likely convinced that loogle should do this :-)

apply? does, I think.

[Joachim Breitner]

I sometimes wish apply would. But maybe it’s one of the wishes I’d regret if it turned true :-)

[Michael Stoll]

It would make apply a bit less efficient when it has to figure out which way it needs to use the lemma, I assume. But it would add a little bit of QoL.

[Jireh Loreaux]

@Michael Stoll Can you please add something about Tonelli's theorem to the docstring of summable_prod_of_nonneg? I immediately thought of this result by name when I started reading this thread.

[Michael Stoll]

Tonelli's Theorem says that the corresponding sum and double sum are equal. I think docs#ENNReal.tsum_prod and docs#ENNReal.tsum_prod' are closest to that statement (and docs#tsum_prod and docs#tsum_prod' are variants of Fubini's Theorem). I agree that it would be good to mention Tonelli in a (so far non-existing) docstring, but then the same applies to the other statements. As I'm not really an expert in measure theory, I'd rather leave that task to somebody else (you? @Jireh Loreaux :smile:).

[Johan Commelin]

Didn't @Floris van Doorn and @Heather Macbeth have a project on Tonelli a while back? They might want to chime in.