integrable_stoppedValue_of_mem_finset

English

If τ is a stopping time and u n are integrable, then stoppedValue u τ is integrable for finite index sets s with τ ω ∈ s.

Русский

Если τ — время останова и u n интегрируемы, то stoppedValue u τ интегрируемо для конечного множества индексов s, где τ ω ∈ s.

LaTeX

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

Lean4

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

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