stoppedProcess — Mathlib

English

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

Русский

Если u адаптирован, а τ — время останова, то stoppedProcess(u, τ) адаптирован.

LaTeX

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

Lean4

/-- The stopped process of an adapted process with continuous paths is adapted. -/
theorem stoppedProcess [MetrizableSpace ι] (hu : Adapted f u) (hu_cont : ∀ ω, Continuous fun i => u i ω)
    (hτ : IsStoppingTime f τ) : Adapted f (stoppedProcess u τ) :=
  ((hu.progMeasurable_of_continuous hu_cont).stoppedProcess hτ).adapted

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