Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation
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.
Authors
- Reynald Affeldt (ORCID: https://orcid.org/0000-0002-2327-953X)
- A. Bruni (ORCID: https://orcid.org/0000-0002-5439-8005)
- Pierre Roux (ORCID: https://orcid.org/0000-0002-3041-7742)
- Takafumi Saikawa (ORCID: https://orcid.org/0000-0003-4492-745X)
- Cyril Cohen (ORCID: https://orcid.org/0000-0003-3540-1050)
Institutions
- Université Claude Bernard Lyon 1 (FR)
- École Normale Supérieure de Lyon (FR)
- Centre National de la Recherche Scientifique (FR)
- Université Fédérale de Toulouse Midi-Pyrénées (FR)
- Université Paris-Saclay (FR)
- Office National d'Études et de Recherches Aérospatiales (FR)
- Laboratoire de l'Informatique du Parallélisme (FR)
- Nagoya University (JP)
- National Institute of Advanced Industrial Science and Technology (JP)
- IT University of Copenhagen (DK)
Publication Details
- Journal
- IT University Of Copenhagen (IT University of Copenhagen)
- Published
- 2025-01-01
- DOI
- https://doi.org/10.4230/lipics.itp.2025.21
- Primary Topic
- Formal Methods in Verification
- Type
- article
- Field-Weighted Citation Impact
- 0.00
Funders
- Japan Society for the Promotion of Science