English
Under finite measure μ, hf a Submartingale, hr ≥ 0, hf0, hbdd as above, then for all i, the same inequality holds with ENNReal toNNReal normalization.
Русский
При конечной мере μ и при тех же предпосылках для субмартинграла, предел в норме eLp с параметром 1 ограничен через ENNReal.toNNReal аналогично предыдущей формуле.
LaTeX
$$$$\text{For all } i,\; eLpNorm(\mathrm{stoppedValue}(f, \mathrm{leastGE}(f,r,i)) , 1, \mu) \le ENNReal.toNNReal \big(2 \mu(\Omega) ENNReal.ofReal(r+R)\big). $$$$
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 μ ≤ ENNReal.toNNReal (2 * μ Set.univ * ENNReal.ofReal (r + R)) :=
by
refine (hf.stoppedValue_leastGE_eLpNorm_le hr hf0 hbdd i).trans ?_
simp [ENNReal.coe_toNNReal (measure_ne_top μ _), ENNReal.coe_toNNReal]
