Advice on proving theorem on sum of random variables

Stream: mathlib4

[David Ledvinka]

I would like to contribute to Mathlib by proving that if $X$ and $Y$ are two independent random variables with pdfs $p$ and $q$ then the pdf of $X + Y$ is the convolution $p * q$ (In particular I would like to prove the identity for the sum of independent Gaussians). The most general and natural way I would think of doing this would be to prove:

For a monoid "$M$":

1. If $X \sim \mu$ and $Y \sim \nu$ are independent random variables taking values in $M$ then the distribution of $XY$ is given by the convolution of $\mu$ with $\nu$.

For a group "$G$":

2. If $\lambda$ is a (left/right) invariant measure on $G$ and $\mu,\nu$ are measures on $G$ with densities $f,g$ w.r.t $\lambda$ respectively, then the convolution of $\mu$ with $\nu$ has density given by the convolution of $f$ and $g$ with respect to $\lambda$ (appropriately defined).

Trying to come up with a statement for 2 I ran into some issues and figured I should ask for advice. Two of the main issues arise from the definition of convolution of functions in mathlib which do not allow for the group to be non-commutative and do not allow for the domain to be the extended reals (or extended non-negative reals). I could still use this definition by dropping some level of generality but even then I find a statement of 2 quite unwieldy because for example you need to take in $f,g : G \to [0,\infty)$, convert them to $G \to [0,\infty]$ so they can be turned into densities, convert them to $G \to \R$ so that you can take a convolution, and then convert the output back to $G \to [0,\infty]$ so it can again be converted into a density. Perhaps this could be all resolved by defining a convolution on functions $G \to [0,\infty]$ but perhaps this would lead to too much confusion / proof duplication from the other notion of convolution and I am not sure if this is a good idea? Perhaps there is a better way to resolve this issue?

[David Ledvinka]

I wrote up this proof of "Step 1". Would love some feedback on the proof structure since I read all of MIL but noticed that many of the proofs in Mathlib look nothing like the proofs in MIL (featuring heavy use of simp etc...)

/- Imports -/
import Mathlib.MeasureTheory.Group.Convolution
import Mathlib.Probability.Independence.Basic

open MeasureTheory ProbabilityTheory Measure AEMeasurable
--open scoped ENNReal

section indepFun

@[to_additive]
theorem IndepFun.map_mul_eq_conv_map_map {M : Type*} [Monoid M] [MeasurableSpace M]
    [MeasurableMul₂ M] {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ]
    {f : Ω → M} {g : Ω → M} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) (hfg : IndepFun f g μ):
    μ.map (f * g) = (μ.map f) ∗ (μ.map g) := by
  have : f * g = (fun (x,y) ↦ x * y) ∘ (fun ω ↦ (f ω, g ω)) := by rfl
  rw[this, ← map_map_of_aemeasurable measurable_mul.aemeasurable (AEMeasurable.prodMk hf hg),
     (indepFun_iff_map_prod_eq_prod_map_map hf hg).mp hfg]
  rfl

end indepFun

[Etienne Marion]

Because we have docs#MeasureTheory.lintegral for ENNReal-valued functions and docs#MeasureTheory.integral for NormedAddCommGroup-valued functions, I think it would make sense to define MeasureTheory.lconvolution.