Commit 2023-03-04 23:57 346bace1
View on Github →feat(measure_theory/function/l1_space): Hölder's inequality specialized to integrable functions (#18550) Specialize Hölder's inequality for scalar product of an integrable and a finite-essential-supremum function.