LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-09

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.

Borel Darboux integrands in finite dimension

Statement

Assume ${A C}_{ω}$ . Let $n \geq 1$ , let $Q = \prod_{j = 1}^{n} [a_{j}, b_{j}]$ with $a_{j} < b_{j}$ , and let $f : Q \to R$ be bounded and Borel. If $f$ is Riemann integrable, then $f \in L^{1} (λ_{n} ∣_{Q})$ and its Lebesgue and Riemann integrals agree.

Facts & Assumptions

Given: Assume ${A C}_{ω}$ . Manifolds are Hausdorff, second countable and smooth, with boundary allowed; $n = 0$ is allowed unless excluded. Densities are pointwise Borel, $0 \cdot \infty = 0$ , and $λ_{0} (R^{0}) = 1$ . Bounded Borel Riemann integrand on a nondegenerate n-box.

[F1]

Lower and upper Darboux sums over a grid partition in $R^{m}$ : Cell infima and suprema times cell volumes define lower and upper Darboux sums.

[F2]

The multidimensional Darboux and tagged-mesh definitions of the Riemann integral agree: Bounded Riemann integrability is equivalent to Darboux integrability with the same value.

[F3]

A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included: Each closed or half-open rectangle has the product of its side lengths as measure.

[F4]

A box with a degenerate side is Lebesgue null, and so is every coordinate hyperplane in $R^{n}$ : All grid faces are null.

[F5]

Monotonicity and nonnegative homogeneity of the nonnegative integral: Nonnegative integrals are monotone and homogeneous.

[F6]

The Lebesgue integral is linear on $L^{1} (μ)$ : The integral is linear on integrable functions.

[F7]

The integral of a nonnegative simple function: The integral of a nonnegative simple function on disjoint sets is the sum of coefficient times measure.

[F8]

The nonnegative integral agrees with the simple integral on simple functions: The nonnegative Lebesgue integral of a simple function equals its simple integral.

Proof

1.1

Choose a finite $C \geq 0$ with $∣ f ∣ \leq C$ , and put $g = f + C \geq 0$ . Its Borel measurability and $g \leq 2 C 1_{Q}$ imply $\int_{Q} g \leq 2 C \prod_{j} (b_{j} - a_{j}) < \infty$ . Likewise $\int_{Q} ∣ f ∣ \leq C \prod_{j} (b_{j} - a_{j})$ , so $f$ is integrable.

F3F5given

2.1

For a finite grid $P$ , list its closed cells $Q_{1}, \dots, Q_{m}$ and disjointify them as $D_{i} = Q_{i} ∖ ⋃_{j < i} Q_{j}$ . These are Borel and partition $Q$ ; each $D_{i}$ contains the interior of $Q_{i}$ and differs from it only by grid faces. Thus $λ_{n} (D_{i}) = vol (Q_{i})$ . Let $m_{i} = \inf_{Q_{i}} g$ and $M_{i} = \sup_{Q_{i}} g$ . Each cell is nonempty and $g$ bounded, so these are finite.

F1F3F4step 1.1

3.1

The nonnegative simple functions $l_{P} = \sum_{i} m_{i} 1_{D_{i}}$ and $u_{P} = \sum_{i} M_{i} 1_{D_{i}}$ satisfy $l_{P} \leq g \leq u_{P}$ everywhere, including every assigned face. Their integrals are respectively $L (g, P)$ and $U (g, P)$ . Hence $L (g, P) \leq \int_{Q} g \leq U (g, P)$ .

F1F5step 2.1F7F8

4.1

Every Riemann sum of $g$ equals the corresponding sum of $f$ plus $C vol (Q)$ , so $g$ is Riemann integrable with value $J = I_{R} (f) + C vol (Q)$ . Darboux equivalence gives $\sup_{P} L (g, P) = \inf_{P} U (g, P) = J$ . Taking supremum and infimum in the preceding bounds yields $\int_{Q} g = J$ .

F2step 3.1

5.1

The constant $C$ is integrable on $Q$ , so linearity gives $\int_{Q} f = \int_{Q} g - C λ_{n} (Q) = I_{R} (f)$ . If $C = 0$ , all these quantities are zero; the proof also applies to $n = 1$ and constant-one integrands. Degenerate boxes and dimension zero are outside the stated domain.

F3F6step 1.1step 4.1∎

Depends on

Used by

Weighted interval volume Example
Measurable integration extends smooth density integration Theorem

Dependency tree · two levels

46 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

Folland §2.2 simple integral, Proposition 2.13 pp.49–50; finite-dimensional Darboux adaptation of the local published one-dimensional comparison proof (standard reference, not scraped)