sigmaFinite_stopping_time — Mathlib

English

If τ is a stopping time with respect to a sigma-finite filtration, then the trimmed measure μ|__{τ} is sigma-finite.

Русский

Если τ является временем останова относительно сигма-конечной фильтрации, то обрезанная мера μ|τ является сигма-конечной.

LaTeX

$$$\text{If } h_τ \text{ is a stopping time and } μ \text{ is sigma-finite relative to } f, \; μ^{\text{trim}}_{h_τ} \text{ is sigma-finite.}$$$

Lean4

instance sigmaFinite_stopping_time {ι} [SemilatticeSup ι] [OrderBot ι] [(Filter.atTop : Filter ι).IsCountablyGenerated]
    {μ : Measure Ω} {f : Filtration ι m} {τ : Ω → ι} [SigmaFiniteFiltration μ f] (hτ : IsStoppingTime f τ) :
    SigmaFinite (μ.trim hτ.measurableSpace_le) :=
  by
  refine @sigmaFiniteTrim_mono _ _ ?_ _ _ _ ?_ ?_
  · exact f ⊥
  · exact hτ.le_measurableSpace_of_const_le fun _ => bot_le
  · infer_instance

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