Commit 2022-03-21 16:35 09750eb8

feat(measure_theory/function/uniform_integrable): add API for uniform integrability in the probability sense (#12678) Uniform integrability in probability theory is commonly defined as the uniform existence of a number for which the expectation of the random variables restricted on the set for which they are greater than said number is arbitrarily small. We have defined it in mathlib, on the other hand, as uniform integrability in the measure theory sense + existence of a uniform bound of the Lp norms. This PR proves the first definition implies the second while a later PR will deal with the reverse direction.