mathlib documentation

measure_theory.outer_measure

Outer Measures

An outer measure is a function μ : set α → ennreal, from the powerset of a type to the extended nonnegative real numbers that satisfies the following conditions:

  1. μ ∅ = 0;
  2. μ is monotone;
  3. μ is countably subadditive. This means that the outer measure of a countable union is at most the sum of the outer measure on the individual sets.

Note that we do not need α to be measurable to define an outer measure.

The outer measures on a type α form a complete lattice.

Given an arbitrary function m : set α → ennreal that sends ∅ to 0 we can define an outer measure on α that on s is defined to be the infimum of ∑ᵢ, m (sᵢ) for all collections of sets sᵢ that cover s. This is the unique maximal outer measure that is at most the given function. We also define this for functions m defined on a subset of set α, by treating the function as having value ∞ outside its domain.

Given an outer measure m, the Carathéodory-measurable sets are the sets s such that for all sets t we have m t = m (t ∩ s) + m (t \ s). This forms a measurable space.

Main definitions and statements

References

Tags

outer measure, Carathéodory-measurable, Carathéodory's criterion

source
structure measure_theory.outer_measure (α : Type u_1) :
Type u_1

An outer measure is a countably subadditive monotone function that sends ∅ to 0.

source
@[instance]
def measure_theory.outer_measure.has_coe_to_fun {α : Type u_1} :
has_coe_to_fun (measure_theory.outer_measure α)

Equations
source
@[simp]
theorem measure_theory.outer_measure.measure_of_eq_coe {α : Type u_1} (m : measure_theory.outer_measure α) :
m.measure_of = ⇑m

source
@[simp]
theorem measure_theory.outer_measure.empty' {α : Type u_1} (m : measure_theory.outer_measure α) :
⇑m ∅ = 0

source
theorem measure_theory.outer_measure.mono' {α : Type u_1} (m : measure_theory.outer_measure α) {s₁ s₂ : set α} (h : s₁ ⊆ s₂) :
⇑m s₁ ≤ ⇑m s₂

source
theorem measure_theory.outer_measure.Union {α : Type u_1} (m : measure_theory.outer_measure α) {β : Type u_2} [encodable β] (s : β → set α) :
⇑m (⋃ (i : β), s i) ≤ ∑' (i : β), ⇑m (s i)

source
theorem measure_theory.outer_measure.Union_null {α : Type u_1} (m : measure_theory.outer_measure α) {β : Type u_2} [encodable β] {s : β → set α} (h : ∀ (i : β), ⇑m (s i) = 0) :
⇑m (⋃ (i : β), s i) = 0

source
theorem measure_theory.outer_measure.Union_finset {α : Type u_1} {β : Type u_2} (m : measure_theory.outer_measure α) (s : β → set α) (t : finset β) :
⇑m (⋃ (i : β) (H : i ∈ t), s i) ≤ ∑ (i : β) in t, ⇑m (s i)

source
theorem measure_theory.outer_measure.union {α : Type u_1} (m : measure_theory.outer_measure α) (s₁ s₂ : set α) :
⇑m (s₁ ∪ s₂) ≤ ⇑m s₁ + ⇑m s₂

source
theorem measure_theory.outer_measure.le_inter_add_diff {α : Type u_1} {m : measure_theory.outer_measure α} {t : set α} (s : set α) :
⇑m t ≤ ⇑m (t ∩ s) + ⇑m (t \ s)

source
theorem measure_theory.outer_measure.diff_null {α : Type u_1} (m : measure_theory.outer_measure α) (s : set α) {t : set α} (ht : ⇑m t = 0) :
⇑m (s \ t) = ⇑m s

source
theorem measure_theory.outer_measure.union_null {α : Type u_1} (m : measure_theory.outer_measure α) {s₁ s₂ : set α} (h₁ : ⇑m s₁ = 0) (h₂ : ⇑m s₂ = 0) :
⇑m (s₁ ∪ s₂) = 0

source
theorem measure_theory.outer_measure.injective_coe_fn {α : Type u_1} :
function.injective (λ (μ : measure_theory.outer_measure α) (s : set α), ⇑μ s)

source
@[ext]
theorem measure_theory.outer_measure.ext {α : Type u_1} {μ₁ μ₂ : measure_theory.outer_measure α} (h : ∀ (s : set α), ⇑μ₁ s = ⇑μ₂ s) :
μ₁ = μ₂

source
@[instance]
def measure_theory.outer_measure.has_zero {α : Type u_1} :
has_zero (measure_theory.outer_measure α)

Equations
source
@[simp]
theorem measure_theory.outer_measure.coe_zero {α : Type u_1} :
⇑0 = 0

source
@[instance]
def measure_theory.outer_measure.inhabited {α : Type u_1} :
inhabited (measure_theory.outer_measure α)

Equations
source
@[instance]
def measure_theory.outer_measure.has_add {α : Type u_1} :
has_add (measure_theory.outer_measure α)

