iSup over finite sum

Stream: Is there code for X?

[Markus de Medeiros]

Is there an elegant way to commute iSup's with finite sums? I think there might be some way to specialize one of the lintegral lemmas to get this, but I'm wondering if there's a better way.

f : T → U → ENNReal
s : Finset T
⊢ ∑ a ∈ s, ⨆ y, f a y = ⨆ i, ∑ a ∈ s, f a i

[Jireh Loreaux]

That's not true. Consider S=T={0,1}, and f 0 0 = 0, f 0 1 = 1, f 1 0 = 2, f 1 1 = 0. Then the LHS is 3, but the RHS is 2.

[Markus de Medeiros]

Thanks-- suppose it makes sense why I couldn't find it then : )

[Markus de Medeiros]

For posterity, I did some more digging, and the is true for monotone functions (which is what I had). The lemma is ENNReal.finsetSum_iSup_of_monotone

[Jireh Loreaux]

@Markus de Medeiros I got distracted by the fact that it wasn't true. But the correct way to find a lemma like this that does exist is: @loogle |- ∑ a ∈ ?s, ⨆ y, ?f a y = ⨆ i, ∑ a ∈ ?s, ?f a i

[loogle]

:search: ENNReal.finsetSum_iSup_of_monotone, ENNReal.finset_sum_iSup_nat, and 1 more

[Jireh Loreaux]

(first hit)

[Markus de Medeiros]

Excellent-- thanks for the help!