TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

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.

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 $δ$

Statement

Let $a < b$ be reals, let $f : [a, b] \to R$ be bounded (Lower bound, bounded below, bounded set) and let $I \in R$ . The following are equivalent.

(Darboux) $f$ is Darboux integrable on $[a, b]$ with $\int_{a}^{b} f = 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$ ).
(Riemann) For every real $ε > 0$ there is a real $δ > 0$ such that $∣ S (f, P, ξ) - I ∣ < ε$ for every tagged partition $(P, ξ)$ of $[a, b]$ with $∥ P ∥ < δ$ (Tagged partitions of $[a, b]$ , with a tag $ξ_{i}$ in each subinterval, and the Riemann sum $S (f, P, ξ) = \sum_{i} f (ξ_{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).

The quantifier over tagged partitions is universal, and that is the content. Condition 2 constrains every tagged partition of small mesh at once, tags included; it is not a statement about one sequence of tagged partitions, and it cannot be weakened to one. The companion page of this pair exhibits a non-integrable function whose Riemann sums are constant along such a sequence.

Boundedness is a hypothesis of both conditions as stated here. Condition 1 presupposes it, since the Darboux sums of an unbounded function do not exist (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}$ ); condition 2 makes sense for unbounded $f$ as well, and in fact implies boundedness, but that implication is not proved here and is not used: every application on this page starts from a bounded $f$ .

Facts & Assumptions

Given: Reals $a < b$ , a bounded $f : [a, b] \to R$ , a real $M \geq 0$ with $∣ f (x) ∣ \leq M$ for every $x \in [a, b]$ , and a real $I$ . Put $M_{+} : = M + 1$ , so $M_{+} > 0$ and $∣ f (x) ∣ \leq M_{+}$ for every $x$ .

[L1]

For a partition $P = (n, t)$ of $[a, b]$ : $n \geq 1$ , the subintervals $I_{i} = [t_{i}, t_{i + 1}]$ are nonempty, $Δ_{i} = t_{i + 1} - t_{i} > 0$ , $\sum_{i < n} Δ_{i} = b - a$ , and $∥ P ∥ = \max {Δ_{i} : i < n}$ . The uniform partition $U_{N}$ into $N \geq 1$ parts has $∥ U_{N} ∥ = (b - a) / ι (N)$ . The common refinement $P \lor P_{0}$ refines both, and $n_{P \lor P_{0}} \leq n_{P} + n_{P_{0}} - 1$ (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, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L2]

$L (f, P) = \sum_{i < n} m_{i} Δ_{i}$ and $U (f, P) = \sum_{i < n} M_{i} Δ_{i}$ with $m_{i} = \inf f [I_{i}]$ and $M_{i} = \sup f [I_{i}]$ ; $L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P)$ ; $f$ is integrable exactly when the two integrals coincide, and then $\int_{a}^{b} f$ is their common value (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}$ , 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$ ).

[L3]

$S (f, P, ξ) = \sum_{i < n} f (ξ_{i}) Δ_{i}$ for a tagging $ξ$ of $P$ , and $L (f, P) \leq S (f, P, ξ) \leq U (f, P)$ when $f$ is bounded (Tagged partitions of $[a, b]$ , with a tag $ξ_{i}$ in each subinterval, and the Riemann sum $S (f, P, ξ) = \sum_{i} f (ξ_{i}) Δ_{i}$ ).

[L4]

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

[L5]

