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

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_{\mathbb{Q}}$ , and Thomae's function $t$ with $t(x) = 1/q$ at a rational $x = p/q$ in lowest terms with $q \ge 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\ne0$ , 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 87 results over 20 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, Exercise 10.2.8 (standard reference, not scraped)