setIntegral_le_nonneg — Mathlib

English

If f is integrable and nonnegative, then the integral over s is less than or equal to the integral over the whole space.

Русский

Если f интегрируемо и неотрицательно, то ∫_s f ≤ ∫ f по всему space.

LaTeX

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

Lean4

theorem setIntegral_le_nonneg {s : Set X} (hs : MeasurableSet s) (hf : StronglyMeasurable f) (hfi : Integrable f μ) :
    ∫ x in s, f x ∂μ ≤ ∫ x in {y | 0 ≤ f y}, f x ∂μ :=
  by
  rw [← integral_indicator hs, ← integral_indicator (stronglyMeasurable_const.measurableSet_le hf)]
  exact
    integral_mono (hfi.indicator hs) (hfi.indicator (stronglyMeasurable_const.measurableSet_le hf))
      (indicator_le_indicator_nonneg s f)

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