pdf_mul_eq_mlconvolution_pdf' — Mathlib

English

Independence implies the density of the sum/product equals mlconvolution of marginals.

Русский

Независимость приводит к тому, что плотность суммы/произведения равна mlconvolution маргиналов.

LaTeX

$$$\text{pdf}(X\cdot Y) =^\text{a.e.} pdf X \star_{\mu} pdf Y.$$$

Lean4

@[to_additive]
theorem pdf_mul_eq_mlconvolution_pdf' [SigmaFinite μ] [HasPDF X ℙ μ] [HasPDF Y ℙ μ] (σX : SigmaFinite (ℙ.map X))
    (σY : SigmaFinite (ℙ.map Y)) (hXY : IndepFun X Y ℙ) : pdf (X * Y) ℙ μ =ᵐ[μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ :=
  by
  rw [pdf, hXY.map_mul_eq_map_mconv_map₀' (HasPDF.aemeasurable' μ) (HasPDF.aemeasurable' μ) σX σY]
  apply rnDeriv_mconv' <;> exact HasPDF.absolutelyContinuous

Похожие утверждения