English
Let s be measurable, f strongly measurable, and integrable. Then ∫_{f≤0} f ≤ ∫_s f, i.e., the integral over the sublevel set where f is nonpositive does not exceed the integral over s.
Русский
Пусть s — измеримо множество, f сильно измеримая и интегрируемая. Тогда ∫_{f≤0} f ≤ ∫_s f, то есть интеграл по подмножеству, где f неположителен, не превосходит интеграл по s.
LaTeX
$$$$\\int_{\\{y:\\, f(y) \\le 0\\}} f(x)\\,d\\mu(x) \\le \\int_{s} f(x)\\,d\\mu(x).$$$$
Lean4
theorem setIntegral_nonpos_le {s : Set X} (hs : MeasurableSet s) (hf : StronglyMeasurable f) (hfi : Integrable f μ) :
∫ x in {y | f y ≤ 0}, f x ∂μ ≤ ∫ x in s, f x ∂μ :=
by
rw [← integral_indicator hs, ← integral_indicator (hf.measurableSet_le stronglyMeasurable_const)]
exact
integral_mono (hfi.indicator (hf.measurableSet_le stronglyMeasurable_const)) (hfi.indicator hs)
(indicator_nonpos_le_indicator s f)
