Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Supermartingale and Azuma–Hoeffding inequality

view this post on Zulip Email Gateway (Aug 22 2022 at 18:21):

From: Kawin Worrasangasilpa <kw448@cam.ac.uk>
Hi,

I am proving results in Isabelle/HOL in which they need the use
of Supermartingale and Azuma–Hoeffding inequality. I have been trying to
search for existing theorems containing them or ways to formalise them but,
unfortunately, have not yet found any. If there anyone who knows where I
should start or an ongoing/published (or unpublished) work regarding these
two, if it is the case, please help me.

Thanks,
Kawin

view this post on Zulip Email Gateway (Aug 22 2022 at 18:21):

From: Johannes Hölzl <johannes.hoelzl@gmx.de>
Dear Kawin,

there is not yet much theory on Martingales. There is the definition
and some theorems (closure under addition) in AFP-DiscretePricing, but
nothing about super-martingales. Unfortunately, we even have two
theories of filtrations:

I'm not aware of any work on these inequalities.

Best,
Johannes

Last updated: Apr 26 2024 at 12:28 UTC