Theorems · Theorem · probability

MeasureTheory.submartingale_iff_expected_stoppedValue_mono

• #62 of the 100 theorems: Fair Games Theorem
• 1000+ list: Optional stopping theorem

∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} [MeasureTheory.SigmaFiniteFiltration μ 𝒢],
  MeasureTheory.StronglyAdapted 𝒢 f →
    (∀ (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): 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 π.

Defined in

Mathlib.Probability.Martingale.OptionalStopping

Cited by

1 results in Mathlib

Foundations

Depth 302 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.SigmaFiniteFiltration