Theorem MeasureTheory.eLpNorm_smul_measure_le

Modification history

2026-07-02 18:37
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
feat: linear map from `L^p (mu)` to `L^p (nu)` when `nu` is bounded by a multiple of `mu` (#40811)
Added MeasureTheory.eLpNorm_smul_measure_leView on Github →