Commit 2022-07-25 18:14 f22fe49a

feat(measure_theory/measure/finite_measure_weak_convergence): Add normalization of finite measures to probability measures and characterize weak convergence in terms of it. (#15528) This PR adds the definition and basic API about normalization of finite measures to probability measures (divide by the total mass, return junk when total mass vanishes). The weak convergence of finite measures is then characterized in terms of convergence of the total mass and the convergence of the probability normalized measures. This characterization allows to obtain results about the weak convergence of finite measures from the often more convenient considerations of weak convergence of probability measures (some implications of portmanteau theorem, in particular).