Majority prediction and its training test

The predictor uses only the observable vote list. Its nonpositive-margin training test also receives the true label, and bounds prediction error including ties and the empty list. The probability laws apply to arbitrary discrete sources, including infinite ambient types.

Main results

• Cslib.BitString.listStrictMajority_error_le: margin-test failure bounds prediction error.
• Cslib.BitString.map_listNonpositiveMargin_true: the exact law of the executable test.

References

Holenstein, Claim 2.16. Adapted from Crypto/Computational/Pseudoentropy/Boosting/Vote.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Cslib.BitString.listStrictMajority_error_le {α : Type u_1} (source : PMF α) (votes : α → List Bool) (truth : α → Bool) : (source.toOuterMeasure {x : α | listStrictMajority (votes x) ≠ truth x}).toReal ≤ (source.toOuterMeasure {x : α | listVoteMargin (votes x) (truth x) ≤ 0}).toReal

The nonpositive-margin event bounds the majority predictor's error on any source.

theorem Cslib.BitString.map_listNonpositiveMargin_true {α : Type u_1} (source : PMF α) (votes : α → List Bool) (truth : α → Bool) : (PMF.map (fun (x : α) => listNonpositiveMargin (votes x) (truth x)) source) true = source.toOuterMeasure {x : α | listVoteMargin (votes x) (truth x) ≤ 0}

Sampling the training test accepts with exactly the nonpositive-margin probability.