English
If τ is a stopping time and τ(x) ≤ N for all x, then the process x ↦ hitting u s (τ x) N x is a stopping time (under adaptedness and measurability hypotheses).
Русский
Если τ — останавливание во времени и для всех x выполняется τ(x) ≤ N, то процесс x ↦ hitting u s (τ x) N x является остановливанием (при условии адаптации и измеримости).
LaTeX
$$$IsStoppingTime\\ f\\ (\\lambda x.\\ hitting\\ u\\ s\\ (\\tau x)\\ N\\ x).$$$
Lean4
/-- The hitting time of a discrete process with the starting time indexed by a stopping time
is a stopping time. -/
theorem isStoppingTime_hitting_isStoppingTime [ConditionallyCompleteLinearOrder ι] [WellFoundedLT ι] [Countable ι]
[TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] [TopologicalSpace β] [PseudoMetrizableSpace β]
[MeasurableSpace β] [BorelSpace β] {f : Filtration ι m} {u : ι → Ω → β} {τ : Ω → ι} (hτ : IsStoppingTime f τ)
{N : ι} (hτbdd : ∀ x, τ x ≤ N) {s : Set β} (hs : MeasurableSet s) (hf : Adapted f u) :
IsStoppingTime f fun x => hitting u s (τ x) N x := by
intro n
have h₁ :
{x | hitting u s (τ x) N x ≤ n} =
(⋃ i ≤ n, {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) ∪ ⋃ i > n, {x | τ x = i} ∩ {x | hitting u s i N x ≤ n} :=
by
ext x
simp [← or_and_right, le_or_gt]
have h₂ : ⋃ i > n, {x | τ x = i} ∩ {x | hitting u s i N x ≤ n} = ∅ :=
by
ext x
simp only [gt_iff_lt, Set.mem_iUnion, Set.mem_inter_iff, Set.mem_setOf_eq, exists_prop, Set.mem_empty_iff_false,
iff_false, not_exists, not_and, not_le]
rintro m hm rfl
exact lt_of_lt_of_le hm (le_hitting (hτbdd _) _)
rw [h₁, h₂, Set.union_empty]
exact
MeasurableSet.iUnion fun i =>
MeasurableSet.iUnion fun hi => (f.mono hi _ (hτ.measurableSet_eq i)).inter (hitting_isStoppingTime hf hs n)
