Module mathcomp.analysis.measure_theory.measure_extension

# Measure Extension NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. ## Measure Extension Theorem: This file provides 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\}.$ ``` sigma_subadditive mu == predicate defining sigma-subadditivity {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 ``` ``` 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. mu .-cara.-measurable == sigma-algebra of Caratheodory measurable sets ``` 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): ``` 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 ```