Theorem MeasureTheory.eLpNorm_le_of_ae_enorm_bound

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_ae_enorm_boundView on Github →
2025-08-16 12:53
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
feat: e-seminormed monoid (#27385) …
Modified MeasureTheory.eLpNorm_le_of_ae_enorm_boundView on Github →
2025-03-09 18:34
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
chore(MeasureTheory/Function/LpSeminorm/Basic): generalise more results to enorm classes (#22708) …
Modified MeasureTheory.eLpNorm_le_of_ae_enorm_boundView on Github →
2025-03-05 16:21
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
feat: add enorm versions of many nnnorm lemmas (#22175) …
Added MeasureTheory.eLpNorm_le_of_ae_enorm_boundView on Github →