∀ {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [inst : AddGroup G]
  {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant]
  {X Y : Ω → G} [MeasureTheory.SFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ],
  MeasureTheory.SigmaFinite (MeasureTheory.Measure.map X ℙ) →
    MeasureTheory.SigmaFinite (MeasureTheory.Measure.map Y ℙ) →
      ProbabilityTheory.IndepFun X Y ℙ → MeasureTheory.HasPDF (X + Y) ℙ μ