English
A family of integrable functions f adapted to a filtration is a submartingale if for all i ≤ j, f i ≤ a.e. μ[f j | ℱ i] and each f i is integrable.
Русский
Семейство интегрируемых функций, адаптированное к фильтрации, является субмартингейлом, если для всех i ≤ j выполняется f i ≤ a.e. μ[f j | ℱ i] и каждый f i интегрируем.
LaTeX
$$$\\text{Submartingale}(f, \\mathcal{F}, \\mu) := \\text{Adapted }\\mathcal{F} f \\\\land (\\forall i j, i \\le j \\Rightarrow f(i) \\le_{ae} \\mu[f(j) | \\mathcal{F}(i)]) \\\\land \\forall i, Integrable(f(i), \\mu)$$$
Lean4
/-- A family of integrable functions `f : ι → Ω → E` is a submartingale with respect to a
filtration `ℱ` if `f` is adapted with respect to `ℱ` and for all `i ≤ j`,
`f i ≤ᵐ[μ] μ[f j | ℱ.le i]`. -/
def Submartingale [LE E] (f : ι → Ω → E) (ℱ : Filtration ι m0) (μ : Measure Ω) : Prop :=
Adapted ℱ f ∧ (∀ i j, i ≤ j → f i ≤ᵐ[μ] μ[f j|ℱ i]) ∧ ∀ i, Integrable (f i) μ