Equations
source
@[simp]
theorem measure_theory.outer_measure.coe_add {α : Type u_1} (m₁ m₂ : measure_theory.outer_measure α) :
⇑(m₁ + m₂) = ⇑m₁ + ⇑m₂

source
theorem measure_theory.outer_measure.add_apply {α : Type u_1} (m₁ m₂ : measure_theory.outer_measure α) (s : set α) :
⇑(m₁ + m₂) s = ⇑m₁ s + ⇑m₂ s

source
@[instance]
def measure_theory.outer_measure.add_comm_monoid {α : Type u_1} :
add_comm_monoid (measure_theory.outer_measure α)

Equations
source
@[instance]
def measure_theory.outer_measure.has_scalar {α : Type u_1} :
has_scalar ennreal (measure_theory.outer_measure α)

Equations
source
@[simp]
theorem measure_theory.outer_measure.coe_smul {α : Type u_1} (c : ennreal) (m : measure_theory.outer_measure α) :
⇑(c • m) = c • ⇑m

source
theorem measure_theory.outer_measure.smul_apply {α : Type u_1} (c : ennreal) (m : measure_theory.outer_measure α) (s : set α) :
⇑(c • m) s = c * ⇑m s

source
@[instance]
def measure_theory.outer_measure.semimodule {α : Type u_1} :
semimodule ennreal (measure_theory.outer_measure α)

Equations
source
@[instance]
def measure_theory.outer_measure.has_bot {α : Type u_1} :
has_bot (measure_theory.outer_measure α)

Equations
source
@[instance]
def measure_theory.outer_measure.outer_measure.order_bot {α : Type u_1} :
order_bot (measure_theory.outer_measure α)

Equations
source
@[instance]
def measure_theory.outer_measure.has_Sup {α : Type u_1} :
has_Sup (measure_theory.outer_measure α)

Equations
source
@[instance]
def measure_theory.outer_measure.complete_lattice {α : Type u_1} :
complete_lattice (measure_theory.outer_measure α)

Equations
source
@[simp]
theorem measure_theory.outer_measure.Sup_apply {α : Type u_1} (ms : set (measure_theory.outer_measure α)) (s : set α) :
⇑(Sup ms) s = ⨆ (m : measure_theory.outer_measure α) (H : m ∈ ms), ⇑m s

source
@[simp]
theorem measure_theory.outer_measure.supr_apply {α : Type u_1} {ι : Sort u_2} (f : ι → measure_theory.outer_measure α) (s : set α) :
(⇑⨆ (i : ι), f i) s = ⨆ (i : ι), ⇑(f i) s

source
theorem measure_theory.outer_measure.coe_supr {α : Type u_1} {ι : Sort u_2} (f : ι → measure_theory.outer_measure α) :
(⇑⨆ (i : ι), f i) = ⨆ (i : ι), ⇑(f i)

source
@[simp]
theorem measure_theory.outer_measure.sup_apply {α : Type u_1} (m₁ m₂ : measure_theory.outer_measure α) (s : set α) :
⇑(m₁ ⊔ m₂) s = ⇑m₁ s ⊔ ⇑m₂ s

source
def measure_theory.outer_measure.map {α : Type u_1} {β : Type u_2} (f : α → β) :
measure_theory.outer_measure α →ₗ[ennreal] measure_theory.outer_measure β

