TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-27 (gpt-5)

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.

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

Statement

Let $a < b$ be reals and let $f : [a, b] \to R$ be bounded (Lower bound, bounded below, bounded set). Then $f$ is Darboux 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$ ) if and only if

$for every real ε > 0 there is a partition P of [a, b] with U (f, P) - L (f, P) < ε$

(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}$ , 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).

This is the criterion every later integrability proof on this page uses. It replaces a statement about a supremum and an infimum over all partitions, which cannot be checked directly, by the exhibition of a single partition for each $ε$ . The criterion says nothing about the value of the integral; that separate lower-and-upper-sum estimate places the integral between $L (f, P)$ and $U (f, P)$ for the same $P$ .

Facts & Assumptions

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

[A1]

The criterion: for every real $ε > 0$ there is a partition $P$ of $[a, b]$ with $U (f, P) - L (f, P) < ε$ .

[L1]

$L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P)$ for every partition $P$ ; $\underline{\int_{a}^{b}} f = \sup L$ and $\overline{\int_{a}^{b}} f = \inf U$ over the nonempty sets $L$ of lower sums and $U$ of upper sums; $f$ is integrable exactly when the two are equal (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$ , 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}$ ).

[L2]

$ε$ -characterisation of the supremum: if $u = \sup S$ with $S$ nonempty then for every real $ε > 0$ there is $s \in S$ with $s > u - ε$ (Epsilon characterisation of the supremum). Dually, if $ℓ = \inf S$ then for every real $ε > 0$ there is $s \in S$ with $s < ℓ + ε$ (Epsilon characterisation of the infimum, Greatest lower bound (infimum)).

[L3]

If $P^{'}$ refines $P$ then $L (f, P) \leq L (f, P^{'})$ and $U (f, P^{'}) \leq U (f, P)$ ; the common refinement $P_{1} \lor P_{2}$ refines both $P_{1}$ and $P_{2}$ (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) \leq L (f, P^{'}) \leq U (f, P^{'}) \leq U (f, P)$ when $P^{'}$ refines $P$ , and $L (f, P) \leq U (f, Q)$ for arbitrary partitions $P$ and $Q$ ; moreover the two changes are at most $2 M (n^{'} - n) ∥ P ∥$ , 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).

[L4]

Ordered-field arithmetic: adding a constant to both sides preserves an inequality, the order is total and transitive, and $t \cdot 2^{- 1} > 0$ for $t > 0$ (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)). 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.1L1

Write $D : = \overline{\int_{a}^{b}} f - \underline{\int_{a}^{b}} f$ , a real number with $D \geq 0$ by [L1]; $f$ is integrable exactly when $D = 0$ .

1.2A1L1L4choose

The criterion is sufficient. Assume [A1] and let a real $ε > 0$ be given. Fix a partition $P$ with $U (f, P) - L (f, P) < ε$ . By [L1], $\underline{\int_{a}^{b}} f \geq L (f, P)$ and $\overline{\int_{a}^{b}} f \leq U (f, P)$ , so $D \leq U (f, P) - L (f, P) < ε$ .

1.3L1L4

The criterion is necessary; this half of the proof is steps 1.3, 2.2 and 3.1, and its symbols are its own. Assume $f$ is integrable and write $I$ for the common value $\underline{\int_{a}^{b}} f = \overline{\int_{a}^{b}} f$ . Let a real $η > 0$ be given; then $η \cdot 2^{- 1} > 0$ by [L4].

2.1step 1.1step 1.2L4

So $0 \leq D < ε$ for every real $ε > 0$ . If $D > 0$ , taking $ε : = D$ gives $D < D$ , which is false; hence $D = 0$ and $f$ is integrable by step 1.1.

2.2step 1.3L1L2choose

By [L2] applied to $L$ , whose supremum is $I$ , there is a partition $P_{1}$ with $L (f, P_{1}) > I - η \cdot 2^{- 1}$ ; by [L2] applied to $U$ , whose infimum is $I$ , there is a partition $P_{2}$ with $U (f, P_{2}) < I + η \cdot 2^{- 1}$ .

3.1step 2.2L3L4

Put $P_{*} : = P_{1} \lor P_{2}$ , which refines both by [L3]. Then $L (f, P_{*}) \geq L (f, P_{1}) > I - η \cdot 2^{- 1}$ and $U (f, P_{*}) \leq U (f, P_{2}) < I + η \cdot 2^{- 1}$ , so $U (f, P_{*}) - L (f, P_{*}) < η$ by [L4]. Since $η > 0$ was arbitrary, the criterion holds.

4.1step 2.1step 3.1∎

Steps 1.2 and 2.1 give the implication from the criterion to integrability, and steps 1.3, 2.2 and 3.1 give the converse; the two halves are independent and use no symbol in common, and together they are the stated equivalence.

Remarks

The strict inequality is not essential. Requiring $U (f, P) - L (f, P) \leq ε$ for every $ε > 0$ defines the same condition, since a partition working for $ε \cdot 2^{- 1}$ works strictly for $ε$ . Statements below use whichever form is convenient and no consequence turns on the difference.
The common refinement is where the two partitions are reconciled. Step 2.2 produces one partition good for the lower sum and another good for the upper sum, and there is no reason for them to be the same. 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) \leq L (f, P^{'}) \leq U (f, P^{'}) \leq U (f, P)$ when $P^{'}$ refines $P$ , and $L (f, P) \leq U (f, Q)$ for arbitrary partitions $P$ and $Q$ ; moreover the two changes are at most $2 M (n^{'} - n) ∥ P ∥$ is exactly what allows a single partition to inherit both properties, and it is the only place in this proof where anything beyond the definitions is used.
No choice principle is used. Steps 1.2, 2.2 and 3.1 instantiate finitely many existential statements, which is ordinary first-order reasoning. See Choice ledger for the Riemann integral: the page results are proved in ZF.

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

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

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

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

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