setIntegral_ge_of_const_le — Mathlib

English

If f ≥ 0 everywhere on s, then the integral over s is nonnegative.

Русский

Если f≥0 на всём s, то интеграл по s неотрицателен.

LaTeX

$$$$\\int_{x\\in s} f(x)\\,d\\mu \\ge 0.$$$$

Lean4

theorem setIntegral_ge_of_const_le {c : ℝ} (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (hf : ∀ x ∈ s, c ≤ f x)
    (hfint : IntegrableOn (fun x : X => f x) s μ) : c * μ.real s ≤ ∫ x in s, f x ∂μ :=
  by
  rw [mul_comm, ← smul_eq_mul, ← setIntegral_const c]
  exact setIntegral_mono_on (integrableOn_const hμs) hfint hs hf

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