leastGE — Mathlib

English

Let μ be finite. If f is Adapted to 𝒢 and f_i equals the conditional expectation of f_{i+1} given 𝒢_i almost surely, then f is a Martingale.

Русский

Пусть μ конечна. Если f адаптирован к 𝒢 и f_i равно условному ожиданию f_{i+1} при 𝒢_i почти наверняка, то f — мартингал.

LaTeX

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

Lean4

/-- `leastGE f r n` is the stopping time corresponding to the first time `f ≥ r`. -/
noncomputable def leastGE (f : ℕ → Ω → ℝ) (r : ℝ) (n : ℕ) :=
  hitting f (Set.Ici r) 0 n

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