Documentation

Mathlib.MeasureTheory.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 innerContent.
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 outerMeasure.
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

μ.innerContent : the inner content associated to μ.
μ.outerMeasure : the outer measure associated to μ.
μ.measure : the Borel measure associated to μ.

These definitions are given for spaces which are R₁. The resulting measure μ.measure is always outer regular by design. When the space is locally compact, μ.measure is also regular.

References #

Paul Halmos (1950), Measure Theory, §53
https://en.wikipedia.org/wiki/Content_(measure_theory)

structure MeasureTheory.Content (G : Type w) [TopologicalSpace G] :

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 : TopologicalSpace.Compacts G → NNReal
mono' (K₁ K₂ : TopologicalSpace.Compacts G) : ↑K₁ ⊆ ↑K₂ → self.toFun K₁ ≤ self.toFun K₂
sup_disjoint' (K₁ K₂ : TopologicalSpace.Compacts G) : Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → self.toFun (K₁ ⊔ K₂) = self.toFun K₁ + self.toFun K₂
sup_le' (K₁ K₂ : TopologicalSpace.Compacts G) : self.toFun (K₁ ⊔ K₂) ≤ self.toFun K₁ + self.toFun K₂

Instances For

instance MeasureTheory.instInhabitedContent {G : Type w} [TopologicalSpace G] :

Inhabited (Content G)

Equations

