English
An adapted integrable process is a submartingale if and only if for all bounded stopping times τ ≤ π, the stopped value inequality holds between τ and π.
Русский
Адаптированный интегрируемый процесс является субмартингалом тогда и только тогда, когда для всех ограниченных останова τ ≤ π выполняется неравенство между остановленными значениями τ и π.
LaTeX
$$$ \\text{Submartingale}(f,\\mathcal{G},\\mu) \\iff \\forall \\tau,\\pi,\\; \\tau \\le \\pi \\Rightarrow \\mu[stoppedValue f \\tau] \\le \\mu[stoppedValue f \\pi] $$$
Lean4
/-- The converse direction of the optional stopping theorem, i.e. an adapted integrable process `f`
is a submartingale if for all bounded stopping times `τ` and `π` such that `τ ≤ π`, the
stopped value of `f` at `τ` has expectation smaller than its stopped value at `π`. -/
theorem submartingale_of_expected_stoppedValue_mono [IsFiniteMeasure μ] (hadp : Adapted 𝒢 f)
(hint : ∀ i, Integrable (f i) μ)
(hf :
∀ τ π : Ω → ℕ,
IsStoppingTime 𝒢 τ →
IsStoppingTime 𝒢 π → τ ≤ π → (∃ N, ∀ ω, π ω ≤ N) → μ[stoppedValue f τ] ≤ μ[stoppedValue f π]) :
Submartingale f 𝒢 μ :=
by
refine submartingale_of_setIntegral_le hadp hint fun i j hij s hs => ?_
classical
specialize
hf (s.piecewise (fun _ => i) fun _ => j) _ (isStoppingTime_piecewise_const hij hs) (isStoppingTime_const 𝒢 j)
(fun x => (ite_le_sup _ _ (x ∈ s)).trans (max_eq_right hij).le) ⟨j, fun _ => le_rfl⟩
rwa [stoppedValue_const, stoppedValue_piecewise_const,
integral_piecewise (𝒢.le _ _ hs) (hint _).integrableOn (hint _).integrableOn, ←
integral_add_compl (𝒢.le _ _ hs) (hint j), add_le_add_iff_right] at hf
