### Abstract

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 $\sigma$-algebra containing all of the $\sigma$-algebras in the filtration. Equivalent statements for martingales and supermartingales are also provided as corollaries.

### License

BSD License

### Topics

- Mathematics/Probability theory

### Related publications

- Ying, K., & Degenne, R. (2022). A Formalization of Doob's Martingale Convergence Theorems in mathlib (Version 1). arXiv. https://doi.org/10.48550/ARXIV.2212.05578

### Session Doob_Convergence

- Martingales_Updates
- Stopping_Time
- Upcrossing
- Doob_Convergence

### Depends on

- Martingales

## Cite

×

Doob_Convergence-AFP

    @article{Doob_Convergence-AFP,
      author  = {Ata Keskin},
      title   = {Doob's Upcrossing Inequality and Martingale Convergence Theorem},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2024},
      note    = {\url{https://isa-afp.org/entries/Doob_Convergence.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest