[Merged by Bors] - feat(MeasureTheory/Measure/Tight): portmanteau condition for compact sets

[jvanwinden]

One part of the portmanteau theorem states that a limsup condition for closed sets implies weak convergence of probability measures. In the situation where the measures are tight however, one only needs to check the limsup condition for compact sets.

This PR thus introduces tendsto_of_forall_isCompact_of_isTightMeasureSet, which is a version of tendsto_of_forall_isClosed_limsup_le but replaces IsClosed with IsCompact, under the additional hypothesis that the measures are tight.

I would have liked to put this lemma in MeasureTheory/Portmeanteau, but this created an import cycle. I am open to suggestions for where it could otherwise be moved.

---

[github-actions]

PR summary 118eff1b25

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.Measure.Tight	2375	1635	-740 (-31.16%)
Mathlib.MeasureTheory.Measure.TightNormed	2377	2247	-130 (-5.47%)
Mathlib.MeasureTheory.Measure.LevyConvergence	2693	2686	-7 (-0.26%)
Mathlib.MeasureTheory.Measure.Prokhorov	2395	2389	-6 (-0.25%)
Mathlib.MeasureTheory.Measure.Portmanteau	2369	2371	+2 (+0.08%)

Import changes for all files

Files	Import difference
Mathlib.MeasureTheory.Measure.Tight	-740
Mathlib.MeasureTheory.Measure.TightNormed	-130
Mathlib.MeasureTheory.Measure.LevyConvergence	-7
Mathlib.MeasureTheory.Measure.Prokhorov	-6
Mathlib.Probability.CentralLimitTheorem	-3
5 files Mathlib.MeasureTheory.Function.ConvergenceInDistribution Mathlib.MeasureTheory.Measure.FiniteMeasurePi Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.MeasureTheory.Measure.Portmanteau	2

---

Declarations diff

+ tendsto_of_forall_isCompact_of_isTightMeasureSet

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 118eff1b25
Reference commit 8d88d2ffc4

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

[jvanwinden]

By analogy with comments of @EtienneC30 in #39501 I also removed the T2Space assumption.

[jvanwinden]

-awaiting-author

[EtienneC30]

Looks like the portmanteau theorem is used to prove metrizability of the space of probability measures, which in turn is used to prove one direction of the Prokhorov theorem. I'd say you can move this (i.e. exists_measure_iUnion_gt_of_isCompact_closure and isTightMeasureSet_of_isCompact_closure) in a new file which would go in a new folder Tight. This folder would contain a Basic file and a ProkhorovTheorem file with the results I mentioned above. Then you should be able to not import Portmanteau in Basic, so that you can put your result in Portmanteau.

[jvanwinden]

Looks like the portmanteau theorem is used to prove metrizability of the space of probability measures, which in turn is used to prove one direction of the Prokhorov theorem. I'd say you can move this (i.e. exists_measure_iUnion_gt_of_isCompact_closure and isTightMeasureSet_of_isCompact_closure) in a new file which would go in a new folder Tight. This folder would contain a Basic file and a ProkhorovTheorem file with the results I mentioned above. Then you should be able to not import Portmanteau in Basic, so that you can put your result in Portmanteau.

I think it might be confusing to have two separate files related to the Prokhorov theorem. I think that both directions of Prokhorov should live in the Tight folder.

Maybe the following could work:

• create Tight/Basic which does not import Portmanteau
• put both directions of Prokhorov's theorem into Tight/Prokhorov
• put the new result in Portmanteau (which then imports Tight/Basic)

Do you think this would be good (if it can be made to work)?

[EtienneC30]

I think it might be confusing to have two separate files related to the Prokhorov theorem.

This is already the case as the other direction is in Mathlib.MeasureTheory.Measure.Prokhorov. So you can put exists_measure_iUnion_gt_of_isCompact_closure and isTightMeasureSet_of_isCompact_closure there.

[jvanwinden]

I have reorganized Prokhorov, Tight, and Portmanteau in the following way:

• the backward direction of Prokhorov (compact closure implies tight) has been moved from Tight to Prokhorov
• Prokhorov now has two sections: one for the forward direction and one for the backward direction
• the new result is moved to Portmanteau, directly below MeasureTheory.tendsto_of_forall_isClosed_limsup_le. This way it can reuse the variables.

I have also tried to minimize the imports (using #min_imports) and the open and open scoped statements in all three files.

I think all the lemmas should still have the same names and function signature, but I do not know how to easily verify this. Is there a tool which can show all the changed declarations in a PR?

[jvanwinden]

-awaiting-author

[EtienneC30]

I think all the lemmas should still have the same names and function signature, but I do not know how to easily verify this. Is there a tool which can show all the changed declarations in a PR?

Regarding the names, the message from the bot lists the declaration diff. I don't know a tool that checks changes in signatures though.

[jvanwinden]

I think all the lemmas should still have the same names and function signature, but I do not know how to easily verify this. Is there a tool which can show all the changed declarations in a PR?

Regarding the names, the message from the bot lists the declaration diff. I don't know a tool that checks changes in signatures though.

But the bot only runs when opening the PR, right? Is there a way to re-trigger it?

[EtienneC30]

The comment is edited after each commit.

[EtienneC30]

Hmm looks like I did not do a very good job with imports here.

public import Mathlib.MeasureTheory.Measure.Prod
public import Mathlib.MeasureTheory.Measure.Regular
public import Mathlib.Topology.Metrizable.CompletelyMetrizable

import Mathlib.MeasureTheory.Measure.RegularityCompacts

should work for Tight.

[jvanwinden]

After merging master I had to change the imports in Tight again (because my other PR about product measures has since been merged...)

[jvanwinden]

-awaiting-author

[jvanwinden]

-awaiting-author

[EtienneC30]

Thanks!
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by EtienneC30.

[RemyDegenne]

Thanks!
bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-Build Step
• ci (staging) / Lint style
• ci (staging) / Post-CI job
• ci (staging) / Build