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