[Merged by Bors] - feat: add last implication of portmanteau characterizations of weak convergence #8097
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…onst and 7 friends.
…ons (except with subtraction counterparts have to assume AddCommGroup and one additional covariance property).
…StronglyMeasurable?).
…ions to one file. Generalize to usual typeclasses.
…r AntitoneOn functions?
kkytola
added
awaiting-review
|
✌️ kkytola can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
bors r+ |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Nov 11, 2023
…onvergence (#8097) This PR adds the last missing implication of the general case of portmanteau equivalent characterizations of convergence in distribution: a sufficient condition for convergence in distribution of a sequence of probability measures is that for all open sets the candidate limit measure is at most the liminf of the measures. Co-authored-by: Kalle <kalle.kytola@aalto.fi> Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
|
Build failed: |
bors r+ |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Nov 12, 2023
…onvergence (#8097) This PR adds the last missing implication of the general case of portmanteau equivalent characterizations of convergence in distribution: a sufficient condition for convergence in distribution of a sequence of probability measures is that for all open sets the candidate limit measure is at most the liminf of the measures. Co-authored-by: Kalle <kalle.kytola@aalto.fi> Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
mathlib-bors
bot
deleted the
kkytola/portmanteau_open_implies_convergence_overview
branch
alexkeizer
pushed a commit
that referenced
this pull request
Nov 17, 2023
…onvergence (#8097) This PR adds the last missing implication of the general case of portmanteau equivalent characterizations of convergence in distribution: a sufficient condition for convergence in distribution of a sequence of probability measures is that for all open sets the candidate limit measure is at most the liminf of the measures. Co-authored-by: Kalle <kalle.kytola@aalto.fi> Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
alexkeizer
pushed a commit
that referenced
this pull request
Nov 21, 2023
…onvergence (#8097) This PR adds the last missing implication of the general case of portmanteau equivalent characterizations of convergence in distribution: a sufficient condition for convergence in distribution of a sequence of probability measures is that for all open sets the candidate limit measure is at most the liminf of the measures. Co-authored-by: Kalle <kalle.kytola@aalto.fi> Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
mathlib-bors bot
pushed a commit
that referenced
this pull request
Nov 25, 2023
In my earlier PR #8097 there there was a typo `variable {Ω : Type}` which should have been a universe polymorphic `variable {Ω : Type*}`. This PR fixes 1 character. Apologies!
grunweg
pushed a commit
that referenced
this pull request
Dec 15, 2023
…onvergence (#8097) This PR adds the last missing implication of the general case of portmanteau equivalent characterizations of convergence in distribution: a sufficient condition for convergence in distribution of a sequence of probability measures is that for all open sets the candidate limit measure is at most the liminf of the measures. Co-authored-by: Kalle <kalle.kytola@aalto.fi> Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
awueth
pushed a commit
that referenced
this pull request
Dec 19, 2023
In my earlier PR #8097 there there was a typo `variable {Ω : Type}` which should have been a universe polymorphic `variable {Ω : Type*}`. This PR fixes 1 character. Apologies!
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds the last missing implication of the general case of portmanteau equivalent characterizations of convergence in distribution: a sufficient condition for convergence in distribution of a sequence of probability measures is that for all open sets the candidate limit measure is at most the liminf of the measures.
(There are more equivalent conditions dubbed portmanteau for the special case of convergence in distribution on R, though. Some of them are easy and I'll add soon. The ones with characteristic functions require characteristic functions.)
One restriction in this implication is that it really talks about a sequence and the
atTopfilter rather than a general filter like the other implications. The reason is that Fatou's lemma is used (and it is not obvious to me that it could be generalized to much more than countably generated filters in countable types).One design choice in the proof is that I could not use the relevant lemma
Monotone.map_liminf_of_continuousAtto commuteliminfwithENNReal.toReal, since the lemma assumes monotonicity, butENNReal.toRealfails to be monotone because of +infty. I used a truncated variantENNReal.truncateToRealinstead. Perhaps a more principled strategy would have been to prove a generalizationMonotoneOn.map_liminf_of_continuousAt, but it was less straightforward to do the correct statement and proof.