mathlib3

dcb6c865 - feat(measure_theory/function/uniform_integrable): Equivalent condition for uniformly integrable in the probability sense (#12955)

feat(measure_theory/function/uniform_integrable): Equivalent condition for uniformly integrable in the probability sense (#12955) A sequence of functions is uniformly integrable in the probability sense if and only if `∀ ε : ℝ, 0 < ε → ∃ C : ℝ≥0, ∀ i, snorm ({x | C ≤ ∥f i x∥₊}.indicator (f i)) p μ ≤ ennreal.of_real ε`.