MeasureTheory.instInhabitedContent = { default := { toFun := fun (x : TopologicalSpace.Compacts G) => 0, mono' := ⋯, sup_disjoint' := ⋯, sup_le' := ⋯ } }

instance MeasureTheory.Content.instFunLikeCompactsENNReal {G : Type w} [TopologicalSpace G] :

FunLike (Content G) (TopologicalSpace.Compacts G) ENNReal

Equations

MeasureTheory.Content.instFunLikeCompactsENNReal = { coe := fun (μ : MeasureTheory.Content G) (s : TopologicalSpace.Compacts G) => ↑(μ.toFun s), coe_injective' := ⋯ }

@[simp]

theorem MeasureTheory.Content.toFun_eq_toNNReal_apply {G : Type w} [TopologicalSpace G] (μ : Content G) (K : TopologicalSpace.Compacts G) :

μ.toFun K = (μ K).toNNReal

@[simp]

theorem MeasureTheory.Content.mk_apply {G : Type w} [TopologicalSpace G] (toFun : TopologicalSpace.Compacts G → NNReal) (mono' : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), ↑K₁ ⊆ ↑K₂ → toFun K₁ ≤ toFun K₂) (sup_disjoint' : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → toFun (K₁ ⊔ K₂) = toFun K₁ + toFun K₂) (sup_le' : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), toFun (K₁ ⊔ K₂) ≤ toFun K₁ + toFun K₂) (K : TopologicalSpace.Compacts G) :

{ toFun := toFun, mono' := mono', sup_disjoint' := sup_disjoint', sup_le' := sup_le' } K = ↑(toFun K)

@[simp]

theorem MeasureTheory.Content.apply_ne_top {G : Type w} [TopologicalSpace G] (μ : Content G) {K : TopologicalSpace.Compacts G} :

μ K ≠ ⊤

@[deprecated MeasureTheory.Content.toFun_eq_toNNReal_apply (since := "2025-02-11")]

theorem MeasureTheory.Content.apply_eq_coe_toFun {G : Type w} [TopologicalSpace G] (μ : Content G) (K : TopologicalSpace.Compacts G) :

μ K = ↑(μ.toFun K)

theorem MeasureTheory.Content.mono {G : Type w} [TopologicalSpace G] (μ : Content G) (K₁ K₂ : TopologicalSpace.Compacts G) (h : ↑K₁ ⊆ ↑K₂) :

μ K₁ ≤ μ K₂

theorem MeasureTheory.Content.sup_disjoint {G : Type w} [TopologicalSpace G] (μ : Content G) (K₁ K₂ : TopologicalSpace.Compacts G) (h : Disjoint ↑K₁ ↑K₂) (h₁ : IsClosed ↑K₁) (h₂ : IsClosed ↑K₂) :

μ (K₁ ⊔ K₂) = μ K₁ + μ K₂

theorem MeasureTheory.Content.sup_le {G : Type w} [TopologicalSpace G] (μ : Content G) (K₁ K₂ : TopologicalSpace.Compacts G) :

μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂

theorem MeasureTheory.Content.lt_top {G : Type w} [TopologicalSpace G] (μ : Content G) (K : TopologicalSpace.Compacts G) :

μ K < ⊤

theorem MeasureTheory.Content.empty {G : Type w} [TopologicalSpace G] (μ : Content G) :

μ ⊥ = 0

def MeasureTheory.Content.innerContent {G : Type w} [TopologicalSpace G] (μ : Content G) (U : TopologicalSpace.Opens G) :

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.

Equations

μ.innerContent U = ⨆ (K : TopologicalSpace.Compacts G), ⨆ (_ : ↑K ⊆ ↑U), μ K

Instances For

theorem MeasureTheory.Content.le_innerContent {G : Type w} [TopologicalSpace G] (μ : Content G) (K : TopologicalSpace.Compacts G) (U : TopologicalSpace.Opens G) (h2 : ↑K ⊆ ↑U) :

μ K ≤ μ.innerContent U

theorem MeasureTheory.Content.innerContent_le {G : Type w} [TopologicalSpace G] (μ : Content G) (U : TopologicalSpace.Opens G) (K : TopologicalSpace.Compacts G) (h2 : ↑U ⊆ ↑K) :

μ.innerContent U ≤ μ K

theorem MeasureTheory.Content.innerContent_of_isCompact {G : Type w} [TopologicalSpace G] (μ : Content G) {K : Set G} (h1K : IsCompact K) (h2K : IsOpen K) :

μ.innerContent { carrier := K, is_open' := h2K } = μ { carrier := K, isCompact' := h1K }

theorem MeasureTheory.Content.innerContent_bot {G : Type w} [TopologicalSpace G] (μ : Content G) :

μ.innerContent ⊥ = 0

theorem MeasureTheory.Content.innerContent_mono {G : Type w} [TopologicalSpace G] (μ : Content G) ⦃U V : Set G⦄ (hU : IsOpen U) (hV : IsOpen V) (h2 : U ⊆ V) :

μ.innerContent { carrier := U, is_open' := hU } ≤ μ.innerContent { carrier := V, is_open' := hV }

This is "unbundled", because that is required for the API of inducedOuterMeasure.

theorem MeasureTheory.Content.innerContent_exists_compact {G : Type w} [TopologicalSpace G] (μ : Content G) {U : TopologicalSpace.Opens G} (hU : μ.innerContent U ≠ ⊤) {ε : NNReal} (hε : ε ≠ 0) :

∃ (K : TopologicalSpace.Compacts G), ↑K ⊆ ↑U ∧ μ.innerContent U ≤ μ K + ↑ε

theorem MeasureTheory.Content.innerContent_iSup_nat {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] (U : ℕ → TopologicalSpace.Opens G) :

μ.innerContent (⨆ (i : ℕ), U i) ≤ ∑' (i : ℕ), μ.innerContent (U i)

The inner content of a supremum of opens is at most the sum of the individual inner contents.

theorem MeasureTheory.Content.innerContent_iUnion_nat {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] ⦃U : ℕ → Set G⦄ (hU : ∀ (i : ℕ), IsOpen (U i)) :

μ.innerContent { carrier := ⋃ (i : ℕ), U i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := U i, is_open' := ⋯ }

The inner content of a union of sets is at most the sum of the individual inner contents. This is the "unbundled" version of innerContent_iSup_nat. It is required for the API of inducedOuterMeasure.

theorem MeasureTheory.Content.innerContent_comap {G : Type w} [TopologicalSpace G] (μ : Content G) (f : G ≃ₜ G) (h : ∀ ⦃K : TopologicalSpace.Compacts G⦄, μ (TopologicalSpace.Compacts.map ⇑f ⋯ K) = μ K) (U : TopologicalSpace.Opens G) :

μ.innerContent ((TopologicalSpace.Opens.comap ↑f) U) = μ.innerContent U

theorem MeasureTheory.Content.is_mul_left_invariant_innerContent {G : Type w} [TopologicalSpace G] (μ : Content G) [Group G] [IsTopologicalGroup G] (h : ∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun (b : G) => g * b) ⋯ K) = μ K) (g : G) (U : TopologicalSpace.Opens G) :

μ.innerContent ((TopologicalSpace.Opens.comap ↑(Homeomorph.mulLeft g)) U) = μ.innerContent U

theorem MeasureTheory.Content.is_add_left_invariant_innerContent {G : Type w} [TopologicalSpace G] (μ : Content G) [AddGroup G] [IsTopologicalAddGroup G] (h : ∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun (b : G) => g + b) ⋯ K) = μ K) (g : G) (U : TopologicalSpace.Opens G) :

μ.innerContent ((TopologicalSpace.Opens.comap ↑(Homeomorph.addLeft g)) U) = μ.innerContent U

theorem MeasureTheory.Content.innerContent_pos_of_is_mul_left_invariant {G : Type w} [TopologicalSpace G] (μ : Content G) [Group G] [IsTopologicalGroup G] (h3 : ∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun (b : G) => g * b) ⋯ K) = μ K) (K : TopologicalSpace.Compacts G) (hK : μ K ≠ 0) (U : TopologicalSpace.Opens G) (hU : (↑U).Nonempty) :

