# mathlib3documentation

probability.martingale.upcrossing

# 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$.

noncomputable def measure_theory.lower_crossing_time_aux {Ω : Type u_1} {ι : Type u_2} [preorder ι] [has_Inf ι] (a : ) (f : ι Ω ) (c N : ι) :
Ω ι

lower_crossing_time_aux a f c N is the first time f reached below a after time c before time N.

Equations
• = c N
noncomputable def measure_theory.upper_crossing_time {Ω : Type u_1} {ι : Type u_2} [preorder ι] [order_bot ι] [has_Inf ι] (a b : ) (f : ι Ω ) (N : ι) :
Ω ι

upper_crossing_time a b f N n is the first time before time N, f reaches above b after f reached below a for the n - 1-th time.

Equations
• (n + 1) = λ (ω : Ω), n ω) N ω) N ω
• 0 =
noncomputable def measure_theory.lower_crossing_time {Ω : Type u_1} {ι : Type u_2} [preorder ι] [order_bot ι] [has_Inf ι] (a b : ) (f : ι Ω ) (N : ι) (n : ) :
Ω ι

lower_crossing_time a b f N n is the first time before time N, f reaches below a after f reached above b for the n-th time.

Equations
• n = λ (ω : Ω), n ω) N ω
@[simp]
theorem measure_theory.upper_crossing_time_zero {Ω : Type u_1} {ι : Type u_2} [preorder ι] [order_bot ι] [has_Inf ι] {a b : } {f : ι Ω } {N : ι} :
0 =
@[simp]
theorem measure_theory.lower_crossing_time_zero {Ω : Type u_1} {ι : Type u_2} [preorder ι] [order_bot ι] [has_Inf ι] {a b : } {f : ι Ω } {N : ι} :
0 = N
theorem measure_theory.upper_crossing_time_succ {Ω : Type u_1} {ι : Type u_2} [preorder ι] [order_bot ι] [has_Inf ι] {a b : } {f : ι Ω } {N : ι} {n : } {ω : Ω} :
(n + 1) ω = n ω) N ω) N ω
theorem measure_theory.upper_crossing_time_succ_eq {Ω : Type u_1} {ι : Type u_2} [preorder ι] [order_bot ι] [has_Inf ι] {a b : } {f : ι Ω } {N : ι} {n : } (ω : Ω) :
(n + 1) ω = n ω) N ω
theorem measure_theory.upper_crossing_time_le {Ω : Type u_1} {ι : Type u_2} {a b : } {f : ι Ω } {N : ι} {n : } {ω : Ω} :
n ω N
@[simp]
theorem measure_theory.upper_crossing_time_zero' {Ω : Type u_1} {ι : Type u_2} {a b : } {f : ι Ω } {n : } {ω : Ω} :
ω =
theorem measure_theory.lower_crossing_time_le {Ω : Type u_1} {ι : Type u_2} {a b : } {f : ι Ω } {N : ι} {n : } {ω : Ω} :
n ω N
theorem measure_theory.upper_crossing_time_le_lower_crossing_time {Ω : Type u_1} {ι : Type u_2} {a b : } {f : ι Ω } {N : ι} {n : } {ω : Ω} :
n ω n ω
theorem measure_theory.lower_crossing_time_le_upper_crossing_time_succ {Ω : Type u_1} {ι : Type u_2} {a b : } {f : ι Ω } {N : ι} {n : } {ω : Ω} :
n ω (n + 1) ω
theorem measure_theory.lower_crossing_time_mono {Ω : Type u_1} {ι : Type u_2} {a b : } {f : ι Ω } {N : ι} {n m : } {ω : Ω} (hnm : n m) :
n ω m ω
theorem measure_theory.upper_crossing_time_mono {Ω : Type u_1} {ι : Type u_2} {a b : } {f : ι Ω } {N : ι} {n m : } {ω : Ω} (hnm : n m) :
n ω m ω
theorem measure_theory.stopped_value_lower_crossing_time {Ω : Type u_1} {a b : } {f : Ω } {N n : } {ω : Ω} (h : n ω N) :
ω a
theorem measure_theory.stopped_value_upper_crossing_time {Ω : Type u_1} {a b : } {f : Ω } {N n : } {ω : Ω} (h : (n + 1) ω N) :
b (n + 1)) ω
theorem measure_theory.upper_crossing_time_lt_lower_crossing_time {Ω : Type u_1} {a b : } {f : Ω } {N n : } {ω : Ω} (hab : a < b) (hn : (n + 1) ω N) :
(n + 1) ω < (n + 1) ω
theorem measure_theory.lower_crossing_time_lt_upper_crossing_time {Ω : Type u_1} {a b : } {f : Ω } {N n : } {ω : Ω} (hab : a < b) (hn : (n + 1) ω N) :
n ω < (n + 1) ω
theorem measure_theory.upper_crossing_time_lt_succ {Ω : Type u_1} {a b : } {f : Ω } {N n : } {ω : Ω} (hab : a < b) (hn : (n + 1) ω N) :
n ω < (n + 1) ω
theorem measure_theory.lower_crossing_time_stabilize {Ω : Type u_1} {a b : } {f : Ω } {N n m : } {ω : Ω} (hnm : n m) (hn : n ω = N) :
m ω = N
theorem measure_theory.upper_crossing_time_stabilize {Ω : Type u_1} {a b : } {f : Ω } {N n m : } {ω : Ω} (hnm : n m) (hn : n ω = N) :
m ω = N
theorem measure_theory.lower_crossing_time_stabilize' {Ω : Type u_1} {a b : } {f : Ω } {N n m : } {ω : Ω} (hnm : n m) (hn : N n ω) :
m ω = N
theorem measure_theory.upper_crossing_time_stabilize' {Ω : Type u_1} {a b : } {f : Ω } {N n m : } {ω : Ω} (hnm : n m) (hn : N n ω) :
m ω = N
theorem measure_theory.exists_upper_crossing_time_eq {Ω : Type u_1} {a b : } (f : Ω ) (N : ) (ω : Ω) (hab : a < b) :
(n : ), n ω = N
theorem measure_theory.upper_crossing_time_lt_bdd_above {Ω : Type u_1} {a b : } {f : Ω } {N : } {ω : Ω} (hab : a < b) :
bdd_above {n : | n ω < N}
theorem measure_theory.upper_crossing_time_lt_nonempty {Ω : Type u_1} {a b : } {f : Ω } {N : } {ω : Ω} (hN : 0 < N) :
{n : | n ω < N}.nonempty
theorem measure_theory.upper_crossing_time_bound_eq {Ω : Type u_1} {a b : } (f : Ω ) (N : ) (ω : Ω) (hab : a < b) :
N ω = N
theorem measure_theory.upper_crossing_time_eq_of_bound_le {Ω : Type u_1} {a b : } {f : Ω } {N n : } {ω : Ω} (hab : a < b) (hn : N n) :
n ω = N
theorem measure_theory.adapted.is_stopping_time_crossing {Ω : Type u_1} {m0 : measurable_space Ω} {a b : } {f : Ω } {N n : } {ℱ : m0} (hf : f) :
theorem measure_theory.adapted.is_stopping_time_upper_crossing_time {Ω : Type u_1} {m0 : measurable_space Ω} {a b : } {f : Ω } {N n : } {ℱ : m0} (hf : f) :
theorem measure_theory.adapted.is_stopping_time_lower_crossing_time {Ω : Type u_1} {m0 : measurable_space Ω} {a b : } {f : Ω } {N n : } {ℱ : m0} (hf : f) :
noncomputable def measure_theory.upcrossing_strat {Ω : Type u_1} (a b : ) (f : Ω ) (N n : ) (ω : Ω) :

