tsum_const

Stream: Is there code for X?

[Gareth Ma]

Is there code for

import Mathlib
open scoped ENNReal
example {α : Type*} {s : Set α} [Countable s] (c : ℝ≥0∞) :
    (∑' x : s, c) = s.encard.toENNReal • c := by
  sorry

?

[Yaël Dillies]

docs#tsum_const ?

[Gareth Ma]

no because ENNReal is not a group (the c)

[Gareth Ma]

And also in that setting the sum will be treated as 0 (since the Nat.card is 0). But maybe I can split cases on whether s is finite or not... let me try

[Yaël Dillies]

docs#ENNReal.tsum_const_eq ?

[Yaël Dillies]

A bit weird that it invokes measure theory, but I'm sure you could extract your statement from the current proof

[Gareth Ma]

Looks like it, might need to figure out some details but yea, thanks :D

[Yaël Dillies]

Thank https://leanprover-community.github.io/mathlib4_docs, not me :smile:

[Gareth Ma]

Lol yeah I didn't look closely enough

[Edward van de Meent]

there is a version of this in the #Carleson project, i believe

[Edward van de Meent]

yup, check this file

[Edward van de Meent]

minus the countable assumption, that is

[Gareth Ma]

Amaazing, thanks! ENNReal.tsum_const_eq' is what I need

[Edward van de Meent]

written by yours truly :heart:

[Floris van Doorn]

Please PR this to Mathlib! (either Edward or Gareth if Edward is fine with it)

[Edward van de Meent]

sure, i'll do it

[Gareth Ma]

Oops, I missed the message. PR'ing would be great, thanks a lot in advance.

[Edward van de Meent]

i can't seem to find a good file for this... Data.Set.card (which contains Set.encard) is hardly ever used, meaning that the home for these lemmas would be Mathlib :face_with_peeking_eye: ... #min_imports suggests three imports...

import Mathlib.Data.Real.ENatENNReal
import Mathlib.Data.Set.Card
import Mathlib.Topology.Instances.ENNReal

[Damiano Testa]

#min_imports is a lower bound, #find_home! are upper bounds: try with that and import Mathlib.

[Edward van de Meent]

that's what i was doing already...

[Gareth Ma]

Data.Set.card (which contains Set.encard) is hardly ever used

:(

[Edward van de Meent]

when i try #find_home! while importing Mathlib it suggests Mathlib

[Damiano Testa]

Ok, I misunderstood your previous comment, sorry.

[Damiano Testa]

In fact, Mathlib.Data.Real.ENatENNReal is also not imported anywhere, other than Mathlib.

[Edward van de Meent]

ah, so it is...

[Damiano Testa]

So it looks like either a new file, or adding an import. I think that the latter would require a little bit of explaining why adding an import is preferred to a new file.

[Edward van de Meent]

i suppose the real question would be if this lemma is even wanted in mathlib then, seeing as its requirements are scarcely or not used

[Gareth Ma]

Yes I think it should be. If this basic lemma are not added, no one will work on using these "scarcely used requirements"

[Edward van de Meent]

i mean that it is thinkable that these requirements are scarcely used because they are part of a pattern that is concidered bad

[Damiano Testa]

New files with new lemmas are constantly added: the review process is a good place to see if the new lemmas are wanted. Besides, Floris already supported the lemma -- that is a big vote of confidence!

[Edward van de Meent]

very well. then remains the question of where to put this new file...

[Edward van de Meent]

somewhere in the Mathlib.Topology.Algebra.InfiniteSum folder i think?

[Edward van de Meent]

although i'm not sure that this is algebra...

[Edward van de Meent]

i'll make the file Mathlib.Topology.Algebra.InfiniteSum.ENNReal

[Edward van de Meent]

ok, it's at #15214

[Yury G. Kudryashov]

Yaël Dillies said:

A bit weird that it invokes measure theory, but I'm sure you could extract your statement from the current proof

At the time it was added, we didn't have ENats (more precisely, PartENats were called enat and we didn't have much theory about this type).

[Yury G. Kudryashov]

Currently, facts about tsum and ENNReals are in Topology/Instances/ENNReal. It would be nice to move them to a new file (and drop this dependency in Topology/Instances/ENNReal).

[Yury G. Kudryashov]

But this should be a separate "move only" PR, not the same PR that adds new lemma(s).

[Edward van de Meent]

with regards to the current docs#ENNReal.tsum_const_eq , i think that maybe it is better replaced with a lemma saying that for [MeasurableSingletonClass α], casting Set.encard is the same as Measure.count or something along those lines...

[Edward van de Meent]

assuming that #15214 gets merged, that is

[Edward van de Meent]

PR is sent off to bors, for those interested :tada: