memLp_stoppedValue — Mathlib

English

Under mild assumptions, if τ is a stopping time and u is MemLp for all n, then stoppedValue u τ is MemLp.

Русский

При умеренных предпосылках, если τ — время останова и u действует в MemLp для всех n, то stoppedValue u τ также в MemLp.

LaTeX

$$$\text{MemLp}(\text{stoppedValue}(u, \tau), p, \mu)$$$

Lean4

theorem memLp_stoppedValue [LocallyFiniteOrderBot ι] (hτ : IsStoppingTime ℱ τ) (hu : ∀ n, MemLp (u n) p μ) {N : ι}
    (hbdd : ∀ ω, τ ω ≤ N) : MemLp (stoppedValue u τ) p μ :=
  memLp_stoppedValue_of_mem_finset hτ hu fun ω => Finset.mem_Iic.mpr (hbdd ω)

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