Theorem MeasureTheory.eLpNorm'_enorm_rpow

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'_enorm_rpowView on Github →
2025-05-12 15:41
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
refactor(LpSeminorm/Basic, LpSpace/Basic): generalise more lemmas to enorms (#24640) …
Added MeasureTheory.eLpNorm'_enorm_rpowView on Github →