stoppedProcess — Mathlib

English

If u is progressively measurable and τ is a stopping time, then the stoppedProcess u τ is progressively measurable.

Русский

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

LaTeX

$$$\text{ProgMeasurable}(f, \text{stoppedProcess}(u, \tau))$$$

Lean4

theorem stoppedProcess [PseudoMetrizableSpace ι] (h : ProgMeasurable f u) (hτ : IsStoppingTime f τ) :
    ProgMeasurable f (stoppedProcess u τ) :=
  h.comp (progMeasurable_min_stopping_time hτ) fun _ _ => min_le_left _ _

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