indepSet_iff_measure_inter_eq_mul

English

Independence of two events s and t is equivalent to the almost-everywhere equality κ a (s ∩ t) = κ a s · κ a t.

Русский

Независимость двух событий s и t эквивалентна почти наверняка равенству κ a (s ∩ t) = κ a s · κ a t.

LaTeX

$$$IndepSet s t κ μ \Leftrightarrow \forall^\text{ae}_{μ}, κ a (s \cap t) = κ a s \cdot κ a t$$$

Lean4

theorem indepSet_iff_measure_inter_eq_mul {_m0 : MeasurableSpace Ω} (hs_meas : MeasurableSet s)
    (ht_meas : MeasurableSet t) (κ : Kernel α Ω) (μ : Measure α) [IsZeroOrMarkovKernel κ] :
    IndepSet s t κ μ ↔ ∀ᵐ a ∂μ, κ a (s ∩ t) = κ a s * κ a t :=
  (indepSet_iff_indepSets_singleton hs_meas ht_meas κ μ).trans indepSets_singleton_iff

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