Classical probability

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 occurring in s to be |s|⁻¹ * |s ∩ t|. With this definition, we recover 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

• ProbabilityTheory.condCount: given a set s, condCount 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 condCount s P. We should avoid this however as none of the lemmas are written for predicates.

def ProbabilityTheory.condCount {Ω : Type u_1} [MeasurableSpace Ω] (s : Set Ω) : MeasureTheory.Measure Ω

Given a set s, condCount s is the counting measure conditioned on s. In particular, condCount 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 ProbabilityTheory.condCount_isProbabilityMeasure.

Equations

• ProbabilityTheory.condCount s = ProbabilityTheory.cond MeasureTheory.Measure.count s

@[simp]

theorem ProbabilityTheory.condCount_empty_meas {Ω : Type u_1} [MeasurableSpace Ω] : ProbabilityTheory.condCount ∅ = 0

theorem ProbabilityTheory.condCount_empty {Ω : Type u_1} [MeasurableSpace Ω] {s : Set Ω} : ↑↑(ProbabilityTheory.condCount s) ∅ = 0

theorem ProbabilityTheory.finite_of_condCount_ne_zero {Ω : Type u_1} [MeasurableSpace Ω] {s : Set Ω} {t : Set Ω} (h : ↑↑(ProbabilityTheory.condCount s) t ≠ 0) : Set.Finite s

theorem ProbabilityTheory.condCount_univ {Ω : Type u_1} [MeasurableSpace Ω] [Fintype Ω] {s : Set Ω} : ↑↑(ProbabilityTheory.condCount Set.univ) s = ↑↑MeasureTheory.Measure.count s / ↑(Fintype.card Ω)

theorem ProbabilityTheory.condCount_isProbabilityMeasure {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (hs : Set.Finite s) (hs' : Set.Nonempty s) : MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.condCount s)

theorem ProbabilityTheory.condCount_singleton {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (ω : Ω) (t : Set Ω) [Decidable (ω ∈ t)] : ↑↑(ProbabilityTheory.condCount {ω}) t = if ω ∈ t then 1 else 0

theorem ProbabilityTheory.condCount_inter_self {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} {t : Set Ω} (hs : Set.Finite s) : ↑↑(ProbabilityTheory.condCount s) (s ∩ t) = ↑↑(ProbabilityTheory.condCount s) t

theorem ProbabilityTheory.condCount_self {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (hs : Set.Finite s) (hs' : Set.Nonempty s) : ↑↑(ProbabilityTheory.condCount s) s = 1

theorem ProbabilityTheory.condCount_eq_one_of {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} {t : Set Ω} (hs : Set.Finite s) (hs' : Set.Nonempty s) (ht : s ⊆ t) : ↑↑(ProbabilityTheory.condCount s) t = 1

theorem ProbabilityTheory.pred_true_of_condCount_eq_one {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} {t : Set Ω} (h : ↑↑(ProbabilityTheory.condCount s) t = 1) : s ⊆ t

theorem ProbabilityTheory.condCount_eq_zero_iff {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} {t : Set Ω} (hs : Set.Finite s) : ↑↑(ProbabilityTheory.condCount s) t = 0 ↔ s ∩ t = ∅

theorem ProbabilityTheory.condCount_of_univ {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (hs : Set.Finite s) (hs' : Set.Nonempty s) : ↑↑(ProbabilityTheory.condCount s) Set.univ = 1

theorem ProbabilityTheory.condCount_inter {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} {t : Set Ω} {u : Set Ω} (hs : Set.Finite s) : ↑↑(ProbabilityTheory.condCount s) (t ∩ u) = ↑↑(ProbabilityTheory.condCount (s ∩ t)) u * ↑↑(ProbabilityTheory.condCount s) t

theorem ProbabilityTheory.condCount_inter' {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} {t : Set Ω} {u : Set Ω} (hs : Set.Finite s) : ↑↑(ProbabilityTheory.condCount s) (t ∩ u) = ↑↑(ProbabilityTheory.condCount (s ∩ u)) t * ↑↑(ProbabilityTheory.condCount s) u

theorem ProbabilityTheory.condCount_union {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} {t : Set Ω} {u : Set Ω} (hs : Set.Finite s) (htu : Disjoint t u) : ↑↑(ProbabilityTheory.condCount s) (t ∪ u) = ↑↑(ProbabilityTheory.condCount s) t + ↑↑(ProbabilityTheory.condCount s) u

theorem ProbabilityTheory.condCount_compl {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (t : Set Ω) (hs : Set.Finite s) (hs' : Set.Nonempty s) : ↑↑(ProbabilityTheory.condCount s) t + ↑↑(ProbabilityTheory.condCount s) tᶜ = 1

theorem ProbabilityTheory.condCount_disjoint_union {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} {t : Set Ω} {u : Set Ω} (hs : Set.Finite s) (ht : Set.Finite t) (hst : Disjoint s t) : ↑↑(ProbabilityTheory.condCount s) u * ↑↑(ProbabilityTheory.condCount (s ∪ t)) s + ↑↑(ProbabilityTheory.condCount t) u * ↑↑(ProbabilityTheory.condCount (s ∪ t)) t = ↑↑(ProbabilityTheory.condCount (s ∪ t)) u

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

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