MeasureTheory.eLpNorm_le_eLpNorm_top_mul_eLpNorm'

theorem eLpNorm_le_eLpNorm_top_mul_eLpNorm' (p : ℝ≥0∞) (f : α → E) {g : α → F}    (hg : AEStronglyMeasurable g μ) (b : E → F → G) (c : ℝ≥0)    (h : ∀ᵐ x ∂μ, ‖b (f x) (g x)‖ₑ ≤ c * ‖f x‖ₑ * ‖g x‖ₑ) :    eLpNorm (fun x => b (f x) (g x)) p μ ≤ c * eLpNorm f ∞ μ * eLpNorm g p μ := by  calc    eLpNorm (fun x => b (f x) (g x)) p μ ≤ eLpNorm (fun x => c • ‖f x‖ₑ * ‖g x‖ₑ) p μ :=      eLpNorm_mono_enorm_ae h    _ ≤ c * eLpNorm f ∞ μ * eLpNorm g p μ := ?_  simp only [smul_mul_assoc, ← Pi.smul_def]  apply eLpNorm_const_smul_le''.trans  simp only [enorm_NNReal]  rw [mul_assoc]  gcongr  obtain (rfl | rfl | hp) := ENNReal.trichotomy p  · simp  · rw [← eLpNorm_enorm f, ← eLpNorm_enorm g]    simp_rw [eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm]    exact ENNReal.essSup_mul_le (‖f ·‖ₑ) (‖g ·‖ₑ)  obtain ⟨hp₁, hp₂⟩ := ENNReal.toReal_pos_iff.mp hp  simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp₁.ne' hp₂.ne, eLpNorm_exponent_top,    eLpNormEssSup, one_div, ENNReal.rpow_inv_le_iff hp]  simp only [enorm_eq_self]  rw [ENNReal.mul_rpow_of_nonneg (hz := hp.le), ENNReal.rpow_inv_rpow hp.ne',    ← lintegral_const_mul'' _ (by fun_prop)]  simp only [← ENNReal.mul_rpow_of_nonneg (hz := hp.le)]  apply lintegral_mono_ae  filter_upwards [h, enorm_ae_le_eLpNormEssSup f μ] with x hb hf  gcongr  exact hf