exact memL1_Lp_mul_Lq hpq hf hg
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ Memℒp (f * g) 1
no goals