mathlib3 documentation

measure_theory.measure.content

Contents #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

References #

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

structure measure_theory.content (G : Type w) [topological_space G] :

to_fun : topological_space.compacts G → nnreal
mono' : ∀ (K₁ K₂ : topological_space.compacts G), ↑K₁ ⊆ ↑K₂ → self.to_fun K₁ ≤ self.to_fun K₂
sup_disjoint' : ∀ (K₁ K₂ : topological_space.compacts G), disjoint ↑K₁ ↑K₂ → self.to_fun (K₁ ⊔ K₂) = self.to_fun K₁ + self.to_fun K₂
sup_le' : ∀ (K₁ K₂ : topological_space.compacts G), self.to_fun (K₁ ⊔ K₂) ≤ self.to_fun K₁ + self.to_fun K₂

A content is an additive function on compact sets taking values in ℝ≥0. It is a device from which one can define a measure.

Instances for measure_theory.content

@[protected, instance]

def measure_theory.content.inhabited {G : Type w} [topological_space G] :

inhabited (measure_theory.content G)

Equations

measure_theory.content.inhabited = {default := {to_fun := λ (K : topological_space.compacts G), 0, mono' := _, sup_disjoint' := _, sup_le' := _}}

@[protected, instance]

def measure_theory.content.has_coe_to_fun {G : Type w} [topological_space G] :

has_coe_to_fun (measure_theory.content G) (λ (_x : measure_theory.content G), topological_space.compacts G → ennreal)

Although the to_fun 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 suprs and infs, which is more convenient in a complete lattice, and aim at constructing a measure.

Equations

measure_theory.content.has_coe_to_fun = {coe := λ (μ : measure_theory.content G) (s : topological_space.compacts G), ↑(μ.to_fun s)}

theorem measure_theory.content.apply_eq_coe_to_fun {G : Type w} [topological_space G] (μ : measure_theory.content G) (K : topological_space.compacts G) :

⇑μ K = ↑(μ.to_fun K)

theorem measure_theory.content.mono {G : Type w} [topological_space G] (μ : measure_theory.content G) (K₁ K₂ : topological_space.compacts G) (h : ↑K₁ ⊆ ↑K₂) :

⇑μ K₁ ≤ ⇑μ K₂

theorem measure_theory.content.sup_disjoint {G : Type w} [topological_space G] (μ : measure_theory.content G) (K₁ K₂ : topological_space.compacts G) (h : disjoint ↑K₁ ↑K₂) :

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

theorem measure_theory.content.sup_le {G : Type w} [topological_space G] (μ : measure_theory.content G) (K₁ K₂ : topological_space.compacts G) :

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

theorem measure_theory.content.lt_top {G : Type w} [topological_space G] (μ : measure_theory.content G) (K : topological_space.compacts G) :

theorem measure_theory.content.empty {G : Type w} [topological_space G] (μ : measure_theory.content G) :

noncomputable def measure_theory.content.inner_content {G : Type w} [topological_space G] (μ : measure_theory.content G) (U : topological_space.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

μ.inner_content U = ⨆ (K : topological_space.compacts G) (h : ↑K ⊆ ↑U), ⇑μ K

theorem measure_theory.content.le_inner_content {G : Type w} [topological_space G] (μ : measure_theory.content G) (K : topological_space.compacts G) (U : topological_space.opens G) (h2 : ↑K ⊆ ↑U) :

⇑μ K ≤ μ.inner_content U

theorem measure_theory.content.inner_content_le {G : Type w} [topological_space G] (μ : measure_theory.content G) (U : topological_space.opens G) (K : topological_space.compacts G) (h2 : ↑U ⊆ ↑K) :

μ.inner_content U ≤ ⇑μ K

theorem measure_theory.content.inner_content_of_is_compact {G : Type w} [topological_space G] (μ : measure_theory.content G) {K : set G} (h1K : is_compact K) (h2K : is_open K) :

μ.inner_content {carrier := K, is_open' := h2K} = ⇑μ {carrier := K, is_compact' := h1K}

theorem measure_theory.content.inner_content_bot {G : Type w} [topological_space G] (μ : measure_theory.content G) :

μ.inner_content ⊥ = 0

theorem measure_theory.content.inner_content_mono {G : Type w} [topological_space G] (μ : measure_theory.content G) ⦃U V : set G⦄ (hU : is_open U) (hV : is_open V) (h2 : U ⊆ V) :

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

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

theorem measure_theory.content.inner_content_exists_compact {G : Type w} [topological_space G] (μ : measure_theory.content G) {U : topological_space.opens G} (hU : μ.inner_content U ≠ ⊤) {ε : nnreal} (hε : ε ≠ 0) :

∃ (K : topological_space.compacts G), ↑K ⊆ ↑U ∧ μ.inner_content U ≤ ⇑μ K + ↑ε

theorem measure_theory.content.inner_content_Sup_nat {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] (U : ℕ → topological_space.opens G) :

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

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

theorem measure_theory.content.inner_content_Union_nat {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] ⦃U : ℕ → set G⦄ (hU : ∀ (i : ℕ), is_open (U i)) :

μ.inner_content {carrier := ⋃ (i : ℕ), U i, is_open' := _} ≤ ∑' (i : ℕ), μ.inner_content {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 inner_content_Sup_nat. It required for the API of induced_outer_measure.

theorem measure_theory.content.inner_content_comap {G : Type w} [topological_space G] (μ : measure_theory.content G) (f : G ≃ₜ G) (h : ∀ ⦃K : topological_space.compacts G⦄, ⇑μ (topological_space.compacts.map ⇑f _ K) = ⇑μ K) (U : topological_space.opens G) :

μ.inner_content (⇑(topological_space.opens.comap f.to_continuous_map) U) = μ.inner_content U

theorem measure_theory.content.is_mul_left_invariant_inner_content {G : Type w} [topological_space G] (μ : measure_theory.content G) [group G] [topological_group G] (h : ∀ (g : G) {K : topological_space.compacts G}, ⇑μ (topological_space.compacts.map (λ (b : G), g * b) _ K) = ⇑μ K) (g : G) (U : topological_space.opens G) :

μ.inner_content (⇑(topological_space.opens.comap (homeomorph.mul_left g).to_continuous_map) U) = μ.inner_content U

theorem measure_theory.content.is_add_left_invariant_inner_content {G : Type w} [topological_space G] (μ : measure_theory.content G) [add_group G] [topological_add_group G] (h : ∀ (g : G) {K : topological_space.compacts G}, ⇑μ (topological_space.compacts.map (λ (b : G), g + b) _ K) = ⇑μ K) (g : G) (U : topological_space.opens G) :

μ.inner_content (⇑(topological_space.opens.comap (homeomorph.add_left g).to_continuous_map) U) = μ.inner_content U

theorem measure_theory.content.inner_content_pos_of_is_mul_left_invariant {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] [group G] [topological_group G] (h3 : ∀ (g : G) {K : topological_space.compacts G}, ⇑μ (topological_space.compacts.map (λ (b : G), g * b) _ K) = ⇑μ K) (K : topological_space.compacts G) (hK : ⇑μ K ≠ 0) (U : topological_space.opens G) (hU : ↑U.nonempty) :

0 < μ.inner_content U

theorem measure_theory.content.inner_content_pos_of_is_add_left_invariant {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] [add_group G] [topological_add_group G] (h3 : ∀ (g : G) {K : topological_space.compacts G}, ⇑μ (topological_space.compacts.map (λ (b : G), g + b) _ K) = ⇑μ K) (K : topological_space.compacts G) (hK : ⇑μ K ≠ 0) (U : topological_space.opens G) (hU : ↑U.nonempty) :

0 < μ.inner_content U

theorem measure_theory.content.inner_content_mono' {G : Type w} [topological_space G] (μ : measure_theory.content G) ⦃U V : set G⦄ (hU : is_open U) (hV : is_open V) (h2 : U ⊆ V) :

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

@[protected]

noncomputable def measure_theory.content.outer_measure {G : Type w} [topological_space G] (μ : measure_theory.content G) :

measure_theory.outer_measure G

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

Equations

μ.outer_measure = measure_theory.induced_outer_measure (λ (U : set G) (hU : is_open U), μ.inner_content {carrier := U, is_open' := hU}) is_open_empty _

theorem measure_theory.content.outer_measure_opens {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] (U : topological_space.opens G) :

⇑(μ.outer_measure) ↑U = μ.inner_content U

theorem measure_theory.content.outer_measure_of_is_open {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] (U : set G) (hU : is_open U) :

⇑(μ.outer_measure) U = μ.inner_content {carrier := U, is_open' := hU}

theorem measure_theory.content.outer_measure_le {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] (U : topological_space.opens G) (K : topological_space.compacts G) (hUK : ↑U ⊆ ↑K) :

⇑(μ.outer_measure) ↑U ≤ ⇑μ K

theorem measure_theory.content.le_outer_measure_compacts {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] (K : topological_space.compacts G) :

⇑μ K ≤ ⇑(μ.outer_measure) ↑K

theorem measure_theory.content.outer_measure_eq_infi {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] (A : set G) :

⇑(μ.outer_measure) A = ⨅ (U : set G) (hU : is_open U) (h : A ⊆ U), μ.inner_content {carrier := U, is_open' := hU}

theorem measure_theory.content.outer_measure_interior_compacts {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] (K : topological_space.compacts G) :

⇑(μ.outer_measure) (interior ↑K) ≤ ⇑μ K

theorem measure_theory.content.outer_measure_exists_compact {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] {U : topological_space.opens G} (hU : ⇑(μ.outer_measure) ↑U ≠ ⊤) {ε : nnreal} (hε : ε ≠ 0) :

∃ (K : topological_space.compacts G), ↑K ⊆ ↑U ∧ ⇑(μ.outer_measure) ↑U ≤ ⇑(μ.outer_measure) ↑K + ↑ε

theorem measure_theory.content.outer_measure_exists_open {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] {A : set G} (hA : ⇑(μ.outer_measure) A ≠ ⊤) {ε : nnreal} (hε : ε ≠ 0) :

∃ (U : topological_space.opens G), A ⊆ ↑U ∧ ⇑(μ.outer_measure) ↑U ≤ ⇑(μ.outer_measure) A + ↑ε

theorem measure_theory.content.outer_measure_preimage {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] (f : G ≃ₜ G) (h : ∀ ⦃K : topological_space.compacts G⦄, ⇑μ (topological_space.compacts.map ⇑f _ K) = ⇑μ K) (A : set G) :

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

theorem measure_theory.content.outer_measure_lt_top_of_is_compact {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] [locally_compact_space G] {K : set G} (hK : is_compact K) :

⇑(μ.outer_measure) K < ⊤

theorem measure_theory.content.is_mul_left_invariant_outer_measure {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] [group G] [topological_group G] (h : ∀ (g : G) {K : topological_space.compacts G}, ⇑μ (topological_space.compacts.map (λ (b : G), g * b) _ K) = ⇑μ K) (g : G) (A : set G) :

⇑(μ.outer_measure) ((λ (h : G), g * h) ⁻¹' A) = ⇑(μ.outer_measure) A

theorem measure_theory.content.is_add_left_invariant_outer_measure {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] [add_group G] [topological_add_group G] (h : ∀ (g : G) {K : topological_space.compacts G}, ⇑μ (topological_space.compacts.map (λ (b : G), g + b) _ K) = ⇑μ K) (g : G) (A : set G) :

⇑(μ.outer_measure) ((λ (h : G), g + h) ⁻¹' A) = ⇑(μ.outer_measure) A

theorem measure_theory.content.outer_measure_caratheodory {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] (A : set G) :

measurable_set A ↔ ∀ (U : topological_space.opens G), ⇑(μ.outer_measure) (↑U ∩ A) + ⇑(μ.outer_measure) (↑U \ A) ≤ ⇑(μ.outer_measure) ↑U

theorem measure_theory.content.outer_measure_pos_of_is_add_left_invariant {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] [add_group G] [topological_add_group G] (h3 : ∀ (g : G) {K : topological_space.compacts G}, ⇑μ (topological_space.compacts.map (λ (b : G), g + b) _ K) = ⇑μ K) (K : topological_space.compacts G) (hK : ⇑μ K ≠ 0) {U : set G} (h1U : is_open U) (h2U : U.nonempty) :

0 < ⇑(μ.outer_measure) U

theorem measure_theory.content.outer_measure_pos_of_is_mul_left_invariant {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] [group G] [topological_group G] (h3 : ∀ (g : G) {K : topological_space.compacts G}, ⇑μ (topological_space.compacts.map (λ (b : G), g * b) _ K) = ⇑μ K) (K : topological_space.compacts G) (hK : ⇑μ K ≠ 0) {U : set G} (h1U : is_open U) (h2U : U.nonempty) :

0 < ⇑(μ.outer_measure) U

theorem measure_theory.content.borel_le_caratheodory {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] [S : measurable_space G] [borel_space G] :

S ≤ μ.outer_measure.caratheodory

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

@[protected]

noncomputable def measure_theory.content.measure {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] [S : measurable_space G] [borel_space G] :

measure_theory.measure G

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

Equations

μ.measure = μ.outer_measure.to_measure _

Instances for measure_theory.content.measure

measure_theory.content.regular

theorem measure_theory.content.measure_apply {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] [S : measurable_space G] [borel_space G] {s : set G} (hs : measurable_set s) :

⇑(μ.measure) s = ⇑(μ.outer_measure) s

@[protected, instance]

def measure_theory.content.regular {G : Type w} [topological_space G] (μ : measure_theory.content G) [t2_space G] [S : measurable_space G] [borel_space G] [locally_compact_space G] :

μ.measure.regular

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

def measure_theory.content.content_regular {G : Type w} [topological_space G] (μ : measure_theory.content G) :

Prop

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

μ.content_regular = ∀ ⦃K : topological_space.compacts G⦄, ⇑μ K = ⨅ (K' : topological_space.compacts G) (hK : ↑K ⊆ interior ↑K'), ⇑μ K'

theorem measure_theory.content.content_regular_exists_compact {G : Type w} [topological_space G] (μ : measure_theory.content G) (H : μ.content_regular) (K : topological_space.compacts G) {ε : nnreal} (hε : ε ≠ 0) :

∃ (K' : topological_space.compacts G), K.carrier ⊆ interior K'.carrier ∧ ⇑μ K' ≤ ⇑μ K + ↑ε

theorem measure_theory.content.measure_eq_content_of_regular {G : Type w} [topological_space G] (μ : measure_theory.content G) [measurable_space G] [t2_space G] [borel_space G] (H : μ.content_regular) (K : topological_space.compacts G) :

⇑(μ.measure) ↑K = ⇑μ K

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