LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21

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.

Changing a bounded integrand on a content-zero set does not change its Riemann integral

Statement

Let $E \subseteq R^{m}$ be bounded and Jordan measurable, let $f, g : E \to R$ be bounded, and suppose ${x \in E : f (x) \neq g (x)}$ has content zero. Then $f$ is Riemann integrable over $E$ if and only if $g$ is, and when they are integrable their integrals are equal.

Facts & Assumptions

Given: The set and functions of the Statement, a nondegenerate bounding rectangle $Q \supseteq E$ , their zero extensions $\tilde{f}, \tilde{g}$ to $Q$ , and $N : = {x \in E : f (x) \neq g (x)}$ .

[L1]

Riemann integrability over $E$ means integrability of the zero extension on $Q$ (The Riemann integral of a bounded function over a bounded Jordan measurable set).

[L2]

A set has content zero when every positive volume allowance admits a finite closed-cube cover within that allowance (Measure zero and content zero in $R^{m}$ by countable and finite cube covers).

[L3]

If a subset of a rectangle is covered by finitely many rectangles of total volume $V$ , then a grid exists whose cells meeting the set have total volume below $V + η$ (A finite rectangle cover admits grid control with arbitrarily small volume excess).

[L4]

A bounded function on a nondegenerate rectangle is Riemann integrable exactly when grids can make its upper-minus-lower sum arbitrarily small (Riemann's criterion on a nondegenerate rectangle in $R^{m}$ : integrability is equivalent to arbitrarily small Darboux gaps).

[L5]

Proper multidimensional Riemann integrals are linear (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ ).

Proof

technique · cases

1.1

Put $h : = \tilde{g} - \tilde{f}$ . It is bounded, vanishes on $Q ∖ N$ , and has some bound $∣ h ∣ \leq M$ .

L1algebra

2.1

In the case $M = 0$ , the function $h$ is identically zero, hence integrable with integral zero.

assume-case zerostep 1.1L4

2.2

In the case $M > 0$ , given $ε > 0$ , [L2] covers $N$ by finitely many cubes of total volume below $ε / (4 M)$ , and [L3] gives a grid whose cells meeting $N$ have total volume below $ε / (2 M)$ . On all other cells $h = 0$ , while on a cell meeting $N$ its oscillation is at most $2 M$ , so the total Darboux gap is below $ε$ . Thus [L4] makes $h$ integrable; the bounds $- M 1_{N} \leq h \leq M 1_{N}$ with the same grids force its integral to be zero.

assume-case posstep 1.1L2L3L4choose

3.1

The two cases exhaust $M \geq 0$ , so $h$ is integrable with integral zero. If $f$ is integrable, then $\tilde{g} = \tilde{f} + h$ is integrable and has the same integral by [L5].

step 2.1step 2.2L5cases-exhaustive

4.1

Interchanging $f$ and $g$ applies step 3.1 to $- h$ , proving the reverse integrability implication and the same equality of values.

step 1.1step 3.1L5∎

Depends on

Used by

Dependency tree · two levels

33 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

M. E. Taylor, Introduction to Analysis in Several Variables, §3.1 (standard reference, not scraped)
W. F. Trench, Introduction to Real Analysis, §7.3 (standard reference, not scraped)