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 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.hittingBtwn_isStoppingTime: a discrete hitting time of an adapted process is a stopping timeMeasureTheory.hittingAfter_isStoppingTime: a discrete hitting time of an 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 adapted and discrete.
Equations
Instances For
@[deprecated MeasureTheory.hittingBtwn (since := "2025-10-25")]
def
MeasureTheory.hitting
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[Preorder ι]
[InfSet ι]
(u : ι → Ω → β)
(s : Set β)
(n m : ι)
:
Ω → ι
Alias of MeasureTheory.hittingBtwn.
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 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
@[deprecated MeasureTheory.hittingBtwn_def (since := "2025-10-25")]
theorem
MeasureTheory.hitting_def
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[Preorder ι]
[InfSet ι]
(u : ι → Ω → β)
(s : Set β)
(n m : ι)
:
Alias of MeasureTheory.hittingBtwn_def.
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.
@[deprecated MeasureTheory.hittingBtwn_of_lt (since := "2025-10-25")]
theorem
MeasureTheory.hitting_of_lt
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
{m : ι}
(h : m < n)
:
Alias of MeasureTheory.hittingBtwn_of_lt.
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 : ι}
(ω : Ω)
:
@[deprecated MeasureTheory.hittingBtwn_le (since := "2025-10-25")]
theorem
MeasureTheory.hitting_le
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n m : ι}
(ω : Ω)
:
Alias of MeasureTheory.hittingBtwn_le.
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
@[deprecated MeasureTheory.notMem_of_lt_hittingBtwn (since := "2025-10-25")]
theorem
MeasureTheory.notMem_of_lt_hitting
{Ω : 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
Alias of MeasureTheory.notMem_of_lt_hittingBtwn.
@[deprecated MeasureTheory.notMem_of_lt_hittingBtwn (since := "2025-05-23")]
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 < hittingBtwn u s n m ω)
(hk₂ : n ≤ k)
:
u k ω ∉ s
Alias of MeasureTheory.notMem_of_lt_hittingBtwn.
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
@[deprecated MeasureTheory.hittingBtwn_eq_end_iff (since := "2025-10-25")]
theorem
MeasureTheory.hitting_eq_end_iff
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
{m : ι}
:
Alias of MeasureTheory.hittingBtwn_eq_end_iff.
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)
:
@[deprecated MeasureTheory.hittingBtwn_of_le (since := "2025-10-25")]
theorem
MeasureTheory.hitting_of_le
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
{m : ι}
(hmn : m ≤ n)
:
Alias of MeasureTheory.hittingBtwn_of_le.
theorem
MeasureTheory.le_hittingBtwn
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n m : ι}
(hnm : n ≤ m)
(ω : Ω)
:
@[deprecated MeasureTheory.le_hittingBtwn (since := "2025-10-25")]
theorem
MeasureTheory.le_hitting
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n m : ι}
(hnm : n ≤ m)
(ω : Ω)
:
Alias of MeasureTheory.le_hittingBtwn.
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)
:
@[deprecated MeasureTheory.le_hittingBtwn_of_exists (since := "2025-10-25")]
theorem
MeasureTheory.le_hitting_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)
:
Alias of MeasureTheory.le_hittingBtwn_of_exists.
theorem
MeasureTheory.hittingBtwn_mem_Icc
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n m : ι}
(hnm : n ≤ m)
(ω : Ω)
:
@[deprecated MeasureTheory.hittingBtwn_mem_Icc (since := "2025-10-25")]
theorem
MeasureTheory.hitting_mem_Icc
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n m : ι}
(hnm : n ≤ m)
(ω : Ω)
:
Alias of MeasureTheory.hittingBtwn_mem_Icc.
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)
:
@[deprecated MeasureTheory.hittingBtwn_mem_set (since := "2025-10-25")]
theorem
MeasureTheory.hitting_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)
:
Alias of MeasureTheory.hittingBtwn_mem_set.
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)
:
@[deprecated MeasureTheory.hittingBtwn_mem_set_of_hittingBtwn_lt (since := "2025-10-25")]
theorem
MeasureTheory.hitting_mem_set_of_hitting_lt
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
[WellFoundedLT ι]
{m : ι}
(hl : hittingBtwn u s n m ω < m)
:
Alias of MeasureTheory.hittingBtwn_mem_set_of_hittingBtwn_lt.
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)
:
@[deprecated MeasureTheory.hittingBtwn_le_of_mem (since := "2025-10-25")]
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)
:
Alias of MeasureTheory.hittingBtwn_le_of_mem.
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)
:
@[deprecated MeasureTheory.hittingBtwn_le_iff_of_exists (since := "2025-10-25")]
theorem
MeasureTheory.hitting_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)
:
@[deprecated MeasureTheory.hittingBtwn_le_iff_of_lt (since := "2025-10-25")]
theorem
MeasureTheory.hitting_le_iff_of_lt
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
[WellFoundedLT ι]
{m : ι}
(i : ι)
(hi : i < m)
:
Alias of MeasureTheory.hittingBtwn_le_iff_of_lt.
theorem
MeasureTheory.hittingBtwn_lt_iff
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
[WellFoundedLT ι]
{m : ι}
(i : ι)
(hi : i ≤ m)
:
@[deprecated MeasureTheory.hittingBtwn_lt_iff (since := "2025-10-25")]
theorem
MeasureTheory.hitting_lt_iff
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
[WellFoundedLT ι]
{m : ι}
(i : ι)
(hi : i ≤ m)
:
Alias of MeasureTheory.hittingBtwn_lt_iff.
theorem
MeasureTheory.hittingAfter_lt_iff
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n i : ι}
{ω : Ω}
[WellFoundedLT ι]
:
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)
:
@[deprecated MeasureTheory.hittingBtwn_eq_hittingBtwn_of_exists (since := "2025-10-25")]
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' : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s)
:
Alias of MeasureTheory.hittingBtwn_eq_hittingBtwn_of_exists.
theorem
MeasureTheory.hittingBtwn_mono
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
{m₁ m₂ : ι}
(hm : m₁ ≤ m₂)
:
@[deprecated MeasureTheory.hittingBtwn_mono (since := "2025-10-25")]
theorem
MeasureTheory.hitting_mono
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrder ι]
{u : ι → Ω → β}
{s : Set β}
{n : ι}
{ω : Ω}
{m₁ m₂ : ι}
(hm : m₁ ≤ m₂)
:
Alias of MeasureTheory.hittingBtwn_mono.
theorem
MeasureTheory.hittingBtwn_isStoppingTime
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[ConditionallyCompleteLinearOrder ι]
[WellFoundedLT ι]
[Countable ι]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[MeasurableSpace β]
[BorelSpace β]
{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.hittingBtwn_isStoppingTime (since := "2025-10-25")]
theorem
MeasureTheory.hitting_isStoppingTime
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[ConditionallyCompleteLinearOrder ι]
[WellFoundedLT ι]
[Countable ι]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[MeasurableSpace β]
[BorelSpace β]
{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.hittingBtwn_isStoppingTime.
A discrete hitting time is a stopping time.
theorem
MeasureTheory.hittingAfter_isStoppingTime
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[ConditionallyCompleteLinearOrder ι]
[WellFoundedLT ι]
[Countable ι]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[MeasurableSpace β]
[BorelSpace β]
{f : Filtration ι m}
{u : ι → Ω → β}
{s : Set β}
{n : ι}
(hu : Adapted f u)
(hs : MeasurableSet s)
:
IsStoppingTime f (hittingAfter u s n)
A discrete hitting time is a stopping time.
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)
:
@[deprecated MeasureTheory.stoppedValue_hittingBtwn_mem (since := "2025-10-25")]
theorem
MeasureTheory.stoppedValue_hitting_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.isStoppingTime_hittingBtwn_isStoppingTime
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[ConditionallyCompleteLinearOrder ι]
[WellFoundedLT ι]
[Countable ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[MeasurableSpace β]
[BorelSpace β]
{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.isStoppingTime_hittingBtwn_isStoppingTime (since := "2025-10-25")]
theorem
MeasureTheory.isStoppingTime_hitting_isStoppingTime
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[ConditionallyCompleteLinearOrder ι]
[WellFoundedLT ι]
[Countable ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[MeasurableSpace β]
[BorelSpace β]
{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.isStoppingTime_hittingBtwn_isStoppingTime.
The hitting time of a discrete process with the starting time indexed by a stopping time is a stopping time.
@[deprecated MeasureTheory.hittingBtwn_eq_sInf (since := "2025-10-25")]
theorem
MeasureTheory.hitting_eq_sInf
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[CompleteLattice ι]
{u : ι → Ω → β}
{s : Set β}
(ω : Ω)
:
Alias of MeasureTheory.hittingBtwn_eq_sInf.
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)
:
@[deprecated MeasureTheory.hittingBtwn_bot_le_iff (since := "2025-10-25")]
theorem
MeasureTheory.hitting_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)
:
Alias of MeasureTheory.hittingBtwn_bot_le_iff.
theorem
MeasureTheory.hittingAfter_bot_le_iff
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[ConditionallyCompleteLinearOrderBot ι]
[WellFoundedLT ι]
{u : ι → Ω → β}
{s : Set β}
{i : ι}
{ω : Ω}
: