zibo yang (May 21 2021 at 13:54): 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: Apr 23 2024 at 20:15 UTC