memLp_limitProcess — Mathlib

English

The limit process of a submartingale is in Lp for any p, given Lp-bounds on f_n and Sigma-finiteness.

Русский

Лемма о принадлежности лимит-процесса в Lp при заданных ограничениях Lp на f_n и условиях сигма-финичности.

LaTeX

$$$\\mathrm{MemLp}(\\mathcal{F}.\\mathrm{limitProcess}(f,\\mu))\\; p\\; \\mu.$$$

Lean4

/-- The limiting process of an Lᵖ-bounded submartingale is Lᵖ. -/
theorem memLp_limitProcess {p : ℝ≥0∞} (hf : Submartingale f ℱ μ) (hbdd : ∀ n, eLpNorm (f n) p μ ≤ R) :
    MemLp (ℱ.limitProcess f μ) p μ :=
  memLp_limitProcess_of_eLpNorm_bdd (fun n => ((hf.stronglyMeasurable n).mono (ℱ.le n)).aestronglyMeasurable) hbdd

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