Commit 2022-04-27 14:57 d3997443

feat(measure_theory/measure/finite_measure_weak_convergence): define the topology of weak convergence of measures and prove some lemmas about it. (#9943) This PR has the definition of the topology of weak convergence ("convergence in law" / "convergence in distribution") on finite_measure _ and on probability_measure _.