integrableOn_isCompact — Mathlib

English

If h is antitone on s, then under suitable endpoint conditions, IntegrableOn f s μ holds when μ(s) is finite.

Русский

Если h антитононна на s, и μ(s) конечна, то IntegrableOn f s μ выполняется.

LaTeX

$$$\text{IntegrableOn}(f,s,\mu)$$$

Lean4

theorem integrableOn_isCompact [IsFiniteMeasureOnCompacts μ] (hs : IsCompact s) (hanti : AntitoneOn f s) :
    IntegrableOn f s μ :=
  memLp_one_iff_integrable.1 (hanti.memLp_isCompact hs)

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