mathlib

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