Theorems · Theorem · probability

MeasureTheory.submartingale_of_expected_stoppedValue_mono

∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} [MeasureTheory.SigmaFiniteFiltration μ 𝒢],
  MeasureTheory.StronglyAdapted 𝒢 f →
    (∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
      (∀ (τ π : Ω → ℕ∞),
          MeasureTheory.IsStoppingTime 𝒢 τ →
            MeasureTheory.IsStoppingTime 𝒢 π →
              τ ≤ π →
                (∃ N, ∀ (ω : Ω), π ω ≤ ↑N) →
                  ∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ) →
        MeasureTheory.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 π.

Defined in

Mathlib.Probability.Martingale.OptionalStopping

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SigmaFiniteFiltration