English
If f is iIndepFun and all f i are measurable, then for i ≠ k and j ≠ l with all pairwise distinct, the independence holds between f_i * f_j and f_k * f_l.
Русский
Если iIndepFun f μ и все f_i измеримы, то при i ≠ k, j ≠ l и отсутствии совпадений независимость сохраняется между произведениями f_i f_j и f_k f_l.
LaTeX
$$$ \\operatorname{iIndepFun} f μ \\rightarrow \\bigl(\\forall i, Measurable (f i)\\bigr) \\rightarrow \\forall i j k l, i \\neq k \\rightarrow i \\neq l \\rightarrow j \\neq k \\rightarrow j \\neq l \\rightarrow \\operatorname{IndepFun} (\\instHMul.hMul (f i) (f j)) (instHMul.hMul (f k) (f l)) μ$$$
Lean4
@[to_additive]
theorem indepFun_mul_mul (hf_indep : iIndepFun f μ) (hf_meas : ∀ i, Measurable (f i)) (i j k l : ι) (hik : i ≠ k)
(hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : IndepFun (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
