English
If f is a mutually independent family with measurability, then the pair of two-indexed function values (f i, f j) is independent from (f k, f l) in the product sense.
Русский
Если f — взаимно независимое семейство и измеримо, то пара (f_i, f_j) независима от (f_k, f_l) в произведении.
LaTeX
$$$\IndepFun (f_i, f_j) (f_k, f_l) κ μ$$$
Lean4
theorem indepFun_prodMk_prodMk (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 (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 (hf_indep.indepFun_finset { i, j } { k, l } (by aesop) hf_meas).comp (hg i j) (hg k l)
