suffices : snorm (fun x => ‖f x • g x‖) 1 μ ≤ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
⊢ snorm (f • g) 1 μ ≤ snorm f p μ * snorm g q μ
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
this : snorm (fun x => ‖f x • g x‖) 1 μ ≤ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ
⊢ snorm (f • g) 1 μ ≤ snorm f p μ * snorm g q μ

case this
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
⊢ snorm (fun x => ‖f x • g x‖) 1 μ ≤ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