## Stream: Beginner Questions

### Topic: chernoff

#### zibo yang (May 21 2021 at 13:54):

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

#### Manuel Eberl (May 21 2021 at 13:59):

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.

#### zibo yang (May 21 2021 at 14:15):

ok, so I guess there is no discrete version of chernoff bound, is that right?

#### zibo yang (May 21 2021 at 14:15):

All the chernoff bound we have is based on measure theory and integral?

#### Manuel Eberl (May 21 2021 at 14:16):

Well, the discrete case is a just a simple special case of this

#### Manuel Eberl (May 21 2021 at 14:18):

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.

#### Manuel Eberl (May 21 2021 at 14:18):

Then the integrals are just sums (finite sums if your PMFs have finite support).

#### zibo yang (May 21 2021 at 14:19):

Well I totally agree, do you have some concrete example in probability to show how to switch continuous results into discrete one

#### Manuel Eberl (May 21 2021 at 14:21):

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

#### zibo yang (May 21 2021 at 14:39):

perfect. btw do you see any article about like using any inequality we established in AFP into some result about game theory?

#### Manuel Eberl (May 21 2021 at 16:34):

I don't understand this question.

Last updated: Aug 13 2022 at 06:26 UTC