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:
μ ∅ = 0
;μ
is monotone;μ
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
outer_measure.bounded_by
is the greatest outer measure that is at most the given function. If you know that the given functions sends∅
to0
, thenouter_measure.of_function
is a special case.caratheodory
is the Carathéodory-measurable space of an outer measure.Inf_eq_of_function_Inf_gen
is a characterization of the infimum of outer measures.induced_outer_measure
is the measure induced by a function on a subset ofset α
References
- https://en.wikipedia.org/wiki/Outer_measure
- https://en.wikipedia.org/wiki/Carath%C3%A9odory%27s_criterion
Tags
outer measure, Carathéodory-measurable, Carathéodory's criterion
- measure_of : set α → ennreal
- empty : c.measure_of ∅ = 0
- mono : ∀ {s₁ s₂ : set α}, s₁ ⊆ s₂ → c.measure_of s₁ ≤ c.measure_of s₂
- Union_nat : ∀ (s : ℕ → set α), c.measure_of (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), c.measure_of (s i)
An outer measure is a countably subadditive monotone function that sends ∅
to 0
.
Equations
- measure_theory.outer_measure.has_coe_to_fun = {F := λ (m : measure_theory.outer_measure α), set α → ennreal, coe := λ (m : measure_theory.outer_measure α), m.measure_of}
Equations
- measure_theory.outer_measure.has_zero = {zero := {measure_of := λ (_x : set α), 0, empty := measure_theory.outer_measure.has_zero._proof_1, mono := _, Union_nat := _}}
Equations
- measure_theory.outer_measure.has_add = {add := λ (m₁ m₂ : measure_theory.outer_measure α), {measure_of := λ (s : set α), ⇑m₁ s + ⇑m₂ s, empty := _, mono := _, Union_nat := _}}
Equations
- measure_theory.outer_measure.add_comm_monoid = {add := has_add.add measure_theory.outer_measure.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, add_comm := _}
Equations
- measure_theory.outer_measure.has_scalar = {smul := λ (c : ennreal) (m : measure_theory.outer_measure α), {measure_of := λ (s : set α), c * ⇑m s, empty := _, mono := _, Union_nat := _}}
Equations
- measure_theory.outer_measure.semimodule = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul measure_theory.outer_measure.has_scalar}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
Equations
Equations
- measure_theory.outer_measure.outer_measure.order_bot = {bot := 0, le := λ (m₁ m₂ : measure_theory.outer_measure α), ∀ (s : set α), ⇑m₁ s ≤ ⇑m₂ s, lt := partial_order.lt._default (λ (m₁ m₂ : measure_theory.outer_measure α), ∀ (s : set α), ⇑m₁ s ≤ ⇑m₂ s), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}
Equations
- measure_theory.outer_measure.has_Sup = {Sup := λ (ms : set (measure_theory.outer_measure α)), {measure_of := λ (s : set α), ⨆ (m : measure_theory.outer_measure α) (H : m ∈ ms), ⇑m s, empty := _, mono := _, Union_nat := _}}
Equations
- measure_theory.outer_measure.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Sup (measure_theory.outer_measure α) measure_theory.outer_measure.complete_lattice._proof_1), le := order_bot.le measure_theory.outer_measure.outer_measure.order_bot, lt := order_bot.lt measure_theory.outer_measure.outer_measure.order_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf (complete_lattice_of_Sup (measure_theory.outer_measure α) measure_theory.outer_measure.complete_lattice._proof_1), inf_le_left := _, inf_le_right := _, le_inf := _, top := complete_lattice.top (complete_lattice_of_Sup (measure_theory.outer_measure α) measure_theory.outer_measure.complete_lattice._proof_1), le_top := _, bot := order_bot.bot measure_theory.outer_measure.outer_measure.order_bot, bot_le := _, Sup := complete_lattice.Sup (complete_lattice_of_Sup (measure_theory.outer_measure α) measure_theory.outer_measure.complete_lattice._proof_1), Inf := complete_lattice.Inf (complete_lattice_of_Sup (measure_theory.outer_measure α) measure_theory.outer_measure.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
The pushforward of m
along f
. The outer measure on s
is defined to be m (f ⁻¹' s)
.
Equations
- measure_theory.outer_measure.map f = {to_fun := λ (m : measure_theory.outer_measure α), {measure_of := λ (s : set β), ⇑m (f ⁻¹' s), empty := _, mono := _, Union_nat := _}, map_add' := _, map_smul' := _}
Equations
- measure_theory.outer_measure.functor = {map := λ (α β : Type u_1) (f : α → β), ⇑(measure_theory.outer_measure.map f), map_const := λ (α β : Type u_1), (λ (f : β → α), ⇑(measure_theory.outer_measure.map f)) ∘ function.const β}
The dirac outer measure.
Equations
- measure_theory.outer_measure.dirac a = {measure_of := λ (s : set α), s.indicator (λ (_x : α), 1) a, empty := _, mono := _, Union_nat := _}
The sum of an (arbitrary) collection of outer measures.
Equations
- measure_theory.outer_measure.sum f = {measure_of := λ (s : set α), ∑' (i : ι), ⇑(f i) s, empty := _, mono := _, Union_nat := _}
Pullback of an outer_measure
: comap f μ s = μ (f '' s)
.
Equations
- measure_theory.outer_measure.comap f = {to_fun := λ (m : measure_theory.outer_measure β), {measure_of := λ (s : set α), ⇑m (f '' s), empty := _, mono := _, Union_nat := _}, map_add' := _, map_smul' := _}
Restrict an outer_measure
to a set.
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
- measure_theory.outer_measure.bounded_by m = measure_theory.outer_measure.of_function (λ (s : set α), ⨆ (h : s.nonempty), m s) _
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)
.
The Carathéodory-measurable sets for an outer measure m
form a Dynkin system.
Equations
- m.caratheodory_dynkin = {has := m.is_caratheodory, has_empty := _, has_compl := _, has_Union_nat := _}
Given an outer measure μ
, the Carathéodory-measurable space is
defined such that s
is measurable if ∀t, μ t = μ (t ∩ s) + μ (t \ s)
.
Equations
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
- measure_theory.outer_measure.Inf_gen m s = ⨅ (μ : measure_theory.outer_measure α) (h : μ ∈ m), ⇑μ s
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.
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.
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
- measure_theory.extend m s = ⨅ (h : P s), m s h
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
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.
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
- m.trim = measure_theory.induced_outer_measure (λ (s : set α) (_x : is_measurable s), ⇑m s) is_measurable.empty _
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.