upcrossing_strat a b f N n is 1 if n is between a consecutive pair of lower and upper crossings and is 0 otherwise. upcrossing_strat is shifted by one index so that it is adapted rather than predictable.

Equations
theorem measure_theory.upcrossing_strat_nonneg {Ω : Type u_1} {a b : } {f : Ω } {N n : } {ω : Ω} :
0 n ω
theorem measure_theory.upcrossing_strat_le_one {Ω : Type u_1} {a b : } {f : Ω } {N n : } {ω : Ω} :
n ω 1
theorem measure_theory.adapted.upcrossing_strat_adapted {Ω : Type u_1} {m0 : measurable_space Ω} {a b : } {f : Ω } {N : } {ℱ : m0} (hf : f) :
theorem measure_theory.submartingale.sum_upcrossing_strat_mul {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {f : Ω } {ℱ : m0} (hf : μ) (a b : ) (N : ) :
measure_theory.submartingale (λ (n : ), (finset.range n).sum (λ (k : ), k * (f (k + 1) - f k))) μ
theorem measure_theory.submartingale.sum_sub_upcrossing_strat_mul {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {f : Ω } {ℱ : m0} (hf : μ) (a b : ) (N : ) :
measure_theory.submartingale (λ (n : ), (finset.range n).sum (λ (k : ), (1 - k) * (f (k + 1) - f k))) μ
theorem measure_theory.submartingale.sum_mul_upcrossing_strat_le {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {a b : } {f : Ω } {N n : } {ℱ : m0} (hf : μ) :
(x : Ω), (finset.range n).sum (λ (k : ), k * (f (k + 1) - f k)) x μ (x : Ω), f n x μ - (x : Ω), f 0 x μ
noncomputable def measure_theory.upcrossings_before {Ω : Type u_1} {ι : Type u_2} [preorder ι] [order_bot ι] [has_Inf ι] (a b : ) (f : ι Ω ) (N : ι) (ω : Ω) :

The number of upcrossings (strictly) before time N.

Equations
@[simp]
theorem measure_theory.upcrossings_before_bot {Ω : Type u_1} {ι : Type u_2} [preorder ι] [order_bot ι] [has_Inf ι] {a b : } {f : ι Ω } {ω : Ω} :
theorem measure_theory.upcrossings_before_zero {Ω : Type u_1} {a b : } {f : Ω } {ω : Ω} :
ω = 0
@[simp]
theorem measure_theory.upcrossings_before_zero' {Ω : Type u_1} {a b : } {f : Ω } :
= 0
theorem measure_theory.upper_crossing_time_lt_of_le_upcrossings_before {Ω : Type u_1} {a b : } {f : Ω } {N n : } {ω : Ω} (hN : 0 < N) (hab : a < b) (hn : n ω) :
n ω < N
theorem measure_theory.upper_crossing_time_eq_of_upcrossings_before_lt {Ω : Type u_1} {a b : } {f : Ω } {N n : } {ω : Ω} (hab : a < b) (hn : ω < n) :
n ω = N
theorem measure_theory.upcrossings_before_le {Ω : Type u_1} {a b : } {N : } (f : Ω ) (ω : Ω) (hab : a < b) :
ω N
theorem measure_theory.crossing_eq_crossing_of_lower_crossing_time_lt {Ω : Type u_1} {a b : } {f : Ω } {N n : } {ω : Ω} {M : } (hNM : N M) (h : n ω < N) :
n ω = n ω n ω = n ω
theorem measure_theory.crossing_eq_crossing_of_upper_crossing_time_lt {Ω : Type u_1} {a b : } {f : Ω } {N n : } {ω : Ω} {M : } (hNM : N M) (h : (n + 1) ω < N) :
(n + 1) ω = (n + 1) ω n ω = n ω
theorem measure_theory.upper_crossing_time_eq_upper_crossing_time_of_lt {Ω : Type u_1} {a b : } {f : Ω } {N n : } {ω : Ω} {M : } (hNM : N M) (h : n ω < N) :
n ω = n ω
theorem measure_theory.upcrossings_before_mono {Ω : Type u_1} {a b : } {f : Ω } (hab : a < b) :
monotone (λ (N : ) (ω : Ω), ω)
theorem measure_theory.upcrossings_before_lt_of_exists_upcrossing {Ω : Type u_1} {a b : } {f : Ω } {N : } {ω : Ω} (hab : a < b) {N₁ N₂ : } (hN₁ : N N₁) (hN₁' : f N₁ ω < a) (hN₂ : N₁ N₂) (hN₂' : b < f N₂ ω) :
ω < (N₂ + 1) ω
theorem measure_theory.lower_crossing_time_lt_of_lt_upcrossings_before {Ω : Type u_1} {a b : } {f : Ω } {N n : } {ω : Ω} (hN : 0 < N) (hab : a < b) (hn : n < ω) :
n ω < N
theorem measure_theory.le_sub_of_le_upcrossings_before {Ω : Type u_1} {a b : } {f : Ω } {N n : } {ω : Ω} (hN : 0 < N) (hab : a < b) (hn : n < ω) :
b - a (n + 1)) ω - ω
theorem measure_theory.sub_eq_zero_of_upcrossings_before_lt {Ω : Type u_1} {a b : } {f : Ω } {N n : } {ω : Ω} (hab : a < b) (hn : ω < n) :
(n + 1)) ω - ω = 0
theorem measure_theory.mul_upcrossings_before_le {Ω : Type u_1} {a b : } {f : Ω } {N : } {ω : Ω} (hf : a f N ω) (hab : a < b) :
(b - a) * ω) (finset.range N).sum (λ (k : ), k ω * (f (k + 1) - f k) ω)
theorem measure_theory.integral_mul_upcrossings_before_le_integral {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {a b : } {f : Ω } {N : } {ℱ : m0} (hf : μ) (hfN : (ω : Ω), a f N ω) (hfzero : 0 f 0) (hab : a < b) :
(b - a) * (x : Ω), x) μ (x : Ω), f N x μ
theorem measure_theory.crossing_pos_eq {Ω : Type u_1} {a b : } {f : Ω } {N n : } (hab : a < b) :
(λ (n : ) (ω : Ω), (f n ω - a)) N n = n (λ (n : ) (ω : Ω), (f n ω - a)) N n = n
theorem measure_theory.upcrossings_before_pos_eq {Ω : Type u_1} {a b : } {f : Ω } {N : } {ω : Ω} (hab : a < b) :
(λ (n : ) (ω : Ω), (f n ω - a)) N ω = ω
theorem measure_theory.mul_integral_upcrossings_before_le_integral_pos_part_aux {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {a b : } {f : Ω } {N : } {ℱ : m0} (hf : μ) (hab : a < b) :
(b - a) * (x : Ω), x) μ (x : Ω), (λ (ω : Ω), (f N ω - a)) x μ
theorem measure_theory.submartingale.mul_integral_upcrossings_before_le_integral_pos_part {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {f : Ω } {ℱ : m0} (a b : ) (hf : μ) (N : ) :
(b - a) * (x : Ω), x) μ (x : Ω), (λ (ω : Ω), (f N ω - a)) x μ

