Alphabeta MathHow 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.
A nonnegative function can have both iterated integrals zero and no double Riemann integral
Statement refuted
If a bounded nonnegative function on has both ordinary iterated Riemann integrals and they are equal, then it has a double Riemann integral.
Facts & Assumptions
Given: Let consist of all with prime and , and let on .
Sections and ordinary iterated Riemann integrals are defined by integrating each fixed-coordinate section and then its section-integral function (Sections, lower and upper section integrals, and iterated Riemann integrals on product rectangles and Jordan sets).
A bounded function on a rectangle is Riemann integrable only if grids can make arbitrarily small (Riemann's criterion on a nondegenerate rectangle in : integrability is equivalent to arbitrarily small Darboux gaps).
The irrationals are dense in (Both and are dense in , and every nonempty open subset of is uncountable).
Changing a bounded integrand on a finite, hence content-zero, set does not change its Riemann integral (Changing a bounded integrand on a content-zero set does not change its Riemann integral).
For every finite list of primes there is a prime outside that list (Euclid's theorem: for every and every list of primes there is a prime not among ; consequently the set of primes is not finite).
For every real bound there is a natural number larger than it (Every complete ordered field is Archimedean).
Counterexample
A fixed coordinate belongs to at most one prime grid, because a fraction with is reduced and its prime denominator is unique. Thus each horizontal and vertical section of is finite; covering its finitely many points by intervals of arbitrarily small total length gives content zero, so [L4] makes every section of integrable with value zero. By [L1], both iterated integrals are zero.
By [L5] and [L6], primes are unbounded, so in every nonempty open rectangle in the unit square a sufficiently fine prime grid supplies a point of . By [L3], the same rectangle contains a point with irrational first coordinate, which is outside . Hence both and its complement are dense in the square.
Every nondegenerate grid cell therefore has supremum and infimum , so every Darboux gap equals the area of the unit square, namely . By [L2], is not double Riemann integrable.
Step 1.1 gives equal iterated integrals although step 2.1 gives no double integral, refuting the Statement.
Depends on
- Sections, lower and upper section integrals, and iterated Riemann integrals on product rectangles and Jordan sets
- Riemann's criterion on a nondegenerate rectangle in $\mathbb{R}^m$: integrability is equivalent to arbitrarily small Darboux gaps
- Euclid's theorem: for every $n \in \mathbb{N}$ and every list $p : n \to \mathbb{Z}$ of primes there is a prime not among $p_0, \dots, p_{n-1}$; consequently the set of primes is not finite
- Every complete ordered field is Archimedean
- Both $\mathbb{Q}$ and $\mathbb{R} \setminus \mathbb{Q}$ are dense in $\mathbb{R}$, and every nonempty open subset of $\mathbb{R}$ is uncountable
- Changing a bounded integrand on a content-zero set does not change its Riemann integral
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
53 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.