English
If u is Adapted to f, τ is a stopping time, and ι is discrete, then for every n the stopped process is StronglyMeasurable.
Русский
Если u адаптирован к f, τ — время остановки, а ι дискретно, то для любого n остановленный процесс является сильно измеримым.
LaTeX
$$$[DiscreteTopology\ ι] \Rightarrow (hu : \text{Adapted } f\ u) \Rightarrow (hτ : \text{IsStoppingTime } f\ τ) \Rightarrow \forall n, \text{StronglyMeasurable } (\text{stoppedProcess } u\ τ\ n)$$$
Lean4
/-- Given stopping times `τ` and `η` which are bounded below, `Set.piecewise s τ η` is also
a stopping time with respect to the same filtration. -/
theorem piecewise_of_le (hτ_st : IsStoppingTime 𝒢 τ) (hη_st : IsStoppingTime 𝒢 η) (hτ : ∀ ω, i ≤ τ ω)
(hη : ∀ ω, i ≤ η ω) (hs : MeasurableSet[𝒢 i] s) : IsStoppingTime 𝒢 (s.piecewise τ η) :=
by
intro n
have : {ω | s.piecewise τ η ω ≤ n} = s ∩ {ω | τ ω ≤ n} ∪ sᶜ ∩ {ω | η ω ≤ n} :=
by
ext1 ω
simp only [Set.piecewise, Set.mem_setOf_eq]
by_cases hx : ω ∈ s <;> simp [hx]
rw [this]
by_cases hin : i ≤ n
· have hs_n : MeasurableSet[𝒢 n] s := 𝒢.mono hin _ hs
exact (hs_n.inter (hτ_st n)).union (hs_n.compl.inter (hη_st n))
· have hτn : ∀ ω, ¬τ ω ≤ n := fun ω hτn => hin ((hτ ω).trans hτn)
have hηn : ∀ ω, ¬η ω ≤ n := fun ω hηn => hin ((hη ω).trans hηn)
simp [hτn, hηn, @MeasurableSet.empty _ _]
