English
Let s be a finite subset of Ω and let u, t be subsets of Ω. Then the law of total probability for the uniform distribution on s holds: the probability of t under the uniform distribution on s equals the probability of t under the uniform distribution on s∩u times the probability of u under the uniform distribution on s, plus the probability of t under the uniform distribution on s∩uᶜ times the probability of uᶜ under the uniform distribution on s.
Русский
Пусть s — конечное множество подмножеств Ω, а u, t — подмножества Ω. Тогда для равномерного распределения на s выполняется закон полной вероятности: вероятность t при равномерном распределении на s равна сумме вероятности t при разделении s на s∩u и s∩uᶜ, умноженной на соответствующую вероятность раздела s на u или uᶜ.
LaTeX
$$$\operatorname{uniformOn}(s \cap u, t) \cdot \operatorname{uniformOn}(s, u) + \operatorname{uniformOn}(s \cap u^{\complement}, t) \cdot \operatorname{uniformOn}(s, u^{\complement}) = \operatorname{uniformOn}(s, t)$$$
Lean4
/-- A version of the law of total probability for counting probabilities. -/
theorem uniformOn_add_compl_eq (u t : Set Ω) (hs : s.Finite) :
uniformOn (s ∩ u) t * uniformOn s u + uniformOn (s ∩ uᶜ) t * uniformOn s uᶜ = uniformOn s t :=
by
conv_rhs =>
rw [(by simp : s = s ∩ u ∪ s ∩ uᶜ), ←
uniformOn_disjoint_union (hs.inter_of_left _) (hs.inter_of_left _)
(disjoint_compl_right.mono inf_le_right inf_le_right)]
simp [uniformOn_inter_self hs]
