Lower bounds for hypothesis testing based on information theory

The goal of this project is to formalize in Lean the definitions and properties of information divergences between probability measures, as well as results about error bounds for (sequential) hypothesis testing.

For a detailed presentation, see the blueprint at https://remydegenne.github.io/testing-lower-bounds/blueprint/index.html

Contents

• Definitions of divergences between measures: f-divergence, Kullback-Leibler (or relative entropy), Rényi, TV, DeGroot statistical information
• Definition of an estimation task and its risk
• Proofs of the data-processing inequality for f-divergences (in progress)

Technical note

To do a Mathlib bump without breaking the blueprint, use lake -R -Kenv=dev update