Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
@affeldt-aist
affeldt-aist committed Dec 9, 2023
1 parent e845e9a commit d5ec088
Showing 1 changed file with 64 additions and 58 deletions.
122 changes: 64 additions & 58 deletions theories/measure.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand All @@ -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 *)
(* <<m D, G >> == monotone class generated by G on D *)
Expand All @@ -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 *)
Expand All @@ -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: *)
Expand Down

0 comments on commit d5ec088

Please sign in to comment.