English
If f is a family of independent random variables and each f i is measurable, then the pair (f i, f j) is independent of f k, considered in the product construction.
Русский
Если f — семейство независимых случайных величин и каждый f i измерим, то пара (f i, f j) независима от f k в произведении.
LaTeX
$$$\IndepFun (f i, f j) \; (f k) κ μ$$$
Lean4
theorem indepFun_prodMk (hf_Indep : iIndepFun f κ μ) (hf_meas : ∀ i, Measurable (f i)) (i j k : ι) (hik : i ≠ k)
(hjk : j ≠ k) : IndepFun (fun a => (f i a, f j a)) (f k) κ μ := by
classical
have h_right :
f k =
(fun p : ∀ j : ({ k } : Finset ι), β j => p ⟨k, Finset.mem_singleton_self k⟩) ∘ fun a (j : ({ k } : Finset ι)) =>
f j a :=
rfl
have h_meas_right : Measurable fun p : ∀ j : ({ k } : Finset ι), β j => p ⟨k, Finset.mem_singleton_self k⟩ :=
measurable_pi_apply _
let s : Finset ι := { i, j }
have h_left :
(fun ω => (f i ω, f j ω)) =
(fun p : ∀ l : s, β l =>
(p ⟨i, Finset.mem_insert_self i _⟩, p ⟨j, Finset.mem_insert_of_mem (Finset.mem_singleton_self _)⟩)) ∘
fun a (j : s) => f j a :=
by
ext1 a
simp only
constructor
have h_meas_left :
Measurable fun p : ∀ l : s, β l =>
(p ⟨i, Finset.mem_insert_self i _⟩, p ⟨j, Finset.mem_insert_of_mem (Finset.mem_singleton_self _)⟩) :=
Measurable.prod (measurable_pi_apply _) (measurable_pi_apply _)
rw [h_left, h_right]
refine (hf_Indep.indepFun_finset s { k } ?_ hf_meas).comp h_meas_left h_meas_right
rw [Finset.disjoint_singleton_right]
simp only [s, Finset.mem_insert, Finset.mem_singleton, not_or]
exact ⟨hik.symm, hjk.symm⟩
