integral_prod_comp — Mathlib

English

Let X be an independent finite family X_i and f_i measurable. Then μ[∏ i (f_i ∘ X_i)] = ∏ i μ[(f_i ∘ X_i)].

Русский

Пусть имеется независимое конечное семейство X_i и измеримые функции f_i. Тогда μ[∏_i (f_i ∘ X_i)] = ∏_i μ[(f_i ∘ X_i)].

LaTeX

$$$\mu\Big[\prod_i (f_i \circ X_i)\Big] = \prod_i \mu[(f_i \circ X_i)]$$$

Lean4

theorem integral_prod_comp (hX : iIndepFun X μ) (mX : ∀ i, AEMeasurable (X i) μ)
    (hf : ∀ i, AEStronglyMeasurable (f i) (μ.map (X i))) : μ[∏ i, (f i) ∘ (X i)] = ∏ i, μ[(f i) ∘ (X i)] :=
  by
  convert hX.integral_fun_prod_comp mX hf
  simp

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