From d5ec088f05f53f5a9a51de30eb6f6cc87e436d21 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 9 Dec 2023 18:21:58 +0900 Subject: [PATCH] fix --- theories/measure.v | 122 ++++++++++++++++++++++++--------------------- 1 file changed, 64 insertions(+), 58 deletions(-) diff --git a/theories/measure.v b/theories/measure.v index 80bfdb7cff..f3f57318b0 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -129,21 +129,21 @@ From HB Require Import structures. (* *) (* ## Instances of measures *) (* ``` *) -(* pushforward mf m == pushforward/image measure of m by f, where mf is a *) -(* proof that f is measurable *) -(* \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 *) +(* pushforward mf m == pushforward/image measure of m by f, where mf is a *) +(* proof that f is measurable *) +(* \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 *) @@ -158,42 +158,46 @@ From HB Require Import structures. (* *) (* ## 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 *) +(* 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 *) +(* 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 *) +(* 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 *) +(* 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 *) +(* 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 *) (* <> == monotone class generated by G on D *) @@ -213,22 +217,22 @@ From HB Require Import structures. (* declared as an instance of the type of filters *) (* ``` *) (* *) -(* # Measure Extension Theorem *) +(* ## 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) *) +(* 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 *) +(* 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} *) +(* 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 *) @@ -239,19 +243,21 @@ From HB Require Import structures. (* 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) *) +(* 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 *) +(* 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 *) +(* generated from T1 x T2, with T1 and T2 *) +(* measurableType's with resp. display d1 *) +(* and d2 *) (* ``` *) (* *) (* Others: *)