Stream: Beginner Questions

Topic: chernoff


view this post on Zulip zibo yang (May 21 2021 at 13:54):

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

view this post on Zulip 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.

view this post on Zulip zibo yang (May 21 2021 at 14:15):

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

view this post on Zulip zibo yang (May 21 2021 at 14:15):

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

view this post on Zulip Manuel Eberl (May 21 2021 at 14:16):

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

view this post on Zulip 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.

view this post on Zulip Manuel Eberl (May 21 2021 at 14:18):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Manuel Eberl (May 21 2021 at 16:34):

I don't understand this question.


Last updated: Aug 13 2022 at 06:26 UTC