If $P^{'}$ refines $P$ then $L (f, P) \leq L (f, P^{'})$ , $U (f, P^{'}) \leq U (f, P)$ , and moreover $U (f, P) - U (f, P^{'}) \leq 2 M_{+} ι (n^{'} - n) ∥ P ∥$ and $L (f, P^{'}) - L (f, P) \leq 2 M_{+} ι (n^{'} - n) ∥ P ∥$ (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 ∥$ ).

[L6]

$ε$ -characterisations: if $u = \sup S$ with $S$ nonempty then for every real $η > 0$ there is $s \in S$ with $s > u - η$ ; dually for the infimum (Epsilon characterisation of the supremum, Epsilon characterisation of the infimum).

[L7]

A family of nonempty sets indexed by a natural number $n$ has a choice function, and this is a theorem of ZF; the family used below is indexed by $i < n$ , which is exactly that listed form. Every natural-number-indexed list of nonempty sets has a choice function on its family of values states it in that form and expressly declines to identify it with "every finite family of nonempty sets has a choice function", no definition of finiteness being available where it is proved (Every natural-number-indexed list of nonempty sets has a choice function on its family of values, Choice function).

[L8]

For every real $η > 0$ there is a natural $N \geq 1$ with $1 / ι (N) < η$ ; $ι$ is nonnegative, additive and nondecreasing on $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).

[L9]

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

[L10]

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 ∣ < c$ exactly when $- c < x < c$ for $c > 0$ (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, The multiplicative identity is positive, 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.1

Condition 2 implies condition 1. Assume condition 2 and let a real $ε > 0$ be given. Fix $δ > 0$ as in condition 2 for this $ε$ , and put $θ : = ε / (b - a) > 0$ by [L10].

givenL10choose

1.2

Condition 1 implies condition 2; this half of the proof is steps 1.2, 2.2, 2.3, 3.3, 4.2, 5.2 and 6.2, and its symbols are its own. Assume $f$ is integrable with $\int_{a}^{b} f = I$ and let a real $η > 0$ be given. By [L4] fix a partition $P_{0} = (n_{0}, t^{0})$ with $U (f, P_{0}) - L (f, P_{0}) < η \cdot 2^{- 1}$ .

givenL4L10choose

2.1

A partition of mesh below $δ$ exists: by [L8] fix $N \geq 1$ with $1 / ι (N) < δ / (b - a)$ and take $P : = U_{N}$ , so $∥ P ∥ = (b - a) / ι (N) < δ$ by [L1] and [L10]. Write $P = (n, t)$ .

step 1.1L1L8L10choose

2.2

By [L2] and integrability, $L (f, P_{0}) \leq \underline{\int_{a}^{b}} f = I = \overline{\int_{a}^{b}} f \leq U (f, P_{0})$ . Hence $U (f, P_{0}) - I \leq U (f, P_{0}) - L (f, P_{0}) < η \cdot 2^{- 1}$ and $I - L (f, P_{0}) \leq U (f, P_{0}) - L (f, P_{0}) < η \cdot 2^{- 1}$ , that is $U (f, P_{0}) < I + η \cdot 2^{- 1}$ and $L (f, P_{0}) > I - η \cdot 2^{- 1}$ .

step 1.2L2L10

2.3

Put $δ_{0} : = η \cdot (8 M_{+} ι (n_{0}))^{- 1}$ , a positive real since $M_{+} > 0$ and $ι (n_{0}) > 0$ by [L8] and $n_{0} \geq 1$ by [L1].

step 1.2L1L8L10construct

3.1

For each $i < n$ the set $X_{i} : = {x \in I_{i} : f (x) > M_{i} - θ}$ is nonempty by [L6], since $M_{i} = \sup f [I_{i}]$ and $f [I_{i}]$ is nonempty by [L1]. By [L7] the finite family ${X_{i} : i < n}$ has a choice function $g$ ; put $ξ_{i} : = g (X_{i})$ for $i < n$ and $ξ_{k} : = b$ for $k \geq n$ , a tagging of $P$ .

step 2.1L1L2L6L7choose

3.2

Likewise the sets $Y_{i} : = {x \in I_{i} : f (x) < m_{i} + θ}$ are nonempty by [L6], and [L7] supplies a tagging $ζ$ of $P$ with $ζ_{i} \in Y_{i}$ for $i < n$ .

step 2.1L1L2L6L7choose

3.3

Let $(Q, υ)$ be any tagged partition of $[a, b]$ with $∥ Q ∥ < δ_{0}$ , and write $Q = (n_{Q}, u)$ and $R : = Q \lor P_{0}$ , with $R = (n_{R}, r)$ . By [L1], $R$ refines both $Q$ and $P_{0}$ , and $n_{R} - n_{Q} \leq n_{0} - 1$ , so $ι (n_{R} - n_{Q}) \leq ι (n_{0})$ by [L8].

step 2.3L1L8given

4.1

$S (f, P, ξ) \geq U (f, P) - ε$ : by step 3.1, $f (ξ_{i}) \geq M_{i} - θ$ for $i < n$ , so multiplying by $Δ_{i} > 0$ and summing gives $S (f, P, ξ) \geq \sum_{i < n} (M_{i} - θ) Δ_{i} = U (f, P) - θ \sum_{i < n} Δ_{i} = U (f, P) - θ (b - a) = U (f, P) - ε$ , by [L9], [L1] and [L3]. Symmetrically $S (f, P, ζ) \leq L (f, P) + ε$ .

step 3.1step 3.2L1L3L9L10

4.2

By [L5] applied to the refinement $R$ of $Q$ , $U (f, Q) - U (f, R) \leq 2 M_{+} ι (n_{R} - n_{Q}) ∥ Q ∥ \leq 2 M_{+} ι (n_{0}) δ_{0} = η \cdot 4^{- 1}$ , and likewise $L (f, R) - L (f, Q) \leq η \cdot 4^{- 1}$ .

step 2.3step 3.3L5L8L10

5.1

By condition 2 both $∣ S (f, P, ξ) - I ∣ < ε$ and $∣ S (f, P, ζ) - I ∣ < ε$ , since $∥ P ∥ < δ$ . Hence $U (f, P) \leq S (f, P, ξ) + ε < I + 2 ε$ and $L (f, P) \geq S (f, P, ζ) - ε > I - 2 ε$ , by step 4.1 and [L10].

step 1.1step 2.1step 4.1L10

5.2

By [L5] applied to the refinement $R$ of $P_{0}$ , $U (f, R) \leq U (f, P_{0})$ and $L (f, R) \geq L (f, P_{0})$ . Combining with step 4.2 and step 2.2: $U (f, Q) \leq U (f, R) + η \cdot 4^{- 1} \leq U (f, P_{0}) + η \cdot 4^{- 1} < I + η \cdot 2^{- 1} + η \cdot 4^{- 1}$ , and symmetrically $L (f, Q) > I - η \cdot 2^{- 1} - η \cdot 4^{- 1}$ .

step 2.2step 3.3step 4.2L5L10

6.1

By [L2], $\overline{\int_{a}^{b}} f \leq U (f, P) < I + 2 ε$ and $\underline{\int_{a}^{b}} f \geq L (f, P) > I - 2 ε$ , and since $\underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f$ by [L2], both integrals lie strictly between $I - 2 ε$ and $I + 2 ε$ ; in particular $∣ \overline{\int_{a}^{b}} f - I ∣ \leq 2 ε$ and $∣ \underline{\int_{a}^{b}} f - I ∣ \leq 2 ε$ .

step 5.1L2L10

6.2

By [L3], $L (f, Q) \leq S (f, Q, υ) \leq U (f, Q)$ , so step 5.2 gives $I - η \cdot 2^{- 1} - η \cdot 4^{- 1} < S (f, Q, υ) < I + η \cdot 2^{- 1} + η \cdot 4^{- 1}$ , whence $∣ S (f, Q, υ) - I ∣ < η \cdot 2^{- 1} + η \cdot 4^{- 1} < η$ by [L10]. Since $(Q, υ)$ was an arbitrary tagged partition of mesh below $δ_{0}$ , condition 2 holds with this $δ_{0}$ .

step 5.2L3L10

7.1

Step 6.1 holds for every real $ε > 0$ . If $\overline{\int_{a}^{b}} f \neq I$ , taking $ε : = ∣ \overline{\int_{a}^{b}} f - I ∣ \cdot 4^{- 1} > 0$ would give $∣ \overline{\int_{a}^{b}} f - I ∣ \leq ∣ \overline{\int_{a}^{b}} f - I ∣ \cdot 2^{- 1}$ , which is false for a positive quantity; so $\overline{\int_{a}^{b}} f = I$ , and the same argument gives $\underline{\int_{a}^{b}} f = I$ . Hence $f$ is integrable with $\int_{a}^{b} f = I$ by [L2], which is condition 1.

step 6.1L2L10

8.1

Steps 1.1, 2.1, 3.1, 3.2, 4.1, 5.1, 6.1 and 7.1 prove that condition 2 implies condition 1; steps 1.2, 2.2, 2.3, 3.3, 4.2, 5.2 and 6.2 prove the converse. The two halves share no symbol, the first working with $ε, δ, P, ξ, ζ, θ$ and the second with $η, δ_{0}, P_{0}, Q, υ, R$ , and together they give the stated equivalence.

step 7.1step 6.2∎

Remarks

What the Riemann condition costs in choice: nothing beyond ZF. The only selection made anywhere above is in steps 3.1 and 3.2, where a tag is picked in each of the $n$ subintervals of one fixed partition. That family is listed by the index $i < n$ , and a family of nonempty sets listed by a natural number has a choice function outright (Every natural-number-indexed list of nonempty sets has a choice function on its family of values), with no appeal to any choice axiom. Every other existential in the proof is instantiated once. This is recorded in 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.
Why the mesh of the coarse partition is the right quantity. Step 4.2 is the only place where the mesh hypothesis is spent, and it is spent through the quantitative clause of 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 ∥$ . The symbols there are those of the second half: adding the at most $n_{0} - 1$ interior points of $P_{0}$ to the arbitrary partition $Q$ can change each Darboux sum by at most $2 M_{+}$ times the total length of the affected subintervals, and each of those has length below $δ_{0}$ , the mesh bound imposed on $Q$ . The number $n_{0}$ is fixed before $δ_{0}$ is chosen, in step 1.2 against step 2.3, which is why the argument is not circular.
The two conditions are not symmetric in what they presuppose. Condition 1 names the integral as a supremum and an infimum and needs the completeness of $R$ to make sense; condition 2 names it as a limit of sums and could be stated over any ordered field. What the theorem says is that on $R$ the two coincide, so the numerical picture and the order-theoretic one describe the same object.
The value $I$ is not a free parameter after the fact. If condition 2 holds for $I$ and for $I^{'}$ then $∣ I - I^{'} ∣ < 2 ε$ for every $ε > 0$ , by evaluating both at one tagged partition of small enough mesh, so $I = I^{'}$ . The integral is therefore determined by condition 2 alone, as it is by condition 1.

Depends on

Used by

Dependency tree · two levels

54 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

Darboux integral (Wikipedia) (standard reference, not scraped)
Riemann integral (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 6 (standard reference, not scraped)
J. Hunter, Chapter 11: The Riemann Integral (standard reference, not scraped)

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