English
Let μ be finite, f: ℕ → Ω → ℝ adapted to 𝒢 and integrable. If for each i, f_i ≤ᵐ μ[ f_{i+1} | 𝒢_i], then f is a Submartingale with respect to 𝒢 and μ.
Русский
Пусть μ — конечная мера, f: ℕ → Ω → ℝ адаптирован к 𝒢 и интегрируем. Если для каждого i верно f_i ≤ f_{i+1} условно по 𝒢_i, то f — субмартингал.
LaTeX
$$$[IsFiniteMeasure \\ μ] \\Rightarrow (Adapted 𝒢 f) \\land (\\forall i, Integrable (f_i) \\ μ) \\land (\\forall i, f_i \\le^{\\text{ae}}_{μ} \\mathbb{E}[f_{i+1} \\mid \\mathcal{G}_i]) \\Rightarrow \\text{Submartingale}(f, 𝒢, μ).$$$
Lean4
theorem submartingale_nat [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ} (hadp : Adapted 𝒢 f) (hint : ∀ i, Integrable (f i) μ)
(hf : ∀ i, f i ≤ᵐ[μ] μ[f (i + 1)|𝒢 i]) : Submartingale f 𝒢 μ :=
by
refine submartingale_of_setIntegral_le_succ hadp hint fun i s hs => ?_
have : ∫ ω in s, f (i + 1) ω ∂μ = ∫ ω in s, (μ[f (i + 1)|𝒢 i]) ω ∂μ := (setIntegral_condExp (𝒢.le i) (hint _) hs).symm
rw [this]
exact setIntegral_mono_ae (hint i).integrableOn integrable_condExp.integrableOn (hf i)
