Theorem MeasureTheory.eLpNorm_count_lt_top_of_lt

Modification history

2026-09-11 14:45
Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
refactor(MeasureTheory): define `eLpNorm f` to be infinite when not `AEStronglyMeasurable` (#42406) …
Modified MeasureTheory.eLpNorm_count_lt_top_of_ltView on Github →
2026-05-04 18:51
Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
refactor(MeasureTheory): golf `Mathlib/MeasureTheory/Function/LpSeminorm/Count` (#38878) …
Modified MeasureTheory.eLpNorm_count_lt_top_of_ltView on Github →
2026-03-06 09:14
Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
feat: lemmas about `Measure.count` (#36205) …
Added MeasureTheory.eLpNorm_count_lt_top_of_ltView on Github →