{𝕜 : Type u𝕜} →
  {G : Type uG} →
    {E : Type uE} →
      {E' : Type uE'} →
        {F : Type uF} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : NormedAddCommGroup E'] →
              [inst_2 : NormedAddCommGroup F] →
                [inst_3 : NontriviallyNormedField 𝕜] →
                  [inst_4 : NormedSpace 𝕜 E] →
                    [inst_5 : NormedSpace 𝕜 E'] →
                      [inst_6 : NormedSpace 𝕜 F] →
                        [inst_7 : MeasurableSpace G] →
                          [Sub G] →
                            (G → E) →
                              (G → E') →
                                (E →L[𝕜] E' →L[𝕜] F) →
                                  autoParam (MeasureTheory.Measure G) MeasureTheory.ConvolutionExists._auto_1 → Prop