mathlibdocumentation

measure_theory.measure.content

Contents #

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₁ and K₂ are disjoint sets in the domain of λ, then λ(K₁ ∪ K₂) = λ(K₁) + λ(K₂);
• subadditive: If K₁ and K₂ are in the domain of λ, then λ(K₁ ∪ K₂) ≤ λ(K₁) + λ(K₂);
• monotone: If K₁ ⊆ K₂ are in the domain of λ, then λ(K₁) ≤ λ(K₂).

We show that:

• Given a content λ on compact sets, let us define a function λ* on open sets, by letting λ* U be the supremum of λ K for K included in U. This is a countably subadditive map that vanishes at . In Halmos (1950) this is called the inner content λ* of λ, and formalized as inner_content.
• Given an inner content, we define an outer measure μ*, by letting μ* E be the infimum of λ* U over the open sets U containing E. This is indeed an outer measure. It is formalized as outer_measure.
• Restricting this outer measure to Borel sets gives a regular measure μ.

We define bundled contents as content. 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 #

For μ : content G, we define

• μ.inner_content : the inner content associated to μ.
• μ.outer_measure : the outer measure associated to μ.
• μ.measure : the Borel measure associated to μ.

We prove that, on a locally compact space, the measure μ.measure is regular.