English
If iIndepFun f μ and each f i is AE-measurable, then for indices i, j, k, l with i ≠ k, i ≠ l, j ≠ k, j ≠ l, the independence between the two pairs holds in the AE sense.
Русский
Если iIndepFun f μ и каждый f_i AE-измерим, то для i, j, k, 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} (\\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, AEMeasurable (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 (by simp [hf]) i j k l hik hil hjk hjl
