Theorem MeasureTheory.eLpNorm_le_of_measure_le_smul

Modification history

2026-09-11 14:45
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
refactor(MeasureTheory): define `eLpNorm f` to be infinite when not `AEStronglyMeasurable` (#42406) …
Modified MeasureTheory.eLpNorm_le_of_measure_le_smulView on Github →
2026-07-02 18:37
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
feat: linear map from `L^p (mu)` to `L^p (nu)` when `nu` is bounded by a multiple of `mu` (#40811)
Added MeasureTheory.eLpNorm_le_of_measure_le_smulView on Github →