iInf_mul_le_setLIntegral — Mathlib

English

For a function f on α, the infimum over a measurable set s of f times μ(s) is a lower bound for the restricted lintegral.

Русский

Инфикс инфимума f на множестве s, умноженный на μ(s), ниже ограничивает линеграл по s.

LaTeX

$$$$ (\inf x \in s, f(x)) \cdot μ(s) ≤ ∫^- x in s, f(x) ∂ μ. $$$$

Lean4

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

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