English
Let a finite measure space be given along with a family of random variables f_i taking values in a multiplicative monoid. If the family {f_i} is conditionally independent in the sense of CondIndepFun relative to a base measurable space, and each f_i is measurable, then for any indices i, j, k with i ≠ j and i ≠ k, the pair (f_i) is independent of the product f_j · f_k, i.e., CondIndepFun m' hm' (f_i) (f_j · f_k) μ.
Русский
Пусть дано пространство меры и семейство случайных величин f_i, принимающих значения в моноиде с умножением. Если семейство {f_i} условно независимо в смысле CondIndepFun относительно заданного множества измеримости и каждая f_i measurable, то для любых i, j, k с i ≠ j и i ≠ k верно, что f_i независимо от произведения f_j · f_k: CondIndepFun m' hm' (f_i) (f_j · f_k) μ.
LaTeX
$$$\forall i,j,k,\; i \neq j \land i \neq k \; \Longrightarrow\; \text{CondIndepFun } m' hm' (f_i) (f_j \cdot f_k)\, \mu\,.$$$
Lean4
@[to_additive]
theorem indepFun_mul_right (hf_indep : iCondIndepFun m' hm' f μ) (hf_meas : ∀ i, Measurable (f i)) (i j k : ι)
(hij : i ≠ j) (hik : i ≠ k) : CondIndepFun m' hm' (f i) (f j * f k) μ :=
Kernel.iIndepFun.indepFun_mul_right hf_indep hf_meas i j k hij hik
