Theorem Real.HolderTriple.all_pos

Modification history

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