integral_comp_mul_comp — Mathlib

English

If X and Y are independent and measurable random variables, then the integral of the composed products equals the product of the integrals of the components.

Русский

Если X и Y независимы и измеримы, то интеграл состава композиции равен произведению интегралов компонентов.

LaTeX

$$$\text{IndepFun } X Y μ \Rightarrow \int (f(X) g(Y)) dμ = (\int f(X) dμ)(\int g(Y) dμ)$$$

Lean4

theorem integral_comp_mul_comp {𝓧 𝓨 : Type*} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {X : Ω → 𝓧} {Y : Ω → 𝓨}
    {f : 𝓧 → 𝕜} {g : 𝓨 → 𝕜} (hXY : IndepFun X Y μ) (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
    (hf : AEStronglyMeasurable f (μ.map X)) (hg : AEStronglyMeasurable g (μ.map Y)) :
    μ[(f ∘ X) * (g ∘ Y)] = μ[f ∘ X] * μ[g ∘ Y] :=
  hXY.integral_fun_comp_mul_comp hX hY hf hg

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