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.

References

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

Proof outline

In this section, we will denote by $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 lowerCrossingTime and upperCrossingTime in our formalization which are defined using MeasureTheory.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 MeasureTheory.integral_mul_upcrossingsBefore_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 MeasureTheory.lowerCrossingTimeAux {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [InfSet ι] (a : ℝ) (f : ι → Ω → ℝ) (c : ι) (N : ι) : Ω → ι

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

Equations

• MeasureTheory.lowerCrossingTimeAux a f c N = MeasureTheory.hitting f (Set.Iic a) c N

noncomputable def MeasureTheory.upperCrossingTime {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [OrderBot ι] [InfSet ι] (a : ℝ) (b : ℝ) (f : ι → Ω → ℝ) (N : ι) : ℕ → Ω → ι

upperCrossingTime 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

• One or more equations did not get rendered due to their size.
• MeasureTheory.upperCrossingTime a b f N 0 = ⊥

noncomputable def MeasureTheory.lowerCrossingTime {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [OrderBot ι] [InfSet ι] (a : ℝ) (b : ℝ) (f : ι → Ω → ℝ) (N : ι) (n : ℕ) : Ω → ι

lowerCrossingTime 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

• MeasureTheory.lowerCrossingTime a b f N n ω = MeasureTheory.hitting f (Set.Iic a) (MeasureTheory.upperCrossingTime a b f N n ω) N ω

@[simp]

theorem MeasureTheory.upperCrossingTime_zero {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [OrderBot ι] [InfSet ι] {a : ℝ} {b : ℝ} {f : ι → Ω → ℝ} {N : ι} : MeasureTheory.upperCrossingTime a b f N 0 = ⊥

@[simp]

theorem MeasureTheory.lowerCrossingTime_zero {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [OrderBot ι] [InfSet ι] {a : ℝ} {b : ℝ} {f : ι → Ω → ℝ} {N : ι} : MeasureTheory.lowerCrossingTime a b f N 0 = MeasureTheory.hitting f (Set.Iic a) ⊥ N

theorem MeasureTheory.upperCrossingTime_succ {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [OrderBot ι] [InfSet ι] {a : ℝ} {b : ℝ} {f : ι → Ω → ℝ} {N : ι} {n : ℕ} {ω : Ω} : MeasureTheory.upperCrossingTime a b f N (n + 1) ω = MeasureTheory.hitting f (Set.Ici b) (MeasureTheory.lowerCrossingTimeAux a f (MeasureTheory.upperCrossingTime a b f N n ω) N ω) N ω

theorem MeasureTheory.upperCrossingTime_succ_eq {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [OrderBot ι] [InfSet ι] {a : ℝ} {b : ℝ} {f : ι → Ω → ℝ} {N : ι} {n : ℕ} (ω : Ω) : MeasureTheory.upperCrossingTime a b f N (n + 1) ω = MeasureTheory.hitting f (Set.Ici b) (MeasureTheory.lowerCrossingTime a b f N n ω) N ω

theorem MeasureTheory.upperCrossingTime_le {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrderBot ι] {a : ℝ} {b : ℝ} {f : ι → Ω → ℝ} {N : ι} {n : ℕ} {ω : Ω} : MeasureTheory.upperCrossingTime a b f N n ω ≤ N

@[simp]

theorem MeasureTheory.upperCrossingTime_zero' {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrderBot ι] {a : ℝ} {b : ℝ} {f : ι → Ω → ℝ} {n : ℕ} {ω : Ω} : MeasureTheory.upperCrossingTime a b f ⊥ n ω = ⊥

theorem MeasureTheory.lowerCrossingTime_le {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrderBot ι] {a : ℝ} {b : ℝ} {f : ι → Ω → ℝ} {N : ι} {n : ℕ} {ω : Ω} : MeasureTheory.lowerCrossingTime a b f N n ω ≤ N

theorem MeasureTheory.upperCrossingTime_le_lowerCrossingTime {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrderBot ι] {a : ℝ} {b : ℝ} {f : ι → Ω → ℝ} {N : ι} {n : ℕ} {ω : Ω} : MeasureTheory.upperCrossingTime a b f N n ω ≤ MeasureTheory.lowerCrossingTime a b f N n ω

theorem MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrderBot ι] {a : ℝ} {b : ℝ} {f : ι → Ω → ℝ} {N : ι} {n : ℕ} {ω : Ω} : MeasureTheory.lowerCrossingTime a b f N n ω ≤ MeasureTheory.upperCrossingTime a b f N (n + 1) ω

theorem MeasureTheory.lowerCrossingTime_mono {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrderBot ι] {a : ℝ} {b : ℝ} {f : ι → Ω → ℝ} {N : ι} {n : ℕ} {m : ℕ} {ω : Ω} (hnm : n ≤ m) : MeasureTheory.lowerCrossingTime a b f N n ω ≤ MeasureTheory.lowerCrossingTime a b f N m ω

theorem MeasureTheory.upperCrossingTime_mono {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrderBot ι] {a : ℝ} {b : ℝ} {f : ι → Ω → ℝ} {N : ι} {n : ℕ} {m : ℕ} {ω : Ω} (hnm : n ≤ m) : MeasureTheory.upperCrossingTime a b f N n ω ≤ MeasureTheory.upperCrossingTime a b f N m ω

theorem MeasureTheory.stoppedValue_lowerCrossingTime {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ω : Ω} (h : MeasureTheory.lowerCrossingTime a b f N n ω ≠ N) : MeasureTheory.stoppedValue f (MeasureTheory.lowerCrossingTime a b f N n) ω ≤ a

theorem MeasureTheory.stoppedValue_upperCrossingTime {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ω : Ω} (h : MeasureTheory.upperCrossingTime a b f N (n + 1) ω ≠ N) : b ≤ MeasureTheory.stoppedValue f (MeasureTheory.upperCrossingTime a b f N (n + 1)) ω

theorem MeasureTheory.upperCrossingTime_lt_lowerCrossingTime {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ω : Ω} (hab : a < b) (hn : MeasureTheory.lowerCrossingTime a b f N (n + 1) ω ≠ N) : MeasureTheory.upperCrossingTime a b f N (n + 1) ω < MeasureTheory.lowerCrossingTime a b f N (n + 1) ω

theorem MeasureTheory.lowerCrossingTime_lt_upperCrossingTime {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ω : Ω} (hab : a < b) (hn : MeasureTheory.upperCrossingTime a b f N (n + 1) ω ≠ N) : MeasureTheory.lowerCrossingTime a b f N n ω < MeasureTheory.upperCrossingTime a b f N (n + 1) ω

theorem MeasureTheory.upperCrossingTime_lt_succ {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ω : Ω} (hab : a < b) (hn : MeasureTheory.upperCrossingTime a b f N (n + 1) ω ≠ N) : MeasureTheory.upperCrossingTime a b f N n ω < MeasureTheory.upperCrossingTime a b f N (n + 1) ω

theorem MeasureTheory.lowerCrossingTime_stabilize {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {m : ℕ} {ω : Ω} (hnm : n ≤ m) (hn : MeasureTheory.lowerCrossingTime a b f N n ω = N) : MeasureTheory.lowerCrossingTime a b f N m ω = N

theorem MeasureTheory.upperCrossingTime_stabilize {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {m : ℕ} {ω : Ω} (hnm : n ≤ m) (hn : MeasureTheory.upperCrossingTime a b f N n ω = N) : MeasureTheory.upperCrossingTime a b f N m ω = N

theorem MeasureTheory.lowerCrossingTime_stabilize' {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {m : ℕ} {ω : Ω} (hnm : n ≤ m) (hn : N ≤ MeasureTheory.lowerCrossingTime a b f N n ω) : MeasureTheory.lowerCrossingTime a b f N m ω = N

theorem MeasureTheory.upperCrossingTime_stabilize' {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {m : ℕ} {ω : Ω} (hnm : n ≤ m) (hn : N ≤ MeasureTheory.upperCrossingTime a b f N n ω) : MeasureTheory.upperCrossingTime a b f N m ω = N

theorem MeasureTheory.exists_upperCrossingTime_eq {Ω : Type u_1} {a : ℝ} {b : ℝ} (f : ℕ → Ω → ℝ) (N : ℕ) (ω : Ω) (hab : a < b) : ∃ (n : ℕ), MeasureTheory.upperCrossingTime a b f N n ω = N

theorem MeasureTheory.upperCrossingTime_lt_bddAbove {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ω : Ω} (hab : a < b) : BddAbove {n : ℕ | MeasureTheory.upperCrossingTime a b f N n ω < N}

theorem MeasureTheory.upperCrossingTime_lt_nonempty {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ω : Ω} (hN : 0 < N) : {n : ℕ | MeasureTheory.upperCrossingTime a b f N n ω < N}.Nonempty

theorem MeasureTheory.upperCrossingTime_bound_eq {Ω : Type u_1} {a : ℝ} {b : ℝ} (f : ℕ → Ω → ℝ) (N : ℕ) (ω : Ω) (hab : a < b) : MeasureTheory.upperCrossingTime a b f N N ω = N

theorem MeasureTheory.upperCrossingTime_eq_of_bound_le {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ω : Ω} (hab : a < b) (hn : N ≤ n) : MeasureTheory.upperCrossingTime a b f N n ω = N

theorem MeasureTheory.Adapted.isStoppingTime_crossing {Ω : Type u_1} {m0 : MeasurableSpace Ω} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ℱ : MeasureTheory.Filtration ℕ m0} (hf : MeasureTheory.Adapted ℱ f) : MeasureTheory.IsStoppingTime ℱ (MeasureTheory.upperCrossingTime a b f N n) ∧ MeasureTheory.IsStoppingTime ℱ (MeasureTheory.lowerCrossingTime a b f N n)

theorem MeasureTheory.Adapted.isStoppingTime_upperCrossingTime {Ω : Type u_1} {m0 : MeasurableSpace Ω} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ℱ : MeasureTheory.Filtration ℕ m0} (hf : MeasureTheory.Adapted ℱ f) : MeasureTheory.IsStoppingTime ℱ (MeasureTheory.upperCrossingTime a b f N n)

theorem MeasureTheory.Adapted.isStoppingTime_lowerCrossingTime {Ω : Type u_1} {m0 : MeasurableSpace Ω} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ℱ : MeasureTheory.Filtration ℕ m0} (hf : MeasureTheory.Adapted ℱ f) : MeasureTheory.IsStoppingTime ℱ (MeasureTheory.lowerCrossingTime a b f N n)

noncomputable def MeasureTheory.upcrossingStrat {Ω : Type u_1} (a : ℝ) (b : ℝ) (f : ℕ → Ω → ℝ) (N : ℕ) (n : ℕ) (ω : Ω) : ℝ

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

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.upcrossingStrat_nonneg {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ω : Ω} : 0 ≤ MeasureTheory.upcrossingStrat a b f N n ω

theorem MeasureTheory.upcrossingStrat_le_one {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ω : Ω} : MeasureTheory.upcrossingStrat a b f N n ω ≤ 1

theorem MeasureTheory.Adapted.upcrossingStrat_adapted {Ω : Type u_1} {m0 : MeasurableSpace Ω} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ℱ : MeasureTheory.Filtration ℕ m0} (hf : MeasureTheory.Adapted ℱ f) : MeasureTheory.Adapted ℱ (MeasureTheory.upcrossingStrat a b f N)

theorem MeasureTheory.Submartingale.sum_upcrossingStrat_mul {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ℕ → Ω → ℝ} {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f ℱ μ) (a : ℝ) (b : ℝ) (N : ℕ) : MeasureTheory.Submartingale (fun (n : ℕ) => (Finset.range n).sum fun (k : ℕ) => MeasureTheory.upcrossingStrat a b f N k * (f (k + 1) - f k)) ℱ μ

theorem MeasureTheory.Submartingale.sum_sub_upcrossingStrat_mul {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ℕ → Ω → ℝ} {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f ℱ μ) (a : ℝ) (b : ℝ) (N : ℕ) : MeasureTheory.Submartingale (fun (n : ℕ) => (Finset.range n).sum fun (k : ℕ) => (1 - MeasureTheory.upcrossingStrat a b f N k) * (f (k + 1) - f k)) ℱ μ

theorem MeasureTheory.Submartingale.sum_mul_upcrossingStrat_le {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f ℱ μ) : ∫ (x : Ω), (Finset.range n).sum (fun (k : ℕ) => MeasureTheory.upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤ ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ

noncomputable def MeasureTheory.upcrossingsBefore {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [OrderBot ι] [InfSet ι] (a : ℝ) (b : ℝ) (f : ι → Ω → ℝ) (N : ι) (ω : Ω) : ℕ

The number of upcrossings (strictly) before time N.

Equations

• MeasureTheory.upcrossingsBefore a b f N ω = sSup {n : ℕ | MeasureTheory.upperCrossingTime a b f N n ω < N}

@[simp]

theorem MeasureTheory.upcrossingsBefore_bot {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [OrderBot ι] [InfSet ι] {a : ℝ} {b : ℝ} {f : ι → Ω → ℝ} {ω : Ω} : MeasureTheory.upcrossingsBefore a b f ⊥ ω = ⊥

theorem MeasureTheory.upcrossingsBefore_zero {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {ω : Ω} : MeasureTheory.upcrossingsBefore a b f 0 ω = 0

@[simp]

theorem MeasureTheory.upcrossingsBefore_zero' {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} : MeasureTheory.upcrossingsBefore a b f 0 = 0

theorem MeasureTheory.upperCrossingTime_lt_of_le_upcrossingsBefore {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ω : Ω} (hN : 0 < N) (hab : a < b) (hn : n ≤ MeasureTheory.upcrossingsBefore a b f N ω) : MeasureTheory.upperCrossingTime a b f N n ω < N

theorem MeasureTheory.upperCrossingTime_eq_of_upcrossingsBefore_lt {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ω : Ω} (hab : a < b) (hn : MeasureTheory.upcrossingsBefore a b f N ω < n) : MeasureTheory.upperCrossingTime a b f N n ω = N

theorem MeasureTheory.upcrossingsBefore_le {Ω : Type u_1} {a : ℝ} {b : ℝ} {N : ℕ} (f : ℕ → Ω → ℝ) (ω : Ω) (hab : a < b) : MeasureTheory.upcrossingsBefore a b f N ω ≤ N

theorem MeasureTheory.crossing_eq_crossing_of_lowerCrossingTime_lt {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ω : Ω} {M : ℕ} (hNM : N ≤ M) (h : MeasureTheory.lowerCrossingTime a b f N n ω < N) : MeasureTheory.upperCrossingTime a b f M n ω = MeasureTheory.upperCrossingTime a b f N n ω ∧ MeasureTheory.lowerCrossingTime a b f M n ω = MeasureTheory.lowerCrossingTime a b f N n ω

theorem MeasureTheory.crossing_eq_crossing_of_upperCrossingTime_lt {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ω : Ω} {M : ℕ} (hNM : N ≤ M) (h : MeasureTheory.upperCrossingTime a b f N (n + 1) ω < N) : MeasureTheory.upperCrossingTime a b f M (n + 1) ω = MeasureTheory.upperCrossingTime a b f N (n + 1) ω ∧ MeasureTheory.lowerCrossingTime a b f M n ω = MeasureTheory.lowerCrossingTime a b f N n ω

theorem MeasureTheory.upperCrossingTime_eq_upperCrossingTime_of_lt {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ω : Ω} {M : ℕ} (hNM : N ≤ M) (h : MeasureTheory.upperCrossingTime a b f N n ω < N) : MeasureTheory.upperCrossingTime a b f M n ω = MeasureTheory.upperCrossingTime a b f N n ω

theorem MeasureTheory.upcrossingsBefore_mono {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} (hab : a < b) : Monotone fun (N : ℕ) (ω : Ω) => MeasureTheory.upcrossingsBefore a b f N ω

theorem MeasureTheory.upcrossingsBefore_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₂ ω) : MeasureTheory.upcrossingsBefore a b f N ω < MeasureTheory.upcrossingsBefore a b f (N₂ + 1) ω

theorem MeasureTheory.lowerCrossingTime_lt_of_lt_upcrossingsBefore {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ω : Ω} (hN : 0 < N) (hab : a < b) (hn : n < MeasureTheory.upcrossingsBefore a b f N ω) : MeasureTheory.lowerCrossingTime a b f N n ω < N

theorem MeasureTheory.le_sub_of_le_upcrossingsBefore {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ω : Ω} (hN : 0 < N) (hab : a < b) (hn : n < MeasureTheory.upcrossingsBefore a b f N ω) : b - a ≤ MeasureTheory.stoppedValue f (MeasureTheory.upperCrossingTime a b f N (n + 1)) ω - MeasureTheory.stoppedValue f (MeasureTheory.lowerCrossingTime a b f N n) ω

theorem MeasureTheory.sub_eq_zero_of_upcrossingsBefore_lt {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} {ω : Ω} (hab : a < b) (hn : MeasureTheory.upcrossingsBefore a b f N ω < n) : MeasureTheory.stoppedValue f (MeasureTheory.upperCrossingTime a b f N (n + 1)) ω - MeasureTheory.stoppedValue f (MeasureTheory.lowerCrossingTime a b f N n) ω = 0

theorem MeasureTheory.mul_upcrossingsBefore_le {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ω : Ω} (hf : a ≤ f N ω) (hab : a < b) : (b - a) * ↑(MeasureTheory.upcrossingsBefore a b f N ω) ≤ (Finset.range N).sum fun (k : ℕ) => MeasureTheory.upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω

theorem MeasureTheory.integral_mul_upcrossingsBefore_le_integral {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f ℱ μ) (hfN : ∀ (ω : Ω), a ≤ f N ω) (hfzero : 0 ≤ f 0) (hab : a < b) : (b - a) * ∫ (x : Ω), ↑(MeasureTheory.upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), f N x ∂μ

theorem MeasureTheory.crossing_pos_eq {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n : ℕ} (hab : a < b) : MeasureTheory.upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) => (f n ω - a)⁺) N n = MeasureTheory.upperCrossingTime a b f N n ∧ MeasureTheory.lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) => (f n ω - a)⁺) N n = MeasureTheory.lowerCrossingTime a b f N n

theorem MeasureTheory.upcrossingsBefore_pos_eq {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ω : Ω} (hab : a < b) : MeasureTheory.upcrossingsBefore 0 (b - a) (fun (n : ℕ) (ω : Ω) => (f n ω - a)⁺) N ω = MeasureTheory.upcrossingsBefore a b f N ω

theorem MeasureTheory.mul_integral_upcrossingsBefore_le_integral_pos_part_aux {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f ℱ μ) (hab : a < b) : (b - a) * ∫ (x : Ω), ↑(MeasureTheory.upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) => (f N ω - a)⁺) x ∂μ

theorem MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ℕ → Ω → ℝ} {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ] (a : ℝ) (b : ℝ) (hf : MeasureTheory.Submartingale f ℱ μ) (N : ℕ) : (b - a) * ∫ (x : Ω), ↑(MeasureTheory.upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) => (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) * 𝔼[upcrossingsBefore a b f N] ≤ 𝔼[(f N - a)⁺] where upcrossingsBefore 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 MeasureTheory.upcrossingsBefore_eq_sum {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ω : Ω} (hab : a < b) : MeasureTheory.upcrossingsBefore a b f N ω = (Finset.Ico 1 (N + 1)).sum fun (i : ℕ) => {n : ℕ | MeasureTheory.upperCrossingTime a b f N n ω < N}.indicator 1 i

theorem MeasureTheory.Adapted.measurable_upcrossingsBefore {Ω : Type u_1} {m0 : MeasurableSpace Ω} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ℱ : MeasureTheory.Filtration ℕ m0} (hf : MeasureTheory.Adapted ℱ f) (hab : a < b) : Measurable (MeasureTheory.upcrossingsBefore a b f N)

