kkytola

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

1

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...

The classes `BoundedSub` and `BoundedMul` were added in PRs #12559 and #12790 to generalize subtraction and multiplication operations on bounded continuous functions (especially for the case of codomain `NNReal`). The...

Add the more interesting direction of topology comparison for the Lévy-Prokhorov distance. Conclude that if the underlying space is separable, then the topology of convergence in distribution coincides with the...