# Documentation

Mathlib.Probability.Martingale.Upcrossing

# Doob's upcrossing estimate #

Given a discrete real-valued submartingale $(f_n)_{n \in \mathbb{N}}$, denoting by $U_N(a, b)$ the number of times $f_n$ crossed from below $a$ to above $b$ before time $N$, Doob's upcrossing estimate (also known as Doob's inequality) states that $$(b - a) \mathbb{E}[U_N(a, b)] \le \mathbb{E}[(f_N - a)^+].$$ Doob's upcrossing estimate is an important inequality and is central in proving the martingale convergence theorems.

## Main definitions #

• MeasureTheory.upperCrossingTime a b f N n: is the stopping time corresponding to f crossing above b the n-th time before time N (if this does not occur then the value is taken to be N).
• MeasureTheory.lowerCrossingTime a b f N n: is the stopping time corresponding to f crossing below a the n-th time before time N (if this does not occur then the value is taken to be N).
• MeasureTheory.upcrossingStrat a b f N: is the predictable process which is 1 if n is between a consecutive pair of lower and upper crossings and is 0 otherwise. Intuitively one might think of the upcrossingStrat as the strategy of buying 1 share whenever the process crosses below a for the first time after selling and selling 1 share whenever the process crosses above b for the first time after buying.
• MeasureTheory.upcrossingsBefore a b f N: is the number of times f crosses from below a to above b before time N.
• MeasureTheory.upcrossings a b f: is the number of times f crosses from below a to above b. This takes value in ℝ≥0∞ and so is allowed to be ∞.

## Main results #

• MeasureTheory.Adapted.isStoppingTime_upperCrossingTime: upperCrossingTime is a stopping time whenever the process it is associated to is adapted.
• MeasureTheory.Adapted.isStoppingTime_lowerCrossingTime: lowerCrossingTime is a stopping time whenever the process it is associated to is adapted.
• MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part: Doob's upcrossing estimate.
• MeasureTheory.Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part: the inequality obtained by taking the supremum on both sides of Doob's upcrossing estimate.

We mostly follow the proof from [Kallenberg, Foundations of modern probability][kallenberg2021]