∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m : MeasurableSpace α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.Measure α} (p : ENNReal)
  (f : α → E) {g : α → F},
  MeasureTheory.AEStronglyMeasurable g μ →
    ∀ (b : E → F → G) (c : NNReal),
      (∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊) →
        MeasureTheory.eLpNorm (fun x => b (f x) (g x)) p μ ≤
          ↑c * MeasureTheory.eLpNorm f ⊤ μ * MeasureTheory.eLpNorm g p μ