Alphabeta MathHow 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 multidimensional Darboux and tagged-mesh definitions of the Riemann integral agree
Statement
A bounded function on a nondegenerate rectangle is Darboux integrable with value if and only if all tagged grid sums converge with mesh to .
Facts & Assumptions
Given: A bounded , with , on a nondegenerate rectangle .
Every tagged sum lies between its grid's Darboux sums (Tagged grid partitions and Riemann sums in ).
Small Darboux gaps characterize integrability (Riemann's criterion on a nondegenerate rectangle in : integrability is equivalent to arbitrarily small Darboux gaps).
Refining by a fixed grid changes the bounds only by the boundary-slab estimate (Refinement raises multidimensional lower sums and lowers upper sums, with a quantitative boundary-slab estimate).
Finite choice selects cell values within any positive distance of infima and suprema (Epsilon characterisation of the supremum, Epsilon characterisation of the infimum, Every natural-number-indexed list of nonempty sets has a choice function on its family of values).
Repeated equal subdivision and the Archimedean reciprocal property give grid partitions of a nondegenerate rectangle with arbitrarily small mesh (Grid partitions of a rectangle in , their cells, refinements and mesh, For every in a complete ordered field there is a natural with ).
Proof
If is Darboux integrable, choose a fixed grid with small gap by [L2]. For any sufficiently fine , refine it with ; [L3] makes the Darboux bounds of differ from those of the refinement by arbitrarily little. Since the refined lower and upper sums trap , [L1] makes every tagged sum over close to .
Conversely, suppose every sufficiently fine tagged sum is close to . By [L5], choose one grid below the convergence mesh threshold and, using [L4], tag each cell near its supremum and then near its infimum. The two tagged sums approximate and , so their common closeness to makes the Darboux gap arbitrarily small.
Apply [L2] in step 1.2. Since the near-upper and near-lower tagged sums are both arbitrarily close to , the common lower/upper integral lies arbitrarily close to and therefore equals . Both directions give the same value.
Depends on
- Tagged grid partitions and Riemann sums in $\mathbb{R}^m$
- The lower and upper Darboux integrals over a nondegenerate rectangle in $\mathbb{R}^m$
- Riemann's criterion on a nondegenerate rectangle in $\mathbb{R}^m$: integrability is equivalent to arbitrarily small Darboux gaps
- Refinement raises multidimensional lower sums and lowers upper sums, with a quantitative boundary-slab estimate
- Lower and upper Darboux sums over a grid partition in $\mathbb{R}^m$
- Grid partitions of a rectangle in $\mathbb{R}^m$, their cells, refinements and mesh
- For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
- Epsilon characterisation of the supremum
- Epsilon characterisation of the infimum
- Every natural-number-indexed list of nonempty sets has a choice function on its family of values
Used by
- A C¹ diffeomorphism satisfies the change-of-variables formula for L¹ functions Corollary
- At m=1, nondegenerate multidimensional rectangles, grid sums and the integral are exactly the published one-dimensional notions Corollary
- A deterministic integral construction of a Gaussian process Example
- Borel change of variables from the compact-support formula and Radon uniqueness Lemma
- Borel Darboux integrands in finite dimension Lemma
- Finite sums of product tests are dense on product open sets Lemma
- Riemann–Lebesgue comparison for distribution test integrands Lemma
- Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in ℝᵐ Theorem
- The cylindrical-shell formula for a solid of revolution about the y-axis Theorem
Dependency tree · two levels
36 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
- 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)