Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-01
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 ∫Ef is independent of the chosen bounding rectangle.

Facts & Assumptions

Given: Nondegenerate bounding rectangles Q1,Q2 for E.

[L1]

There is a nondegenerate rectangle Q that contains both Q1,Q2 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 Rm and their volume).

[L2]

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 Rm.

[L3]

A bounded function on a nondegenerate rectangle is integrable when its discontinuity set is null (Lebesgue's criterion in Rm: 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

technique · direct
1.1

Extend the zero extension on Qi further by zero to Q. Cut Q at the lower and upper endpoint of Qi in each coordinate. The strict containment in [L1] and nondegeneracy of Qi make every cut strictly interior. On every added nondegenerate subrectangle the restriction is zero away from the finitely many coordinate faces of Qi; only shared boundary points may retain nonzero values.

L1given
2.1

Every bounded piece of a coordinate hyperplane has content zero: subdivide its bounded (m−1)-dimensional coordinate ranges into cubes of side at most 1/ι(N), and thicken the fixed coordinate by the same amount. The number of cubes grows at most as a fixed multiple of ι(N)m−1, so their total m-volume is at most a fixed multiple of 1/ι(N), which can be made arbitrarily small (Measure zero and content zero in Rm by countable and finite cube covers, For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε). Finite unions preserve this estimate. Thus the exceptional face set H from step 1.1 is Jordan measurable with content zero, and [L3] gives ∫1H=0.

step 1.1L3
3.1

On each added subrectangle the extended function is bounded and is zero off H, so its discontinuities lie in the null set H. It is integrable by [L3]. If ∣f∣≤B, then ∣h∣≤B1H; monotonicity and the absolute-value estimate in [L2] give ∣∫h∣≤∫∣h∣≤B∫1H=0. Hence every added subrectangle has integral 0.

step 1.1step 2.1L2L3
4.1

Repeated coordinate-slice additivity [L2] now says that the extension is integrable on Q exactly when it is integrable on Qi, and its integral equals the Qi-integral because every added integral is 0. Applying this to i=1,2 gives the same integrability decision and value in both rectangles.

step 3.1L2given∎

Depends on

Used by

Cited to discharge well-definedness by The Riemann integral of a bounded function over a bounded Jordan measurable set.

Dependency tree · two levels

52 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