Commit 2026-04-15 17:10 cdb1ff9d
View on Github →feat(MeasureTheory/LpSeminorm): add rpow_add_le_mul_rpow_add_rpow' variants (#37547)
Add two variants of ENNReal.rpow_add_le_mul_rpow_add_rpow using LpAddConst as the constant, valid for all 0 ≤ p (not just 1 ≤ p).
Upstreamed from the Carleson project.