mul_hasPDF — Mathlib

English

Under independence, the product has a density given that X and Y have densities.

Русский

При независимости произведение имеет плотность, если X и Y обладают плотностями.

LaTeX

$$$\text{HasPDF}(X\cdot Y) \text{ under independence and existing PDFs}.$$$

Lean4

@[to_additive]
theorem mul_hasPDF [SFinite μ] [HasPDF X ℙ μ] [HasPDF Y ℙ μ] [IsFiniteMeasure ℙ] (hXY : IndepFun X Y ℙ) :
    HasPDF (X * Y) ℙ μ := by apply hXY.mul_hasPDF' <;> apply IsFiniteMeasure.toSigmaFinite

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