stronglyMeasurable_limit_process'

English

LimitProcess f ℱ μ is a measurable selection defined by a conditional convergence criterion: it picks a limit g ω when a suitable a.e. convergence and measurability hold, otherwise 0.

Русский

LimitProcess f ℱ μ задаёт предел по условиям сходимости almost everywhere и измеримости, иначе принимает значение 0.

LaTeX

$$$\\mathrm{limitProcess}(f,\\mathcal F, μ) = \\begin{cases} g, & \\text{if } ∃g: Ω→E\\;\\text{with appropriate measurability and convergence a.e.} \\\\ 0, & \\text{otherwise} \\end{cases}$$$

Lean4

theorem stronglyMeasurable_limit_process' : StronglyMeasurable[m] (limitProcess f ℱ μ) :=
  stronglyMeasurable_limitProcess.mono (sSup_le fun _ ⟨_, hn⟩ => hn ▸ ℱ.le _)

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