Commit 2025-03-10 19:49 268d5377

View on Github →

chore(LpSeminorm/Basic): generalise one more section to ENorm classes (#22801) For the Carleson project.

Estimated changes

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

modified theorem MeasurableEmbedding.eLpNormEssSup_map_measure

modified theorem MeasurableEmbedding.eLpNorm_map_measure

modified theorem MeasurableEmbedding.memLp_map_measure_iff

modified theorem MeasurableEquiv.memLp_map_measure_iff