CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck 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.

One existing iterated integral does not imply multiple Riemann integrability

Statement refuted

False claim. If one ordinary iterated Riemann integral of a bounded function on a rectangle exists, then the function is Riemann integrable on the rectangle.

Facts & Assumptions

Given: On $[- 1, 1] \times [0, 1]$ , let $f (x, y) = x$ for rational $y$ and $f (x, y) = 0$ for irrational $y$ .

[L1]

Rational and irrational numbers are dense, and the Dirichlet function takes the values $1$ and $0$ on them respectively (The Dirichlet function $1_{Q}$ , and Thomae's function $t$ with $t (x) = 1 / q$ at a rational $x = p / q$ in lowest terms with $q \geq 1$ and $t (x) = 0$ at every irrational $x$ ).

[L2]

For an integrable function, Riemann--Fubini makes the lower and upper section-integral envelopes integrable with the same multiple integral (Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections).

Counterexample

technique · direct

1.1

For each fixed $y$ , the $x$ -section is either $x \mapsto x$ or zero; both have integral $0$ on $[- 1, 1]$ . Hence the $x$ -first iterated integral exists and is $0$ .

given

1.2

For fixed $x \neq 0$ , density in [L1] makes every lower and upper Darboux sum of the $y$ -section equal to the interval length times $\min (x, 0)$ and $\max (x, 0)$ respectively. Thus the section is nonintegrable, and integrating its lower and upper integral functions in $x$ gives $- 1 / 2$ and $1 / 2$ .

L1given

2.1

If $f$ were multiply Riemann integrable, [L2] would force those two envelope integrals to agree. They do not, so $f$ is not Riemann integrable although the iteration in step 1.1 exists. This refutes the claim.

L2step 1.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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

J. Lebl, Basic Analysis II, Exercise 10.2.8 (standard reference, not scraped)