English
If a family {f_i} of random variables is conditionally independent and each f_i is measurable, then the products f_i f_j and f_k f_l are independent provided i, j, k, l are pairwise distinct in the sense that i ≠ k, i ≠ l, j ≠ k, j ≠ l.
Русский
Если семейство случайных величин {f_i} условно независимо и каждая f_i измерима, то произведения f_i f_j и f_k f_l независимы при попарной неравности индексов: i ≠ k, i ≠ l, j ≠ k, j ≠ l.
LaTeX
$$$\forall i,j,k,l,\; i \neq k \land i \neq l \land j \neq k \land j \neq l \;\Rightarrow\; \text{CondIndepFun } m' hm' (f_i f_j) (f_k f_l)\, μ.$$$
Lean4
@[to_additive]
theorem indepFun_mul_mul (hf_indep : iCondIndepFun m' hm' f μ) (hf_meas : ∀ i, Measurable (f i)) (i j k l : ι)
(hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : CondIndepFun m' hm' (f i * f j) (f k * f l) μ :=
Kernel.iIndepFun.indepFun_mul_mul hf_indep hf_meas i j k l hik hil hjk hjl
