Optional stopping theorem (fair game theorem)

The optional stopping theorem states that a strongly 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

• MeasureTheory.submartingale_iff_expected_stoppedValue_mono: the optional stopping theorem.
• MeasureTheory.Submartingale.stoppedProcess: the stopped process of a submartingale with respect to a stopping time is a submartingale.
• MeasureTheory.maximal_ineq: Doob's maximal inequality.

theorem MeasureTheory.Submartingale.expected_stoppedValue_mono {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {𝒢 : Filtration ℕ m0} {τ π : Ω → ℕ∞} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] [ClosedIciTopology E] [SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E} (hf : Submartingale f 𝒢 μ) (hτ : IsStoppingTime 𝒢 τ) (hπ : IsStoppingTime 𝒢 π) (hle : τ ≤ π) {N : ℕ} (hbdd : ∀ (ω : Ω), π ω ≤ ↑N) : ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ

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

theorem MeasureTheory.submartingale_of_expected_stoppedValue_mono {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {𝒢 : Filtration ℕ m0} {f : ℕ → Ω → ℝ} [SigmaFiniteFiltration μ 𝒢] (hadp : StronglyAdapted 𝒢 f) (hint : ∀ (i : ℕ), Integrable (f i) μ) (hf : ∀ (τ π : Ω → ℕ∞), IsStoppingTime 𝒢 τ → IsStoppingTime 𝒢 π → τ ≤ π → (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ ↑N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ) : Submartingale f 𝒢 μ

The converse direction of the optional stopping theorem, i.e. a strongly 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 MeasureTheory.submartingale_iff_expected_stoppedValue_mono {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {𝒢 : Filtration ℕ m0} {f : ℕ → Ω → ℝ} [SigmaFiniteFiltration μ 𝒢] (hadp : StronglyAdapted 𝒢 f) (hint : ∀ (i : ℕ), Integrable (f i) μ) : Submartingale f 𝒢 μ ↔ ∀ (τ π : Ω → ℕ∞), IsStoppingTime 𝒢 τ → IsStoppingTime 𝒢 π → τ ≤ π → (∃ (N : ℕ), ∀ (x : Ω), π x ≤ ↑N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ

The optional stopping theorem (fair game theorem): a strongly 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 π.

theorem MeasureTheory.Submartingale.stoppedProcess {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {𝒢 : Filtration ℕ m0} {f : ℕ → Ω → ℝ} {τ : Ω → ℕ∞} [SigmaFiniteFiltration μ 𝒢] (h : Submartingale f 𝒢 μ) (hτ : IsStoppingTime 𝒢 τ) : Submartingale (stoppedProcess f τ) 𝒢 μ

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

theorem MeasureTheory.smul_le_stoppedValue_hittingBtwn {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {𝒢 : Filtration ℕ m0} {f : ℕ → Ω → ℝ} [IsFiniteMeasure μ] (hsub : Submartingale f 𝒢 μ) {ε : NNReal} (n : ℕ) : ε • μ {ω : Ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun (k : ℕ) => f k ω} ≤ ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun (k : ℕ) => f k ω}, stoppedValue f (fun (ω : Ω) => ↑(hittingBtwn f {y : ℝ | ↑ε ≤ y} 0 n ω)) ω ∂μ)

theorem MeasureTheory.maximal_ineq {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {𝒢 : Filtration ℕ m0} {f : ℕ → Ω → ℝ} [IsFiniteMeasure μ] (hsub : Submartingale f 𝒢 μ) (hnonneg : 0 ≤ f) {ε : NNReal} (n : ℕ) : ↑ε * μ {ω : Ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun (k : ℕ) => f k ω} ≤ ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun (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 upcoming PR).