integrable_stoppedProcess_of_mem_finset

English

Under mild hypotheses, stoppedProcess with finite index set preserves integrability.

Русский

При умеренных предпосылках остановленный процесс с конечным индексом сохраняет интегрируемость.

LaTeX

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

Lean4

theorem integrable_stoppedProcess_of_mem_finset (hτ : IsStoppingTime ℱ τ) (hu : ∀ n, Integrable (u n) μ) (n : ι)
    {s : Finset ι} (hbdd : ∀ ω, τ ω < n → τ ω ∈ s) : Integrable (stoppedProcess u τ n) μ :=
  by
  simp_rw [← memLp_one_iff_integrable] at hu ⊢
  exact memLp_stoppedProcess_of_mem_finset hτ hu n hbdd

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