integrable_stoppedValue — Mathlib

English

In the countable/finite setting, integrability passes to stoppedValue via a finite indicator decomposition.

Русский

В конечном/области счётности интегрируемость переносится к stoppedValue через конечную декомпозицию индикаторов.

LaTeX

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

Lean4

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

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