English
For a nonnegative submartingale f, the Doob maximal inequality provides an upper bound for the probability (or measure) that the running maximum exceeds a level ε, in terms of the last value f_n and an integral bound.
Русский
Для неотрицательного субмартингала Doob неравенство максимума даёт верхнюю границу на вероятность того, что максимум до n превысит уровень ε, через последнее значение f_n и интегральное ограничение.
LaTeX
$$$ ε \\cdot μ\\{ω : ε ≤ \\sup_{0≤k≤n} f_k(ω)\\} ≤ \\mathbb{E}_μ[ f_n \\mathbf{1}_{\\{ε ≤ \\sup_{0≤k≤n} f_k\\}} ] $$$
Lean4
/-- **The optional stopping theorem** (fair game theorem): an adapted integrable process `f`
is a submartingale if and only 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_iff_expected_stoppedValue_mono [IsFiniteMeasure μ] (hadp : Adapted 𝒢 f)
(hint : ∀ i, Integrable (f i) μ) :
Submartingale f 𝒢 μ ↔
∀ τ π : Ω → ℕ,
IsStoppingTime 𝒢 τ →
IsStoppingTime 𝒢 π → τ ≤ π → (∃ N, ∀ x, π x ≤ N) → μ[stoppedValue f τ] ≤ μ[stoppedValue f π] :=
⟨fun hf _ _ hτ hπ hle ⟨_, hN⟩ => hf.expected_stoppedValue_mono hτ hπ hle hN,
submartingale_of_expected_stoppedValue_mono hadp hint⟩
