setLIntegral_lt_top_of_le_nnreal — Mathlib

English

Lebesgue integral of a nonnegative function over a set of finite measure is finite provided it is bounded above on that set.

Русский

Лебегов интеграл неотрицательной функции по множеству конечной меры конечен, если функция ограничена сверху на этом множестве.

LaTeX

$$$$\\int_{a\\in s} f(a) \\, 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_le_nnreal {s : Set α} (hs : μ s ≠ ∞) {f : α → ℝ≥0∞}
    (hbdd : ∃ y : ℝ≥0, ∀ x ∈ s, f x ≤ y) : ∫⁻ x in s, f x ∂μ < ∞ :=
  by
  obtain ⟨M, hM⟩ := hbdd
  refine lt_of_le_of_lt (setLIntegral_mono measurable_const hM) ?_
  simp [ENNReal.mul_lt_top, hs.lt_top]

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