Documentation

Complexity.Probability.PMF.Event

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 and success 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), lower bounds on a first stage and on its continuation from supported members multiply (toOuterMeasure_bind_ge_mul), 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 #

References #

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

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

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

source
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 - ε.

source
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 - ε.

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

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

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

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

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

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

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

source
theorem Cslib.Probability.PMF.toOuterMeasure_bind_ge_mul {α : Type u_1} {β : Type u_2} (p : PMF α) (kernel : α → PMF β) (pre : Set α) (event : Set β) {s₁ s₂ : ℝ} (hs₂ : 0 ≤ s₂) (hp : s₁ ≤ (p.toOuterMeasure pre).toReal) (hstep : ∀ a ∈ p.support, a ∈ pre → s₂ ≤ ((kernel a).toOuterMeasure event).toReal) :
s₁ * s₂ ≤ ((p.bind kernel).toOuterMeasure event).toReal

If a first stage p lands in pre with probability at least s₁ and for every supported a ∈ pre the continuation kernel a lands in event with probability at least s₂, then p.bind kernel lands in event with probability at least s₁ * s₂.

source
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 #

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

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

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

source
theorem Cslib.Probability.PMF.map_true_mono {α : Type u_1} (p : PMF α) {E F : α → Bool} (h : ∀ a ∈ p.support, E a = true → F a = true) :
(PMF.map E p) true ≤ (PMF.map F p) true

Pointwise implication on the support makes the mapped true-mass monotone.

source
theorem Cslib.Probability.PMF.map_true_le_add {α : Type u_1} (p : PMF α) {E A B : α → Bool} (h : ∀ a ∈ p.support, E a = true → A a = true ∨ B a = true) :
(PMF.map E p) true ≤ (PMF.map A p) true + (PMF.map B p) true

Union bound for two Boolean predicates pushed forward along p.map.

source
theorem Cslib.Probability.PMF.map_any_range_true_le_sum {α : Type u_1} (p : PMF α) (K : ℕ) (F : ℕ → α → Bool) :
(PMF.map (fun (a : α) => (List.range K).any fun (j : ℕ) => F j a) p) true ≤ ∑ j ∈ Finset.range K, (PMF.map (F j) p) true

Union bound for List.any over List.range K pushed forward along p.map.

source
theorem Cslib.Probability.PMF.map_not_true {α : Type u_1} (p : PMF α) (E : α → Bool) :
(PMF.map (fun (a : α) => !E a) p) true = 1 - (PMF.map E p) true

Negating a Boolean predicate complements its true-mass in ℝ≥0∞.