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.
Axis-parallel rectangles in and their volume
Definition
Fix a natural number . For with for , define The product is the recursively defined finite product of Finite sums and finite products, by recursion. The rectangle is nondegenerate when every , and it is a cube when all side lengths are equal.
Every factor is nonnegative, so volume is nonnegative. For a coordinate index , cutting at gives two rectangles whose volumes add to the original, by distributivity in that factor and Laws of finite sums and finite products. Under the standard identification ( as the set of functions , and , , are metrics on it, The -norms for rational , and ), this is the interval and its length.
Depends on
- $\mathbb{R}^n$ as the set of functions $n \to \mathbb{R}$, and $d_1$, $d_2$, $d_\infty$ are metrics on it
- The $p$-norms $\lVert x\rVert_p$ for rational $p \ge 1$, and $\lVert x\rVert_\infty$
- Finite sums and finite products, by recursion
- Laws of finite sums and finite products
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Canonical naturals are positive and strictly increasing
Used by
- At m=1, cube-nullity and cube-content-zero are exactly the published interval-cover notions Corollary
- At m=1, nondegenerate multidimensional rectangles, grid sums and the integral are exactly the published one-dimensional notions Corollary
- The Jordan content of the parallelepiped spanned by the columns of a square real matrix is the absolute value of its determinant Corollary
- Grid partitions of a rectangle in ℝᵐ, their cells, refinements and mesh Definition
- Jordan inner and outer content and Jordan measurable bounded sets in ℝᵐ Definition
- Lower and upper Darboux sums over a grid partition in ℝᵐ Definition
- Measure zero and content zero in ℝᵐ by countable and finite cube covers Definition
- Sections, lower and upper section integrals, and iterated Riemann integrals on product rectangles and Jordan sets Definition
- Tagged grid partitions and Riemann sums in ℝᵐ Definition
- The Riemann integral of a bounded function over a bounded Jordan measurable set Definition
- The support of a function on ℝⁿ and its compactly supported Riemann integral Definition
- The Cantor slab C×[0,1] has content zero in ℝ² Example
- The right triangle {(x,y)∈[0,1]²:x+y≤1} has Jordan content 1/2 Example
- The unit box in ℝᵐ has volume 1, and the integral of a constant c over it is c Example
- A finite rectangle cover admits grid control with arbitrarily small volume excess Lemma
- For compact subsets of ℝᵐ, measure zero and content zero coincide Lemma
- If every finite interval cover of A⊆ℝ has total length at least c, then every rectangle cover of A×[0,d] has total area at least cd Lemma
- Refinement raises multidimensional lower sums and lowers upper sums, with a quantitative boundary-slab estimate Lemma
- The Riemann integral over a Jordan set is independent of the bounding rectangle Lemma
- A bounded set is Jordan measurable iff its indicator is Riemann integrable, and the integral is its Jordan content Theorem
- A Lipschitz map ℝᵐ→ℝᵐ sends null sets to null sets Theorem
- Every continuous function on a closed nondegenerate rectangle in ℝᵐ is Riemann integrable Theorem
- Lebesgue's criterion in ℝᵐ: a bounded function on a closed nondegenerate rectangle is Riemann integrable iff its discontinuity set is null Theorem
- The graph of a continuous function on a closed nondegenerate rectangle in ℝᵐ has content zero in ℝᵐ⁺¹ Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 82 results over 22 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, Riemann Integral in Several Variables (standard reference, not scraped)
- J. Lebl, Basic Analysis, The Riemann-Lebesgue Criterion (standard reference, not scraped)