Documentation

Mathlib.Probability.Process.HittingTime

Hitting time #

Given a stochastic process, the hitting time provides the first time the process "hits" some subset of the state space. The hitting time is a stopping time in the case that the time index is discrete and the process is adapted (this is true in a far more general setting however we have only proved it for the discrete case so far).

Main definition #

Main results #

Implementation notes #

In the definition of the hitting time, we bound the hitting time by an upper and lower bound. This is to ensure that our result is meaningful in the case we are taking the infimum of an empty set or the infimum of a set which is unbounded from below. With this, we can talk about hitting times indexed by the natural numbers or the reals. By taking the bounds to be and , we obtain the standard definition in the case that the index is ℕ∞ or ℝ≥0∞.

noncomputable def MeasureTheory.hitting {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [Preorder ι] [InfSet ι] (u : ιΩβ) (s : Set β) (n : ι) (m : ι) :
Ωι

Hitting time: given a stochastic process u and a set s, hitting u s n m is the first time u is in s after time n and before time m (if u does not hit s after time n and before m then the hitting time is simply m).

The hitting time is a stopping time if the process is adapted and discrete.

Equations
Instances For
    theorem MeasureTheory.hitting_def {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [Preorder ι] [InfSet ι] (u : ιΩβ) (s : Set β) (n : ι) (m : ι) :
    MeasureTheory.hitting u s n m = fun (x : Ω) => if jSet.Icc n m, u j x s then sInf (Set.Icc n m {i : ι | u i x s}) else m
    theorem MeasureTheory.hitting_of_lt {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] {u : ιΩβ} {s : Set β} {n : ι} {ω : Ω} {m : ι} (h : m < n) :

    This lemma is strictly weaker than hitting_of_le.

    theorem MeasureTheory.hitting_le {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] {u : ιΩβ} {s : Set β} {n : ι} {m : ι} (ω : Ω) :
    theorem MeasureTheory.not_mem_of_lt_hitting {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] {u : ιΩβ} {s : Set β} {n : ι} {ω : Ω} {m : ι} {k : ι} (hk₁ : k < MeasureTheory.hitting u s n m ω) (hk₂ : n k) :
    u k ωs
    theorem MeasureTheory.hitting_eq_end_iff {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] {u : ιΩβ} {s : Set β} {n : ι} {ω : Ω} {m : ι} :
    MeasureTheory.hitting u s n m ω = m (∃ jSet.Icc n m, u j ω s)sInf (Set.Icc n m {i : ι | u i ω s}) = m
    theorem MeasureTheory.hitting_of_le {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] {u : ιΩβ} {s : Set β} {n : ι} {ω : Ω} {m : ι} (hmn : m n) :
    theorem MeasureTheory.le_hitting {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] {u : ιΩβ} {s : Set β} {n : ι} {m : ι} (hnm : n m) (ω : Ω) :
    theorem MeasureTheory.le_hitting_of_exists {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] {u : ιΩβ} {s : Set β} {n : ι} {ω : Ω} {m : ι} (h_exists : jSet.Icc n m, u j ω s) :
    theorem MeasureTheory.hitting_mem_Icc {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] {u : ιΩβ} {s : Set β} {n : ι} {m : ι} (hnm : n m) (ω : Ω) :
    theorem MeasureTheory.hitting_mem_set {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] {u : ιΩβ} {s : Set β} {n : ι} {ω : Ω} [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] {m : ι} (h_exists : jSet.Icc n m, u j ω s) :
    u (MeasureTheory.hitting u s n m ω) ω s
    theorem MeasureTheory.hitting_mem_set_of_hitting_lt {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] {u : ιΩβ} {s : Set β} {n : ι} {ω : Ω} [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] {m : ι} (hl : MeasureTheory.hitting u s n m ω < m) :
    u (MeasureTheory.hitting u s n m ω) ω s
    theorem MeasureTheory.hitting_le_of_mem {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] {u : ιΩβ} {s : Set β} {n : ι} {i : ι} {ω : Ω} {m : ι} (hin : n i) (him : i m) (his : u i ω s) :
    theorem MeasureTheory.hitting_le_iff_of_exists {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] {u : ιΩβ} {s : Set β} {n : ι} {i : ι} {ω : Ω} [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] {m : ι} (h_exists : jSet.Icc n m, u j ω s) :
    MeasureTheory.hitting u s n m ω i jSet.Icc n i, u j ω s
    theorem MeasureTheory.hitting_le_iff_of_lt {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] {u : ιΩβ} {s : Set β} {n : ι} {ω : Ω} [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] {m : ι} (i : ι) (hi : i < m) :
    MeasureTheory.hitting u s n m ω i jSet.Icc n i, u j ω s
    theorem MeasureTheory.hitting_lt_iff {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] {u : ιΩβ} {s : Set β} {n : ι} {ω : Ω} [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] {m : ι} (i : ι) (hi : i m) :
    MeasureTheory.hitting u s n m ω < i jSet.Ico n i, u j ω s
    theorem MeasureTheory.hitting_eq_hitting_of_exists {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] {u : ιΩβ} {s : Set β} {n : ι} {ω : Ω} {m₁ : ι} {m₂ : ι} (h : m₁ m₂) (h' : jSet.Icc n m₁, u j ω s) :
    MeasureTheory.hitting u s n m₁ ω = MeasureTheory.hitting u s n m₂ ω
    theorem MeasureTheory.hitting_mono {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] {u : ιΩβ} {s : Set β} {n : ι} {ω : Ω} {m₁ : ι} {m₂ : ι} (hm : m₁ m₂) :
    MeasureTheory.hitting u s n m₁ ω MeasureTheory.hitting u s n m₂ ω
    theorem MeasureTheory.hitting_isStoppingTime {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [ConditionallyCompleteLinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [Countable ι] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] {f : MeasureTheory.Filtration ι m} {u : ιΩβ} {s : Set β} {n : ι} {n' : ι} (hu : MeasureTheory.Adapted f u) (hs : MeasurableSet s) :

    A discrete hitting time is a stopping time.

    theorem MeasureTheory.stoppedValue_hitting_mem {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] {u : ιΩβ} {s : Set β} {n : ι} {m : ι} {ω : Ω} (h : jSet.Icc n m, u j ω s) :
    theorem MeasureTheory.isStoppingTime_hitting_isStoppingTime {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [ConditionallyCompleteLinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [Countable ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] {f : MeasureTheory.Filtration ι m} {u : ιΩβ} {τ : Ωι} (hτ : MeasureTheory.IsStoppingTime f τ) {N : ι} (hτbdd : ∀ (x : Ω), τ x N) {s : Set β} (hs : MeasurableSet s) (hf : MeasureTheory.Adapted f u) :
    MeasureTheory.IsStoppingTime f fun (x : Ω) => MeasureTheory.hitting u s (τ x) N x

    The hitting time of a discrete process with the starting time indexed by a stopping time is a stopping time.

    theorem MeasureTheory.hitting_eq_sInf {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [CompleteLattice ι] {u : ιΩβ} {s : Set β} (ω : Ω) :
    MeasureTheory.hitting u s ω = sInf {i : ι | u i ω s}
    theorem MeasureTheory.hitting_bot_le_iff {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrderBot ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] {u : ιΩβ} {s : Set β} {i : ι} {n : ι} {ω : Ω} (hx : jn, u j ω s) :
    MeasureTheory.hitting u s n ω i ji, u j ω s