pdf_mul_eq_mlconvolution_pdf — Mathlib

English

Independent X and Y yield the joint density equal to mlconvolution of their densities almost everywhere.

Русский

Независимые X и Y дают совместную плотность, равную mlconvolution плотностей X и Y almost everywhere.

LaTeX

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

Lean4

@[to_additive]
theorem pdf_mul_eq_mlconvolution_pdf [SFinite μ] [HasPDF X ℙ μ] [HasPDF Y ℙ μ] [IsFiniteMeasure ℙ]
    (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' μ)]
  apply rnDeriv_mconv <;> exact HasPDF.absolutelyContinuous

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