LemmaStatement: 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.

A product grid bounds the Darboux sums of the lower and upper section-integral functions

Statement

Let $A\subseteq\mathbb R^p$ and $B\subseteq\mathbb R^q$ be nondegenerate closed rectangles, let $f:A\times B\to\mathbb R$ be bounded, and let $P$ and $R$ be grids of $A$ and $B$ . With $\ell_B,u_B:A\to\mathbb R$ the lower and upper $B$ -section-integral functions of Sections, lower and upper section integrals, and iterated Riemann integrals on product rectangles and Jordan sets, $L(f,P\times R)\le L(\ell_B,P)\le U(\ell_B,P)\le U(u_B,P)\le U(f,P\times R).$ The symmetric chain holds after exchanging $A$ and $B$ . No individual section is assumed integrable.

Facts & Assumptions

Given: Rectangles $A,B$ , a bounded $f:A\times B\to\mathbb R$ , grids $P,R$ , and the section envelopes $\ell_B,u_B$ .

[L1]

For a bounded function on a product rectangle, the lower and upper section integrals are defined for every parameter even when the section is not Riemann integrable (Sections, lower and upper section integrals, and iterated Riemann integrals on product rectangles and Jordan sets).

[L2]

A grid cell of a product rectangle is the product of the corresponding cells of the two factor grids, and a sum over cells is the associated finite iterated sum (Grid partitions of a rectangle in $\mathbb{R}^m$ , their cells, refinements and mesh).

[L3]

Lower and upper Darboux sums are the finite sums of the cell infima and suprema weighted by cell volume (Lower and upper Darboux sums over a grid partition in $\mathbb{R}^m$ ); finite sums may be regrouped and preserve inequalities term by term (Laws of finite sums and finite products).

Proof

technique · direct

1.1

For a cell $I$ of $P$ and a cell $J$ of $R$ , put $m_{IJ}:=\inf_{I\times J}f$ and $M_{IJ}:=\sup_{I\times J}f$ . Regrouping the finite sums over the product grid gives $L(f,P\times R)=\sum_I\operatorname{vol}(I)\sum_Jm_{IJ}\operatorname{vol}(J)$ and the analogous formula with $M_{IJ}$ for the upper sum.

L2L3given

2.1

If $x\in I$ , then $\inf_J f_x\ge m_{IJ}$ and $\sup_Jf_x\le M_{IJ}$ for every $J$ . Hence $\ell_B(x)\ge\sum_Jm_{IJ}\operatorname{vol}(J)$ and $u_B(x)\le\sum_JM_{IJ}\operatorname{vol}(J)$ . Taking the infimum or supremum over $x\in I$ preserves these inequalities.

L1L3step 1.1algebra

3.1

Multiply the cellwise inequalities by $\operatorname{vol}(I)$ and sum over $I$ . Together with $\ell_B\le u_B$ , this gives the displayed chain. Exchanging the coordinate blocks gives the symmetric chain.

L1L3step 2.1algebra∎

Depends on

Used by

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

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 67 results over 21 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, §10.2, Exercises 10.2.2-10.2.3 (standard reference, not scraped)
A. Leibman, Multidimensional Real Analysis, §5.4 (standard reference, not scraped)