English
Let X be an independent family of random variables X_i: Ω→𝓧_i and f_i measurable. Then ∫Ω ∏ i f_i(X_i(ω)) dμ(ω) = ∏ i ∫Ω f_i(X_i(ω)) dμ(ω).
Русский
Пусть имеется независимая семейство случайных величин X_i: Ω→𝓧_i и измеримая семейство f_i. Тогда интеграл по Ω от произведения f_i(X_i(ω)) равен произведению интегралов: ∫Ω ∏_i f_i(X_i(ω)) dμ(ω) = ∏_i ∫Ω f_i(X_i(ω)) dμ(ω).
LaTeX
$$$\int_\Omega \prod_i f_i(X_i(\omega)) \, d\mu(\omega) = \prod_i \int_\Omega f_i(X_i(\omega)) \, d\mu(\omega)$$$
Lean4
theorem integral_fun_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
have := hX.isProbabilityMeasure
change ∫ ω, (fun x ↦ ∏ i, f i (x i)) (X · ω) ∂μ = _
rw [← integral_map (f := fun x ↦ ∏ i, f i (x i)) (φ := fun ω ↦ (X · ω)), (iIndepFun_iff_map_fun_eq_pi_map mX).1 hX,
integral_fintype_prod_eq_prod]
· congr with i
rw [integral_map (mX i) (hf i)]
· fun_prop
rw [(iIndepFun_iff_map_fun_eq_pi_map mX).1 hX]
exact
Finset.aestronglyMeasurable_fun_prod Finset.univ fun i _ ↦
(hf i).comp_quasiMeasurePreserving (Measure.quasiMeasurePreserving_eval _ i)
