English
If f is a family of independent random variables in the iIndepFun sense, and each f i is AE-measurable, then the two finite subtuples over S and T are independent.
Русский
Если f образует семью независимых случайных величин в смысле iIndepFun, и каждый f i AE-измерим, то две конечные подпоследовательности на S и T независимы.
LaTeX
$$$\text{IndepFun } (f_i)_{i\in S} \; (f_j)_{j\in T} κ μ$$$
Lean4
theorem indepFun_finset₀ (S T : Finset ι) (hST : Disjoint S T) (hf_Indep : iIndepFun f κ μ)
(hf_meas : ∀ i, AEMeasurable (f i) (κ ∘ₘ μ)) : IndepFun (fun a (i : S) ↦ f i a) (fun a (i : T) ↦ f i a) κ μ :=
by
have h : IndepFun (fun a (i : S) ↦ (hf_meas i).mk (f i) a) (fun a (i : T) ↦ (hf_meas i).mk (f i) a) κ μ :=
by
refine iIndepFun.indepFun_finset S T hST ?_ fun i ↦ (hf_meas i).measurable_mk
exact iIndepFun.congr' hf_Indep fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk
refine IndepFun.congr' h ?_ ?_
· have : ∀ᵐ (a : α) ∂μ, ∀ (i : S), f i =ᵐ[κ a] (hf_meas i).mk :=
by
rw [ae_all_iff]
exact fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk
filter_upwards [this] with a ha
filter_upwards [ae_all_iff.2 ha] with b hb
ext i
exact (hb i).symm
· have : ∀ᵐ (a : α) ∂μ, ∀ (i : T), f i =ᵐ[κ a] (hf_meas i).mk :=
by
rw [ae_all_iff]
exact fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk
filter_upwards [this] with a ha
filter_upwards [ae_all_iff.2 ha] with b hb
ext i
exact (hb i).symm
