English
Let f be a family of random variables f_i mapping from the sample space Ω to β, and κ be a kernel with base measure μ on α. If (i) the family f is independent in the iIndepFun sense with respect to κ and μ, and (ii) every f_i is Measurable, then for any finite index set s and any i not in s, the product over j in s of f_j is independent from f_i (with respect to κ and μ).
Русский
Пусть последовательность случайных величин f_i: Ω → β образует семейство с независимостью в смысле iIndepFun относительно κ и μ. Пусть каждая f_i измерима. Тогда для любого конечного множества индексов s и любого i, не принадлежащего s, произведение по j в s функций f_j независимо от f_i (относительно κ и μ).
LaTeX
$$$\\text{IndepFun}\\left(\\prod_{j \\in s} f_j\\right)\\left(f_i\\right)\\kappa\\mu$$$
Lean4
@[to_additive]
theorem indepFun_finset_prod_of_notMem (hf_Indep : iIndepFun f κ μ) (hf_meas : ∀ i, Measurable (f i)) {s : Finset ι}
{i : ι} (hi : i ∉ s) : IndepFun (∏ j ∈ s, f j) (f i) κ μ := by
classical
have h_right :
f i =
(fun p : ({ i } : Finset ι) → β => p ⟨i, Finset.mem_singleton_self i⟩) ∘ fun a (j : ({ i } : Finset ι)) =>
f j a :=
rfl
have h_meas_right : Measurable fun p : ({ i } : Finset ι) → β => p ⟨i, Finset.mem_singleton_self i⟩ :=
measurable_pi_apply _
have h_left : ∏ j ∈ s, f j = (fun p : s → β => ∏ j, p j) ∘ fun a (j : s) => f j a :=
by
ext1 a
simp only [Function.comp_apply]
have : (∏ j : ↥s, f (↑j) a) = (∏ j : ↥s, f ↑j) a := by rw [Finset.prod_apply]
rw [this, Finset.prod_coe_sort]
have h_meas_left : Measurable fun p : s → β => ∏ j, p j :=
Finset.univ.measurable_fun_prod fun (j : ↥s) (_H : j ∈ Finset.univ) => measurable_pi_apply j
rw [h_left, h_right]
exact
(hf_Indep.indepFun_finset s { i } (Finset.disjoint_singleton_left.mpr hi).symm hf_meas).comp h_meas_left
h_meas_right
