English
Two random variables X and Y defined on Ω and Ω' are independent when considered on the product space with μ × ν.
Русский
Две случайные величины X и Y на пространствах Ω и Ω' независимы, если их совместное распределение на произведении пространств является произведением маргинальных распределений.
LaTeX
$$$IndepFun(\lambda ω, X ω) (λ ω, Y ω) (μ \otimes ν)$$$
Lean4
/-- Given random variables `X : Ω → 𝓧` and `Y : Ω' → 𝓨`, they are independent when viewed as random
variables defined on the product space `Ω × Ω'`. -/
theorem indepFun_prod₀ (mX : AEMeasurable X μ) (mY : AEMeasurable Y ν) :
IndepFun (fun ω ↦ X ω.1) (fun ω ↦ Y ω.2) (μ.prod ν) :=
by
have : IndepFun (fun ω ↦ mX.mk X ω.1) (fun ω ↦ mY.mk Y ω.2) (μ.prod ν) :=
indepFun_prod mX.measurable_mk mY.measurable_mk
refine this.congr ?_ ?_
· rw [← Function.comp_def, ← Function.comp_def]
apply ae_eq_comp
· exact measurable_fst.aemeasurable
· rw [measurePreserving_fst.map_eq]
exact (AEMeasurable.ae_eq_mk mX).symm
· rw [← Function.comp_def, ← Function.comp_def]
apply ae_eq_comp
· exact measurable_snd.aemeasurable
· rw [measurePreserving_snd.map_eq]
exact (AEMeasurable.ae_eq_mk mY).symm
