sigmaFinite_stopping_time_of_le — Mathlib

English

If a stopping time τ is bounded above by n, then the trimmed measure μ.trim(hτ.measurableSpace_le_of_le hτ_le) is sigma-finite.

Русский

Если остановочное время τ ограничено сверху константой n, то обрезанная мера является сигма-конечной.

LaTeX

$$$\text{If } τ(ω) \le n \; \forall ω, \; μ_{\text{trim}}^{h_τ(≤)} \text{ is sigma-finite.}$$$

Lean4

instance sigmaFinite_stopping_time_of_le {ι} [SemilatticeSup ι] [OrderBot ι] {μ : Measure Ω} {f : Filtration ι m}
    {τ : Ω → ι} [SigmaFiniteFiltration μ f] (hτ : IsStoppingTime f τ) {n : ι} (hτ_le : ∀ ω, τ ω ≤ n) :
    SigmaFinite (μ.trim (hτ.measurableSpace_le_of_le hτ_le)) :=
  by
  refine @sigmaFiniteTrim_mono _ _ ?_ _ _ _ ?_ ?_
  · exact f ⊥
  · exact hτ.le_measurableSpace_of_const_le fun _ => bot_le
  · infer_instance

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