0 < μ.innerContent U

theorem MeasureTheory.Content.innerContent_pos_of_is_add_left_invariant {G : Type w} [TopologicalSpace G] (μ : Content G) [AddGroup G] [IsTopologicalAddGroup G] (h3 : ∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun (b : G) => g + b) ⋯ K) = μ K) (K : TopologicalSpace.Compacts G) (hK : μ K ≠ 0) (U : TopologicalSpace.Opens G) (hU : (↑U).Nonempty) :

0 < μ.innerContent U

theorem MeasureTheory.Content.innerContent_mono' {G : Type w} [TopologicalSpace G] (μ : Content G) ⦃U V : Set G⦄ (hU : IsOpen U) (hV : IsOpen V) (h2 : U ⊆ V) :

μ.innerContent { carrier := U, is_open' := hU } ≤ μ.innerContent { carrier := V, is_open' := hV }

def MeasureTheory.Content.outerMeasure {G : Type w} [TopologicalSpace G] (μ : Content G) :

Extending a content on compact sets to an outer measure on all sets.

Equations

μ.outerMeasure = MeasureTheory.inducedOuterMeasure (fun (U : Set G) (hU : IsOpen U) => μ.innerContent { carrier := U, is_open' := hU }) ⋯ ⋯

Instances For

theorem MeasureTheory.Content.outerMeasure_opens {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] (U : TopologicalSpace.Opens G) :

μ.outerMeasure ↑U = μ.innerContent U

theorem MeasureTheory.Content.outerMeasure_of_isOpen {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] (U : Set G) (hU : IsOpen U) :

μ.outerMeasure U = μ.innerContent { carrier := U, is_open' := hU }

theorem MeasureTheory.Content.outerMeasure_le {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] (U : TopologicalSpace.Opens G) (K : TopologicalSpace.Compacts G) (hUK : ↑U ⊆ ↑K) :

μ.outerMeasure ↑U ≤ μ K

theorem MeasureTheory.Content.le_outerMeasure_compacts {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] (K : TopologicalSpace.Compacts G) :

μ K ≤ μ.outerMeasure ↑K

theorem MeasureTheory.Content.outerMeasure_eq_iInf {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] (A : Set G) :

μ.outerMeasure A = ⨅ (U : Set G), ⨅ (hU : IsOpen U), ⨅ (_ : A ⊆ U), μ.innerContent { carrier := U, is_open' := hU }

theorem MeasureTheory.Content.outerMeasure_interior_compacts {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] (K : TopologicalSpace.Compacts G) :

μ.outerMeasure (interior ↑K) ≤ μ K

theorem MeasureTheory.Content.outerMeasure_exists_compact {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] {U : TopologicalSpace.Opens G} (hU : μ.outerMeasure ↑U ≠ ⊤) {ε : NNReal} (hε : ε ≠ 0) :

∃ (K : TopologicalSpace.Compacts G), ↑K ⊆ ↑U ∧ μ.outerMeasure ↑U ≤ μ.outerMeasure ↑K + ↑ε

theorem MeasureTheory.Content.outerMeasure_exists_open {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] {A : Set G} (hA : μ.outerMeasure A ≠ ⊤) {ε : NNReal} (hε : ε ≠ 0) :

∃ (U : TopologicalSpace.Opens G), A ⊆ ↑U ∧ μ.outerMeasure ↑U ≤ μ.outerMeasure A + ↑ε

theorem MeasureTheory.Content.outerMeasure_preimage {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] (f : G ≃ₜ G) (h : ∀ ⦃K : TopologicalSpace.Compacts G⦄, μ (TopologicalSpace.Compacts.map ⇑f ⋯ K) = μ K) (A : Set G) :

μ.outerMeasure (⇑f ⁻¹' A) = μ.outerMeasure A

theorem MeasureTheory.Content.outerMeasure_lt_top_of_isCompact {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] [WeaklyLocallyCompactSpace G] {K : Set G} (hK : IsCompact K) :

μ.outerMeasure K < ⊤

theorem MeasureTheory.Content.is_mul_left_invariant_outerMeasure {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] [Group G] [IsTopologicalGroup G] (h : ∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun (b : G) => g * b) ⋯ K) = μ K) (g : G) (A : Set G) :

μ.outerMeasure ((fun (x : G) => g * x) ⁻¹' A) = μ.outerMeasure A

theorem MeasureTheory.Content.is_add_left_invariant_outerMeasure {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] [AddGroup G] [IsTopologicalAddGroup G] (h : ∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun (b : G) => g + b) ⋯ K) = μ K) (g : G) (A : Set G) :

μ.outerMeasure ((fun (x : G) => g + x) ⁻¹' A) = μ.outerMeasure A

theorem MeasureTheory.Content.outerMeasure_caratheodory {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] (A : Set G) :

MeasurableSet A ↔ ∀ (U : TopologicalSpace.Opens G), μ.outerMeasure (↑U ∩ A) + μ.outerMeasure (↑U \ A) ≤ μ.outerMeasure ↑U

theorem MeasureTheory.Content.outerMeasure_pos_of_is_mul_left_invariant {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] [Group G] [IsTopologicalGroup G] (h3 : ∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun (b : G) => g * b) ⋯ K) = μ K) (K : TopologicalSpace.Compacts G) (hK : μ K ≠ 0) {U : Set G} (h1U : IsOpen U) (h2U : U.Nonempty) :

0 < μ.outerMeasure U

theorem MeasureTheory.Content.outerMeasure_pos_of_is_add_left_invariant {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] [AddGroup G] [IsTopologicalAddGroup G] (h3 : ∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun (b : G) => g + b) ⋯ K) = μ K) (K : TopologicalSpace.Compacts G) (hK : μ K ≠ 0) {U : Set G} (h1U : IsOpen U) (h2U : U.Nonempty) :

