∀ {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [inst : Group G]
  {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant]
  {X Y : Ω → G} [MeasureTheory.SigmaFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ],
  MeasureTheory.SigmaFinite (MeasureTheory.Measure.map X ℙ) →
    MeasureTheory.SigmaFinite (MeasureTheory.Measure.map Y ℙ) →
      ProbabilityTheory.IndepFun X Y ℙ →
        MeasureTheory.pdf (X * Y) ℙ μ =ᵐ[μ]
          MeasureTheory.mlconvolution (MeasureTheory.pdf X ℙ μ) (MeasureTheory.pdf Y ℙ μ) μ