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_toReal_add_compl). Conditioning keeps the event's masses and divides them by its probability (filter_apply_toReal).

After a random first stage, an event's probability is the average of its conditional probabilities (toOuterMeasure_bind_toReal). Failure bounds compose without independence: a randomized continuation fails because its precondition already failed or because it fails from a valid input (toOuterMeasure_bind_failure_le), and average bias turns into the probability of good first stages (toOuterMeasure_rate_ge). The real-valued masses of true and false under a Boolean distribution sum to one (toReal_true_add_toReal_false).

Main results

• Cslib.Probability.PMF.toOuterMeasure_ne_top, Cslib.Probability.PMF.toOuterMeasure_le_one: events have probability at most one.
• Cslib.Probability.PMF.toOuterMeasure_apply_toReal, Cslib.Probability.PMF.toOuterMeasure_toReal_add_compl, Cslib.Probability.PMF.toOuterMeasure_toReal_pos_iff: real-valued event probabilities.
• Cslib.Probability.PMF.filter_apply_toReal: conditioned masses.
• Cslib.Probability.PMF.toOuterMeasure_bind_toReal: averaging over a first stage.
• Cslib.Probability.PMF.toOuterMeasure_bind_failure_le, Cslib.Probability.PMF.toOuterMeasure_bind_failure_toReal_le: composing failure bounds.
• Cslib.Probability.PMF.toOuterMeasure_rate_ge: average bias as the probability of good inputs.
• Cslib.Probability.PMF.toReal_true_add_toReal_false, Cslib.Probability.PMF.toReal_false_eq_one_sub, Cslib.Probability.PMF.toReal_true_eq_one_sub: Boolean outcome masses.

References

Adapted in part from Probability/PMF.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

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_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_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.

theorem Cslib.Probability.PMF.toOuterMeasure_bind_toReal {α : Type u_1} {β : Type u_2} [Fintype α] (p : PMF α) (kernel : α → PMF β) (event : Set β) : ((p.bind kernel).toOuterMeasure event).toReal = ∑ a : α, (p a).toReal * ((kernel a).toOuterMeasure event).toReal

Event probability after a finite random choice is the average conditional probability.

theorem Cslib.Probability.PMF.toOuterMeasure_bind_failure_le {α : Type u_1} {β : Type u_2} (p : PMF α) (kernel : α → PMF β) (pre : Set α) (failure : Set β) (error : ENNReal) (hstep : ∀ a ∈ p.support, a ∈ pre → (kernel a).toOuterMeasure failure ≤ error) : (p.bind kernel).toOuterMeasure failure ≤ p.toOuterMeasure preᶜ + error

A randomized continuation can fail because its precondition was already false or because it fails from a valid input. No independence or finite-state assumption is needed.

theorem Cslib.Probability.PMF.toOuterMeasure_bind_failure_toReal_le {α : Type u_1} {β : Type u_2} (p : PMF α) (kernel : α → PMF β) (pre : Set α) (failure : Set β) {error : ℝ} (herror : 0 ≤ error) (hstep : ∀ a ∈ p.support, a ∈ pre → ((kernel a).toOuterMeasure failure).toReal ≤ error) : ((p.bind kernel).toOuterMeasure failure).toReal ≤ (p.toOuterMeasure preᶜ).toReal + error

The real-valued error rule for a randomized continuation.

theorem Cslib.Probability.PMF.toOuterMeasure_rate_ge {α : Type u_1} {β : Type u_2} (p : PMF α) (kernel : α → PMF β) (event : Set β) {threshold : ℝ} (hthreshold : 0 ≤ threshold) : ((p.bind kernel).toOuterMeasure event).toReal - threshold ≤ (p.toOuterMeasure {a : α | threshold ≤ ((kernel a).toOuterMeasure event).toReal}).toReal

If a randomized test beats a threshold on average, at least its excess probability mass consists of inputs whose conditional acceptance probability reaches that threshold.

Boolean distributions

theorem Cslib.Probability.PMF.toReal_true_add_toReal_false (p : PMF Bool) : (p true).toReal + (p false).toReal = 1

The real-valued probabilities of true and false under a Boolean distribution sum to one.

theorem Cslib.Probability.PMF.toReal_false_eq_one_sub (p : PMF Bool) : (p false).toReal = 1 - (p true).toReal

The real-valued probability of false under a Boolean distribution is one minus the probability of true.

theorem Cslib.Probability.PMF.toReal_true_eq_one_sub (p : PMF Bool) : (p true).toReal = 1 - (p false).toReal

The real-valued probability of true under a Boolean distribution is one minus the probability of false.