[Merged by Bors] - feat(measure_theory/measure/measure_space): In sigma finite measure spaces, disjoint unions can have at most countably many positive measure parts. #15492

kkytola · 2022-07-18T12:17:59Z

Main addition of this PR: In sigma finite measure spaces, disjoint unions can have at most countably many positive measure parts.

Also in this PR: A disjoint union whose measure is finite has at most finitely many parts of measure greater than any positive constant.

…paces, disjoint unions can have at most countably many positive measure parts.

fpvandoorn

I think some things can be improved about this PR. I gave some suggestions to refactor the proofs.
I'm think the results in data/real/ennreal are very specific, so are probably not worth having in that generality. Some of them are unused, and I think you can avoid using the others by using an arbitrary sequence using something like exists_seq_strict_anti_tendsto instead of 1/n specifically.

fpvandoorn · 2022-07-19T15:42:53Z

src/data/real/ennreal.lean

@@ -1371,6 +1371,42 @@ begin
  exact n.lt_two_pow
 end

+lemma Union_Ioi_add_inv_nat (z : ℝ≥0∞) : (⋃ (n : ℕ), Ioi (z + n⁻¹)) = Ioi z :=


It would be nice to have a lemma (⋃ (i : ι), Ioi (f i)) = Ioi (⨅ i, f i) (on an arbitrary type with appropriate order conditions), and that should simplify this proof.

I added the lemma you suggested, Union_Ioi_eq_Ioi_infi. But it is not clear it leads to a simplification here. I rewrote the proof (and also tested directly for the proof of the next lemma, if the current one is too specialized), and it is almost the same length and I think uses less familiar components.

I of course agree that Union_Ioi_eq_Ioi_infi is in principle good to have, and I'll try to find the right place for it. But I would consider reverting the proofs here to the original ones, or similar, perhaps keeping only the ones that are actually used in this PR.

There is ennreal.add_infi, and it would be nice if you could add lemmas computing ⨅ i, (f i)⁻¹ (I think that is (⨆ i, f i)⁻¹ assuming f i ≠ 0).

But as I said, I'm not sure if this special case is worth having, especially since you're not using it.

I removed these --- indeed exists_seq_strict_anti_tendsto' and the general lemmas you suggested are sufficiently convenient to use within the main proof that the auxiliary pieces here are not necessary.

fpvandoorn · 2022-07-19T15:52:55Z

src/data/real/ennreal.lean

+by simp_rw [(show {x : ℝ≥0∞ | x ≠ 0} = Ioi 0, by { ext x, exact pos_iff_ne_zero.symm, }),
+            ← ennreal.Union_Ioi_add_inv_nat 0, zero_add]
+
+lemma Union_Ici_add_inv_nat {z : ℝ≥0∞} (z_ne_top : z ≠ ∞) : (⋃ (n : ℕ), Ici (z + n⁻¹)) = Ioi z :=


Can you prove (⋃ (i : ι), Ici (f i)) = Ioi (⨅ i, f i) under the assumption that there is no least f i? Not sure how to best write that, maybe disjoint (range f) (lower_bounds (range f)).

I don't think these parts will simplify a lot, but I made #17587 for what I think are the appropriate versions of the requested lemma. Instead of the disjoint (range f) (lower_bounds (range f)) spelling I propose is_glb and conditions about whether the glb is a member of the set (here the range) or not.

I'm requesting your review of that very small PR, I hope that's ok. I will return to the design choices in this PR afterwards.

src/measure_theory/measure/measure_space.lean

fpvandoorn · 2022-07-19T16:07:39Z

src/measure_theory/measure/measure_space.lean

+
+/-- If the union of disjoint measurable sets has finite measure, then there are only
+finitely many members of the union whose measure exceeds any given positive number. -/
+lemma finite_const_le_meas_of_disjoint_Union {ι : Type*} [measurable_space α] {μ : measure α}


The main part of this proof should be a result about tsum on ennreal: if you have a tsum on ennreal that is finite, then there are finitely many terms above ε. I feel like we should have that already somewhere.

I found summable.tendsto_cofinite_zero. To me it would look useful to have also the more explicit statement about the finiteness of the set of indices for which the summands exceed a given positive level.

I will try to rewrite using this.

In fact, the summands here are ennreal-valued (measures), and so summable hypothesis is automatic from ennreal.summable, but useless because the additive group hypothesis is not true. Therefore summable.tendsto_cofinite_zero does not apply here. Maybe one needs ennreal-specific versions, with summable hypothesis replaced by ∑' i, a i < ∞.

