A finite regular measure from positive function covers
Written by GPT-6.1 Sol (OpenAI), Ultra, October 2026. Original exposition and embedded diagram: public domain (CC0).
Let be a compact metric space and let be positive and real linear. We construct the unique finite regular Borel measure representing . The starting point is a countable cover by nonnegative continuous functions: its cost is the sum of their functional values. Metric separation makes the resulting outer measure additive on separated sets. Compactness then recovers the functional from the measure.
This is a local construction in the classical Daniell–Stone viewpoint. An authorized free primary treatment of positive functionals and their representing measures is D. H. Fremlin, Measure Theory, Chapter 43, 436A–D, 436H–K and Exercise 436X(c), author-supplied TeX. Fremlin proves broader representation results for truncated Riesz spaces and locally compact Hausdorff spaces; Exercise 436X(c) also formulates an outer-measure construction from increasing continuous approximants. The construction below gives a complete positive-cover outer measure, metric measurability argument, compact-metric regularity proof and integral comparison. Its mathematical inputs are the complete scalar integration proofs, Sections 0–2, the elementary compact-metric facts SS2, the complete ordered real field and choice. No representation theorem is an input.
RM01. The outer measure and its total mass
If is empty, its function space, functional and measure are zero. Henceforth . Put . Positivity gives , monotonicity and
Indeed . In particular no boundedness hypothesis on has been added.
For any , define
Each nonnegative sum is the supremum of its finite partial sums. Finite covers are included by adjoining zeros. The constant function one gives a cover of every set, so . The zero sequence covers the empty set. Enlarging a set restricts its admissible covers, proving monotonicity.
To prove countable subadditivity, consider . If , the desired inequality is immediate. Otherwise, for , choose a function cover for each of cost less than . Enumerate all its functions by a single sequence, using diagonal enumeration of pairs of positive integers. The resulting sequence covers ; its total cost is the sum of the individual costs, by equality of the suprema over finite subsums of nonnegative numbers. Hence
Let . Thus is an outer measure.
Its total mass is exactly . Given a function cover of and , the increasing open sets cover . Compactness gives one index for which that partial sum exceeds everywhere. Positivity and linearity imply
Let and take the infimum over covers. The opposite bound was given by the constant cover, so
This proof also applies when .
RM02. Metric separation makes every Borel set measurable
If nonempty sets have distance , their distance functions are continuous and . Consequently
is continuous, lies in , is one on , and is zero on . Any function cover of splits into covers of and of . Linearity and nonnegative sums give
Take the infimum over covers and use subadditivity for the reverse inequality. Empty sets cause no change. We have proved
Here is the complete Borel-measurability argument, including the limiting step for an outer measure. Let be closed; the empty case is immediate. For an arbitrary , set
Any finite collection of the with indices of one parity consists of mutually separated sets. For indices differing by at least two, the distance-value ranges have a positive gap; the distance function is 1-Lipschitz, so this also separates the sets themselves. Taking a minimum over the finitely many gaps lets (RM4) be applied repeatedly to their union. Therefore each parity's finite sum of outer measures is at most , and
The tails of this nonnegative scalar series tend to zero by real completeness. Also
where the second inequality uses the separation of from . Subadditivity now gives
Let . The reverse inequality is subadditivity, so satisfies the Carathéodory condition. The complete Carathéodory proof in scalar integration, Section 1, says that the measurable sets form a sigma-algebra and that the outer measure restricts to a measure there. This sigma-algebra contains the closed sets, hence all Borel sets. Write
It is a finite Borel measure with mass . In particular, the preceding argument has not assumed continuity from below for arbitrary outer-measurable subsets before proving their measurability.
RM03. Regularity on every Borel set
A finite Borel measure on this compact metric space has both required approximations. If is closed, the open sets decrease to ; continuity from above gives . For , use the empty open set. If is open with nonempty complement, the closed sets increase to , so continuity from below gives . For , use . All the closed sets are compact.
To include every Borel set, let consist of the Borel sets such that for every there are closed and open with and . It contains closed sets by the preceding paragraph and is closed under complements: replace by .
For with , choose with , and put . Then . Since , continuity from below supplies with . The compact set then has . Combining the two errors gives . Thus is a sigma-algebra containing the closed sets, and contains every Borel set. We have proved
Finiteness is used in the continuity-from-above and finite-union approximation steps. This argument asserts full Borel regularity on compact metric ; it makes no stronger regularity assertion on an arbitrary noncompact space.
RM04. Recovering the functional
For a closed , the cover definition gives the exact compact-majorant identity
The measure is at most each displayed cost, since one function is an admissible cover. Conversely, for any function cover of and , compactness of supplies a finite partial sum at least on . Dividing it by gives a displayed majorant of cost at most . Take the infimum over covers and let . This proves (RM7), including . Clipping a majorant to preserves its value one on and only decreases its functional value. Thus, for , (RM3) and (RM7) give
If a continuous has zero set , put . These functions increase, lie in the set in (RM8), and
Indeed, for any in that set and , the compact set lies in . On a nonempty such set, has a positive minimum, so eventually there. Elsewhere ; hence everywhere. Positivity gives . Take the supremum over , then let , to prove (RM9). For the empty compact set the same bound is immediate. If , positivity of the minimum of makes eventually; if , all functions are zero.
Now fix continuous . For , define the Borel simple function and continuous approximants
At every point, including exact subdivision endpoints, and . Apply (RM9) to each continuous function , keeping fixed. Finite linearity and the simple-integral formula give
Since , the uniform bound on implies . Let . Applying this same inequality to , and using , gives the reverse inequality. Thus
Scaling treats every continuous nonnegative function, because it is bounded on . Positive and negative parts treat every real continuous function. For complex continuous , the complexification is consequently its complex integral.
An exact two-point example
Take , with distance one, and . The separator in (RM4) has , splitting every function cover into its two costs. Thus , and . For , the strict lower step in (RM10) at has . Consequently , , and their difference is exactly . The following diagram shows this example, including the strict-endpoint convention; it does not assert that a general representing measure is atomic.
RM05. Uniqueness and the exact supplied contract
Let be another finite regular Borel measure representing . For a nonempty closed , the continuous functions lie between zero and one and converge pointwise to . Scalar dominated convergence, with the constant majorant one integrable for both finite measures, gives
The empty set agrees as well. Both total masses equal , so complements give agreement on open sets. Outer regularity then gives agreement on every Borel set. This proves uniqueness.
The supplied theorem is exactly: every positive real-linear functional on , for every compact metric space , has a unique finite Borel measure representing it, outer regular and compact-inner-regular on every Borel set, with total mass ; complexification gives the complex integral identity. There is no countability condition on an ambient operator Hilbert space. Scalar completeness on arbitrary, possibly non-sigma-finite or noncomplete measure spaces is supplied separately by SS1 and its stated measurable-representative convention. The construction here does not replace the general locally compact Hausdorff theorem.