condIndepSet_iff — Mathlib

English

CondIndepSet_iff_condIndep: independence of two sets s,t is equivalent to independence of induced events in the product sense.

Русский

Условная независимость множеств s,t эквивалентна независимости порожденных событий в произведении вероятностей.

LaTeX

$$$CondIndepSet(m', hm', s, t, μ) \\iff CondIndep(m', generateFrom\\{s\\}, generateFrom\\{t\\}, hm', μ)$$$

Lean4

theorem condIndepSet_iff (s t : Set Ω) (hs : MeasurableSet s) (ht : MeasurableSet t) (μ : Measure Ω)
    [IsFiniteMeasure μ] : CondIndepSet m' hm' s t μ ↔ (μ⟦s ∩ t|m'⟧) =ᵐ[μ] (μ⟦s|m'⟧) * (μ⟦t|m'⟧) := by
  rw [condIndepSet_iff_condIndepSets_singleton _ _ hs ht μ, condIndepSets_singleton_iff _ _ hs ht]

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