Theorem MeasureTheory.meas_ge_le_mul_pow_eLpNorm_enorm

Modification history

2025-05-12 13:27
Mathlib/MeasureTheory/Function/LpSeminorm/ChebyshevMarkov.lean
chore(LpSeminorm/ChebyshevMarkov): generalise to enorms (#24482)
Added MeasureTheory.meas_ge_le_mul_pow_eLpNorm_enormView on Github →