upcrossings_ae_lt_top — Mathlib

English

L¹-bounded submartingale has bounded upcrossings almost everywhere; in particular, for rational a<b the upcrossings is finite a.e.

Русский

У субмартингала в L¹ ограничены upcrossings почти наверно; для рациональных a<b—upcrossings конечны почти наверно.

LaTeX

$$$\\forall a

Lean4

theorem upcrossings_ae_lt_top [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ) (hbdd : ∀ n, eLpNorm (f n) 1 μ ≤ R) :
    ∀ᵐ ω ∂μ, ∀ a b : ℚ, a < b → upcrossings a b f ω < ∞ :=
  by
  simp only [ae_all_iff, eventually_imp_distrib_left]
  rintro a b hab
  exact hf.upcrossings_ae_lt_top' hbdd (Rat.cast_lt.2 hab)

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