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.
Measure zero (a countable cover by intervals of total length below every ) and content zero (a finite such cover)
Definition
Throughout, is the complete ordered field (Complete ordered field (least-upper-bound property)), intervals and their lengths are as in Intervals of : the nine order-convex forms, nondegeneracy, and length, and a sequence is a function on , which contains . Let .
- has measure zero, equivalently is null, when for every real there are sequences and of reals with for every , such that
- has content zero when for every real there are and reals with
The number is the length of (Intervals of : the nine order-convex forms, nondegeneracy, and length), and the sums are the series and the finite sums of Series, partial sums, convergence and the sum, divergence, and the tail series and Finite sums and finite products, by recursion.
Working form: only the partial sums have to be checked. All the terms are , so by claim 2 of A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum the series converges exactly when its partial sums are bounded above, and its sum is then their supremum. Consequently, for a fixed ,
since a supremum is exactly when is an upper bound of the set it is the supremum of (Complete ordered field (least-upper-bound property)). Every verification of nullity below checks the right-hand condition.
Closed intervals lose nothing. A bounded interval with endpoints is contained in and has the same length (Intervals of : the nine order-convex forms, nondegeneracy, and length), so a cover by intervals of any of the four bounded forms yields a cover by closed intervals with the same lengths. The definition is therefore stated with closed intervals once and for all. Covers by open intervals are a genuinely different demand, and passing to one costs a little extra length: the enlargement is carried out where it is needed, in A sequence of intervals covering has total length at least , so no interval of positive length has measure zero and in For a compact subset of , measure zero and content zero coincide.
Both notions are inherited by subsets. If and is null, then any cover of covers , so is null; the same sentence with finite covers shows a subset of a set of content zero has content zero.
A finite cover is a countable cover, so content zero implies measure zero. Padding the list with the degenerate intervals for leaves the total length unchanged, by the splitting law for finite sums (Laws of finite sums and finite products). This is recorded as a lemma with its proof, A set of content zero has measure zero, because it is cited on its own.
Remarks
-
The two notions genuinely differ. is null and does not have content zero ( has measure zero and not content zero, although it is bounded ↗), so the two quantifier patterns, "a sequence of intervals" and "a finite list of intervals", are not interchangeable. They do agree for compact sets (For a compact subset of , measure zero and content zero coincide), and the compact case is the only one in which content zero is used anywhere on this pair of pages. Nothing is claimed about what later pages will do with it.
-
Why "content" and not "measure" for the finite version. The finite-cover notion is the vanishing of the Jordan outer content, and the countable-cover notion is the vanishing of the Lebesgue outer measure. Neither outer quantity is available at this point in the reading order. Jordan outer content is defined later in Jordan inner and outer content and Jordan measurable bounded sets in ↗; Lebesgue outer measure is still not defined. No item on this page assigns a nonzero size to any set. Every statement is of the shape "can, or cannot, be covered by intervals of total length below such and such a bound". That is a deliberate restriction of scope at this point in the reading order, not a claim that the general notions are unavailable in mathematics.
-
Measure zero is not vacuous and not universal. No interval with two distinct endpoints is null (A sequence of intervals covering has total length at least , so no interval of positive length has measure zero), while every at most countable set is (Every at most countable subset of has measure zero) and so is the uncountable Cantor set (The Cantor set is compact, perfect, uncountable, nowhere dense and of measure zero, and it contains no interval of positive length, so its only nonempty connected subsets are single points). The three facts together are what make the notion worth having.
Depends on
Intervals of : the nine order-convex forms, nondegeneracy, and length
Series, partial sums, convergence and the sum, divergence, and the tail series
Finite, countably infinite, countable, uncountable
A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum
Finite sums and finite products, by recursion
Laws of finite sums and finite products
Complete ordered field (least-upper-bound property)