Theorems · Definition · probability

MeasureTheory.upperCrossingTime

{Ω : Type u_1} → {ι : Type u_2} → [inst : Preorder ι] → [OrderBot ι] → [InfSet ι] → ℝ → ℝ → (ι → Ω → ℝ) → ι → ℕ → Ω → ι

upperCrossingTime a b f N n is the first time before time N, f reaches above b after f reached below a for the n - 1-th time.

Defined in

Mathlib.Probability.Martingale.Upcrossing

Cited by

42 results in Mathlib

Foundations

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

Assumes

PreorderOrderBotInfSet