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