mathlib

346bace1 - feat(measure_theory/function/l1_space): Hölder's inequality specialized to integrable functions (#18550)

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. Co-authored-by: Alex Kontorovich <58564076+AlexKontorovich@users.noreply.github.com>