LemmaStatement: 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.

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

Statement

Let $a < b$ be reals and let $f : [a, b] \to R$ be bounded, say $∣ f (x) ∣ \leq M$ for every $x \in [a, b]$ with $M \geq 0$ real (Lower bound, bounded below, bounded set). Darboux sums are those of 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}$ and partitions those of 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. Then:

Refinement. If $P^{'} = (n^{'}, t^{'})$ refines $P = (n, t)$ then $L (f, P) \leq L (f, P^{'}) \leq U (f, P^{'}) \leq U (f, P) .$
Every lower sum is at most every upper sum. For arbitrary partitions $P$ and $Q$ of $[a, b]$ , $L (f, P) \leq U (f, Q) .$
Quantitative form. If $P^{'} = (n^{'}, t^{'})$ refines $P = (n, t)$ then $0 \leq U (f, P) - U (f, P^{'}) \leq 2 M (n^{'} - n) ∥ P ∥, 0 \leq L (f, P^{'}) - L (f, P) \leq 2 M (n^{'} - n) ∥ P ∥ .$

Notation. In claim 3 the natural number $n^{'} - n$ multiplies a real, and as in clause 2 of Laws of finite sums and finite products it stands there for its canonical natural $ι (n^{'} - n) \in R$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field); $ι$ is additive and nondecreasing on $N$ (Canonical naturals are positive and strictly increasing). The same abbreviation is used throughout the proof.

Claims 1 and 2 are what make the Darboux-integral definition well posed. Claim 3 is the extra information that a refinement changes the sums by an amount controlled by the mesh of the coarse partition and by how many points were added; it is the bound a later Darboux-versus-Riemann comparison needs and nothing else on this page uses it. Here $n^{'} - n \geq 0$ (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), so the right-hand bounds are nonnegative.

Facts & Assumptions

Given: Reals $a < b$ , a bounded $f : [a, b] \to R$ with $∣ f (x) ∣ \leq M$ for all $x \in [a, b]$ and $M \geq 0$ real, and partitions $P = (n, t)$ and $P^{'} = (n^{'}, t^{'})$ of $[a, b]$ with $P^{'}$ refining $P$ .

[L1]

A refinement carries an index map $φ$ with $φ (0) = 0$ , $φ (n) = n^{'}$ and $φ (i) < φ (i + 1)$ for $i < n$ ; hence $φ (k) \geq k$ for $k \leq n$ and $n \leq n^{'}$ . For $i < n$ and $φ (i) \leq j < φ (i + 1)$ one has $I_{j}^{'} \subseteq I_{i}$ , and $\sum_{j = φ (i)}^{φ (i + 1) - 1} Δ_{j}^{'} = Δ_{i}$ . Every $Δ_{i}$ satisfies $0 < Δ_{i} \leq ∥ P ∥$ , and $\sum_{i < n} Δ_{i} = b - a$ (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).

[L2]

For any partitions $R, S$ of $[a, b]$ the common refinement $R \lor S$ refines both (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).

[L3]

With $m_{i} = \inf f [I_{i}]$ and $M_{i} = \sup f [I_{i}]$ : $- M \leq m_{i} \leq f (x) \leq M_{i} \leq M$ for $x \in I_{i}$ , $L (f, P) = \sum_{i < n} m_{i} Δ_{i}$ , $U (f, P) = \sum_{i < n} M_{i} Δ_{i}$ , and $L (f, R) \leq U (f, R)$ for every partition $R$ (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}$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L4]

If $\emptyset \neq S \subseteq T \subseteq R$ and $T$ is bounded above then $\sup S \leq \sup T$ (Monotonicity of the supremum under inclusion); dually, if $T$ is bounded below then $\inf S \geq \inf T$ , since $\inf T$ is a lower bound of $T$ and hence of $S$ , and $\inf S$ is the greatest lower bound of $S$ (Greatest lower bound (infimum), Every nonempty set bounded below has an infimum).

[L5]

Finite sums: splitting $\sum_{j < q} c_{j} = \sum_{j < p} c_{j} + \sum_{j = p}^{q - 1} c_{j}$ for $p \leq q$ , additivity, scaling, monotonicity in the terms, and telescoping (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L6]

Induction on $N$ (The principle of mathematical induction).

[L7]

Ordered-field arithmetic: adding a constant and multiplying by a nonnegative quantity preserve an inequality, and the order is total and transitive (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.

[L8]

A natural number multiplying a real means its canonical natural $ι (\cdot)$ ; $ι (0) = 0$ , $ι (p + q) = ι (p) + ι (q)$ , $ι (p) \geq 0$ , and $p \leq q$ implies $ι (p) \leq ι (q)$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing, Laws of finite sums and finite products).

Proof

technique · induction

1.1

Fix the index map $φ$ of [L1] and, for $k \leq n$ , put $A_{k} : = \sum_{j < φ (k)} M_{j}^{'} Δ_{j}^{'}$ , $B_{k} : = \sum_{i < k} M_{i} Δ_{i}$ , $A_{k}^{-} : = \sum_{j < φ (k)} m_{j}^{'} Δ_{j}^{'}$ and $B_{k}^{-} : = \sum_{i < k} m_{i} Δ_{i}$ ; let $Q (k)$ be the conjunction $B_{k} - 2 M ∥ P ∥ (φ (k) - k) \leq A_{k} \leq B_{k}$ and $B_{k}^{-} \leq A_{k}^{-} \leq B_{k}^{-} + 2 M ∥ P ∥ (φ (k) - k)$ . The proof is an induction on $k$ using [L6].

givenL1L6construct

1.2

Base, $k = 0$ . All four sums are empty, hence $0$ , and $φ (0) - 0 = 0$ , so $Q (0)$ reads $0 \leq 0 \leq 0$ twice.

baseL1L5

1.3

Induction hypothesis. Fix $k < n$ and assume $Q (k)$ .

ihgiven

2.1

Put $β : = \sum_{j = φ (k)}^{φ (k + 1) - 1} M_{j}^{'} Δ_{j}^{'}$ and $γ : = \sum_{j = φ (k)}^{φ (k + 1) - 1} m_{j}^{'} Δ_{j}^{'}$ . For $φ (k) \leq j < φ (k + 1)$ one has $I_{j}^{'} \subseteq I_{k}$ , hence $f [I_{j}^{'}] \subseteq f [I_{k}]$ , hence $m_{k} \leq m_{j}^{'} \leq M_{j}^{'} \leq M_{k}$ by [L4] and [L3]; also $∣ M_{j}^{'} ∣ \leq M$ and $∣ m_{j}^{'} ∣ \leq M$ by [L3].

