integral_mul_eq_mul_integral — Mathlib

English

Let X,Y: Ω → 𝕜 be independent random variables that are measurable with respect to μ. Then the expectation of their product equals the product of their expectations: ∫Ω X(ω)Y(ω) dμ(ω) = (∫Ω X(ω) dμ(ω))·(∫Ω Y(ω) dμ(ω)).

Русский

Пусть X,Y: Ω → 𝕜 — независимые случайные величины, измеримые относительно μ. Тогда математическое ожидание произведения равно произведению математических ожиданий: ∫Ω X(ω)Y(ω) dμ(ω) = (∫Ω X(ω) dμ(ω))·(∫Ω Y(ω) dμ(ω)).

LaTeX

$$$\int_\Omega X \cdot Y \, d\mu = \left(\int_\Omega X \, d\mu\right)\left(\int_\Omega Y \, d\mu\right)$$$

Lean4

theorem integral_mul_eq_mul_integral (hXY : IndepFun X Y μ) (hX : AEStronglyMeasurable X μ)
    (hY : AEStronglyMeasurable Y μ) : μ[X * Y] = μ[X] * μ[Y] :=
  hXY.integral_comp_mul_comp hX.aemeasurable hY.aemeasurable aestronglyMeasurable_id aestronglyMeasurable_id

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