Alphabeta Math

The Riemann Integral: Definition and Integrability

About this page
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.

✓ 13 results · all verified · 6 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 7 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Abstract Algebra
Number Theory
Real Analysis
Set Theory
Topology
2 · Logical flowchart

3 · Items

Definition

Partition of [a,b] as a finite strictly increasing list a = t₀ < t₁ < … < tₙ = b, its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions

Definition

For bounded f on [a,b] and a partition P: the infimum mᵢ and supremum Mᵢ of f on the i-th subinterval, and the lower and upper Darboux sums L(f,P) = ∑ᵢ mᵢ Δᵢ and U(f,P) = ∑ᵢ Mᵢ Δᵢ

Lemma

Refining a partition raises the lower Darboux sum and lowers the upper one, and every lower sum is at most every upper sum: L(f,P) ≤ L(f,P') ≤ U(f,P') ≤ U(f,P) when P' refines P, and L(f,P) ≤ U(f,Q) for arbitrary partitions P and Q; moreover the two changes are at most 2M(n' - n)‖P‖

Definition

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 ∫ₐᵇ f

Lemma

If m ≤ f ≤ M on [a,b] then m(b-a) ≤ L(f,P) ≤ ∫ₐᵇ f ≤ ∫ₐᵇ f ≤ U(f,P) ≤ M(b-a) for every partition P; in particular every constant function is integrable, with ∫ₐᵇ c = c(b-a)

Theorem

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) < ε

Definition

Tagged partitions of [a,b], with a tag ξᵢ in each subinterval, and the Riemann sum S(f,P,ξ) = ∑ᵢ f(ξᵢ) Δᵢ

Theorem

The Darboux and Riemann definitions agree: a bounded f on [a,b] is Darboux integrable with integral I if and only if for every real ε > 0 there is a real δ > 0 such that |S(f,P,ξ) - I| < ε for every tagged partition of mesh below δ

Theorem

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

Theorem

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)

Theorem

A bounded function on [a,b] that is continuous except at finitely many points is Riemann integrable

Lemma

A countable union of compact content-zero subsets of the line is null in ZF

Theorem

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

Corollary

A bounded function on [a,b] whose set of discontinuities is at most countable is Riemann integrable

Remark

Choice ledger for the Riemann integral: the page results are proved in ZF

False statement

FALSE: every bounded function on [a,b] is Riemann integrable

False statement

FALSE: a bounded function on [a,b] is Riemann integrable exactly when its set of discontinuities is nowhere dense

False statement

FALSE: a nonnegative Riemann integrable function on [a,b] with ∫ₐᵇ f = 0 is identically zero

False statement

FALSE: a pointwise limit of a sequence of Riemann integrable functions on [a,b] is Riemann integrable

Sources