indepFun_finset_prod_of_notMem — Mathlib

English

Let the family (f_i) be iIndepFun μ and each f_i be measurable. Then for any finite set s of indices and any i not in s, the product ∏_{j∈s} f_j is independent of f_i.

Русский

Пусть семейство (f_i) является iIndepFun μ и каждая f_i измерима. Тогда для любого конечного множества индексов s и любого i не из s произведение ∏_{j∈s} f_j независимо от f_i.

LaTeX

$$$\\forall s\\in Finset\\ ι,\ \forall i\\notin s:\\ IndepFun\\Big(\\prod_{j\\in s} f_j, f_i\\Big)\\mu$$$

Lean4

@[to_additive]
theorem indepFun_finset_prod_of_notMem (hf_Indep : iIndepFun f μ) (hf_meas : ∀ i, Measurable (f i)) {s : Finset ι}
    {i : ι} (hi : i ∉ s) : IndepFun (∏ j ∈ s, f j) (f i) μ :=
  Kernel.iIndepFun.indepFun_finset_prod_of_notMem hf_Indep hf_meas hi

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