Theorems · Theorem · probability

MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part

∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ℕ → Ω → ℝ}
  {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ] (a b : ℝ),
  MeasureTheory.Submartingale f ℱ μ →
    ∀ (N : ℕ),
      (b - a) * ∫ (x : Ω), ↑(MeasureTheory.upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ

Doob's upcrossing estimate: given a real-valued discrete submartingale f and real values a and b, we have (b - a) * 𝔼[upcrossingsBefore a b f N] ≤ 𝔼[(f N - a)⁺] where upcrossingsBefore a b f N is the number of times the process f crossed from below a to above b before the time N.

Defined in

Mathlib.Probability.Martingale.Upcrossing

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasure