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.
Series in the nonnegative extended real line
Definition
Let take values in (The extended real line , its order, and the arithmetic that is left undefined). Its partial sums are the unique sequence in satisfying
To apply The recursion theorem with a fixed successor function, use the state space and the self-map , starting from . Recursion gives a unique state sequence; induction makes its first coordinate , and its second coordinates are exactly the unique satisfying the displayed recurrence. Addition of two nonnegative extended reals is always defined, including when either is . The sequence is nondecreasing, and its nonnegative extended sum is
whose existence follows from completeness of the extended real line (Every subset of has a least upper bound and a greatest lower bound in , agreeing with the real supremum and infimum on nonempty sets bounded in ). More generally, for ,
Finite sums use the same recursion: , so the empty sum at is . A double sum such as means that the inner nonnegative extended sum is formed first and the resulting nonnegative extended sequence is then summed.
Depends on
- The extended real line $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$, its order, and the arithmetic that is left undefined
- Every subset of $\overline{\mathbb{R}}$ has a least upper bound and a greatest lower bound in $\overline{\mathbb{R}}$, agreeing with the real supremum and infimum on nonempty sets bounded in $\mathbb{R}$
- The recursion theorem
Used by
- Two-dimensional simple symmetric walk is recurrent Corollary
- Hausdorff content at a prescribed scale Definition
- Lebesgue outer measure on ℝⁿ Definition
- Measures on sigma-algebras Definition
- Nonnegative kernel action and finite drift Definition
- Nonnegative scalar multiples and countable weighted sums of measures Definition
- Outer measures Definition
- Premeasures on algebras of sets Definition
- Laziness makes an irreducible chain aperiodic Example
- Negative drift gives a finite mean small-set hit Example
- FALSE: measures are additive on arbitrary countable unions False statement
- A measurable set of positive finite measure occupies more than any prescribed proportion of some dyadic cube Lemma
- Boundary layers of finite metric outer measure exhaust the complement of a closed set in outer measure Lemma
- Countable covers by closed boxes, by open boxes and by closed cubes all compute Lebesgue outer measure Lemma
- For a Lebesgue measurable set and every positive ε there is an open superset whose difference from it has outer measure below ε Lemma
- Green-kernel resolvent identity Lemma
- Maximal dyadic cubes above a level Lemma
- Outer measure splits exactly over finite Carathéodory-measurable partitions Lemma
- The volume of a half-open box is the sum of the volumes of the cells of any coordinate grid subdividing it Lemma
- A Dirac set function is a probability measure Proposition
- Counting measure is a measure Proposition
- Elementary volume is finitely additive, monotone and finitely subadditive on the elementary algebra Proposition
- A measure on a finite sigma-algebra is a finite weighted sum over its atoms Theorem
- A subset of ℝ has Lebesgue outer measure zero if and only if it has measure zero in the sense of countable closed-interval covers Theorem
- A subset of ℝᵐ has Lebesgue outer measure zero if and only if it is null in the sense of countable closed-cube covers Theorem
- Assuming countable choice, Carathéodory measurability of a finite-outer-measure set is equivalent to source-algebra approximation Theorem
- Assuming countable choice, countable covering costs define an outer measure 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
- Continuity from below for measures Theorem
- Countable additivity and continuity of finitely additive set functions Theorem
- Countable disjoint unions of Carathéodory measurable sets are measurable and split every test set Theorem
- Elementary volume is a sigma-finite premeasure on the algebra of elementary sets Theorem
- Finite and countable subadditivity of measures Theorem
- First-step equations for nonnegative exit costs Theorem
- For a nonzero real c, dilation by c multiplies Lebesgue outer measure by |c|ⁿ, and reflection in the origin preserves it Theorem
- Hausdorff measure is an outer measure Theorem
- Hitting probability as minimal harmonic extension Theorem
- Lebesgue outer measure is at most Jordan outer content, and a bounded Jordan measurable set is Lebesgue measurable with Lebesgue measure equal to its Jordan content Theorem
- Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation Theorem
- Superharmonic majorants bound exit costs Theorem
…and 3 more results.
Dependency tree · two levels
15 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, Notation and §1.4.3 (standard reference, not scraped)