Alphabeta Math
TheoremStatement: Literature-sourcedProof: Literature-sourcedprecheck 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.

Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable

Statement

Let E⊆Rp+q be a bounded Jordan set and let g:E→R be Riemann integrable. Suppose that for all x outside a content-zero set N⊆Rp, the section Ex is Jordan measurable and gx is integrable over it. Put h(x)=∫Exgx there and assign arbitrary bounded values to h on N, with empty-section integral equal to 0. Then h is integrable on any rectangle containing the projection of E, its integral is independent of that rectangle and of the values on N, and ∫Eg=∫h(x) dx. The symmetric assertion holds for the other coordinate block.

Facts & Assumptions

Given: A bounded Jordan set E, an integrable g:E→R, and the stated content-zero exceptional family of sections.

[L1]

Riemann--Fubini applies to bounded functions on a product rectangle using lower and upper section integrals and a content-zero exceptional set (Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections).

[L2]

An empty Jordan section has integral zero, and section integrals are taken after zero extension to a bounding rectangle (Sections, lower and upper section integrals, and iterated Riemann integrals on product rectangles and Jordan sets).

[L3]

The Jordan-set integral is independent of the chosen bounding rectangle (The Riemann integral over a Jordan set is independent of the bounding rectangle).

Proof

technique · direct
1.1

Choose nondegenerate rectangles A⊆Rp and B⊆Rq with E⊆A×B, and extend g by zero to A×B. For every x, the resulting section is the zero extension to B of gx, and it is identically zero when Ex is empty.

L2given
2.1

The zero extension is integrable by the definition of the Jordan-set integral. Apply [L1]; outside N its ordinary section integral is exactly h(x), so the exceptional-section clause gives ∫Eg=∫Ah.

L1step 1.1
3.1

Enlarging A or B only adds zero to the zero extension. Independence of the Jordan integral from a bounding rectangle [L3] and the content-zero invariance in [L1] therefore prove independence of both factor rectangles and of the assigned values on N.

L1L2L3step 2.1algebra∎

Depends on

Used by

Dependency tree · two levels

23 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