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.
Every finite Borel measure on splits as an atomic part plus an atomless part
Statement
Assume the Axiom of Countable Choice. Let be a finite Borel measure on . Then there are a countable set and a finite atomless Borel measure such that
The set is exactly the set of atoms of .
Facts & Assumptions
Given: The Axiom of Countable Choice and a finite Borel measure on .
Assuming Countable Choice, finite-on-compacts Borel measures correspond to increasing right-continuous distribution functions, and the resulting Lebesgue-Stieltjes measure is the original measure. (Assuming countable choice, finite-on-compacts Borel measures on correspond to nondecreasing right-continuous functions modulo constants)
For a Lebesgue-Stieltjes measure, atoms are exactly positive jumps, and there are at most countably many of them. (Interval formulas and atoms for a Lebesgue-Stieltjes measure)
Every Dirac measure is a probability measure, and countable nonnegative weighted sums of measures are measures. (A Dirac set function is a probability measure, Nonnegative scalar multiples and countable weighted sums of measures are measures)
Proof
Let be the distribution function of . By [L1], one has . Therefore [L2] shows that the atom set.
is at most countable. If , then for every , so is already atomless; taking proves the theorem. Otherwise choose an injective enumeration , where if is finite and if is infinite.
By [L3], the weighted Dirac sum
is a Borel measure. For every Borel set ,
because the singletons are pairwise disjoint and countable additivity of applies to their union. [step 1.1, L3, algebra]
Define
Because remains pairwise disjoint whenever is, the same countable additivity as for shows that is a finite Borel measure. [step 2.1, given, algebra]
For every Borel set , the disjoint decomposition gives.
If , then ; if , then by definition of , so also . Hence is atomless. [step 2.1, step 3.1, algebra]
If , step 1.1 already gives the claimed decomposition. Otherwise step 4.1 is exactly that decomposition, and step 1.1 identifies as the atom set of .
Depends on
- An atom of a measure on $\mathbb{R}$
- The Dirac set function at a point
- A Dirac set function is a probability measure
- Assuming countable choice, finite-on-compacts Borel measures on $\mathbb{R}$ correspond to nondecreasing right-continuous functions modulo constants
- Nonnegative scalar multiples and countable weighted sums of measures are measures
- Interval formulas and atoms for a Lebesgue-Stieltjes measure
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
22 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
- Gerald B. Folland, Real Analysis, 2nd ed., Section 1.5 (standard reference, not scraped)