mathlib3 documentation

probability.cond_count

Classical probability #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The classical formulation of probability states that the probability of an event occurring in a finite probability space 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 #

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.

source
noncomputable def probability_theory.cond_count {Ω : Type u_1} [measurable_space Ω] (s : set Ω) :
measure_theory.measure Ω

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
source
@[simp]
theorem probability_theory.cond_count_empty_meas {Ω : Type u_1} [measurable_space Ω] :
probability_theory.cond_count ∅ = 0
source
theorem probability_theory.cond_count_empty {Ω : Type u_1} [measurable_space Ω] {s : set Ω} :
⇑(probability_theory.cond_count s) ∅ = 0
source
theorem probability_theory.finite_of_cond_count_ne_zero {Ω : Type u_1} [measurable_space Ω] {s t : set Ω} (h : ⇑(probability_theory.cond_count s) t ≠ 0) :
s.finite
source
theorem probability_theory.cond_count_univ {Ω : Type u_1} [measurable_space Ω] [fintype Ω] {s : set Ω} :
⇑(probability_theory.cond_count set.univ) s = ⇑measure_theory.measure.count s / ↑(fintype.card Ω)
source
theorem probability_theory.cond_count_is_probability_measure {Ω : Type u_1} [measurable_space Ω] [measurable_singleton_class Ω] {s : set Ω} (hs : s.finite) (hs' : s.nonempty) :
measure_theory.is_probability_measure (probability_theory.cond_count s)
source
theorem probability_theory.cond_count_singleton {Ω : Type u_1} [measurable_space Ω] [measurable_singleton_class Ω] (ω : Ω) (t : set Ω) [decidable (ω ∈ t)] :
⇑(probability_theory.cond_count {ω}) t = ite (ω ∈ t) 1 0
source
theorem probability_theory.cond_count_inter_self {Ω : Type u_1} [measurable_space Ω] [measurable_singleton_class Ω] {s t : set Ω} (hs : s.finite) :
⇑(probability_theory.cond_count s) (s ∩ t) = ⇑(probability_theory.cond_count s) t
source
theorem probability_theory.cond_count_self {Ω : Type u_1} [measurable_space Ω] [measurable_singleton_class Ω] {s : set Ω} (hs : s.finite) (hs' : s.nonempty) :
⇑(probability_theory.cond_count s) s = 1
source
theorem probability_theory.cond_count_eq_one_of {Ω : Type u_1} [measurable_space Ω] [measurable_singleton_class Ω] {s t : set Ω} (hs : s.finite) (hs' : s.nonempty) (ht : s ⊆ t) :
⇑(probability_theory.cond_count s) t = 1
source
theorem probability_theory.pred_true_of_cond_count_eq_one {Ω : Type u_1} [measurable_space Ω] [measurable_singleton_class Ω] {s t : set Ω} (h : ⇑(probability_theory.cond_count s) t = 1) :
s ⊆ t
source
theorem probability_theory.cond_count_eq_zero_iff {Ω : Type u_1} [measurable_space Ω] [measurable_singleton_class Ω] {s t : set Ω} (hs : s.finite) :
⇑(probability_theory.cond_count s) t = 0 ↔ s ∩ t = ∅
source
theorem probability_theory.cond_count_of_univ {Ω : Type u_1} [measurable_space Ω] [measurable_singleton_class Ω] {s : set Ω} (hs : s.finite) (hs' : s.nonempty) :
⇑(probability_theory.cond_count s) set.univ = 1
source
theorem probability_theory.cond_count_inter {Ω : Type u_1} [measurable_space Ω] [measurable_singleton_class Ω] {s t u : set Ω} (hs : s.finite) :
⇑(probability_theory.cond_count s) (t ∩ u) = ⇑(probability_theory.cond_count (s ∩ t)) u * ⇑(probability_theory.cond_count s) t
source
theorem probability_theory.cond_count_inter' {Ω : Type u_1} [measurable_space Ω] [measurable_singleton_class Ω] {s t u : set Ω} (hs : s.finite) :
⇑(probability_theory.cond_count s) (t ∩ u) = ⇑(probability_theory.cond_count (s ∩ u)) t * ⇑(probability_theory.cond_count s) u
source
theorem probability_theory.cond_count_union {Ω : Type u_1} [measurable_space Ω] [measurable_singleton_class Ω] {s t u : set Ω} (hs : s.finite) (htu : disjoint t u) :
⇑(probability_theory.cond_count s) (t ∪ u) = ⇑(probability_theory.cond_count s) t + ⇑(probability_theory.cond_count s) u
source
theorem probability_theory.cond_count_compl {Ω : Type u_1} [measurable_space Ω] [measurable_singleton_class Ω] {s : set Ω} (t : set Ω) (hs : s.finite) (hs' : s.nonempty) :
⇑(probability_theory.cond_count s) t + ⇑(probability_theory.cond_count s) tᶜ = 1
source
theorem probability_theory.cond_count_disjoint_union {Ω : Type u_1} [measurable_space Ω] [measurable_singleton_class Ω] {s t u : set Ω} (hs : s.finite) (ht : t.finite) (hst : disjoint s t) :
⇑(probability_theory.cond_count s) u * ⇑(probability_theory.cond_count (s ∪ t)) s + ⇑(probability_theory.cond_count t) u * ⇑(probability_theory.cond_count (s ∪ t)) t = ⇑(probability_theory.cond_count (s ∪ t)) u
source
theorem probability_theory.cond_count_add_compl_eq {Ω : Type u_1} [measurable_space Ω] [measurable_singleton_class Ω] {s : set Ω} (u t : set Ω) (hs : s.finite) :
⇑(probability_theory.cond_count (s ∩ u)) t * ⇑(probability_theory.cond_count s) u + ⇑(probability_theory.cond_count (s ∩ uᶜ)) t * ⇑(probability_theory.cond_count s) uᶜ = ⇑(probability_theory.cond_count s) t

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