integrable_stoppedProcess — Mathlib

English

If τ is a stopping time and all u n are integrable, then the stoppedProcess is integrable for all n.

Русский

Если τ — время останова и все u n интегрируемы, тогда stoppedProcess интегрируемо для всех n.

LaTeX

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

Lean4

theorem integrable_stoppedProcess [LocallyFiniteOrderBot ι] (hτ : IsStoppingTime ℱ τ) (hu : ∀ n, Integrable (u n) μ)
    (n : ι) : Integrable (stoppedProcess u τ n) μ :=
  integrable_stoppedProcess_of_mem_finset hτ hu n fun _ h => Finset.mem_Iio.mpr h

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