Theorems · Theorem · probability

MeasureTheory.Submartingale.expected_stoppedValue_mono

∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  {τ π : Ω → ℕ∞} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] [ClosedIciTopology E]
  [MeasureTheory.SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E},
  MeasureTheory.Submartingale f 𝒢 μ →
    MeasureTheory.IsStoppingTime 𝒢 τ →
      MeasureTheory.IsStoppingTime 𝒢 π →
        τ ≤ π →
          ∀ {N : ℕ},
            (∀ (ω : Ω), π ω ≤ ↑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.

Defined in

Mathlib.Probability.Martingale.OptionalStopping

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpacePartialOrderIsOrderedAddMonoidIsOrderedModuleClosedIciTopologyMeasureTheory.SigmaFiniteFiltration