English
If a family of random variables indexed by ι is mutually conditionally independent, then the subfamily indexed by any two disjoint finite sets S and T are also conditionally independent.
Русский
Если семейство случайных величин, индексируемое по ι, условно взаимно независимо, то подпоследовательности, индексируемые двумя несовпадающими конечными множествами S и T, тоже условно независимы.
LaTeX
$$$\text{Disjoint } S, T \Rightarrow iCondIndepFun\; m' \; hm' \; f \; μ \Rightarrow (\forall i, Measurable (f i)) \Rightarrow \operatorname{CondIndepFun} \; m' \; hm' \; (a \mapsto (f i a)_{i \in S}) \; (a \mapsto (f i a)_{i \in T}) \; μ$$$
Lean4
/-- If `f` is a family of mutually conditionally independent random variables
(`iCondIndepFun m' hm' m f μ`) and `S, T` are two disjoint finite index sets, then the tuple formed
by `f i` for `i ∈ S` is conditionally independent of the tuple `(f i)_i` for `i ∈ T`. -/
theorem condIndepFun_finset {β : ι → Type*} {m : ∀ i, MeasurableSpace (β i)} {f : ∀ i, Ω → β i} (S T : Finset ι)
(hST : Disjoint S T) (hf_Indep : iCondIndepFun m' hm' f μ) (hf_meas : ∀ i, Measurable (f i)) :
CondIndepFun m' hm' (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
