Module mathcomp.analysis.measure_theory.measurable_structure

# Measure Theory NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. 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. 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. ``` ## About sets of sets ``` 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 setD_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 set system <<M G >> == monotone set system 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 ``` preimage_set_system D f G == set system of the preimages by f of sets in G g_sigma_algebra_preimage f == sigma-algebra generated by the function f g_sigma_algebra_preimageType f == the measurableType corresponding to g_sigma_algebra_preimage f This is an HB alias. f.-preimage.-measurable A == A is measurable for g_sigma_algebra_preimage f image_set_system D f G == set system of the sets with a preimage by f in G subset_sigma_subadditive mu == alternative predicate defining sigma-subadditivity ``` ## Product of measurable spaces ``` g_sigma_preimageU 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 g_sigma_preimage n (f : 'I_n -> aT -> rT) == the sigma-algebra over aT generated by the projections f n.-tuple T is equipped with a measurableType using g_sigma_preimage and the tnth projections. ```