Failure of a continuation after a bad first stage

After a random first stage p, a continuation kernel reaches event with probability at most the probability that the first stage is bad plus a bound on reaching event from its supported good outcomes. This is toOuterMeasure_bind_failure_le stated for the bad set instead of its complement; it replaces the recurring split of ∑' a, p a * (kernel a).toOuterMeasure event into bad.indicator 1 a + error.

Main results

• Cslib.Probability.PMF.toOuterMeasure_bind_le_add: the failure bound for a bad first stage.

theorem Cslib.Probability.PMF.toOuterMeasure_bind_le_add {α : Type u_1} {β : Type u_2} (p : PMF α) (kernel : α → PMF β) (bad : Set α) (event : Set β) (error : ENNReal) (hstep : ∀ a ∈ p.support, a ∉ bad → (kernel a).toOuterMeasure event ≤ error) : (p.bind kernel).toOuterMeasure event ≤ p.toOuterMeasure bad + error

A continuation reaches event with probability at most that of a bad first stage plus error, when every supported good first-stage outcome leads to event with probability at most error.