English
If X and Y are independent and have PDFs, then their product has a PDF.
Русский
Если X и Y независимы и имеют плотности, то произведение X·Y имеет плотность.
LaTeX
$$$\text{HasPDF}(X\cdot Y) \;\text{under independence and PDFs}.$$$
Lean4
@[to_additive]
theorem mul_hasPDF' [SFinite μ] [HasPDF X ℙ μ] [HasPDF Y ℙ μ] (σX : SigmaFinite (ℙ.map X)) (σY : SigmaFinite (ℙ.map Y))
(hXY : IndepFun X Y ℙ) : HasPDF (X * Y) ℙ μ :=
by
have : AEMeasurable X ℙ := HasPDF.aemeasurable' μ
have : AEMeasurable Y ℙ := HasPDF.aemeasurable' μ
rw [hasPDF_iff_of_aemeasurable (by fun_prop), hXY.map_mul_eq_map_mconv_map₀' (by fun_prop) (by fun_prop) σX σY]
refine ⟨?_, mconv_absolutelyContinuous HasPDF.absolutelyContinuous⟩
apply HaveLebesgueDecomposition.mconv <;> exact HasPDF.absolutelyContinuous
