English
If iIndepFun f μ and all f i are measurable, then for indices i, j, k, l with i ≠ k, i ≠ l, j ≠ k, j ≠ l, the pair of pairs (f i, f j) is independent of (f k, f l).
Русский
Если iIndepFun f μ и все f_i измеримы, то для i,j,k,l с несколькими различиями независимость между парой пар сохраняется.
LaTeX
$$$ \\operatorname{iIndepFun} f μ \\rightarrow (\\forall i, \\Measurable (f i)) \\rightarrow \\forall i j k l, i \\neq k \\rightarrow i \\neq l \\rightarrow j \\neq k \\rightarrow j \\neq l \\rightarrow \\operatorname{IndepFun} (\\lambda a \\mapsto (f i a, f j a)) (\\lambda a \\mapsto (f k a, f l a)) μ$$$
Lean4
theorem indepFun_prodMk_prodMk (h_indep : iIndepFun f μ) (hf : ∀ i, Measurable (f i)) (i j k l : ι) (hik : i ≠ k)
(hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : IndepFun (fun a ↦ (f i a, f j a)) (fun a ↦ (f k a, f l a)) μ :=
Kernel.iIndepFun.indepFun_prodMk_prodMk h_indep hf i j k l hik hil hjk hjl
