Commit 2025-07-26 12:55 cd9fe442

View on Github →

feat: generalise more lemmas to enorms (#27456) The selection of lemmas may seem eclectic, but follows a clear path: these are necessary for generalising the last section of IntegrableOn.lean to enorms.

Estimated changes

Modified Mathlib/Analysis/BoxIntegral/Integrability.lean

Modified Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean

added theorem MeasureTheory.HasFiniteIntegral.of_bounded

added theorem MeasureTheory.HasFiniteIntegral.of_bounded_enorm

added theorem MeasureTheory.HasFiniteIntegral.smul_enorm

deleted theorem MeasureTheory.hasFiniteIntegral_of_bounded

deleted theorem MeasureTheory.hasFiniteIntegral_of_bounded_enorm

Modified Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

added theorem MeasureTheory.Integrable.fun_smul_enorm

added theorem MeasureTheory.Integrable.smul_enorm

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

added theorem MeasureTheory.MemLp.const_mul'

added theorem MeasureTheory.MemLp.const_smul'

added theorem MeasureTheory.eLpNorm'_const_smul_le'

added theorem MeasureTheory.eLpNormEssSup_const_smul_le'

added theorem MeasureTheory.eLpNorm_const_smul_le'

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

added theorem MeasureTheory.HasFiniteIntegral.restrict_of_bounded

added theorem MeasureTheory.HasFiniteIntegral.restrict_of_bounded_enorm

deleted theorem MeasureTheory.hasFiniteIntegral_restrict_of_bounded

Modified Mathlib/MeasureTheory/Integral/Prod.lean

Modified Mathlib/Probability/Martingale/Upcrossing.lean