Certifying Statistical Robustness in Coq

Robustness properties are a class of statistical properties that specify that perturbations in the input data should not significantly affect the result of a statistical method. In this presentation, we explore our work in verifying claims robust mean estimators in Coq, from the seminal work of Tukey in the 1960s showing robustness bounds for the trimmed mean algorithm, as well as ongoing work in verifying more recent claims of robustness. In the process, we have contributed new probability lemmas of the coq-infotheo library for information theory, and — in order to better handle the probability theory of more advanced algorithms — we present a new library for probability theory based on Lebesgue Measure theory that is being integrated into MathComp-analysis.