Event probabilities after a random first stage

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_ennreal, toOuterMeasure_bind_ge_mul), and failure bounds multiply when success is retained (toOuterMeasure_bind_le_mul_ennreal). Average bias turns into the probability of good first stages (toOuterMeasure_rate_ge).

Main results

• Cslib.Probability.PMF.toOuterMeasure_bind_toReal: averaging over a first stage.
• Cslib.Probability.PMF.toOuterMeasure_bind_le, Cslib.Probability.PMF.toOuterMeasure_bind_failure_le, Cslib.Probability.PMF.toOuterMeasure_bind_failure_toReal_le, Cslib.Probability.PMF.toOuterMeasure_bind_ge_mul, Cslib.Probability.PMF.toOuterMeasure_bind_ge_mul_ennreal, Cslib.Probability.PMF.toOuterMeasure_bind_le_mul_ennreal: composing failure and success bounds.
• Cslib.Probability.PMF.toOuterMeasure_rate_ge: average bias as the probability of good inputs.

References

toOuterMeasure_bind_toReal, toOuterMeasure_bind_failure_le and toOuterMeasure_bind_failure_toReal_le are adapted from Probability/PMF.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8. The ENNReal event-composition lemmas were extracted from Renfei Zhou's Karger algorithm development.

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_le {α : Type u_1} {β : Type u_2} (p : PMF α) (kernel : α → PMF β) (event : Set β) {error : ENNReal} (h : ∀ (a : α), (kernel a).toOuterMeasure event ≤ error) : (p.bind kernel).toOuterMeasure event ≤ error

A uniform upper bound on (kernel a).toOuterMeasure event bounds (p.bind kernel).toOuterMeasure event.

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_bind_ge_mul_ennreal {α : Type u_3} {β : Type u_4} (p : PMF α) (kernel : α → PMF β) (pre : Set α) (event : Set β) {s₁ s₂ : ENNReal} (hp : s₁ ≤ p.toOuterMeasure pre) (hstep : ∀ a ∈ p.support, a ∈ pre → s₂ ≤ (kernel a).toOuterMeasure event) : s₁ * s₂ ≤ (p.bind kernel).toOuterMeasure event

ENNReal multiplication rule for sequential success lower bounds across PMF.bind.

theorem Cslib.Probability.PMF.toOuterMeasure_bind_le_mul_ennreal {α : Type u_3} {β : Type u_4} (p : PMF α) (kernel : α → PMF β) (stillFailing : Set α) (failure : Set β) {q₁ q₂ : ENNReal} (hp : p.toOuterMeasure stillFailing ≤ q₁) (hfail : ∀ a ∈ p.support, a ∈ stillFailing → (kernel a).toOuterMeasure failure ≤ q₂) (hsucc : ∀ a ∈ p.support, a ∉ stillFailing → (kernel a).toOuterMeasure failure = 0) : (p.bind kernel).toOuterMeasure failure ≤ q₁ * q₂

ENNReal multiplication rule for sequential failure upper bounds: if p stays in stillFailing with probability at most q₁, every supported a ∈ stillFailing fails under kernel a with probability at most q₂, and every supported a ∉ stillFailing has zero failure probability under kernel a, then p.bind kernel fails with probability at most q₁ * q₂.

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

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.