Theorems · Theorem · probability

MeasureTheory.crossing_eq_crossing_of_lowerCrossingTime_lt

∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω} {M : ℕ},
  N ≤ M →
    MeasureTheory.lowerCrossingTime a b f N n ω < N →
      MeasureTheory.upperCrossingTime a b f M n ω = MeasureTheory.upperCrossingTime a b f N n ω ∧
        MeasureTheory.lowerCrossingTime a b f M n ω = MeasureTheory.lowerCrossingTime a b f N n ω

Defined in

Mathlib.Probability.Martingale.Upcrossing

Cited by

1 results in Mathlib

Foundations

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