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 Riemann integral over a Jordan set is independent of the bounding rectangle
Statement
The definition of is independent of the chosen bounding rectangle.
Facts & Assumptions
Given: Nondegenerate bounding rectangles for .
There is a nondegenerate rectangle that contains both strictly in every coordinate: decrease each of the finitely many lower endpoints and increase each upper endpoint by any fixed positive margin (Axis-parallel rectangles in and their volume).
Coordinate-slice additivity, including its converse integrability clause, is part of Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in .
A bounded function on a nondegenerate rectangle is integrable when its discontinuity set is null (Lebesgue's criterion in : a bounded function on a closed nondegenerate rectangle is Riemann integrable iff its discontinuity set is null), and the indicator of a Jordan measurable set integrates to its Jordan content (A bounded set is Jordan measurable iff its indicator is Riemann integrable, and the integral is its Jordan content).
Proof
Extend the zero extension on further by zero to . Cut at the lower and upper endpoint of in each coordinate. The strict containment in [L1] and nondegeneracy of make every cut strictly interior. On every added nondegenerate subrectangle the restriction is zero away from the finitely many coordinate faces of ; only shared boundary points may retain nonzero values.
Every bounded piece of a coordinate hyperplane has content zero: subdivide its bounded -dimensional coordinate ranges into cubes of side at most , and thicken the fixed coordinate by the same amount. The number of cubes grows at most as a fixed multiple of , so their total -volume is at most a fixed multiple of , which can be made arbitrarily small (Measure zero and content zero in by countable and finite cube covers, For every in a complete ordered field there is a natural with ). Finite unions preserve this estimate. Thus the exceptional face set from step 1.1 is Jordan measurable with content zero, and [L3] gives .
On each added subrectangle the extended function is bounded and is zero off , so its discontinuities lie in the null set . It is integrable by [L3]. If , then ; monotonicity and the absolute-value estimate in [L2] give . Hence every added subrectangle has integral .
Repeated coordinate-slice additivity [L2] now says that the extension is integrable on exactly when it is integrable on , and its integral equals the -integral because every added integral is . Applying this to gives the same integrability decision and value in both rectangles.
Depends on
- The Riemann integral of a bounded function over a bounded Jordan measurable set
- Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $\mathbb{R}^m$
- Lebesgue's criterion in $\mathbb{R}^m$: a bounded function on a closed nondegenerate rectangle is Riemann integrable iff its discontinuity set is null
- A bounded set is Jordan measurable iff its indicator is Riemann integrable, and the integral is its Jordan content
- Measure zero and content zero in $\mathbb{R}^m$ by countable and finite cube covers
- Grid partitions of a rectangle in $\mathbb{R}^m$, their cells, refinements and mesh
- Axis-parallel rectangles in $\mathbb{R}^m$ and their volume
- For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
Used by
- The Riemann integral of a compactly supported function is independent of its bounding rectangle Lemma
- A continuous real function on a compact Jordan measurable set is Riemann integrable over that set Theorem
- Change of variables for an injective C¹ map on a compact Jordan set Theorem
- Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable Theorem
Cited to discharge well-definedness by The Riemann integral of a bounded function over a bounded Jordan measurable set.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 145 results over 25 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, Jordan Measurable Sets (standard reference, not scraped)
- J. Lebl, Basic Analysis, Outer Measure and Null Sets (standard reference, not scraped)