stronglyMeasurable_stoppedProcess_of_discrete

English

If the index set ι has the discrete topology, and u is adapted and τ is a stopping time, then for every n the stopped process is strongly measurable.

Русский

Если время индексирования имеет дискретную топологию, и u адаптирован, а τ — время остановки, то для каждого n останленный процесс существенно измерим.

LaTeX

$$$[DiscreteTopology\ ι] \Rightarrow (hu : \text{Adapted } f\ u) \Rightarrow (hτ : \text{IsStoppingTime } f\ τ) \Rightarrow \forall n, \text{StronglyMeasurable } (\text{stoppedProcess } u\ τ\ n)$$$

Lean4

theorem stronglyMeasurable_stoppedProcess_of_discrete [DiscreteTopology ι] (hu : Adapted f u) (hτ : IsStoppingTime f τ)
    (n : ι) : StronglyMeasurable (MeasureTheory.stoppedProcess u τ n) :=
  hu.progMeasurable_of_discrete.stronglyMeasurable_stoppedProcess hτ n

Похожие утверждения