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 on a nondegenerate rectangle in : integrability is equivalent to arbitrarily small Darboux gaps
Statement
A bounded on a nondegenerate rectangle is Riemann integrable if and only if, for every , some grid satisfies .
Facts & Assumptions
Given: A bounded function on a nondegenerate rectangle.
The lower and upper integrals are the supremum and infimum in The lower and upper Darboux integrals over a nondegenerate rectangle in .
Near-supremum and near-infimum elements exist (Epsilon characterisation of the supremum, Epsilon characterisation of the infimum).
Proof
If the two integrals equal , choose with and with . A common refinement has gap below .
Conversely, a common refinement shows every lower sum is at most every upper sum, so for every , . Arbitrarily small gaps force the integral difference to be .
Thus the conditions are equivalent.
Depends on
- The lower and upper Darboux integrals over a nondegenerate rectangle in $\mathbb{R}^m$
- Lower and upper Darboux sums over a grid partition in $\mathbb{R}^m$
- Refinement raises multidimensional lower sums and lowers upper sums, with a quantitative boundary-slab estimate
- Grid partitions of a rectangle in $\mathbb{R}^m$, their cells, refinements and mesh
- Epsilon characterisation of the supremum
- Epsilon characterisation of the infimum
Used by
- A Riemann-integrable Thomae-type function whose x-sections are nonintegrable at every rational height Example
- An integrable function on the unit square with one Dirichlet section and only one defined order of ordinary iteration Example
- A bounded set is Jordan measurable iff its indicator is Riemann integrable, and the integral is its Jordan content Theorem
- Every continuous function on a closed nondegenerate rectangle in ℝᵐ is Riemann integrable Theorem
- Lebesgue's criterion in ℝᵐ: a bounded function on a closed nondegenerate rectangle is Riemann integrable iff its discontinuity set is null Theorem
- Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in ℝᵐ Theorem
- Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections Theorem
- The multidimensional Darboux and tagged-mesh definitions of the Riemann integral agree Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 59 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- J. Lebl, Basic Analysis, Riemann Integral in Several Variables (standard reference, not scraped)
- J. Lebl, Basic Analysis, The Riemann-Lebesgue Criterion (standard reference, not scraped)