Commit 2025-05-15 08:57 56a334b0

View on Github →

feat(LpSeminorm/Trim): generalise to enorms (#24842)

Estimated changes

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Trim.lean

modified theorem MeasureTheory.eLpNorm'_trim

modified theorem MeasureTheory.eLpNormEssSup_trim

modified theorem MeasureTheory.eLpNorm_trim

modified theorem MeasureTheory.eLpNorm_trim_ae

modified theorem MeasureTheory.memLp_of_memLp_trim