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 | 𝒢_i]) \\Rightarrow \\text{Submartingale}(f, 𝒢, μ).$$$
Lean4
/-- A predictable submartingale is a.e. greater equal than its initial state. -/
theorem zero_le_of_predictable [Preorder E] [SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E} (hfmgle : Submartingale f 𝒢 μ)
(hfadp : Adapted 𝒢 fun n => f (n + 1)) (n : ℕ) : f 0 ≤ᵐ[μ] f n := by
induction n with
| zero => rfl
| succ k ih =>
exact
ih.trans
((hfmgle.2.1 k (k + 1) k.le_succ).trans_eq <|
Germ.coe_eq.mp <|
congr_arg Germ.ofFun <| condExp_of_stronglyMeasurable (𝒢.le _) (hfadp _) <| hfmgle.integrable _)
