mathlib3

533c67bc - feat(analysis/sum_integral_comparisons): Comparison lemmas between finite sums and integrals (#13179)

feat(analysis/sum_integral_comparisons): Comparison lemmas between finite sums and integrals (#13179) In this pull request we target the following lemmas: ```lean lemma antitone_on.integral_le_sum {x₀ : ℝ} {a : ℕ} {f : ℝ → ℝ} (hf : antitone_on f (Icc x₀ (x₀ + a))) : ∫ x in x₀..(x₀ + a), f x ≤ ∑ i in finset.range a, f (x₀ + i) lemma antitone_on.sum_le_integral {x₀ : ℝ} {a : ℕ} {f : ℝ → ℝ} (hf : antitone_on f (Icc x₀ (x₀ + a))) : ∑ i in finset.range a, f (x₀ + i + 1) ≤ ∫ x in x₀..(x₀ + a), f x := ``` as well as their `monotone_on` equivalents. These lemmas are critical to many analytic facts, specifically because it so often is the way that error terms end up getting computed. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>