∀ {α : 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 α} {f : α → E} {g : α → F}
  {p q r : ENNReal},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      ∀ (b : E → F → G) (c : NNReal),
        (∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊) →
          ∀ [hpqr : p.HolderTriple q r],
            MeasureTheory.eLpNorm (fun x => b (f x) (g x)) r μ ≤
              ↑c * MeasureTheory.eLpNorm f p μ * MeasureTheory.eLpNorm g q μ