Concentration Inequalities

Emin Karayel 📧 and Yong Kiam Tan 📧

November 13, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


Concentration inequalities provide bounds on how a random variable (or a sum/composition of random variables) deviate from their expectation, usually based on moments/independence of the variables. The most important concentration inequalities (the Markov, Chebyshev, and Hoelder inequalities and the Chernoff bounds) are already part of HOL-Probability. This entry collects more advanced results, such as Bennett's/Bernstein's Inequality, Bienayme's Identity, Cantelli's Inequality, the Efron-Stein Inequality, McDiarmid's Inequality, and the Paley-Zygmund Inequality.


BSD License


Session Concentration_Inequalities