0 < μ.outerMeasure U

theorem MeasureTheory.Content.borel_le_caratheodory {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] [S : MeasurableSpace G] [BorelSpace G] :

S ≤ μ.outerMeasure.caratheodory

For the outer measure coming from a content, all Borel sets are measurable.

def MeasureTheory.Content.measure {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] [S : MeasurableSpace G] [BorelSpace G] :

The measure induced by the outer measure coming from a content, on the Borel sigma-algebra.

Equations

μ.measure = μ.outerMeasure.toMeasure ⋯

Instances For

theorem MeasureTheory.Content.measure_apply {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] [S : MeasurableSpace G] [BorelSpace G] {s : Set G} (hs : MeasurableSet s) :

μ.measure s = μ.outerMeasure s

instance MeasureTheory.Content.outerRegular {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] [S : MeasurableSpace G] [BorelSpace G] :

μ.measure.OuterRegular

instance MeasureTheory.Content.regular {G : Type w} [TopologicalSpace G] (μ : Content G) [R1Space G] [S : MeasurableSpace G] [BorelSpace G] [WeaklyLocallyCompactSpace G] :

μ.measure.Regular

In a locally compact space, any measure constructed from a content is regular.

def MeasureTheory.Content.ContentRegular {G : Type w} [TopologicalSpace G] (μ : Content G) :

A content μ is called regular if for every compact set K, μ(K) = inf {μ(K') : K ⊂ int K' ⊂ K'}. See Paul Halmos (1950), Measure Theory, §54.

Equations

μ.ContentRegular = ∀ ⦃K : TopologicalSpace.Compacts G⦄, μ K = ⨅ (K' : TopologicalSpace.Compacts G), ⨅ (_ : ↑K ⊆ interior ↑K'), μ K'

Instances For

theorem MeasureTheory.Content.contentRegular_exists_compact {G : Type w} [TopologicalSpace G] (μ : Content G) (H : μ.ContentRegular) (K : TopologicalSpace.Compacts G) {ε : NNReal} (hε : ε ≠ 0) :

∃ (K' : TopologicalSpace.Compacts G), K.carrier ⊆ interior K'.carrier ∧ μ K' ≤ μ K + ↑ε

theorem MeasureTheory.Content.measure_eq_content_of_regular {G : Type w} [TopologicalSpace G] (μ : Content G) [MeasurableSpace G] [R1Space G] [BorelSpace G] (H : μ.ContentRegular) (K : TopologicalSpace.Compacts G) :

μ.measure ↑K = μ K

If μ is a regular content, then the measure induced by μ will agree with μ on compact sets.