English
If iCondIndepFun holds for a family {f_i}, then the pair of two-pairs (f_i, f_j) and (f_k, f_l) are independent when indices i,j,k,l are all distinct pairwise.
Русский
Если для семейства {f_i} выполняется условная независимость, то пара двойка (f_i, f_j) и (f_k, f_l) независимы при попарно различии индексов.
LaTeX
$$$\operatorname{CondIndepFun} \; m' \; hm' \; (f_i, f_j) \; (f_k, f_l) \; μ$$$
Lean4
theorem condIndepFun_prodMk_prodMk (h_indep : iCondIndepFun m' hm' f μ) (hf : ∀ i, Measurable (f i)) (i j k l : ι)
(hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) :
CondIndepFun m' hm' (fun a ↦ (f i a, f j a)) (fun a ↦ (f k a, f l a)) μ := by
classical
let g (i j : ι) (v : Π x : ({ i, j } : Finset ι), β x) : β i × β j :=
⟨v ⟨i, mem_insert_self _ _⟩, v ⟨j, mem_insert_of_mem <| mem_singleton_self _⟩⟩
have hg (i j : ι) : Measurable (g i j) := by fun_prop
exact (h_indep.indepFun_finset { i, j } { k, l } (by aesop) hf).comp (hg i j) (hg k l)
