∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : Mul G] [inst_1 : Inv G] (f g : G → ENNReal)
  (μ : MeasureTheory.Measure G) (x : G), MeasureTheory.mlconvolution f g μ x = ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