Commit 2025-05-12 15:41 c05f2327

View on Github →

refactor(LpSeminorm/Basic, LpSpace/Basic): generalise more lemmas to enorms (#24640) Continuation of #24356, part of #24352.

Estimated changes

Modified Mathlib/Analysis/Normed/MulAction.lean

added theorem IsBoundedSMul.of_enorm_smul_le

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

added theorem MeasureTheory.eLpNorm'_enorm_rpow

added theorem MeasureTheory.eLpNorm_enorm_rpow

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

added theorem MeasureTheory.MemLp.enorm_rpow

added theorem MeasureTheory.MemLp.enorm_rpow_div

added theorem MeasureTheory.memLp_enorm_rpow_iff