Doob's upcrossing estimate: given a real valued discrete submartingale f and real values a and b, we have (b - a) * 𝔼[upcrossings_before a b f N] ≤ 𝔼[(f N - a)⁺] where upcrossings_before a b f N is the number of times the process f crossed from below a to above b before the time 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.

theorem measure_theory.upcrossings_before_eq_sum {Ω : Type u_1} {a b : } {f : Ω } {N : } {ω : Ω} (hab : a < b) :
ω = (N + 1)).sum (λ (i : ), {n : | n ω < N}.indicator 1 i)
theorem measure_theory.adapted.measurable_upcrossings_before {Ω : Type u_1} {m0 : measurable_space Ω} {a b : } {f : Ω } {N : } {ℱ : m0} (hf : f) (hab : a < b) :
theorem measure_theory.adapted.integrable_upcrossings_before {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {a b : } {f : Ω } {N : } {ℱ : m0} (hf : f) (hab : a < b) :
measure_theory.integrable (λ (ω : Ω), ω)) μ
noncomputable def measure_theory.upcrossings {Ω : Type u_1} {ι : Type u_2} [preorder ι] [order_bot ι] [has_Inf ι] (a b : ) (f : ι Ω ) (ω : Ω) :

The number of upcrossings of a realization of a stochastic process (upcrossing takes value in ℝ≥0∞ and so is allowed to be ∞).

Equations
theorem measure_theory.adapted.measurable_upcrossings {Ω : Type u_1} {m0 : measurable_space Ω} {a b : } {f : Ω } {ℱ : m0} (hf : f) (hab : a < b) :
theorem measure_theory.upcrossings_lt_top_iff {Ω : Type u_1} {a b : } {f : Ω } {ω : Ω} :
ω < (k : ), (N : ), ω k
theorem measure_theory.submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {f : Ω } {ℱ : m0} (a b : ) (hf : μ) :
ennreal.of_real (b - a) * ∫⁻ (ω : Ω), ω μ (N : ), ∫⁻ (ω : Ω), ennreal.of_real (f N ω - a) μ

A variant of Doob's upcrossing estimate obtained by taking the supremum on both sides.