Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableSession-authored (Fable 5 assisted)judge pass (z-ai/glm-5.2)audited 2026-07-27
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 ε\varepsilon) and content zero (a finite such cover)

Definition

Throughout, R\mathbb{R} is the complete ordered field (Complete ordered field (least-upper-bound property)), intervals and their lengths are as in Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length, and a sequence is a function on N\mathbb{N}, which contains 00. Let ARA \subseteq \mathbb{R}.

  • AA has measure zero, equivalently AA is null, when for every real ε>0\varepsilon > 0 there are sequences (ak)kN(a_k)_{k \in \mathbb{N}} and (bk)kN(b_k)_{k \in \mathbb{N}} of reals with akbka_k \le b_k for every kk, such that AkN[ak,bk]andk=0(bkak) converges with sum ε.A \subseteq \bigcup_{k \in \mathbb{N}} [a_k, b_k] \qquad \text{and} \qquad \sum_{k=0}^{\infty} (b_k - a_k) \text{ converges with sum } \le \varepsilon .
  • AA has content zero when for every real ε>0\varepsilon > 0 there are nNn \in \mathbb{N} and reals a0b0,,anbna_0 \le b_0, \dots, a_n \le b_n with Ajn[aj,bj]andj=0n(bjaj)ε.A \subseteq \bigcup_{j \le n} [a_j, b_j] \qquad \text{and} \qquad \sum_{j=0}^{n} (b_j - a_j) \le \varepsilon .

The number bkak0b_k - a_k \ge 0 is the length of [ak,bk][a_k,b_k] (Intervals of R\mathbb{R}: 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 bkakb_k - a_k are 0\ge 0, 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 ε>0\varepsilon > 0,

k=0(bkak) converges with sumεk<n(bkak)ε  for every nN,\sum_{k=0}^{\infty}(b_k - a_k) \text{ converges with sum} \le \varepsilon \quad \Longleftrightarrow \quad \sum_{k<n} (b_k - a_k) \le \varepsilon \ \text{ for every } n \in \mathbb{N},

since a supremum is ε\le \varepsilon exactly when ε\varepsilon 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 aba \le b is contained in [a,b][a,b] and has the same length (Intervals of R\mathbb{R}: 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 [ak,bk](akδk, bk+δk)[a_k,b_k] \subseteq (a_k - \delta_k,\ b_k + \delta_k) is carried out where it is needed, in A sequence of intervals covering [a,b][a,b] has total length at least bab - a, so no interval of positive length has measure zero and in For a compact subset of R\mathbb{R}, measure zero and content zero coincide.

Both notions are inherited by subsets. If BAB \subseteq A and AA is null, then any cover of AA covers BB, so BB 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 [a0,b0],,[an,bn][a_0,b_0], \dots, [a_n,b_n] with the degenerate intervals [0,0][0,0] for k>nk > n 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

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 65 results over 14 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