English
If each X_i is a random variable that is almost surely measurable with respect to μ_i, then the family X_i(ω_i) is independent under the product measure π μ.
Русский
Если каждое X_i измеримо почти наверняка относительно μ_i, то семейство X_i(ω_i) независимо по произведению мер.
LaTeX
$$$iIndepFun(\lambda i, Ω_i \mapsto X_i) μ \Rightarrow iIndepFun(\lambda i, Ω_i \mapsto X_i(ω_i)) (Measure.pi μ)$$$
Lean4
/-- Given random variables `X : Ω → 𝓧` and `Y : Ω' → 𝓨`, they are independent when viewed as random
variables defined on the product space `Ω × Ω'`. -/
theorem indepFun_prod (mX : Measurable X) (mY : Measurable Y) : IndepFun (fun ω ↦ X ω.1) (fun ω ↦ Y ω.2) (μ.prod ν) :=
by
refine indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop) |>.2 ?_
convert Measure.map_prod_map μ ν mX mY |>.symm
· rw [← Function.comp_def, ← Measure.map_map mX measurable_fst, Measure.map_fst_prod, measure_univ, one_smul]
· rw [← Function.comp_def, ← Measure.map_map mY measurable_snd, Measure.map_snd_prod, measure_univ, one_smul]
