feat(MeasureTheory): a relatively compact set of measures is tight

[FormulaRabbit81]

---

[github-actions[bot]]

PR summary 0a79887f2a

Import changes exceeding 2%

%	File
+68.95%	Mathlib.MeasureTheory.Measure.Tight

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.Measure.Tight	1285	2171	+886 (+68.95%)

Import changes for all files

Files	Import difference
Mathlib.MeasureTheory.Measure.TightNormed	152
Mathlib.MeasureTheory.Measure.Tight	886

---

Declarations diff

+ exists_measure_iUnion_gt_of_isCompact_closure + isTightMeasureSet_of_isCompact_closure

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[FormulaRabbit81]

Thanks! This is a first round of comments on the auxiliary lemma. There are several remarks about the code which can be applied to your other proofs, so please try and apply them also there to make the review process more efficient.

Thank you for your detailed and instructive review - it is hugely appreciated. I've implemented the suggestions you made (I also found a large golf for the first lemma) to the best of my ability to all of the code.

[FormulaRabbit81]

-awaiting-author

[FormulaRabbit81]

Thanks for the PR! It's getting close to a mergeable state.

Sorry for the huge suggestions in the comments, but they are due to one change with effects everywhere: replacing the explicit sequence 1/(m+1) by an antitone sequence u that tends to 0. The reason is explained in one of the comments.

Thank you very much for the review and code improvements! In fact I tried this myself at one point, but couldn't get it to work cleanly :)

[FormulaRabbit81]

-awaiting-author

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[FormulaRabbit81]

Thanks again for the review! I've committed your suggestions and had a few small notes / questions:

• isTightMeasureSet_singleton broke when I merged so I had to add an import for it. I assume this is due to a recent PR
• The docstring I've added isn't very descriptive. Should I add more or is this sufficent? Other than it being part of Prokhorov's theorem I am not sure what could be added
• I’ve named the first theorem exists_union_of_OpenCover_of_mass_precompact_Set_ProbabilityMeasure, which is hopefully more appropriate, but very long.
• I put @[gcongr] on ProbabilityMeasure.apply_mono. Does this need to be a separate PR?
• I got a warning on line 204 that I need to squeeze the simp, but it doesn’t work without this weird amount of spacing.

[FormulaRabbit81]

-awaiting-author

[mathlib-bors[bot]]

:v: FormulaRabbit81 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[RemyDegenne]

Thanks! bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Post-Build Step
• Build
• Lint style