English
For a family (f_n) of random variables, the product of the first n terms is independent of the next term f_n, provided independence and measurability.
Русский
Для семейства (f_n) независимость произведения первых n членов от следующего члена f_n сохраняется при соблюдении условий независимости и измеримости.
LaTeX
$$$\\forall n:\\ IndepFun\\Big(\\prod_{j=0}^{n-1} f_j, f_n\\Big)\\mu$$$
Lean4
@[to_additive]
theorem indepFun_prod_range_succ {f : ℕ → Ω → β} (hf_Indep : iIndepFun f μ) (hf_meas : ∀ i, Measurable (f i)) (n : ℕ) :
IndepFun (∏ j ∈ Finset.range n, f j) (f n) μ :=
Kernel.iIndepFun.indepFun_prod_range_succ hf_Indep hf_meas n