Commit 2022-03-07 19:47 f28023e9

feat(measure_theory/function/uniform_integrable): Uniform integrability and Vitali convergence theorem (#12408) This PR defines uniform integrability (both in the measure theory sense as well as the probability theory sense) and proves the Vitali convergence theorem which establishes a relation between convergence in measure and uniform integrability with convergence in Lp.