[isabelle] Supermartingale and Azuma–Hoeffding inequality

[Kawin Worrasangasilpa]

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

[Johannes Hölzl]

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:

* Filtration.thy in AFP-DiscretePricing
* Stopping_Time.thy in HOL-Probability

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

Best,
Johannes

Post by Kawin Worrasangasilpa
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