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.
A compact-metric probability representation using countable choice
Statement
Assume the Axiom of Countable Choice. Let be a nonempty compact metric space and let be real-linear, positive in the sense that implies , and normalized by . Then there is a Borel probability on with for every continuous real . It is outer regular on Borel sets and inner regular on open sets by compact subsets. No Dependent Choice is required.
Facts & Assumptions
Every open cover of has a finite subcover. Open cover, subcover, compact metric space, and compact subset of a metric space.
A closed subset of a compact metric space is compact. A closed subset of a compact metric space is compact.
The measurable sets of an outer measure form a sigma-algebra carrying its restriction as a complete measure. Carathéodory's theorem: measurable sets form a sigma-algebra carrying a complete measure.
The nonnegative integral is monotone and homogeneous. Monotonicity and nonnegative homogeneity of the nonnegative integral.
The Lebesgue integral is linear on integrable real functions. The Lebesgue integral is linear on .
Proof
Given: Assume the Axiom of Countable Choice. Let be a nonempty compact metric space and let be real-linear, positive in the sense that implies , and normalized by . Then there is a Borel probability on with for every continuous real . It is outer regular on Borel sets and inner regular on open sets by compact subsets. No Dependent Choice is required.
For an open set define when , and . The triangle inequality, followed by the infimum, shows that is 1-Lipschitz in the first case; it is positive at every point of because that point has a ball contained in , and it vanishes outside . If a nonempty closed lies in , the sets for positive integers cover . Adjoining and using [F1] gives a with on . Consequently equals 1 on , takes values in , and has support contained in . Here support means the closure in of the nonzero set, which is compact by [F2]. For use . Any compact subset of a metric space is closed: the empty subset is closed, and for a nonempty compact subset, if is outside it, its balls centered at of radii have a finite subcover; the minimum of these finitely many positive radii gives a ball at missing the subset. Thus these cutoffs apply also to every compact .
Write for continuous with and support contained in . Positivity and linearity give monotonicity of by applying positivity to differences, and by comparison with constants. The norm is finite: the open sets cover and a finite subcover bounds . Define and . The zero function and the open set make both families nonempty; , , and . Monotonicity immediately implies for open , and monotonicity and zero empty-set value for .
For a closed nonempty with finitely many open , put . Compactness, applied to the sets and , gives with on . Set and . Define where , and zero where . Near a zero of the formula is , proving continuity there. Each has support in , is nonnegative and at most 1, and on the open neighborhood of . For empty use all zero functions. This constructs a finite subordinate partition without any selection principle.
For open and , its closed support is covered by finitely many distinct by [F1] after adjoining . If is empty, . Otherwise the partition in step 2.1 gives , with . Hence ; taking the supremum proves open-set subadditivity. Given arbitrary and , countable choice now selects simultaneously open with . These are a specified countable family of nonempty sets of admissible opens. Thus . Letting decrease to zero proves that is an outer measure; if the sum on the right is infinite the inequality is immediate and no selection is needed.
For open and , with support . For any , the supports are disjoint, so . Therefore . Taking the supremum over gives . For arbitrary , monotonicity replaces in the two terms by ; taking the infimum over open proves . The opposite inequality is outer subadditivity. Thus every open is Carathéodory measurable, and [F3] gives a Borel measure . It satisfies and is outer regular by its defining infimum and .
For compact , one has . Indeed such is nonnegative everywhere, and for the open set contains . Every satisfies , whence , and then . Conversely for each open , step 1.1 supplies with on ; hence the displayed infimum is at most . Infimizing over gives the reverse inequality. Empty has both sides zero using . If and , then for every , so the compact formula gives . Taking the supremum over proves ; monotonicity proves equality. This is the required inner regularity on opens.
Let and . Choose a positive integer with , put , for , and . These are continuous, the are compact by [F2], , and . The compact formula gives the lower bound ; comparison with every continuous majorant of gives the upper bound . By [F4] the same bounds hold for . All these integrals are finite since and . Summing and applying [F5] locates both and in the same interval of length . Since is arbitrary they are equal. Finally proves equality for every real continuous , using positivity, linearity and [F5]. Countable choice was spent only on the admissible open supersets in step 3.1; the cutoffs and partitions are explicit metric formulas.
Depends on
- Open cover, subcover, compact metric space, and compact subset of a metric space
- A closed subset of a compact metric space is compact
- Carathéodory's theorem: measurable sets form a sigma-algebra carrying a complete measure
- Monotonicity and nonnegative homogeneity of the nonnegative integral
- The Lebesgue integral is linear on $L^1(\mu)$
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
Dependency tree · two levels
28 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
- Compact-metric adaptation of the RMK construction; Cohn, Measure Theory, 2nd ed., Chapter 7 (standard reference, not scraped)