Hitting times #
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 strongly adapted (this is true in a far more general setting however we have only proved it for the discrete case so far).
Main definition #
MeasureTheory.hittingBtwn u s n m: the first time a stochastic processuenters a setsafter timenand before timemMeasureTheory.hittingAfter u s n: the first time a stochastic processuenters a setsafter timen
Main results #
MeasureTheory.Adapted.isStoppingTime_hittingBtwn: a discrete hitting time of an adapted process is a stopping timeMeasureTheory.Adapted.isStoppingTime_hittingAfter: a discrete hitting time of a adapted process is a stopping time
noncomputable def
MeasureTheory.hittingBtwn
{Ω : 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, hittingBtwn 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 strongly adapted and discrete.
Equations
Instances For
noncomputable def
MeasureTheory.hittingAfter
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[Preorder ι]
[InfSet ι]
(u : ι → Ω → β)
(s : Set β)
(n : ι)
:
Ω → WithTop ι
Hitting time: given a stochastic process u and a set s, hittingAfter u s n is
the first time u is in s after time n (if u does not hit s after time n then the
hitting time is ⊤).
Equations
Instances For
@[simp]
theorem
MeasureTheory.hittingBtwn_univ
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
(n m : ι)
:
@[simp]
theorem
MeasureTheory.hittingAfter_univ
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[ConditionallyCompleteLattice ι]
{u : ι → Ω → β}
(n : ι)
:
theorem
MeasureTheory.hittingBtwn_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 hittingBtwn_of_le.
theorem
MeasureTheory.hittingBtwn_le
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n m : ι}
(ω : Ω)
:
theorem
MeasureTheory.notMem_of_lt_hittingBtwn
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
{m k : ι}
(hk₁ : k < hittingBtwn u s n m ω)
(hk₂ : n ≤ k)
:
u k ω ∉ s
theorem
MeasureTheory.notMem_of_lt_hittingAfter
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
{k : ι}
(hk₁ : ↑k < hittingAfter u s n ω)
(hk₂ : n ≤ k)
:
u k ω ∉ s
theorem
MeasureTheory.hittingAfter_eq_top_iff
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
:
theorem
MeasureTheory.hittingBtwn_of_le
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
{m : ι}
(hmn : m ≤ n)
:
theorem
MeasureTheory.le_hittingBtwn
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n m : ι}
(hnm : n ≤ m)
(ω : Ω)
:
theorem
MeasureTheory.le_hittingAfter
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
(ω : Ω)
:
theorem
MeasureTheory.le_hittingBtwn_of_exists
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
{m : ι}
(h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s)
:
theorem
MeasureTheory.hittingBtwn_mem_Icc
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n m : ι}
(hnm : n ≤ m)
(ω : Ω)
:
theorem
MeasureTheory.hittingBtwn_mem_set
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
[WellFoundedLT ι]
{m : ι}
(h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s)
:
theorem
MeasureTheory.hittingAfter_mem_set
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
[WellFoundedLT ι]
(h_exists : ∃ (j : ι), n ≤ j ∧ u j ω ∈ s)
:
theorem
MeasureTheory.hittingBtwn_mem_set_of_hittingBtwn_lt
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
[WellFoundedLT ι]
{m : ι}
(hl : hittingBtwn u s n m ω < m)
:
theorem
MeasureTheory.hittingAfter_mem_set_of_ne_top
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
[WellFoundedLT ι]
(hl : hittingAfter u s n ω ≠ ⊤)
:
theorem
MeasureTheory.hittingBtwn_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.hittingAfter_le_of_mem
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n i : ι}
{ω : Ω}
(hin : n ≤ i)
(his : u i ω ∈ s)
:
theorem
MeasureTheory.hittingBtwn_le_iff_of_exists
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n i : ι}
{ω : Ω}
[WellFoundedLT ι]
{m : ι}
(h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s)
:
theorem
MeasureTheory.hittingAfter_le_iff
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n i : ι}
{ω : Ω}
[WellFoundedLT ι]
:
theorem
MeasureTheory.hittingBtwn_le_iff_of_lt
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
[WellFoundedLT ι]
{m : ι}
(i : ι)
(hi : i < m)
:
theorem
MeasureTheory.hittingBtwn_lt_iff
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
{m : ι}
(i : ι)
(hi : i ≤ m)
:
theorem
MeasureTheory.hittingAfter_lt_iff
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n i : ι}
{ω : Ω}
:
theorem
MeasureTheory.hittingBtwn_eq_hittingBtwn_of_exists
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
{m₁ m₂ : ι}
(h : m₁ ≤ m₂)
(h' : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s)
:
theorem
MeasureTheory.hittingBtwn_anti
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
(u : ι → Ω → β)
(n m : ι)
:
Antitone fun (x : Set β) => hittingBtwn u x n m
hittingBtwn is nonincreasing with respect to the set.
theorem
MeasureTheory.hittingAfter_anti
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
(u : ι → Ω → β)
(n : ι)
:
Antitone fun (x : Set β) => hittingAfter u x n
hittingAfter is nonincreasing with respect to the set.
theorem
MeasureTheory.hittingBtwn_apply_anti
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
(u : ι → Ω → β)
(n m : ι)
(ω : Ω)
:
Antitone fun (x : Set β) => hittingBtwn u x n m ω
theorem
MeasureTheory.hittingAfter_apply_anti
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
(u : ι → Ω → β)
(n : ι)
(ω : Ω)
:
Antitone fun (x : Set β) => hittingAfter u x n ω
theorem
MeasureTheory.hittingBtwn_mono_right
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{ω : Ω}
(u : ι → Ω → β)
(s : Set β)
(n : ι)
:
Monotone fun (x : ι) => hittingBtwn u s n x ω
hittingBtwn is monotone with respect to the maximal time.
theorem
MeasureTheory.hittingBtwn_mono_left
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
(u : ι → Ω → β)
(s : Set β)
(m : ι)
:
Monotone fun (x : ι) => hittingBtwn u s x m
hittingBtwn is monotone with respect to the minimal time.
theorem
MeasureTheory.hittingAfter_mono
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
(u : ι → Ω → β)
(s : Set β)
:
Monotone (hittingAfter u s)
hittingAfter is monotone with respect to the minimal time.
theorem
MeasureTheory.hittingBtwn_apply_mono_right
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
(u : ι → Ω → β)
(s : Set β)
(n : ι)
(ω : Ω)
:
Monotone fun (x : ι) => hittingBtwn u s n x ω
theorem
MeasureTheory.hittingBtwn_apply_mono_left
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
(u : ι → Ω → β)
(s : Set β)
(m : ι)
(ω : Ω)
:
Monotone fun (x : ι) => hittingBtwn u s x m ω
theorem
MeasureTheory.hittingAfter_apply_mono
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
(u : ι → Ω → β)
(s : Set β)
(ω : Ω)
:
Monotone fun (x : ι) => hittingAfter u s x ω
theorem
MeasureTheory.Adapted.isStoppingTime_hittingBtwn
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[ConditionallyCompleteLinearOrder ι]
[WellFoundedLT ι]
[Countable ι]
{x✝ : MeasurableSpace β}
{f : Filtration ι m}
{u : ι → Ω → β}
{s : Set β}
{n n' : ι}
(hu : Adapted f u)
(hs : MeasurableSet s)
:
IsStoppingTime f fun (ω : Ω) => ↑(hittingBtwn u s n n' ω)
A discrete hitting time is a stopping time.
@[deprecated MeasureTheory.Adapted.isStoppingTime_hittingBtwn (since := "2026-01-25")]
theorem
MeasureTheory.hittingBtwn_isStoppingTime
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[ConditionallyCompleteLinearOrder ι]
[WellFoundedLT ι]
[Countable ι]
{x✝ : MeasurableSpace β}
{f : Filtration ι m}
{u : ι → Ω → β}
{s : Set β}
{n n' : ι}
(hu : Adapted f u)
(hs : MeasurableSet s)
:
IsStoppingTime f fun (ω : Ω) => ↑(hittingBtwn u s n n' ω)
Alias of MeasureTheory.Adapted.isStoppingTime_hittingBtwn.
A discrete hitting time is a stopping time.
theorem
MeasureTheory.Adapted.isStoppingTime_hittingAfter
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[ConditionallyCompleteLinearOrder ι]
[WellFoundedLT ι]
[Countable ι]
{x✝ : MeasurableSpace β}
{f : Filtration ι m}
{u : ι → Ω → β}
{s : Set β}
{n : ι}
(hu : Adapted f u)
(hs : MeasurableSet s)
:
IsStoppingTime f (hittingAfter u s n)
@[deprecated MeasureTheory.Adapted.isStoppingTime_hittingAfter (since := "2026-01-25")]
theorem
MeasureTheory.hittingAfter_isStoppingTime
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[ConditionallyCompleteLinearOrder ι]
[WellFoundedLT ι]
[Countable ι]
{x✝ : MeasurableSpace β}
{f : Filtration ι m}
{u : ι → Ω → β}
{s : Set β}
{n : ι}
(hu : Adapted f u)
(hs : MeasurableSet s)
:
IsStoppingTime f (hittingAfter u s n)
theorem
MeasureTheory.stoppedValue_hittingBtwn_mem
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
[WellFoundedLT ι]
{u : ι → Ω → β}
{s : Set β}
{n m : ι}
{ω : Ω}
(h : ∃ j ∈ Set.Icc n m, u j ω ∈ s)
:
theorem
MeasureTheory.Adapted.isStoppingTime_hittingBtwn_isStoppingTime
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[ConditionallyCompleteLinearOrder ι]
[WellFoundedLT ι]
[Countable ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
[MeasurableSpace β]
{f : Filtration ι m}
{u : ι → Ω → β}
{τ : Ω → WithTop ι}
(hτ : IsStoppingTime f τ)
{N : ι}
(hτbdd : ∀ (x : Ω), τ x ≤ ↑N)
{s : Set β}
(hs : MeasurableSet s)
(hf : Adapted f u)
:
IsStoppingTime f fun (x : Ω) => ↑(hittingBtwn u s (τ x).untopA N x)
The hitting time of a discrete process with the starting time indexed by a stopping time is a stopping time.
@[deprecated MeasureTheory.Adapted.isStoppingTime_hittingBtwn_isStoppingTime (since := "2026-01-25")]
theorem
MeasureTheory.isStoppingTime_hittingBtwn_isStoppingTime
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[ConditionallyCompleteLinearOrder ι]
[WellFoundedLT ι]
[Countable ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
[MeasurableSpace β]
{f : Filtration ι m}
{u : ι → Ω → β}
{τ : Ω → WithTop ι}
(hτ : IsStoppingTime f τ)
{N : ι}
(hτbdd : ∀ (x : Ω), τ x ≤ ↑N)
{s : Set β}
(hs : MeasurableSet s)
(hf : Adapted f u)
:
IsStoppingTime f fun (x : Ω) => ↑(hittingBtwn u s (τ x).untopA N x)
Alias of MeasureTheory.Adapted.isStoppingTime_hittingBtwn_isStoppingTime.
The hitting time of a discrete process with the starting time indexed by a stopping time is a stopping time.
theorem
MeasureTheory.hittingBtwn_bot_le_iff
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrderBot ι]
[WellFoundedLT ι]
{u : ι → Ω → β}
{s : Set β}
{i n : ι}
{ω : Ω}
(hx : ∃ j ≤ n, u j ω ∈ s)
:
theorem
MeasureTheory.hittingAfter_bot_le_iff
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrderBot ι]
[WellFoundedLT ι]
{u : ι → Ω → β}
{s : Set β}
{i : ι}
{ω : Ω}
: