∀ {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) ∂μ