How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
A monotone function on is Riemann integrable: for the uniform partition into parts the upper minus lower sum telescopes to
Statement
Let be reals and let be monotone, that is nondecreasing or nonincreasing on (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of , with the dictionary to monotone sequences). Then is bounded (Lower bound, bounded below, bounded set) and Riemann integrable on (The lower and upper Darboux integrals of a bounded on as and , Darboux integrability as their equality, and the notation ).
Moreover, for the uniform partition of into parts (Partition of as a finite strictly increasing list , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions),
where is the canonical natural of in (The canonical natural of a field). The right-hand side is an equality, not an estimate: the sum telescopes exactly, because on each subinterval a monotone function attains its extremes at the two endpoints.
No continuity is assumed, and none holds in general: a nondecreasing function may be discontinuous at every rational (Converse to Froda: for every at most countable there is a bounded nondecreasing whose set of discontinuities is exactly , every one of them a jump), and the companion page of this pair works out the integral of the floor function, the simplest discontinuous monotone integrand.
Facts & Assumptions
Given: Reals and a monotone . Let be a natural number and let be the uniform partition of into parts, with subintervals and lengths for .
is nondecreasing, meaning whenever in , or nonincreasing, meaning whenever ; these two cases are what "monotone" means and they exhaust it (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of , with the dictionary to monotone sequences).
For the uniform partition: , , , every , and (Partition of as a finite strictly increasing list , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions).
If a nonempty set has a greatest element then that element is , and if it has a least element then that element is (Maximum and minimum of a set, Greatest lower bound (infimum), Complete ordered field (least-upper-bound property)).
Finite sums: scaling and telescoping, (Finite sums and finite products, by recursion, Laws of finite sums and finite products).
Riemann's criterion: a bounded is integrable if and only if for every real there is a partition with (Riemann's criterion: a bounded on is Darboux integrable if and only if for every real there is a partition with ).
For every real there is a natural with , and for (For every in a complete ordered field there is a natural with , Every complete ordered field is Archimedean, The canonical natural of a field, Canonical naturals are positive and strictly increasing).
Ordered-field arithmetic and the absolute value: adding a constant and multiplying by a positive quantity preserve an inequality; the order is total and transitive; for and for (Basic properties of the absolute value, Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication, Ordered field, Complete ordered field (least-upper-bound property), Intervals of : the nine order-convex forms, nondegeneracy, and length). These order-arithmetic facts are stated by their sources for the strict order only; the nonstrict forms used below follow by adjoining the equality case, in which the two sides coincide.
Proof
By [L1] there are two cases, nondecreasing and nonincreasing, and they exhaust the hypothesis. Every satisfies (Intervals of : the nine order-convex forms, nondegeneracy, and length).
Case: is nondecreasing. Then for every , so is bounded by [L8]; and for and one has , hence . Since and themselves lie in , they are its least and greatest elements, so and by [L3].
Case: is nonincreasing. Then for every , so is bounded; and for and one has , so and by [L3].
In the nondecreasing case, , so by [L4], [L2] and [L5], , and , so this equals by [L8].
In the nonincreasing case the same computation gives with , which is again by [L8]. The two cases of step 1.1 exhaust the hypothesis, so the displayed identity holds for every monotone , which is also bounded.
Let a real be given and put , a positive real by [L8]. By [L7] fix a natural with .
Then : the first inequality because and , and the second because and . So .
Since the real was arbitrary and step 4.1 produced a partition with , criterion [L6] applies: is bounded by steps 1.2 and 1.3 and Riemann integrable on .
Remarks
-
The telescoping is exact, and that is what makes the proof short. No estimate of is needed subinterval by subinterval: the whole sum of the gaps is the total rise of , however wildly the rise is distributed. This is why a monotone function with infinitely many jumps is no harder than a continuous one here, and it is the same telescoping that Partition of as a finite strictly increasing list , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions uses for the lengths.
-
Uniformity of the partition is a convenience, not a necessity. For an arbitrary partition the same identification of and gives , by bounding each by the mesh before telescoping. The uniform partition is used above only so that can be pulled out of the sum as a constant.
-
No choice principle is used. The partition is given by a formula in , and is obtained from one instance of the Archimedean property. See What this page costs in choice: Riemann's criterion, the Darboux-Riemann equivalence and integrability of a monotone function are theorems of ZF; integrability of a continuous function inherits the single use of countable choice inside Heine-Cantor; and only the forward half of the Lebesgue criterion spends countable choice, once, at the countable union of null sets.
-
Monotone is strictly weaker than continuous here. The floor function is nondecreasing with jumps at every integer and is integrable (the companion page of this pair); and a monotone function has at most countably many discontinuities (Froda's theorem: the set of discontinuities of a monotone function on an interval is at most countable, the injection into being built from one fixed enumeration of the rationals by least index, so no choice principle is used), so this theorem is also a special case of A bounded function on whose set of discontinuities is at most countable is Riemann integrable once that is available. The direct proof is kept because it is elementary and quantitative, and because it costs no choice at all.
Depends on
- Riemann's criterion: a bounded $f$ on $[a,b]$ is Darboux integrable if and only if for every real $\varepsilon > 0$ there is a partition $P$ with $U(f,P) - L(f,P) < \varepsilon$
- Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $\mathbb{R}$, with the dictionary to monotone sequences
- Partition of $[a,b]$ as a finite strictly increasing list $a = t_0 < t_1 < \dots < t_n = b$, its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions
- For bounded $f$ on $[a,b]$ and a partition $P$: the infimum $m_i$ and supremum $M_i$ of $f$ on the $i$-th subinterval, and the lower and upper Darboux sums $L(f,P) = \sum_i m_i \Delta_i$ and $U(f,P) = \sum_i M_i \Delta_i$
- The lower and upper Darboux integrals of a bounded $f$ on $[a,b]$ as $\sup_P L(f,P)$ and $\inf_P U(f,P)$, Darboux integrability as their equality, and the notation $\int_a^b f$
- Laws of finite sums and finite products
- Finite sums and finite products, by recursion
- Lower bound, bounded below, bounded set
- For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
- Every complete ordered field is Archimedean
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Canonical naturals are positive and strictly increasing
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- Maximum and minimum of a set
- Greatest lower bound (infimum)
- Basic properties of the absolute value
- Complete ordered field (least-upper-bound property)
- Ordered field
- Order is preserved by adding a constant and by adding inequalities
- Sign rules for products and monotonicity of multiplication
Used by
- Every bounded-variation function on a compact interval is Riemann integrable Corollary
- Integrable φ and integrable f with φ∘ f not integrable: the order of the hypotheses in the composition theorem cannot be reversed Counterexample
- ∫₀³ lfloor x rfloor = 3: the floor function is nondecreasing, hence integrable, and the integral is computed from the uniform partitions Example
- A step function integrated by additivity over subintervals, and the same value from the definition Example
- What this page costs in choice: Riemann's criterion, the Darboux-Riemann equivalence and integrability of a monotone function are theorems of ZF; integrability of a continuous function inherits the single use of countable choice inside Heine-Cantor; and only the forward half of the Lebesgue criterion spends countable choice, once, at the countable union of null sets Remark
- Bonnet's second mean value theorem: for f monotone and g integrable on [a,b] there is ξ∈[a,b] with ∫ₐᵇ fg = f(a)∫ₐ^ξ g + f(b)∫_ξᵇ g Theorem
- The integral test: for f ≥ 0 nonincreasing on [0,∞), ∑ₖ f(k) converges if and only if the sequence (∫₀^N f)_N is bounded, with ∫₀^N f ≤ ∑_k<N f(k) ≤ f(0) + ∫₀^N f Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 69 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Riemann integral (Wikipedia) (standard reference, not scraped)
- Monotonic function (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 6 (standard reference, not scraped)
- J. Lebl, Basic Analysis I, The Riemann Integral (standard reference, not scraped)
- J. Hunter, MAT 125B Lecture Notes (standard reference, not scraped)