From 2fc1a66485357e59118e7e60bbd06e2ab0bb5474 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 24 Nov 2023 15:28:43 +0900 Subject: [PATCH] test a few files --- classical/boolp.v | 26 ++-- classical/cardinality.v | 6 +- classical/classical_sets.v | 105 +++++++++----- classical/fsbigop.v | 6 +- classical/functions.v | 180 +++++++++--------------- classical/mathcomp_extra.v | 14 +- classical/set_interval.v | 12 +- theories/Rstruct.v | 8 +- theories/cantor.v | 75 +++++----- theories/charge.v | 17 ++- theories/constructive_ereal.v | 26 ++-- theories/convex.v | 7 +- theories/derive.v | 6 +- theories/ereal.v | 15 +- theories/esum.v | 6 +- theories/exp.v | 13 +- theories/forms.v | 5 +- theories/hoelder.v | 7 +- theories/itv.v | 28 +++- theories/kernel.v | 11 +- theories/landau.v | 66 +++++---- theories/lebesgue_integral.v | 26 ++-- theories/lebesgue_measure.v | 18 ++- theories/lebesgue_stieltjes_measure.v | 6 +- theories/measure.v | 64 ++++++--- theories/normedtype.v | 72 ++++++---- theories/nsatz_realtype.v | 7 +- theories/numfun.v | 6 +- theories/probability.v | 7 +- theories/real_interval.v | 5 +- theories/realfun.v | 17 ++- theories/reals.v | 15 +- theories/sequences.v | 42 +++--- theories/signed.v | 47 +++++-- theories/summability.v | 4 + theories/topology.v | 194 ++++++++++++++++---------- theories/trigo.v | 6 +- 37 files changed, 701 insertions(+), 474 deletions(-) diff --git a/classical/boolp.v b/classical/boolp.v index 1bb538d611..d0b71e9b61 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -7,18 +7,18 @@ From mathcomp Require Import all_ssreflect. -(******************************************************************************) -(* Classical Logic *) +(***markdown*******************************************************************) +(* # Classical Logic *) (* *) (* This file provides the axioms of classical logic and tools to perform *) (* classical reasoning in the Mathematical Compnent framework. The three *) (* axioms are taken from the standard library of Coq, more details can be *) (* found in Section 5 of *) -(* Reynald Affeldt, Cyril Cohen, Damien Rouhling: *) -(* Formalization Techniques for Asymptotic Reasoning in Classical Analysis. *) -(* Journal of Formalized Reasoning, 2018 *) +(* - R. Affeldt, C. Cohen, D. Rouhling. Formalization Techniques for *) +(* Asymptotic Reasoning in Classical Analysis. JFR 2018 *) (* *) -(* * Axioms *) +(* ## Axioms *) +(* ``` *) (* functional_extensionality_dep == functional extensionality (on dependently *) (* typed functions), i.e., functions that are pointwise *) (* equal are equal *) @@ -27,14 +27,19 @@ From mathcomp Require Import all_ssreflect. (* constructive_indefinite_description == existential in Prop (ex) implies *) (* existential in Type (sig) *) (* cid := constructive_indefinite_description (shortcut) *) -(* --> A number of properties are derived below from these axioms and are *) +(* ``` *) +(* *) +(* A number of properties are derived below from these axioms and are *) (* often more pratical to use than directly using the axioms. For instance *) (* propext, funext, the excluded middle (EM),... *) (* *) -(* * Boolean View of Prop *) +(* ## Boolean View of Prop *) +(* ``` *) (* `[< P >] == boolean view of P : Prop, see all lemmas about asbool *) +(* ``` *) (* *) -(* * Mathematical Components Structures *) +(* ## Mathematical Components Structures *) +(* ``` *) (* {classic T} == Endow T : Type with a canonical eqType/choiceType. *) (* This is intended for local use. *) (* E.g., T : Type |- A : {fset {classic T}} *) @@ -43,8 +48,9 @@ From mathcomp Require Import all_ssreflect. (* {eclassic T} == Endow T : eqType with a canonical choiceType. *) (* On the model of {classic _}. *) (* See also the lemmas Peq and eqPchoice. *) +(* ``` *) (* *) -(* --> Functions into a porderType (resp. latticeType) are equipped with *) +(* Functions into a porderType (resp. latticeType) are equipped with *) (* a porderType (resp. latticeType), (f <= g)%O when f x <= g x for all x, *) (* see lemma lefP. *) (******************************************************************************) diff --git a/classical/cardinality.v b/classical/cardinality.v index 654763b373..dbd0f0b56b 100644 --- a/classical/cardinality.v +++ b/classical/cardinality.v @@ -3,8 +3,8 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -(******************************************************************************) -(* Cardinality *) +(***markdown*******************************************************************) +(* # Cardinality *) (* *) (* This file provides an account of cardinality properties of classical sets. *) (* This includes standard results of set theory such as the Pigeon Hole *) @@ -16,6 +16,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions. (* only relations A #<= B and A #= B to compare the cardinals of two sets *) (* (on two possibly different types). *) (* *) +(* ``` *) (* A #<= B == the cardinal of A is smaller or equal to the one of B *) (* A #>= B := B #<= A *) (* A #= B == the cardinal of A is equal to the cardinal of B *) @@ -32,6 +33,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions. (* A.`1 := [fset x.1 | x in A] *) (* A.`2 := [fset x.2 | x in A] *) (* {fimfun aT >-> T} == type of functions with a finite image *) +(* ``` *) (* *) (******************************************************************************) diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 169bbd94ce..1e1792f330 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -3,19 +3,62 @@ From mathcomp Require Import all_ssreflect ssralg matrix finmap order ssrnum. From mathcomp Require Import ssrint interval. From mathcomp Require Import mathcomp_extra boolp. -(******************************************************************************) +(***markdown*******************************************************************) +(* # Set Theory *) +(* *) (* This file develops a basic theory of sets and types equipped with a *) -(* canonical inhabitant (pointed types). *) +(* canonical inhabitant (pointed types): *) +(* - A decidable equality is defined for any type. It is thus possible to *) +(* define an eqType structure for any type using the mixin gen_eqMixin. *) +(* - This file adds the possibility to define a choiceType structure for *) +(* any type thanks to an axiom gen_choiceMixin giving a choice mixin. *) +(* - We chose to have generic mixins and no global instances of the eqType *) +(* and choiceType structures to let the user choose which definition of *) +(* equality to use and to avoid conflict with already declared instances. *) +(* *) +(* Thanks to this basic set theory, we proved Zorn's Lemma, which states *) +(* that any ordered set such that every totally ordered subset admits an *) +(* upper bound has a maximal element. We also proved an analogous version *) +(* for preorders, where maximal is replaced with premaximal: $t$ is *) +(* premaximal if whenever $t < s$ we also have $s < t$. *) +(* *) +(* About the naming conventions in this file: *) +(* - use T, T', T1, T2, etc., aT (domain type), rT (return type) for names *) +(* of variables in Type (or choiceType/pointedType/porderType) *) +(* + use the same suffix or prefix for the sets as their containing type *) +(* (e.g., A1 in T1, etc.) *) +(* + as a consequence functions are rather of type aT -> rT *) +(* - use I, J when the type corresponds to an index *) +(* - sets are named A, B, C, D, etc., or Y when it is ostensibly an image *) +(* set (i.e., of type set rT) *) +(* - indexed sets are rather named F *) (* *) -(* --> A decidable equality is defined for any type. It is thus possible to *) -(* define an eqType structure for any type using the mixin gen_eqMixin. *) -(* --> This file adds the possibility to define a choiceType structure for *) -(* any type thanks to an axiom gen_choiceMixin giving a choice mixin. *) -(* --> We chose to have generic mixins and no global instances of the eqType *) -(* and choiceType structures to let the user choose which definition of *) -(* equality to use and to avoid conflict with already declared instances. *) +(* Sample notations: *) +(* | Coq notations | Meaning | *) +(* |-------------------------------------|----------------------------------| *) +(* | set0 | $\emptyset$ | *) +(* | [set: A] | the full set of elements | *) +(* | | of type A | *) +(* | `` `\|` `` | $\cup$ | *) +(* | `` `&` `` | $\cap$ | *) +(* | `` `\` `` | set difference | *) +(* | `` ~` `` | set complement | *) +(* | `` `<=` `` | $\subseteq$ | *) +(* | `` f @` A `` | image by f of A | *) +(* | `` f @^-1` A `` | preimage by f of A | *) +(* | [set x] | The singleton set $\{x\}$ | *) +(* | [set~ x] | The complement of $\{x\}$ | *) +(* | [set E \| x in P] | the set of E with x ranging in P | *) +(* | range f | image by f of the full set | *) +(* | \big[setU/set0]_(i <- s \| P i) f i | finite union | *) +(* | \bigcup_(k in P) F k | countable union | *) +(* | \bigcap_(k in P) F k | countable intersection | *) +(* | trivIset D F | F is a sequence of pairwise | *) +(* | | disjoint sets indexed over | *) +(* | | the domain D | *) (* *) -(* * Sets: *) +(* ## Sets *) +(* ``` *) (* set T == type of sets on T. *) (* (x \in P) == boolean membership predicate from ssrbool *) (* for set P, available thanks to a canonical *) @@ -86,8 +129,10 @@ From mathcomp Require Import mathcomp_extra boolp. (* if there is one, to f0 x otherwise. *) (* F `#` G <-> intersections beween elements of F an G are *) (* all non empty. *) +(* ``` *) (* *) -(* * Pointed types: *) +(* ## Pointed types *) +(* ``` *) (* pointedType == interface type for types equipped with a *) (* canonical inhabitant. *) (* PointedType T m == packs the term m : T to build a *) @@ -99,20 +144,19 @@ From mathcomp Require Import mathcomp_extra boolp. (* point == canonical inhabitant of a pointedType. *) (* get P == point x in P if it exists, point otherwise; *) (* P must be a set on a pointedType. *) +(* ``` *) (* *) -(* --> Thanks to this basic set theory, we proved Zorn's Lemma, which states *) -(* that any ordered set such that every totally ordered subset admits an *) -(* upper bound has a maximal element. We also proved an analogous version *) -(* for preorders, where maximal is replaced with premaximal: t is *) -(* premaximal if whenever t < s we also have s < t. *) -(* *) +(* ``` *) (* $| T | == T : Type is inhabited *) (* squash x == proof of $| T | (with x : T) *) (* unsquash s == extract a witness from s : $| T | *) -(* --> Tactic: *) +(* ``` *) +(* *) +(* ## Tactic *) (* - squash x: *) (* solves a goal $| T | by instantiating with x or [the T of x] *) (* *) +(* ``` *) (* trivIset D F == the sets F i, where i ranges over D : set I,*) (* are pairwise-disjoint *) (* cover D F := \bigcup_(i in D) F i *) @@ -124,12 +168,17 @@ From mathcomp Require Import mathcomp_extra boolp. (* maximal_disjoint_subcollection F A B == A is a maximal (for inclusion) *) (* disjoint subcollection of the collection *) (* B of elements in F : I -> set T *) +(* ``` *) (* *) -(* * Upper and lower bounds: *) +(* ## Upper and lower bounds *) +(* ``` *) (* ubound A == the set of upper bounds of the set A *) (* lbound A == the set of lower bounds of the set A *) +(* ``` *) +(* *) (* Predicates to express existence conditions of supremum and infimum of *) (* sets of real numbers: *) +(* ``` *) (* has_ubound A := ubound A != set0 *) (* has_sup A := A != set0 /\ has_ubound A *) (* has_lbound A := lbound A != set0 *) @@ -142,26 +191,18 @@ From mathcomp Require Import mathcomp_extra boolp. (* infimum x0 A == infimum of A or x0 if A is empty *) (* *) (* F `#` G := the classes of sets F and G intersect *) +(* ``` *) (* *) -(* * sections: *) +(* ## Sections *) (* xsection A x == with A : set (T1 * T2) and x : T1 is the *) (* x-section of A *) (* ysection A y == with A : set (T1 * T2) and y : T2 is the *) (* y-section of A *) (* *) -(* * About the naming conventions in this file: *) -(* - use T, T', T1, T2, etc., aT (domain type), rT (return type) for names of *) -(* variables in Type (or choiceType/pointedType/porderType) *) -(* + use the same suffix or prefix for the sets as their containing type *) -(* (e.g., A1 in T1, etc.) *) -(* + as a consequence functions are rather of type aT -> rT *) -(* - use I, J when the type corresponds to an index *) -(* - sets are named A, B, C, D, etc., or Y when it is ostensibly an image set *) -(* (i.e., of type set rT) *) -(* - indexed sets are rather named F *) -(* *) -(* * Composition of relations: *) +(* ## Composition of relations *) +(* ``` *) (* A \; B == [set x | exists z, A (x.1, z) & B (z, x.2)] *) +(* ``` *) (* *) (******************************************************************************) diff --git a/classical/fsbigop.v b/classical/fsbigop.v index 6d9f5d76ce..05a38cdc44 100644 --- a/classical/fsbigop.v +++ b/classical/fsbigop.v @@ -3,13 +3,15 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality. -(******************************************************************************) -(* Finitely-supported big operators *) +(***markdown*******************************************************************) +(* # Finitely-supported big operators *) (* *) +(* ``` *) (* finite_support idx D F := D `&` F @^-1` [set~ idx] *) (* \big[op/idx]_(i \in A) F i == iterated application of the operator op *) (* with neutral idx over finite_support idx A F *) (* \sum_(i \in A) F i == iterated addition, in ring_scope *) +(* ``` *) (* *) (******************************************************************************) diff --git a/classical/functions.v b/classical/functions.v index 4b107ada1c..0a1ad9e554 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -7,12 +7,13 @@ Add Search Blacklist "__functions_". Add Search Blacklist "_factory_". Add Search Blacklist "_mixin_". -(******************************************************************************) -(* Theory of functions *) +(***markdown*******************************************************************) +(* # Theory of functions *) (* *) -(* This file provides a theory of functions whose domain and codomain are *) -(* represented by sets. *) +(* This file provides a theory of functions $f : A\to B$ whose domain $A$ *) +(* and codomain $B$ are represented by sets. *) (* *) +(* ``` *) (* set_fun A B f == f : aT -> rT is a function with domain *) (* A : set aT and codomain B : set rT *) (* set_surj A B f == f is surjective *) @@ -44,7 +45,9 @@ Add Search Blacklist "_mixin_". (* {splitsurj A >-> B} *) (* 'inj_ f == proof of {in A &, injective f} where f has type *) (* {splitinj A >-> _} *) +(* ``` *) (* *) +(* ``` *) (* funin A f == alias for f : aT -> rT, with A : set aT *) (* [fun f in A] == the function f from the set A to the set f @` A*) (* 'split_ d f == partial injection from aT : Type to rt : Type; *) @@ -78,8 +81,10 @@ Add Search Blacklist "_mixin_". (* 'pinv_ d A f == inverse of the function [fun f in A] over *) (* f @` A, function d outside of f @` A *) (* pinv := notation for 'pinv_point *) +(* ``` *) (* *) -(* * Function restriction: *) +(* ## Function restriction *) +(* ``` *) (* patch d A f == "partial function" that behaves as the function *) (* f over the set A and as the function d otherwise *) (* restrict D f := patch (fun=> point) D f *) @@ -105,11 +110,14 @@ Add Search Blacklist "_mixin_". (* valLfun_ v A B f := [fun of valL_ f] with f : {fun [set: A] >-> B} *) (* valL := 'valL_ point *) (* valLRfun v := 'valLfun_ v \o valR_fun *) +(* ``` *) (* *) +(* ``` *) (* Section function_space == canonical ringType and lmodType *) (* structures for functions whose range is *) (* a ringType, comRingType, or lmodType. *) (* fctE == multi-rule for fct *) +(* ``` *) (* *) (******************************************************************************) @@ -348,10 +356,8 @@ HB.structure Definition SplitBij {aT rT} {A : set aT} {B : set rT} := Notation "{ 'splitbij' A >-> B }" := (@SplitBij.type _ _ A B) : type_scope. Notation "[ 'splitbij' 'of' f ]" := [the {splitbij _ >-> _} of f] : form_scope. -(** begin hide *) (* Hint View for move / Inversible.sort inv | 2. *) (* Hint View for apply / Inversible.sort inv | 2. *) -(** end hide *) Module ShortFunSyntax. Notation "A ~> B" := {fun A >-> B} (at level 70) : type_scope. @@ -371,9 +377,9 @@ Notation "A <~> B" := {bij A >-> B} (at level 70) : type_scope. Notation "A <<~> B" := {splitbij A >-> B} (at level 70) : type_scope. End ShortFunSyntax. -(**********) -(* Theory *) -(**********) +(***markdown*******************************************************************) +(* ## Theory *) +(******************************************************************************) Definition phant_funS aT rT (A : set aT) (B : set rT) (f : {fun A >-> B}) of phantom (_ -> _) f := @funS _ _ _ _ f. @@ -478,9 +484,7 @@ Definition phant_funK aT rT (A : set aT) (f : {splitinj A >-> rT}) Notation "'funK_ f" := (phant_funK (Phantom (_ -> _) f)) : form_scope. #[global] Hint Resolve funK : core. -(**********************) -(* Structure Equality *) -(**********************) +(** Structure Equality *) Lemma funP {aT rT} {A : set aT} {B : set rT} (f g : {fun A >-> B}) : f = g <-> f =1 g. @@ -491,9 +495,7 @@ rewrite eqfg in ffun *; congr {| Fun.sort := _; Fun.class := {| exact: Prop_irrelevance. Qed. -(************************) -(* Preliminary Builders *) -(************************) +(** Preliminary Builders *) HB.factory Record Inv_Can {aT rT} {A : set aT} (f : aT -> rT) of Inv _ _ f := { funK : {in A, cancel f f^-1} }. @@ -517,9 +519,7 @@ HB.builders Context {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) HB.instance Definition _ := OInv_CanV.Build _ _ _ _ f oinvS oinvK. HB.end. -(*********************) -(* Trivial instances *) -(*********************) +(** Trivial instances *) Section OInverse. Context {aT rT : Type} {A : set aT} {B : set rT}. @@ -770,9 +770,7 @@ HB.instance Definition _ (f : {surjfun A >-> B}) := Fun.on (omap f). HB.instance Definition _ (f : {bij A >-> B}) := Fun.on (omap f). End Map. -(************) -(* Builders *) -(************) +(** Builders *) HB.factory Record CanV {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) := { inv; invS : {homo inv : x / B x >-> A x}; invK : {in B, cancel inv f}; }. @@ -857,9 +855,7 @@ HB.builders Context {aT rT} f of BijTT aT rT f. (in1W (projT2 exg).1) (in1W (projT2 exg).2). HB.end. -(**********) -(* Fun in *) -(**********) +(** Fun in *) Section surj_oinv. Context {aT rT} {A : set aT} {B : set rT} {f : aT -> rT} (fsurj : set_surj A B f). @@ -927,9 +923,7 @@ Notation "[ 'fun' f 'in' A ]" := (funin A f) format "[ 'fun' f 'in' A ]") : function_scope. #[global] Hint Resolve set_fun_image : core. -(*********************) -(* Partial injection *) -(*********************) +(** Partial injection *) Section split. Context {aT rT} (A : set aT) (B : set rT). @@ -967,9 +961,7 @@ End split. Notation "''split_' a" := (split_ a) : form_scope. Notation split := 'split_point. -(*****************) -(* More Builders *) -(*****************) +(** More Builders *) HB.factory Record Inj {aT rT} (A : set aT) (f : aT -> rT) := { inj : {in A &, injective f} }. @@ -1014,9 +1006,9 @@ HB.instance Definition _ (f : {inj A >-> rT}) := SurjFun_Inj.Build _ _ _ _ [fun f in A] 'inj_f. End Inverses. -(********************) -(* Simple Factories *) -(********************) +(***markdown*******************************************************************) +(* ## Simple Factories *) +(******************************************************************************) Section Pinj. Context {aT rT} {A : set aT} {f : aT -> rT} (finj : {in A &, injective f}). @@ -1109,20 +1101,16 @@ Proof. by move/in1W/(@funPsplitsurj _ _ _ _ [fun of totalfun f] [fun of totalfun g]). Qed. -(*************) -(* Instances *) -(*************) +(***markdown*******************************************************************) +(* ## Instances *) +(******************************************************************************) -(*************************************) -(* The identity is a split bijection *) -(*************************************) +(** The identity is a split bijection *) HB.instance Definition _ T A := @Can2.Build T T A A idfun idfun (fun x y => y) (fun x y => y) (fun _ _ => erefl) (fun _ _ => erefl). -(**********************************************************) -(* Iteration preserves Fun, Injectivity, and Surjectivity *) -(**********************************************************) +(** Iteration preserves Fun, Injectivity, and Surjectivity *) Section iter_inv. Context {aT} {A : set aT}. @@ -1189,9 +1177,7 @@ HB.instance Definition _ n (f : {splitbij A >-> A}) := Surject.on (iter n f). End iter_surj. -(**********) -(* Unbind *) -(**********) +(** Unbind *) Section Unbind. Context {aT rT} {A : set aT} {B : set rT} (dflt : aT -> rT). @@ -1248,9 +1234,7 @@ HB.instance Definition _ (f : {splitbij A >-> some @` B}) := Bij.on (unbind f). End Unbind. -(*********) -(* Odflt *) -(*********) +(** Odflt *) Section Odflt. Context {T} {A : set T} (x : T). @@ -1264,9 +1248,7 @@ HB.instance Definition _ := SplitBij.copy (odflt x) End Odflt. -(************) -(* Subtypes *) -(************) +(** Subtypes *) Section SubType. Context {T : Type} {P : pred T} (sT : subType P) (x0 : sT). @@ -1291,9 +1273,7 @@ Lemma inv_insubd : (insubd x0)^-1 = val. Proof. by []. Qed. End SubType. -(***********) -(* To setT *) -(***********) +(** To setT *) Definition to_setT {T} (x : T) : [set: T] := @SigSub _ _ _ x (mem_set I : x \in setT). @@ -1306,9 +1286,7 @@ Definition setTbij {T} := [splitbij of @to_setT T]. Lemma inv_to_setT T : (@to_setT T)^-1 = val. Proof. by []. Qed. -(**********) -(* Subfun *) -(**********) +(** Subfun *) Section subfun. Context {T} {A B : set T}. @@ -1364,9 +1342,8 @@ HB.instance Definition _ := seteqfun_can2_subproof. End seteqfun. -(*************) -(* Inclusion *) -(*************) +(** Inclusion *) + Section incl. Context {T} {A B : set T}. Definition incl (AB : A `<=` B) := @id T. @@ -1385,9 +1362,7 @@ HB.instance Definition _ AB := eqincl_surj AB. End incl. Notation inclT A := (incl (@subsetT _ _)). -(*******************) -(* Ad hoc function *) -(*******************) +(** Ad hoc function *) Section mkfun. Context {aT} {rT} {A : set aT} {B : set rT}. @@ -1404,9 +1379,7 @@ HB.instance Definition _ (f : {splitsurj A >-> B}) fAB := SplitSurj.on (@mkfun f fAB). End mkfun. -(***********) -(* set_val *) -(***********) +(** set_val *) Section set_val. Context {T} {A : set T}. @@ -1419,27 +1392,21 @@ End set_val. #[global] Hint Extern 0 (is_true (set_val _ \in _)) => solve [apply: valP] : core. -(**********) -(* Squash *) -(**********) +(** Squash *) HB.instance Definition _ T := CanV.Build T $|T| setT setT squash (fun _ _ => I) (in1W unsquashK). HB.instance Definition _ T := SplitInj.copy (@unsquash T) squash^-1%FUN. Definition ssquash {T} := [splitsurj of @squash T]. -(***********************) -(* pickle and unpickle *) -(***********************) +(** pickle and unpickle *) HB.instance Definition _ (T : countType) := Inj.Build _ _ setT (@choice.pickle T) (in2W (pcan_inj choice.pickleK)). HB.instance Definition _ (T : countType) := isFun.Build _ _ setT setT (@choice.pickle T) (fun _ _ => I). -(***********) -(* set0fun *) -(***********) +(** set0fun *) Lemma set0fun_inj {P T} : injective (@set0fun P T). Proof. by case=> x x0; have := set_mem x0. Qed. @@ -1449,18 +1416,14 @@ HB.instance Definition _ P T := HB.instance Definition _ P T := isFun.Build _ _ setT setT (@set0fun P T) (fun _ _ => I). -(************) -(* cast_ord *) -(************) +(** cast_ord *) HB.instance Definition _ {m n} {eq_mn : m = n} := Can2.Build 'I_m 'I_n setT setT (cast_ord eq_mn) (fun _ _ => I) (fun _ _ => I) (in1W (cast_ordK _)) (in1W (cast_ordKV _)). -(************************) -(* enum_val & enum_rank *) -(************************) +(** enum_val & enum_rank *) HB.instance Definition _ (T : finType) := Can2.Build T _ setT setT enum_rank (fun _ _ => I) (fun _ _ => I) @@ -1470,9 +1433,7 @@ HB.instance Definition _ (T : finType) := Can2.Build _ T setT setT enum_val (fun _ _ => I) (fun _ _ => I) (in1W enum_valK) (in1W enum_rankK). -(**************) -(* Finset val *) -(**************) +(** Finset val *) Definition finset_val {T : choiceType} {X : {fset T}} (x : X) : [set` X] := exist (fun x => x \in [set` X]) (val x) (mem_set (valP x)). @@ -1494,17 +1455,15 @@ HB.instance Definition _ {T : choiceType} {X : {fset T}} := Can2.Build _ X setT setT val_finset (fun _ _ => I) (fun _ _ => I) (in1W val_finsetK) (in1W finset_valK). -(*****************) -(* 'I_n and `I_n *) -(*****************) +(** 'I_n and `I_n *) HB.instance Definition _ n := Can2.Build _ _ setT setT (@ordII n) (fun _ _ => I) (fun _ _ => I) (in1W ordIIK) (in1W IIordK). HB.instance Definition _ n := SplitBij.copy (@IIord n) (ordII^-1). -(***********) -(* Glueing *) -(***********) +(***markdown*******************************************************************) +(* ## Glueing *) +(******************************************************************************) Definition glue {T T'} {X Y : set T} {A B : set T'} of [disjoint X & Y] & [disjoint A & B] := @@ -1599,9 +1558,7 @@ HB.instance Definition _ (f : {splitbij X >-> A}) (g : {splitbij Y >-> B}) := End Glue. -(************************************) -(* Z-module addition is a bijection *) -(************************************) +(** Z-module addition is a bijection *) Section addition. Context {V : zmodType} (x : V). @@ -1616,9 +1573,7 @@ HB.instance Definition _ := addr_can2_subproof. End addition. -(************************************) -(* Z-module opposite is a bijection *) -(************************************) +(** Z-module opposite is a bijection *) Section addition. Context {V : zmodType} (x : V). @@ -1633,9 +1588,7 @@ HB.instance Definition _ := oppr_can2_subproof. End addition. -(*************) -(* emtpyType *) -(*************) +(** emtpyType *) Section empty. Context {T : emptyType} {T' : Type} {X : set T}. @@ -1656,9 +1609,9 @@ HB.instance Definition _ := empty_canv_subproof. End empty. -(************************) -(* Theory of surjection *) -(************************) +(***markdown*******************************************************************) +(* ## Theory of surjection *) +(******************************************************************************) Section surj_lemmas. Variables aT rT : Type. @@ -1795,9 +1748,7 @@ move=> j; apply/seteqP; split=> x. by move=> [f fDE fF i Fi]; exists (f i); [apply: fDE|apply: fF]. Qed. -(**************) -(* Injections *) -(**************) +(** Injections *) Lemma trivIset_inj T I (D : set I) (F : I -> set T) : (forall i, D i -> F i !=set0) -> trivIset D F -> set_inj D F. @@ -1806,9 +1757,7 @@ move=> FN0 Ftriv i j; rewrite !inE => Di Dj Fij. by apply: Ftriv Di (Dj) _; rewrite Fij setIid; apply: FN0. Qed. -(**************) -(* Bijections *) -(**************) +(** Bijections *) Section set_bij_lemmas. Context {aT rT : Type} {A : set aT} {B : set rT} {f : aT -> rT}. @@ -1873,9 +1822,9 @@ Definition phant_bijTT aT rT (f : {bij [set: aT] >-> [set: rT]}) Notation "''bijTT_' f" := (phant_bijTT (Phantom (_ -> _) f)) : form_scope. #[global] Hint Extern 0 (bijective _) => solve [apply: bijTT] : core. -(*****************************) -(* Patching and restrictions *) -(*****************************) +(***markdown*******************************************************************) +(* ## Patching and restrictions *) +(******************************************************************************) Section patch. Context {aT rT : Type} (d : aT -> rT) (A : set aT). @@ -1957,10 +1906,9 @@ do 2![case: ifPn => //]; rewrite !in_setE => Di Dj Fix Fjx. by apply: FDtriv => //; exists x. Qed. - -(**************************************) -(* Restriction of domain and codomain *) -(**************************************) +(***markdown*******************************************************************) +(* ## Restriction of domain and codomain *) +(******************************************************************************) Section RestrictionLeft. Context {U V : Type} (v : V) {A : set U} {B : set V}. diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 55b8c3b3a8..1bc93f99fb 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -9,13 +9,12 @@ Coercion choice.Choice.mixin : choice.Choice.class_of >-> choice.Choice.mixin_of From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat. From mathcomp Require Import finset interval. -(***************************) -(* MathComp 1.15 additions *) -(***************************) - -(******************************************************************************) +(***markdown*******************************************************************) +(* # MathComp extra *) +(* *) (* This files contains lemmas and definitions missing from MathComp. *) (* *) +(* ``` *) (* f \max g := fun x => Num.max (f x) (g x) *) (* f \min g := fun x => Num.min (f x) (g x) *) (* oflit f := Some \o f *) @@ -30,6 +29,7 @@ From mathcomp Require Import finset interval. (* dfwith f x == fun j => x if j = i, and f j otherwise *) (* given x : T i *) (* swap x := (x.2, x.1) *) +(* ``` *) (* *) (******************************************************************************) @@ -37,6 +37,10 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +(***************************) +(* MathComp 1.15 additions *) +(***************************) + Reserved Notation "f \* g" (at level 40, left associativity). Reserved Notation "f \- g" (at level 50, left associativity). Reserved Notation "\- f" (at level 35, f at level 35). diff --git a/classical/set_interval.v b/classical/set_interval.v index de21257682..c5889c6e81 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -4,9 +4,12 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets. From HB Require Import structures. From mathcomp Require Import functions. -(******************************************************************************) +(***markdown*******************************************************************) +(* # Sets and Intervals *) +(* *) (* This files contains lemmas about sets and intervals. *) (* *) +(* ``` *) (* neitv i == the interval i is non-empty *) (* when the support type is a numFieldType, this *) (* is equivalent to (i.1 < i.2)%O (lemma neitvE) *) @@ -17,6 +20,7 @@ From mathcomp Require Import functions. (* factor a b x := (x - a) / (b - a) *) (* set_itvE == multirule to turn intervals into inequalities *) (* disjoint_itv i j == intervals i and j are disjoint *) +(* ``` *) (* *) (******************************************************************************) @@ -28,8 +32,8 @@ Import Order.TTheory GRing.Theory Num.Def Num.Theory. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -(* definitions and lemmas to make a bridge between MathComp intervals and *) -(* classical sets *) +(** definitions and lemmas to make a bridge between MathComp intervals and + classical sets *) Section set_itv_porderType. Variables (d : unit) (T : porderType d). Implicit Types (i j : interval T) (x y : T) (a : itv_bound T). @@ -319,7 +323,7 @@ rewrite predeqE => /= r; split => [[{}r + <-]|]. by exists (- r); rewrite ?opprK// !in_itv/= ltr_oppl ltr_oppr andbC. Qed. -(* lemmas between itv and set-theoretic operations *) +(** lemmas between itv and set-theoretic operations *) Section set_itv_porderType. Variables (d : unit) (T : orderType d). Implicit Types (a : itv_bound T) (x y : T) (i j : interval T) (b : bool). diff --git a/theories/Rstruct.v b/theories/Rstruct.v index 299ff3eb29..3861f49099 100644 --- a/theories/Rstruct.v +++ b/theories/Rstruct.v @@ -21,6 +21,10 @@ the economic rights, and the successive licensors have only limited liability. See the COPYING file for more details. *) +(***markdown*******************************************************************) +(* # Compatibility with the real numbers of Coq *) +(******************************************************************************) + Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf. Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def. Require Import Rtrigo1 Reals. @@ -201,9 +205,10 @@ by move/RlebP=> ->; rewrite orbT. Qed. Lemma RnormM : {morph Rabs : x y / x * y}. -exact: Rabs_mult. Qed. +Proof. exact: Rabs_mult. Qed. Lemma Rleb_def x y : (Rleb x y) = (Rabs (y - x) == y - x). +Proof. apply/(sameP (RlebP x y))/(iffP idP)=> [/eqP H| /Rle_minus H]. apply: Rminus_le; rewrite -Ropp_minus_distr. apply/Rge_le/Ropp_0_le_ge_contravar. @@ -214,6 +219,7 @@ by apply/Ropp_0_ge_le_contravar/Rle_ge. Qed. Lemma Rltb_def x y : (Rltb x y) = (y != x) && (Rleb x y). +Proof. apply/(sameP (RltbP x y))/(iffP idP). case/andP=> /eqP H /RlebP/Rle_not_gt H2. by case: (Rtotal_order x y)=> // [][] // /esym. diff --git a/theories/cantor.v b/theories/cantor.v index 308447c4b9..51cb0a9afe 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -6,17 +6,32 @@ From mathcomp Require Import cardinality. Require Import reals signed topology. From HB Require Import structures. -(******************************************************************************) -(* The Cantor Space and Applications *) +(***markdown*******************************************************************) +(* # The Cantor Space and Applications *) (* *) (* This file develops the theory of the Cantor space, that is bool^nat with *) (* the product topology. The two main theorems proved here are *) (* homeomorphism_cantor_like, and cantor_surj, a.k.a. Alexandroff-Hausdorff. *) (* *) +(* ``` *) (* cantor_space == the Cantor space, with its canonical metric *) (* cantor_like T == perfect + compact + hausdroff + zero dimensional *) (* pointed_discrete T == equips T with the discrete topology *) (* tree_of T == builds a topological tree with levels (T n) *) +(* ``` *) +(* *) +(* The overall goal of the next few sections is to prove that *) +(* Every compact metric space `T` is the image of the Cantor space. *) +(* The overall proof will build two continuous functions *) +(* Cantor space -> a bespoke tree for `T` -> `T` *) +(* *) +(* The proof is in 4 parts: *) +(* - Part 1: Some generic machinery about continuous functions from trees. *) +(* - Part 2: All cantor-like spaces are homeomorphic to the Cantor space. *) +(* (an application of part 1) *) +(* - Part 3: Finitely branching trees are Cantor-like. *) +(* - Part 4: Every compact metric space has a finitely branching tree with *) +(* a continuous surjection. (a second application of part 1) *) (* *) (******************************************************************************) @@ -62,29 +77,20 @@ split. - exact: cantor_zero_dimensional. Qed. -(* The overall goal of the next few sections is to prove that - Every compact metric space `T` is the image of the Cantor space. - The overall proof will build two continuous functions - Cantor space -> a bespoke tree for `T` -> `T` - The proof is in 4 parts. - - Part 1: Some generic machinery about continuous functions from trees. - Part 2: All cantor-like spaces are homeomorphic to the Cantor space. - (an application of part 1) - Part 3: Finitely branching trees are Cantor-like. - Part 4: Every compact metric space has a finitely branching tree with - a continuous surjection. (a second application of part 1) - - Part 1: - A tree here has countable levels, and nodes of type `K n` on the nth level. - Each level is in the 'discrete' topology, so the nodes are independent. - The goal is to build a map from branches to X. - 1. Each level of the tree corresponds to an approximation of `X`. - 2. Each level refines the previous approximation. - 3. Then each branch has a corresponding Cauchy filter. - 4. The overall function from branches to X is a continuous surjection. - 5. With an extra disjointness condition, this is also an injection -*) +(***markdown*******************************************************************) +(* ## Part 1 *) +(* *) +(* A tree here has countable levels, and nodes of type `K n` on the nth *) +(* level. *) +(* Each level is in the 'discrete' topology, so the nodes are independent. *) +(* The goal is to build a map from branches to X. *) +(* 1. Each level of the tree corresponds to an approximation of `X`. *) +(* 2. Each level refines the previous approximation. *) +(* 3. Then each branch has a corresponding Cauchy filter. *) +(* 4. The overall function from branches to X is a continuous surjection. *) +(* 5. With an extra disjointness condition, this is also an injection *) +(* *) +(******************************************************************************) Section topological_trees. Context {K : nat -> topologicalType} {X : topologicalType} (refine_apx : forall n, set X -> K n -> set X) @@ -235,10 +241,11 @@ Qed. End topological_trees. -(* - Part 2: We can use `tree_map_props` to build a homeomorphism from the - cantor_space to a Cantor-like space T. -*) +(***markdown*******************************************************************) +(* ## Part 2 *) +(* We can use `tree_map_props` to build a homeomorphism from the *) +(* cantor_space to a Cantor-like space T. *) +(******************************************************************************) Section TreeStructure. Context {R : realType} {T : pseudoMetricType R}. @@ -332,7 +339,9 @@ Qed. End TreeStructure. -(* Part 3: Finitely branching trees are Cantor-like *) +(***markdown*******************************************************************) +(* ## Part 3: Finitely branching trees are Cantor-like *) +(******************************************************************************) Section FinitelyBranchingTrees. Context {R : realType}. @@ -366,7 +375,9 @@ End FinitelyBranchingTrees. Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope. -(* Part 4: Building a finitely branching tree to cover `T` *) +(***markdown*******************************************************************) +(* ## Part 4: Building a finitely branching tree to cover `T` *) +(******************************************************************************) Section alexandroff_hausdorff. Context {R : realType} {T : pseudoMetricType R}. @@ -525,7 +536,7 @@ Qed. End two_pointed. -(* The Alexandroff-Hausdorff theorem*) +(** The Alexandroff-Hausdorff theorem *) Theorem cantor_surj : exists f : {surj [set: cantor_space] >-> [set: T]}, continuous f. Proof. diff --git a/theories/charge.v b/theories/charge.v index f1cebbc9f2..1f629daaff 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -7,15 +7,16 @@ From HB Require Import structures. Require Import reals ereal signed topology numfun normedtype sequences. Require Import esum measure realfun lebesgue_measure lebesgue_integral. -(******************************************************************************) -(* Charges *) +(***markdown*******************************************************************) +(* # Charges *) (* *) (* NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. *) (* *) (* This file contains a formalization of charges (a.k.a. signed measures) and *) (* their theory (Hahn decomposition theorem, etc.). *) (* *) -(* * Structures for functions on classes of sets *) +(* ## Structures for functions on classes of sets *) +(* ``` *) (* {additive_charge set T -> \bar R} == notation for additive charges where *) (* T is a semiring of sets and R is a *) (* numFieldType *) @@ -25,8 +26,10 @@ Require Import esum measure realfun lebesgue_measure lebesgue_integral. (* The HB class is Charge. *) (* isCharge == factory corresponding to the "textbook *) (* definition" of charges *) +(* ``` *) (* *) -(* * Instances of mathematical structures *) +(* ## Instances of mathematical structures *) +(* ``` *) (* measure_of_charge nu nu0 == measure corresponding to the charge nu, nu0 *) (* is a proof that nu is non-negative *) (* crestr nu mD == restriction of the charge nu to the domain D *) @@ -35,8 +38,11 @@ Require Import esum measure realfun lebesgue_measure lebesgue_integral. (* non-measurable sets *) (* czero == zero charge *) (* cscale r nu == charge nu scaled by a factor r : R *) +(* ``` *) (* *) -(* * Theory *) +(* ## Theory *) +(* ``` *) + (* nu.-positive_set P == P is a positive set with nu a charge *) (* nu.-negative_set N == N is a negative set with nu a charge *) (* hahn_decomposition nu P N == the full set can be decomposed in P and N, *) @@ -50,6 +56,7 @@ Require Import esum measure realfun lebesgue_measure lebesgue_integral. (* decomposition nuPN: hahn_decomposition nu P N *) (* 'd nu '/d mu == Radon-Nikodym derivative of nu w.r.t. mu *) (* (the scope is charge_scope) *) +(* ``` *) (* *) (******************************************************************************) diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v index 9ab6dd84ef..1e38de9579 100644 --- a/theories/constructive_ereal.v +++ b/theories/constructive_ereal.v @@ -13,18 +13,18 @@ From mathcomp Require Import all_ssreflect all_algebra finmap. From mathcomp Require Import mathcomp_extra. Require Import signed. -(******************************************************************************) -(* Extended real numbers *) +(***markdown*******************************************************************) +(* # Extended real numbers $\overline{R}$ *) (* *) -(* Given a type R for numbers, \bar R is the type R extended with symbols -oo *) -(* and +oo (notation scope: %E), suitable to represent extended real numbers. *) -(* When R is a numDomainType, \bar R is equipped with a canonical porderType *) -(* and operations for addition/opposite. When R is a realDomainType, \bar R *) -(* is equipped with a Canonical orderType. *) +(* Given a type R for numbers, \bar R is the type R extended with symbols *) +(* -oo and +oo (notation scope: %E), suitable to represent extended real *) +(* numbers. When R is a numDomainType, \bar R is equipped with a canonical *) +(* porderType and operations for addition/opposite. When R is a *) +(* realDomainType, \bar R is equipped with a Canonical orderType. *) (* *) (* Naming convention: in definition/lemma identifiers, "e" stands for an *) (* extended number and "y" and "Ny" for +oo ad -oo respectively. *) -(* *) +(* ``` *) (* \bar R == coproduct of R and {+oo, -oo}; *) (* notation for extended (R:Type) *) (* r%:E == injects real numbers into \bar R *) @@ -48,22 +48,26 @@ Require Import signed. (* (\sum_(i in A) f i)%E == bigop-like notation in scope %E *) (* maxe x y, mine x y == notation for the maximum/minimum of two *) (* extended real numbers *) +(* ``` *) (* *) -(* Signed extended real numbers: *) +(* ## Signed extended real numbers *) +(* ``` *) (* {posnum \bar R} == interface type for elements in \bar R that are *) (* positive, c.f., signed.v, notation in scope %E *) (* {nonneg \bar R} == interface types for elements in \bar R that are *) (* non-negative, c.f. signed.v, notation in scope %E *) (* x%:pos == explicitly casts x to {posnum \bar R}, in scope %E *) (* x%:nng == explicitly casts x to {nonneg \bar R}, in scope %E *) +(* ``` *) (* *) -(* Topology of extended real numbers: *) +(* ## Topology of extended real numbers *) +(* ``` *) (* contract == order-preserving bijective function *) (* from extended real numbers to [-1; 1] *) (* expand == function from real numbers to extended *) (* real numbers that cancels contract in *) (* [-1; 1] *) -(* *) +(* ``` *) (******************************************************************************) Set Implicit Arguments. diff --git a/theories/convex.v b/theories/convex.v index 7b4047c6c0..f57be77624 100644 --- a/theories/convex.v +++ b/theories/convex.v @@ -7,15 +7,18 @@ Require Import ereal reals signed topology prodnormedzmodule normedtype derive. Require Import realfun itv. From HB Require Import structures. -(******************************************************************************) -(* Convexity *) +(***markdown*******************************************************************) +(* # Convexity *) (* *) (* This file provides a small account of convexity using convex spaces, to be *) (* completed with material from infotheo. *) (* *) +(* ``` *) (* isConvexSpace R T == interface for convex spaces *) (* ConvexSpace R == structure of convex space *) (* a <| t |> b == convexity operator *) +(* ``` *) +(* *) (* E : lmodType R with R : realDomainType and R : realDomainType are shown to *) (* be convex spaces *) (* *) diff --git a/theories/derive.v b/theories/derive.v index 3a3bbb626e..64e73aa843 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -3,7 +3,9 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. Require Import reals signed topology prodnormedzmodule normedtype landau forms. -(******************************************************************************) +(***markdown*******************************************************************) +(* # Differentiation *) +(* *) (* This file provides a theory of differentiation. It includes the standard *) (* rules of differentiation (differential of a sum, of a product, of *) (* exponentiation, of the inverse, etc.) as well as standard theorems (the *) @@ -11,6 +13,7 @@ Require Import reals signed topology prodnormedzmodule normedtype landau forms. (* *) (* Parsable notations (in all of the following, f is not supposed to be *) (* differentiable): *) +(* ``` *) (* 'd f x == the differential of a function f at a point x *) (* differentiable f x == the function f is differentiable at a point x *) (* 'J f x == the Jacobian of f at a point x *) @@ -20,6 +23,7 @@ Require Import reals signed topology prodnormedzmodule normedtype landau forms. (* and R : numFieldType *) (* f^`() == the derivative of f of domain R *) (* f^`(n) == the nth derivative of f of domain R *) +(* ``` *) (******************************************************************************) Set Implicit Arguments. diff --git a/theories/ereal.v b/theories/ereal.v index a249452e7d..37f97d4159 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -11,27 +11,31 @@ From mathcomp Require Import fsbigop cardinality set_interval. Require Import reals signed topology. Require Export constructive_ereal. -(******************************************************************************) -(* Extended real numbers, classical part *) +(***markdown*******************************************************************) +(* # Extended real numbers, classical part ($\overline{\mathbb{R}}$) *) (* *) (* This is an addition to the file constructive_ereal.v with classical logic *) (* elements. *) -(* *) +(* ``` *) (* (\sum_(i \in A) f i)%E == finitely supported sum, see fsbigop.v *) (* *) (* ereal_sup E == supremum of E *) (* ereal_inf E == infimum of E *) (* ereal_supremums_neq0 S == S has a supremum *) +(* ``` *) (* *) -(* Topology of extended real numbers: *) +(* ## Topology of extended real numbers *) +(* ``` *) (* ereal_topologicalType R == topology for extended real numbers over *) (* R, a realFieldType *) (* ereal_pseudoMetricType R == pseudometric space for extended reals *) (* over R where is a realFieldType; the *) (* distance between x and y is defined by *) (* `|contract x - contract y| *) +(* ``` *) (* *) -(* Filters: *) +(* ## Filters *) +(* ``` *) (* ereal_dnbhs x == filter on extended real numbers that *) (* corresponds to the deleted neighborhood *) (* x^' if x is a real number and to *) @@ -41,6 +45,7 @@ Require Export constructive_ereal. (* replaced with nbhs. *) (* ereal_loc_seq x == sequence that converges to x in the set *) (* of extended real numbers. *) +(* ``` *) (* *) (******************************************************************************) diff --git a/theories/esum.v b/theories/esum.v index c4498e8cf0..5c26a91604 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -4,12 +4,13 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop. Require Import reals ereal signed topology sequences normedtype numfun. -(******************************************************************************) -(* Summation over classical sets *) +(***markdown*******************************************************************) +(* # Summation over classical sets *) (* *) (* This file provides a definition of sum over classical sets and a few *) (* lemmas in particular for the case of sums of non-negative terms. *) (* *) +(* ``` *) (* fsets S == the set of finite sets (fset) included in S *) (* \esum_(i in I) f i == summation of non-negative extended real numbers over *) (* classical sets; I is a classical set and f is a *) @@ -17,6 +18,7 @@ Require Import reals ereal signed topology sequences normedtype numfun. (* reals; it is 0 if I = set0 and sup(\sum_A a) where A *) (* is a finite set included in I o.w. *) (* summable D f := \esum_(x in D) `| f x | < +oo *) +(* ``` *) (* *) (******************************************************************************) diff --git a/theories/exp.v b/theories/exp.v index 8290ad844a..b274b5dca7 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -7,15 +7,17 @@ Require Import reals ereal. Require Import signed topology normedtype landau sequences derive realfun. Require Import itv convex. -(******************************************************************************) -(* Theory of exponential/logarithm functions *) +(***markdown*******************************************************************) +(* # Theory of exponential/logarithm functions *) (* *) (* This file defines exponential and logarithm functions and develops their *) (* theory. *) (* *) -(* * Differentiability of series (Section PseriesDiff) *) -(* This formalization is inspired by HOL-Light (transc.ml). This part is *) -(* temporary: it should be subsumed by a proper theory of power series. *) +(* ## Differentiability of series (Section PseriesDiff) *) +(* *) +(* This formalization is inspired by HOL-Light (transc.ml). This part is *) +(* temporary: it should be subsumed by a proper theory of power series. *) +(* ``` *) (* pseries f x == [series f n * x ^ n]_n *) (* pseries_diffs f i == (i + 1) * f (i + 1) *) (* *) @@ -27,6 +29,7 @@ Require Import itv convex. (* of type realType *) (* e `^?(r +? s) == validity condition for the distributivity of *) (* the power of the addition, in ereal_scope *) +(* ``` *) (* *) (******************************************************************************) diff --git a/theories/forms.v b/theories/forms.v index 881a498b61..59f3193927 100644 --- a/theories/forms.v +++ b/theories/forms.v @@ -6,7 +6,10 @@ From mathcomp Require Import fieldext. From mathcomp Require Import vector. -(* From mathcomp Require classfun. *) +(***markdown*******************************************************************) +(* # Bilinear forms *) +(* (undocumented) *) +(******************************************************************************) Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/hoelder.v b/theories/hoelder.v index 349535838c..d82b1b49f6 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -7,13 +7,14 @@ Require Import signed reals ereal topology normedtype sequences real_interval. Require Import esum measure lebesgue_measure lebesgue_integral numfun exp. Require Import convex itv. -(******************************************************************************) -(* Hoelder's Inequality *) +(***markdown*******************************************************************) +(* # Hoelder's Inequality *) (* *) (* This file provides Hoelder's inequality. *) -(* *) +(* ``` *) (* 'N[mu]_p[f] := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1 *) (* The corresponding definition is Lnorm. *) +(* ``` *) (* *) (******************************************************************************) diff --git a/theories/itv.v b/theories/itv.v index e8630b0deb..b912ed1904 100644 --- a/theories/itv.v +++ b/theories/itv.v @@ -5,7 +5,9 @@ From mathcomp Require Import interval. From mathcomp Require Import mathcomp_extra boolp. Require Import signed. -(******************************************************************************) +(***markdown*******************************************************************) +(* # Numbers within an intervel *) +(* *) (* This file develops tools to make the manipulation of numbers within *) (* a known interval easier, thanks to canonical structures. This adds types *) (* like {itv R & `[a, b]}, a notation e%:itv that infers an enclosing *) @@ -14,7 +16,8 @@ Require Import signed. (* For instance, x : {i01 R}, we have (1 - x%:inum)%:itv : {i01 R} *) (* automatically inferred. *) (* *) -(* * types for values within known interval *) +(* ## types for values within known interval *) +(* ``` *) (* {i01 R} == interface type for elements in R that live in `[0, 1]; *) (* R must have a numDomainType structure. *) (* Allows to solve automatically goals of the form x >= 0 *) @@ -23,15 +26,19 @@ Require Import signed. (* {itv R & i} == more generic type of values in interval i : interval int *) (* R must have a numDomainType structure. This type is shown *) (* to be a porderType. *) +(* ``` *) (* *) -(* * casts from/to values within known interval *) +(* ## casts from/to values within known interval *) +(* ``` *) (* x%:itv == explicitly casts x to the most precise known {itv R & i} *) (* according to existing canonical instances. *) (* x%:i01 == explicitly casts x to {i01 R} according to existing *) (* canonical instances. *) (* x%:inum == explicit cast from {itv R & i} to R. *) +(* ``` *) (* *) -(* * sign proofs *) +(* ## sign proofs *) +(* ``` *) (* [itv of x] == proof that x is in interval inferred by x%:itv *) (* [lb of x] == proof that lb < x or lb <= x with lb the lower bound *) (* inferred by x%:itv *) @@ -39,15 +46,18 @@ Require Import signed. (* inferred by x%:itv *) (* [lbe of x] == proof that lb <= x *) (* [ube of x] == proof that x <= ub *) +(* ``` *) (* *) -(* * constructors *) +(* ## constructors *) +(* ``` *) (* ItvNum xin == builds a {itv R & i} from a proof xin : x \in i *) (* where x : R *) +(* ``` *) (* *) -(* --> A number of canonical instances are provided for common operations, if *) +(* A number of canonical instances are provided for common operations, if *) (* your favorite operator is missing, look below for examples on how to add *) (* the appropriate Canonical. *) -(* --> Canonical instances are also provided according to types, as a *) +(* Canonical instances are also provided according to types, as a *) (* fallback when no known operator appears in the expression. Look to *) (* itv_top_typ below for an example on how to add your favorite type. *) (******************************************************************************) @@ -849,12 +859,15 @@ Variable R : numDomainType. Variable x : {i01 R}. Goal 0%:i01 = 1%:i01 :> {i01 R}. +Proof. Abort. Goal (- x%:inum)%:itv = (- x%:inum)%:itv :> {itv R & `[-1, 0]}. +Proof. Abort. Goal (1 - x%:inum)%:i01 = x. +Proof. Abort. End Test1. @@ -865,6 +878,7 @@ Variable R : realDomainType. Variable x y : {i01 R}. Goal (x%:inum * y%:inum)%:i01 = x%:inum%:i01. +Proof. Abort. End Test2. diff --git a/theories/kernel.v b/theories/kernel.v index 39950c0943..954ca5677b 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -6,14 +6,18 @@ From mathcomp Require Import cardinality fsbigop. Require Import reals ereal signed topology normedtype sequences esum measure. Require Import numfun lebesgue_measure lebesgue_integral. -(******************************************************************************) -(* Kernels *) +(***markdown*******************************************************************) +(* # Kernels *) (* *) (* This file provides a formation of kernels, s-finite kernels, finite *) (* kernels, subprobability kernels, and probability kernels. The main *) (* formalized result is the fact that s-finite kernels are stable by *) (* composition. *) +(* Reference: *) +(* - R. Affeldt, C. Cohen, A. Saito. Semantics of probabilistic programs *) +(* using s-finite kernels in Coq. CPP 2023 *) (* *) +(* ``` *) (* R.-ker X ~> Y == kernel from X to Y where X and Y are of type *) (* measurableType *) (* The HB class is Kernel. *) @@ -39,9 +43,8 @@ Require Import numfun lebesgue_measure lebesgue_integral. (* kprobability m == kernel defined by a probability measure *) (* kadd k1 k2 == lifting of the addition of measures to kernels *) (* l \; k == composition of kernels *) +(* ``` *) (* *) -(* ref: R. Affeldt, C. Cohen, A. Saito, Semantics of probabilistic programs *) -(* using s-finite kernels in Coq, CPP 2023 *) (******************************************************************************) Set Implicit Arguments. diff --git a/theories/landau.v b/theories/landau.v index 054abf4c61..eb03faeb02 100644 --- a/theories/landau.v +++ b/theories/landau.v @@ -3,23 +3,19 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. Require Import ereal reals signed topology normedtype prodnormedzmodule. -(******************************************************************************) -(* BACHMANN-LANDAU NOTATIONS : BIG AND LITTLE O *) -(******************************************************************************) -(******************************************************************************) -(* F is a filter, K is an absRingType and V W X Y Z are normed spaces over K *) -(* alternatively, K can be equal to the reals R (from the standard library *) -(* for now) *) +(***markdown*******************************************************************) +(* # Bachmann-Landau notations: $f=o(e)$, $f=O(e)$ *) +(* *) (* This library is very asymmetric, in multiple respects: *) (* - most rewrite rules can only be rewritten from left to right. *) -(* e.g. an equation 'o_F f = 'O_G g can be used only from LEFT TO RIGHT *) +(* e.g., an equation 'o_F f = 'O_G g can be used only from LEFT TO RIGHT *) (* - conversely most small 'o_F f in your goal are very specific, *) (* only 'a_F f is mutable *) (* *) -(* - most notations are either parse only or print only. *) -(* Indeed all the 'O_F notations contain a function which is NOT displayed. *) -(* This might be confusing as sometimes you might get 'O_F g = 'O_F g *) -(* and not be able to solve by reflexivity. *) +(* Most notations are either parse only or print only. *) +(* Indeed all the 'O_F notations contain a function which is NOT displayed. *) +(* This might be confusing as sometimes you might get 'O_F g = 'O_F g *) +(* and not be able to solve by reflexivity. *) (* - In order to have a look at the hidden function, rewrite showo. *) (* - Do not use showo during a normal proof. *) (* - All theorems should be stated so that when an impossible reflexivity *) @@ -27,12 +23,15 @@ Require Import ereal reals signed topology normedtype prodnormedzmodule. (* know you should use eqOE in order to generalize your 'O_F g *) (* to an arbitrary 'O_F g *) (* *) +(* In this file, F is a filter and V W X Y Z are normed spaces over K. *) +(* *) (* To prove that f is a bigO of g near F, you should go back to filter *) (* reasoning only as a last resort. To do so, use the view eqOP. Similarly, *) (* you can use eqaddOP to prove that f is equal to g plus a bigO of e near F *) (* using filter reasoning. *) (* *) -(* Parsable notations: *) +(* ## Parsable notations *) +(* ``` *) (* [bigO of f] == recovers the canonical structure of big-o of f *) (* expands to itself *) (* f =O_F h == f is a bigO of h near F, *) @@ -56,37 +55,44 @@ Require Import ereal reals signed topology normedtype prodnormedzmodule. (* 'O == pattern to match a bigO with a generic F *) (* f x =O_(x \near F) e x == alternative way of stating f =O_F e (provably *) (* equal using the lemma eqOEx *) +(* ``` *) +(* *) +(* WARNING: The piece of syntax "=O_(" is only valid in the syntax *) +(* "=O_(x \near F)", not in the syntax "=O_(x : U)". *) (* *) -(* Printing only notations: *) +(* ## Printing only notations: *) +(* ``` *) (* {O_F f} == the type of functions that are a bigO of f near F *) (* 'a_O_F f == an existential bigO, must come from (apply: eqOE) *) (* 'O_F f == a generic bigO, with a function you should not rely on, *) (* but there is no way you can use eqOE on it. *) +(* ``` *) +(* The former works exactly same by with littleo instead of bigO. *) (* *) -(* The former works exactly the same by with littleo instead of bigO. *) -(* *) -(* Asymptotic equivalence: *) +(* ## Asymptotic equivalence *) +(* ``` *) (* f ~_ F g == function f is asymptotically equivalent to *) (* function g for filter F, i.e., f = g +o_ F g *) (* f ~~_ F g == f == g +o_ F g (i.e., as a boolean relation) *) -(* --> asymptotic equivalence proved to be an equivalence relation *) +(* ``` *) +(* Asymptotic equivalence is proved to be an equivalence relation. *) (* *) -(* Big-Omega and big-Theta notations on the model of bigO and littleo: *) -(* {Omega_F f} == the type of functions that are a big Omega of f near F *) -(* [bigOmega of f] == recovers the canonical structure of big-Omega of f *) -(* [Omega_F e of f] == returns a function with a bigOmega canonical structure *) -(* provably equal to f if f is indeed a bigOmega of e *) -(* or e otherwise *) +(* ## Big-Omega and big-Theta notations on the model of bigO and littleo *) +(* ``` *) +(* {Omega_F f} == the type of functions that are a big Omega of f *) +(* near F *) +(* [bigOmega of f] == recovers the canonical structure of big-Omega of f *) +(* [Omega_F e of f] == returns a function with a bigOmega canonical *) +(* structure provably equal to f if f is indeed a *) +(* bigOmega of e or e otherwise *) (* f \is 'Omega_F(e) == f : T -> V is a bigOmega of e : T -> W near F *) (* f =Omega_F h == f : T -> V is a bigOmega of h : T -> V near F *) -(* --> lemmas: relation with big-O, transitivity, product of functions, etc. *) +(* ``` *) +(* Lemmas: relation with big-O, transitivity, product of functions, etc. *) (* *) (* Similar notations available for big-Theta. *) -(* --> lemmas: relations with big-O and big-Omega, reflexivity, symmetry, *) -(* transitivity, product of functions, etc. *) -(* *) -(* WARNING: The piece of syntax "=O_(" is only valid in the syntax *) -(* "=O_(x \near F)", not in the syntax "=O_(x : U)". *) +(* Lemmas: relations with big-O and big-Omega, reflexivity, symmetry, *) +(* transitivity, product of functions, etc. *) (* *) (******************************************************************************) Set Implicit Arguments. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 2fd8600015..2b60b1866b 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -6,8 +6,8 @@ From mathcomp Require Import cardinality fsbigop . Require Import signed reals ereal topology normedtype sequences real_interval. Require Import esum measure lebesgue_measure numfun. -(******************************************************************************) -(* Lebesgue Integral *) +(***markdown*******************************************************************) +(* # Lebesgue Integral *) (* *) (* This file contains a formalization of the Lebesgue integral. It starts *) (* with simple functions and their integral, provides basic operations *) @@ -16,12 +16,20 @@ Require Import esum measure lebesgue_measure numfun. (* measurable functions, proves the approximation theorem, the properties of *) (* their integral (semi-linearity, non-decreasingness), the monotone *) (* convergence theorem, and Fatou's lemma. Finally, it proves the linearity *) -(* properties of the integral, the dominated convergence theorem and Fubini's *) -(* theorem. *) +(* properties of the integral, the dominated convergence theorem and *) +(* Fubini's theorem, etc. *) +(* *) +(* Main notation: *) +(* | Coq notation | Meaning | *) +(* |-----------------------|---------------------------------| *) +(* | \int[mu]_(x in D) f x | $\int_{x\in D} f(x)\mathbf{d}x$ | *) +(* | \int[mu]_x f x | $\int_x f(x)\mathbf{d}x$ | *) (* *) (* Main reference: *) (* - Daniel Li, Intégration et applications, 2016 *) (* *) +(* Detailed contents: *) +(* ```` *) (* {mfun T >-> R} == type of real-valued measurable functions *) (* {sfun T >-> R} == type of simple functions *) (* {nnsfun T >-> R} == type of non-negative simple functions *) @@ -45,6 +53,7 @@ Require Import esum measure lebesgue_measure numfun. (* m1 \x^ m2 == product measure over T1 * T2, m2 is a measure *) (* measure over T1, and m1 is a sigma finite *) (* measure over T2 *) +(* ```` *) (* *) (******************************************************************************) @@ -597,8 +606,9 @@ by apply: (mulemu_ge0 (fun x => f @^-1` [set x])); exact: preimage_nnfun0. Qed. End mulem_ge0. -(* Definition of Simple Integrals *) -(**********************************) +(***markdown*******************************************************************) +(* ## Definition of Simple Integrals *) +(******************************************************************************) Section simple_fun_raw_integral. Local Open Scope ereal_scope. @@ -4388,8 +4398,8 @@ Qed. End integral_ae_eq. -(******************************************************************************) -(* * product measure *) +(***markdown*******************************************************************) +(* ## Product measure *) (******************************************************************************) Section measurable_section. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 594b396d66..a48abe4e55 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -8,23 +8,29 @@ From HB Require Import structures. Require Import sequences esum measure real_interval realfun exp. Require Export lebesgue_stieltjes_measure. -(******************************************************************************) -(* Lebesgue Measure *) +(***markdown*******************************************************************) +(* # Lebesgue Measure *) (* *) (* This file contains a formalization of the Lebesgue measure using the *) -(* Measure Extension theorem from measure.v and further develops the theory *) -(* of measurable functions. *) +(* Measure Extension theorem from measure.v, further develops the theory of *) +(* of measurable functions, and prove properties of the Lebesgue measure *) +(* such as Vitali's covering lemma (infinite case), i.e., given a Vitali *) +(* cover $V$ of $A$, there exists a countable subcollection $D \subseteq V$ *) +(* of pairwise disjoint closed balls such that *) +(* $\lambda(A \setminus \bigcup_k D_k) = 0$. *) (* *) -(* Main reference: *) +(* Main references: *) (* - Daniel Li, Intégration et applications, 2016 *) (* - Achim Klenke, Probability Theory 2nd edition, 2014 *) (* *) +(* ``` *) (* lebesgue_measure == the Lebesgue measure *) (* ps_infty == inductive definition of the powerset *) (* {0, {-oo}, {+oo}, {-oo,+oo}} *) (* emeasurable G == sigma-algebra over \bar R built out of the *) (* measurables G of a sigma-algebra over R *) (* elebesgue_measure == the Lebesgue measure extended to \bar R *) +(* ``` *) (* *) (* The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens provide proofs *) (* of equivalence between the sigma-algebra generated by list of intervals *) @@ -35,8 +41,10 @@ Require Export lebesgue_stieltjes_measure. (* of equivalence between emeasurable and the sigma-algebras generated open *) (* rays and closed rays. *) (* *) +(* ``` *) (* vitali_cover A B V == V is a Vitali cover of A, here B is a *) (* collection of non-empty closed balls *) +(* ``` *) (* *) (******************************************************************************) diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index 4414860f1c..01b4644700 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -7,8 +7,8 @@ From mathcomp.classical Require Import functions fsbigop cardinality. Require Import reals ereal signed topology numfun normedtype sequences esum. Require Import real_interval measure realfun. -(******************************************************************************) -(* Lebesgue Stieltjes Measure *) +(***markdown*******************************************************************) +(* # Lebesgue Stieltjes Measure *) (* *) (* This file contains a formalization of the Lebesgue-Stieltjes measure using *) (* the Measure Extension theorem from measure.v. *) @@ -16,6 +16,7 @@ Require Import real_interval measure realfun. (* Reference: *) (* - Achim Klenke, Probability Theory 2nd edition, 2014 *) (* *) +(* ``` *) (* right_continuous f == the function f is right-continuous *) (* cumulative R == type of non-decreasing, right-continuous *) (* functions (with R : numFieldType) *) @@ -30,6 +31,7 @@ Require Import real_interval measure realfun. (* numbers A being delimited by a and b *) (* lebesgue_stieltjes_measure f == Lebesgue-Stieltjes measure for f *) (* f is a cumulative function. *) +(* ``` *) (* *) (******************************************************************************) diff --git a/theories/measure.v b/theories/measure.v index 1dfdeecfa3..80bfdb7cff 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -5,20 +5,26 @@ From mathcomp Require Import cardinality fsbigop . Require Import reals ereal signed topology normedtype sequences esum numfun. From HB Require Import structures. -(******************************************************************************) -(* Measure Theory *) +(***markdown*******************************************************************) +(* # Measure Theory *) (* *) (* NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. *) (* *) (* This files provides a formalization of the basics of measure theory. This *) (* includes the formalization of mathematical structures and of measures, as *) -(* well as standard theorems such as the Measure Extension theorem. *) +(* well as standard theorems such as 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\}.$ *) (* *) -(* References: *) -(* - Daniel Li, Intégration et applications, 2016 *) -(* - Achim Klenke, Probability Theory 2nd edition, 2014 *) +(* Reference: *) +(* - 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 *) +(* ## 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. *) @@ -33,8 +39,10 @@ From HB Require Import structures. (* The HB class is AlgebraOfsets. *) (* measurableType == the type of sigma-algebras *) (* The HB class is Measurable. *) +(* ``` *) (* *) -(* * Instances of mathematical structures *) +(* ## Instances of mathematical structures *) +(* ``` *) (* discrete_measurable_unit == the measurableType corresponding to *) (* [set: set unit] *) (* discrete_measurable_bool == the measurableType corresponding to *) @@ -57,10 +65,14 @@ From HB Require Import structures. (* salgebraType G == the measurableType corresponding to <> *) (* This is an HB alias. *) (* mu .-cara.-measurable == sigma-algebra of Caratheodory measurable sets *) +(* ``` *) +(* *) +(* ## Structures for functions on classes of sets *) (* *) -(* * Structures for functions on classes of sets *) -(* (There are a few details about mixins/factories to highlight *) -(* implementations peculiarities.) *) +(* A few details about mixins/factories to highlight implementations *) +(* peculiarities: *) +(* *) +(* ``` *) (* {content set T -> \bar R} == type of contents *) (* T is expected to be a semiring of sets and R a *) (* numFieldType. *) @@ -113,8 +125,10 @@ From HB Require Import structures. (* of elements of type T : Type where R is *) (* expected to be a numFieldType *) (* The HB class is OuterMeasure. *) +(* ``` *) (* *) -(* * Instances of measures *) +(* ## 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 *) @@ -140,8 +154,10 @@ From HB Require Import structures. (* countable union *) (* trivIset_closed G == the set of sets G is closed under pairwise-disjoint *) (* countable union *) +(* ``` *) (* *) -(* * Hierarchy of s-finite, sigma-finite, finite measures: *) +(* ## 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 *) @@ -195,14 +211,20 @@ From HB Require Import structures. (* measure_is_complete mu == the measure mu is complete *) (* {ae mu, forall x, P x} == P holds almost everywhere for the measure mu, *) (* declared as an instance of the type of filters *) +(* ``` *) +(* *) +(* # Measure Extension Theorem *) (* *) -(* * From a premeasure to an outer measure (Measure Extension Theorem part 1) *) +(* 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): *) +(* ``` *) +(* From an outer measure to a measure (Measure Extension Theorem part 2): *) +(* ``` *) (* 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) *) @@ -213,12 +235,16 @@ From HB Require Import structures. (* measure. *) (* Remark: sets that are negligible for *) (* this measure are Caratheodory measurable. *) -(* * Measure Extension Theorem: *) +(* ``` *) +(* 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) *) +(* ``` *) (* *) -(* * Product of measurable spaces: *) +(* 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 *) @@ -226,10 +252,14 @@ From HB Require Import structures. (* (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 *) +(* ``` *) (* *) +(* Others: *) +(* ``` *) (* 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 *) (* measurableType and R is a realType *) +(* ``` *) (* *) (******************************************************************************) diff --git a/theories/normedtype.v b/theories/normedtype.v index 951ead23ef..c4505dc4fc 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -5,12 +5,19 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality set_interval Rstruct. Require Import ereal reals signed topology prodnormedzmodule. -(******************************************************************************) -(* This file extends the topological hierarchy with norm-related notions. *) +(***markdown*******************************************************************) +(* # Norm-related Notions *) (* *) +(* This file extends the topological hierarchy with norm-related notions. *) (* Note that balls in topology.v are not necessarily open, here they are. *) +(* We used these definitions to prove the intermediate value theorem and *) +(* the Heine-Borel theorem, which states that the compact sets of *) +(* $\mathbb{R}^n$ are the closed and bounded sets, Urysohn's lemma, Vitali's *) +(* covering lemmas (finite case), etc. *) +(* *) (* *) -(* * Normed Topological Abelian groups: *) +(* ## Normed Topological Abelian groups *) +(* ``` *) (* pseudoMetricNormedZmodType R == interface type for a normed topological *) (* Abelian group equipped with a norm *) (* PseudoMetricNormedZmodule.Mixin nb == builds the mixin for a normed *) @@ -18,8 +25,10 @@ Require Import ereal reals signed topology prodnormedzmodule. (* compatibility between the norm and *) (* balls; the carrier type must have a *) (* normed Zmodule over a numDomainType. *) +(* ``` *) (* *) -(* * Normed modules : *) +(* ## Normed modules *) +(* ``` *) (* normedModType K == interface type for a normed module *) (* structure over the numDomainType K. *) (* NormedModMixin normZ == builds the mixin for a normed module *) @@ -56,8 +65,10 @@ Require Import ereal reals signed topology prodnormedzmodule. (* maxr (f a) (f b)]%classic *) (* f @`] a , b [ := `]minr (f a) (f b), *) (* maxr (f a) (f b)[%classic *) +(* ``` *) (* *) -(* * Domination notations: *) +(* ## Domination notations *) +(* ``` *) (* dominated_by h k f F == `|f| <= k * `|h|, near F *) (* bounded_near f F == f is bounded near F *) (* [bounded f x | x in A] == f is bounded on A, ie F := globally A *) @@ -83,22 +94,24 @@ Require Import ereal reals signed topology prodnormedzmodule. (* Rhull A == the real interval hull of a set A *) (* shift x y == y + x *) (* center c := shift (- c) *) +(* ``` *) (* *) -(* * Complete normed modules : *) +(* ## Complete normed modules *) +(* ``` *) (* completeNormedModType K == interface type for a complete normed *) (* module structure over a realFieldType *) (* K. *) (* [completeNormedModType K of T] == clone of a canonical complete normed *) (* module structure over K on T. *) +(* ``` *) (* *) -(* * Filters : *) +(* ## Filters *) +(* ``` *) (* at_left x, at_right x == filters on real numbers for predicates *) (* s.t. nbhs holds on the left/right of x *) +(* ``` *) (* *) -(* --> We used these definitions to prove the intermediate value theorem and *) -(* the Heine-Borel theorem, which states that the compact sets of R^n are *) -(* the closed and bounded sets. *) -(* *) +(* ``` *) (* cpoint A == the center of the set A if it is an open ball *) (* radius A == the radius of the set A if it is an open ball *) (* Radius A has type {nonneg R} with R a numDomainType. *) @@ -107,6 +120,7 @@ Require Import ereal reals signed topology prodnormedzmodule. (* if A is an open ball and set0 o.w. *) (* vitali_collection_partition B V r n == subset of indices of V such the *) (* the ball B i has a radius between r/2^n+1 and r/2^n *) +(* ``` *) (* *) (******************************************************************************) @@ -409,8 +423,6 @@ Qed. #[global] Hint Extern 0 (ProperFilter _^') => (apply: Proper_dnbhs_numFieldType) : typeclass_instances. -(** * Some Topology on extended real numbers *) - Definition pinfty_nbhs (R : numFieldType) : set (set R) := fun P => exists M, M \is Num.real /\ forall x, M < x -> P x. Arguments pinfty_nbhs R : clear implicits. @@ -828,7 +840,9 @@ Lemma cvgenyP {R : realType} {T} {F : set (set T)} {FF : Filter F} (f : T -> nat (((f n)%:R : R)%:E @[n --> F] --> +oo%E) <-> (f @ F --> \oo). Proof. by rewrite cvgeryP cvgrnyP. Qed. -(** ** Modules with a norm *) +(***markdown*******************************************************************) +(* ## Modules with a norm *) +(******************************************************************************) Module NormedModule. @@ -1894,7 +1908,7 @@ Section open_closed_sets. in a numDomainType *) Variable R : realFieldType. -(** Some open sets of [R] *) +(** Some open sets of R *) Lemma open_lt (y : R) : open [set x : R| x < y]. Proof. move=> x /=; rewrite -subr_gt0 => yDx_gt0. exists (y - x) => // z. @@ -1929,10 +1943,9 @@ move: a b => [[]a|[]] [[]b|[]]// _ _. - by rewrite (_ : mkset _ = setT); [exact: openT | rewrite predeqE]. Qed. -(** Some closed sets of [R] *) +(** Some closed sets of R *) (* TODO: we can probably extend these results to numFieldType by adding a precondition that y \is Num.real *) - Lemma closed_le (y : R) : closed [set x : R | x <= y]. Proof. rewrite (_ : mkset _ = ~` [set x | x > y]); first exact: open_closedC. @@ -2800,8 +2813,7 @@ Proof. by move=> cf /cvg_eq->// e; rewrite subrr normr0. Qed. note="simply use the fact that `(x --> l) -> (x = l)`")] Notation continuous_cvg_dist := __deprecated__continuous_cvg_dist (only parsing). -(** ** Matrices *) - +(** Matrices: *) Section mx_norm. Variables (K : numDomainType) (m n : nat). Implicit Types x y : 'M[K]_(m, n). @@ -2921,8 +2933,7 @@ Canonical matrix_normedModType := End matrix_NormedModule. -(** ** Pairs *) - +(** Pairs: *) Section prod_PseudoMetricNormedZmodule. Context {K : numDomainType} {U V : pseudoMetricNormedZmodType K}. @@ -3013,8 +3024,8 @@ Arguments cvgr2dist_lt {_ _ _ _ _ F G FF FG}. note="use `fcvgr2dist_ltP` or a variant instead")] Notation cvg_dist2P := fcvgr2dist_ltP (only parsing). -(** Normed vector spaces have some continuous functions *) -(** that are in fact continuous on pseudoMetricNormedZmodType *) +(** Normed vector spaces have some continuous functions that are in fact +continuous on pseudoMetricNormedZmodType *) Section NVS_continuity_pseudoMetricNormedZmodType. Context {K : numFieldType} {V : pseudoMetricNormedZmodType K}. @@ -4694,9 +4705,9 @@ End CompleteNormedModule. Export CompleteNormedModule.Exports. -(** * Extended Types *) - -(** * The topology on real numbers *) +(***markdown*******************************************************************) +(* ## The topology on real numbers *) +(******************************************************************************) Lemma R_complete (R : realType) (F : set (set R)) : ProperFilter F -> cauchy F -> cvg F. Proof. @@ -5431,7 +5442,7 @@ End interval_realType. Section segment. Variable R : realType. -(** properties of segments in [R] *) +(** properties of segments in R *) Lemma segment_connected (a b : R) : connected `[a, b]. Proof. exact/connected_intervalP/interval_is_interval. Qed. @@ -5512,7 +5523,7 @@ apply/connected_intervalP/connected_continuous_connected => //. exact: segment_connected. Qed. -(** Local properties in [R] *) +(* Local properties in R *) (* Topology on [R]² *) @@ -5755,8 +5766,9 @@ have /mapP[j Hj ->] : `|v ord0 i| \in [seq `|v x.1 x.2| | x : 'I_1 * 'I_n.+1]. by rewrite [leRHS]/normr /= mx_normrE; apply/bigmax_geP; right => /=; exists j. Qed. - -(** * Some limits on real functions *) +(***markdown*******************************************************************) +(* ## Some limits on real functions *) +(******************************************************************************) Section Shift. diff --git a/theories/nsatz_realtype.v b/theories/nsatz_realtype.v index 00be33ae98..a91866301c 100644 --- a/theories/nsatz_realtype.v +++ b/theories/nsatz_realtype.v @@ -3,14 +3,15 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum. From mathcomp Require Import boolp. Require Import reals ereal. -(******************************************************************************) -(* nsatz for realType *) +(***markdown*******************************************************************) +(* # nsatz for realType *) (* *) (* This file registers the ring corresponding to the MathComp-Analysis type *) (* realType to the tactic nsatz of Coq. This enables some automation used for *) (* example in the file trigo.v. *) (* *) -(* ref: https://coq.inria.fr/refman/addendum/nsatz.html *) +(* Reference: *) +(* - https://coq.inria.fr/refman/addendum/nsatz.html *) (* *) (******************************************************************************) diff --git a/theories/numfun.v b/theories/numfun.v index 4e8db0caba..31ec96fa80 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -5,9 +5,12 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets fsbigop. From mathcomp Require Import functions cardinality set_interval. Require Import signed reals ereal topology normedtype sequences. -(******************************************************************************) +(***markdown*******************************************************************) +(* # Numerical functions *) +(* *) (* This file provides definitions and lemmas about numerical functions. *) (* *) +(* ``` *) (* {nnfun T >-> R} == type of non-negative functions *) (* f ^\+ == the function formed by the non-negative outputs *) (* of f (from a type to the type of extended real *) @@ -17,6 +20,7 @@ Require Import signed reals ereal topology normedtype sequences. (* of f and 0 o.w. *) (* rendered as f ⁻ with company-coq (U+207B) *) (* \1_ A == indicator function 1_A *) +(* ``` *) (* *) (******************************************************************************) diff --git a/theories/probability.v b/theories/probability.v index a61d3b1296..262b9fc589 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -8,12 +8,13 @@ Require Import exp numfun lebesgue_measure lebesgue_integral. Require Import reals ereal signed topology normedtype sequences esum measure. Require Import exp numfun lebesgue_measure lebesgue_integral. -(******************************************************************************) -(* Probability (experimental) *) +(***markdown*******************************************************************) +(* # Probability *) (* *) (* This file provides basic notions of probability theory. See measure.v for *) (* the type probability T R (a measure that sums to 1). *) (* *) +(* ``` *) (* {RV P >-> R} == real random variable: a measurable function from *) (* the measurableType of the probability P to R *) (* distribution X == measure image of P by X : {RV P -> R}, declared *) @@ -29,6 +30,7 @@ Require Import exp numfun lebesgue_measure lebesgue_integral. (* dRV_enum X == bijection between the domain and the range of X *) (* pmf X r := fine (P (X @^-1` [set r])) *) (* enum_prob X k == probability of the kth value in the range of X *) +(* ``` *) (* *) (******************************************************************************) @@ -683,6 +685,7 @@ Context d (T : measurableType d) (R : realType) (P : probability T R). Definition dRV_dom_enum (X : {dRV P >-> R}) : { B : set nat & {splitbij B >-> range X}}. +Proof. have /countable_bijP/cid[B] := @countable_range _ _ _ X. move/card_esym/ppcard_eqP/unsquash => f. exists B; exact: f. diff --git a/theories/real_interval.v b/theories/real_interval.v index b22f52486e..90ede435b0 100644 --- a/theories/real_interval.v +++ b/theories/real_interval.v @@ -6,9 +6,8 @@ From mathcomp Require Export set_interval. From HB Require Import structures. Require Import reals ereal signed topology normedtype sequences. -(******************************************************************************) -(* This files contains lemmas about sets and intervals on reals. *) -(* *) +(***markdown*******************************************************************) +(* # Sets and intervals on $\overline{\mathbb{R}}$ *) (******************************************************************************) Set Implicit Arguments. diff --git a/theories/realfun.v b/theories/realfun.v index b84a816cc0..50a3ceba8e 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -7,10 +7,13 @@ Require Import ereal reals signed topology prodnormedzmodule normedtype derive. Require Import real_interval. From HB Require Import structures. -(******************************************************************************) +(***markdown*******************************************************************) +(* # Real-valued functions over reals *) +(* *) (* This file provides properties of standard real-valued functions over real *) (* numbers (e.g., the continuity of the inverse of a continuous function). *) (* *) +(* ``` *) (* nondecreasing_fun f == the function f is non-decreasing *) (* nonincreasing_fun f == the function f is non-increasing *) (* increasing_fun f == the function f is (strictly) increasing *) @@ -18,6 +21,7 @@ From HB Require Import structures. (* *) (* derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and *) (* continuous up to the boundary *) +(* ``` *) (* *) (******************************************************************************) @@ -422,10 +426,9 @@ Section real_inverse_functions. Variable R : realType. Implicit Types (a b : R) (f g : R -> R). -(* This lemma should be used with caution. Generally `{within I, continuous f}` +(** This lemma should be used with caution. Generally `{within I, continuous f}` is what one would intend. So having `{in I, continuous f}` as a condition - may indicate potential issues at the endpoints of the interval. -*) + may indicate potential issues at the endpoints of the interval. *) Lemma continuous_subspace_itv (I : interval R) (f : R -> R) : {in I, continuous f} -> {within [set` I], continuous f}. Proof. @@ -567,8 +570,8 @@ move=> /(_ b a); rewrite !bound_itvE fafb. by move=> /(_ (ltW aLb) (ltW aLb)); rewrite lt_geF. Qed. -(* The condition "f a <= f b" is unnecessary because the last *) -(* interval condition is vacuously true otherwise. *) +(** The condition "f a <= f b" is unnecessary because the last + interval condition is vacuously true otherwise. *) Lemma segment_can_le a b f g : a <= b -> {within `[a, b], continuous f} -> {in `[a, b], cancel f g} -> @@ -595,7 +598,7 @@ Proof. by split=> x /=; rewrite oppr_itvcc. Qed. HB.instance Definition _ a b := itv_oppr_is_fun a b. End negation_itv. -(* The condition "f b <= f a" is unnecessary---see seg...increasing above *) +(** The condition "f b <= f a" is unnecessary---see seg...increasing above *) Lemma segment_can_ge a b f g : a <= b -> {within `[a, b], continuous f} -> {in `[a, b], cancel f g} -> diff --git a/theories/reals.v b/theories/reals.v index 2762e36dc3..b0dee262b8 100644 --- a/theories/reals.v +++ b/theories/reals.v @@ -5,24 +5,27 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -(******************************************************************************) -(* An axiomatization of real numbers *) +(***markdown*******************************************************************) +(* # An axiomatization of real numbers $\mathbb{R}$ *) (* *) (* This file provides a classical axiomatization of real numbers as a *) (* discrete real archimedean field with in particular a theory of floor and *) (* ceil. *) (* *) +(* ``` *) (* realType == type of real numbers *) (* sup A == where A : set R with R : realType, the supremum of A when *) (* it exists, 0 otherwise *) (* inf A := - sup (- A) *) +(* ``` *) (* *) (* The mixin corresponding to realType extends an archiFieldType with two *) (* properties: *) -(* - when sup A exists, it is an upper bound of A (lemma sup_upper_bound) *) -(* - when sup A exists, there exists an element x in A such that *) -(* sup A - eps < x for any 0 < eps (lemma sup_adherent) *) +(* - when sup A exists, it is an upper bound of A (lemma sup_upper_bound) *) +(* - when sup A exists, there exists an element x in A such that *) +(* sup A - eps < x for any 0 < eps (lemma sup_adherent) *) (* *) +(* ``` *) (* Rint == the set of real numbers that can be written as z%:~R, *) (* i.e., as an integer *) (* Rtoint r == r when r is an integer, 0 otherwise *) @@ -32,6 +35,7 @@ (* range1 x := [set y |x <= y < x + 1] *) (* Rceil x == the ceil of x as a real number, i.e., - Rfloor (- x) *) (* ceil x := - floor (- x) *) +(* ``` *) (* *) (******************************************************************************) @@ -315,6 +319,7 @@ Qed. Lemma Rint_ltr_addr1 (x y : R) : x \is a Rint -> y \is a Rint -> (x < y + 1) = (x <= y). +Proof. move=> /RintP[xi ->] /RintP[yi ->]; rewrite -{3}[1]mulr1z. by rewrite -intrD !(ltr_int, ler_int) ltz_addr1. Qed. diff --git a/theories/sequences.v b/theories/sequences.v index 3ab4bc4754..47deb45264 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -5,18 +5,20 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import set_interval. Require Import reals ereal signed topology normedtype landau. -(******************************************************************************) -(* Definitions and lemmas about sequences *) +(***markdown*******************************************************************) +(* # Definitions and lemmas about sequences *) (* *) (* The purpose of this file is to gather generic definitions and lemmas about *) (* sequences. *) -(* *) +(* ``` *) (* nondecreasing_seq u == the sequence u is non-decreasing *) (* nonincreasing_seq u == the sequence u is non-increasing *) (* increasing_seq u == the sequence u is (strictly) increasing *) (* decreasing_seq u == the sequence u is (strictly) decreasing *) +(* ``` *) (* *) -(* * About sequences of real numbers: *) +(* ## About sequences of real numbers *) +(* ``` *) (* [sequence u_n]_n == the sequence of general element u_n *) (* R ^nat == notation for the type of sequences, i.e., *) (* functions of type nat -> R *) @@ -38,13 +40,14 @@ Require Import reals ereal signed topology normedtype landau. (* exponential *) (* expR x == the exponential function defined on a realType *) (* is_cvg_series_exp_coeff == convergence of \sum_n^+oo x^n / n! *) -(* *) (* \sum_ F i == lim (fun n => (\sum_) F i)) where *) (* can be (i = n} *) (* sups u := [sequence sup (sdrop u n)]_n *) (* infs u := [sequence inf (sdrop u n)]_n *) @@ -77,6 +82,7 @@ Require Import reals ereal signed topology normedtype landau. (* esups u := [sequence ereal_sup (sdrop u n)]_n *) (* einfs u := [sequence ereal_inf (sdrop u n)]_n *) (* limn_e{inf,sup} == limit inferior/superior for \bar R *) +(* ``` *) (* *) (******************************************************************************) @@ -201,9 +207,7 @@ Proof. by move=> ndf ndg t m n mn; apply: ler_add; [exact/ndf|exact/ndg]. Qed. Local Notation eqolimn := (@eqolim _ _ _ eventually_filter). Local Notation eqolimPn := (@eqolimP _ _ _ eventually_filter). -(*********************) -(* Sequences of sets *) -(*********************) +(** Sequences of sets *) Section seqDU. Variables (T : Type). @@ -327,9 +331,7 @@ Qed. End seqD. -(************************************) -(* Convergence of patched sequences *) -(************************************) +(** Convergence of patched sequences *) Section sequences_patched. (* TODO: generalizations to numDomainType *) @@ -1281,9 +1283,9 @@ End exponential_series. (* TODO: generalize *) Definition expR {R : realType} (x : R) : R := lim (series (exp_coeff x)). -(********************************) -(* Sequences of natural numbers *) -(********************************) +(***markdown*******************************************************************) +(* ## Sequences of natural numbers *) +(******************************************************************************) Lemma __deprecated__nat_dvg_real (R : realType) (u_ : nat ^nat) : u_ --> \oo -> ([sequence (u_ n)%:R : R^o]_n --> +oo)%R. @@ -1352,9 +1354,9 @@ exists l => _ [n _ <-]; rewrite leNgt; apply/negP => lun; apply: lu. by near do rewrite (leq_trans lun) ?le_nseries//; apply: nbhs_infty_ge. Unshelve. all: by end_near. Qed. -(**************************************) -(* Sequences of extended real numbers *) -(**************************************) +(***markdown*******************************************************************) +(* ## Sequences of extended real numbers *) +(******************************************************************************) Notation "\big [ op / idx ]_ ( m <= i (\big[ op / idx ]_(m <= i < n | P) F))) : big_scope. diff --git a/theories/signed.v b/theories/signed.v index d4edf48b89..b9e4691325 100644 --- a/theories/signed.v +++ b/theories/signed.v @@ -3,7 +3,9 @@ From Coq Require Import ssreflect ssrfun ssrbool. From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint. From mathcomp Require Import mathcomp_extra. -(******************************************************************************) +(***markdown*******************************************************************) +(* # Positive, non-negative numbers, etc. *) +(* *) (* This file develops tools to make the manipulation of numbers with a known *) (* sign easier, thanks to canonical structures. This adds types like *) (* {posnum R} for positive values in R, a notation e%:pos that infers the *) @@ -12,7 +14,8 @@ From mathcomp Require Import mathcomp_extra. (* For instance, given x, y : {posnum R}, we have *) (* ((x%:num + y%:num) / 2)%:pos : {posnum R} automatically inferred. *) (* *) -(* * types for values with known sign *) +(* ## Types for values with known sign *) +(* ``` *) (* {posnum R} == interface type for elements in R that are positive; R *) (* must have a zmodType structure. *) (* Allows to solve automatically goals of the form x > 0 if *) @@ -49,8 +52,10 @@ From mathcomp Require Import mathcomp_extra. (* {!= x0 : T} == same with an explicit type T *) (* {?= x0} == {compare x0 & ?=0 & >?<0} *) (* {?= x0 : T} == same with an explicit type T *) +(* ``` *) (* *) -(* * casts from/to values with known sign *) +(* ## Casts from/to values with known sign *) +(* ``` *) (* x%:pos == explicitly casts x to {posnum R}, triggers the inference *) (* of a {posnum R} structure for x. *) (* x%:nng == explicitly casts x to {nonneg R}, triggers the inference *) @@ -62,23 +67,29 @@ From mathcomp Require Import mathcomp_extra. (* particular this works from {posnum R} and {nonneg R} to R.*) (* x%:posnum == explicit cast from {posnum R} to R. *) (* x%:nngnum == explicit cast from {nonneg R} to R. *) +(* ``` *) (* *) -(* * nullity conditions nz *) +(* ## Nullity conditions nz *) (* All nz above can be the following (in scope snum_nullity_scope delimited *) (* by %snum_nullity) *) +(* ``` *) (* !=0 == to encode x != 0 *) (* ?=0 == unknown nullity *) +(* ``` *) (* *) -(* * reality conditions cond *) +(* ## Reality conditions cond *) (* All cond above can be the following (in scope snum_sign_scope delimited by *) (* by %snum_sign) *) +(* ``` *) (* =0 == to encode x == 0 *) (* >=0 == to encode x >= 0 *) (* <=0 == to encode x <= 0 *) (* >=<0 == to encode x >=< 0 *) (* >?<0 == unknown reality *) +(* ``` *) (* *) -(* * sign proofs *) +(* ## Sign proofs *) +(* ``` *) (* [sgn of x] == proof that x is of sign inferred by x%:sgn *) (* [gt0 of x] == proof that x > 0 *) (* [lt0 of x] == proof that x < 0 *) @@ -86,23 +97,29 @@ From mathcomp Require Import mathcomp_extra. (* [le0 of x] == proof that x <= 0 *) (* [cmp0 of x] == proof that 0 >=< x *) (* [neq0 of x] == proof that x != 0 *) +(* ``` *) (* *) -(* * constructors *) +(* ## Constructors *) +(* ``` *) (* PosNum xgt0 == builds a {posnum R} from a proof xgt0 : x > 0 where x : R *) (* NngNum xge0 == builds a {posnum R} from a proof xgt0 : x >= 0 where x : R*) (* Signed.mk p == builds a {compare x0 & nz & cond} from a proof p that *) (* some x satisfies sign conditions encoded by nz and cond *) +(* ``` *) (* *) -(* * misc *) +(* ## Misc. *) +(* ``` *) (* !! x == triggers pretyping to fill the holes of the term x. The *) (* main use case is to trigger typeclass inference in the *) (* body of a ssreflect have := !! body. *) (* Credits: Enrico Tassi. *) +(* ``` *) (* *) -(* --> A number of canonical instances are provided for common operations, if *) +(* A number of canonical instances are provided for common operations, if *) (* your favorite operator is missing, look below for examples on how to add *) (* the appropriate Canonical. *) -(* --> Canonical instances are also provided according to types, as a *) +(* *) +(* Canonical instances are also provided according to types, as a *) (* fallback when no known operator appears in the expression. Look to *) (* nat_snum below for an example on how to add your favorite type. *) (******************************************************************************) @@ -353,7 +370,7 @@ Lemma typ_snum_subproof d nz cond (xt : Signed.typ d nz cond) Signed.spec (Signed.sort_x0 xt) nz cond x. Proof. by move: xt x => []. Qed. -(* This adds _ <- Signed.r ( typ_snum ) +(** This adds _ <- Signed.r ( typ_snum ) to canonical projections (c.f., Print Canonical Projections Signed.r) meaning that if no other canonical instance (with a registered head symbol) is found, a canonical instance of @@ -1180,10 +1197,10 @@ Proof. by move=> xge0; rewrite xge0 -[x]/(NngNum xge0)%:num; constructor. Qed. (* End NonnegOrder. *) -(* These proofs help integrate more arithmetic with signed.v. The issue is *) -(* Terms like `0 < 1-q` with subtraction don't work well. So we hide the *) -(* subtractions behind `PosNum` and `NngNum` constructors, see sequences.v *) -(* for examples. *) +(** These proofs help integrate more arithmetic with signed.v. The issue is + Terms like `0 < 1-q` with subtraction don't work well. So we hide the + subtractions behind `PosNum` and `NngNum` constructors, see sequences.v + for examples. *) Section onem_signed. Variable R : numDomainType. Implicit Types r : R. diff --git a/theories/summability.v b/theories/summability.v index 0ed596ee5f..44de6719c9 100644 --- a/theories/summability.v +++ b/theories/summability.v @@ -5,6 +5,10 @@ From mathcomp Require Import interval zmodp. From mathcomp Require Import boolp classical_sets. Require Import ereal reals Rstruct signed topology normedtype. +(***markdown*******************************************************************) +(* (undocumented experiment) *) +(******************************************************************************) + Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/topology.v b/theories/topology.v index a87aff7eb4..0aa7ac480b 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -4,21 +4,33 @@ From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import cardinality mathcomp_extra fsbigop. Require Import reals signed. -(******************************************************************************) -(* Filters and basic topological notions *) +(***markdown*******************************************************************) +(* # Filters and basic topological notions *) (* *) (* This file develops tools for the manipulation of filters and basic *) -(* topological notions. The development of topological notions builds on *) -(* "filtered types". They are types equipped with an interface that *) -(* associates to each element a set of sets, intended to represent a filter. *) -(* The notions of limit and convergence are defined for filtered types and in *) -(* the documentation below we call "canonical filter" of an element the set *) -(* of sets associated to it by the interface of filtered types. *) +(* topological notions. *) +(* *) +(* The development of topological notions builds on "filtered types". They *) +(* are types equipped with an interface that associates to each element a *) +(* set of sets, intended to represent a filter. The notions of limit and *) +(* convergence are defined for filtered types and in the documentation below *) +(* we call "canonical filter" of an element the set of sets associated to it *) +(* by the interface of filtered types. *) +(* *) +(* To make the manipulation of filters easier, this file also introduces *) +(* "near notations and tactics". Instead of proving $F\; G$, one can prove *) +(* $G\; x$ for $x$ "near $F$", i.e., for $x$ such that $H\; x$ for $H$ *) +(* arbitrarily precise as long as $F\; H$. The near tactics allow for a *) +(* delayed introduction of $H$: $H$ is introduced as an existential variable *) +(* and progressively instantiated during the proof process. *) (* *) +(* Here follow the detailed contents of this file: *) +(* ``` *) (* monotonous A f := {in A &, {mono f : x y / x <= y}} \/ *) (* {in A &, {mono f : x y /~ x <= y}}. *) -(* *) -(* * Filters : *) +(* ``` *) +(* ## Filters *) +(* ``` *) (* filteredType U == interface type for types whose *) (* elements represent sets of sets on U. *) (* These sets are intended to be filters *) @@ -126,15 +138,12 @@ Require Import reals signed. (* join_product f == The function (x => f ^~ x). When the *) (* family f separates points from closed *) (* sets, join_product is an embedding. *) +(* ``` *) +(* *) +(* ## Near notations and tactics *) (* *) -(* * Near notations and tactics: *) -(* --> The purpose of the near notations and tactics is to make the *) -(* manipulation of filters easier. Instead of proving F G, one can *) -(* prove G x for x "near F", i.e. for x such that H x for H arbitrarily *) -(* precise as long as F H. The near tactics allow for a delayed *) -(* introduction of H: H is introduced as an existential variable and *) -(* progressively instantiated during the proof process. *) -(* --> Notations: *) +(* Notations: *) +(* ``` *) (* {near F, P} == the property P holds near the *) (* canonical filter associated to F; P *) (* must have the form forall x, Q x. *) @@ -147,27 +156,30 @@ Require Import reals signed. (* \forall x & y \near F, P x y == same as before, with G = F. *) (* \near x & y, P x y := \forall z \near x & t \near y, P x y. *) (* x \is_near F == x belongs to a set P : in_filter F. *) -(* --> Tactics: *) -(* - near=> x introduces x: *) -(* On the goal \forall x \near F, G x, introduces the variable x and an *) -(* "existential", and unaccessible hypothesis ?H x and asks the user to *) -(* prove (G x) in this context. *) -(* Under the hood delays the proof of F ?H and waits for near: x *) -(* Also exists under the form near=> x y. *) -(* - near: x discharges x: *) -(* On the goal H_i x, and where x \is_near F, it asks the user to prove *) -(* that (\forall x \near F, H_i x), provided that H_i x does not depend *) -(* on variables introduced after x. *) -(* Under the hood, it refines by intersection the existential variable *) -(* ?H attached to x, computes the intersection with F, and asks the *) -(* user to prove F H_i, right now *) -(* - end_near should be used to close remaining existentials trivially *) -(* - near F => x poses a variable near F, where F is a proper filter *) -(* adds to the context a variable x that \is_near F, i.e. one may *) -(* assume H x for any H in F. This new variable x can be dealt with *) -(* using near: x, as for variables introduced by near=>. *) +(* ``` *) (* *) -(* * Topology : *) +(* Tactics: *) +(* - near=> x introduces x: *) +(* On the goal \forall x \near F, G x, introduces the variable x and an *) +(* "existential", and unaccessible hypothesis ?H x and asks the user to *) +(* prove (G x) in this context. *) +(* Under the hood delays the proof of F ?H and waits for near: x *) +(* Also exists under the form near=> x y. *) +(* - near: x discharges x: *) +(* On the goal H_i x, and where x \is_near F, it asks the user to prove *) +(* that (\forall x \near F, H_i x), provided that H_i x does not depend *) +(* on variables introduced after x. *) +(* Under the hood, it refines by intersection the existential variable *) +(* ?H attached to x, computes the intersection with F, and asks the *) +(* user to prove F H_i, right now *) +(* - end_near should be used to close remaining existentials trivially *) +(* - near F => x poses a variable near F, where F is a proper filter *) +(* adds to the context a variable x that \is_near F, i.e. one may *) +(* assume H x for any H in F. This new variable x can be dealt with *) +(* using near: x, as for variables introduced by near=>. *) +(* *) +(* ## Topology *) +(* ``` *) (* topologicalType == interface type for topological space *) (* structure. *) (* TopologicalMixin nbhs_filt nbhsE == builds the mixin for a topological *) @@ -260,8 +272,10 @@ Require Import reals signed. (* quotient_topology Q == the quotient topology corresponding to *) (* quotient Q : quotType T where T has *) (* type topologicalType *) +(* ``` *) (* *) -(* * Function space topologies : *) +(* ## Function space topologies *) +(* ``` *) (* {uniform` A -> V} == The space U -> V, equipped with the topology of *) (* uniform convergence from a set A to V, where *) (* V is a uniformType. *) @@ -277,11 +291,14 @@ Require Import reals signed. (* In particular {family compact, U -> V} is the *) (* topology of compact convergence. *) (* {family fam, F --> f} == F converges to f in {family fam, U -> V}. *) +(* ``` *) +(* *) +(* We used these topological notions to prove Tychonoff's Theorem, which *) +(* states that any product of compact sets is compact according to the *) +(* product topology. *) (* *) -(* --> We used these topological notions to prove Tychonoff's Theorem, which *) -(* states that any product of compact sets is compact according to the *) -(* product topology. *) -(* * Uniform spaces : *) +(* ## Uniform spaces *) +(* ``` *) (* nbhs_ ent == neighbourhoods defined using entourages *) (* uniformType == interface type for uniform spaces: a *) (* type equipped with entourages *) @@ -313,8 +330,10 @@ Require Import reals signed. (* gauge_psuedoMetricType E == the pseudoMetricType associated with the *) (* `gauge E` *) (* discrete_ent == entourages for the discrete topology *) +(* ``` *) (* *) -(* * PseudoMetric spaces : *) +(* ## PseudoMetric spaces *) +(* ``` *) (* entourage_ ball == entourages defined using balls *) (* pseudoMetricType == interface type for pseudo metric space *) (* structure: a type equipped with balls. *) @@ -343,8 +362,10 @@ Require Import reals signed. (* quotient Q : quotType T. where T has *) (* type topologicalType *) (* discrete_ball == singleton balls for thediscrete topology *) +(* ``` *) (* *) -(* * Complete uniform spaces : *) +(* ## Complete uniform spaces *) +(* ``` *) (* cauchy F <-> the set of sets F is a cauchy filter *) (* (entourage definition) *) (* completeType == interface type for a complete uniform *) @@ -357,8 +378,10 @@ Require Import reals signed. (* cT. *) (* [completeType of T] == clone of a canonical structure of *) (* completeType on T. *) +(* ``` *) (* *) -(* * Complete pseudometric spaces : *) +(* ## Complete pseudometric spaces *) +(* ``` *) (* cauchy_ex F <-> the set of sets F is a cauchy filter *) (* (epsilon-delta definition). *) (* cauchy F <-> the set of sets F is a cauchy filter *) @@ -379,18 +402,23 @@ Require Import reals signed. (* value N *) (* dense S == the set (S : set T) is dense in T, with *) (* T of type topologicalType *) +(* ``` *) (* *) -(* * Subspaces of topological spaces : *) +(* ## Subspaces of topological spaces *) +(* ``` *) (* subspace A == for (A : set T), this is a copy of T with *) (* a topology that ignores points outside A *) (* incl_subspace x == with x of type subspace A with (A : set T), *) (* inclusion of subspace A into T *) +(* ``` *) (* *) -(* * Arzela Ascoli' theorem : *) +(* ## Arzela Ascoli' theorem *) +(* ``` *) (* singletons T := [set [set x] | x in [set: T]]. *) (* equicontinuous W x == the set (W : X -> Y) is equicontinuous at x *) (* pointwise_precompact W == For each (x : X), set of images [f x | f in W] *) (* is precompact *) +(* ``` *) (* *) (* We endow several standard types with the types of topological notions: *) (* - products: prod_topologicalType, prod_uniformType, prod_pseudoMetricType *) @@ -791,9 +819,9 @@ rewrite propeqE; split => -[[/=A B] [FA FB] ABP]; by exists (B, A) => // -[x y] [/=Bx Ay]; apply: (ABP (y, x)). Qed. -(** * Filters *) - -(** ** Definitions *) +(***markdown*******************************************************************) +(* ## Filters *) +(******************************************************************************) Class Filter {T : Type} (F : set (set T)) := { filterT : F setT ; @@ -1159,7 +1187,9 @@ move=> ? PF; near do move=> /asboolP. by case: asboolP=> [/PF|_]; by [apply: filterS|apply: nearW]. Unshelve. all: by end_near. Qed. -(** ** Limits expressed with filters *) +(***markdown*******************************************************************) +(* ## Limits expressed with filters *) +(******************************************************************************) Definition fmap {T U : Type} (f : T -> U) (F : set (set T)) := [set P | F (f @^-1` P)]. @@ -1305,7 +1335,7 @@ Global Instance globally_properfilter {T : Type} (A : set T) a : infer (A a) -> ProperFilter (globally A). Proof. by move=> Aa; apply: Build_ProperFilter' => /(_ a). Qed. -(** ** Specific filters *) +(** Specific filters *) Section frechet_filter. Variable T : Type. @@ -1633,7 +1663,9 @@ Canonical bool_discrete_filter := FilteredType bool bool principal_filter. End PrincipalFilters. -(** * Topological spaces *) +(***markdown*******************************************************************) +(* ## Topological spaces *) +(******************************************************************************) Module Topological. @@ -2004,7 +2036,7 @@ End within_topologicalType. Notation "[ 'locally' P ]" := (@locally_of _ _ _ (Phantom _ P)). -(** ** Topology defined by a filter *) +(** Topology defined by a filter *) Section TopologyOfFilter. @@ -2027,7 +2059,7 @@ Next Obligation. done. Qed. End TopologyOfFilter. -(** ** Topology defined by open sets *) +(** Topology defined by open sets *) Section TopologyOfOpen. @@ -2064,7 +2096,7 @@ Qed. End TopologyOfOpen. -(** ** Topology defined by a base of open sets *) +(** Topology defined by a base of open sets *) Section TopologyOfBase. @@ -2161,7 +2193,7 @@ move=> [P sFP] [Q sFQ] PQB /filterS; apply; rewrite -PQB. by apply: (filterI _ _); [exact: (IH _ _ sFP)|exact: (IH _ _ sFQ)]. Qed. -(** ** Topology defined by a subbase of open sets *) +(** Topology defined by a subbase of open sets *) Definition finI_from (I : choiceType) T (D : set I) (f : I -> set T) := [set \bigcap_(i in [set` D']) f i | @@ -2244,7 +2276,7 @@ Qed. End TopologyOfSubbase. -(* Topology on nat *) +(** Topology on nat *) Section nat_topologicalType. @@ -2368,7 +2400,7 @@ End map. End infty_nat. -(** ** Topology on the product of two spaces *) +(** Topology on the product of two spaces *) Section Prod_Topology. @@ -2399,7 +2431,7 @@ Canonical prod_topologicalType := End Prod_Topology. -(** ** Topology on matrices *) +(** Topology on matrices *) Section matrix_Topology. @@ -2435,7 +2467,7 @@ Canonical matrix_topologicalType := End matrix_Topology. -(** ** Weak topology by a function *) +(** Weak topology by a function *) Section Weak_Topology. @@ -2492,7 +2524,7 @@ Qed. End Weak_Topology. -(** ** Supremum of a family of topologies *) +(** Supremum of a family of topologies *) Section Sup_Topology. @@ -2529,7 +2561,7 @@ Qed. End Sup_Topology. -(** ** Product topology *) +(** Product topology *) Section Product_Topology. @@ -2579,7 +2611,7 @@ Proof. by move => FF /cvg_ex [l H]; apply/cvg_ex; exists l; exact: cvg_within_fi Lemma nbhs_dnbhs {T : topologicalType} (x : T) : x^' `=>` nbhs x. Proof. exact: cvg_within. Qed. -(** meets *) +(** meets: *) Lemma meets_openr {T : topologicalType} (F : set (set T)) (x : T) : F `#` nbhs x = F `#` open_nbhs x. @@ -2615,7 +2647,9 @@ Qed. Lemma proper_meetsxx T (F : set (set T)) (FF : ProperFilter F) : F `#` F. Proof. by rewrite meetsxx; apply: filter_not_empty. Qed. -(** ** Closed sets in topological spaces *) +(***markdown*******************************************************************) +(* ## Closed sets in topological spaces *) +(******************************************************************************) Section Closed. @@ -2807,7 +2841,9 @@ Qed. End closure_lemmas. -(** ** Compact sets *) +(***markdown*******************************************************************) +(* ## Compact sets *) +(******************************************************************************) Section Compact. @@ -4057,7 +4093,9 @@ Qed. End set_nbhs. -(** * Uniform spaces *) +(***markdown*******************************************************************) +(* ## Uniform spaces *) +(******************************************************************************) Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope. @@ -4458,7 +4496,7 @@ End prod_Uniform. Canonical prod_uniformType (U V : uniformType) := UniformType (U * V) (@prod_uniformType_mixin U V). -(** matrices *) +(** Matrices *) Section matrix_Uniform. @@ -4623,7 +4661,9 @@ Definition entourage_set (U : uniformType) (A : set ((set U) * (set U))) := Canonical set_filter_source (U : uniformType) := @Filtered.Source Prop _ U (fun A => nbhs_ (@entourage_set U) A). -(** * PseudoMetric spaces defined using balls *) +(***markdown*******************************************************************) +(* ## PseudoMetric spaces defined using balls *) +(******************************************************************************) Definition entourage_ {R : numDomainType} {T T'} (ball : T -> R -> set T') := @filter_from R _ [set x | 0 < x] (fun e => [set xy | ball xy.1 e xy.2]). @@ -5211,7 +5251,9 @@ rewrite /= -[leRHS]invrK lef_pinv ?posrE ?invr_gt0// -natr1. by rewrite natr_absz ger0_norm ?floor_ge0 ?invr_ge0// 1?ltW// lt_succ_floor. Qed. -(** ** Specific pseudoMetric spaces *) +(***markdown*******************************************************************) +(* ## Specific pseudoMetric spaces *) +(******************************************************************************) (** matrices *) Section matrix_PseudoMetric. @@ -5414,7 +5456,9 @@ End discrete_pseudoMetric. Definition pseudoMetric_bool {R : realType} := @discrete_pseudoMetricType R [topologicalType of bool] discrete_bool. -(** ** Complete uniform spaces *) +(***markdown*******************************************************************) +(* ## Complete uniform spaces *) +(******************************************************************************) Definition cauchy {T : uniformType} (F : set (set T)) := (F, F) --> entourage. @@ -5543,7 +5587,7 @@ Canonical fun_completeType := CompleteType (T -> U) fun_complete. End fun_Complete. -(** ** Limit switching *) +(** Limit switching *) Section Cvg_switch. Context {T1 T2 : choiceType}. @@ -5593,7 +5637,9 @@ Qed. End Cvg_switch. -(** ** Complete pseudoMetric spaces *) +(***markdown*******************************************************************) +(* ## Complete pseudoMetric spaces *) +(******************************************************************************) Definition cauchy_ex {R : numDomainType} {T : pseudoMetricType R} (F : set (set T)) := forall eps : R, 0 < eps -> exists x, F (ball x eps). diff --git a/theories/trigo.v b/theories/trigo.v index b1809ffba3..36587ffe33 100644 --- a/theories/trigo.v +++ b/theories/trigo.v @@ -5,12 +5,13 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions. Require Import reals ereal nsatz_realtype signed topology normedtype landau. Require Import sequences derive realfun exp. -(******************************************************************************) -(* Theory of trigonometric functions *) +(***markdown*******************************************************************) +(* # Theory of trigonometric functions *) (* *) (* This file provides the definitions of basic trigonometric functions and *) (* develops their theories. *) (* *) +(* ``` *) (* periodic f T == f is a periodic function of period T *) (* alternating f T == f is an alternating function of period T *) (* sin_coeff x == the sequence of coefficients of sin x *) @@ -24,6 +25,7 @@ Require Import sequences derive realfun exp. (* acos x == the arccos function *) (* asin x == the arcsin function *) (* atan x == the arctangent function *) +(* ``` *) (* *) (* Acknowledgments: the proof of cos 2 < 0 is inspired from HOL-light, some *) (* proofs of trigonometric relations are taken from *)