Is there any lemma or theorem about chernoff bound inequality in HOL-probability?

In Isabelle2021, no.

In the development version, yes:

https://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Analysis/Set_Integral.thy

https://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy

(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