English
If f is i-independently distributed and each f i is measurable, then the tuple of f i over S is independent of the tuple over T for disjoint finite sets S and T.
Русский
Если f образует i-независимую совокупность и каждый f_i измерим, то кортежи f_i на двух попарно несовместных конечных множествах S и T независимы друг от друга.
LaTeX
$$$ \\forall S,T\\;\\bigl(S,T\\text{ дисъюнкты},\\; \\operatorname{hf\\_Indep} : iIndepFun f μ,\\; (\\forall i, \\ Measurable (f i))\\bigr) \\rightarrow \\operatorname{IndepFun} (\\lambda a (i:S) \\mapsto f i a) (\\lambda a (i:T) \\mapsto f i a) μ$$
Lean4
/-- If `f` is a family of mutually independent random variables (`iIndepFun m f μ`) and `S, T` are
two disjoint finite index sets, then the tuple formed by `f i` for `i ∈ S` is independent of the
tuple `(f i)_i` for `i ∈ T`. -/
theorem indepFun_finset (S T : Finset ι) (hST : Disjoint S T) (hf_Indep : iIndepFun f μ)
(hf_meas : ∀ i, Measurable (f i)) : IndepFun (fun a (i : S) ↦ f i a) (fun a (i : T) ↦ f i a) μ :=
Kernel.iIndepFun.indepFun_finset S T hST hf_Indep hf_meas
