theorem
MeasureTheory.Submartingale.expected_stoppedValue_mono_real
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : Measure Ω}
{𝒢 : Filtration ℕ m0}
{f : ℕ → Ω → ℝ}
{τ π : Ω → ℕ∞}
[SigmaFiniteFiltration μ 𝒢]
(hf : Submartingale f 𝒢 μ)
(hτ : IsStoppingTime 𝒢 τ)
(hπ : IsStoppingTime 𝒢 π)
(hle : τ ≤ π)
{N : ℕ}
(hbdd : ∀ (ω : Ω), π ω ≤ ↑N)
:
Optional stopping inequality for submartingales: if τ ≤ π are stopping times with π
bounded by some constant N, then E[f_τ] ≤ E[f_π]. This is the monotonicity of expected
stopped values along bounded stopping times.
theorem
MeasureTheory.Supermartingale.expected_stoppedValue_le
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : Measure Ω}
{𝒢 : Filtration ℕ m0}
{f : ℕ → Ω → ℝ}
{τ : Ω → ℕ∞}
[SigmaFiniteFiltration μ 𝒢]
(hf : Supermartingale f 𝒢 μ)
(hτ : IsStoppingTime 𝒢 τ)
{N : ℕ}
(hbdd : ∀ (ω : Ω), τ ω ≤ ↑N)
:
Optional stopping inequality for supermartingales: if τ is a bounded stopping time and
f is a supermartingale, then E[f_τ] ≤ E[f_0]. Dual of the submartingale version, obtained
by negating.