condIndepFun_finset_prod_of_notMem

English

Let hf_Indep be a CondIndepFun family {f_i}. For any finite set s of indices and an index i not in s, the product of f_j over j in s is CondIndepFun with respect to f_i, i.e., the product variable is independent of f_i.

Русский

Пусть hf_Indep задаёт CondIndepFun семейство {f_i}. Для любого конечного набора индексов s и индекса i, не принадлежащего s, произведение по j∈s f_j независимо от f_i.

LaTeX

$$$\forall s:\text{Finset } ι, \; \forall i\notin s, \; \text{CondIndepFun } m' hm' (\prod_{j\in s} f_j) (f_i) μ.$$$

Lean4

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

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