Theorem NNReal.summable_mul_rpow_of_Lp_Lq

Modification history

2026-03-18 18:48
Mathlib/Analysis/MeanInequalities.lean
feat: generalize Hölder's inequality for sums to `Real.HolderTriple` (#35198) …
Added NNReal.summable_mul_rpow_of_Lp_LqView on Github →