integral_fun_prod_eq_prod_integral

English

Let X be an independent family X_i and a measurable family of functions; then ∫Ω ∏ X_i(ω) dμ(ω) = ∏ i μ[X_i].

Русский

Пусть X_i образуют независимое семейство, и каждая X_i измерима; тогда ∫Ω ∏ X_i(ω) dμ(ω) = ∏ i μ[X_i].

LaTeX

$$$\int_\Omega \prod_i X_i \, d\mu = \prod_i μ[X_i]$$$

Lean4

theorem integral_fun_prod_eq_prod_integral (hX : iIndepFun X μ) (mX : ∀ i, AEStronglyMeasurable (X i) μ) :
    ∫ ω, ∏ i, X i ω ∂μ = ∏ i, μ[X i] :=
  hX.integral_fun_prod_comp (fun i ↦ (mX i).aemeasurable) (fun _ ↦ aestronglyMeasurable_id)

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