Document Open Access Logo

Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation

Authors Reynald Affeldt , Alessandro Bruni , Cyril Cohen , Pierre Roux , Takafumi Saikawa

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2025.21.pdf
  • Filesize: 0.99 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
  • Mathematics of computing → Probability and statistics
Keywords
  • Rocq prover
  • Mathematical Components library
  • abstraction interpretation
  • probability theory
  • concentration inequalities

Metrics

Abstract

Concentration inequalities are standard lemmas providing upper bounds on deviations of random variables. To formalize concentration inequalities, we have been developing a general library of lemmas for probability theory in the Rocq prover. This effort led us to revisit already established technical aspects of the Mathematical Components libraries. In this paper, we report on improvements of general interest resulting from our formalization. We devise types for numeric values and a lightweight semi-decision procedure, based on interval arithmetic. We also extend the hierarchy of available mathematical structures to formalize Lebesgue spaces. We illustrate our new formalization of probability theory with the complete proof of a concentration inequality for Bernoulli sampling.

Cite As Get BibTex

Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, and Takafumi Saikawa. Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.21

Author Details

Reynald Affeldt
  • National Institute of Advanced Industrial Science and Technology (AIST), Tokyo, Japan
Alessandro Bruni
  • IT University of Copenhagen, Denmark
Cyril Cohen
  • Inria, CNRS, ENS de Lyon, Université Claude Bernard Lyon 1, LIP, UMR 5668, Lyon, France
Pierre Roux
  • ONERA/DTIS, Université de Toulouse, France
Takafumi Saikawa
  • Nagoya University, Japan

Funding

The first and last authors acknowledge support of the JSPS KAKENHI Grant Number 22H00520, the second author acknowledges support of the Carlsberg Foundation, grant CF24-2347.

Acknowledgements

The authors are grateful to S. Sonoda for his inputs. The authors would like to thank the anonymous referees of ITP 2025 for their careful and informative review.

Supplementary Materials

