ProbabilityTheory.condCount_add_compl_eq

theorem ProbabilityTheory.condCount_add_compl_eq : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSingletonClass Ω] {s : Set Ω} (u t : Set Ω), s.Finite → ↑↑(ProbabilityTheory.condCount (s ∩ u)) t * ↑↑(ProbabilityTheory.condCount s) u + ↑↑(ProbabilityTheory.condCount (s ∩ uᶜ)) t * ↑↑(ProbabilityTheory.condCount s) uᶜ = ↑↑(ProbabilityTheory.condCount s) t

This theorem is a version of the law of total probability tailored for counting probabilities. For any measurable space `Ω`, given a set `s` in `Ω` that is finite, and two other sets `u` and `t` in `Ω`, the total conditional count of `t` given `s` is equal to the sum of the conditional counts of `t` given `s` intersected with `u` and `s` intersected with the complement of `u`, each multiplied by the conditional count of `u` and the complement of `u` given `s`, respectively. In mathematical terms, we have `condCount(s) t = condCount(s ∩ u) t * condCount(s) u + condCount(s ∩ uᶜ) t * condCount(s) uᶜ`.

More concisely: The total conditional count of `t` given `s` in a measurable space is equal to the sum of the conditional counts of `t` given `s` intersected with `u` and `s` intersected with the complement of `u`, each multiplied by the respective conditional counts of `u` and its complement given `s`. In symbols: `condCount(s) t = condCount(s ∩ u) t * condCount(s) u + condCount(s ∩ uᶜ) t * condCount(s) uᶜ`.