indepFun_finset_prod_of_notMem₀

English

Under the same hypotheses as above but with AEMeasurability, the product over a finite set not containing i is independent of f_i.

Русский

При тех же предпосылках, но с AEMeasurable, произведение по конечному множеству, не содержащее i, независимо от f_i.

LaTeX

$$$\\forall s\\in Finset\\ ι,\ \forall i\\notin s:\\ IndepFun\\Big(\\prod_{j\\in s} f_j, f_i\\Big)\\mu,$ с условием AEMeasurable.$$

Lean4

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

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