Skip to content

fixes #1176 (duplicate in doc) #1180

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
proux01 merged 1 commit into from
Mar 5, 2024
Merged

fixes #1176 (duplicate in doc) #1180

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
182 changes: 75 additions & 107 deletions theories/measure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ From HB Require Import structures.
(* intermediate outer measure being *)
(* $\inf_F\{ \sum_{k=0}^\infty \mu(F_k) | X \subseteq \bigcup_k F_k\}.$ *)
(* *)
(* Reference: *)
(* 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 *)
Expand Down Expand Up @@ -54,7 +54,7 @@ From HB Require Import structures.
(* <<r G >> := smallest setring G *)
(* <<r G >> is equipped with a structure of ring *)
(* of sets. *)
(* G.-ring.-measurable A == A belongs for the ring of sets <<r G >> *)
(* G.-ring.-measurable A == A belongs to the ring of sets <<r 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 *)
Expand All @@ -69,67 +69,72 @@ From HB Require Import structures.
(* *)
(* ## Structures for functions on classes of sets *)
(* *)
(* A few details about mixins/factories to highlight implementations *)
(* peculiarities: *)
(* *)
(* 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. *)
(* 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 a *)
(* numFieldType. *)
(* The HB class is Measure. *)
(* Content_SubSigmaAdditive_isMeasure == mixin that extends a content to a *)
(* measure with the proof that it is *)
(* semi_sigma_additive *)
(* Content_isMeasure == factory that extends a content to a measure *)
(* with the proof that it is sub_sigma_additive *)
(* isMeasure == factory corresponding to the "textbook *)
(* definition" of measures *)
(* sfinite_measure == predicate for s-finite measure functions *)
(* T is expected to be a semiring of sets and *)
(* R is expected to be a numFieldType. *)
(* The HB class is Measure. *)
(* Content_SubSigmaAdditive_isMeasure == mixin that extends a content to *)
(* a measure with the proof that it is *)
(* semi_sigma_additive *)
(* Content_isMeasure == mixin that extends a content to a measure *)
Copy link
Collaborator

@proux01 proux01 Mar 5, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well technically, mixins are factories, and the doc probably shouldn't care to document which factories are mixin or not (because the user shouldn't rely on that and doe not need to know it).

Copy link
Member Author

@affeldt-aist affeldt-aist Mar 5, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should we call them all "interfaces"? "factory" is a bit HB-specific. "mixin" is not HB-specific but calling "mixins" "factories" might not help.

Copy link
Collaborator

@proux01 proux01 Mar 5, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

At least factory is what it is called in the (the bit of) doc we have for HB. Not sure it would be easy to relate a new term like "interface" to that. And at least, factory conveys well the fact that the thing is used to build an instance of the structure. "interface" seems to vague to me.

(* with the proof that it is semi_sigma_additive *)
(* isMeasure == factory 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 *)
(* Measure_isSFinite_subdef == mixin for s-finite measures *)
(* Measure_isSFinite == factory for s-finite measures *)
(* The HB class is SFiniteMeasure. *)
(* sfinite_measure_seq mu == the sequence of finite measures of the *)
(* s-finite measure mu *)
(* Measure_isSFinite_subdef == mixin for s-finite measures *)
Copy link
Collaborator

@proux01 proux01 Mar 5, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe this shouldn't be called _subdef if it needs to be documented?

(* Measure_isSFinite == factory for s-finite measures *)
(* isSigmaFinite == mixin corresponding to sigma finiteness *)
(* {sigma_finite_content set T -> \bar R} == contents that are also sigma *)
(* finite *)
(* The HB class is SigmaFiniteContent. *)
(* 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 *)
(* 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. *)
(* SigmaFinite_isFinite == mixin for finite measures *)
(* Measure_isFinite == factory for finite measures *)
(* subprobability T R == subprobability measure over the measurableType *)
(* T with values in \bar R with R : realType *)
(* The HB class is SubProbability. *)
(* probability T R == probability measure over the measurableType T *)
(* with values in \bar with R : realType *)
(* probability == type of probability measures *)
(* The HB class is Probability. *)
(* Measure_isProbability == factor for 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 *)
(* The HB class is FiniteMeasure. *)
(* SigmaFinite_isFinite == mixin for finite measures *)
(* Measure_isFinite == factory for finite measures *)
(* FiniteMeasure_isSubProbability == mixin corresponding to 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 == factory for subprobability measures *)
(* isProbability == mixin corresponding to 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 == factory for 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 *)
(* {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. *)
(* of elements of type T : Type where R is *)
(* expected to be a numFieldType *)
(* The HB class is OuterMeasure. *)
(* ``` *)
(* *)
(* ## Instances of measures *)
Expand All @@ -150,7 +155,13 @@ From HB Require Import structures.
(* 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 *)
Expand All @@ -160,63 +171,20 @@ From HB Require Import structures.
(* countable union *)
(* trivIset_closed G == the set of sets G is closed under pairwise-disjoint *)
(* countable union *)
(* monotone_class D G == G is a monotone class of subsets of D *)
(* <<m D, G >> == monotone class generated by G on D *)
(* <<m G >> := <<m setT, G >> *)
(* dynkin G == G is a set of sets that form a Dynkin *)
(* (or a lambda) system *)
(* <<d G >> == Dynkin system generated by G, i.e., *)
(* smallest dynkin G *)
(* ``` *)
(* ## Other measure-theoretic definitions *)
(* *)
(* ## 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 *)
(* *)
(* 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 *)
(* 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 *)
(* *)
(* 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 *)
(* <<m G >> := <<m setT, G >> *)
(* dynkin G == G is a set of sets that form a Dynkin *)
(* (or a lambda) system *)
(* <<d G >> == Dynkin system generated by G, i.e., *)
(* smallest dynkin G *)
(* *)
(* 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 *)
(* *)
(* 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, *)
Expand Down Expand Up @@ -267,7 +235,7 @@ From HB Require Import structures.
(* and d2 *)
(* ``` *)
(* *)
(* ## Others *)
(* ## 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 *)
Expand Down