integrable_stoppedValue — Mathlib

English

As above: discrete submartingale with natural-number indexing under adaptedness and integrability conditions.

Русский

Как выше: дискретный субмартингал с индексированием по натовым номерам при адаптации и интегрируемости.

LaTeX

$$$[IsFiniteMeasure \\ μ] \\Rightarrow (Adapted 𝒢 f) \\land (\\forall i, Integrable (f i) \\ μ) \\land (\\forall i, (f_i) \\le^{\\text{ae}} μ[f_{i+1}|𝒢_i]) \\Rightarrow \\text{Submartingale}(f, 𝒢, μ).$$$

Lean4

protected theorem integrable_stoppedValue [LE E] {f : ℕ → Ω → E} (hf : Submartingale f 𝒢 μ) {τ : Ω → ℕ}
    (hτ : IsStoppingTime 𝒢 τ) {N : ℕ} (hbdd : ∀ ω, τ ω ≤ N) : Integrable (stoppedValue f τ) μ :=
  integrable_stoppedValue ℕ hτ hf.integrable hbdd

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