English
If a finite-measure martingale is almost surely non-decreasing in n and its predictable part converges, then the martingale converges to the same limit a.s.
Русский
Если мартингал над мерой с конечной мерой почти наверняка возрастает по n и предсказуемая часть сходится, то сам мартингал сходится к тому же пределу почти наверняка.
LaTeX
$$$$\text{If } \forall^*\omega, f(n,\omega) \uparrow f(\infty,\omega) \text{ and } \mathrm{predictablePart} f \text{ converges, then } f(n,\omega) \to L(\omega)\text{ a.e.}$$$$
Lean4
theorem ae_not_tendsto_atTop_atTop [IsFiniteMeasure μ] (hf : Martingale f ℱ μ)
(hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) : ∀ᵐ ω ∂μ, ¬Tendsto (fun n => f n ω) atTop atTop := by
filter_upwards [hf.bddAbove_range_iff_bddBelow_range hbdd] with ω hω htop using
not_bddAbove_of_tendsto_atTop htop (hω.2 <| bddBelow_range_of_tendsto_atTop_atTop htop)
