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.
Assuming countable choice, finite-on-compacts Borel measures on correspond to nondecreasing right-continuous functions modulo constants
Statement
Assume the Axiom of Countable Choice. Let be a Borel measure on finite on compact sets, and let be its normalized distribution function from The distribution function of a Borel measure on , normalized at . Then:
-
is nondecreasing and right-continuous;
-
for every ,
-
the Lebesgue-Stieltjes measure attached to is exactly .
Conversely, if are nondecreasing and right-continuous, then if and only if is constant on .
Facts & Assumptions
Given: Countable choice, a Borel measure on finite on compact sets, its distribution function , and two nondecreasing right-continuous functions .
Measures are continuous from above when one set in the decreasing chain has finite measure. (Continuity from above when one set has finite measure)
Assuming countable choice (The Axiom of Countable Choice ()), every nondecreasing right-continuous function defines a Borel measure on with the prescribed values on half-open intervals (Assuming countable choice, a nondecreasing right-continuous function defines a Borel measure on ). This is where the stated choice assumption is used.
A Borel measure finite on compact sets is uniquely determined by its values on half-open intervals . (The interval data on determines the Borel measure uniquely)
Proof
The function is nondecreasing.
If , then , so . If , then , so , again giving . If , then . [given, algebra]
Suppose first that . Then for every ,
So for all , and therefore is constant. [algebra]
Conversely, if is constant, then for every .
For every one has .
In the three sign cases:
and
So the displayed interval formula always holds. [step 1.1, given, algebra]
The function is right-continuous. Fix and let with .
For all large one has when , while for no sign change occurs. In either case, step 2.1 gives
The sets decrease to , and the first one has finite measure because it is contained in a compact interval. Therefore [L1] gives , so . [step 2.1, L1]
By [L3], the function determines a Lebesgue-Stieltjes measure .
Step 2.1 says that and agree on every half-open interval, so [L4] gives . [step 2.1, step 3.1, L3, L4]
The interval values of and therefore agree by [L3], and [L4] yields . Together with steps 1.1, 1.2, 1.3, 2.1, and 3.1 this proves the theorem. [step 1.1, step 1.2, step 1.3, step 2.1, step 3.1, L3, L4] ∎
Depends on
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- The distribution function of a Borel measure on $\mathbb{R}$, normalized at $0$
- Continuity from above when one set has finite measure
- Continuity from below for measures
- Assuming countable choice, a nondecreasing right-continuous function defines a Borel measure on $\mathbb{R}$
- The interval data on $(a,b]$ determines the Borel measure uniquely
Used by
- Arcsine equilibrium measure and capacity of a segment Example
- Two different normalizations give the same Lebesgue-Stieltjes measure Example
- FALSE: a Lebesgue-Stieltjes measure determines its distribution function uniquely False statement
- A monotone function is differentiable almost everywhere by the Lebesgue-Stieltjes route Theorem
- A right-continuous nondecreasing function splits uniquely as absolutely continuous plus jump plus singular continuous Theorem
- Every finite Borel measure on ℝ splits as an atomic part plus an atomless part Theorem
- Interval formulas and atoms for a Lebesgue-Stieltjes measure Theorem
- Lebesgue-Stieltjes measures on ℝ are outer regular and inner regular by compact sets Theorem
- Probability laws correspond to distribution functions Theorem
Dependency tree · two levels
23 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., Theorem 1.16 (standard reference, not scraped)
- John K. Hunter, Measure Theory, Theorem 2.34 (standard reference, not scraped)