I found also nnreal.tendsto_cofinite_zero_of_summable, but it is also not exactly what I want.

I agree that summable.tendsto_cofinite_zero doesn't apply, but probably you can easily get an ennreal version from nnreal.tendsto_cofinite_zero_of_summable (from the assumption that the tsum is finite, all elements are finite and you can use ennreal.to_nnreal to use the nnreal result).

The main part of this proof should be a result about tsum on ennreal: if you have a tsum on ennreal that is finite, then there are finitely many terms above ε. I feel like we should have that already somewhere.

As discussed, I don't believe we had this as such. I made #17588 for that. The approach there is to translate measure theory results from counting measure to tsum and finset.card, which may be a bit import-heavy, but I think it is way more convenient than to use cardinalities API directly (I expect the convenience gap will only increase in the long run for more substantial manipulation of tsums).

I'd be grateful if you could review that PR!

fpvandoorn · 2022-07-19T16:08:12Z

src/measure_theory/measure/measure_space.lean

+
+/-- In a σ-finite space, among disjoint measurable sets, only countably many can have positive
+measure. -/
+lemma countable_meas_pos_of_disjoint_Union


The main part of this proof should be a lemma about tsum on ennreal: if you have a tsum on ennreal that is finite, then there are countably many positive terms. I feel like we should have that already somewhere.

I did not actually find this fact about tsum, but it is a similar argument as in the PR, at least if one first reformulates summable.tendsto_cofinite_zero as the finiteness of the set of indices where the summands exceed a given positive level.

Actually... How did you plan to reduce countable_meas_pos_of_disjoint_Union to a fact about tsum anyway?

If the indexing type of the disjoint union is not countable to start with, the measure of the disjoint union is not the tsum of measures of the sets in the union. And if the indexing type is countable, there is nothing to prove.

Oh, that is a good point. I didn't think that through very well. Is it true that the measure of a (not necessarily countable) disjoint union is always at least the sum of the measures?

Yes, I added tsum_meas_le_meas_Union_of_disjoint and use it to shorten the main proof.

…gested by Floris.

…infi. Not an obvious improvement for this purpose.

RemyDegenne · 2022-10-07T07:21:29Z

Is this PR still awaiting-author?

kkytola · 2022-10-07T12:07:41Z

Is this PR still awaiting-author?

Yes! Sorry!

The remaining two implications of portmanteau theorem and also a useful variant of the layercake representation (needed also for one of the remaining portmanteau implications) definitely need this, so I have not abandoned this. It is just that I have time for Lean only very sporadically, and for the past two months I have unfortunately not had time for Lean. I keep hoping that I will have time for Lean "next weekend", and things related to the "awaiting author" issue here are first on my agenda.

Specifically, Floris raised some (perhaps minor) implementation questions, and I will have to think them through. I will want the implementation to be good for mathlib, and I want to simultaneously make sure that this applies to portmanteau and layercake as intended.

Or do you need this immediately for something else?

RemyDegenne · 2022-10-07T12:12:35Z

No problem, there is no rush and I don't need this right now. I simply saw that there were a couple of commits since the awaiting-author tag was applied and thought that maybe you forgot to switch it back to awaiting-review.

…lete linear orders.

…che).

src/measure_theory/measure/measure_space.lean

sgouezel · 2022-12-04T09:54:03Z

bors r+
Thanks!

