English
If X and Y are AEMeasurable (with respect to μ and ν respectively), then IndepFun for (X on Ω) and (Y on Ω') holds under μ × ν.
Русский
Если X и Y являются АЕ-измеримыми относительно μ и ν, то независимость для (X на Ω) и (Y на Ω') верна по мере μ × ν.
LaTeX
$$$IndepFun( X, Y, μ \otimes ν )$ with AEMeasurability assumptions$$
Lean4
/-- Given random variables `X i : Ω i → 𝓧 i`, they are independent when viewed as random
variables defined on the product space `Π i, Ω i`. -/
theorem iIndepFun_pi (mX : ∀ i, AEMeasurable (X i) (μ i)) : iIndepFun (fun i ω ↦ X i (ω i)) (Measure.pi μ) :=
by
refine iIndepFun_iff_map_fun_eq_pi_map ?_ |>.2 ?_
· exact fun i ↦ (mX i).comp_quasiMeasurePreserving (Measure.quasiMeasurePreserving_eval _ i)
rw [Measure.pi_map_pi mX]
congr
ext i : 1
rw [← (measurePreserving_eval μ i).map_eq, AEMeasurable.map_map_of_aemeasurable, Function.comp_def]
· rw [(measurePreserving_eval μ i).map_eq]
exact mX i
· exact (measurable_pi_apply i).aemeasurable