References

  1. Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, and Carsten Schürmann. Robust mean estimation by all means (short paper). In 15th International Conference on Interactive Theorem Proving (ITP 2024), September 9-14, 2024, Tbilisi, Georgia, volume 309 of LIPIcs, pages 39:1-39:8. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.ITP.2024.39.
  2. Reynald Affeldt, Yves Bertot, Alessandro Bruni, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Pierre Roux, Kazuhiko Sakaguchi, Zachary Stone, Pierre-Yves Strub, and Laurent Théry. MathComp-Analysis: Mathematical components compliant analysis library. https://github.com/math-comp/analysis, July 2025. Since 2017. Latest stable version: 1.12.0.
  3. Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, and Takafumi Saikawa. Formalizing concentration inequalities in Rocq: infrastructure and automation. https://github.com/math-comp/analysis/pull/1645, July 2025. Development corresponding to Sections 5.3 and 6. Pull request to [Reynald Affeldt et al., 2025].
  4. Reynald Affeldt and Cyril Cohen. Measure construction by extension in dependent type theory with application to integration. J. Autom. Reason., 67(3):28, 2023. URL: https://doi.org/10.1007/s10817-023-09671-5.
  5. Reynald Affeldt, Cyril Cohen, and Damien Rouhling. Formalization techniques for asymptotic reasoning in classical analysis. J. Formaliz. Reason., 11(1):43-76, 2018. URL: https://doi.org/10.6092/issn.1972-5787/8124.
  6. Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa. Formal adventures in convex and conical spaces. In 13th Conference on Intelligent Computer Mathematics (CICM 2020), Bertinoro, Forli, Italy, July 26-31, 2020, volume 12236 of Lecture Notes in Artificial Intelligence, pages 23-38. Springer, July 2020. URL: https://doi.org/10.1007/978-3-030-53518-6_2.
  7. Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa. A library for formalization of linear error-correcting codes. J. Autom. Reason., 64(6):1123-1164, 2020. URL: https://doi.org/10.1007/s10817-019-09538-8.
  8. Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa. Reasoning with conditional probabilities and joint distributions in Coq. Computer Software, 37(3):79-95, 2020. Japan Society for Software Science and Technology. URL: https://doi.org/10.11309/jssst.37.3_79.
  9. Reynald Affeldt, Manabu Hagiwara, and Jonas Sénizergues. Formalization of Shannon’s theorems. J. Autom. Reason., 53(1):63-103, 2014. URL: https://doi.org/10.1007/S10817-013-9298-1.
  10. Reynald Affeldt and Zachary Stone. A comprehensive overview of the Lebesgue differentiation theorem in Coq. In 15th International Conference on Interactive Theorem Proving (ITP 2024), September 9-14, 2024, Tbilisi, Georgia, volume 309 of LIPIcs, pages 5:1-5:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.ITP.2024.5.
  11. Jeremy Avigad, Johannes Hölzl, and Luke Serafin. A formally verified proof of the central limit theorem. J. Autom. Reason., 59(4):389-423, 2017. URL: https://doi.org/10.1007/s10817-017-9404-x.
  12. Anne Baanen. Use and abuse of instance parameters in the Lean mathematical library. In 13th International Conference on Interactive Theorem Proving (ITP 2022), August 7-10, 2022, Haifa, Israel, volume 237 of LIPIcs, pages 4:1-4:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.ITP.2022.4.
  13. Frédéric Besson, David Cachera, Thomas P. Jensen, and David Pichardie. Certified static analysis by abstract interpretation. In Foundations of Security Analysis and Design V (FOSAD 2007/2008/2009), Tutorial Lectures, volume 5705 of Lecture Notes in Computer Science, pages 223-257. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03829-7_8.
  14. Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A user-friendly library of real analysis for Coq. Math. Comput. Sci., 9(1):41-62, 2015. URL: https://doi.org/10.1007/S11786-014-0181-1.
  15. Stéphane Boucheron, Gábor Lugosi, and Pascal Massart. Concentration Inequalities: A Nonasymptotic Theory of Independence. Oxford University Press, 2013. URL: https://doi.org/10.1093/ACPROF:OSO/9780199535255.001.0001.
  16. Matteo Capucci. On quantifiers for quantitative reasoning, 2025. URL: https://doi.org/10.48550/arXiv.2406.04936.
  17. Cyril Cohen. Pragmatic quotient types in Coq. In 4th International Conference on Interactive Theorem Proving (ITP 2013), Rennes, France, July 22-26, 2013, volume 7998 of Lecture Notes in Computer Science, pages 213-228. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_17.
  18. Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. Hierarchy builder: Algebraic hierarchies made easy in Coq with Elpi (system description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 34:1-34:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.34.
  19. Patrick Cousot and Radhia Cousot. Abstract interpretation frameworks. Journal of logic and computation, 2(4):511-547, 1992. URL: https://doi.org/10.1093/LOGCOM/2.4.511.
  20. Ieva Daukantas, Alessandro Bruni, and Carsten Schürmann. Trimming data sets: a verified algorithm for robust mean estimation. In 23rd International Symposium on Principles and Practice of Declarative Programming (PPDP 2021), Tallinn, Estonia, September 6-8, 2021, pages 17:1-17:9. ACM, 2021. URL: https://doi.org/10.1145/3479394.3479412.
  21. The MathComp development team. Mathematical components. https://github.com/math-comp/math-comp, 2005. Last stable version: 2.4.0 (2025).
  22. Jean Dieudonné. Treatise On Analysis, volume II. Academic Press, 1976. Google Scholar
  23. Sebastien Gouezel. Lp spaces. Archive of Formal Proofs, October 2016. , Formal proof development. URL: https://isa-afp.org/entries/Lp.html.
  24. Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal. Asynchronous probabilistic couplings in higher-order separation logic. Proc. ACM Program. Lang., 8(POPL):753-784, 2024. URL: https://doi.org/10.1145/3632868.
  25. InfoTheo. InfoTheo: A Coq formalization of information theory and linear error-correcting codes. https://github.com/affeldt-aist/infotheo, 2025. Authors: Reynald Affeldt, Manabu Hagiwara, Jonas Sénizergues, Jacques Garrigue, Kazuhiko Sakaguchi, Taku Asai, Takafumi Saikawa, Naruomi Obata, and Alessando Bruni. Last stable release: 0.9.3 (2025).
  26. Yoshihiro Ishiguro and Reynald Affeldt. The Radon-Nikodým theorem and the Lebesgue-Stieltjes measure in Coq. Computer Software, 41(2):41-59, 2024. Japan Society for Software Science and Technology. URL: https://doi.org/10.11309/jssst.41.2_41.
  27. Emin Karayel and Yong Kiam Tan. Concentration inequalities. Archive of Formal Proofs, November 2023. , Formal proof development. URL: https://isa-afp.org/entries/Concentration_Inequalities.html.
  28. Assia Mahboubi and Enrico Tassi. Mathematical Components. Zenodo, January 2021. URL: https://doi.org/10.5281/zenodo.4457887.
  29. Filip Markovic, Pierre Roux, Sergey Bozhko, Alessandro V. Papadopoulos, and Björn B. Brandenburg. CTA: A correlation-tolerant analysis of the deadline-failure probability of dependent tasks. In IEEE Real-Time Systems Symposium (RTSS 2023), Taipei, Taiwan, December 5-8, 2023, pages 317-330. IEEE, 2023. URL: https://doi.org/10.1109/RTSS59052.2023.00035.
  30. Jairo Miguel Marulanda-Giraldo, Ekaterina Komendantskaya, Alessandro Bruni, Reynald Affeldt, Matteo Capucci, and Enrico Marchioni. Quantifiers for differentiable logics in Rocq (extended abstract). In 8th International Symposium on AI Verification (SAIV 2025), Zagreb, Croatia, July 21-22, 2025, July 2025. Google Scholar
  31. Mathlib 4. File MeasureTheory/Function/LpSpace/Basic.lean. https://github.com/leanprover-community/mathlib4/blob/f3731eaabfa91f8610f09b48be38213d6c16d171/Mathlib/MeasureTheory/Function/LpSpace/Basic.lean#L87, June 2025.
  32. Guillaume Melquiond. Proving bounds on real-valued functions with computations. In 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Sydney, Australia, August 12-15, 2008, volume 5195 of Lecture Notes in Computer Science, pages 2-17. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71070-7_2.
  33. Guillaume Melquiond, Érik Martin-Dorel, Pierre Roux, and Thomas Sibut-Pinote. CoqInterval. https://coqinterval.gitlabpages.inria.fr/, 2025. Since 2008. Version 4.11.1.
  34. Michael Mitzenmacher and Eli Upfal. Probability and Computing - Randomized Algorithms and Probabilistic Analysis. Cambridge University Press, 2005. URL: https://doi.org/10.1017/CBO9780511813603.
  35. Samir Rajani. Applications of Chernoff bounds. http://math.uchicago.edu/~may/REU2019/REUPapers/Rajani.pdf, 2019. The University of Chicago Mathematics REU 2019.
  36. Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, and Naoto Onda. Lean formalization of generalization error bound by Rademacher complexity, 2025. URL: https://doi.org/10.48550/arXiv.2503.19605.
  37. Philip B. Stark. Risk-limiting postelection audits: conservative P-values from common probability inequalities. IEEE Trans. Inf. Forensics Secur., 4(4):1005-1014, 2009. URL: https://doi.org/10.1109/TIFS.2009.2034190.
  38. M. H. Stone. Postulates for the barycentric calculus. Annali di Matematica Pura ed Applicata, 29:25-30, 1949. Google Scholar
  39. Joseph Tassarotti. A probability theory library for the Coq theorem prover. https://github.com/jtassarotti/coq-proba, 2023. Since 2020.
  40. The Coq Development Team. Automatic solvers and programmable tactics, 2024. Chapter in [The Coq Development Team, 2024]. Google Scholar
  41. The Coq Development Team. The SSReflect proof language, 2024. Chapter in [The Coq Development Team, 2024]. Google Scholar
  42. The Coq Development Team. The Coq reference manual. https://rocq-prover.org/doc/V8.20.1/refman/index.html, 2024. Release 8.20.1.
  43. The FormalML development team. FormalML: Formalization of machine learning theory with applications to program synthesis. https://github.com/IBM/FormalML, 2025. Since 2019.
  44. The mathlib Community. The lean mathematical library. In 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), New Orleans, LA, USA, January 20-21, 2020, pages 367-381. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373824.
  45. Koundinya Vajjha, Avraham Shinnar, Barry M. Trager, Vasily Pestun, and Nathan Fulton. CertRL: formalizing convergence proofs for value and policy iteration in Coq. In 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021), Virtual Event, Denmark, January 17-19, 2021, pages 18-31. ACM, 2021. URL: https://doi.org/10.1145/3437992.3439927.
  46. Koundinya Vajjha, Barry M. Trager, Avraham Shinnar, and Vasily Pestun. Formalization of a stochastic approximation theorem. In 13th International Conference on Interactive Theorem Proving (ITP 2022), August 7-10, 2022, Haifa, Israel, volume 237 of LIPIcs, pages 31:1-31:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.ITP.2022.31.
  47. Rosalind Cecily Young. The algebra of many-valued quantities. Mathematische Annalen, 104(1):260-290, 1931. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact