setLIntegral_lt_top_of_bddAbove — Mathlib

English

If μ(s) ≠ ∞ and f is bounded above by some NNReal value on s, then the lintegral of f (viewed as ENNReal) over s is finite.

Русский

Если μ(s) не бесконечно и f ограничена сверху на s в виде NNReal, то линегральный интеграл f на s (как ENNReal) конечен.

LaTeX

$$$$\\text{If } \\exists y\\in\\mathbb{R}_{\\ge 0}, \\forall x\\in s, f(x) \\le y \\quad\\Rightarrow\\quad \\int_{x\\in s} f(x) \\, d\\mu < \\infty.$$$$

Lean4

/-- Lebesgue integral of a bounded function over a set of finite measure is finite.
Note that this lemma assumes no regularity of either `f` or `s`. -/
theorem setLIntegral_lt_top_of_bddAbove {s : Set α} (hs : μ s ≠ ∞) {f : α → ℝ≥0} (hbdd : BddAbove (f '' s)) :
    ∫⁻ x in s, f x ∂μ < ∞ :=
  setLIntegral_lt_top_of_le_nnreal hs <| hbdd.imp fun _M hM _x hx ↦ ENNReal.coe_le_coe.2 <| hM (mem_image_of_mem f hx)

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