Event probabilities of discrete distributions

The probability p.toOuterMeasure s of an event under a discrete distribution is finite and at most one (toOuterMeasure_ne_top, toOuterMeasure_le_one); on a finite type its real value is the sum of the masses of the event's members (toOuterMeasure_apply_toReal), and an event and its complement have total probability one (toOuterMeasure_add_compl_ennreal, toOuterMeasure_toReal_add_compl). Conditioning keeps the event's masses and divides them by its probability (filter_apply_toReal).

Event probabilities after a random first stage are in CslibFrontier.Probability.PMF.EventBind, and the outcome masses of Boolean distributions and Boolean predicates are in CslibFrontier.Probability.PMF.Bool.

Main results

• Cslib.Probability.PMF.toOuterMeasure_ne_top, Cslib.Probability.PMF.toOuterMeasure_le_one: events have probability at most one.
• Cslib.Probability.PMF.toOuterMeasure_eq_tsum_mul_indicator: an event's probability is the expectation of its indicator.
• Cslib.Probability.PMF.toOuterMeasure_abs_sub_ge_le, Cslib.Probability.PMF.toOuterMeasure_abs_sub_ge_toReal_le: two-sided tail bounds from upper and lower tails.
• Cslib.Probability.PMF.toOuterMeasure_apply_toReal, Cslib.Probability.PMF.toOuterMeasure_toReal_eq_sum_ite, Cslib.Probability.PMF.toOuterMeasure_toReal_add_compl, Cslib.Probability.PMF.toOuterMeasure_toReal_pos_iff: real-valued event probabilities.
• Cslib.Probability.PMF.toOuterMeasure_add_compl_ennreal, Cslib.Probability.PMF.toOuterMeasure_compl_le_one_sub: complementation and failure bounds.
• Cslib.Probability.PMF.filter_apply_toReal: conditioned masses.

References

Adapted in part from Probability/PMF.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8. The ENNReal complement lemmas were extracted from Renfei Zhou's Karger algorithm development.

theorem Cslib.Probability.PMF.toOuterMeasure_ne_top {α : Type u_1} (p : PMF α) (event : Set α) : p.toOuterMeasure event ≠ ⊤

Every event has finite probability, including on an infinite ambient type. Adapted from the cslib crypto branch at 5ff69ca.

theorem Cslib.Probability.PMF.toOuterMeasure_le_one {α : Type u_1} (p : PMF α) (event : Set α) : p.toOuterMeasure event ≤ 1

An event has probability at most one.

theorem Cslib.Probability.PMF.toOuterMeasure_eq_tsum_mul_indicator {α : Type u_1} (p : PMF α) (event : Set α) : p.toOuterMeasure event = ∑' (a : α), p a * event.indicator 1 a

The probability of an event is the expectation of its indicator.

theorem Cslib.Probability.PMF.toOuterMeasure_abs_sub_ge_le {α : Type u_1} (p : PMF α) (f : α → ℝ) (m ε : ℝ) : p.toOuterMeasure {a : α | ε ≤ |f a - m|} ≤ p.toOuterMeasure {a : α | m + ε ≤ f a} + p.toOuterMeasure {a : α | f a ≤ m - ε}

The event that f a deviates from m by at least ε is covered by the upper tail m + ε ≤ f a and the lower tail f a ≤ m - ε.

theorem Cslib.Probability.PMF.toOuterMeasure_abs_sub_ge_toReal_le {α : Type u_1} (p : PMF α) (f : α → ℝ) (m ε : ℝ) : (p.toOuterMeasure {a : α | ε ≤ |f a - m|}).toReal ≤ (p.toOuterMeasure {a : α | m + ε ≤ f a}).toReal + (p.toOuterMeasure {a : α | f a ≤ m - ε}).toReal

In real-valued probabilities, the two-sided tail ε ≤ |f a - m| is bounded by the sum of the upper tail m + ε ≤ f a and the lower tail f a ≤ m - ε.

theorem Cslib.Probability.PMF.toOuterMeasure_apply_toReal {α : Type u_1} [Fintype α] (p : PMF α) (event : Set α) : (p.toOuterMeasure event).toReal = ∑ a : α, if a ∈ event then (p a).toReal else 0

Event probabilities on finite spaces are sums of the masses of their members.

theorem Cslib.Probability.PMF.toOuterMeasure_toReal_eq_sum_ite {α : Type u_1} [Fintype α] (p : PMF α) (event : Set α) [DecidablePred fun (x : α) => x ∈ event] : (p.toOuterMeasure event).toReal = ∑ a : α, (p a).toReal * if a ∈ event then 1 else 0

The probability of an event in a finite space, as the mean of its indicator.

theorem Cslib.Probability.PMF.toOuterMeasure_add_compl_ennreal {α : Type u_2} (p : PMF α) (s : Set α) : p.toOuterMeasure s + p.toOuterMeasure sᶜ = 1

Exact complementation law p.toOuterMeasure s + p.toOuterMeasure sᶜ = 1 for discrete PMFs, valid on arbitrary types without measurability hypotheses.

theorem Cslib.Probability.PMF.toOuterMeasure_compl_le_one_sub {α : Type u_2} (p : PMF α) (s : Set α) {q : ENNReal} (hq : q ≤ p.toOuterMeasure s) : p.toOuterMeasure sᶜ ≤ 1 - q

A lower bound on success gives the complementary upper bound on failure.

theorem Cslib.Probability.PMF.toOuterMeasure_toReal_add_compl {α : Type u_1} (p : PMF α) (event : Set α) : (p.toOuterMeasure event).toReal + (p.toOuterMeasure eventᶜ).toReal = 1

An event and its complement have total probability one, in real-valued probability units.

theorem Cslib.Probability.PMF.toOuterMeasure_toReal_pos_iff {α : Type u_1} (p : PMF α) (event : Set α) : 0 < (p.toOuterMeasure event).toReal ↔ ∃ a ∈ event, a ∈ p.support

An event has positive real probability exactly when it contains a possible outcome.

theorem Cslib.Probability.PMF.filter_apply_toReal {α : Type u_1} (p : PMF α) (event : Set α) (hevent : ∃ a ∈ event, a ∈ p.support) (a : α) : ((p.filter event hevent) a).toReal = if a ∈ event then (p a).toReal / (p.toOuterMeasure event).toReal else 0

Conditioning keeps the event's masses and divides them by its probability.