Elementary finite probability

This file avoids measure-theory overhead for the upper-bound proof. All random objects used there are uniform on finite types, so probability and expectation are just normalized finite sums.

noncomputable def PebblingLean.FiniteProbability.uniformProbability {Ω : Type u_1} [Fintype Ω] (P : Ω → Prop) [DecidablePred P] : ℚ

Uniform probability of an event on a finite sample space, as a rational number.

Equations

• PebblingLean.FiniteProbability.uniformProbability P = ↑(Finset.filter P Finset.univ).card / ↑(Fintype.card Ω)

noncomputable def PebblingLean.FiniteProbability.uniformExpectation {Ω : Type u_1} [Fintype Ω] (X : Ω → ℕ) : ℚ

Uniform expectation of a natural-valued random variable on a finite sample space, as a rational number.

Equations

• PebblingLean.FiniteProbability.uniformExpectation X = (∑ ω : Ω, ↑(X ω)) / ↑(Fintype.card Ω)

theorem PebblingLean.FiniteProbability.exists_not_of_uniformProbability_lt_one {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {P : Ω → Prop} [DecidablePred P] (hprob : uniformProbability P < 1) : ∃ (ω : Ω), ¬P ω

theorem PebblingLean.FiniteProbability.uniformProbability_exists_le_sum {Ω : Type u_1} {ι : Type u_2} [Fintype Ω] [Nonempty Ω] [Fintype ι] (P : ι → Ω → Prop) [(i : ι) → DecidablePred (P i)] [DecidablePred fun (ω : Ω) => ∃ (i : ι), P i ω] : (uniformProbability fun (ω : Ω) => ∃ (i : ι), P i ω) ≤ ∑ i : ι, uniformProbability (P i)

Union bound for finite uniform probabilities.