English
Same as Inde pFun_prodMk with AE-measurability replaced by AE assumptions; independence is preserved under AE-measurable approximations.
Русский
Те же выводы как в IndepFun_prodMk₀ с AE-условиями; независимость сохраняется под AE-приближениями.
LaTeX
$$$\IndepFun (f_i, f_j) (f_k) κ μ$$$
Lean4
theorem indepFun_prodMk₀ (hf_Indep : iIndepFun f κ μ) (hf_meas : ∀ i, AEMeasurable (f i) (κ ∘ₘ μ)) (i j k : ι)
(hik : i ≠ k) (hjk : j ≠ k) : IndepFun (fun a ↦ (f i a, f j a)) (f k) κ μ :=
by
have h : IndepFun (fun a ↦ ((hf_meas i).mk (f i) a, (hf_meas j).mk (f j) a)) ((hf_meas k).mk (f k)) κ μ :=
by
refine iIndepFun.indepFun_prodMk ?_ (fun i ↦ (hf_meas i).measurable_mk) _ _ _ hik hjk
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]
· exact Measure.ae_ae_of_ae_comp (hf_meas k).ae_eq_mk.symm
