mathlib documentation

probability.martingale.upcrossing

Doob's upcrossing estimate #

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 #

Main results #

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
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
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
@[simp]
theorem measure_theory.upper_crossing_time_zero {Ω : Type u_1} {ι : Type u_2} [preorder ι] [order_bot ι] [has_Inf ι] {a b : } {f : ι → Ω → } {N : ι} :
@[simp]
theorem measure_theory.lower_crossing_time_zero {Ω : Type u_1} {ι : Type u_2} [preorder ι] [order_bot ι] [has_Inf ι] {a b : } {f : ι → Ω → } {N : ι} :
theorem measure_theory.upper_crossing_time_succ {Ω : Type u_1} {ι : Type u_2} [preorder ι] [order_bot ι] [has_Inf ι] {a b : } {f : ι → Ω → } {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 : } (ω : Ω) :
theorem measure_theory.upper_crossing_time_le {Ω : Type u_1} {ι : Type u_2} [conditionally_complete_linear_order_bot ι] {a b : } {f : ι → Ω → } {N : ι} {n : } {ω : Ω} :
@[simp]
theorem measure_theory.upper_crossing_time_zero' {Ω : Type u_1} {ι : Type u_2} [conditionally_complete_linear_order_bot ι] {a b : } {f : ι → Ω → } {n : } {ω : Ω} :
theorem measure_theory.lower_crossing_time_le {Ω : Type u_1} {ι : Type u_2} [conditionally_complete_linear_order_bot ι] {a b : } {f : ι → Ω → } {N : ι} {n : } {ω : Ω} :
theorem measure_theory.upper_crossing_time_le_lower_crossing_time {Ω : Type u_1} {ι : Type u_2} [conditionally_complete_linear_order_bot ι] {a b : } {f : ι → Ω → } {N : ι} {n : } {ω : Ω} :
theorem measure_theory.lower_crossing_time_le_upper_crossing_time_succ {Ω : Type u_1} {ι : Type u_2} [conditionally_complete_linear_order_bot ι] {a b : } {f : ι → Ω → } {N : ι} {n : } {ω : Ω} :
theorem measure_theory.lower_crossing_time_mono {Ω : Type u_1} {ι : Type u_2} [conditionally_complete_linear_order_bot ι] {a b : } {f : ι → Ω → } {N : ι} {n m : } {ω : Ω} (hnm : n m) :
theorem measure_theory.upper_crossing_time_mono {Ω : Type u_1} {ι : Type u_2} [conditionally_complete_linear_order_bot ι] {a b : } {f : ι → Ω → } {N : ι} {n m : } {ω : Ω} (hnm : n m) :
theorem measure_theory.stopped_value_lower_crossing_time {Ω : Type u_1} {a b : } {f : Ω → } {N n : } {ω : Ω} (h : measure_theory.lower_crossing_time a b f N n ω N) :
theorem measure_theory.stopped_value_upper_crossing_time {Ω : Type u_1} {a b : } {f : Ω → } {N n : } {ω : Ω} (h : measure_theory.upper_crossing_time a b f N (n + 1) ω N) :
theorem measure_theory.upper_crossing_time_lt_lower_crossing_time {Ω : Type u_1} {a b : } {f : Ω → } {N n : } {ω : Ω} (hab : a < b) (hn : measure_theory.lower_crossing_time a b f N (n + 1) ω N) :
theorem measure_theory.lower_crossing_time_lt_upper_crossing_time {Ω : Type u_1} {a b : } {f : Ω → } {N n : } {ω : Ω} (hab : a < b) (hn : measure_theory.upper_crossing_time a b f N (n + 1) ω N) :
theorem measure_theory.upper_crossing_time_lt_succ {Ω : Type u_1} {a b : } {f : Ω → } {N n : } {ω : Ω} (hab : a < b) (hn : measure_theory.upper_crossing_time a b f N (n + 1) ω N) :
theorem measure_theory.lower_crossing_time_stabilize {Ω : Type u_1} {a b : } {f : Ω → } {N n m : } {ω : Ω} (hnm : n m) (hn : measure_theory.lower_crossing_time a b f N n ω = N) :
theorem measure_theory.upper_crossing_time_stabilize {Ω : Type u_1} {a b : } {f : Ω → } {N n m : } {ω : Ω} (hnm : n m) (hn : measure_theory.upper_crossing_time a b f N n ω = N) :
theorem measure_theory.lower_crossing_time_stabilize' {Ω : Type u_1} {a b : } {f : Ω → } {N n m : } {ω : Ω} (hnm : n m) (hn : N measure_theory.lower_crossing_time a b f N n ω) :
theorem measure_theory.upper_crossing_time_stabilize' {Ω : Type u_1} {a b : } {f : Ω → } {N n m : } {ω : Ω} (hnm : n m) (hn : N measure_theory.upper_crossing_time a b f N n ω) :
theorem measure_theory.exists_upper_crossing_time_eq {Ω : Type u_1} {a b : } (f : Ω → ) (N : ) (ω : Ω) (hab : a < b) :
∃ (n : ), measure_theory.upper_crossing_time a b f N n ω = N
theorem measure_theory.upper_crossing_time_lt_bdd_above {Ω : Type u_1} {a b : } {f : Ω → } {N : } {ω : Ω} (hab : a < b) :
theorem measure_theory.upper_crossing_time_lt_nonempty {Ω : Type u_1} {a b : } {f : Ω → } {N : } {ω : Ω} (hN : 0 < N) :
theorem measure_theory.upper_crossing_time_bound_eq {Ω : Type u_1} {a b : } (f : Ω → ) (N : ) (ω : Ω) (hab : a < b) :
theorem measure_theory.upper_crossing_time_eq_of_bound_le {Ω : Type u_1} {a b : } {f : Ω → } {N n : } {ω : Ω} (hab : a < b) (hn : N n) :
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 : } {ω : Ω} :
theorem measure_theory.upcrossing_strat_le_one {Ω : Type u_1} {a b : } {f : Ω → } {N n : } {ω : Ω} :
theorem measure_theory.submartingale.sum_upcrossing_strat_mul {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {f : Ω → } {ℱ : measure_theory.filtration m0} [measure_theory.is_finite_measure μ] (hf : measure_theory.submartingale f μ) (a b : ) (N : ) :
measure_theory.submartingale (λ (n : ), (finset.range n).sum (λ (k : ), measure_theory.upcrossing_strat a b f N 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 : Ω → } {ℱ : measure_theory.filtration m0} [measure_theory.is_finite_measure μ] (hf : measure_theory.submartingale f μ) (a b : ) (N : ) :
measure_theory.submartingale (λ (n : ), (finset.range n).sum (λ (k : ), (1 - measure_theory.upcrossing_strat a b f N 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 : } {ℱ : measure_theory.filtration m0} [measure_theory.is_finite_measure μ] (hf : measure_theory.submartingale f μ) :
(x : Ω), (finset.range n).sum (λ (k : ), measure_theory.upcrossing_strat a b f N 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 : Ω → } {ω : Ω} :
@[simp]
theorem measure_theory.upcrossings_before_zero' {Ω : Type u_1} {a b : } {f : Ω → } :
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 measure_theory.upcrossings_before a b f N ω) :
theorem measure_theory.upper_crossing_time_eq_of_upcrossings_before_lt {Ω : Type u_1} {a b : } {f : Ω → } {N n : } {ω : Ω} (hab : a < b) (hn : measure_theory.upcrossings_before a b f N ω < n) :
theorem measure_theory.upcrossings_before_le {Ω : Type u_1} {a b : } {N : } (f : Ω → ) (ω : Ω) (hab : a < b) :
theorem measure_theory.crossing_eq_crossing_of_lower_crossing_time_lt {Ω : Type u_1} {a b : } {f : Ω → } {N n : } {ω : Ω} {M : } (hNM : N M) (h : measure_theory.lower_crossing_time a b f 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 : measure_theory.upper_crossing_time a b f N (n + 1) ω < 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 : measure_theory.upper_crossing_time a b f N n ω < N) :
theorem measure_theory.upcrossings_before_mono {Ω : Type u_1} {a b : } {f : Ω → } (hab : a < b) :
monotone (λ (N : ) (ω : Ω), measure_theory.upcrossings_before a b f 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₂ ω) :
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 < measure_theory.upcrossings_before a b f 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 < measure_theory.upcrossings_before a b f N ω) :
theorem measure_theory.sub_eq_zero_of_upcrossings_before_lt {Ω : Type u_1} {a b : } {f : Ω → } {N n : } {ω : Ω} (hab : a < b) (hn : measure_theory.upcrossings_before a b f N ω < n) :
theorem measure_theory.mul_upcrossings_before_le {Ω : Type u_1} {a b : } {f : Ω → } {N : } {ω : Ω} (hf : a f N ω) (hab : a < b) :
(b - a) * (measure_theory.upcrossings_before a b f N ω) (finset.range N).sum (λ (k : ), measure_theory.upcrossing_strat a b f N 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 : } {ℱ : measure_theory.filtration m0} [measure_theory.is_finite_measure μ] (hf : measure_theory.submartingale f μ) (hfN : ∀ (ω : Ω), a f N ω) (hfzero : 0 f 0) (hab : a < b) :
(b - a) * (x : Ω), (measure_theory.upcrossings_before a b f N x) μ (x : Ω), f N x μ
theorem measure_theory.crossing_pos_eq {Ω : Type u_1} {a b : } {f : Ω → } {N n : } (hab : a < b) :
measure_theory.upper_crossing_time 0 (b - a) (λ (n : ) (ω : Ω), (f n ω - a)) N n = measure_theory.upper_crossing_time a b f N n measure_theory.lower_crossing_time 0 (b - a) (λ (n : ) (ω : Ω), (f n ω - a)) N n = measure_theory.lower_crossing_time a b f N n
theorem measure_theory.upcrossings_before_pos_eq {Ω : Type u_1} {a b : } {f : Ω → } {N : } {ω : Ω} (hab : a < b) :
measure_theory.upcrossings_before 0 (b - a) (λ (n : ) (ω : Ω), (f n ω - a)) N ω = measure_theory.upcrossings_before a b f 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 : } {ℱ : measure_theory.filtration m0} [measure_theory.is_finite_measure μ] (hf : measure_theory.submartingale f μ) (hab : a < b) :
(b - a) * (x : Ω), (measure_theory.upcrossings_before a b f N 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 : Ω → } {ℱ : measure_theory.filtration m0} [measure_theory.is_finite_measure μ] (a b : ) (hf : measure_theory.submartingale f μ) (N : ) :
(b - a) * (x : Ω), (measure_theory.upcrossings_before a b f N 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) :
measure_theory.upcrossings_before a b f N ω = (finset.Ico 1 (N + 1)).sum (λ (i : ), {n : | measure_theory.upper_crossing_time a b f N n ω < N}.indicator 1 i)
theorem measure_theory.adapted.measurable_upcrossings_before {Ω : Type u_1} {m0 : measurable_space Ω} {a b : } {f : Ω → } {N : } {ℱ : measure_theory.filtration m0} (hf : measure_theory.adapted f) (hab : a < b) :
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 : Ω → } {ℱ : measure_theory.filtration m0} (hf : measure_theory.adapted f) (hab : a < b) :
theorem measure_theory.upcrossings_lt_top_iff {Ω : Type u_1} {a b : } {f : Ω → } {ω : Ω} :
measure_theory.upcrossings a b f ω < ∃ (k : ), ∀ (N : ), measure_theory.upcrossings_before a b f N ω k

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