Theorem MeasureTheory.eLpNorm_smul_measure_of_ne_top'

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_smul_measure_of_ne_top'View 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_smul_measure_of_ne_top'View on Github →

2024-11-26 12:47

Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

feat: more `eLpNorm` API (#19293) …

Added MeasureTheory.eLpNorm_smul_measure_of_ne_top'View on Github →