English
Let μ be finite and f: ℕ → Ω → ℝ adapted to 𝒢. If for all i we have f_i =ᵐ[μ] μ[f_{i+1} | 𝒢_i], then f is a Martingale 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 =^{\\text{ae}}_{μ} \\mathbb{E}[f_{i+1} \\mid \\mathcal{G}_i]) \\Rightarrow \\text{Martingale}(f, 𝒢, μ).$$$
Lean4
theorem supermartingale_nat [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ} (hadp : Adapted 𝒢 f) (hint : ∀ i, Integrable (f i) μ)
(hf : ∀ i, μ[f (i + 1)|𝒢 i] ≤ᵐ[μ] f i) : Supermartingale f 𝒢 μ :=
by
rw [← neg_neg f]
refine
(submartingale_nat hadp.neg (fun i => (hint i).neg) fun i => EventuallyLE.trans ?_ (condExp_neg ..).symm.le).neg
filter_upwards [hf i] with x hx using neg_le_neg hx
