CPS Seminar: 25 June 2025, 11:30 – 13:00

B58, room 1065

Speaker: Alessandro Bruni, ITU Copenhagen

Title: Formalizing concentration inequalities in Rocq: infrastructure and automation

Authors: 

• Reynald Affeldt
• Alessandro Bruni
• Cyril Cohen
• Pierre Roux
• Takafumi Saikawa

 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.