English
Let μ be finite. If f: ℕ → Ω → ℝ is adapted to 𝒢, integrable, and for all i we have 0 ≤ᵐ[μ] μ[f_{i+1} − f_i | 𝒢_i], then f is a Submartingale.
Русский
Пусть μ конечна. Если f адаптирован к 𝒢, интегрируем, и для всех i верно 0 ≤ᵐ μ[ f_{i+1} − f_i | 𝒢_i], то f — субмартингал.
LaTeX
$$$[IsFiniteMeasure \\ μ] \\Rightarrow (Adapted 𝒢 f) \\land (\\forall i, Integrable (f_i) \\ μ) \\land (\\forall i, 0 \\le^{\\text{ae}}_μ μ[f_{i+1} - f_i \\mid \\mathcal{G}_i]) \Rightarrow \\text{Submartingale}(f, 𝒢, μ).$$$
Lean4
theorem submartingale_of_condExp_sub_nonneg_nat [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ} (hadp : Adapted 𝒢 f)
(hint : ∀ i, Integrable (f i) μ) (hf : ∀ i, 0 ≤ᵐ[μ] μ[f (i + 1) - f i|𝒢 i]) : Submartingale f 𝒢 μ :=
by
refine submartingale_nat hadp hint fun i => ?_
rw [← condExp_of_stronglyMeasurable (𝒢.le _) (hadp _) (hint _), ← eventually_sub_nonneg]
exact EventuallyLE.trans (hf i) (condExp_sub (hint _) (hint _) _).le
