martingale_const — Mathlib

English

The constant process f(i) = x is a martingale for any filtration, finite measure μ, and any x ∈ E.

Русский

Пусть f(i) = x константа; тогда для любой фильтрации, сколь угодно мера μ и любой x ∈ E, процесс является мартингейлом.

LaTeX

$$$\\text{Martingale}(\\lambda i. x, \\mathcal{F}, \\mu)$$$

Lean4

theorem martingale_const (ℱ : Filtration ι m0) (μ : Measure Ω) [IsFiniteMeasure μ] (x : E) :
    Martingale (fun _ _ => x) ℱ μ :=
  ⟨adapted_const ℱ _, fun i j _ => by rw [condExp_const (ℱ.le _)]⟩

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