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 #
measure_theory.hitting: the hitting time of a stochastic process
Main results #
measure_theory.hitting_is_stopping_time: a discrete hitting time of an adapted process is a stopping time
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.
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) :
measure_theory.hitting u s n m ω = m
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 : ι}
(ω : Ω) :
measure_theory.hitting u s n m ω ≤ 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 : ι} :
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) :
measure_theory.hitting u s n m ω = 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)
(ω : Ω) :
n ≤ measure_theory.hitting u s n m ω
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)
(ω : Ω) :
measure_theory.hitting u s n m ω ∈ set.Icc 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) :
measure_theory.hitting u s n m ω ≤ i
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) :
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) :
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) :
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₂) :
measure_theory.hitting u s n m₁ ω ≤ measure_theory.hitting u s n m₂ ω
theorem
measure_theory.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]
[countable ι]
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[measurable_space β]
[borel_space β]
{f : measure_theory.filtration ι m}
{u : ι → Ω → β}
{s : set β}
{n n' : ι}
(hu : measure_theory.adapted f u)
(hs : measurable_set s) :
measure_theory.is_stopping_time f (measure_theory.hitting u s n n')
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) :
measure_theory.stopped_value u (measure_theory.hitting u s n m) ω ∈ 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]
[countable ι]
[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) :
measure_theory.is_stopping_time f (λ (x : Ω), measure_theory.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
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) :