Module mathcomp.analysis.measure

# Measure Theory 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 $\inf_F\{ \sum_{k=0}^\infty \mu(F_k) | X \subseteq \bigcup_k F_k\}.$ Reference: - R. Affeldt, C. Cohen. Measure construction by extension in dependent type theory with application to integration. JAR 2023 - Daniel Li. Intégration et applications. 2016 - Achim Klenke. Probability Theory. 2014 ## Mathematical structures ``` 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. ``` ## Instances of mathematical structures ``` 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 ``` ## Structures for functions on classes of 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. ``` ## Instances of measures ``` 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 ``` ## Hierarchy of s-finite, sigma-finite, finite measures ``` 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 ``` ## Measure extension theorem 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) ``` ## Product of measurable spaces ``` 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 ``` ## Others ``` 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 ```