integral_mono_on — Mathlib

English

If f is integrable with μ and nonnegative a.e., then the integral is nonnegative.

Русский

Если f интегрируема относительно μ и неотрицательна почти всюду, то интеграл неотрицателен.

LaTeX

$$$0 \\le ∫ f\\;dμ$ when $0 ≤^a_μ f$ and $f$ is integrable.$$

Lean4

theorem integral_mono_on (h : ∀ x ∈ Icc a b, f x ≤ g x) : (∫ u in a..b, f u ∂μ) ≤ ∫ u in a..b, g u ∂μ :=
  by
  let H x hx := h x <| Ioc_subset_Icc_self hx
  simpa only [integral_of_le hab] using setIntegral_mono_on hf.1 hg.1 measurableSet_Ioc H

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