memLp_stoppedValue_of_mem_finset — Mathlib

English

If τ is a stopping time and u is p-integrable for all indices, and s is finite with τ ω ∈ s, then stoppedValue u τ is p-integrable.

Русский

Если τ — время останова и u ∈ MemLp для всех индексов, и s конечно, причем τ ω ∈ s, тогда stoppedValue u τ ∈ MemLp.

LaTeX

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

Lean4

theorem memLp_stoppedValue_of_mem_finset (hτ : IsStoppingTime ℱ τ) (hu : ∀ n, MemLp (u n) p μ) {s : Finset ι}
    (hbdd : ∀ ω, τ ω ∈ s) : MemLp (stoppedValue u τ) p μ :=
  by
  rw [stoppedValue_eq_of_mem_finset hbdd]
  refine memLp_finset_sum' _ fun i _ => MemLp.indicator ?_ (hu i)
  refine ℱ.le i {a : Ω | τ a = i} (hτ.measurableSet_eq_of_countable_range ?_ i)
  refine ((Finset.finite_toSet s).subset fun ω hω => ?_).countable
  obtain ⟨y, rfl⟩ := hω
  exact hbdd y

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