Theorems · Theorem · probability

MeasureTheory.Submartingale.sum_mul_upcrossingStrat_le

∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ}
  {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    ∫ (x : Ω), (∑ k ∈ Finset.range n, MeasureTheory.upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
      ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ

Defined in

Mathlib.Probability.Martingale.Upcrossing

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasure