stronglyMeasurable_limitProcess — Mathlib

English

If a sequence f n is AEStronglyMeasurable and eLpNorm (f n) p μ ≤ R for all n, then MemLp (limitProcess f ℱ μ) p μ.

Русский

Если последовательность результативности сильного математического ожидания обеспечивает AEStronglyMeasurable и eLpNorm ограничена на каждом n, то limitProcess принадлежит MemLp.

LaTeX

$$$\\forall n,\\ AEStronglyMeasurable(f_n, μ) \\wedge \\forall n, eLpNorm(f_n, p, μ) \\le R \\Rightarrow MemLp(\\mathrm{limitProcess}\\, f\\, \\mathcal F\\, μ)\\ p\\ μ$$$

Lean4

theorem stronglyMeasurable_limitProcess : StronglyMeasurable[⨆ n, ℱ n] (limitProcess f ℱ μ) :=
  by
  rw [limitProcess]
  split_ifs with h
  exacts [(Classical.choose_spec h).1, stronglyMeasurable_zero]

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