Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-11
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 of a compactly supported function is independent of its bounding rectangle

Statement

Let n≥1 and let f:Rn→R have compact support. If f is Riemann integrable on one closed rectangle whose interior contains its support, then it is integrable on every such rectangle, and all the resulting integrals are equal. This includes the empty-support case.

Facts & Assumptions

Given: Compactly supported f and bounding rectangles Q1,Q2 whose interiors contain its support.

[L1]

Extending an integrable function on a Jordan set by zero to a bounding rectangle gives a well-defined integral independent of that rectangle (The Riemann integral over a Jordan set is independent of the bounding rectangle).

[L2]

Cutting rectangles along coordinate hyperplanes preserves integrability and adds the integrals of the pieces (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in Rm).

Proof

technique · common-extension
1.1given

Choose a third rectangle Q whose interior contains Q1∪Q2. Since f=0 outside its support, extending f∣Qi by zero to Q recovers exactly f∣Q.

2.1L1L2step 1.1

If f∣Q1 is integrable, [L1] makes its zero extension integrable on Q with the same integral. Restricting this function to Q2 by the coordinate cuts in [L2] gives integrability there, again with zero contribution off the support.

3.1L1step 2.1∎

Applying [L1] to Q1 and Q2 inside the common rectangle yields ∫Q1f=∫Qf=∫Q2f. If the support is empty, all three functions are identically zero, so the same argument gives value 0.

Depends on

Dependency tree · 2 levels

Sources