English
Let Ω be a standard Borel space with a fixed measurable space m' ≤ mΩ and a family (m_i)_{i∈ι} of measurable subspaces of Ω (each m_i ≤ mΩ). For any finite measure μ on Ω, the conditional independence of m' from the family (m_i) with respect to μ is equivalent to the conditional independence of m' from the family of σ-algebras generated by each m_i.
Русский
Пусть Ω — стандартное пространство Бореля, m' ≤ mΩ и семейство сигма-алгебр (m_i) индексации ι. Для конечной меры μ на Ω условная независимость m' от семейства (m_i) относительно μ эквивалентна условной независимости m' от семейства сигма-алгебр, образованных каждой m_i.
LaTeX
$$$i\\text{CondIndep}(m', hm', m, \\mu) \\iff i\\text{CondIndepSets}(m', hm', (\\lambda x . \\{S : \\Omega \\mid \\text{MeasurableSet}[m_x]\, S\\}), \\mu)$$$
Lean4
theorem iCondIndep_iff_iCondIndepSets (m : ι → MeasurableSpace Ω) (μ : @Measure Ω mΩ) [IsFiniteMeasure μ] :
iCondIndep m' hm' m μ ↔ iCondIndepSets m' hm' (fun x ↦ {s | MeasurableSet[m x] s}) μ := by
simp only [iCondIndep, iCondIndepSets, Kernel.iIndep]
