Theorem MeasureTheory.eLpNorm_smul_le_mul_eLpNorm_of_pos

Modification history

2026-09-11 14:45
Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
refactor(MeasureTheory): define `eLpNorm f` to be infinite when not `AEStronglyMeasurable` (#42406) …
Added MeasureTheory.eLpNorm_smul_le_mul_eLpNorm_of_posView on Github →