TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck 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.

Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections

Statement

Let $A\subseteq\mathbb R^p$ and $B\subseteq\mathbb R^q$ be nondegenerate closed rectangles, and let $f:A\times B\to\mathbb R$ be Riemann integrable. Then the four lower and upper section-integral functions of Sections, lower and upper section integrals, and iterated Riemann integrals on product rectangles and Jordan sets are Riemann integrable and $\int_A\ell_B=\int_Au_B=\int_{A\times B}f=\int_B\ell_A=\int_Bu_A.$

If the $B$ -sections are integrable outside a content-zero set $N\subseteq A$ , every bounded exceptionally completed function $h$ with $h(x)=\int_Bf_x$ for $x\notin N$ is integrable and $\int_{A\times B}f=\int_Ah.$ The same assertion holds with the coordinate blocks exchanged. In particular, when every section in an order is integrable, the ordinary iterated integral in that order exists and equals the multiple integral. The theorem does not assert that every section of an integrable function is integrable.

Facts & Assumptions

Given: Nondegenerate rectangles $A,B$ and a Riemann-integrable $f:A\times B\to\mathbb R$ .

[L1]

Product-grid Darboux sums bound the outer Darboux sums of the lower and upper section-integral functions (A product grid bounds the Darboux sums of the lower and upper section-integral functions).

[L2]

A bounded $f:Q\to\mathbb R$ on a nondegenerate rectangle is Riemann integrable if and only if, for every $\varepsilon>0$ , some grid $P$ satisfies $U(f,P)-L(f,P)<\varepsilon$ (Riemann's criterion on a nondegenerate rectangle in $\mathbb{R}^m$ : integrability is equivalent to arbitrarily small Darboux gaps).

[L3]

A content-zero set has finite cube covers of arbitrarily small total volume (Measure zero and content zero in $\mathbb{R}^m$ by countable and finite cube covers).

[L4]

The multidimensional Riemann integral is linear on integrable functions (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $\mathbb{R}^m$ ).

Proof

technique · direct

1.1

Given $\varepsilon>0$ , [L2] supplies a grid of $A\times B$ with Darboux gap below $\varepsilon$ . Its coordinate grids form a product grid, and [L1] places the lower and upper Darboux gaps of both $\ell_B$ and $u_B$ inside that same gap.

L1L2given

2.1

By [L2], both $\ell_B$ and $u_B$ are integrable. The inequalities in [L1], applied to grids with gaps tending to zero, give $\int_A\ell_B\ge\int_{A\times B}f$ and $\int_Au_B\le\int_{A\times B}f$ ; since $\ell_B\le u_B$ , all three values are equal. The same argument after exchanging $A$ and $B$ gives the other two equalities.

L2step 1.1algebra

3.1

Suppose $h=\int_Bf_x$ outside a content-zero $N$ . There $h=\ell_B=u_B$ . If $M$ bounds $|h|,|\ell_B|,|u_B|$ , a finite cube cover of $N$ with arbitrarily small total volume, refined into an outer grid, bounds the upper integral of $|h-\ell_B|$ by $2M$ times that volume. The criterion [L2] therefore makes $h-\ell_B$ integrable with integral $0$ , and linearity gives $\int_Ah=\int_A\ell_B=\int_{A\times B}f$ . The exchanged assertion is identical.

L2L3L4step 2.1algebra∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 70 results over 19 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 II, Theorems 10.2.2-10.2.3 (standard reference, not scraped)
A. Leibman, Multidimensional Real Analysis, Theorem 5.4.1 (standard reference, not scraped)