English
If iIndepFun f μ and AE-measurability holds for all f i, then for i ≠ k and j ≠ l with i ≠ j, independence holds between f_i * f_j and f_k * f_l in AE sense.
Русский
Если iIndepFun f μ и AE-измеримость выполняется для всех f_i, то независимость между f_i f_j и f_k f_l сохраняется в AE-смысле при заданных неравенствах.
LaTeX
$$$ \\operatorname{iIndepFun} f μ \\rightarrow \\bigl(\\forall i, AEMeasurable (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, AEMeasurable (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 (by simp [hf_meas]) i j k l hik hil hjk hjl
