# mathlib3documentation

probability.martingale.optional_stopping

# Optional stopping theorem (fair game theorem) #

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

The optional stopping theorem states that an adapted integrable process f is a submartingale if and only if for all bounded stopping times τ and π such that τ ≤ π, the stopped value of f at τ has expectation smaller than its stopped value at π.

This file also contains Doob's maximal inequality: given a non-negative submartingale f, for all ε : ℝ≥0, we have ε • μ {ε ≤ f* n} ≤ ∫ ω in {ε ≤ f* n}, f n where f* n ω = max_{k ≤ n}, f k ω.

### Main results #

• measure_theory.submartingale_iff_expected_stopped_value_mono: the optional stopping theorem.
• measure_theory.submartingale.stopped_process: the stopped process of a submartingale with respect to a stopping time is a submartingale.
• measure_theory.maximal_ineq: Doob's maximal inequality.
theorem measure_theory.submartingale.expected_stopped_value_mono {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : m0} {f : Ω } {τ π : Ω } (hf : μ) (hτ : τ) (hπ : π) (hle : τ π) {N : } (hbdd : (ω : Ω), π ω N) :
(x : Ω), μ (x : Ω), μ

Given a submartingale f and bounded stopping times τ and π such that τ ≤ π, the expectation of stopped_value f τ is less than or equal to the expectation of stopped_value f π. This is the forward direction of the optional stopping theorem.

theorem measure_theory.submartingale_of_expected_stopped_value_mono {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : m0} {f : Ω } (hadp : f) (hint : (i : ), μ) (hf : (τ π : Ω ), τ π ( (N : ), (ω : Ω), π ω N) (x : Ω), μ (x : Ω), μ) :

The converse direction of the optional stopping theorem, i.e. an adapted integrable process f is a submartingale if for all bounded stopping times τ and π such that τ ≤ π, the stopped value of f at τ has expectation smaller than its stopped value at π.

theorem measure_theory.submartingale_iff_expected_stopped_value_mono {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : m0} {f : Ω } (hadp : f) (hint : (i : ), μ) :
(τ π : Ω ), τ π ( (N : ), (x : Ω), π x N) (x : Ω), μ (x : Ω), μ

The optional stopping theorem (fair game theorem): an adapted integrable process f is a submartingale if and only if for all bounded stopping times τ and π such that τ ≤ π, the stopped value of f at τ has expectation smaller than its stopped value at π.

@[protected]
theorem measure_theory.submartingale.stopped_process {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : m0} {f : Ω } {τ : Ω } (h : μ) (hτ : τ) :

The stopped process of a submartingale with respect to a stopping time is a submartingale.

theorem measure_theory.smul_le_stopped_value_hitting {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : m0} {f : Ω } (hsub : μ) {ε : nnreal} (n : ) :
ε μ {ω : Ω | ε (λ (k : ), f k ω)} ennreal.of_real ( (ω : Ω) in {ω : Ω | ε (λ (k : ), f k ω)}, {y : | ε y} 0 n) ω μ)
theorem measure_theory.maximal_ineq {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : m0} {f : Ω } (hsub : μ) (hnonneg : 0 f) {ε : nnreal} (n : ) :
ε μ {ω : Ω | ε (λ (k : ), f k ω)} ennreal.of_real ( (ω : Ω) in {ω : Ω | ε (λ (k : ), f k ω)}, f n ω μ)

Doob's maximal inequality: Given a non-negative submartingale f, for all ε : ℝ≥0, we have ε • μ {ε ≤ f* n} ≤ ∫ ω in {ε ≤ f* n}, f n where f* n ω = max_{k ≤ n}, f k ω.

In some literature, the Doob's maximal inequality refers to what we call Doob's Lp inequality (which is a corollary of this lemma and will be proved in an upcomming PR).