English
The discrete hitting time is a stopping time with respect to a filtration under suitable adaptedness and measurability assumptions: the map ω ↦ hitting u s n n′ ω is a stopping time for the filtration f.
Русский
Дискретное время попадания является останавливанием относительно заданной фильтрации при соответствующих предпосылках об адаптации и измеримости: отображение ω ↦ hitting u s n n′ ω является stopping time.
LaTeX
$$$\\text{IsStoppingTime}_f\\ (\\lambda \\omega.\\ hitting\\ u\\ s\\ n\\ n'\\ \\omega)\\ (f)$.$$
Lean4
/-- A discrete hitting time is a stopping time. -/
theorem hitting_isStoppingTime [ConditionallyCompleteLinearOrder ι] [WellFoundedLT ι] [Countable ι] [TopologicalSpace β]
[PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] {f : Filtration ι m} {u : ι → Ω → β} {s : Set β}
{n n' : ι} (hu : Adapted f u) (hs : MeasurableSet s) : IsStoppingTime f (hitting u s n n') :=
by
intro i
rcases le_or_gt n' i with hi | hi
· have h_le : ∀ ω, hitting u s n n' ω ≤ i := fun x => (hitting_le x).trans hi
simp [h_le]
· have h_set_eq_Union : {ω | hitting u s n n' ω ≤ i} = ⋃ j ∈ Set.Icc n i, u j ⁻¹' s :=
by
ext x
rw [Set.mem_setOf_eq, hitting_le_iff_of_lt _ hi]
simp only [Set.mem_Icc, exists_prop, Set.mem_iUnion, Set.mem_preimage]
rw [h_set_eq_Union]
exact MeasurableSet.iUnion fun j => MeasurableSet.iUnion fun hj => f.mono hj.2 _ ((hu j).measurable hs)