The pushforward of m along f. The outer measure on s is defined to be m (f ⁻¹' s).

Equations
source
@[simp]
theorem measure_theory.outer_measure.map_apply {α : Type u_1} {β : Type u_2} (f : α → β) (m : measure_theory.outer_measure α) (s : set β) :
⇑(⇑(measure_theory.outer_measure.map f) m) s = ⇑m (f ⁻¹' s)

source
@[simp]
theorem measure_theory.outer_measure.map_id {α : Type u_1} (m : measure_theory.outer_measure α) :
⇑(measure_theory.outer_measure.map id) m = m

source
@[simp]
theorem measure_theory.outer_measure.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) (m : measure_theory.outer_measure α) :
⇑(measure_theory.outer_measure.map g) (⇑(measure_theory.outer_measure.map f) m) = ⇑(measure_theory.outer_measure.map (g ∘ f)) m

source
@[instance]
def measure_theory.outer_measure.functor  :
functor measure_theory.outer_measure

Equations
source
@[instance]
def measure_theory.outer_measure.is_lawful_functor  :
is_lawful_functor measure_theory.outer_measure

source
def measure_theory.outer_measure.dirac {α : Type u_1} (a : α) :
measure_theory.outer_measure α

The dirac outer measure.

Equations
source
@[simp]
theorem measure_theory.outer_measure.dirac_apply {α : Type u_1} (a : α) (s : set α) :
⇑(measure_theory.outer_measure.dirac a) s = s.indicator (λ (_x : α), 1) a

source
def measure_theory.outer_measure.sum {α : Type u_1} {ι : Type u_2} (f : ι → measure_theory.outer_measure α) :
measure_theory.outer_measure α

The sum of an (arbitrary) collection of outer measures.

Equations
source
@[simp]
theorem measure_theory.outer_measure.sum_apply {α : Type u_1} {ι : Type u_2} (f : ι → measure_theory.outer_measure α) (s : set α) :
⇑(measure_theory.outer_measure.sum f) s = ∑' (i : ι), ⇑(f i) s

source
theorem measure_theory.outer_measure.smul_dirac_apply {α : Type u_1} (a : ennreal) (b : α) (s : set α) :
⇑(a • measure_theory.outer_measure.dirac b) s = s.indicator (λ (_x : α), a) b

source
def measure_theory.outer_measure.comap {α : Type u_1} {β : Type u_2} (f : α → β) :
measure_theory.outer_measure β →ₗ[ennreal] measure_theory.outer_measure α

Pullback of an outer_measure: comap f μ s = μ (f '' s).

Equations
source
@[simp]
theorem measure_theory.outer_measure.comap_apply {α : Type u_1} {β : Type u_2} (f : α → β) (m : measure_theory.outer_measure β) (s : set α) :
⇑(⇑(measure_theory.outer_measure.comap f) m) s = ⇑m (f '' s)

source
def measure_theory.outer_measure.restrict {α : Type u_1} (s : set α) :
measure_theory.outer_measure α →ₗ[ennreal] measure_theory.outer_measure α

Restrict an outer_measure to a set.

Equations
source
@[simp]
theorem measure_theory.outer_measure.restrict_apply {α : Type u_1} (s t : set α) (m : measure_theory.outer_measure α) :
⇑(⇑(measure_theory.outer_measure.restrict s) m) t = ⇑m (t ∩ s)

source
theorem measure_theory.outer_measure.top_apply {α : Type u_1} {s : set α} (h : s.nonempty) :
⇑⊤ s = ⊤

source
def measure_theory.outer_measure.of_function {α : Type u_1} (m : set α → ennreal) (m_empty : m ∅ = 0) :
measure_theory.outer_measure α

Given any function m assigning measures to sets satisying m ∅ = 0, there is a unique maximal outer measure μ satisfying μ s ≤ m s for all s : set α.

Equations
source
theorem measure_theory.outer_measure.of_function_apply {α : Type u_1} (m : set α → ennreal) (m_empty : m ∅ = 0) (s : set α) :
⇑(measure_theory.outer_measure.of_function m m_empty) s = ⨅ (t : ℕ → set α) (h : s ⊆ set.Union t), ∑' (n : ℕ), m (t n)

source
theorem measure_theory.outer_measure.of_function_le {α : Type u_1} {m : set α → ennreal} {m_empty : m ∅ = 0} (s : set α) :
⇑(measure_theory.outer_measure.of_function m m_empty) s ≤ m s

source
theorem measure_theory.outer_measure.of_function_eq {α : Type u_1} {m : set α → ennreal} {m_empty : m ∅ = 0} (s : set α) (m_mono : ∀ ⦃t : set α⦄, s ⊆ t → m s ≤ m t) (m_subadd : ∀ (s : ℕ → set α), m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), m (s i)) :
⇑(measure_theory.outer_measure.of_function m m_empty) s = m s

source
theorem measure_theory.outer_measure.le_of_function {α : Type u_1} {m : set α → ennreal} {m_empty : m ∅ = 0} {μ : measure_theory.outer_measure α} :
μ ≤ measure_theory.outer_measure.of_function m m_empty ↔ ∀ (s : set α), ⇑μ s ≤ m s

source
def measure_theory.outer_measure.bounded_by {α : Type u_1} (m : set α → ennreal) :
measure_theory.outer_measure α

Given any function m assigning measures to sets, there is a unique maximal outer measure μ satisfying μ s ≤ m s for all s : set α. This is the same as outer_measure.of_function, except that it doesn't require m ∅ = 0.

Equations
source
theorem measure_theory.outer_measure.bounded_by_le {α : Type u_1} {m : set α → ennreal} (s : set α) :
⇑(measure_theory.outer_measure.bounded_by m) s ≤ m s

source
theorem measure_theory.outer_measure.bounded_by_eq_of_function {α : Type u_1} {m : set α → ennreal} (m_empty : m ∅ = 0) (s : set α) :
⇑(measure_theory.outer_measure.bounded_by m) s = ⇑(measure_theory.outer_measure.of_function m m_empty) s

source
theorem measure_theory.outer_measure.bounded_by_apply {α : Type u_1} {m : set α → ennreal} (s : set α) :
⇑(measure_theory.outer_measure.bounded_by m) s = ⨅ (t : ℕ → set α) (h : s ⊆ set.Union t), ∑' (n : ℕ), ⨆ (h : (t n).nonempty), m (t n)

