Holder inequality

Stream: Is there code for X?

[Alex Kontorovich]

Do we have Holder? Even just an L^1*L^infty\le L^1 bound?

import measure_theory.function.l1_space

open measure_theory

variables {E : Type*} [measurable_space E] (μ : measure E)

example (f g : E → ℂ) (hf : integrable f μ) (hg : mem_ℒp g ∞ μ) :
integrable (λ x, f x * g x) μ :=
begin
  sorry,
end

[Ruben Van de Velde]

There's some versions in src/analysis/mean_inequalities.lean, at least

[Ruben Van de Velde]

Also src/analysis/normed_space/lp_space.lean, src/measure_theory/integral/mean_inequalities.lean