Commit 2021-09-18 23:07 c1d7ee55

feat(measure_theory/measure/finite_measure_weak_convergence): definitions of types of finite_measures and probability_measures, to be equipped with the topologies of weak convergence (#8904) feat(measure_theory/measure/finite_measure_weak_convergence): definitions of types of finite_measures and probability_measures, to be equipped with the topologies of weak convergence This PR defines the types probability_measure and finite_measure. The next step is to give a topology instance on these types.