mathlib3

f28023e9 - feat(measure_theory/function/uniform_integrable): Uniform integrability and Vitali convergence theorem (#12408)

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.