condIndepSets_singleton_iff — Mathlib

English

Singleton conditioning: independence of single events s and t is equivalent to the product rule for their joint conditional measures.

Русский

Условное независимое по синглтону: независимость единичных событий равнозначна правилу произведения для их условных мер.

LaTeX

$$$CondIndepSets(m',hm',\\{s\\},{t})\\iff μ⟦s∩t|m'⟧ = μ⟦s|m'⟧ \\cdot μ⟦t|m'⟧$$$

Lean4

theorem condIndepSets_singleton_iff {μ : Measure Ω} [IsFiniteMeasure μ] {s t : Set Ω} (hs : MeasurableSet s)
    (ht : MeasurableSet t) : CondIndepSets m' hm' { s } { t } μ ↔ (μ⟦s ∩ t|m'⟧) =ᵐ[μ] (μ⟦s|m'⟧) * (μ⟦t|m'⟧) :=
  by
  rw [condIndepSets_iff _ _ _ _ ?_ ?_]
  · simp only [Set.mem_singleton_iff, forall_eq_apply_imp_iff, forall_eq]
  · intro s' hs'
    rw [Set.mem_singleton_iff] at hs'
    rwa [hs']
  · intro s' hs'
    rw [Set.mem_singleton_iff] at hs'
    rwa [hs']

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