Theorem NNReal.Lr_rpow_le_Lp_mul_Lq_tsum

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.Lr_rpow_le_Lp_mul_Lq_tsumView on Github →