English
For a countable index, the independent product measure equality holds when projecting onto each X_i; the joint projection equals the product of marginals.
Русский
Для счётного индекса произведение проекции равно произведению маргинальных; совместное распределение равно произведению маргиналов.
LaTeX
$$$\{f : ι \to Ω \to β\} \Rightarrow (\prod) = (\prod) $$$
Lean4
theorem lintegral_prod_eq_prod_lintegral_of_indepFun {ι : Type*} (s : Finset ι) (X : ι → Ω → ℝ≥0∞) (hX : iIndepFun X μ)
(x_mea : ∀ i, Measurable (X i)) : ∫⁻ ω, ∏ i ∈ s, (X i ω) ∂μ = ∏ i ∈ s, ∫⁻ ω, X i ω ∂μ :=
by
have : IsProbabilityMeasure μ := hX.isProbabilityMeasure
induction s using Finset.cons_induction with
| empty => simp only [Finset.prod_empty, lintegral_const, measure_univ, mul_one]
| cons j s hj ihs =>
simp only [← Finset.prod_apply, Finset.prod_cons, ← ihs]
apply lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'
· exact (x_mea j).aemeasurable
· exact s.aemeasurable_prod (fun i _ ↦ (x_mea i).aemeasurable)
· exact (iIndepFun.indepFun_finset_prod_of_notMem hX x_mea hj).symm
