mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(measure_theory/measure/finite_measure_weak_convergence): Add portmanteau implications concerning open and closed sets.

Open kkytola opened this issue 3 years ago • 1 comments

Add equivalence of a limsup condition for closed sets and a liminf condition for open sets, which will later both be shown to be characterizing conditions of weak convergence of probability measures.

Also add that either of these equivalent conditions implies that for any Borel set whose boundary carries zero probability in the candidate limit measure, we have that the measures of this set tend to its measure under the candidate limit measure.

  • [x] depends on: #15218 [Lemmas about limsups and liminfs under decreasing functions are used.]

Open in Gitpod

kkytola avatar Jul 13 '22 20:07 kkytola

This PR/issue depends on:

  • ~~leanprover-community/mathlib#15218~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Jul 27 '22 06:07 mathlib-dependent-issues-bot

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

bors[bot] avatar Aug 21 '22 07:08 bors[bot]

bors r+

kkytola avatar Aug 27 '22 13:08 kkytola

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Aug 27 '22 16:08 bors[bot]