English
For every finite subset S ⊆ ι and every family of sets f_i ∈ m_i with each f_i measurable, the conditional probability of the intersection equals the product of the conditional probabilities given m'. More precisely, μ⟦⋂ i∈S f_i | m'⟧ =ᵐ[μ] ∏ i∈S μ⟦f_i | m'⟧.
Русский
Для любого конечного подмножества S ⊆ ι и любой семейство множеств f_i ∈ m_i, где каждый f_i измерим, условная вероятность пересечения равна произведению условных вероятностей: μ⟦⋂ i∈S f_i | m'⟧ =ᵐ[μ] ∏ i∈S μ⟦f_i | m'⟧.
LaTeX
$$$\\forall S \\subseteq_f \\iota,\\; \\forall f : \\iota \\to \\mathcal{P}(\\Omega), \\; (\\forall i \\in S, \\text{MeasurableSet}[m_i](f_i)) \\;: \\\\ μ\\lVert\\big\\langle \\bigcap_{i\\in S} f_i \\big| m' \\big\\rVert = ᵐ[μ] \\prod_{i\\in S} μ\\lVert f_i \\mid m' \\rVert$$$
Lean4
theorem iCondIndep_iff (m : ι → MeasurableSpace Ω) (hm : ∀ i, m i ≤ mΩ) (μ : @Measure Ω mΩ) [IsFiniteMeasure μ] :
iCondIndep m' hm' m μ ↔
∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i, i ∈ s → MeasurableSet[m i] (f i)),
μ⟦⋂ i ∈ s, f i|m'⟧ =ᵐ[μ] ∏ i ∈ s, (μ⟦f i|m'⟧) :=
by
rw [iCondIndep_iff_iCondIndepSets, iCondIndepSets_iff]
· rfl
· exact hm
