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);
MeasureTheory.toMeasurable μ 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
MeasurableSpace instance on
MeasureTheory.NullMeasurableSpace α μ. We also say that
f : α → β is
MeasureTheory.NullMeasurable 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
MeasureTheory.NullMeasurableSpace α μ → β.
Complete measures #
We say that a measure
μ is complete w.r.t. the
MeasurableSpace α σ-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.
Implementation notes #
@MeasurableSet (NullMeasurableSpace α μ) _ so
that theorems about
MeasurableSet.union can be applied to
NullMeasurableSets. However, these lemmas output terms of the same form
@MeasurableSet (NullMeasurableSpace α μ) _ _. While this is definitionally equal to the
NullMeasurableSet s μ, it looks different and may be misleading. So we copy all
standard lemmas about measurable sets to the
MeasureTheory.NullMeasurableSet namespace and fix
the output type.
measurable, measure, null measurable, completion
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.
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.