TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck pass

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 continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion

Statement

Let $a < b$ be reals and let $f : [a, b] \to R$ be continuous on $[a, b]$ (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point). Then $f$ is bounded (Lower bound, bounded below, bounded set) and Riemann integrable on $[a, b]$ (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$ ).

The proof gives more than integrability: it gives a partition that works. For every real $ε > 0$ the uniform partition into $N$ parts already satisfies $U (f, P) - L (f, P) < ε$ , as soon as $N$ is large enough that $(b - a) / ι (N)$ is below the $δ$ that uniform continuity supplies for $ε / (2 (b - a))$ . Uniform continuity is exactly what makes one $δ$ serve all $N$ subintervals at once, and it is the only place where the compactness of $[a, b]$ is used.

Statement references

Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point

Lower bound, bounded below, bounded set

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$

Facts & Assumptions

Given: Reals $a < b$ and a function $f : [a, b] \to R$ continuous on $[a, b]$ .

[L1]

$[a, b]$ is closed and bounded, hence compact (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, Open subset of $R$ (every point has a neighbourhood inside it), closed subset (complement open), and clopen, Lower bound, bounded below, bounded set, A subset of $R$ is compact if and only if it is closed and bounded, Open cover, subcover, compact subset of $R$ (every open cover has a finite subcover), and sequentially compact subset).

[L2]

A continuous real function on a compact subset of $R$ is bounded there (A continuous real function on a compact subset of $R$ is bounded).

[L3]

Heine-Cantor: a continuous real function on a compact subset $K$ of $R$ is uniformly continuous on $K$ , that is, for every real $η > 0$ there is a real $δ > 0$ with $∣ f (x) - f (y) ∣ < η$ for all $x, y \in K$ with $∣ x - y ∣ < δ$ (Heine-Cantor in $R$ : a continuous real function on a compact subset of $R$ is uniformly continuous, Uniform continuity of $f : A \to R$ : one $δ$ serving every pair of points of $A$ ).

[L4]

For a partition $P = (n, t)$ of $[a, b]$ : $Δ_{i} = t_{i + 1} - t_{i} > 0$ , $\sum_{i < n} Δ_{i} = b - a$ , and the uniform partition $U_{N}$ into $N \geq 1$ parts has every $Δ_{i}$ equal to $(b - a) / ι (N)$ (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).

[L5]

$U (f, P) - L (f, P) = \sum_{i < n} (M_{i} - m_{i}) Δ_{i}$ and $M_{i} - m_{i} = \sup {∣ f (x) - f (y) ∣ : x, y \in I_{i}}$ for bounded $f$ (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} Δ_{i}$ and $U (f, P) = \sum_{i} M_{i} Δ_{i}$ , Laws of finite sums and finite products).

[L6]

Riemann's criterion: a bounded $f$ is integrable if and only if for every real $ε > 0$ there is a partition $P$ with $U (f, P) - L (f, P) < ε$ (Riemann's criterion: a bounded $f$ on $[a, b]$ is Darboux integrable if and only if for every real $ε > 0$ there is a partition $P$ with $U (f, P) - L (f, P) < ε$ ).

[L7]

For every real $η > 0$ there is a natural $N \geq 1$ with $1 / ι (N) < η$ , and $ι (N) > 0$ for $N \geq 1$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Every complete ordered field is Archimedean, The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing).

[L8]

