English
If μ is finite and f is a Submartingale with bounded increments, then for almost every ω, boundedness of the range {f n ω} implies existence of a limit: there exists c with Tendsto f n ω to c as n→∞.
Русский
Пусть μ конечна, f — субмартингал с ограниченными приращениями; почти наверняка существует предел последовательности f n ω как n → ∞, если диапазон ограничен.
LaTeX
$$$$[IsFiniteMeasure \mu]\; \text{hf : Submartingale } f,\; hf_0 : f(0)=0,\; hbdd: \forall^* \omega \partial\mu, \forall i, |f(i+1)\omega - f(i)\omega| \le R \Rightarrow \forall^* \omega,\, BddAbove (\{f n(\omega) : n\in\mathbb{N}\}) \Rightarrow \exists c, \lim_{n\to\infty} f n(\omega) = c.$$$$
Lean4
/-- This lemma is superseded by `Submartingale.bddAbove_iff_exists_tendsto`. -/
theorem exists_tendsto_of_abs_bddAbove_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
have ht : ∀ᵐ ω ∂μ, ∀ i : ℕ, ∃ c, Tendsto (fun n => stoppedValue f (leastGE f i n) ω) atTop (𝓝 c) :=
by
rw [ae_all_iff]
exact fun i =>
Submartingale.exists_ae_tendsto_of_bdd (hf.stoppedValue_leastGE i)
(hf.stoppedValue_leastGE_eLpNorm_le' i.cast_nonneg hf0 hbdd)
filter_upwards [ht] with ω hω hωb
rw [BddAbove] at hωb
obtain ⟨i, hi⟩ := exists_nat_gt hωb.some
have hib : ∀ n, f n ω < i := by
intro n
exact lt_of_le_of_lt ((mem_upperBounds.1 hωb.some_mem) _ ⟨n, rfl⟩) hi
have heq : ∀ n, stoppedValue f (leastGE f i n) ω = f n ω :=
by
intro n
rw [leastGE]; unfold hitting; rw [stoppedValue]
rw [if_neg]
simp only [Set.mem_Icc, Set.mem_Ici]
push_neg
exact fun j _ => hib j
simp only [← heq, hω i]
