integral_prod_eq_prod_integral — Mathlib

English

Let X be an independent family X_i and mX measurables. Then μ[∏ X_i] = ∏ μ[X_i].

Русский

Пусть X_i образуют независимое семейство и каждое X_i измеримо. Тогда μ[∏_i X_i] = ∏_i μ[X_i].

LaTeX

$$$\mu\Big[\prod_i X_i\Big] = \prod_i \mu[X_i]$$$

Lean4

theorem integral_prod_eq_prod_integral (hX : iIndepFun X μ) (mX : ∀ i, AEStronglyMeasurable (X i) μ) :
    μ[∏ i, X i] = ∏ i, μ[X i] :=
  hX.integral_prod_comp (fun i ↦ (mX i).aemeasurable) (fun _ ↦ aestronglyMeasurable_id)

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