English
Let f: R → R be a function and x0 ∈ R, a ∈ N. If f is monotone on the closed interval [x0, x0 + a], then the integral of f over [x0, x0 + a] is bounded above by the sum of its values at the right endpoints: ∫_{x0}^{x0+a} f(x) dx ≤ ∑_{i=0}^{a−1} f(x0 + i + 1).
Русский
Пусть f: R → R, x0 ∈ R и a ∈ N. Если f монотонна на отрезке [x0, x0 + a], то интеграл по этому отрезку не превосходит сумму значений f в точках x0+1, x0+2, ..., x0+a: ∫_{x0}^{x0+a} f(x) dx ≤ ∑_{i=0}^{a−1} f(x0 + i + 1).
LaTeX
$$$\\forall x_0 \\in \\mathbb{R}, \\forall a \\in \\mathbb{N}, \\forall f: \\mathbb{R} \\to \\mathbb{R},\\;\\big(\\operatorname{MonotoneOn} f (\\mathrm{Icc}(x_0, x_0 + a))\\big) \\Rightarrow \\displaystyle \\int_{x_0}^{x_0 + a} f(x) \\, dx \\le \\sum_{i=0}^{a-1} f(x_0 + i + 1).$$$
Lean4
theorem integral_le_sum (hf : MonotoneOn f (Icc x₀ (x₀ + a))) :
(∫ x in x₀..x₀ + a, f x) ≤ ∑ i ∈ Finset.range a, f (x₀ + (i + 1 : ℕ)) :=
by
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
exact hf.neg.sum_le_integral
