Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Doob's Upcrossing Inequality a...


view this post on Zulip Email Gateway (Mar 29 2024 at 22:02):

From: Manuel Eberl <manuel@pruvisto.org>
I am happy to present another substantial addition to our already
substantial collection of probability theory:

Doob's Upcrossing Inequality and Martingale Convergence Theorem
by Ata Keskin

In this entry, we formalize Doob's upcrossing inequality and
subsequently prove Doob's first martingale convergence theorem.

The upcrossing inequality is a fundamental result in the study of
martingales. It provides a bound on the expected number of times a
submartingale crosses a certain threshold within a given interval.

Doob's martingale convergence theorem states that if we have a
submartingale where the supremum over the mean of the positive parts is
finite, then the limit process exists almost surely and is integrable.
Furthermore, the limit process is measurable with respect to the
smallest σ-algebra containing all of the σ-algebras in the filtration.
Equivalent statements for martingales and supermartingales are also
provided as corollaries.

https://www.isa-afp.org/entries/Doob_Convergence.html

Enjoy!

Manuel


Last updated: May 04 2024 at 20:16 UTC