MeasureTheory.eLpNorm'_le_eLpNorm'_mul_eLpNorm''

theorem eLpNorm'_le_eLpNorm'_mul_eLpNorm'' {p q r : ℝ} (hf : AEStronglyMeasurable f μ)    (hg : AEStronglyMeasurable g μ) (b : E → F → G) (c : ℝ≥0)    (h : ∀ᵐ x ∂μ, ‖b (f x) (g x)‖ₑ ≤ c * ‖f x‖ₑ * ‖g x‖ₑ) (hro_lt : 0 < r) (hrp : r < p)    (hpqr : 1 / r = 1 / p + 1 / q) :    eLpNorm' (fun x => b (f x) (g x)) r μ ≤ c * eLpNorm' f p μ * eLpNorm' g q μ := by  calc    eLpNorm' (fun x => b (f x) (g x)) r μ      ≤ eLpNorm' (fun x ↦ c • ‖f x‖ₑ * ‖g x‖ₑ) r μ := by      simp only [eLpNorm']      gcongr ?_ ^ _      refine lintegral_mono_ae <| h.mono fun a ha ↦ ?_      simp only [Algebra.smul_mul_assoc, enorm_eq_self]      gcongr      rwa [ENNReal.smul_def, smul_eq_mul, ← mul_assoc]    _ ≤ c * eLpNorm' f p μ * eLpNorm' g q μ := by      simp only [smul_mul_assoc, ← Pi.smul_def]      apply (eLpNorm'_const_smul_le'' hro_lt).trans      rw [enorm_NNReal, mul_assoc]      gcongr      simpa only [eLpNorm', enorm_mul, enorm_norm] using!        ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr hro_lt hrp hpqr μ hf.enorm hg.enorm