English
Under independence, the joint density equals the product of marginals via mlconvolution.
Русский
При независимости совместная плотность равна произведению модуля плотностей через mlconvolution.
LaTeX
$$$\text{pdf}(X\cdot Y)_{\mu} =^\text{a.e.} pdf X_{\mathbb{P}} pdf Y_{\mathbb{P}}$ через mlconvolution.$$
Lean4
/-- Random variables are independent iff their joint density is a product of marginal densities. -/
theorem indepFun_iff_pdf_prod_eq_pdf_mul_pdf [IsFiniteMeasure ℙ] [SigmaFinite μ] [SigmaFinite ν]
[HasPDF (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν)] :
IndepFun X Y ℙ ↔ pdf (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν) =ᵐ[μ.prod ν] fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2 :=
by
have : HasPDF X ℙ μ := quasiMeasurePreserving_hasPDF' (μ := μ.prod ν) (fun ω ↦ (X ω, Y ω)) quasiMeasurePreserving_fst
have : HasPDF Y ℙ ν := quasiMeasurePreserving_hasPDF' (μ := μ.prod ν) (fun ω ↦ (X ω, Y ω)) quasiMeasurePreserving_snd
have h₀ : (ℙ.map X).prod (ℙ.map Y) = (μ.prod ν).withDensity fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2 :=
prod_eq fun s t hs ht ↦ by
rw [withDensity_apply _ (hs.prod ht), ← prod_restrict,
lintegral_prod_mul (measurable_pdf X ℙ μ).aemeasurable (measurable_pdf Y ℙ ν).aemeasurable,
map_eq_setLIntegral_pdf X ℙ μ hs, map_eq_setLIntegral_pdf Y ℙ ν ht]
rw [indepFun_iff_map_prod_eq_prod_map_map (HasPDF.aemeasurable X ℙ μ) (HasPDF.aemeasurable Y ℙ ν), ←
eq_of_map_eq_withDensity, h₀]
exact (((measurable_pdf X ℙ μ).comp measurable_fst).mul ((measurable_pdf Y ℙ ν).comp measurable_snd)).aemeasurable
