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 #

Main results #

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
Instances For
    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
    Instances For
      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
      Instances For
        @[simp]
        theorem MeasureTheory.upperCrossingTime_zero {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [OrderBot ι] [InfSet ι] {a : } {b : } {f : ιΩ} {N : ι} :
        @[simp]
        theorem MeasureTheory.lowerCrossingTime_zero {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [OrderBot ι] [InfSet ι] {a : } {b : } {f : ιΩ} {N : ι} :
        theorem MeasureTheory.upperCrossingTime_succ {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [OrderBot ι] [InfSet ι] {a : } {b : } {f : ιΩ} {N : ι} {n : } {ω : Ω} :
        theorem MeasureTheory.upperCrossingTime_succ_eq {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [OrderBot ι] [InfSet ι] {a : } {b : } {f : ιΩ} {N : ι} {n : } (ω : Ω) :
        theorem MeasureTheory.upperCrossingTime_le {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrderBot ι] {a : } {b : } {f : ιΩ} {N : ι} {n : } {ω : Ω} :
        @[simp]
        theorem MeasureTheory.upperCrossingTime_zero' {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrderBot ι] {a : } {b : } {f : ιΩ} {n : } {ω : Ω} :
        theorem MeasureTheory.lowerCrossingTime_le {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrderBot ι] {a : } {b : } {f : ιΩ} {N : ι} {n : } {ω : Ω} :
        theorem MeasureTheory.upperCrossingTime_le_lowerCrossingTime {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrderBot ι] {a : } {b : } {f : ιΩ} {N : ι} {n : } {ω : Ω} :
        theorem MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrderBot ι] {a : } {b : } {f : ιΩ} {N : ι} {n : } {ω : Ω} :
        theorem MeasureTheory.lowerCrossingTime_mono {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrderBot ι] {a : } {b : } {f : ιΩ} {N : ι} {n : } {m : } {ω : Ω} (hnm : n m) :
        theorem MeasureTheory.upperCrossingTime_mono {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrderBot ι] {a : } {b : } {f : ιΩ} {N : ι} {n : } {m : } {ω : Ω} (hnm : n m) :
        theorem MeasureTheory.stoppedValue_lowerCrossingTime {Ω : Type u_1} {a : } {b : } {f : Ω} {N : } {n : } {ω : Ω} (h : MeasureTheory.lowerCrossingTime a b f N n ω N) :
        theorem MeasureTheory.stoppedValue_upperCrossingTime {Ω : Type u_1} {a : } {b : } {f : Ω} {N : } {n : } {ω : Ω} (h : MeasureTheory.upperCrossingTime a b f N (n + 1) ω N) :
        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) :
        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) :
        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) :
        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) :
        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) :
        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 ω) :
        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 ω) :
        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) :
        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) :
        theorem MeasureTheory.upperCrossingTime_eq_of_bound_le {Ω : Type u_1} {a : } {b : } {f : Ω} {N : } {n : } {ω : Ω} (hab : a < b) (hn : 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.
        Instances For
          theorem MeasureTheory.upcrossingStrat_nonneg {Ω : Type u_1} {a : } {b : } {f : Ω} {N : } {n : } {ω : Ω} :
          theorem MeasureTheory.upcrossingStrat_le_one {Ω : Type u_1} {a : } {b : } {f : Ω} {N : } {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 : ) => kFinset.range n, 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 : ) => kFinset.range n, (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 : Ω), (∑ kFinset.range n, 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
          Instances For
            @[simp]
            theorem MeasureTheory.upcrossingsBefore_bot {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [OrderBot ι] [InfSet ι] {a : } {b : } {f : ιΩ} {ω : Ω} :
            theorem MeasureTheory.upcrossingsBefore_zero {Ω : Type u_1} {a : } {b : } {f : Ω} {ω : Ω} :
            @[simp]
            theorem MeasureTheory.upcrossingsBefore_zero' {Ω : Type u_1} {a : } {b : } {f : Ω} :
            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 ω) :
            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) :
            theorem MeasureTheory.upcrossingsBefore_le {Ω : Type u_1} {a : } {b : } {N : } (f : Ω) (ω : Ω) (hab : a < b) :
            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) :
            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) :
            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) :
            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₂ ω) :
            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 ω) :
            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 ω) :
            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) :
            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 ω) kFinset.range N, 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 ω = iFinset.Ico 1 (N + 1), {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) :
            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 : ιΩ) (ω : Ω) :

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

            Equations
            Instances For
              theorem MeasureTheory.Adapted.measurable_upcrossings {Ω : Type u_1} {m0 : MeasurableSpace Ω} {a : } {b : } {f : Ω} {ℱ : MeasureTheory.Filtration m0} (hf : MeasureTheory.Adapted f) (hab : a < b) :
              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.