Theorems · Theorem · probability

MeasureTheory.upperCrossingTime_succ

∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] [inst_1 : OrderBot ι] [inst_2 : InfSet ι] {a b : ℝ} {f : ι → Ω → ℝ}
  {N : ι} {n : ℕ} {ω : Ω},
  MeasureTheory.upperCrossingTime a b f N (n + 1) ω =
    MeasureTheory.hittingBtwn f (Set.Ici b)
      (MeasureTheory.lowerCrossingTimeAux a f (MeasureTheory.upperCrossingTime a b f N n ω) N ω) N ω

Defined in

Mathlib.Probability.Martingale.Upcrossing

Cited by

3 results in Mathlib

Foundations

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

Assumes

PreorderOrderBotInfSet