Theorem MeasureTheory.lpNorm_exponent_zero

Modification history

2026-09-11 14:45
Mathlib/MeasureTheory/Function/LpSeminorm/LpNorm.lean
refactor(MeasureTheory): define `eLpNorm f` to be infinite when not `AEStronglyMeasurable` (#42406) …
Modified MeasureTheory.lpNorm_exponent_zeroView on Github →
2026-02-09 07:29
Mathlib/MeasureTheory/Function/LpSeminorm/LpNorm.lean
feat: real-valued Lᵖ norm (#23881)
Added MeasureTheory.lpNorm_exponent_zeroView on Github →