Contents
In this file we work with contents. A content λ is a function from a certain class of subsets
(such as the the compact subsets) to ennreal (or nnreal) that is
- additive: If
K₁andK₂are disjoint sets in the domain ofλ, thenλ(K₁ ∪ K₂) = λ(K₁) + λ(K₂); - subadditive: If
K₁andK₂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, we get a countably subadditive map that vanishes at∅. In Halmos (1950) this is called the inner contentλ*ofλ. - Given an inner content, we define an outer measure.
We don't explicitly define the type of contents. 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
measure_theory.inner_content: define an inner content from an contentmeasure_theory.outer_measure.of_content: construct an outer measure from a content
References
- Paul Halmos (1950), Measure Theory, §53
- https://en.wikipedia.org/wiki/Content_(measure_theory)
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
- measure_theory.inner_content μ U = ⨆ (K : topological_space.compacts G) (h : K.val ⊆ ↑U), μ K
theorem
measure_theory.le_inner_content
{G : Type w}
[topological_space G]
{μ : topological_space.compacts G → ennreal}
(K : topological_space.compacts G)
(U : topological_space.opens G) :
K.val ⊆ ↑U → μ K ≤ measure_theory.inner_content μ U
theorem
measure_theory.inner_content_le
{G : Type w}
[topological_space G]
{μ : topological_space.compacts G → ennreal}
(h : ∀ (K₁ K₂ : topological_space.compacts G), K₁.val ⊆ K₂.val → μ K₁ ≤ μ K₂)
(U : topological_space.opens G)
(K : topological_space.compacts G) :
↑U ⊆ K.val → measure_theory.inner_content μ U ≤ μ K
theorem
measure_theory.inner_content_of_is_compact
{G : Type w}
[topological_space G]
{μ : topological_space.compacts G → ennreal}
(h : ∀ (K₁ K₂ : topological_space.compacts G), K₁.val ⊆ K₂.val → μ K₁ ≤ μ K₂)
{K : set G}
(h1K : is_compact K)
(h2K : is_open K) :
measure_theory.inner_content μ ⟨K, h2K⟩ = μ ⟨K, h1K⟩
theorem
measure_theory.inner_content_empty
{G : Type w}
[topological_space G]
{μ : topological_space.compacts G → ennreal} :
μ ⊥ = 0 → measure_theory.inner_content μ ∅ = 0
theorem
measure_theory.inner_content_mono
{G : Type w}
[topological_space G]
{μ : topological_space.compacts G → ennreal}
⦃U V : set G⦄
(hU : is_open U)
(hV : is_open V) :
U ⊆ V → measure_theory.inner_content μ ⟨U, hU⟩ ≤ measure_theory.inner_content μ ⟨V, hV⟩
This is "unbundled", because that it required for the API of induced_outer_measure.
theorem
measure_theory.inner_content_exists_compact
{G : Type w}
[topological_space G]
{μ : topological_space.compacts G → ennreal}
{U : topological_space.opens G}
(hU : measure_theory.inner_content μ U < ⊤)
{ε : nnreal} :
0 < ε → (∃ (K : topological_space.compacts G), K.val ⊆ ↑U ∧ measure_theory.inner_content μ U ≤ μ K + ↑ε)
theorem
measure_theory.inner_content_Sup_nat
{G : Type w}
[topological_space G]
[t2_space G]
{μ : topological_space.compacts G → ennreal}
(h1 : μ ⊥ = 0)
(h2 : ∀ (K₁ K₂ : topological_space.compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂)
(U : ℕ → topological_space.opens G) :
measure_theory.inner_content μ (⨆ (i : ℕ), U i) ≤ ∑' (i : ℕ), measure_theory.inner_content μ (U i)
The inner content of a surpremum of opens is at most the sum of the individual inner contents.
theorem
measure_theory.inner_content_Union_nat
{G : Type w}
[topological_space G]
[t2_space G]
{μ : topological_space.compacts G → ennreal}
(h1 : μ ⊥ = 0)
(h2 : ∀ (K₁ K₂ : topological_space.compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂)
⦃U : ℕ → set G⦄
(hU : ∀ (i : ℕ), is_open (U i)) :
measure_theory.inner_content μ ⟨⋃ (i : ℕ), U i, _⟩ ≤ ∑' (i : ℕ), measure_theory.inner_content μ ⟨U i, _⟩
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.inner_content_comap
{G : Type w}
[topological_space G]
{μ : topological_space.compacts G → ennreal}
(f : G ≃ₜ G)
(h : ∀ ⦃K : topological_space.compacts G⦄, μ (topological_space.compacts.map ⇑f _ K) = μ K)
(U : topological_space.opens G) :
theorem
measure_theory.is_left_invariant_inner_content
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
{μ : topological_space.compacts G → ennreal}
(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) :
theorem
measure_theory.inner_content_pos
{G : Type w}
[topological_space G]
[t2_space G]
[group G]
[topological_group G]
{μ : topological_space.compacts G → ennreal}
(h1 : μ ⊥ = 0)
(h2 : ∀ (K₁ K₂ : topological_space.compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂)
(h3 : ∀ (g : G) {K : topological_space.compacts G}, μ (topological_space.compacts.map (λ (b : G), g * b) _ K) = μ K)
(K : topological_space.compacts G)
(hK : 0 < μ K)
(U : topological_space.opens G) :
↑U.nonempty → 0 < measure_theory.inner_content μ U
theorem
measure_theory.inner_content_mono'
{G : Type w}
[topological_space G]
{μ : topological_space.compacts G → ennreal}
⦃U V : set G⦄
(hU : is_open U)
(hV : is_open V) :
U ⊆ V → measure_theory.inner_content μ ⟨U, hU⟩ ≤ measure_theory.inner_content μ ⟨V, hV⟩
def
measure_theory.outer_measure.of_content
{G : Type w}
[topological_space G]
[t2_space G]
(μ : topological_space.compacts G → ennreal) :
μ ⊥ = 0 → measure_theory.outer_measure G
Extending a content on compact sets to an outer measure on all sets.
Equations
- measure_theory.outer_measure.of_content μ h1 = measure_theory.induced_outer_measure (λ (U : set G) (hU : is_open U), measure_theory.inner_content μ ⟨U, hU⟩) is_open_empty _
theorem
measure_theory.outer_measure.of_content_opens
{G : Type w}
[topological_space G]
[t2_space G]
{μ : topological_space.compacts G → ennreal}
{h1 : μ ⊥ = 0}
(h2 : ∀ (K₁ K₂ : topological_space.compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂)
(U : topological_space.opens G) :
theorem
measure_theory.outer_measure.le_of_content_compacts
{G : Type w}
[topological_space G]
[t2_space G]
{μ : topological_space.compacts G → ennreal}
{h1 : μ ⊥ = 0}
(h2 : ∀ (K₁ K₂ : topological_space.compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂)
(K : topological_space.compacts G) :
μ K ≤ ⇑(measure_theory.outer_measure.of_content μ h1) K.val
theorem
measure_theory.outer_measure.of_content_eq_infi
{G : Type w}
[topological_space G]
[t2_space G]
{μ : topological_space.compacts G → ennreal}
{h1 : μ ⊥ = 0}
(h2 : ∀ (K₁ K₂ : topological_space.compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂)
(A : set G) :
⇑(measure_theory.outer_measure.of_content μ h1) A = ⨅ (U : set G) (hU : is_open U) (h : A ⊆ U), measure_theory.inner_content μ ⟨U, hU⟩
theorem
measure_theory.outer_measure.of_content_interior_compacts
{G : Type w}
[topological_space G]
[t2_space G]
{μ : topological_space.compacts G → ennreal}
{h1 : μ ⊥ = 0}
(h2 : ∀ (K₁ K₂ : topological_space.compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂)
(h3 : ∀ (K₁ K₂ : topological_space.compacts G), K₁.val ⊆ K₂.val → μ K₁ ≤ μ K₂)
(K : topological_space.compacts G) :
⇑(measure_theory.outer_measure.of_content μ h1) (interior K.val) ≤ μ K
theorem
measure_theory.outer_measure.of_content_exists_compact
{G : Type w}
[topological_space G]
[t2_space G]
{μ : topological_space.compacts G → ennreal}
{h1 : μ ⊥ = 0}
(h2 : ∀ (K₁ K₂ : topological_space.compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂)
{U : topological_space.opens G}
(hU : ⇑(measure_theory.outer_measure.of_content μ h1) ↑U < ⊤)
{ε : nnreal} :
0 < ε → (∃ (K : topological_space.compacts G), K.val ⊆ ↑U ∧ ⇑(measure_theory.outer_measure.of_content μ h1) ↑U ≤ ⇑(measure_theory.outer_measure.of_content μ h1) K.val + ↑ε)
theorem
measure_theory.outer_measure.of_content_exists_open
{G : Type w}
[topological_space G]
[t2_space G]
{μ : topological_space.compacts G → ennreal}
{h1 : μ ⊥ = 0}
(h2 : ∀ (K₁ K₂ : topological_space.compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂)
{A : set G}
(hA : ⇑(measure_theory.outer_measure.of_content μ h1) A < ⊤)
{ε : nnreal} :
0 < ε → (∃ (U : topological_space.opens G), A ⊆ ↑U ∧ ⇑(measure_theory.outer_measure.of_content μ h1) ↑U ≤ ⇑(measure_theory.outer_measure.of_content μ h1) A + ↑ε)
theorem
measure_theory.outer_measure.of_content_preimage
{G : Type w}
[topological_space G]
[t2_space G]
{μ : topological_space.compacts G → ennreal}
{h1 : μ ⊥ = 0}
(h2 : ∀ (K₁ K₂ : topological_space.compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂)
(f : G ≃ₜ G)
(h : ∀ ⦃K : topological_space.compacts G⦄, μ (topological_space.compacts.map ⇑f _ K) = μ K)
(A : set G) :
⇑(measure_theory.outer_measure.of_content μ h1) (⇑f ⁻¹' A) = ⇑(measure_theory.outer_measure.of_content μ h1) A
theorem
measure_theory.outer_measure.is_left_invariant_of_content
{G : Type w}
[topological_space G]
[t2_space G]
{μ : topological_space.compacts G → ennreal}
{h1 : μ ⊥ = 0}
(h2 : ∀ (K₁ K₂ : topological_space.compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂)
[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) :
⇑(measure_theory.outer_measure.of_content μ h1) ((λ (h : G), g * h) ⁻¹' A) = ⇑(measure_theory.outer_measure.of_content μ h1) A
theorem
measure_theory.outer_measure.of_content_caratheodory
{G : Type w}
[topological_space G]
[t2_space G]
{μ : topological_space.compacts G → ennreal}
{h1 : μ ⊥ = 0}
(h2 : ∀ (K₁ K₂ : topological_space.compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂)
(A : set G) :
(measure_theory.outer_measure.of_content μ h1).caratheodory.is_measurable A ↔ ∀ (U : topological_space.opens G), ⇑(measure_theory.outer_measure.of_content μ h1) (↑U ∩ A) + ⇑(measure_theory.outer_measure.of_content μ h1) (↑U \ A) ≤ ⇑(measure_theory.outer_measure.of_content μ h1) ↑U
theorem
measure_theory.outer_measure.of_content_pos_of_is_open
{G : Type w}
[topological_space G]
[t2_space G]
{μ : topological_space.compacts G → ennreal}
{h1 : μ ⊥ = 0}
(h2 : ∀ (K₁ K₂ : topological_space.compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂)
[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 : 0 < μ K)
{U : set G} :
is_open U → U.nonempty → 0 < ⇑(measure_theory.outer_measure.of_content μ h1) U