stronglyMeasurable_stoppedProcess

English

If u is progressively measurable and τ is a stopping time, then stoppedProcess u τ is strongly measurable for each fixed time.

Русский

Если u прогрессивно измерима и τ — время останова, то stoppedProcess u τ является сильно измеримой по каждому фиксированному времени.

LaTeX

$$$\text{StronglyMeasurable}(\text{stoppedProcess}(u, \tau))$ for each time$$

Lean4

theorem stronglyMeasurable_stoppedProcess [PseudoMetrizableSpace ι] (hu : ProgMeasurable f u) (hτ : IsStoppingTime f τ)
    (i : ι) : StronglyMeasurable (MeasureTheory.stoppedProcess u τ i) :=
  (hu.adapted_stoppedProcess hτ i).mono (f.le _)

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