memLp_stoppedProcess — Mathlib

English

If τ is a stopping time and each u n is MemLp, then stoppedProcess u τ n is MemLp for each n.

Русский

Если τ — время останова и каждый u n принадлежит MemLp, то stoppedProcess(u, τ, n) принадлежит MemLp для каждого n.

LaTeX

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

Lean4

theorem memLp_stoppedProcess [LocallyFiniteOrderBot ι] (hτ : IsStoppingTime ℱ τ) (hu : ∀ n, MemLp (u n) p μ) (n : ι) :
    MemLp (stoppedProcess u τ n) p μ :=
  memLp_stoppedProcess_of_mem_finset hτ hu n fun _ h => Finset.mem_Iio.mpr h

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