In this file we work with contents. A content
λ is a function from a certain class of subsets
(such as the compact subsets) to
ℝ≥0 that is
- additive: If
K₂are disjoint sets in the domain of
λ(K₁ ∪ K₂) = λ(K₁) + λ(K₂);
- subadditive: If
K₂are in the domain of
λ(K₁ ∪ K₂) ≤ λ(K₁) + λ(K₂);
- monotone: If
K₁ ⊆ K₂are in the domain of
λ(K₁) ≤ λ(K₂).
We show that:
- Given a content
λon compact sets, let us define a function
λ*on open sets, by letting
λ* Ube the supremum of
U. This is a countably subadditive map that vanishes at
∅. In Halmos (1950) this is called the inner content
λ, and formalized as
- Given an inner content, we define an outer measure
μ*, by letting
μ* Ebe the infimum of
λ* Uover the open sets
E. This is indeed an outer measure. It is formalized as
- Restricting this outer measure to Borel sets gives a regular measure
We define bundled contents as
In this file we only work on contents on compact sets, and inner contents on open sets, and both
contents and inner contents map into the extended nonnegative reals. However, in other applications
other choices can be made, and it is not a priori clear what the best interface should be.
Main definitions #
μ : Content G, we define
μ.innerContent: the inner content associated to
μ.outerMeasure: the outer measure associated to
μ.measure: the Borel measure associated to
We prove that, on a locally compact space, the measure
μ.measure is regular.
- Paul Halmos (1950), Measure Theory, §53
A content is an additive function on compact sets taking values in
ℝ≥0. It is a device
from which one can define a measure.
toFun field of a content takes values in
ℝ≥0, we register a coercion to
functions taking values in
ℝ≥0∞ as most constructions below rely on taking iSups and iInfs, which
is more convenient in a complete lattice, and aim at constructing a measure.
Constructing the inner content of a content. From a content defined on the compact sets, we obtain a function defined on all open sets, by taking the supremum of the content of all compact subsets.
This is "unbundled", because that is required for the API of
The inner content of a supremum of opens is at most the sum of the individual inner contents.
The inner content of a union of sets is at most the sum of the individual inner contents.
This is the "unbundled" version of
It is required for the API of
For the outer measure coming from a content, all Borel sets are measurable.
In a locally compact space, any measure constructed from a content is regular.
μ is a regular content, then the measure induced by
μ will agree with
on compact sets.