English
If μ is finite, f is a submartingale, r ≥ 0, f(0) = 0, and the increments are almost surely bounded by R, then for each i we have the eLpNorm (stoppedValue f (leastGE f r i)) with parameter 1 is bounded above by 2 μ(Ω) ENNReal.ofReal(r+R).
Русский
Пусть μ конечна, f — субмартingale, r ≥ 0, f(0)=0, и при a.e. выполняются |f(i+1)-f(i)| ≤ R. Тогда для каждого i выполнено: eLpNorm(stoppedValue(f, leastGE(f,r,i)), 1) ≤ 2 μ(Ω) ENNReal.ofReal(r+R).
LaTeX
$$$$\text{If } [IsFiniteMeasure \mu],\; hf:\ Submartingale f\, \mathcal{F}\, \mu,\; hr\ge 0,\; hf_0:\ f(0)=0,\; hbdd:\forall^*\omega:\forall i:\, |f(i+1)\omega - f(i)\omega| \le R \Rightarrow \\ eLpNorm(\mathrm{stoppedValue}(f, \mathrm{leastGE}(f,r,i)) , 1, \mu) \le 2 \mu(\Omega) ENNReal.ofReal(r+R). $$$$
Lean4
theorem stoppedValue_leastGE_eLpNorm_le [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ) (hr : 0 ≤ r) (hf0 : f 0 = 0)
(hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) (i : ℕ) :
eLpNorm (stoppedValue f (leastGE f r i)) 1 μ ≤ 2 * μ Set.univ * ENNReal.ofReal (r + R) :=
by
refine
eLpNorm_one_le_of_le' ((hf.stoppedValue_leastGE r).integrable _) ?_ (norm_stoppedValue_leastGE_le hr hf0 hbdd i)
rw [← setIntegral_univ]
refine le_trans ?_ ((hf.stoppedValue_leastGE r).setIntegral_le (zero_le _) MeasurableSet.univ)
simp_rw [stoppedValue, leastGE, hitting_of_le le_rfl, hf0, integral_zero', le_rfl]
