mathlib3 documentation

probability.process.hitting_time

Hitting time #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 measure_theory.hitting {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [preorder ι] [has_Inf ι] (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
theorem measure_theory.hitting_of_lt {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order ι] {u : ι Ω β} {s : set β} {n : ι} {ω : Ω} {m : ι} (h : m < n) :

This lemma is strictly weaker than hitting_of_le.

theorem measure_theory.hitting_le {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order ι] {u : ι Ω β} {s : set β} {n m : ι} (ω : Ω) :
theorem measure_theory.not_mem_of_lt_hitting {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order ι] {u : ι Ω β} {s : set β} {n : ι} {ω : Ω} {m k : ι} (hk₁ : k < measure_theory.hitting u s n m ω) (hk₂ : n k) :
u k ω s
theorem measure_theory.hitting_eq_end_iff {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order ι] {u : ι Ω β} {s : set β} {n : ι} {ω : Ω} {m : ι} :
measure_theory.hitting u s n m ω = m ( (j : ι) (H : j set.Icc n m), u j ω s) has_Inf.Inf (set.Icc n m {i : ι | u i ω s}) = m
theorem measure_theory.hitting_of_le {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order ι] {u : ι Ω β} {s : set β} {n : ι} {ω : Ω} {m : ι} (hmn : m n) :
theorem measure_theory.le_hitting {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order ι] {u : ι Ω β} {s : set β} {n m : ι} (hnm : n m) (ω : Ω) :
theorem measure_theory.le_hitting_of_exists {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order ι] {u : ι Ω β} {s : set β} {n : ι} {ω : Ω} {m : ι} (h_exists : (j : ι) (H : j set.Icc n m), u j ω s) :
theorem measure_theory.hitting_mem_Icc {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order ι] {u : ι Ω β} {s : set β} {n m : ι} (hnm : n m) (ω : Ω) :
theorem measure_theory.hitting_mem_set {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order ι] {u : ι Ω β} {s : set β} {n : ι} {ω : Ω} [is_well_order ι has_lt.lt] {m : ι} (h_exists : (j : ι) (H : j set.Icc n m), u j ω s) :
u (measure_theory.hitting u s n m ω) ω s
theorem measure_theory.hitting_mem_set_of_hitting_lt {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order ι] {u : ι Ω β} {s : set β} {n : ι} {ω : Ω} [is_well_order ι has_lt.lt] {m : ι} (hl : measure_theory.hitting u s n m ω < m) :
u (measure_theory.hitting u s n m ω) ω s
theorem measure_theory.hitting_le_of_mem {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order ι] {u : ι Ω β} {s : set β} {n i : ι} {ω : Ω} {m : ι} (hin : n i) (him : i m) (his : u i ω s) :
theorem measure_theory.hitting_le_iff_of_exists {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order ι] {u : ι Ω β} {s : set β} {n i : ι} {ω : Ω} [is_well_order ι has_lt.lt] {m : ι} (h_exists : (j : ι) (H : j set.Icc n m), u j ω s) :
measure_theory.hitting u s n m ω i (j : ι) (H : j set.Icc n i), u j ω s
theorem measure_theory.hitting_le_iff_of_lt {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order ι] {u : ι Ω β} {s : set β} {n : ι} {ω : Ω} [is_well_order ι has_lt.lt] {m : ι} (i : ι) (hi : i < m) :
measure_theory.hitting u s n m ω i (j : ι) (H : j set.Icc n i), u j ω s
theorem measure_theory.hitting_lt_iff {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order ι] {u : ι Ω β} {s : set β} {n : ι} {ω : Ω} [is_well_order ι has_lt.lt] {m : ι} (i : ι) (hi : i m) :
measure_theory.hitting u s n m ω < i (j : ι) (H : j set.Ico n i), u j ω s
theorem measure_theory.hitting_eq_hitting_of_exists {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order ι] {u : ι Ω β} {s : set β} {n : ι} {ω : Ω} {m₁ m₂ : ι} (h : m₁ m₂) (h' : (j : ι) (H : j set.Icc n m₁), u j ω s) :
measure_theory.hitting u s n m₁ ω = measure_theory.hitting u s n m₂ ω
theorem measure_theory.hitting_mono {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order ι] {u : ι Ω β} {s : set β} {n : ι} {ω : Ω} {m₁ m₂ : ι} (hm : m₁ m₂) :

A discrete hitting time is a stopping time.

theorem measure_theory.stopped_value_hitting_mem {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order ι] [is_well_order ι has_lt.lt] {u : ι Ω β} {s : set β} {n m : ι} {ω : Ω} (h : (j : ι) (H : j set.Icc n m), u j ω s) :

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

theorem measure_theory.hitting_eq_Inf {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [complete_lattice ι] {u : ι Ω β} {s : set β} (ω : Ω) :
measure_theory.hitting u s ω = has_Inf.Inf {i : ι | u i ω s}
theorem measure_theory.hitting_bot_le_iff {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [conditionally_complete_linear_order_bot ι] [is_well_order ι has_lt.lt] {u : ι Ω β} {s : set β} {i n : ι} {ω : Ω} (hx : (j : ι), j n u j ω s) :
measure_theory.hitting u s n ω i (j : ι) (H : j i), u j ω s