TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 multidimensional Darboux and tagged-mesh definitions of the Riemann integral agree

Statement

A bounded function on a nondegenerate rectangle is Darboux integrable with value $I$ if and only if all tagged grid sums converge with mesh to $I$ .

Facts & Assumptions

Given: A bounded $f:Q\to\mathbb R$ , with $|f|\le B$ , on a nondegenerate rectangle $Q$ .

[L1]

Every tagged sum lies between its grid's Darboux sums (Tagged grid partitions and Riemann sums in $\mathbb{R}^m$ ).

[L2]

Small Darboux gaps characterize integrability (Riemann's criterion on a nondegenerate rectangle in $\mathbb{R}^m$ : integrability is equivalent to arbitrarily small Darboux gaps).

[L3]

Refining by a fixed grid changes the bounds only by the boundary-slab estimate (Refinement raises multidimensional lower sums and lowers upper sums, with a quantitative boundary-slab estimate).

[L4]

Finite choice selects cell values within any positive distance of infima and suprema (Epsilon characterisation of the supremum, Epsilon characterisation of the infimum, Every natural-number-indexed list of nonempty sets has a choice function on its family of values).

[L5]

Repeated equal subdivision and the Archimedean reciprocal property give grid partitions of a nondegenerate rectangle with arbitrarily small mesh (Grid partitions of a rectangle in $\mathbb{R}^m$ , their cells, refinements and mesh, For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$ ).

Proof

technique · direct

1.1

If $f$ is Darboux integrable, choose a fixed grid $P_0$ with small gap by [L2]. For any sufficiently fine $P$ , refine it with $P_0$ ; [L3] makes the Darboux bounds of $P$ differ from those of the refinement by arbitrarily little. Since the refined lower and upper sums trap $I$ , [L1] makes every tagged sum over $P$ close to $I$ .

L1L2L3

1.2

Conversely, suppose every sufficiently fine tagged sum is close to $I$ . By [L5], choose one grid below the convergence mesh threshold and, using [L4], tag each cell near its supremum and then near its infimum. The two tagged sums approximate $U(f,P)$ and $L(f,P)$ , so their common closeness to $I$ makes the Darboux gap arbitrarily small.

L4L5given

2.1

Apply [L2] in step 1.2. Since the near-upper and near-lower tagged sums are both arbitrarily close to $I$ , the common lower/upper integral lies arbitrarily close to $I$ and therefore equals $I$ . Both directions give the same value.

step 1.1step 1.2L1L2∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 75 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, Riemann Integral in Several Variables (standard reference, not scraped)
J. Lebl, Basic Analysis, The Riemann-Lebesgue Criterion (standard reference, not scraped)