English
A strengthened independence result for pairs of product variables with AE-measurability, akin to the Prod MkProdMk₀ case.
Русский
Усиленный вывод независимости для пар переменных произведения с AE-измеримостью.
LaTeX
$$$\IndepFun (f_i, f_j) (f_k, f_l) κ μ$$$
Lean4
theorem indepFun_prodMk_prodMk₀ (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 (fun a ↦ (f i a, f j a)) (fun a ↦ (f k a, f l a)) κ μ :=
by
have h :
IndepFun (fun a ↦ ((hf_meas i).mk (f i) a, (hf_meas j).mk (f j) a))
(fun a ↦ ((hf_meas k).mk (f k) a, (hf_meas l).mk (f l) a)) κ μ :=
by
refine iIndepFun.indepFun_prodMk_prodMk ?_ (fun i ↦ (hf_meas i).measurable_mk) _ _ _ _ hik hil hjk hjl
exact iIndepFun.congr' hf_indep fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk
refine IndepFun.congr' h ?_ ?_
· filter_upwards [Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk, Measure.ae_ae_of_ae_comp (hf_meas j).ae_eq_mk] with a
hi hj
filter_upwards [hi, hj] with ω hωi hωj
rw [← hωi, ← hωj]
· filter_upwards [Measure.ae_ae_of_ae_comp (hf_meas k).ae_eq_mk, Measure.ae_ae_of_ae_comp (hf_meas l).ae_eq_mk] with a
hk hl
filter_upwards [hk, hl] with ω hωk hωl
rw [← hωk, ← hωl]