source
theorem measure_theory.outer_measure.bounded_by_eq {α : Type u_1} {m : set α → ennreal} (s : set α) (m_empty : m ∅ = 0) (m_mono : ∀ ⦃t : set α⦄, s ⊆ t → m s ≤ m t) (m_subadd : ∀ (s : ℕ → set α), m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), m (s i)) :
⇑(measure_theory.outer_measure.bounded_by m) s = m s

source
theorem measure_theory.outer_measure.le_bounded_by {α : Type u_1} {m : set α → ennreal} {μ : measure_theory.outer_measure α} :
μ ≤ measure_theory.outer_measure.bounded_by m ↔ ∀ (s : set α), ⇑μ s ≤ m s

source
theorem measure_theory.outer_measure.le_bounded_by' {α : Type u_1} {m : set α → ennreal} {μ : measure_theory.outer_measure α} :
μ ≤ measure_theory.outer_measure.bounded_by m ↔ ∀ (s : set α), s.nonempty → ⇑μ s ≤ m s

source
def measure_theory.outer_measure.is_caratheodory {α : Type u} (m : measure_theory.outer_measure α) (s : set α) :
Prop

A set s is Carathéodory-measurable for an outer measure m if for all sets t we have m t = m (t ∩ s) + m (t \ s).

Equations
source
theorem measure_theory.outer_measure.is_caratheodory_iff_le' {α : Type u} (m : measure_theory.outer_measure α) {s : set α} :
m.is_caratheodory s ↔ ∀ (t : set α), ⇑m (t ∩ s) + ⇑m (t \ s) ≤ ⇑m t

source
@[simp]
theorem measure_theory.outer_measure.is_caratheodory_empty {α : Type u} (m : measure_theory.outer_measure α) :
m.is_caratheodory ∅

source
theorem measure_theory.outer_measure.is_caratheodory_compl {α : Type u} (m : measure_theory.outer_measure α) {s₁ : set α} :
m.is_caratheodory s₁ → m.is_caratheodory s₁ᶜ

source
@[simp]
theorem measure_theory.outer_measure.is_caratheodory_compl_iff {α : Type u} (m : measure_theory.outer_measure α) {s : set α} :
m.is_caratheodory sᶜ ↔ m.is_caratheodory s

source
theorem measure_theory.outer_measure.is_caratheodory_union {α : Type u} (m : measure_theory.outer_measure α) {s₁ s₂ : set α} (h₁ : m.is_caratheodory s₁) (h₂ : m.is_caratheodory s₂) :
m.is_caratheodory (s₁ ∪ s₂)

source
theorem measure_theory.outer_measure.measure_inter_union {α : Type u} (m : measure_theory.outer_measure α) {s₁ s₂ : set α} (h : s₁ ∩ s₂ ⊆ ∅) (h₁ : m.is_caratheodory s₁) {t : set α} :
⇑m (t ∩ (s₁ ∪ s₂)) = ⇑m (t ∩ s₁) + ⇑m (t ∩ s₂)

source
theorem measure_theory.outer_measure.is_caratheodory_Union_lt {α : Type u} (m : measure_theory.outer_measure α) {s : ℕ → set α} {n : ℕ} :
(∀ (i : ℕ), i < n → m.is_caratheodory (s i)) → m.is_caratheodory (⋃ (i : ℕ) (H : i < n), s i)

source
theorem measure_theory.outer_measure.is_caratheodory_inter {α : Type u} (m : measure_theory.outer_measure α) {s₁ s₂ : set α} (h₁ : m.is_caratheodory s₁) (h₂ : m.is_caratheodory s₂) :
m.is_caratheodory (s₁ ∩ s₂)

source
theorem measure_theory.outer_measure.is_caratheodory_sum {α : Type u} (m : measure_theory.outer_measure α) {s : ℕ → set α} (h : ∀ (i : ℕ), m.is_caratheodory (s i)) (hd : pairwise (disjoint on s)) {t : set α} {n : ℕ} :
∑ (i : ℕ) in finset.range n, ⇑m (t ∩ s i) = ⇑m (t ∩ ⋃ (i : ℕ) (H : i < n), s i)

source
theorem measure_theory.outer_measure.is_caratheodory_Union_nat {α : Type u} (m : measure_theory.outer_measure α) {s : ℕ → set α} (h : ∀ (i : ℕ), m.is_caratheodory (s i)) (hd : pairwise (disjoint on s)) :
m.is_caratheodory (⋃ (i : ℕ), s i)

source
theorem measure_theory.outer_measure.f_Union {α : Type u} (m : measure_theory.outer_measure α) {s : ℕ → set α} (h : ∀ (i : ℕ), m.is_caratheodory (s i)) (hd : pairwise (disjoint on s)) :
⇑m (⋃ (i : ℕ), s i) = ∑' (i : ℕ), ⇑m (s i)

source
def measure_theory.outer_measure.caratheodory_dynkin {α : Type u} (m : measure_theory.outer_measure α) :
measurable_space.dynkin_system α

The Carathéodory-measurable sets for an outer measure m form a Dynkin system.

