question about functions with finite support

Stream: Carleson

[Clara Torres]

I'm having trouble with this lemma:
lemma volume_lt_of_not_GeneralCase (h : ¬ GeneralCase f α) : volume (univ : Set X) < ∞
I understand the proof is one line in the blueprint, but to apply the formalized results I would need that f is in L^1 (which I don't see where it comes from)
I would also need to provide the fact that f has finite measure support and is bounded, which are assumptions of the Lemma 10.2.5, but I don't know where to find them in th ecode.

[Michael Rothgang]

You can certainly assume BoundedFiniteSupport f to start --- if you can prove volume_lt_of_not_GeneralCase with that, it's fine. Indeed, that assumption is currently not made in the Lean file (but in Lemma 10.2.5).

[Michael Rothgang]

Mathematically, BoundedFiniteSupport f implies that f is in L¹. That is not formalised yet (so this should be added). In the end, it would be great to

• have a lemma that BoundedFiniteSupport implies being in L¹
• use that lemma in volume_lt_of_not_GeneralCase

Feel free to do as much of that now as you want: you can merely add a MemLp f 1 assumption to your lemma, with a TODO to remove it, just state a sorried statement that BoundedFiniteSupport f implies being in L¹ (and use that to prove f is in L¹) or even prove that.

[Michael Rothgang]

I wonder if the hypothesis ¬ GeneralCase f α implies that f has bounded finite support. (I haven't absorbed chapter 10 at all, so don't have an answer here.) If so, something similar should be done about that hypothesis in volume_lt_of_not_GeneralCase. Again, up to you how much of that you already want to do.

[Michael Rothgang]

Michael Rothgang said:

Mathematically, BoundedFiniteSupport f implies that f is in L¹. That is not formalised yet (so this should be added). In the end, it would be great to

• have a lemma that BoundedFiniteSupport implies being in L¹
• use that lemma in volume_lt_of_not_GeneralCase

Feel free to do as much of that now as you want: you can merely add a MemLp f 1 assumption to your lemma, with a TODO to remove it, just state a sorried statement that BoundedFiniteSupport f implies being in L¹ (and use that to prove f is in L¹) or even prove that.

To elaborate: mathlib should certainly get a result "if p <= q and f is L^q on a finite measure space, it is L^p". Loogle only finds docs#MeasureTheory.SimpleFunc.memLp_of_isFiniteMeasure, which is not that. This would also be a welcome lemma to add.

[Joris Roos]

Michael Rothgang said:

Mathematically, BoundedFiniteSupport f implies that f is in L¹. That is not formalised yet (so this should be added). (..)

This and similar things are absolutely formalized already, in a slight variant -- BoundedCompactSupport. Having both BoundedCompactSupport and BoundedFiniteSupport seems redundant and as we can see here can lead to unnecessary confusion. I would propose to use just one of them everywhere and refactor lemma statements appropriately.

[Sébastien Gouëzel]

docs#MeasureTheory.Memℒp.mono_exponent is the lemma you want.

[Sébastien Gouëzel]

I mean https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.html#MeasureTheory.Mem%E2%84%92p.mono_exponent

[Yury G. Kudryashov]

docs#MeasureTheory.MemLp.mono_exponent is the non-deprecated version

[Floris van Doorn]

Joris Roos said:

This and similar things are absolutely formalized already, in a slight variant -- BoundedCompactSupport. Having both BoundedCompactSupport and BoundedFiniteSupport seems redundant and as we can see here can lead to unnecessary confusion. I would propose to use just one of them everywhere and refactor lemma statements appropriately.

I was also wondering whether we really need both of these, since they are so similar. Mathematically, if we want to avoid BoundedFiniteSupport, I expect we have to strengthen Theorems 1.0.2 and 10.0.1 so that they say "compact support" instead of "finite support". This might not be a problem, but would be a significant change.

Secondly, on formalization grounds I'm not sure which is the better notion to have. For sensible measures, BoundedFiniteSupport is weaker than BoundedCompactSupport, and moreover it doesn't require that the domain is a topological space.

So I'm not sure that we should just use BoundedCompactSupport everywhere.

[Joris Roos]

@Floris van Doorn Exactly my thoughts, that's why I said pick one of them. For this project, they are interchangeable. In other settings, one might be more natural than the other. I can see an argument for both; there are lots of possible slight variants of this function class. Anyways, I don't think this is an important discussion and I don't care which one is used. My point is we should be consistent avoid effort duplication.

[Kevin Buzzard]

It's going to be hard finding all these conversations later, filed under this uninformative thread title :-/

[Notification Bot]

12 messages were moved here from #Carleson > new member by Floris van Doorn.

[Floris van Doorn]

I created fpvandoorn/carleson#306 to at least connect the two notions, and prove that BoundedFiniteSupport-functions are in L^p.

[Floris van Doorn]

I don't want to remove one of the notions now. I think it's fine to experiment with both notions (and perhaps copy-paste some lemmas between the two). We can decide later which of the two notions we want to upstream to Mathlib.

[Floris van Doorn]

(the required Mathlib lemma was docs#MeasureTheory.MemLp.mono_exponent_of_measure_support_ne_top btw )