Doob's upcrossing estimate #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given a discrete real-valued submartingale $(f_n)_{n \in \mathbb{N}}$, denoting $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 #

• measure_theory.upper_crossing_time 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).
• measure_theory.lower_crossing_time 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).
• measure_theory.upcrossing_strat a b f N: is the predictable process which is 1 if n is between a consecutive pair of lower and upper crossing and is 0 otherwise. Intuitively one might think of the upcrossing_strat 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.
• measure_theory.upcrossings_before a b f N: is the number of times f crosses from below a to above b before time N.
• measure_theory.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 #

• measure_theory.adapted.is_stopping_time_upper_crossing_time: upper_crossing_time is a stopping time whenever the process it is associated to is adapted.
• measure_theory.adapted.is_stopping_time_lower_crossing_time: lower_crossing_time is a stopping time whenever the process it is associated to is adapted.
• measure_theory.submartingale.mul_integral_upcrossings_before_le_integral_pos_part: Doob's upcrossing estimate.
• measure_theory.submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part: the inequality obtained by taking the supremum on both sides of Doob's upcrossing estimate.

References #

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

Proof outline #

In this section, we will denote $U_N(a, b)$ the number of upcrossings of $(f_n)$ from below $a$ to above $b$ before time $N$.

To define $U_N(a, b)$, we will construct two stopping times corresponding to when $(f_n)$ crosses below $a$ and above $b$. Namely, we define $$ \sigma_n := \inf \{n \ge \tau_n \mid f_n \le a\} \wedge N; $$ $$ \tau_{n + 1} := \inf \{n \ge \sigma_n \mid f_n \ge b\} \wedge N. $$ These are lower_crossing_time and upper_crossing_time in our formalization which are defined using measure_theory.hitting allowing us to specify a starting and ending time. Then, we may simply define $U_N(a, b) := \sup \{n \mid \tau_n < N\}$.

Fixing $a < b \in \mathbb{R}$, we will first prove the theorem in the special case that $0 \le f_0$ and $a \le f_N$. In particular, we will show $$ (b - a) \mathbb{E}[U_N(a, b)] \le \mathbb{E}[f_N]. $$ This is measure_theory.integral_mul_upcrossings_before_le_integral in our formalization.

To prove this, we use the fact that given a non-negative, bounded, predictable process $(C_n)$ (i.e. $(C_{n + 1})$ is adapted), $(C \bullet f)_n := \sum_{k \le n} C_{k + 1}(f_{k + 1} - f_k)$ is a submartingale if $(f_n)$ is.

Define $C_n := \sum_{k \le n} \mathbf{1}_{[\sigma_k, \tau_{k + 1})}(n)$. It is easy to see that $(1 - C_n)$ is non-negative, bounded and predictable, and hence, given a submartingale $(f_n)$, $(1 - C) \bullet f$ is also a submartingale. Thus, by the submartingale property, $0 \le \mathbb{E}[((1 - C) \bullet f)_0] \le \mathbb{E}[((1 - C) \bullet f)_N]$ implying $$ \mathbb{E}[(C \bullet f)_N] \le \mathbb{E}[(1 \bullet f)_N] = \mathbb{E}[f_N] - \mathbb{E}[f_0]. $$

Furthermore, \begin{align} (C \bullet f)_N & = \sum_{n \le N} \sum_{k \le N} \mathbf{1}_{[\sigma_k, \tau_{k + 1})}(n)(f_{n + 1} - f_n)\\ & = \sum_{k \le N} \sum_{n \le N} \mathbf{1}_{[\sigma_k, \tau_{k + 1})}(n)(f_{n + 1} - f_n)\\ & = \sum_{k \le N} (f_{\sigma_k + 1} - f_{\sigma_k} + f_{\sigma_k + 2} - f_{\sigma_k + 1} + \cdots + f_{\tau_{k + 1}} - f_{\tau_{k + 1} - 1})\\ & = \sum_{k \le N} (f_{\tau_{k + 1}} - f_{\sigma_k}) \ge \sum_{k < U_N(a, b)} (b - a) = (b - a) U_N(a, b) \end{align} where the inequality follows since for all $k < U_N(a, b)$, $f_{\tau_{k + 1}} - f_{\sigma_k} \ge b - a$ while for all $k > U_N(a, b)$, $f_{\tau_{k + 1}} = f_{\sigma_k} = f_N$ and $f_{\tau_{U_N(a, b) + 1}} - f_{\sigma_{U_N(a, b)}} = f_N - a \ge 0$. Hence, we have $$ (b - a) \mathbb{E}[U_N(a, b)] \le \mathbb{E}[(C \bullet f)_N] \le \mathbb{E}[f_N] - \mathbb{E}[f_0] \le \mathbb{E}[f_N], $$ as required.

To obtain the general case, we simply apply the above to $((f_n - a)^+)_n$.

Variant of the upcrossing estimate #

Now, we would like to prove a variant of the upcrossing estimate obtained by taking the supremum over $N$ of the original upcrossing estimate. Namely, we want the inequality $$ (b - a) \sup_N \mathbb{E}[U_N(a, b)] \le \sup_N \mathbb{E}[f_N]. $$ This inequality is central for the martingale convergence theorem as it provides a uniform bound for the upcrossings.

We note that on top of taking the supremum on both sides of the inequality, we had also used the monotone convergence theorem on the left hand side to take the supremum outside of the integral. To do this, we need to make sure $U_N(a, b)$ is measurable and integrable. Integrability is easy to check as $U_N(a, b) ≤ N$ and so it suffices to show measurability. Indeed, by noting that $$ U_N(a, b) = \sum_{i = 1}^N \mathbf{1}_{\{U_N(a, b) < N\}} $$ $U_N(a, b)$ is measurable as $\{U_N(a, b) < N\}$ is a measurable set since $U_N(a, b)$ is a stopping time.