supermartingale_of_condExp_sub_nonneg_nat

English

Let μ be finite. If f: ℕ → Ω → ℝ is Adapted to 𝒢, and for all i, 0 ≤ᵐ[μ] μ[f i+1 − f i | 𝒢 i], then f is a Martingale.

Русский

Пусть μ конечна. Если f адаптирован к 𝒢 и для всех i верно 0 ≤ᵐ μ[f_{i+1} − f_i | 𝒢_i], тогда f — мартингал.

LaTeX

$$$[IsFiniteMeasure \\ μ] \\Rightarrow (Adapted 𝒢 f) \\land (\\forall i, 0 \\le^{\\text{ae}}_μ μ[f_{i+1} - f_i | \\mathcal{G}_i]) \\Rightarrow \\text{Martingale}(f, 𝒢, μ).$$$

Lean4

theorem supermartingale_of_condExp_sub_nonneg_nat [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ} (hadp : Adapted 𝒢 f)
    (hint : ∀ i, Integrable (f i) μ) (hf : ∀ i, 0 ≤ᵐ[μ] μ[f i - f (i + 1)|𝒢 i]) : Supermartingale f 𝒢 μ :=
  by
  rw [← neg_neg f]
  refine (submartingale_of_condExp_sub_nonneg_nat hadp.neg (fun i => (hint i).neg) ?_).neg
  simpa only [Pi.zero_apply, Pi.neg_apply, neg_sub_neg]

Похожие утверждения