theorem MeasureTheory.MemLp.of_bilin' {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m : MeasurableSpace α} [TopologicalSpace E] [ENormedAddCommMonoid E] [TopologicalSpace F] [ENormedAddCommMonoid F] [TopologicalSpace G] [ENormedAddCommMonoid G] {μ : Measure α} {p q r : ENNReal} {f : α → E} {g : α → F} (b : E → F → G) (c : NNReal) (hf : MemLp f p μ) (hg : MemLp g q μ) (h : AEStronglyMeasurable (fun (x : α) => b (f x) (g x)) μ) (hb : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ₑ ≤ ↑c * ‖f x‖ₑ * ‖g x‖ₑ) [hpqr : p.HolderTriple q r] : MemLp (fun (x : α) => b (f x) (g x)) r μ