mathlib documentation

probability.hitting_time

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 with_top 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) :
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.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_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₂ ω

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) :
theorem measure_theory.is_stopping_time_hitting_is_stopping_time {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [conditionally_complete_linear_order ι] [is_well_order ι has_lt.lt] [encodable ι] [topological_space ι] [order_topology ι] [topological_space.first_countable_topology ι] [topological_space β] [topological_space.pseudo_metrizable_space β] [measurable_space β] [borel_space β] {f : measure_theory.filtration ι m} {u : ι → Ω → β} {τ : Ω → ι} (hτ : measure_theory.is_stopping_time f τ) {N : ι} (hτbdd : ∀ (x : Ω), τ x N) {s : set β} (hs : measurable_set s) (hf : measure_theory.adapted f u) :

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