feat: Generalize assumptions in liminf and limsup results in ENNReals#15115
feat: Generalize assumptions in liminf and limsup results in ENNReals#15115
Conversation
…map limsup lemmas
…ola/misc_ENNReal_lemmas
…ola/misc_ENNReal_lemmas
|
This PR/issue depends on:
|
|
@kkytola these proofs could use some cleaning up. For example, there is a |
Sorry about this! I had apparently completely forgotten to clean up this part of the refactor which finally obtained the requested generalization. (The only defensible bit in the code is that the variable name The code was in a terrible shape and not ready for review, indeed --- apologies again. I will clean it up! |
|
No problem, thanks! |
| have xs_bdd : ∀ᶠ i in F, xs i ≤ ENNReal.ofReal b := by | ||
| filter_upwards [ev_ne_top, hb] with i ne_top le_b | ||
| exact (ENNReal.le_ofReal_iff_toReal_le ne_top (le_trans toReal_nonneg le_b)).mpr le_b | ||
| have oops := limsup_eq_top ▸ limsup_le_of_le ⟨0, by simp⟩ xs_bdd |
|
Coming here for PR triage: is this PR still relevant? If so, can you merge master and address the review comments, please? (Otherwise, you can also label with help-wanted, to signal that help updating this would be welcome.) |
I think this is still relevant if we want characterizations of convergence in distribution (weak convergence of probability measures) over general filters in Mathlib (although that is unfortunately blocked by a few other trivial preliminaries, too). Merging master looks nontrivial (already the couple of merge-bumps last summer bitrot quite fast), maybe starting from scratch is more realistic. If it would be clear whether this generalization is in principle wanted with this approach, then I could try to return to this in the summer. For now I will mark the PR as "help-wanted". |
In a review comment it was pointed out that results about liminf and limsup in ENNReal hold under milder assumptions. This PR does the generalization.
This PR is split off from #13938, where the review comment was made. The changes needed for the suggested generalization were of different kind than the simple PR's content, justifying a separate PR.