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.

source

theorem measure_theory.submartingale.expected_stopped_value_mono {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : measure_theory.filtration ℕ m0} {f : ℕ → Ω → ℝ} {τ π : Ω → ℕ} [measure_theory.sigma_finite_filtration μ 𝒢] (hf : measure_theory.submartingale f 𝒢 μ) (hτ : measure_theory.is_stopping_time 𝒢 τ) (hπ : measure_theory.is_stopping_time 𝒢 π) (hle : τ ≤ π) {N : ℕ} (hbdd : ∀ (ω : Ω), π ω ≤ N) :

∫ (x : Ω), measure_theory.stopped_value f τ x ∂μ ≤ ∫ (x : Ω), measure_theory.stopped_value f π 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.

source

theorem measure_theory.submartingale_of_expected_stopped_value_mono {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : measure_theory.filtration ℕ m0} {f : ℕ → Ω → ℝ} [measure_theory.is_finite_measure μ] (hadp : measure_theory.adapted 𝒢 f) (hint : ∀ (i : ℕ), measure_theory.integrable (f i) μ) (hf : ∀ (τ π : Ω → ℕ), measure_theory.is_stopping_time 𝒢 τ → measure_theory.is_stopping_time 𝒢 π → τ ≤ π → (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ N) → ∫ (x : Ω), measure_theory.stopped_value f τ x ∂μ ≤ ∫ (x : Ω), measure_theory.stopped_value f π x ∂μ) :

measure_theory.submartingale f 𝒢 μ

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 π.

source

theorem measure_theory.submartingale_iff_expected_stopped_value_mono {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : measure_theory.filtration ℕ m0} {f : ℕ → Ω → ℝ} [measure_theory.is_finite_measure μ] (hadp : measure_theory.adapted 𝒢 f) (hint : ∀ (i : ℕ), measure_theory.integrable (f i) μ) :

measure_theory.submartingale f 𝒢 μ ↔ ∀ (τ π : Ω → ℕ), measure_theory.is_stopping_time 𝒢 τ → measure_theory.is_stopping_time 𝒢 π → τ ≤ π → (∃ (N : ℕ), ∀ (x : Ω), π x ≤ N) → ∫ (x : Ω), measure_theory.stopped_value f τ x ∂μ ≤ ∫ (x : Ω), measure_theory.stopped_value f π 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 π.

source

@[protected]

theorem measure_theory.submartingale.stopped_process {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : measure_theory.filtration ℕ m0} {f : ℕ → Ω → ℝ} {τ : Ω → ℕ} [measure_theory.is_finite_measure μ] (h : measure_theory.submartingale f 𝒢 μ) (hτ : measure_theory.is_stopping_time 𝒢 τ) :

measure_theory.submartingale (measure_theory.stopped_process f τ) 𝒢 μ

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

source

theorem measure_theory.smul_le_stopped_value_hitting {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : measure_theory.filtration ℕ m0} {f : ℕ → Ω → ℝ} [measure_theory.is_finite_measure μ] (hsub : measure_theory.submartingale f 𝒢 μ) {ε : nnreal} (n : ℕ) :

ε • ⇑μ {ω : Ω | ↑ε ≤ (finset.range (n + 1)).sup' finset.nonempty_range_succ (λ (k : ℕ), f k ω)} ≤ ennreal.of_real (∫ (ω : Ω) in {ω : Ω | ↑ε ≤ (finset.range (n + 1)).sup' finset.nonempty_range_succ (λ (k : ℕ), f k ω)}, measure_theory.stopped_value f (measure_theory.hitting f {y : ℝ | ↑ε ≤ y} 0 n) ω ∂μ)

source

theorem measure_theory.maximal_ineq {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : measure_theory.filtration ℕ m0} {f : ℕ → Ω → ℝ} [measure_theory.is_finite_measure μ] (hsub : measure_theory.submartingale f 𝒢 μ) (hnonneg : 0 ≤ f) {ε : nnreal} (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).