English
Given a sequence of measurable X_i, the products over finite ranges are independent of the next term; i.e., conditional independence of the partial product and the next term.
Русский
Для последовательности измеримых X_i произведение первых n членов независимо от следующего члена.
LaTeX
$$$\forall n,\; \text{CondIndepFun } m' hm' (\prod_{j< n} f_j) (f_n) μ.$$$
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_infinitePi (mX : ∀ i, Measurable (X i)) : iIndepFun (fun i ω ↦ X i (ω i)) (infinitePi μ) :=
by
refine iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop) |>.2 ?_
rw [infinitePi_map_pi _ mX]
congr
ext i : 1
rw [← (measurePreserving_eval_infinitePi μ i).map_eq, map_map (mX i) (by fun_prop), Function.comp_def]
