bddAbove_iff_exists_tendsto_aux — Mathlib

English

Under IsFiniteMeasure, for Submartingale f with bounded increments, almost surely the set {f n ω} is bounded above iff there exists a limit of f n ω as n tends to infinity.

Русский

При условии конечной меры и ограниченных приращений субмартингала, почти наверняка множество значений является ограниченным сверху тогда и только тогда существует предел последовательности.

LaTeX

$$$$\\forall^* \\omega \\partial\\mu,\; BddAbove(\\{f n(\\omega) : n\\in\\mathbb{N}\\}) \\iff \\exists c, \\lim_{n\\to\\infty} f n(\\omega) = c.$$$$

Lean4

theorem bddAbove_iff_exists_tendsto_aux [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ) (hf0 : f 0 = 0)
    (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) :
    ∀ᵐ ω ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) := by
  filter_upwards [hf.exists_tendsto_of_abs_bddAbove_aux hf0 hbdd] with ω hω using ⟨hω, fun ⟨c, hc⟩ => hc.bddAbove_range⟩

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