# mathlibdocumentation

probability.cond_count

# Classical probability #

The classical formulation of probability states that the probability of an event occurring is the ratio of that event to all possible events. This notion can be expressed with measure theory using the counting measure. In particular, given the sets s and t, we define the probability of t occuring in s to be |s|⁻¹ * |s ∩ t|. With this definition, we recover the the probability over the entire sample space when s = set.univ.

Classical probability is often used in combinatorics and we prove some useful lemmas in this file for that purpose.

## main definition #

• probability_theory.cond_count: given a set s, cond_count s is the counting measure conditioned on s. This is a probability measure when s is finite and nonempty.

## notes #

The original aim of this file is to provide a measure theoretic method of describing the probability an element of a set s satisfies some predicate P. Our current formulation still allow us to describe this by abusing the definitional equality of sets and predicates by simply writing cond_count s P. We should avoid this however as none of the lemmas are written for predicates.

noncomputable def probability_theory.cond_count {α : Type u_1} (s : set α) :

Given a set s, cond_count s is the counting measure conditioned on s. In particular, cond_count s t is the proportion of s that is contained in t.

This is a probability measure when s is finite and nonempty and is given by probability_theory.cond_count_is_probability_measure.

Equations
@[simp]
theorem probability_theory.cond_count_empty_meas {α : Type u_1}  :
theorem probability_theory.cond_count_empty {α : Type u_1} {s : set α} :
theorem probability_theory.finite_of_cond_count_ne_zero {α : Type u_1} {s t : set α} (h : 0) :
theorem probability_theory.cond_count_is_probability_measure {α : Type u_1} {s : set α} (hs : s.finite) (hs' : s.nonempty) :
theorem probability_theory.cond_count_singleton {α : Type u_1} (a : α) (t : set α) [decidable (a t)] :
= ite (a t) 1 0
theorem probability_theory.cond_count_inter_self {α : Type u_1} {s t : set α} (hs : s.finite) :
(s t) =
theorem probability_theory.cond_count_self {α : Type u_1} {s : set α} (hs : s.finite) (hs' : s.nonempty) :
theorem probability_theory.cond_count_eq_one_of {α : Type u_1} {s t : set α} (hs : s.finite) (hs' : s.nonempty) (ht : s t) :
theorem probability_theory.pred_true_of_cond_count_eq_one {α : Type u_1} {s t : set α} (h : = 1) :
s t
theorem probability_theory.cond_count_eq_zero_iff {α : Type u_1} {s t : set α} (hs : s.finite) :
s t =
theorem probability_theory.cond_count_univ {α : Type u_1} {s : set α} (hs : s.finite) (hs' : s.nonempty) :
theorem probability_theory.cond_count_inter {α : Type u_1} {s t u : set α} (hs : s.finite) :
theorem probability_theory.cond_count_inter' {α : Type u_1} {s t u : set α} (hs : s.finite) :
theorem probability_theory.cond_count_union {α : Type u_1} {s t u : set α} (hs : s.finite) (htu : u) :
(t u) =
theorem probability_theory.cond_count_compl {α : Type u_1} {s : set α} (t : set α) (hs : s.finite) (hs' : s.nonempty) :
theorem probability_theory.cond_count_add_compl_eq {α : Type u_1} {s : set α} (u t : set α) (hs : s.finite) :

A version of the law of total probability for counting probabilites.