English
A process is a submartingale iff it is adapted, integrable at every time, and increment expectations are nonnegative in the conditional sense.
Русский
Процесс является субмартингалом тогда и только тогда, когда он адаптирован, интегрируем на каждом моменте, а условные ожидания приращений неотрицательны.
LaTeX
$$$\mathrm{Submartingale}(f,\mathcal{F},\mu) \iff \big( \mathrm{Adapted}(\mathcal{F},f) \land (\forall i, \mathrm{Integrable}(f(i),\mu)) \land (\forall i,j, i\le j, 0 \le_{a.e.} \mu[f_j - f_i|\mathcal{F}_i]) \big)$$$
Lean4
theorem submartingale_iff_condExp_sub_nonneg [SigmaFiniteFiltration μ ℱ] {f : ι → Ω → ℝ} :
Submartingale f ℱ μ ↔ Adapted ℱ f ∧ (∀ i, Integrable (f i) μ) ∧ ∀ i j, i ≤ j → 0 ≤ᵐ[μ] μ[f j - f i|ℱ i] :=
⟨fun h => ⟨h.adapted, h.integrable, fun _ _ => h.condExp_sub_nonneg⟩, fun ⟨hadp, hint, h⟩ =>
submartingale_of_condExp_sub_nonneg hadp hint h⟩
