Documentation

Mathlib.Probability.Martingale.OptionalStopping

Optional stopping theorem (fair game theorem) #

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 #

theorem MeasureTheory.Submartingale.expected_stoppedValue_mono {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} {f : Ω} {τ : Ω} {π : Ω} [MeasureTheory.SigmaFiniteFiltration μ 𝒢] (hf : MeasureTheory.Submartingale f 𝒢 μ) (hτ : MeasureTheory.IsStoppingTime 𝒢 τ) (hπ : MeasureTheory.IsStoppingTime 𝒢 π) (hle : τ π) {N : } (hbdd : ∀ (ω : Ω), π ω N) :
∫ (x : Ω), MeasureTheory.stoppedValue f τ xμ ∫ (x : Ω), MeasureTheory.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 Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} {f : Ω} [MeasureTheory.IsFiniteMeasure μ] (hadp : MeasureTheory.Adapted 𝒢 f) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (τ π : Ω), MeasureTheory.IsStoppingTime 𝒢 τMeasureTheory.IsStoppingTime 𝒢 πτ π(∃ (N : ), ∀ (ω : Ω), π ω N)∫ (x : Ω), MeasureTheory.stoppedValue f τ xμ ∫ (x : Ω), MeasureTheory.stoppedValue f π 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 MeasureTheory.submartingale_iff_expected_stoppedValue_mono {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} {f : Ω} [MeasureTheory.IsFiniteMeasure μ] (hadp : MeasureTheory.Adapted 𝒢 f) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) :
MeasureTheory.Submartingale f 𝒢 μ ∀ (τ π : Ω), MeasureTheory.IsStoppingTime 𝒢 τMeasureTheory.IsStoppingTime 𝒢 πτ π(∃ (N : ), ∀ (x : Ω), π x N)∫ (x : Ω), MeasureTheory.stoppedValue f τ xμ ∫ (x : Ω), MeasureTheory.stoppedValue 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 π.

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

theorem MeasureTheory.smul_le_stoppedValue_hitting {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} {f : Ω} [MeasureTheory.IsFiniteMeasure μ] (hsub : MeasureTheory.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 ω}, MeasureTheory.stoppedValue f (MeasureTheory.hitting f {y : | ε y} 0 n) ωμ)
theorem MeasureTheory.maximal_ineq {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} {f : Ω} [MeasureTheory.IsFiniteMeasure μ] (hsub : MeasureTheory.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).