Commit 2022-04-11 16:38 dcb6c865
View on Github →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 ε.