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.
For bounded on and a partition : the infimum and supremum of on the -th subinterval, and the lower and upper Darboux sums and
Definition
Let be reals, let be bounded (Lower bound, bounded below, bounded set), so that there is a real with for every , and let be a partition of with subintervals and lengths for (Partition of as a finite strictly increasing list , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions).
The two extreme values on a subinterval
For put
Both exist. The set is nonempty, because makes nonempty (Intervals of : the nine order-convex forms, nondegeneracy, and length), and it is bounded, because for every (Lower bound, bounded below, bounded set). A nonempty set bounded above has a supremum (Complete ordered field (least-upper-bound property)) and a nonempty set bounded below has an infimum (Every nonempty set bounded below has an infimum, Greatest lower bound (infimum)); each is unique, so the notations and name single real numbers (Suprema and infima are unique).
They bracket the values, and each other. For ,
the outer inequalities because is a lower bound and an upper bound of , and the middle ones by the definitions of infimum and supremum. In particular and .
The dependence of and on and on is suppressed in the notation, as is customary; where two partitions are in play the sums below carry the partition and the extreme values are written out.
The two Darboux sums
the finite sums of Finite sums and finite products, by recursion, indexed by with . Both are real numbers, being finite sums of reals, and
by monotonicity of finite sums, clause 4 of Laws of finite sums and finite products, since for every : multiplying by preserves the inequality (Ordered field).
The gap on a subinterval is the oscillation there
For every ,
the oscillation of on the set (The oscillation of on a set and the oscillation at a point, both taken in the extended reals). The supremum is a real number here rather than an extended one, because is bounded (The oscillation of on a set and the oscillation at a point, both taken in the extended reals, The extended real line , its order, and the arithmetic that is left undefined). The identity is proved in two inequalities.
The oscillation is at most the gap. For both and lie in , so and , whence (Basic properties of the absolute value). So is an upper bound of the set whose supremum is .
The gap is at most the oscillation. Let be real. By the -characterisations of the supremum and the infimum (Epsilon characterisation of the supremum, Epsilon characterisation of the infimum) there are with and ; then
so . As was arbitrary, : otherwise would be positive and give .
This identity is what connects the Darboux machinery to the pointwise oscillation of The oscillation of on a set and the oscillation at a point, both taken in the extended reals, and it is the hinge of Lebesgue's criterion for Riemann integrability: a bounded on is Riemann integrable if and only if its set of discontinuities has measure zero.
Remarks
-
Boundedness is a hypothesis of the definition, not of the theorems. Without it may fail to have a supremum in and is not defined at all. Every statement on this page that mentions or therefore carries "bounded " in its hypotheses, and none of them is a restriction that could be lifted: an unbounded function has no Darboux sums to compare.
-
Why the infimum and the supremum, and not a value of . Replacing by for a point gives the Riemann sums of Tagged partitions of , with a tag in each subinterval, and the Riemann sum , which depend on a choice of points and are not extremal. The Darboux sums are canonical functions of and alone, which is what makes the supremum and infimum over all partitions in The lower and upper Darboux integrals of a bounded on as and , Darboux integrability as their equality, and the notation well posed without any selection.
-
The empty sum does not occur. A partition has (Partition of as a finite strictly increasing list , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions), so and are sums of at least one term. The first term is , over the subinterval ; the indexing starts at throughout this page.
Depends on
Partition of as a finite strictly increasing list , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions
Lower bound, bounded below, bounded set
Complete ordered field (least-upper-bound property)
Ordered field
Greatest lower bound (infimum)
Every nonempty set bounded below has an infimum
Finite sums and finite products, by recursion
Laws of finite sums and finite products
Intervals of : the nine order-convex forms, nondegeneracy, and length
Suprema and infima are unique
Epsilon characterisation of the supremum
Epsilon characterisation of the infimum
The oscillation of on a set and the oscillation at a point, both taken in the extended reals
The extended real line , its order, and the arithmetic that is left undefined
Basic properties of the absolute value