2025-12-19 18:35
Mathlib/MeasureTheory/Function/UniformIntegrable.lean
feat: the family of limits in probability of sequences of uniformly integrable random variables is uniformly integrable (#31886)
Added MeasureTheory.UnifIntegrable.unifIntegrable_of_ae_tendsto