Theorems · Definition · probability

MeasureTheory.stoppedAbove

{ι : Type u_1} →
  {Ω : Type u_2} →
    {β : Type u_3} → [inst : LinearOrder ι] → [OrderBot ι] → [InfSet ι] → [Preorder β] → (ι → Ω → β) → β → ι → Ω → β

The stopped process of f above r is the process that is equal to f until leastGE f r (the first time f passes above r), and then is constant afterwards.

Defined in

Mathlib.Probability.Martingale.BorelCantelli

Cited by

5 results in Mathlib

Foundations

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

Assumes

LinearOrderOrderBotInfSetPreorder