theorem MeasureTheory.Adapted.integrable_upcrossingsBefore {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Adapted ℱ f) (hab : a < b) : MeasureTheory.Integrable (fun (ω : Ω) => ↑(MeasureTheory.upcrossingsBefore a b f N ω)) μ

noncomputable def MeasureTheory.upcrossings {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [OrderBot ι] [InfSet ι] (a : ℝ) (b : ℝ) (f : ι → Ω → ℝ) (ω : Ω) : ENNReal

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

Equations

• MeasureTheory.upcrossings a b f ω = ⨆ (N : ι), ↑(MeasureTheory.upcrossingsBefore a b f N ω)

theorem MeasureTheory.Adapted.measurable_upcrossings {Ω : Type u_1} {m0 : MeasurableSpace Ω} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {ℱ : MeasureTheory.Filtration ℕ m0} (hf : MeasureTheory.Adapted ℱ f) (hab : a < b) : Measurable (MeasureTheory.upcrossings a b f)

theorem MeasureTheory.upcrossings_lt_top_iff {Ω : Type u_1} {a : ℝ} {b : ℝ} {f : ℕ → Ω → ℝ} {ω : Ω} : MeasureTheory.upcrossings a b f ω < ⊤ ↔ ∃ (k : ℕ), ∀ (N : ℕ), MeasureTheory.upcrossingsBefore a b f N ω ≤ k

theorem MeasureTheory.Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ℕ → Ω → ℝ} {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ] (a : ℝ) (b : ℝ) (hf : MeasureTheory.Submartingale f ℱ μ) : ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), MeasureTheory.upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ

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