Commit 2025-11-27 12:30 a30baca9

View on Github →

feat: bounded Lp norm of limit if converge in measure (#31882) We prove that if the eLpNorm of a collection of AEStronglyMeasurable functions that converges in measure is bounded by some constant C, then the eLpNorm of its limit is also bounded by C. We also weaken some assumptions in proofs of other theorems.

Estimated changes

Modified Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

added theorem MeasureTheory.eLpNorm_le_of_tendstoInMeasure

modified theorem MeasureTheory.tendstoInMeasure_iff_enorm

modified theorem MeasureTheory.tendstoInMeasure_iff_measureReal_enorm

modified theorem MeasureTheory.tendstoInMeasure_iff_measureReal_norm

modified theorem MeasureTheory.tendstoInMeasure_iff_norm

modified theorem MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_top

Modified Mathlib/MeasureTheory/Function/LpSpace/Complete.lean

added theorem MeasureTheory.Lp.eLpNorm_le_of_ae_tendsto