Theorem Real.summable_Lr_of_Lp_Lq_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.summable_Lr_of_Lp_Lq_of_nonnegView on Github →