integral_mul_eq_integral — Mathlib

English

If X and Y have PDFs and μ is left-invariant under multiplication, then X·Y has a PDF with respect to μ.

Русский

Если X и Y имеют плотности и μ инвариантно слева относительно умножения, то X·Y имеет плотность по отношению к μ.

LaTeX

$$$\text{HasPDF}(X\cdot Y,\mathbb{P},\mu).$$$

Lean4

/-- If `X` is a real-valued random variable that has pdf `f`, then the expectation of `X` equals
`∫ x, x * f x ∂λ` where `λ` is the Lebesgue measure. -/
theorem integral_mul_eq_integral [HasPDF X ℙ] : ∫ x, x * (pdf X ℙ volume x).toReal = ∫ x, X x ∂ℙ :=
  calc
    _ = ∫ x, (pdf X ℙ volume x).toReal * x := by congr with x; exact mul_comm _ _
    _ = _ := integral_pdf_smul measurable_id.aestronglyMeasurable

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