English
For a submartingale f with respect to a filtration, the expectation of stoppedValue at τ is less than or equal to that at π whenever τ ≤ π and both are bounded.
Русский
Для субмартингала f относительно фильтрации, если τ ≤ π и оба ограничены, то E[stoppedValue f τ] ≤ E[stoppedValue f π].
LaTeX
$$$ \\mu[stoppedValue f \\tau] \\le \\mu[stoppedValue f \\pi] $$$
Lean4
/-- Given a submartingale `f` and bounded stopping times `τ` and `π` such that `τ ≤ π`, the
expectation of `stoppedValue f τ` is less than or equal to the expectation of `stoppedValue f π`.
This is the forward direction of the optional stopping theorem. -/
theorem expected_stoppedValue_mono [SigmaFiniteFiltration μ 𝒢] (hf : Submartingale f 𝒢 μ) (hτ : IsStoppingTime 𝒢 τ)
(hπ : IsStoppingTime 𝒢 π) (hle : τ ≤ π) {N : ℕ} (hbdd : ∀ ω, π ω ≤ N) : μ[stoppedValue f τ] ≤ μ[stoppedValue f π] :=
by
rw [← sub_nonneg, ← integral_sub', stoppedValue_sub_eq_sum' hle hbdd]
· simp only [Finset.sum_apply]
have : ∀ i, MeasurableSet[𝒢 i] {ω : Ω | τ ω ≤ i ∧ i < π ω} :=
by
intro i
refine (hτ i).inter ?_
convert (hπ i).compl using 1
ext x
simp; rfl
rw [integral_finset_sum]
· refine Finset.sum_nonneg fun i _ => ?_
rw [integral_indicator (𝒢.le _ _ (this _)), integral_sub', sub_nonneg]
· exact hf.setIntegral_le (Nat.le_succ i) (this _)
· exact (hf.integrable _).integrableOn
· exact (hf.integrable _).integrableOn
intro i _
exact Integrable.indicator (Integrable.sub (hf.integrable _) (hf.integrable _)) (𝒢.le _ _ (this _))
· exact hf.integrable_stoppedValue hπ hbdd
· exact hf.integrable_stoppedValue hτ fun ω => le_trans (hle ω) (hbdd ω)