Equations
source
def measure_theory.outer_measure.caratheodory {α : Type u} (m : measure_theory.outer_measure α) :
measurable_space α

Given an outer measure μ, the Carathéodory-measurable space is defined such that s is measurable if ∀t, μ t = μ (t ∩ s) + μ (t \ s).

Equations
source
theorem measure_theory.outer_measure.is_caratheodory_iff {α : Type u} (m : measure_theory.outer_measure α) {s : set α} :
m.caratheodory.is_measurable' s ↔ ∀ (t : set α), ⇑m t = ⇑m (t ∩ s) + ⇑m (t \ s)

source
theorem measure_theory.outer_measure.is_caratheodory_iff_le {α : Type u} (m : measure_theory.outer_measure α) {s : set α} :
m.caratheodory.is_measurable' s ↔ ∀ (t : set α), ⇑m (t ∩ s) + ⇑m (t \ s) ≤ ⇑m t

source
theorem measure_theory.outer_measure.Union_eq_of_caratheodory {α : Type u} (m : measure_theory.outer_measure α) {s : ℕ → set α} (h : ∀ (i : ℕ), m.caratheodory.is_measurable' (s i)) (hd : pairwise (disjoint on s)) :
⇑m (⋃ (i : ℕ), s i) = ∑' (i : ℕ), ⇑m (s i)

source
theorem measure_theory.outer_measure.of_function_caratheodory {α : Type u_1} {m : set α → ennreal} {s : set α} {h₀ : m ∅ = 0} (hs : ∀ (t : set α), m (t ∩ s) + m (t \ s) ≤ m t) :
(measure_theory.outer_measure.of_function m h₀).caratheodory.is_measurable' s

source
theorem measure_theory.outer_measure.bounded_by_caratheodory {α : Type u_1} {m : set α → ennreal} {s : set α} (hs : ∀ (t : set α), m (t ∩ s) + m (t \ s) ≤ m t) :
(measure_theory.outer_measure.bounded_by m).caratheodory.is_measurable' s

source
@[simp]
theorem measure_theory.outer_measure.zero_caratheodory {α : Type u_1} :
0.caratheodory = ⊤

source
theorem measure_theory.outer_measure.top_caratheodory {α : Type u_1} :
⊤.caratheodory = ⊤

source
theorem measure_theory.outer_measure.le_add_caratheodory {α : Type u_1} (m₁ m₂ : measure_theory.outer_measure α) :
m₁.caratheodory ⊓ m₂.caratheodory ≤ (m₁ + m₂).caratheodory

source
theorem measure_theory.outer_measure.le_sum_caratheodory {α : Type u_1} {ι : Type u_2} (m : ι → measure_theory.outer_measure α) :
(⨅ (i : ι), (m i).caratheodory) ≤ (measure_theory.outer_measure.sum m).caratheodory

source
theorem measure_theory.outer_measure.le_smul_caratheodory {α : Type u_1} (a : ennreal) (m : measure_theory.outer_measure α) :
m.caratheodory ≤ (a • m).caratheodory

source
@[simp]
theorem measure_theory.outer_measure.dirac_caratheodory {α : Type u_1} (a : α) :
(measure_theory.outer_measure.dirac a).caratheodory = ⊤

source
def measure_theory.outer_measure.Inf_gen {α : Type u_1} (m : set (measure_theory.outer_measure α)) (s : set α) :
ennreal

Given a set of outer measures, we define a new function that on a set s is defined to be the infimum of μ(s) for the outer measures μ in the collection. We ensure that this function is defined to be 0 on ∅, even if the collection of outer measures is empty. The outer measure generated by this function is the infimum of the given outer measures.

Equations
source
theorem measure_theory.outer_measure.Inf_gen_def {α : Type u_1} (m : set (measure_theory.outer_measure α)) (t : set α) :
measure_theory.outer_measure.Inf_gen m t = ⨅ (μ : measure_theory.outer_measure α) (h : μ ∈ m), ⇑μ t

source
theorem measure_theory.outer_measure.Inf_eq_bounded_by_Inf_gen {α : Type u_1} (m : set (measure_theory.outer_measure α)) :
Inf m = measure_theory.outer_measure.bounded_by (measure_theory.outer_measure.Inf_gen m)

source
theorem measure_theory.outer_measure.supr_Inf_gen_nonempty {α : Type u_1} {m : set (measure_theory.outer_measure α)} (h : m.nonempty) (t : set α) :
(⨆ (h : t.nonempty), measure_theory.outer_measure.Inf_gen m t) = ⨅ (μ : measure_theory.outer_measure α) (h : μ ∈ m), ⇑μ t

source
theorem measure_theory.outer_measure.Inf_apply {α : Type u_1} {m : set (measure_theory.outer_measure α)} {s : set α} (h : m.nonempty) :
⇑(Inf m) s = ⨅ (t : ℕ → set α) (h2 : s ⊆ set.Union t), ∑' (n : ℕ), ⨅ (μ : measure_theory.outer_measure α) (h3 : μ ∈ m), ⇑μ (t n)

The value of the Infimum of a nonempty set of outer measures on a set is not simply the minimum value of a measure on that set: it is the infimum sum of measures of countable set of sets that covers that set, where a different measure can be used for each set in the cover.

source
theorem measure_theory.outer_measure.restrict_Inf_eq_Inf_restrict {α : Type u_1} (m : set (measure_theory.outer_measure α)) {s : set α} (hm : m.nonempty) :
⇑(measure_theory.outer_measure.restrict s) (Inf m) = Inf (⇑(measure_theory.outer_measure.restrict s) '' m)

This proves that Inf and restrict commute for outer measures, so long as the set of outer measures is nonempty.

Induced Outer Measure

We can extend a function defined on a subset of set α to an outer measure. The underlying function is called extend, and the measure it induces is called induced_outer_measure.

Some lemmas below are proven twice, once in the general case, and one where the function m is only defined on measurable sets (i.e. when P = is_measurable). In the latter cases, we can remove some hypotheses in the statement. The general version has the same name, but with a prime at the end.

source
def measure_theory.extend {α : Type u_1} {P : α → Prop} (m : Π (s : α), P s → ennreal) (s : α) :
ennreal

We can trivially extend a function defined on a subclass of objects (with codomain ennreal) to all objects by defining it to be ∞ on the objects not in the class.

Equations
source
theorem measure_theory.extend_eq {α : Type u_1} {P : α → Prop} (m : Π (s : α), P s → ennreal) {s : α} (h : P s) :
measure_theory.extend m s = m s h

source
theorem measure_theory.le_extend {α : Type u_1} {P : α → Prop} (m : Π (s : α), P s → ennreal) {s : α} (h : P s) :
m s h ≤ measure_theory.extend m s

source
theorem measure_theory.extend_empty {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P s → ennreal} (P0 : P ∅) (m0 : m ∅ P0 = 0) :
measure_theory.extend m ∅ = 0

source
theorem measure_theory.extend_Union_nat {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P s → ennreal} (PU : ∀ ⦃f : ℕ → set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) {f : ℕ → set α} (hm : ∀ (i : ℕ), P (f i)) (mU : m (⋃ (i : ℕ), f i) _ = ∑' (i : ℕ), m (f i) _) :
measure_theory.extend m (⋃ (i : ℕ), f i) = ∑' (i : ℕ), measure_theory.extend m (f i)

source
theorem measure_theory.extend_Union_le_tsum_nat' {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P s → ennreal} (PU : ∀ ⦃f : ℕ → set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) _ ≤ ∑' (i : ℕ), m (f i) _) (s : ℕ → set α) :
measure_theory.extend m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), measure_theory.extend m (s i)

