Comparison of a series and an integral
Builds on Riemann integral
Statement
Let be a real number, let be a natural number, and let be a decreasing function. Then
Remarks
On each interval we have . Integrate and add over .
The integral exists because monotone functions are Riemann integrable.
With and it gives 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
- no evidence level
- Partition of an interval definition
- Mesh of a partition definition
- Riemann sum definition
- Riemann integrable function definition
- Riemann integral definition
- Comparison of a series and an integral statement
Where this leads
1 page builds on this one.
Further reading
About this page
| Tag | 069HKV4X1E |
|---|---|
| URI | m2://069HKV4X1E |
| Kind | statement, proposition |
| Writing | W1 stated |
| MSC | 26A42 |
| Status | This copy of the site has no build data. Run m2 status 069HKV4X1E. |
| Uses | Riemann 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.