step 1.1L1L3L4

3.1

Since $Δ_{j}^{'} > 0$ and the lengths in the block sum to $Δ_{k}$ by [L1], monotonicity and scaling of finite sums ([L5]) give $m_{k} Δ_{k} \leq γ \leq β \leq M_{k} Δ_{k}$ and $- M Δ_{k} \leq γ \leq β \leq M Δ_{k}$ .

step 2.1L1L5L7

4.1

Both $M_{k} Δ_{k} - β$ and $γ - m_{k} Δ_{k}$ lie in $[0, 2 M ∥ P ∥ (φ (k + 1) - φ (k) - 1)]$ . Nonnegativity is step 3.1. If $φ (k + 1) = φ (k) + 1$ the block is the single index $j = φ (k)$ , and then $I_{j}^{'} = I_{k}$ by [L1], so $M_{j}^{'} = M_{k}$ , $m_{j}^{'} = m_{k}$ , $Δ_{j}^{'} = Δ_{k}$ and both quantities are $0$ . Otherwise $φ (k + 1) - φ (k) - 1 \geq 1$ , and by step 3.1 and [L3] each quantity is at most $M Δ_{k} + M Δ_{k} = 2 M Δ_{k} \leq 2 M ∥ P ∥$ , hence at most $2 M ∥ P ∥ (φ (k + 1) - φ (k) - 1)$ .

step 2.1step 3.1L1L3L5L7L8

5.1

The upper half of $Q (k + 1)$ . By the splitting law [L5], $A_{k + 1} = A_{k} + β$ and $B_{k + 1} = B_{k} + M_{k} Δ_{k}$ . From step 1.3 and step 3.1, $A_{k + 1} \leq B_{k} + M_{k} Δ_{k} = B_{k + 1}$ ; and from step 1.3 and step 4.1, $A_{k + 1} \geq B_{k} - 2 M ∥ P ∥ (φ (k) - k) + M_{k} Δ_{k} - 2 M ∥ P ∥ (φ (k + 1) - φ (k) - 1) = B_{k + 1} - 2 M ∥ P ∥ (φ (k + 1) - (k + 1))$ .

step 1.3step 3.1step 4.1L5L7L8

5.2

The lower half of $Q (k + 1)$ . Likewise $A_{k + 1}^{-} = A_{k}^{-} + γ$ and $B_{k + 1}^{-} = B_{k}^{-} + m_{k} Δ_{k}$ , so step 1.3 with step 3.1 gives $A_{k + 1}^{-} \geq B_{k + 1}^{-}$ , and step 1.3 with step 4.1 gives $A_{k + 1}^{-} \leq B_{k}^{-} + 2 M ∥ P ∥ (φ (k) - k) + m_{k} Δ_{k} + 2 M ∥ P ∥ (φ (k + 1) - φ (k) - 1) = B_{k + 1}^{-} + 2 M ∥ P ∥ (φ (k + 1) - (k + 1))$ . So $Q (k + 1)$ holds.

step 1.3step 3.1step 4.1L5L7L8

6.1

By [L6] with steps 1.2, 1.3, 5.1 and 5.2, $Q (k)$ holds for every $k \leq n$ . Taking $k = n$ and using $φ (n) = n^{'}$ from [L1]: $A_{n} = U (f, P^{'})$ , $B_{n} = U (f, P)$ , $A_{n}^{-} = L (f, P^{'})$ and $B_{n}^{-} = L (f, P)$ , so $U (f, P) - 2 M ∥ P ∥ (n^{'} - n) \leq U (f, P^{'}) \leq U (f, P)$ and $L (f, P) \leq L (f, P^{'}) \leq L (f, P) + 2 M ∥ P ∥ (n^{'} - n)$ . With $L (f, P^{'}) \leq U (f, P^{'})$ from [L3] this is claim 1, and it is claim 3.

step 1.2step 1.3step 5.1step 5.2L1L3L6L8

7.1

Claim 2. Let $P$ and $Q$ be arbitrary partitions of $[a, b]$ and let $R : = P \lor Q$ , which refines both by [L2]. Applying step 6.1 to the pair $(P, R)$ and to the pair $(Q, R)$ gives $L (f, P) \leq L (f, R) \leq U (f, R) \leq U (f, Q)$ , the middle inequality by [L3]. All three claims are now established, the first and third in step 6.1 from the completed induction and the second here.

step 6.1L2L3L6discharge-induction∎

Remarks

Where the hypothesis $∣ f ∣ \leq M$ is used, and where it is not. Claims 1 and 2 need only that $f$ is bounded, so that the Darboux sums exist at all; the particular bound $M$ enters only in claim 3, through step 4.1, and the factor $2 M$ there is exactly the largest possible value of $M_{k} - m_{k}$ (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 mesh in claim 3 is that of the coarse partition. It has to be: the refinement $P^{'}$ may have very short subintervals, and what the estimate measures is how much a single one of $P$ 's subintervals can be improved by being cut up. That is why the later theorem comparing Darboux and Riemann integration can fix a partition $P_{0}$ once and then let $P$ range over all partitions of small mesh.
The count $n^{'} - n$ is not a count of new points in disguise. It is the difference of the two index counts, and by the telescoping identity of 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 it equals the total amount by which the blocks of $φ$ exceed length one. That is the form the proof uses, and it needs no notion of the cardinality of $pts (P^{'}) ∖ pts (P)$ .

Depends on

Used by

Dependency tree · two levels

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