Commit 2025-12-19 18:35 cd8ba0f6

View on Github →

feat: the family of limits in probability of sequences of uniformly integrable random variables is uniformly integrable (#31886)

Estimated changes

Modified Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

modified theorem MeasureTheory.TendstoInMeasure.comp

added theorem MeasureTheory.TendstoInMeasure.indicator

modified theorem MeasureTheory.TendstoInMeasure.mono

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean

added theorem MeasureTheory.UnifIntegrable.unifIntegrable_of_ae_tendsto

added theorem MeasureTheory.UnifIntegrable.unifIntegrable_of_tendstoInMeasure

added theorem MeasureTheory.UniformIntegrable.uniformIntegrable_of_ae_tendsto

added theorem MeasureTheory.UniformIntegrable.uniformIntegrable_of_tendstoInMeasure