indepFun_prod_range_succ — Mathlib

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

Похожие утверждения