Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Concentration Inequalities


view this post on Zulip Email Gateway (Dec 05 2023 at 23:46):

From: Manuel Eberl <manuel@pruvisto.org>
Concentration Inequalities

by Emin Karayel and Yong Kiam Tan

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.

https://www.isa-afp.org/entries/Concentration_Inequalities.html

Enjoy,

Manuel


Last updated: Apr 28 2024 at 20:16 UTC