condIndep_iff_condIndepSets — Mathlib

English

The conditional independence of m' from two sub-sigma-algebras m1 and m2 with respect to μ is equivalent to the conditional independence of m' from the pair of σ-algebras generated respectively by m1 and m2.

Русский

Условная независимость m' от двух сигма-алгебр m1, m2 относительно μ эквивалентна условной независимости m' от пары сигма-алгебр, порождённых m1 и m2.

LaTeX

$$$CondIndep(m', hm', m_1, m_2, hm', μ) \\iff CondIndepSets(m', hm', {s \\mid MeasurableSet[m_1] s}, {s \\mid MeasurableSet[m_2] s}, μ)$$

Lean4

theorem condIndep_iff_condIndepSets (m' m₁ m₂ : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω]
    (hm' : m' ≤ mΩ) (μ : Measure Ω) [IsFiniteMeasure μ] :
    CondIndep m' m₁ m₂ hm' μ ↔ CondIndepSets m' hm' {s | MeasurableSet[m₁] s} {s | MeasurableSet[m₂] s} μ := by
  simp only [CondIndep, CondIndepSets, Kernel.Indep]

Похожие утверждения