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\}.$ References: - 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. sigmaRingType d == the type of sigma-rings (of sets) The HB class is SigmaRing. 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 T == alias for the sigma-algebra [set: set T] setring G == the set of sets G contains the empty set, is closed by union, and difference (it is a ring of sets in the sense of ringOfSetsType) <<r G >> := smallest setring G <<r G >> is equipped with a structure of ring of sets. G.-ring.-measurable A == A belongs to the ring of sets <<r G >> sigma_ring G == the set of sets G forms a sigma-ring <<sr G >> == sigma-ring generated by G := smallest sigma_ring 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 >> g_sigma_algebraType 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 Hierarchy of contents, measures, s-finite/sigma-finite/finite measures, etc. Also contains a number of details about its implementation. ``` {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 is expected to be a numFieldType. The HB class is Measure. Content_isMeasure == interface that extends a content to a measure with the proof that it is semi_sigma_additive Content_SubSigmaAdditive_isMeasure == interface that extends a content to a measure with the proof that it is sigma_sub_additive isMeasure == interface 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 isSFinite == interface for functions that satisfy the sfinite_measure predicate s-finite measure using a sequence of finite measures Measure_isSFinite == interface that extends a measure to an s-finite measure using a sequence of finite measures isSigmaFinite == interface for functions that satisfy sigma finiteness {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. isFinite == interface for functions that satisfy the fin_num_fun predicate Measure_isFinite == interface that extends a measure to a finite measure using a proof of fin_num_fun isSubProbability == interface for functions that satisfy the property of subprobability The HB class is SubProbability. subprobability T R == subprobability measure over the measurableType T with values in \bar R with R : realType The HB class is SubProbability. Measure_isSubProbability == interface that extends measures to subprobability measures isProbability == interface for functions that satisfy the property of probability measures The HB class is Probability. probability T R == type of probability measure over the measurableType T with values in \bar R with R : realType Measure_isProbability == interface that extends measures to probability measures mnormalize mu == normalization of a measure to a probability mset U r == the set of probability measures mu such that mu U < r pset == the sets mset U r with U measurable and r \in [0,1] pprobability == the measurable type generated by pset lim_sup_set F == limit superior (or upper limit) of a sequence of sets F {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. interfaces: isOuterMeasure, isSubsetOuterMeasure ``` ## 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 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 ``` ## About sets of sets ``` 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 setSD_closed G == the set of sets G is closed under proper difference setDI_closed G == the set of sets G is closed under difference setY_closed G == the set of sets G is closed under symmetric difference ndseq_closed G == the set of sets G is closed under non-decreasing countable union niseq_closed G == the set of sets G is closed under non-increasing countable intersection trivIset_closed G == the set of sets G is closed under pairwise-disjoint countable union lambda_system D G == G is a lambda_system of subsets of D <<l D, G >> == lambda-system generated by G on D <<l G >> := <<m setT, G >> monotone G == G is a monotone class <<M G >> == monotone class generated by G := smallest monotone G dynkin G == G is a set of sets that form a Dynkin system (or a d-system) <<d G >> == Dynkin system generated by G, i.e., smallest dynkin G strace G D := [set x `&` D | x in G] ``` ## Other measure-theoretic definitions ``` 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 sigma_subadditive mu == predicate defining sigma-subadditivity subset_sigma_subadditive mu == alternative predicate defining sigma-subadditivity 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 measurableType 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) completed_measure_extension mu == similar to measure_extension but returns a complete measure ``` ## 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 semiRingOfSetsType's (d1, d2).-prod.-measurable A == A is measurable for the sigma-algebra generated from T1 x T2, with T1 and T2 semiRingOfSetsType's with resp. display d1 and d2 ``` ## More measure-theoretic definitions ``` 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 semiRingOfSetsType and R is a realType ```