English
A general equivalence: CondIndep m' m1 m2 hm' μ is equivalent to the statement that for all finite S ⊆ ι, and suitable f_i, the conditional expectation of the intersection equals the product of the conditional expectations, almost surely.
Русский
Общее эквивалентное утверждение: CondIndep m' m1 m2 hm' μ эквивалентно тому, что для любого конечного поднабора S и подходящих множеств f_i, условное ожидание пересечения равняется произведению условных ожиданий, почти surely.
LaTeX
$$$CondIndep(m', hm', m, μ) \\iff \\forall S\\subseteq_f ι, \\{f_i\\}, (\\forall i\\in S, f_i \\text{ MeasurableSet under } m_i) \\Rightarrow μ⟦⋂ i∈S f_i|m'⟧ =ᵐ[μ] ∏_{i∈S} μ⟦f_i|m'⟧$$
Lean4
theorem condIndep_iff (m' m₁ m₂ : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (hm' : m' ≤ mΩ)
(hm₁ : m₁ ≤ mΩ) (hm₂ : m₂ ≤ mΩ) (μ : Measure Ω) [IsFiniteMeasure μ] :
CondIndep m' m₁ m₂ hm' μ ↔
∀ t1 t2, MeasurableSet[m₁] t1 → MeasurableSet[m₂] t2 → (μ⟦t1 ∩ t2|m'⟧) =ᵐ[μ] (μ⟦t1|m'⟧) * (μ⟦t2|m'⟧) :=
by
rw [condIndep_iff_condIndepSets, condIndepSets_iff]
· rfl
· exact hm₁
· exact hm₂
