Null measurable sets and complete measures #
Main definitions #
Null measurable sets and functions #
- there exists a measurable set
s =ᵐ[μ] t(this is used as a definition);
measure_theory.to_measurable μ s =ᵐ[μ] s;
- there exists a measurable subset
t ⊆ ssuch that
t =ᵐ[μ] s(in this case the latter equality means that
μ (s \ t) = 0);
scan be represented as a union of a measurable set and a set of measure zero;
scan be represented as a difference of a measurable set and a set of measure zero.
Null measurable sets form a σ-algebra that is registered as a
measurable_space instance on
measure_theory.null_measurable_space α μ. We also say that
f : α → β is
measure_theory.null_measurable if the preimage of a measurable set is a null measurable set.
In other words,
f : α → β is null measurable if it is measurable as a function
measure_theory.null_measurable_space α μ → β.
Complete measures #
We say that a measure
μ is complete w.r.t. the
measurable_space α σ-algebra (or the σ-algebra is
complete w.r.t measure
μ) if every set of measure zero is measurable. In this case all null
measurable sets and functions are measurable.
For each measure
μ, we define
measure_theory.measure.completion μ to be the same measure
interpreted as a measure on
measure_theory.null_measurable_space α μ and prove that this is a
Implementation notes #
@measurable_set (null_measurable_space α μ) _ so
that theorems about
measurable_set.union can be applied to
null_measurable_sets. However, these lemmas output terms of the same form
@measurable_set (null_measurable_space α μ) _ _. While this is definitionally equal to the
null_measurable_set s μ, it looks different and may be misleading. So we copy all
standard lemmas about measurable sets to the
measure_theory.null_measurable_set namespace and fix
the output type.
measurable, measure, null measurable, completion
A type tag for
measurable_set given by
A set is called
null_measurable_set if it can be approximated by a measurable set up to
a set of null measure.
sᵢ is a countable family of (null) measurable pairwise
μ-a.e. disjoint sets, then there
exists a subordinate family
tᵢ ⊆ sᵢ of measurable pairwise disjoint sets such that
tᵢ =ᵐ[μ] sᵢ.
A null measurable set
t is Carathéodory measurable: for any
s, we have
μ (s ∩ t) + μ (s \ t) = μ s.
f : α → β is null measurable if the preimage of a measurable set is a null
A measure is complete if every null set is also measurable.
A null set is a subset of a measurable set with measure
Since every measure is defined as a special case of an outer measure, we can more simply state
that a set
s is null if
μ s = 0.
Instances of this typeclass
Given a measure we can complete it to a (complete) measure on all null measurable sets.