setLIntegral_le_iSup_mul — Mathlib

English

Let f: α → ℝ≥0∞ be a nonnegative function and s ⊆ α a measurable set. Then the restricted Lebesgue integral over s is at most the essential bound of f on s times μ(s): ∫_s f dμ ≤ (sup_{x∈s} f(x)) · μ(s).

Русский

Пусть f: α → ℝ≥0∞ неотрицательно и s ⊆ α измеримо. Тогда линегральный интеграл по s не превосходит произведение меры μ(s) на верхнюю границу f на s: ∫_s f dμ ≤ (sup_{x∈s} f(x)) · μ(s).

LaTeX

$$$\\int_s f \\, d\\mu \\le \\left(\\sup_{x \\in s} f(x)\\right) \\mu(s)$$$

Lean4

theorem setLIntegral_le_iSup_mul (f : α → ℝ≥0∞) {s : Set α} (hs : MeasurableSet s) :
    ∫⁻ x in s, f x ∂μ ≤ (⨆ x ∈ s, f x) * μ s := by
  calc
    ∫⁻ x in s, f x ∂μ
    _ ≤ ∫⁻ y in s, ⨆ x ∈ s, f x ∂μ := (setLIntegral_mono' hs fun x hx ↦ le_iSup₂ (f := fun x _ ↦ f x) x hx)
    _ = (⨆ x ∈ s, f x) * μ s := by simp

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