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.
Elementary volume is a sigma-finite premeasure on the algebra of elementary sets
Statement
Let , let be the algebra of elementary subsets of (The elementary sets form an algebra of subsets of containing every half-open box) and let be elementary volume (The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition). Then is a sigma-finite premeasure on (Premeasures on algebras of sets): ; whenever is a pairwise disjoint sequence in whose union again lies in ,
and with for every .
No choice principle is used. The one place where a textbook proof selects countably many objects is the enlargement of each , and here the enlarged set is the canonical of Every elementary set is squeezed in volume between a compact subset and an elementary set whose interior contains it with the least natural number that works, which is a definition rather than a selection. The compact inner set and the finite subcover are each a single instantiation of an existential statement.
Facts & Assumptions
Given: A natural number , the algebra with elementary volume , and a pairwise disjoint sequence in whose union lies in .
is an algebra of subsets of , it contains every half-open box, and it is closed under intersection of two members and under difference (The elementary sets form an algebra of subsets of containing every half-open box).
For every , there is exactly one function whose value at is the sum of the volumes of the members of any presentation of by a finite list of pairwise disjoint half-open boxes; it satisfies and for every half-open box (The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition).
Elementary volume is finitely additive on pairwise disjoint elementary sets, monotone, and finitely subadditive (Elementary volume is finitely additive, monotone and finitely subadditive on the elementary algebra).
is an elementary set, it is determined by and alone, it contains , and every point of is an interior point of in (Every elementary set is squeezed in volume between a compact subset and an elementary set whose interior contains it, claim 1).
For every real there is with (Every elementary set is squeezed in volume between a compact subset and an elementary set whose interior contains it, claim 2).
If , then for every real there are an elementary set and a compact set with and (Every elementary set is squeezed in volume between a compact subset and an elementary set whose interior contains it, claim 3).
For a nonempty box when or for some , and when every and every is real; ; and (Half-open boxes in and their volume).
A subset is an elementary set when there are a natural number and a list of half-open boxes with (Elementary sets: the finite unions of half-open boxes in ).
A premeasure on an algebra vanishes at the empty set and is countably additive whenever a disjoint sequence in has its union in ; it is sigma-finite if there is a sequence in with and for every (Premeasures on algebras of sets).
The nonnegative extended sum of a sequence in is , the supremum of its nondecreasing partial sums (Series in the nonnegative extended real line).
is a compact subset of if and only if for every set and every family of open subsets of with there are and indices with , or else (A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it, claim 3; Open cover, subcover, compact metric space, and compact subset of a metric space).
The interior is open, and it is the largest open subset of (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).
Every nonempty subset has a least element (The well-ordering principle).
If then ; in particular (For , , and for the series diverges).
Every complete ordered field is Archimedean: for every there is a natural number with (Every complete ordered field is Archimedean).
For sequences of reals, ; if for all then ; and if for all then , with when every (Laws of finite sums and finite products, claims 1, 4 and 6).
Finite sums and finite products of a sequence of reals are defined by the recursions , and , (Finite sums and finite products, by recursion).
For , when and , or and (The extended real line , its order, and the arithmetic that is left undefined).
Proof
is a function on the algebra with values in and , which is the first premeasure clause.
Each cube is a half-open box, hence elementary, with for and ; and , because for the Archimedean property supplies a natural above each of the finitely many reals .
For every , finite additivity gives and monotonicity gives , so every partial sum is at most and therefore , that supremum being the nonnegative extended sum.
Suppose and let be real. Fix an elementary and a compact with and ; for each let be the least natural number with , which exists because the set of such naturals is nonempty and is well ordered, and put , an open set containing . Since , compactness yields finitely many indices covering , hence a natural with , so that ; monotonicity, finite subadditivity and the geometric series then give , whence ; as was an arbitrary positive real and is finite, .
Suppose instead and put ; if then holds, and if a contradiction follows. Fix a disjoint box presentation ; some has infinite volume, hence is nonempty with or for some . Take and put when and otherwise, so that and , where for and . For a real exceeding every and every , the box with parameter pairs for and , respectively , in coordinate according as or , satisfies and has volume at least . On the other hand is elementary of finite volume and is the disjoint union of the elementary sets , so step 1.4 and monotonicity give ; taking above by the Archimedean property contradicts this.
Steps 1.3, 1.4 and 2.1 give in every case, which with steps 1.1 and 1.2 makes a sigma-finite premeasure on .
Depends on
- The elementary sets form an algebra of subsets of $\mathbb{R}^n$ containing every half-open box
- The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition
- Elementary volume is finitely additive, monotone and finitely subadditive on the elementary algebra
- Every elementary set is squeezed in volume between a compact subset and an elementary set whose interior contains it
- Premeasures on algebras of sets
- Elementary sets: the finite unions of half-open boxes in $\mathbb{R}^n$
- Half-open boxes in $\mathbb{R}^n$ and their volume
- Series in the nonnegative extended real line
- The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
- Interior, closure, boundary, limit point, isolated point and dense subset of a metric space
- Open cover, subcover, compact metric space, and compact subset of a metric space
- A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it
- For $|r| < 1$, $\sum_{k \ge 0} r^k = 1/(1-r)$, and for $|r| \ge 1$ the series diverges
- The well-ordering principle
- Every complete ordered field is Archimedean
- The extended real line $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$, its order, and the arithmetic that is left undefined
- Laws of finite sums and finite products
- Finite sums and finite products, by recursion
Used by
- L(ℝⁿ) is exactly the completion of the restriction of λₙ to the Borel sets Corollary
- Lebesgue outer measure on ℝⁿ Definition
- Assuming countable choice, L(ℝⁿ) is a sigma-algebra containing every elementary set and λₙ is a complete measure extending elementary volume Theorem
- Assuming countable choice, Lebesgue outer measure is an outer measure that restricts to elementary volume Theorem
Dependency tree · two levels
73 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
- E. A. Carlen, Notes on Lebesgue Measure on $\mathbb{R}^n$ and $S^{n-1}$ (Rutgers Math 501), Theorem 1.1 (standard reference, not scraped)
- John K. Hunter, Measure Theory (UC Davis lecture notes), Chapter 2 (standard reference, not scraped)