Is there any lemma or theorem about chernoff bound inequality in HOL-probability?
In Isabelle2021, no.
In the development version, yes:
(search for "chernoff")
The proofs are very short, so if you really need those bounds, you can just copy them out from there.
ok, so I guess there is no discrete version of chernoff bound, is that right?
All the chernoff bound we have is based on measure theory and integral?
Well, the discrete case is a just a simple special case of this
Discrete probability stuff in Isabelle is usually done with the
pmf type (
'a pmf is the type of discrete probability distributions over a type
'a). You can convert an
'a pmf into an
'a measure with the
measure_pmf function. If you simply plug in
measure_pmf p for some PMF
p in the theorems above, you have the discrete version.
Then the integrals are just sums (finite sums if your PMFs have finite support).
Well I totally agree, do you have some concrete example in probability to show how to switch continuous results into discrete one
Not sure how readable it is, but here I first prove Hoeffding's inequality for general measures and then use it for Bernoulli distributions, which are discrete: https://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Probability/Hoeffding.thy
perfect. btw do you see any article about like using any inequality we established in AFP into some result about game theory?
I don't understand this question.
Last updated: Sep 25 2022 at 23:25 UTC