Finite sums: scaling and monotonicity in the terms (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L9]

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; $x, y \in [c, d]$ gives $∣ x - y ∣ \leq d - c$ (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 $R$ : 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

technique · direct

1.1givenL1L3L4L7L8L9choose

$[a, b]$ is compact by [L1], so [L3] supplies uniform continuity. Apply it with tolerance $1$ and fix $δ_{0} > 0$ such that $∣ f (x) - f (y) ∣ < 1$ whenever $x, y \in [a, b]$ and $∣ x - y ∣ < δ_{0}$ . By [L7], choose $N_{0} \geq 1$ with $(b - a) / ι (N_{0}) < δ_{0}$ , and take the uniform partition with nodes $t_{0} = a, \dots, t_{N_{0}} = b$ . Adjacent nodes have distance less than $δ_{0}$ , so $∣ f (t_{j + 1}) - f (t_{j}) ∣ < 1$ . Telescoping the inequalities $- 1 < f (t_{j + 1}) - f (t_{j}) < 1$ and using the absolute-value bounds give $∣ f (t_{i}) ∣ \leq ∣ f (a) ∣ + ι (i)$ for every $i \leq N_{0}$ . Every $x \in [a, b]$ lies in some $[t_{i}, t_{i + 1}]$ , with $i < N_{0}$ , and has $∣ x - t_{i} ∣ < δ_{0}$ ; hence $f (t_{i}) - 1 < f (x) < f (t_{i}) + 1$ and therefore $∣ f (x) ∣ < ∣ f (a) ∣ + ι (N_{0}) + 1$ . Thus $f$ is bounded and its Darboux sums and integrals are defined. Compactness has been used only to obtain uniform continuity.

1.2givenL9

Let a real $ε > 0$ be given and put $η : = ε \cdot (2 (b - a))^{- 1}$ , a positive real by [L9] since $b - a > 0$ .

2.1step 1.1step 1.2L1L3choose

By [L3] applied to the compact set $[a, b]$ with this $η$ , fix a real $δ > 0$ such that $∣ f (x) - f (y) ∣ < η$ for all $x, y \in [a, b]$ with $∣ x - y ∣ < δ$ .

3.1step 2.1L4L7L9choose

By [L7] fix a natural $N \geq 1$ with $1 / ι (N) < δ \cdot (b - a)^{- 1}$ , and put $P : = U_{N} = (N, t)$ , the uniform partition of $[a, b]$ into $N$ parts. Then every $Δ_{i}$ equals $(b - a) / ι (N) < δ$ by [L4] and [L9].

4.1step 2.1step 3.1L5L9

For each $i < N$ and all $x, y \in I_{i} = [t_{i}, t_{i + 1}]$ one has $∣ x - y ∣ \leq Δ_{i} < δ$ by [L9], hence $∣ f (x) - f (y) ∣ < η$ by step 2.1. So $η$ is an upper bound of the set ${∣ f (x) - f (y) ∣ : x, y \in I_{i}}$ , and therefore $M_{i} - m_{i} \leq η$ by [L5].

5.1step 4.1L4L5L8L9

Consequently $U (f, P) - L (f, P) = \sum_{i < N} (M_{i} - m_{i}) Δ_{i} \leq \sum_{i < N} η Δ_{i} = η (b - a) = ε \cdot 2^{- 1} < ε$ , using [L5], step 4.1, $Δ_{i} > 0$ , [L8], [L4] and [L9].

6.1step 1.1step 1.2step 5.1L6∎

Since the real $ε > 0$ of step 1.2 was arbitrary and step 5.1 produced a partition with $U (f, P) - L (f, P) < ε$ , criterion [L6] applies and $f$ is Riemann integrable on $[a, b]$ ; it is bounded by step 1.1.

Remarks

Continuity is sufficient and very far from necessary. A monotone function may have infinitely many discontinuities and is still integrable (A monotone function on $[a, b]$ is Riemann integrable: for the uniform partition into $N$ parts the upper minus lower sum telescopes to $∣ f (b) - f (a) ∣ (b - a) / ι (N)$ ); Thomae's function is discontinuous at every rational and integrable (A bounded function on $[a, b]$ whose set of discontinuities is at most countable is Riemann integrable); and the indicator of the Cantor set is discontinuous at uncountably many points and integrable. The exact frontier is Lebesgue's criterion for Riemann integrability: a bounded $f$ on $[a, b]$ is Riemann integrable if and only if its set of discontinuities has measure zero.
Where compactness enters, and what it buys. Only through [L1] to apply Heine-Cantor in $R$ : a continuous real function on a compact subset of $R$ is uniformly continuous and get uniform continuity on the whole interval. Step 1.1 derives boundedness from this uniform continuity by a finite uniform mesh, so no separate compactness argument is needed for boundedness. On a non-compact interval both uniform continuity and boundedness can fail: $x \mapsto 1 / x$ is continuous on $(0, 1)$ and unbounded there, so it has no Darboux sums at all.
Choice. The proof selects nothing from an infinite family. The current proof of Heine-Cantor in $R$ : a continuous real function on a compact subset of $R$ is uniformly continuous also uses only a finite subcover, so this integrability argument is choice-free. See Choice ledger for the Riemann integral: the page results are proved in ZF.

Depends on

Used by

A continuous real function on [0,1] whose every moment ∫₀¹ xⁿf vanishes is identically zero Corollary
Complete noncompact manifolds with nonnegative ricci curvature have at most euclidean volume growth Corollary
Every continuous function on an interval has a primitive; two primitives differ by a constant; and ∫ₐᵇ f = G(b)-G(a) for any primitive G Corollary
A boundary mode has a different concentration rate Counterexample
A boundary null has a nonstandard likelihood-ratio limit Counterexample
A large adverse zero-order term destroys Dirichlet coercivity Counterexample
A singular interior mode need not have Gaussian scaling Counterexample
An oscillatory L1-bounded sequence with unbounded spatial TV Counterexample
Cantor function has singular distributional derivative Counterexample
Continuous f and integrable sign-changing g with ∫ₐᵇ fg ≠ f(ξ)∫ₐᵇ g for every ξ Counterexample
Continuous fₙ → 0 pointwise on [0,1] with ∫₀¹ fₙ = 1 for every n Counterexample
Finite speed of propagation does not imply strong Huygens Counterexample
Henstock–Kurzweil integrability does not imply integrability of the absolute value Counterexample
Iid strong law fails at infinite absolute mean Counterexample
Infinite variance can defeat square-root-n CLT scaling Counterexample
Omitting the second-stage correction destroys cubic local accuracy Counterexample
The sine integral is improperly Riemann integrable and not Lebesgue integrable Counterexample
Two equal modes contribute two Gaussian terms Counterexample
Uniform moving support invalidates the naive score bound Counterexample
Wave energy need not be conserved through an open boundary Counterexample
Arcsine-weighted inner product on the Chebyshev interval Definition
Distributed delays through a finite-window history integral Definition
Finite-interval oscillatory integral and phase convention Definition
Index form of a geodesic segment Definition
Legendre polynomials by Rodrigues' formula and their unweighted pairing Definition
Nyström quadrature operators and their reconstructed equations Definition
Peano kernel of a finite quadrature functional Definition
Riemann area between two continuous graphs and the disc as a vertically simple region Definition
Scalar line integrals with respect to arc length and vector-field line integrals Definition
Shifted character observables p_ρ^# and profile moments p̃ₖ Definition
Spherical means and the weighted ball integral of space-dependent data Definition
Standard Cauchy probability law Definition
The integral logarithm L(x):=∫₁ˣdt/t for x>0 Definition
∫_-∞^∞(1+x²)⁻¹ dx converges absolutely Example
∫₀¹ x² = 1/3, computed from the Darboux definition with uniform partitions and the closed form ∑_k<n k² = n(n-1)(2n-1)/6 Example
∫₀¹ xᵐ = 1/ι(m+1), computed by the fundamental theorem and checked against the definition Example
A broken P1 test exposes a nonzero consistency residual Example
A continuous likelihood-ratio test Example
A convergent sequence in ℝ³ and the integral ∫₀¹ (1, t, t²), computed componentwise Example
A deterministic integral construction of a Gaussian process Example

…and 160 more results.

Dependency tree · two levels

63 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Riemann integral (Wikipedia) (standard reference, not scraped)
Heine-Cantor theorem (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, Chapter 11: The Riemann Integral (standard reference, not scraped)

A continuous function on [a,b][a,b] is Riemann integrable, by Heine-Cantor and Riemann's criterion