source
theorem measure_theory.extend_mono' {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P s → ennreal} (m_mono : ∀ ⦃s₁ s₂ : set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) ⦃s₁ s₂ : set α⦄ (h₁ : P s₁) (hs : s₁ ⊆ s₂) :
measure_theory.extend m s₁ ≤ measure_theory.extend m s₂

source
theorem measure_theory.extend_Union {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P s → ennreal} (P0 : P ∅) (m0 : m ∅ P0 = 0) (PU : ∀ ⦃f : ℕ → set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (mU : ∀ ⦃f : ℕ → set α⦄ (hm : ∀ (i : ℕ), P (f i)), pairwise (disjoint on f) → m (⋃ (i : ℕ), f i) _ = ∑' (i : ℕ), m (f i) _) {β : Type u_2} [encodable β] {f : β → set α} (hd : pairwise (disjoint on f)) (hm : ∀ (i : β), P (f i)) :
measure_theory.extend m (⋃ (i : β), f i) = ∑' (i : β), measure_theory.extend m (f i)

source
theorem measure_theory.extend_union {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P s → ennreal} (P0 : P ∅) (m0 : m ∅ P0 = 0) (PU : ∀ ⦃f : ℕ → set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (mU : ∀ ⦃f : ℕ → set α⦄ (hm : ∀ (i : ℕ), P (f i)), pairwise (disjoint on f) → m (⋃ (i : ℕ), f i) _ = ∑' (i : ℕ), m (f i) _) {s₁ s₂ : set α} (hd : disjoint s₁ s₂) (h₁ : P s₁) (h₂ : P s₂) :
measure_theory.extend m (s₁ ∪ s₂) = measure_theory.extend m s₁ + measure_theory.extend m s₂

source
def measure_theory.induced_outer_measure {α : Type u_1} {P : set α → Prop} (m : Π (s : set α), P s → ennreal) (P0 : P ∅) (m0 : m ∅ P0 = 0) :
measure_theory.outer_measure α

Given an arbitrary function on a subset of sets, we can define the outer measure corresponding to it (this is the unique maximal outer measure that is at most m on the domain of m).

Equations
source
theorem measure_theory.induced_outer_measure_eq_extend' {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P s → ennreal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) _ ≤ ∑' (i : ℕ), m (f i) _) (m_mono : ∀ ⦃s₁ s₂ : set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) {s : set α} (hs : P s) :
⇑(measure_theory.induced_outer_measure m P0 m0) s = measure_theory.extend m s

source
theorem measure_theory.induced_outer_measure_eq' {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P s → ennreal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) _ ≤ ∑' (i : ℕ), m (f i) _) (m_mono : ∀ ⦃s₁ s₂ : set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) {s : set α} (hs : P s) :
⇑(measure_theory.induced_outer_measure m P0 m0) s = m s hs

source
theorem measure_theory.induced_outer_measure_eq_infi {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P s → ennreal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) _ ≤ ∑' (i : ℕ), m (f i) _) (m_mono : ∀ ⦃s₁ s₂ : set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) (s : set α) :
⇑(measure_theory.induced_outer_measure m P0 m0) s = ⨅ (t : set α) (ht : P t) (h : s ⊆ t), m t ht

source
theorem measure_theory.induced_outer_measure_preimage {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P s → ennreal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) _ ≤ ∑' (i : ℕ), m (f i) _) (m_mono : ∀ ⦃s₁ s₂ : set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) (f : α ≃ α) (Pm : ∀ (s : set α), P (⇑f ⁻¹' s) ↔ P s) (mm : ∀ (s : set α) (hs : P s), m (⇑f ⁻¹' s) _ = m s hs) {A : set α} :
⇑(measure_theory.induced_outer_measure m P0 m0) (⇑f ⁻¹' A) = ⇑(measure_theory.induced_outer_measure m P0 m0) A

source
theorem measure_theory.induced_outer_measure_exists_set {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P s → ennreal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) _ ≤ ∑' (i : ℕ), m (f i) _) (m_mono : ∀ ⦃s₁ s₂ : set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) {s : set α} (hs : ⇑(measure_theory.induced_outer_measure m P0 m0) s < ⊤) {ε : ℝ≥0} (hε : 0 < ε) :
∃ (t : set α) (ht : P t), s ⊆ t ∧ ⇑(measure_theory.induced_outer_measure m P0 m0) t ≤ ⇑(measure_theory.induced_outer_measure m P0 m0) s + ↑ε

source
theorem measure_theory.induced_outer_measure_caratheodory {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P s → ennreal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) _ ≤ ∑' (i : ℕ), m (f i) _) (m_mono : ∀ ⦃s₁ s₂ : set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) (s : set α) :
(measure_theory.induced_outer_measure m P0 m0).caratheodory.is_measurable' s ↔ ∀ (t : set α), P t → ⇑(measure_theory.induced_outer_measure m P0 m0) (t ∩ s) + ⇑(measure_theory.induced_outer_measure m P0 m0) (t \ s) ≤ ⇑(measure_theory.induced_outer_measure m P0 m0) t

To test whether s is Carathéodory-measurable we only need to check the sets t for which P t holds. See of_function_caratheodory for another way to show the Carathéodory-measurability of s.

If P is is_measurable for some measurable space, then we can remove some hypotheses of the above lemmas.

source
theorem measure_theory.extend_mono {α : Type u_1} [measurable_space α] {m : Π (s : set α), is_measurable s → ennreal} (m0 : m ∅ is_measurable.empty = 0) (mU : ∀ ⦃f : ℕ → set α⦄ (hm : ∀ (i : ℕ), is_measurable (f i)), pairwise (disjoint on f) → m (⋃ (i : ℕ), f i) _ = ∑' (i : ℕ), m (f i) _) {s₁ s₂ : set α} (h₁ : is_measurable s₁) (hs : s₁ ⊆ s₂) :
measure_theory.extend m s₁ ≤ measure_theory.extend m s₂

source
theorem measure_theory.extend_Union_le_tsum_nat {α : Type u_1} [measurable_space α] {m : Π (s : set α), is_measurable s → ennreal} (m0 : m ∅ is_measurable.empty = 0) (mU : ∀ ⦃f : ℕ → set α⦄ (hm : ∀ (i : ℕ), is_measurable (f i)), pairwise (disjoint on f) → m (⋃ (i : ℕ), f i) _ = ∑' (i : ℕ), m (f i) _) (s : ℕ → set α) :
measure_theory.extend m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), measure_theory.extend m (s i)

source
theorem measure_theory.induced_outer_measure_eq_extend {α : Type u_1} [measurable_space α] {m : Π (s : set α), is_measurable s → ennreal} (m0 : m ∅ is_measurable.empty = 0) (mU : ∀ ⦃f : ℕ → set α⦄ (hm : ∀ (i : ℕ), is_measurable (f i)), pairwise (disjoint on f) → m (⋃ (i : ℕ), f i) _ = ∑' (i : ℕ), m (f i) _) {s : set α} (hs : is_measurable s) :
⇑(measure_theory.induced_outer_measure m is_measurable.empty m0) s = measure_theory.extend m s

source
theorem measure_theory.induced_outer_measure_eq {α : Type u_1} [measurable_space α] {m : Π (s : set α), is_measurable s → ennreal} (m0 : m ∅ is_measurable.empty = 0) (mU : ∀ ⦃f : ℕ → set α⦄ (hm : ∀ (i : ℕ), is_measurable (f i)), pairwise (disjoint on f) → m (⋃ (i : ℕ), f i) _ = ∑' (i : ℕ), m (f i) _) {s : set α} (hs : is_measurable s) :
⇑(measure_theory.induced_outer_measure m is_measurable.empty m0) s = m s hs

source
def measure_theory.outer_measure.trim {α : Type u_1} [measurable_space α] (m : measure_theory.outer_measure α) :
measure_theory.outer_measure α

Given an outer measure m we can forget its value on non-measurable sets, and then consider m.trim, the unique maximal outer measure less than that function.

Equations
source
theorem measure_theory.outer_measure.le_trim {α : Type u_1} [measurable_space α] (m : measure_theory.outer_measure α) :
m ≤ m.trim

source
theorem measure_theory.outer_measure.trim_eq {α : Type u_1} [measurable_space α] (m : measure_theory.outer_measure α) {s : set α} (hs : is_measurable s) :
⇑(m.trim) s = ⇑m s

source
theorem measure_theory.outer_measure.trim_congr {α : Type u_1} [measurable_space α] {m₁ m₂ : measure_theory.outer_measure α} (H : ∀ {s : set α}, is_measurable s → ⇑m₁ s = ⇑m₂ s) :
m₁.trim = m₂.trim

source
theorem measure_theory.outer_measure.trim_le_trim {α : Type u_1} [measurable_space α] {m₁ m₂ : measure_theory.outer_measure α} (H : m₁ ≤ m₂) :
m₁.trim ≤ m₂.trim

source
theorem measure_theory.outer_measure.le_trim_iff {α : Type u_1} [measurable_space α] {m₁ m₂ : measure_theory.outer_measure α} :
m₁ ≤ m₂.trim ↔ ∀ (s : set α), is_measurable s → ⇑m₁ s ≤ ⇑m₂ s

source
theorem measure_theory.outer_measure.trim_eq_infi {α : Type u_1} [measurable_space α] (m : measure_theory.outer_measure α) (s : set α) :
⇑(m.trim) s = ⨅ (t : set α) (st : s ⊆ t) (ht : is_measurable t), ⇑m t

source
theorem measure_theory.outer_measure.trim_eq_infi' {α : Type u_1} [measurable_space α] (m : measure_theory.outer_measure α) (s : set α) :
⇑(m.trim) s = ⨅ (t : {t // s ⊆ t ∧ is_measurable t}), ⇑m ↑t

source
theorem measure_theory.outer_measure.trim_trim {α : Type u_1} [measurable_space α] (m : measure_theory.outer_measure α) :
m.trim.trim = m.trim

source
@[simp]
theorem measure_theory.outer_measure.trim_zero {α : Type u_1} [measurable_space α] :
0.trim = 0

source
theorem measure_theory.outer_measure.trim_add {α : Type u_1} [measurable_space α] (m₁ m₂ : measure_theory.outer_measure α) :
(m₁ + m₂).trim = m₁.trim + m₂.trim

source
theorem measure_theory.outer_measure.trim_sum_ge {α : Type u_1} [measurable_space α] {ι : Type u_2} (m : ι → measure_theory.outer_measure α) :
measure_theory.outer_measure.sum (λ (i : ι), (m i).trim) ≤ (measure_theory.outer_measure.sum m).trim

source
theorem measure_theory.outer_measure.exists_is_measurable_superset_eq_trim {α : Type u_1} [measurable_space α] (m : measure_theory.outer_measure α) (s : set α) :
∃ (t : set α), s ⊆ t ∧ is_measurable t ∧ ⇑m t = ⇑(m.trim) s

source
theorem measure_theory.outer_measure.exists_is_measurable_superset_of_trim_eq_zero {α : Type u_1} [measurable_space α] {m : measure_theory.outer_measure α} {s : set α} (h : ⇑(m.trim) s = 0) :
∃ (t : set α), s ⊆ t ∧ is_measurable t ∧ ⇑m t = 0

source
theorem measure_theory.outer_measure.trim_smul {α : Type u_1} [measurable_space α] (c : ennreal) (m : measure_theory.outer_measure α) :
(c • m).trim = c • m.trim

source
theorem measure_theory.outer_measure.restrict_trim {α : Type u_1} [measurable_space α] {μ : measure_theory.outer_measure α} {s : set α} (hs : is_measurable s) :
(⇑(measure_theory.outer_measure.restrict s) μ).trim = ⇑(measure_theory.outer_measure.restrict s) μ.trim

The trimmed property of a measure μ states that μ.to_outer_measure.trim = μ.to_outer_measure. This theorem shows that a restricted trimmed outer measure is a trimmed outer measure.