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.
The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition
Statement
Let and let be an elementary set (Elementary sets: the finite unions of half-open boxes in ). If
for finite lists of pairwise disjoint half-open boxes (Half-open boxes in and their volume), then
in . Consequently there is exactly one function , the elementary volume, 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 .
Facts & Assumptions
Given: A natural number , an elementary set , and two presentations by finite lists of pairwise disjoint half-open boxes.
Every elementary set has a presentation as a finite pairwise disjoint union of half-open boxes. Applied to the concatenated list , the generated grid has pairwise disjoint cells whose union is ; for every member of the list, a cell that meets it is contained in it, and that member is the union of the cells contained in it (Every elementary set is a finite disjoint union of half-open boxes, and any finitely many boxes admit a common grid refinement).
For a nonempty box and strictly increasing lists with , the cells are nonempty pairwise disjoint boxes with union and (The volume of a half-open box is the sum of the volumes of the cells of any coordinate grid subdividing it).
, and a box is nonempty exactly when for every (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 ).
For sequences of reals, , and if then (Laws of finite sums and finite products, claims 1 and 3).
Finite sums of a sequence of reals are defined by the recursion , , written (Finite sums and finite products, by recursion).
Proof
Let be the cells of the grid generated by the concatenated list, indexed by the multi-indices with for ; they are nonempty, pairwise disjoint, cover , and each of them is either contained in or disjoint from each and each .
If one of the boxes in either decomposition has infinite volume, then both sums are and there is nothing left to prove. Indeed, by [L3] a nonempty box has infinite volume exactly when some endpoint is infinite, and such a box is unbounded. Conversely, a finite union of boxes all of whose endpoints are real is bounded: for each such box every coordinate of every point of lies between the real endpoints and , so choosing one real bound for each box and then taking the maximum over the finite list bounds the whole union. Therefore, if contains an unbounded box from one decomposition, the other decomposition cannot consist entirely of finite-volume boxes, since that would make bounded. So it remains only to treat the case in which every and every has finite volume; from now on all the volumes that appear are real numbers and the finite-sum laws of [F1] apply to them.
For each let when and otherwise; then , because for no cell is contained in it and both sides are , while for nonempty the parameters and occur among the grid points, say and with , the cells contained in are exactly those with in every coordinate, the lists subdivide so that [L2] applies, and widening each summation range from to only inserts zero terms.
A cell is contained in exactly when it is contained in exactly one , since a cell contained in meets , hence meets some and is contained in it, while a cell contained in two of the pairwise disjoint boxes would be empty; so, writing when and otherwise, one has for every .
Summing the identities of step 2.1 over and regrouping the resulting finite real sums by repeated use of the additivity law in [F1] gives . Since step 2.2 identifies the inner sum with , this is .
The right-hand side of step 3.1 is built from and the grid alone, and the same computation applied to the list , whose parameters also generate the same grid, gives for the same value; hence the two sums agree, and since every elementary set has at least one presentation by a finite list of pairwise disjoint half-open boxes, the assignment is a well-defined function on with and for a single box.
Depends on
- Elementary sets: the finite unions of half-open boxes in $\mathbb{R}^n$
- Every elementary set is a finite disjoint union of half-open boxes, and any finitely many boxes admit a common grid refinement
- The volume of a half-open box is the sum of the volumes of the cells of any coordinate grid subdividing it
- Half-open boxes in $\mathbb{R}^n$ and their volume
- Finite sums and finite products, by recursion
- Laws of finite sums and finite products
- Series in the nonnegative extended real line
- The extended real line $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$, its order, and the arithmetic that is left undefined
Used by
- Countable covers by closed boxes, by open boxes and by closed cubes all compute Lebesgue outer measure Lemma
- Every elementary set is squeezed in volume between a compact subset and an elementary set whose interior contains it Lemma
- Elementary volume is finitely additive, monotone and finitely subadditive on the elementary algebra Proposition
- Assuming countable choice, L(ℝⁿ) is a sigma-algebra containing every elementary set and λₙ is a complete measure extending elementary volume Theorem
- Assuming countable choice, the Lebesgue outer measure of an arbitrary subset of ℝⁿ is the infimum of the measures of the open sets containing it Theorem
- Elementary volume is a sigma-finite premeasure on the algebra of elementary sets Theorem
- Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation Theorem
Dependency tree · two levels
30 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
- T. Tao, An Introduction to Measure Theory (GSM 126), Section 1.1 (standard reference, not scraped)
- John K. Hunter, Measure Theory (UC Davis lecture notes), Chapter 2 (standard reference, not scraped)