Theorem Real.Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg

Modification history

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