Theorems · Theorem · probability

MeasureTheory.Submartingale.stoppedProcess

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

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

Defined in: Mathlib.Probability.Martingale.OptionalStopping
Cited by: 1 results in Mathlib
Foundations: Depth 303 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasureTheory.SigmaFiniteFiltration

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites27

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
Top.topproof · cited by 9,680
ENatstatement and proof · cited by 4,985
LE.le.transproof · cited by 3,151
MeasureTheory.integralproof · cited by 1,779
le_rflproof · cited by 1,558
WithTop.someproof · cited by 1,128
MeasureTheory.Filtrationstatement and proof · cited by 425
Classical.arbitraryproof · cited by 161
MeasureTheory.IsStoppingTimestatement and proof · cited by 122

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.Submartingale.stoppedAboveproof · cited by 2