Theorem ENNReal.rpow_add_le_mul_rpow_add_rpow''

Modification history

2026-04-15 17:10
Mathlib/Analysis/MeanInequalitiesPow.lean
feat(MeasureTheory/LpSeminorm): add `rpow_add_le_mul_rpow_add_rpow'` variants (#37547) …
Added ENNReal.rpow_add_le_mul_rpow_add_rpow''View on Github →