Math 2.0

Real functions Proposition

Comparison of a series and an integral

Builds on Riemann integral

Statement

Let aa be a real number, let nn be a natural number, and let f ⁣:[a,a+n]→ℝf \colon [a, a + n] \to \mathbb{R} be a decreasing function. Then ∑i=1nf(a+i)≤∫aa+nf(x) dx≤∑i=0n−1f(a+i).\sum_{i=1}^{n} f(a + i) \le \int_a^{a+n} f(x)\, dx \le \sum_{i=0}^{n-1} f(a + i).

Remarks

On each interval [a+i,a+i+1][a + i, a + i + 1] we have f(a+i+1)≤f(x)≤f(a+i)f(a + i + 1) \le f(x) \le f(a + i). Integrate and add over ii. The integral exists because monotone functions are Riemann integrable. With f(x)=1/xf(x) = 1/x and a=1a = 1 it gives ln⁡(n+1)≤Hn≤1+ln⁡n\ln(n + 1) \le H_n \le 1 + \ln n for the harmonic numbers. Mathlib states the first inequality as AntitoneOn.sum_le_integral.

Reading path

To understand this page from the ground up, read these 6 pages in order. The foundations come first.

Show the path as a graph
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Partition of an interval definition
  2. Mesh of a partition definition
  3. Riemann sum definition
  4. Riemann integrable function definition
  5. Riemann integral definition
  6. Comparison of a series and an integral statement

Where this leads

1 page builds on this one.

Further reading

  1. Web https://en.wikipedia.org/wiki/Integral_test_for_convergence, Proof
About this page
Tag069HKV4X1E
URIm2://069HKV4X1E
Kindstatement, proposition
WritingW1 stated
MSC26A42
StatusThis copy of the site has no build data. Run m2 status 069HKV4X1E.
UsesRiemann integral

Markdown · JSON · Edit on GitHub

What this page needs for W2

  • edge about out: the concepts that the statement is about (0 of 1)
  • edge proves in: at least one proof node (0 of 1)
  • edge instance_of or illustrates in: one example that shows the statement at work (0 of 1)
  • explanation L2 (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

Used by