English
Let a ≤ b be natural numbers and f: R → R be monotone on Icc(a, b). Then the integral from a to b is bounded above by the sum over i in Ico(a, b) of f(i+1).
Русский
Пусть a ≤ b — натуральные числа, и f: R → R монотонна на Icc(a, b). Тогда интеграл от a до b не превосходит суммы по i из Ico(a, b) от f(i+1).
LaTeX
$$$\\forall a,b \\in \\mathbb{N},\\ a \\le b,\\ \\forall f:\\mathbb{R}\\to\\mathbb{R},\\;\\operatorname{MonotoneOn} f (\\mathrm{Icc}\\ a.cast\\ b.cast) \\Rightarrow \\displaystyle \\int_{a}^{b} f(x) \\, dx \\le \\sum_{i \\in \\mathrm{Finset}.Ico\\ a\\ b} f(i+1).$$$
Lean4
theorem integral_le_sum_Ico (hab : a ≤ b) (hf : MonotoneOn f (Set.Icc a b)) :
(∫ x in a..b, f x) ≤ ∑ i ∈ Finset.Ico a b, f (i + 1 : ℕ) :=
by
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
exact hf.neg.sum_le_integral_Ico hab
