Commit 2024-07-20 16:12 f7d51b0b

View on Github →

refactor(MeasureTheory.Function.UniformIntegrable): Rename Vitali convergence related theorems to reflect the IsFiniteMeasure hypothesis. (#14954) Renaming in preparation for the general version of Vitali's convergence theorem in #9163.

Estimated changes

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean

deleted theorem MeasureTheory.tendstoInMeasure_iff_tendsto_Lp

added theorem MeasureTheory.tendstoInMeasure_iff_tendsto_Lp_finite

added theorem MeasureTheory.tendsto_Lp_finite_of_tendstoInMeasure

added theorem MeasureTheory.tendsto_Lp_finite_of_tendsto_ae

added theorem MeasureTheory.tendsto_Lp_finite_of_tendsto_ae_of_meas

deleted theorem MeasureTheory.tendsto_Lp_of_tendstoInMeasure

deleted theorem MeasureTheory.tendsto_Lp_of_tendsto_ae

deleted theorem MeasureTheory.tendsto_Lp_of_tendsto_ae_of_meas

Modified Mathlib/Probability/Martingale/Convergence.lean

Modified Mathlib/Probability/StrongLaw.lean