### Abstract

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.

### License

BSD License

### Topics

- Mathematics/Probability theory

### Session Concentration_Inequalities

- Concentration_Inequalities_Preliminary
- Bennett_Inequality
- Bienaymes_Identity
- Cantelli_Inequality
- Efron_Stein_Inequality
- McDiarmid_Inequality
- Paley_Zygmund_Inequality

### Depends on

- Lp spaces

### Used by

- Approximate Model Counting

## Cite

×

Concentration_Inequalities-AFP

    @article{Concentration_Inequalities-AFP,
      author  = {Emin Karayel and Yong Kiam Tan},
      title   = {Concentration Inequalities},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Concentration_Inequalities.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest