mathlib3

d3997443 - feat(measure_theory/measure/finite_measure_weak_convergence): define the topology of weak convergence of measures and prove some lemmas about it. (#9943)

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 _`. Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>