English
Let f be a filtration, u a family of β-valued processes adapted to f, and suppose u(i,ω) depends continuously on i for each ω, τ is a stopping time, and ι is such that every stopped value at n is measurable. Then for every n, the stopped process at time n is strongly measurable.
Русский
Пусть f — фильтрация, u — семейство процессов, приспособленных к f, и пусть u непрерывно зависит от времени i для каждого ω; пусть τ — время остановки. Тогда для каждого n процесс, остановленный в момент n, является сильно измеримым.
LaTeX
$$$(hu : \text{Adapted } f\ u) \wedge (\forall\omega,\text{Continuous } i\mapsto u(i,\omega)) \wedge (hτ : \text{IsStoppingTime } f\ τ) \wedge (n : ι) \Rightarrow \text{StronglyMeasurable} (\text{stoppedProcess } u\ τ\ n)$$$
Lean4
theorem stronglyMeasurable_stoppedProcess [MetrizableSpace ι] (hu : Adapted f u)
(hu_cont : ∀ ω, Continuous fun i => u i ω) (hτ : IsStoppingTime f τ) (n : ι) :
StronglyMeasurable (MeasureTheory.stoppedProcess u τ n) :=
(hu.progMeasurable_of_continuous hu_cont).stronglyMeasurable_stoppedProcess hτ n
