Estimating acceptance probabilities by repeated trials

The success counter is an ordinary probabilistic program. Its independent product law gives Hoeffding bounds for the count and for its empirical acceptance probability. Division and real numbers occur only in the specification: the program returns a natural number.

Cslib.Computability.Probabilistic.Repeat supplies the separate strict PPT certificate whenever the trial program and its unary repetition count are efficient.

Main results

• Cslib.ProbComp.countTrue_average_deviation_pow: exponentially accurate empirical rates with a polynomial trial budget in the confidence and inverse tolerance.
• Cslib.ProbComp.testProbabilityLT_error_pow_of_bounds: rational threshold tests satisfy overlapping postconditions except with exponentially small probability.
• Cslib.ProbComp.replicate_failure_pow: repeated sampling finds a good value with high probability; its proof predicate need not be computable.

References

Adapted from Languages/Probabilistic/Concentration.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8. The concentration estimate is the finite-product bound from Probability.Concentration, following Hoeffding.

theorem Cslib.ProbComp.countTrue_deviation (count : ℕ) (program : ProbComp Bool) {ε : ℝ} (hε : 0 ≤ ε) : ((eval (OracleComp.countTrue count program)).toOuterMeasure {successes : ℕ | ε ≤ |↑successes - ↑count * (program.eval true).toReal|}).toReal ≤ 2 * Real.exp (-2 * ε ^ 2 / ↑count)

A repeated success count deviates from its mean with exponentially small probability. This unnormalized bound also holds at count zero.

theorem Cslib.ProbComp.countTrue_average_deviation (count : ℕ) (hcount : 0 < count) (program : ProbComp Bool) {ε : ℝ} (hε : 0 ≤ ε) : ((eval (OracleComp.countTrue count program)).toOuterMeasure {successes : ℕ | ε ≤ |↑successes / ↑count - (program.eval true).toReal|}).toReal ≤ 2 * Real.exp (-2 * ↑count * ε ^ 2)

The empirical acceptance probability estimates the true probability to additive tolerance ε, with failure at most 2 exp (-2 * count * ε²). The count must be positive.

theorem Cslib.ProbComp.countTrue_average_deviation_pow (confidence inverseTolerance : ℕ) (htolerance : 0 < inverseTolerance) (program : ProbComp Bool) : ((eval (OracleComp.countTrue ((confidence + 1) * inverseTolerance ^ 2) program)).toOuterMeasure {successes : ℕ | 1 / ↑inverseTolerance ≤ |↑successes / ↑((confidence + 1) * inverseTolerance ^ 2) - (program.eval true).toReal|}).toReal ≤ (1 / 2) ^ confidence

A polynomial trial budget gives inverse-polynomial accuracy and exponentially small failure. Both parameters are natural numbers, so a client can compute the budget with unary arithmetic.

theorem Cslib.ProbComp.replicate_failure_pow {α : Type} (source : ProbComp α) (good : α → Prop) (confidence inverseSuccess : ℕ) (hinverse : 0 < inverseSuccess) (hsuccess : 1 / ↑inverseSuccess ≤ (source.eval.toOuterMeasure {value : α | good value}).toReal) : ((eval (OracleComp.replicate ((confidence + 1) * inverseSuccess ^ 2) source)).toOuterMeasure {values : List α | ¬∃ value ∈ values, good value}).toReal ≤ (1 / 2) ^ confidence

Polynomially many independent draws find a good value except with exponentially small probability whenever one draw succeeds with inverse-polynomial probability. The predicate is used only in the proof and need not be efficiently decidable.

theorem Cslib.ProbComp.testProbabilityLT_error (count numerator denominator : ℕ) (hcount : 0 < count) (hdenominator : 0 < denominator) (program : ProbComp Bool) {ε : ℝ} (hε : 0 ≤ ε) : ((eval (OracleComp.testProbabilityLT count numerator denominator program)).toOuterMeasure {below : Bool | ¬if below = true then (program.eval true).toReal ≤ ↑numerator / ↑denominator + ε else ↑numerator / ↑denominator - ε ≤ (program.eval true).toReal}).toReal ≤ 2 * Real.exp (-2 * ↑count * ε ^ 2)

Except with the Hoeffding error, a true test result implies the probability is at most the threshold plus tolerance; a false result implies it is at least the threshold minus tolerance.

theorem Cslib.ProbComp.testProbabilityLT_error_pow (confidence inverseTolerance numerator denominator : ℕ) (htolerance : 0 < inverseTolerance) (hdenominator : 0 < denominator) (program : ProbComp Bool) : ((eval (OracleComp.testProbabilityLT ((confidence + 1) * inverseTolerance ^ 2) numerator denominator program)).toOuterMeasure {below : Bool | ¬if below = true then (program.eval true).toReal ≤ ↑numerator / ↑denominator + 1 / ↑inverseTolerance else ↑numerator / ↑denominator - 1 / ↑inverseTolerance ≤ (program.eval true).toReal}).toReal ≤ (1 / 2) ^ confidence

The rational threshold test has a polynomial trial budget and exponentially small error.

theorem Cslib.ProbComp.testProbabilityLT_error_pow_of_bounds (confidence inverseTolerance numerator denominator : ℕ) (htolerance : 0 < inverseTolerance) (hdenominator : 0 < denominator) (program : ProbComp Bool) {lower upper : ℝ} (hlower : lower ≤ ↑numerator / ↑denominator - 1 / ↑inverseTolerance) (hupper : ↑numerator / ↑denominator + 1 / ↑inverseTolerance ≤ upper) : ((eval (OracleComp.testProbabilityLT ((confidence + 1) * inverseTolerance ^ 2) numerator denominator program)).toOuterMeasure {below : Bool | ¬if below = true then (program.eval true).toReal ≤ upper else lower ≤ (program.eval true).toReal}).toReal ≤ (1 / 2) ^ confidence

A threshold test may target wider, overlapping postconditions. This form lets clients use the bounds required by an algorithm without carrying its sampling tolerance further.