English
If τ is a stopping time and u n are integrable, then the stoppedProcess u τ n is integrable for each n, by a finite-index decomposition.
Русский
Если τ — время останова и u n интегрируемы для каждого n, то stoppedProcess u τ n интегрируемо.
LaTeX
$$$\text{Integrable}(\text{stoppedProcess}(u, \tau, n), \mu)$$$
Lean4
theorem memLp_stoppedProcess_of_mem_finset (hτ : IsStoppingTime ℱ τ) (hu : ∀ n, MemLp (u n) p μ) (n : ι) {s : Finset ι}
(hbdd : ∀ ω, τ ω < n → τ ω ∈ s) : MemLp (stoppedProcess u τ n) p μ :=
by
rw [stoppedProcess_eq_of_mem_finset n hbdd]
refine MemLp.add ?_ ?_
· exact MemLp.indicator (ℱ.le n {a : Ω | n ≤ τ a} (hτ.measurableSet_ge n)) (hu n)
· suffices MemLp (fun ω => ∑ i ∈ s with i < n, {a : Ω | τ a = i}.indicator (u i) ω) p μ by convert this using 1;
ext1 ω; simp only [Finset.sum_apply]
refine memLp_finset_sum _ fun i _ => MemLp.indicator ?_ (hu i)
exact ℱ.le i {a : Ω | τ a = i} (hτ.measurableSet_eq i)
