NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.
This files provides a formalization of the basics of measure theory. This
includes the formalization of mathematical structures and of measures, as
well as standard theorems such as the Measure Extension theorem that
builds a measure given a function defined over a semiring of sets, the
intermediate outer measure being
Reference:
semiRingOfSetsType d == the type of semirings of sets
The carrier is a set of sets A_i such that
"measurable A_i" holds.
"measurable A" is printed as "d.-measurable A"
where d is a "display parameter" whose purpose
is to distinguish different "measurable"
predicates in the same context.
The HB class is SemiRingOfSets.
ringOfSetsType d == the type of rings of sets
The HB class is RingOfSets.
algebraOfSetsType d == the type of algebras of sets
The HB class is AlgebraOfsets.
measurableType == the type of sigma-algebras
The HB class is Measurable.
discrete_measurable_unit == the measurableType corresponding to
[set: set unit]
discrete_measurable_bool == the measurableType corresponding to
[set: set bool]
discrete_measurable_nat == the measurableType corresponding to
[set: set nat]
setring G == the set of sets G contains the empty set, is
closed by union, and difference
<<r G >> := smallest setring G
<<r G >> is equipped with a structure of ring
of sets.
G.-ring.-measurable A == A belongs for the ring of sets <<r G >>
sigma_algebra D G == the set of sets G forms a sigma algebra on D
<<s D, G >> == sigma-algebra generated by G on D
:= smallest (sigma_algebra D) G
<<s G >> := <<s setT, G >>
<<s G >> is equipped with a structure of
sigma-algebra
G.-sigma.-measurable A == A is measurable for the sigma-algebra <<s G >>
salgebraType G == the measurableType corresponding to <<s G >>
This is an HB alias.
mu .-cara.-measurable == sigma-algebra of Caratheodory measurable sets
A few details about mixins/factories to highlight implementations
peculiarities:
{content set T -> \bar R} == type of contents
T is expected to be a semiring of sets and R a
numFieldType.
The HB class is Content.
{measure set T -> \bar R} == type of (non-negative) measures
T is expected to be a semiring of sets and R a
numFieldType.
The HB class is Measure.
Content_SubSigmaAdditive_isMeasure ==
mixin that extends a content to a measure with the
proof that it is semi_sigma_additive
Content_isMeasure == factory that extends a content to a measure with
the proof that it is sub_sigma_additive
isMeasure == factory corresponding to the "textbook
definition" of measures
sfinite_measure == predicate for s-finite measure functions
{sfinite_measure set T -> \bar R} == type of s-finite measures
The HB class is SFiniteMeasure.
sfinite_measure_seq mu == the sequence of finite measures of the
s-finite measure mu
Measure_isSFinite_subdef == mixin for s-finite measures
Measure_isSFinite == factory for s-finite measures
{sigma_finite_content set T -> \bar R} == contents that are also sigma
finite
The HB class is SigmaFiniteContent.
{sigma_finite_measure set T -> \bar R} == measures that are also sigma
finite
The HB class is SigmaFiniteMeasure.
sigma_finite A f == the measure function f is sigma-finite on the
A : set T with T a semiring of sets
fin_num_fun == predicate for finite function over measurable
sets
FinNumFun.type == type of functions over semiring of sets
returning a fin_num
The HB class is FinNumFun.
{finite_measure set T -> \bar R} == finite measures
The HB class is FiniteMeasure.
SigmaFinite_isFinite == mixin for finite measures
Measure_isFinite == factory for finite measures
subprobability T R == subprobability measure over the measurableType
T with values in \bar R with R : realType
The HB class is SubProbability.
probability T R == probability measure over the measurableType T
with values in \bar with R : realType
probability == type of probability measures
The HB class is Probability.
Measure_isProbability == factor for probability measures
mnormalize mu == normalization of a measure to a probability
{outer_measure set T -> \bar R} == type of an outer measure over sets
of elements of type T : Type where R is
expected to be a numFieldType
The HB class is OuterMeasure.
pushforward mf m == pushforward/image measure of m by f, where mf is a
proof that f is measurable
m has type set T -> \bar R.
\d_a == Dirac measure
msum mu n == the measure corresponding to the sum of the measures
mu_0, ..., mu_{n-1}
@mzero T R == the zero measure
measure_add m1 m2 == the measure corresponding to the sum of the
measures m1 and m2
mscale r m == the measure of corresponding to fun A => r * m A
where r has type {nonneg R}
mseries mu n == the measure corresponding to the sum of the
measures mu_n, mu_{n+1}, ...
mrestr mu mD == restriction of the measure mu to a set D; mD is a
proof that D is measurable
counting T R == counting measure
setI_closed G == the set of sets G is closed under finite
intersection
setU_closed G == the set of sets G is closed under finite union
setC_closed G == the set of sets G is closed under complement
setD_closed G == the set of sets G is closed under difference
ndseq_closed G == the set of sets G is closed under non-decreasing
countable union
trivIset_closed G == the set of sets G is closed under pairwise-disjoint
countable union
sfinite_measure == predicate for s-finite measure
functions
Measure_isSFinite_subdef == mixin for s-finite measures
SFiniteMeasure == structure of s-finite measures
{sfinite_measure set T -> \bar R} == type of s-finite measures
Measure_isSFinite == factory for s-finite measures
sfinite_measure_seq mu == the sequence of finite measures of
the s-finite measure mu
sigma_finite A f == the measure function f is
sigma-finite on the set A:set T
with T : semiRingOfSetsType
isSigmaFinite == mixin corresponding to
sigma finiteness
{sigma_finite_content set T -> \bar R} == contents that are also sigma
finite
{sigma_finite_measure set T -> \bar R} == measures that are also sigma
finite
fin_num_fun == predicate for finite function over measurable sets
SigmaFinite_isFinite == mixin for finite measures
FiniteMeasure == structure of finite measures
Measure_isFinite == factory for finite measures
mfrestr mD muDoo == finite measure corresponding to the restriction of
the measure mu over D with mu D < +oo,
mD : measurable D, muDoo : mu D < +oo
FiniteMeasure_isSubProbability == mixin corresponding to subprobability
SubProbability == structure of subprobability
subprobability T R == subprobability measure over the
measurableType T with value
in R : realType
Measure_isSubProbability == factory for subprobability measures
isProbability == mixin corresponding to probability measures
Probability == structure of probability measures
probability T R == probability measure over the
measurableType T with value in R : realType
Measure_isProbability == factor for probability measures
monotone_class D G == G is a monotone class of subsets of D
<<m D, G >> == monotone class generated by G on D
<<m G >> := <<m setT, G >>
dynkin G == G is a set of sets that form a Dynkin
(or a lambda) system
<<d G >> == Dynkin system generated by G, i.e.,
smallest dynkin G
measurable_fun D f == the function f with domain D is measurable
preimage_class D f G == class of the preimages by f of sets in G
image_class D f G == class of the sets with a preimage by f in G
mu.-negligible A == A is mu negligible
measure_is_complete mu == the measure mu is complete
{ae mu, forall x, P x} == P holds almost everywhere for the measure mu,
declared as an instance of the type of filters
ae_eq D f g == f is equal to g almost everywhere
From a premeasure to an outer measure (Measure Extension Theorem part 1):
measurable_cover X == the set of sequences F such that
- forall k, F k is measurable
- X `<=` \bigcup_k (F k)
mu^* == extension of the measure mu over a semiring of
sets (it is an outer measure)
From an outer measure to a measure (Measure Extension Theorem part 2):
mu.-caratheodory == the set of Caratheodory measurable sets for the
outer measure mu, i.e., sets A such that
forall B, mu A = mu (A `&` B) + mu (A `&` ~` B)
caratheodory_type mu := T, where mu : {outer_measure set T -> \bar R}
It is a canonical mesurableType copy of T.
The restriction of the outer measure mu to the
sigma algebra of Caratheodory measurable sets is a
measure.
Remark: sets that are negligible for
this measure are Caratheodory measurable.
Measure Extension Theorem:
measure_extension mu == extension of the content mu over a semiring of
sets to a measure over the generated
sigma algebra (requires a proof of
sigma-sub-additivity)
preimage_classes f1 f2 == sigma-algebra generated by the union of
the preimages by f1 and the preimages by
f2 with f1 : T -> T1 and f : T -> T2, T1
and T2 being measurableType's
(d1, d2).-prod.-measurable A == A is measurable for the sigma-algebra
generated from T1 x T2, with T1 and T2
measurableType's with resp. display d1
and d2
m1 `<< m2 == m1 is absolutely continuous w.r.t. m2 or m2 dominates m1
ess_sup f == essential supremum of the function f : T -> R where T is a
measurableType and R is a realType