…paces, disjoint unions can have at most countably many positive measure parts. (#15492) Main addition of this PR: In sigma finite measure spaces, disjoint unions can have at most countably many positive measure parts. Also in this PR: A disjoint union whose measure is finite has at most finitely many parts of measure greater than any positive constant. Co-authored-by: kkytola <“kalle.kytola@aalto.fi”>

bors · 2022-12-04T12:16:52Z

Pull request successfully merged into master.

Build succeeded:

kkytola added 2 commits July 18, 2022 15:06

feat(measure_theory/measure/measure_space): In sigma finite measure s…

bfdf5dd

…paces, disjoint unions can have at most countably many positive measure parts.

Moved ennreal lemmas to data.real.ennreal.

f11b658

kkytola added the WIP Work in progress label Jul 18, 2022

kkytola added 2 commits July 18, 2022 16:32

Add three docstrings.

b8aabc5

Fix gt to lt and add docstrings.

4040640

kkytola added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Jul 18, 2022

fpvandoorn reviewed Jul 19, 2022

View reviewed changes

fpvandoorn added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 19, 2022

kkytola added 2 commits July 20, 2022 01:16

Golfed the proof of forall_measure_inter_spanning_sets_eq_zero as sug…

572e68f

…gested by Floris.

A version of the Union_Ioi lemma via a more general Union_Ioi_eq_Ioi_…

aa26097

…infi. Not an obvious improvement for this purpose.

RemyDegenne added the t-measure-probability Measure theory / Probability theory label Sep 14, 2022

kkytola added 4 commits November 18, 2022 10:54

Merge branch 'master' into kkytola/sigma_finite_countable_pos_meas

f2bd031

Still add versions of union of closed semi-infinite intervals in comp…

85eafe2

…lete linear orders.

Try to add two small lemmas in hopefully a suitable place (and get ca…

2355372

…che).

Clean up.

b3a1b96

kkytola requested a review from a team as a code owner November 18, 2022 09:07

kkytola and others added 7 commits November 18, 2022 13:29

Fix some broken proofs.

f9c0f53

Add still versions that are hopefully more practical.

7b1af12

Fix a long line by using dot notation.

8281b4b

Merge branch 'master' into kkytola/sigma_finite_countable_pos_meas

d1639d8

Get cache. Start refactoring.

1ee9104

Cleaning up and removing unnecessary lemmas.

8160790

Remove an accidentally left duplicate lemma.

7203c46

kkytola added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Dec 1, 2022

sgouezel reviewed Dec 2, 2022

View reviewed changes

src/measure_theory/measure/measure_space.lean Outdated Show resolved Hide resolved

src/measure_theory/measure/measure_space.lean Outdated Show resolved Hide resolved

sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Dec 2, 2022

kkytola added 2 commits December 2, 2022 23:19

Implement suggestions from PR review.

37b3916

Remove an unnecessary lemma application.

d89242d

kkytola added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Dec 3, 2022

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Dec 4, 2022

bors bot closed this Dec 4, 2022

bors bot deleted the kkytola/sigma_finite_countable_pos_meas branch December 4, 2022 12:16

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(measure_theory/measure/measure_space): In sigma finite measure spaces, disjoint unions can have at most countably many positive measure parts. #15492

[Merged by Bors] - feat(measure_theory/measure/measure_space): In sigma finite measure spaces, disjoint unions can have at most countably many positive measure parts. #15492

kkytola commented Jul 18, 2022

fpvandoorn left a comment

fpvandoorn Jul 19, 2022

kkytola Jul 19, 2022 •

edited

fpvandoorn Jul 20, 2022

kkytola Dec 1, 2022

fpvandoorn Jul 19, 2022

kkytola Nov 17, 2022 •

edited

fpvandoorn Jul 19, 2022

kkytola Jul 19, 2022

kkytola Jul 19, 2022 •

edited

fpvandoorn Jul 20, 2022

kkytola Nov 18, 2022 •

edited

fpvandoorn Jul 19, 2022 •

edited

kkytola Jul 19, 2022

kkytola Jul 19, 2022 •

edited

fpvandoorn Jul 20, 2022

kkytola Dec 1, 2022

RemyDegenne commented Oct 7, 2022

kkytola commented Oct 7, 2022

RemyDegenne commented Oct 7, 2022

sgouezel commented Dec 4, 2022

bors bot commented Dec 4, 2022

[Merged by Bors] - feat(measure_theory/measure/measure_space): In sigma finite measure spaces, disjoint unions can have at most countably many positive measure parts. #15492

[Merged by Bors] - feat(measure_theory/measure/measure_space): In sigma finite measure spaces, disjoint unions can have at most countably many positive measure parts. #15492

Conversation

kkytola commented Jul 18, 2022

fpvandoorn left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kkytola Jul 19, 2022 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kkytola Nov 17, 2022 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kkytola Jul 19, 2022 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kkytola Nov 18, 2022 • edited

Choose a reason for hiding this comment

fpvandoorn Jul 19, 2022 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kkytola Jul 19, 2022 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RemyDegenne commented Oct 7, 2022

kkytola commented Oct 7, 2022

RemyDegenne commented Oct 7, 2022

sgouezel commented Dec 4, 2022

bors bot commented Dec 4, 2022

kkytola Jul 19, 2022 •

edited

kkytola Nov 17, 2022 •

edited

kkytola Jul 19, 2022 •

edited

kkytola Nov 18, 2022 •

edited

fpvandoorn Jul 19, 2022 •

edited

kkytola Jul 19, 2022 •

edited