From 7a7ac3a855ddd975cbccd839057586654ea661ab Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Fri, 24 Jul 2026 07:52:56 +0000 Subject: [PATCH] deflists docs --- classical/boolp.v | 67 +-- classical/cardinality.v | 55 ++- classical/classical_orders.v | 21 +- classical/classical_sets.v | 459 ++++++++++++------ classical/contra.v | 61 +-- classical/filter.v | 301 +++++++----- classical/fsbigop.v | 15 +- classical/functions.v | 307 +++++++----- classical/mathcomp_extra.v | 10 +- classical/set_interval.v | 70 ++- classical/unstable.v | 75 ++- classical/wochoice.v | 61 ++- reals/constructive_ereal.v | 144 ++++-- reals/reals.v | 53 +- theories/borel_hierarchy.v | 13 +- theories/cantor.v | 13 +- theories/convex.v | 39 +- theories/derive.v | 33 +- theories/ereal.v | 53 +- theories/ess_sup_inf.v | 11 +- theories/esum.v | 21 +- theories/exp.v | 40 +- theories/ftc.v | 5 +- theories/hoelder.v | 51 +- theories/homotopy_theory/continuous_path.v | 19 +- theories/homotopy_theory/wedge_sigT.v | 49 +- theories/independence.v | 23 +- theories/kernel.v | 129 +++-- theories/landau.v | 109 +++-- theories/lebesgue_integral_theory/giry.v | 58 ++- .../lebesgue_Rintegral.v | 5 +- .../lebesgue_integrable.v | 7 +- .../lebesgue_integral_definition.v | 15 +- .../lebesgue_integral_differentiation.v | 38 +- .../lebesgue_integral_fubini.v | 20 +- .../lebesgue_integral_under.v | 7 +- .../measurable_fun_approximation.v | 21 +- .../lebesgue_integral_theory/radon_nikodym.v | 16 +- .../simple_functions.v | 56 ++- theories/lebesgue_measure.v | 20 +- theories/lebesgue_stieltjes_measure.v | 107 ++-- theories/measurable_realfun.v | 38 +- theories/measure_theory/counting_measure.v | 5 +- theories/measure_theory/dirac_measure.v | 5 +- theories/measure_theory/measurable_function.v | 15 +- .../measure_theory/measurable_structure.v | 219 +++++---- theories/measure_theory/measure_extension.v | 79 ++- theories/measure_theory/measure_function.v | 180 ++++--- theories/measure_theory/measure_negligible.v | 55 ++- theories/measure_theory/probability_measure.v | 60 +-- theories/measure_theory/signed_measure.v | 103 ++-- .../complete_normed_module.v | 9 +- theories/normedtype_theory/ereal_normedtype.v | 19 +- .../normedtype_theory/matrix_normedtype.v | 7 +- theories/normedtype_theory/normed_module.v | 97 ++-- theories/normedtype_theory/num_normedtype.v | 44 +- .../pseudometric_normed_Zmodule.v | 82 ++-- theories/normedtype_theory/tvs.v | 144 +++--- theories/normedtype_theory/urysohn.v | 40 +- theories/normedtype_theory/vitali_lemma.v | 27 +- theories/numfun.v | 54 ++- .../bernoulli_distribution.v | 11 +- .../probability_theory/beta_distribution.v | 26 +- .../binomial_distribution.v | 19 +- .../exponential_distribution.v | 9 +- .../probability_theory/normal_distribution.v | 21 +- .../probability_theory/poisson_distribution.v | 9 +- .../probability_theory/uniform_distribution.v | 11 +- theories/realfun.v | 40 +- theories/sequences.v | 179 ++++--- theories/showcase/pnt.v | 5 +- theories/topology_theory/compact.v | 57 ++- theories/topology_theory/connected.v | 15 +- theories/topology_theory/discrete_topology.v | 50 +- theories/topology_theory/function_spaces.v | 96 ++-- theories/topology_theory/initial_topology.v | 24 +- theories/topology_theory/matrix_topology.v | 11 +- theories/topology_theory/metric_structure.v | 13 +- theories/topology_theory/order_topology.v | 29 +- .../topology_theory/pseudometric_structure.v | 61 ++- theories/topology_theory/quotient_topology.v | 8 +- theories/topology_theory/separation_axioms.v | 67 +-- theories/topology_theory/sigT_topology.v | 7 +- theories/topology_theory/subspace_topology.v | 50 +- theories/topology_theory/subtype_topology.v | 9 +- theories/topology_theory/supremum_topology.v | 11 +- theories/topology_theory/topology_structure.v | 157 +++--- theories/topology_theory/uniform_structure.v | 66 +-- theories/trigo.v | 53 +- 89 files changed, 3049 insertions(+), 2024 deletions(-) diff --git a/classical/boolp.v b/classical/boolp.v index 290b102779..a9120e8253 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -20,25 +20,28 @@ From mathcomp Require internal_Eqdep_dec. (* Asymptotic Reasoning in Classical Analysis. JFR 2018 *) (* *) (* ## Axioms *) -(* ``` *) -(* functional_extensionality_dep == functional extensionality (on dependently *) -(* typed functions), i.e., functions that are pointwise *) -(* equal are equal *) -(* propositional_extensionality == propositional extensionality, i.e., iff *) -(* and equality are the same on Prop *) -(* constructive_indefinite_description == existential in Prop (ex) implies *) -(* existential in Type (sig) *) -(* cid := constructive_indefinite_description (shortcut) *) -(* ``` *) +(* `functional_extensionality_dep` *) +(* ~ functional extensionality (on dependently typed functions), *) +(* i.e., functions that are pointwise equal are equal *) +(* *) +(* `propositional_extensionality` *) +(* ~ propositional extensionality, i.e., iff and equality are the *) +(* same on `Prop` *) +(* *) +(* `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 *) (* often more pratical to use than directly using the axioms. For instance *) (* propext, funext, the excluded middle (EM),... *) (* *) (* ## Boolean View of Prop *) -(* ``` *) -(* `[< P >] == boolean view of P : Prop, see all lemmas about asbool *) -(* ``` *) +(* `` `[< P >] `` *) +(* ~ boolean view of `P : Prop`, see all lemmas about `asbool` *) (* *) (* ## Mathematical Components Structures *) (* *) @@ -50,26 +53,32 @@ From mathcomp Require internal_Eqdep_dec. (* and choiceType structures to let the user choose which definition of *) (* equality to use and to avoid conflict with already declared instances. *) (* *) -(* ``` *) -(* {classic T} == Endow T : Type with a canonical eqType/choiceType. *) -(* This is intended for local use. *) -(* E.g., T : Type |- A : {fset {classic T}} *) -(* Alternatively one may use elim/Pchoice: T => T in H *. *) -(* to substitute T with T : choiceType once and for all. *) -(* {eclassic T} == Endow T : eqType with a canonical choiceType. *) -(* On the model of {classic _}. *) -(* See also the lemmas Peq and eqPchoice. *) -(* ``` *) +(* `{classic T}` *) +(* ~ Endow `T : Type` with a canonical `eqType`/`choiceType`. *) +(* ~ This is intended for local use. *) +(* ~ E.g., `T : Type |- A : {fset {classic T}}` *) +(* ~ Alternatively one may use `elim/Pchoice: T => T in H *.` to *) +(* substitute `T` with `T : choiceType` once and for all. *) +(* *) +(* `{eclassic T}` *) +(* ~ Endow `T : eqType` with a canonical `choiceType`. *) +(* ~ On the model of `{classic _}`. *) +(* ~ See also the lemmas `Peq` and `eqPchoice`. *) (* *) (* Functions onto a porderType (resp. latticeType) are equipped with *) (* a porderType (resp. latticeType), so that the generic notation (_ <= _)%O *) (* (resp. `&`, `|`) from `order.v` can be used. *) -(* ``` *) -(* FunOrder.lef f g == pointwise large inequality between two functions *) -(* FunOrder.ltf f g == pointwise strict inequality between two functions *) -(* FunLattice.meetf f g == pointwise meet between two functions *) -(* FunLattice.joinf f g == pointwise join between two functions *) -(* ``` *) +(* `FunOrder.lef f g` *) +(* ~ pointwise large inequality between two functions *) +(* *) +(* `FunOrder.ltf f g` *) +(* ~ pointwise strict inequality between two functions *) +(* *) +(* `FunLattice.meetf f g` *) +(* ~ pointwise meet between two functions *) +(* *) +(* `FunLattice.joinf f g` *) +(* ~ pointwise join between two functions *) (* *) (******************************************************************************) diff --git a/classical/cardinality.v b/classical/cardinality.v index 209d323baf..e1f663b8e1 100644 --- a/classical/cardinality.v +++ b/classical/cardinality.v @@ -16,25 +16,42 @@ 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 *) -(* A #!= B := ~~ (A #= B) *) -(* finite_set A == the set A is finite *) -(* := exists n, A #= `I_n *) -(* <-> exists X : {fset T}, A = [set` X] *) -(* <-> ~ ([set: nat] #<= A) *) -(* infinite_set A := ~ finite_set A *) -(* cofinite_set A := finite_set (~` A) *) -(* countable A <-> A is countable *) -(* := A #<= [set: nat] *) -(* fset_set A == the finite set corresponding if A : set T is finite, *) -(* set0 otherwise (T : choiceType) *) -(* 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 *) -(* ``` *) +(* `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` *) +(* *) +(* `A #!= B` *) +(* ~ `~~ (A #= B)` *) +(* *) +(* `finite_set A` *) +(* ~ the set `A` is finite *) +(* ~ ``:= exists n, A #= `I_n`` *) +(* ~ ``<-> exists X : {fset T}, A = [set` X]`` *) +(* ~ `<-> ~ ([set: nat] #<= A)` *) +(* *) +(* `infinite_set A` *) +(* ~ `~ finite_set A` *) +(* *) +(* `cofinite_set A` *) +(* ~ ``finite_set (~` A)`` *) +(* *) +(* `countable A` *) +(* ~ `A` is countable *) +(* ~ `:= A #<= [set: nat]` *) +(* *) +(* ``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_orders.v b/classical/classical_orders.v index c7c58d8225..8afc80ba1d 100644 --- a/classical/classical_orders.v +++ b/classical/classical_orders.v @@ -8,13 +8,20 @@ From mathcomp Require Import functions set_interval. (* *) (* This file provides some additional order theory that requires stronger *) (* axioms than mathcomp's own orders expect. *) -(* ``` *) -(* same_prefix n == two elements in a product space agree up n *) -(* first_diff x y == the first occurrence where x n != y n, or None *) -(* big_lexi_le == the (countably) infinite lexicographical ordering *) -(* big_lexi_order == an alias for attaching this order type *) -(* start_with n x y == x for the first n values, then switches to y *) -(* ``` *) +(* `same_prefix n` *) +(* ~ two elements in a product space agree up `n` *) +(* *) +(* `first_diff x y` *) +(* ~ the first occurrence where `x n != y n`, or `None` *) +(* *) +(* `big_lexi_le` *) +(* ~ the (countably) infinite lexicographical ordering *) +(* *) +(* `big_lexi_order` *) +(* ~ an alias for attaching this order type *) +(* *) +(* `start_with n x y` *) +(* ~ `x` for the first `n` values, then switches to `y` *) (* *) (******************************************************************************) diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 6a7a102599..fbdfbe49f8 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -54,184 +54,333 @@ From mathcomp Require Import mathcomp_extra boolp wochoice. (* *) (* Detailed documentation: *) (* ## Sets *) -(* ``` *) -(* set T == type of sets on T *) -(* (x \in P) == boolean membership predicate from ssrbool *) -(* for set P, available thanks to a canonical *) -(* predType T structure on sets on T *) -(* [set x : T | P] == set of points x : T such that P holds *) -(* [set x | P] == same as before with T left implicit *) -(* [set E | x in A] == set defined by the expression E for x in *) -(* set A *) -(* [set E | x in A & y in B] == same as before for E depending on 2 *) -(* variables x and y in sets A and B *) -(* setT == full set *) -(* set0 == empty set *) -(* range f == the range of f, i.e., [set f x | x in setT] *) -(* [set a] == set containing only a *) -(* [set a : T] == same as before with the type of a made *) -(* explicit *) -(* A `|` B == union of A and B *) -(* a |` A == A extended with a *) -(* [set a1; a2; ..; an] == set containing only the n elements ai *) -(* A `&` B == intersection of A and B *) -(* A `*` B == product of A and B, i.e., set of pairs *) -(* (a,b) such that A a and B b *) -(* A.`1 == set of points a such that there exists b so *) -(* that A (a, b) *) -(* A.`2 == set of points a such that there exists b so *) -(* that A (b, a) *) -(* ~` A == complement of A *) -(* [set~ a] == complement of [set a] *) -(* A `\` B == complement of B in A *) -(* A `\ a == A deprived of a *) -(* `I_n := [set k | k < n] *) -(* \bigcup_(i in P) F == union of the elements of the family F whose *) -(* index satisfies P *) -(* \bigcup_(i : T) F == union of the family F indexed on T *) -(* \bigcup_(i < n) F := \bigcup_(i in `I_n) F *) -(* \bigcup_(i >= n) F := \bigcup_(i in [set i | i >= n]) F *) -(* \bigcup_i F == same as before with T left implicit *) -(* \bigcap_(i in P) F == intersection of the elements of the family *) -(* F whose index satisfies P *) -(* \bigcap_(i : T) F == union of the family F indexed on T *) -(* \bigcap_(i < n) F := \bigcap_(i in `I_n) F *) -(* \bigcap_(i >= n) F := \bigcap_(i in [set i | i >= n]) F *) -(* \bigcap_i F == same as before with T left implicit *) -(* ``` *) +(* `set T` *) +(* ~ type of sets on `T` *) +(* *) +(* `(x \in P)` *) +(* ~ boolean membership predicate from `ssrbool` for set `P`, *) +(* available thanks to a canonical `predType T` structure on sets *) +(* on `T` *) +(* *) +(* `[set x : T | P]` *) +(* ~ set of points `x : T` such that `P` holds *) +(* *) +(* `[set x | P]` *) +(* ~ same as before with `T` left implicit *) +(* *) +(* `[set E | x in A]` *) +(* ~ set defined by the expression `E` for `x` in set `A` *) +(* *) +(* `[set E | x in A & y in B]` *) +(* ~ same as before for `E` depending on 2 variables `x` and `y` in *) +(* sets `A` and `B` *) +(* *) +(* `setT` *) +(* ~ full set *) +(* *) +(* `set0` *) +(* ~ empty set *) +(* *) +(* `range f` *) +(* ~ the range of `f`, i.e., `[set f x | x in setT]` *) +(* *) +(* `[set a]` *) +(* ~ set containing only `a` *) +(* *) +(* `[set a : T]` *) +(* ~ same as before with the type of `a` made explicit *) +(* *) +(* ``A `|` B`` *) +(* ~ union of `A` and `B` *) +(* *) +(* ``a |` A`` *) +(* ~ `A` extended with `a` *) +(* *) +(* `[set a1; a2; ..; an]` *) +(* ~ set containing only the `n` elements `ai` *) +(* *) +(* ``A `&` B`` *) +(* ~ intersection of `A` and `B` *) +(* *) +(* ``A `*` B`` *) +(* ~ product of `A` and `B`, i.e., set of pairs `(a,b)` such that *) +(* `A a` and `B b` *) +(* *) +(* ``A.`1`` *) +(* ~ set of points `a` such that there exists `b` so that *) +(* `A (a, b)` *) +(* *) +(* ``A.`2`` *) +(* ~ set of points `a` such that there exists `b` so that *) +(* `A (b, a)` *) +(* *) +(* ``~` A`` *) +(* ~ complement of `A` *) +(* *) +(* `[set~ a]` *) +(* ~ complement of `[set a]` *) +(* *) +(* ``A `\` B`` *) +(* ~ complement of `B` in `A` *) +(* *) +(* ``A `\ a`` *) +(* ~ `A` deprived of `a` *) +(* *) +(* `` `I_n `` *) +(* ~ `[set k | k < n]` *) +(* *) +(* `\bigcup_(i in P) F` *) +(* ~ union of the elements of the family `F` whose index satisfies *) +(* `P` *) +(* *) +(* `\bigcup_(i : T) F` *) +(* ~ union of the family `F` indexed on `T` *) +(* *) +(* `\bigcup_(i < n) F` *) +(* ~ ``\bigcup_(i in `I_n) F`` *) +(* *) +(* `\bigcup_(i >= n) F` *) +(* ~ `\bigcup_(i in [set i | i >= n]) F` *) +(* *) +(* `\bigcup_i F` *) +(* ~ same as before with `T` left implicit *) +(* *) +(* `\bigcap_(i in P) F` *) +(* ~ intersection of the elements of the family `F` whose index *) +(* satisfies `P` *) +(* *) +(* `\bigcap_(i : T) F` *) +(* ~ union of the family `F` indexed on `T` *) +(* *) +(* `\bigcap_(i < n) F` *) +(* ~ ``\bigcap_(i in `I_n) F`` *) +(* *) +(* `\bigcap_(i >= n) F` *) +(* ~ `\bigcap_(i in [set i | i >= n]) F` *) +(* *) +(* `\bigcap_i F` *) +(* ~ same as before with `T` left implicit *) (* *) (* ### About sets of sets *) -(* ``` *) -(* set_system T := set (set T) *) -(* setI_closed G == the set of sets G is closed under finite *) -(* intersection *) -(* setU_closed G == the set of sets G is closed under finite *) -(* union *) -(* rectangle X Y := [set U `*` V | U in X & V in Y] *) -(* preimage_set_system D f G == set system of the preimages by f of sets *) -(* in G *) -(* image_set_system D f G == set system of the sets with a preimage *) -(* by f in G *) -(* cross f g X Y := preimage_set_system setT f X *) -(* `|` preimage_set_system setT g Y *) -(* X `x` Y := cross fst snd X Y *) -(* ``` *) -(* *) -(* ``` *) -(* *) -(* R ^nat == notation for the type of sequences, i.e., *) -(* functions of type nat -> R *) -(* bigcup2 A B == the sequence A, B, 0, 0, ... *) -(* bigcup2 A B == the sequence A, B, T, T, ... *) -(* smallest C G := \bigcap_(A in [set M | C M /\ G `<=` M]) A *) -(* A `<=` B <-> A is included in B *) -(* A `<` B := A `<=` B /\ ~ (B `<=` A) *) -(* A `<=>` B <-> double inclusion A `<=` B and B `<=` A *) -(* f @^-1` A == preimage of A by f *) -(* f @` A == image of A by f *) -(* This is a notation for `image A f` *) -(* A !=set0 := exists x, A x *) -(* [set` p] == a classical set corresponding to the *) -(* predType p *) -(* `[a, b] := [set` `[a, b]], i.e., a classical set *) -(* corresponding to the interval `[a, b] *) -(* `]a, b] := [set` `]a, b]] *) -(* `[a, b[ := [set` `[a, b[] *) -(* `]a, b[ := [set` `]a, b[] *) -(* `]-oo, b] := [set` `]-oo, b]] *) -(* `]-oo, b[ := [set` `]-oo, b[] *) -(* `[a, +oo[ := [set` `[a, +oo[] *) -(* `]a, +oo[ := [set` `]a, +oo[] *) -(* `]-oo, +oo[ := [set` `]-oo, +oo[] *) -(* is_subset1 A <-> A contains only 1 element *) -(* is_fun f <-> for each a, f a contains only 1 element *) -(* is_total f <-> for each a, f a is non empty *) -(* is_totalfun f <-> conjunction of is_fun and is_total *) -(* xget x0 P == point x in P if it exists, x0 otherwise; *) -(* P must be a set on a choiceType *) -(* fun_of_rel f0 f == function that maps x to an element of f x *) -(* if there is one, to f0 x otherwise *) -(* F `#` G <-> intersections beween elements of F an G are *) -(* all non empty *) -(* seqDU F := sequence F_0, F_1\F_0, F_2\(F_0 U F_1),... *) -(* seqD F == the sequence F_0, F_1 \ F_0, F_2 \ F_1,... *) -(* ``` *) +(* `set_system T` *) +(* ~ `set (set T)` *) +(* *) +(* `setI_closed G` *) +(* ~ the set of sets `G` is closed under finite intersection *) +(* *) +(* `setU_closed G` *) +(* ~ the set of sets `G` is closed under finite union *) +(* *) +(* `rectangle X Y` *) +(* ~ ``[set U `*` V | U in X & V in Y]`` *) +(* *) +(* `preimage_set_system D f G` *) +(* ~ set system of the preimages by `f` of sets in `G` *) +(* *) +(* `image_set_system D f G` *) +(* ~ set system of the sets with a preimage by `f` in `G` *) +(* *) +(* `cross f g X Y` *) +(* ~ ``preimage_set_system setT f X `|` preimage_set_system setT g Y`` *) +(* *) +(* ``X `x` Y`` *) +(* ~ `cross fst snd X Y` *) +(* *) +(* `R ^nat` *) +(* ~ notation for the type of sequences, i.e., functions of type *) +(* `nat -> R` *) +(* *) +(* `bigcup2 A B` *) +(* ~ the sequence `A`, `B`, `0`, `0`, ... *) +(* *) +(* `bigcup2 A B` *) +(* ~ the sequence `A`, `B`, `T`, `T`, ... *) +(* *) +(* `smallest C G` *) +(* ~ ``\bigcap_(A in [set M | C M /\ G `<=` M]) A`` *) +(* *) +(* ``A `<=` B`` *) +(* ~ `A` is included in `B` *) +(* *) +(* ``A `<` B`` *) +(* ~ ``A `<=` B /\ ~ (B `<=` A)`` *) +(* *) +(* ``A `<=>` B`` *) +(* ~ double inclusion ``A `<=` B`` and ``B `<=` A`` *) +(* *) +(* ``f @^-1` A`` *) +(* ~ preimage of `A` by `f` *) +(* *) +(* ``f @` A`` *) +(* ~ image of `A` by `f`. This is a notation for `image A f` *) +(* *) +(* `A !=set0` *) +(* ~ `exists x, A x` *) +(* *) +(* ``[set` p]`` *) +(* ~ a classical set corresponding to the `predType p` *) +(* *) +(* `` `[a, b] `` *) +(* ~ ``[set` `[a, b]]``, i.e., a classical set corresponding to *) +(* the interval `` `[a, b] `` *) +(* *) +(* `` `]a, b] `` *) +(* ~ ``[set` `]a, b]]`` *) +(* *) +(* `` `[a, b[ `` *) +(* ~ ``[set` `[a, b[]`` *) +(* *) +(* `` `]a, b[ `` *) +(* ~ ``[set` `]a, b[]`` *) +(* *) +(* `` `]-oo, b] `` *) +(* ~ ``[set` `]-oo, b]]`` *) +(* *) +(* `` `]-oo, b[ `` *) +(* ~ ``[set` `]-oo, b[]`` *) +(* *) +(* `` `[a, +oo[ `` *) +(* ~ ``[set` `[a, +oo[]`` *) +(* *) +(* `` `]a, +oo[ `` *) +(* ~ ``[set` `]a, +oo[]`` *) +(* *) +(* `` `]-oo, +oo[ `` *) +(* ~ ``[set` `]-oo, +oo[]`` *) +(* *) +(* `is_subset1 A` *) +(* ~ `A` contains only 1 element *) +(* *) +(* `is_fun f` *) +(* ~ for each `a`, `f a` contains only 1 element *) +(* *) +(* `is_total f` *) +(* ~ for each `a`, `f a` is non empty *) +(* *) +(* `is_totalfun f` *) +(* ~ conjunction of `is_fun` and `is_total` *) +(* *) +(* `xget x0 P` *) +(* ~ point `x` in `P` if it exists, `x0` otherwise; `P` must be a *) +(* set on a `choiceType` *) +(* *) +(* `fun_of_rel f0 f` *) +(* ~ function that maps `x` to an element of `f x` if there is *) +(* one, to `f0 x` otherwise *) +(* *) +(* ``F `#` G`` *) +(* ~ intersections beween elements of `F` an `G` are all non *) +(* empty *) +(* *) +(* `seqDU F` *) +(* ~ sequence `F_0`, `F_1\F_0`, `F_2\(F_0 U F_1)`,... *) +(* *) +(* `seqD F` *) +(* ~ the sequence `F_0`, `F_1 \ F_0`, `F_2 \ F_1`,... *) (* *) (* ## Pointed types *) -(* ``` *) -(* pointedType == interface type for types equipped with a *) -(* canonical inhabitant *) -(* The HB class is Pointed. *) -(* 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. *) -(* ``` *) +(* `pointedType` *) +(* ~ interface type for types equipped with a canonical inhabitant. *) +(* The HB class is `Pointed`. *) +(* *) +(* `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` *) (* *) (* ## squash/unsquash *) -(* ``` *) -(* $| T | == the type `T : Type` is inhabited *) -(* $| T | has type `Prop`. *) -(* $| T | is a notation for `squashed T`. *) -(* squash x == object of type $| T | (with x : T) *) -(* unsquash s == extract an inhabitant of type `T` *) -(* (with s : $| T |) *) -(* ``` *) +(* `$| T |` *) +(* ~ the type `T : Type` is inhabited. `$| T |` has type `Prop`. *) +(* `$| T |` is a notation for `squashed T`. *) +(* *) +(* `squash x` *) +(* ~ object of type `$| T |` (with `x : T`) *) +(* *) +(* `unsquash s` *) +(* ~ extract an inhabitant of type `T` (with `s : $| T |`) *) (* Tactic: *) (* - squash x: *) (* solves a goal $| T | by instantiating with x or [the T of x] *) (* *) (* ## Pairwise-disjoint sets *) -(* ``` *) -(* 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 *) -(* partition D F A == the non-empty sets F i,where i ranges over *) -(* D : set I, form a partition of A *) -(* pblock_index D F x == index i such that i \in D and x \in F i *) -(* pblock D F x := F (pblock_index D F x) *) -(* *) -(* 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 *) -(* ``` *) +(* `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` *) +(* *) +(* `partition D F A` *) +(* ~ the non-empty sets `F i`,where `i` ranges over `D : set I`, *) +(* form a partition of `A` *) +(* *) +(* `pblock_index D F x` *) +(* ~ index `i` such that `i \in D` and `x \in F i` *) +(* *) +(* `pblock D F x` *) +(* ~ `F (pblock_index D F x)` *) +(* *) +(* `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 *) -(* ``` *) -(* ubound A == the set of upper bounds of the set A *) -(* lbound A == the set of lower bounds of the set A *) -(* ``` *) +(* `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 *) -(* has_inf A := A != set0 /\ has_lbound A *) +(* `has_ubound A` *) +(* ~ `ubound A != set0` *) +(* *) +(* `has_sup A` *) +(* ~ `A != set0 /\ has_ubound A` *) +(* *) +(* `has_lbound A` *) +(* ~ `lbound A != set0` *) +(* *) +(* `has_inf A` *) +(* ~ `A != set0 /\ has_lbound A` *) +(* *) +(* `isLub A m` *) +(* ~ `m` is a least upper bound of the set `A` *) (* *) -(* isLub A m := m is a least upper bound of the set A *) -(* supremums A := set of supremums of the set A *) -(* supremum x0 A == supremum of A or x0 if A is empty *) -(* infimums A := set of infimums of the set A *) -(* infimum x0 A == infimum of A or x0 if A is empty *) +(* `supremums A` *) +(* ~ set of supremums of the set `A` *) (* *) -(* F `#` G := the classes of sets F and G intersect *) -(* ``` *) +(* `supremum x0 A` *) +(* ~ supremum of `A` or `x0` if `A` is empty *) +(* *) +(* `infimums A` *) +(* ~ set of infimums of the set `A` *) +(* *) +(* `infimum x0 A` *) +(* ~ infimum of `A` or `x0` if `A` is empty *) +(* *) +(* ``F `#` G`` *) +(* ~ the classes of sets `F` and `G` intersect *) (* *) (* ## 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 *) -(* ``` *) +(* `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` *) (* *) (* ## Relations *) (* Notations for composition and inverse (scope: relation_scope): *) -(* ``` *) -(* B \; A == [set x | exists z, A (x.1, z) & B (z, x.2)] *) -(* A^-1 == [set xy | A (xy.2, xy.1)] *) -(* ``` *) +(* `B \; A` *) +(* ~ `[set x | exists z, A (x.1, z) & B (z, x.2)]` *) +(* *) +(* `A^-1` *) +(* ~ `[set xy | A (xy.2, xy.1)]` *) (* *) (******************************************************************************) diff --git a/classical/contra.v b/classical/contra.v index ba36be4f4d..b18198f10d 100644 --- a/classical/contra.v +++ b/classical/contra.v @@ -13,35 +13,36 @@ Unset Printing Implicit Defensive. (* This file provides tactics to reason by contraposition and contradiction. *) (* *) (* ## Tactics *) -(* ``` *) -(* assume_not == add a goal negation assumption. The tactic also works for *) -(* goals in Type, simplifies the added assumption, and *) -(* exposes its top-level constructive content. *) -(* absurd_not == proof by contradiction. Same as assume_not, but the goal is *) -(* erased and replaced by False. *) -(* Caveat: absurd_not cannot be used as a move/ view because *) -(* its conclusion is indeterminate. The more general notP can *) -(* be used instead. *) -(* contra == proof by contraposition. Change a goal of the form *) -(* assumption -> conclusion to ~ conclusion -> ~ assumption. *) -(* As with assume_not, contra allows both assumption and *) -(* conclusion to be in Type, simplifies the negation of both *) -(* assumption and conclusion, and exposes the constructive *) -(* contents of the negated conclusion. *) -(* The contra tactic also supports a limited form of the ':' *) -(* discharge pseudo tactical, whereby contra: means *) -(* move: ; contra. *) -(* The only allowed are one term, possibly preceded *) -(* by a clear switch. *) -(* absurd == proof by contradiction. The defective form of the tactic *) -(* simply replaces the entire goal with False (just as the Ltac *) -(* exfalso), leaving the user to derive a contradiction from *) -(* the assumptions. *) -(* The ':' form absurd: replaces the goal with the *) -(* negation of the (single) (as with contra:, a clear *) -(* switch is also allowed. *) -(* Finally the Ltac absurd term form is also supported. *) -(* ``` *) +(* `assume_not` *) +(* ~ add a goal negation assumption. The tactic also works for goals *) +(* in `Type`, simplifies the added assumption, and exposes its *) +(* top-level constructive content. *) +(* *) +(* `absurd_not` *) +(* ~ proof by contradiction. Same as `assume_not`, but the goal is *) +(* erased and replaced by `False`. Caveat: `absurd_not` cannot be *) +(* used as a `move/` view because its conclusion is indeterminate. *) +(* The more general `notP` can be used instead. *) +(* *) +(* `contra` *) +(* ~ proof by contraposition. Change a goal of the form *) +(* `assumption -> conclusion` to `~ conclusion -> ~ assumption`. As *) +(* with `assume_not`, `contra` allows both assumption and conclusion *) +(* to be in `Type`, simplifies the negation of both assumption and *) +(* conclusion, and exposes the constructive contents of the negated *) +(* conclusion. The `contra` tactic also supports a limited form of *) +(* the `':'` discharge pseudo tactical, whereby `contra: ` *) +(* means `move: ; contra`. The only `` allowed are *) +(* one term, possibly preceded by a clear switch. *) +(* *) +(* `absurd` *) +(* ~ proof by contradiction. The defective form of the tactic simply *) +(* replaces the entire goal with `False` (just as the Ltac *) +(* `exfalso`), leaving the user to derive a contradiction from the *) +(* assumptions. The `':'` form `absurd: ` replaces the goal *) +(* with the negation of the (single) `` (as with `contra:`, *) +(* a clear switch is also allowed. Finally the `Ltac absurd term` *) +(* form is also supported. *) (******************************************************************************) (** Hiding module for the internal definitions and lemmas used by the tactics @@ -534,7 +535,7 @@ Canonical eq_op_pos T x y := PositedBool (@eq_op_posP T x y). (******************************************************************************) (**md**************************************************************************) -(* Similarly to negatedProp, witnessedType returns the witness proposition *) +(* Similarly to negatedProp, witnessedType returns the witness proposition *) (* via a projection argument P, but does not need to signal "trivial" *) (* instances as the default value for P is nontrivial (namely, inhabited T), *) (* while the "trivial" case where P = T is actually desireable and handled *) diff --git a/classical/filter.v b/classical/filter.v index b26d00d72f..62fd2b88a7 100644 --- a/classical/filter.v +++ b/classical/filter.v @@ -14,33 +14,46 @@ From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval. (* a (set_system T) is really a filter in T, as a Filter or Properfilter. *) (* *) (* ## Structure of filter *) -(* ``` *) -(* filteredType U == interface type for types whose elements *) -(* represent sets of sets on U *) -(* These sets are intended to be filters on U *) -(* but this is not enforced yet. *) -(* The HB class is called Filtered. *) -(* It extends Pointed. *) -(* nbhs p == set of sets associated to p (in a filtered *) -(* type) *) -(* pfilteredType U == a pointed and filtered type *) -(* hasNbhs == factory for filteredType *) -(* nbhsType == type of a structure that has a set system *) -(* of neighborhoods associated to each point *) -(* pnbhsType == same has nbhsType for pointed types *) -(* continuous f == f is continuous w.r.t the topology *) -(* isSubNbhs V S U == interface that states the continuity of val *) -(* for U which has a subChoiceType and a *) -(* nbhsType *) -(* subNbhsType V S == structure that extends a *) -(* subChoiceType/nbhsType with the isSubNbhs *) -(* interface *) -(* The HB class is SubNbhs. *) -(* filterI_iter F n == nth stage of recursively building the *) -(* filter of finite intersections of F *) -(* finI_from D f == set of \bigcap_(i in E) f i where E is a *) -(* a finite subset of D *) -(* ``` *) +(* `filteredType U` *) +(* ~ interface type for types whose elements represent sets of sets *) +(* on `U` These sets are intended to be filters on `U` but this is *) +(* not enforced yet. The HB class is called `Filtered`. It extends *) +(* `Pointed`. *) +(* *) +(* `nbhs p` *) +(* ~ set of sets associated to `p` (in a filtered type) *) +(* *) +(* `pfilteredType U` *) +(* ~ a pointed and filtered type *) +(* *) +(* `hasNbhs` *) +(* ~ factory for `filteredType` *) +(* *) +(* `nbhsType` *) +(* ~ type of a structure that has a set system of neighborhoods *) +(* associated to each point *) +(* *) +(* `pnbhsType` *) +(* ~ same has `nbhsType` for pointed types *) +(* *) +(* `continuous f` *) +(* ~ `f` is continuous w.r.t the topology *) +(* *) +(* `isSubNbhs V S U` *) +(* ~ interface that states the continuity of val for `U` which has a *) +(* `subChoiceType` and a `nbhsType` *) +(* *) +(* `subNbhsType V S` *) +(* ~ structure that extends a `subChoiceType`/`nbhsType` with the *) +(* `isSubNbhs` interface The HB class is `SubNbhs`. *) +(* *) +(* `filterI_iter F n` *) +(* ~ nth stage of recursively building the filter of finite *) +(* intersections of `F` *) +(* *) +(* `finI_from D f` *) +(* ~ set of `\bigcap_(i in E) f i` where `E` is a a finite subset of *) +(* `D` *) (* *) (* We endow several standard types with the structure of filter, e.g.: *) (* - products `(X1 * X2)%type` *) @@ -48,83 +61,115 @@ From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval. (* - natural numbers `nat` *) (* *) (* ## Theory of filters *) -(* ``` *) -(* filter_from D B == set of the supersets of the elements *) -(* of the family of sets B whose indices *) -(* are in the domain D *) -(* This is a filter if (B_i)_(i in D) *) -(* forms a filter base. *) -(* filter_prod F G == product of the filters F and G *) -(* F `=>` G <-> G is included in F *) -(* F and G are sets of sets. *) -(* \oo == "eventually" filter on nat: set of *) -(* predicates on natural numbers that are *) -(* eventually true *) -(* F --> G <-> the canonical filter associated to G *) -(* is included in the canonical filter *) -(* associated to F *) -(* lim F == limit of the canonical filter *) -(* associated with F if there is such a *) -(* limit, i.e., an element l such that *) -(* the canonical filter associated to l *) -(* is a subset of F *) -(* [lim F in T] == limit of the canonical filter *) -(* associated to F in T where T has type *) -(* filteredType U *) -(* [cvg F in T] <-> the canonical filter associated to F *) -(* converges in T *) -(* cvg F <-> same as [cvg F in T] where T is *) -(* inferred from the type of the *) -(* canonical filter associated to F *) -(* Filter F == type class proving that the set of *) -(* sets F is a filter *) -(* ProperFilter F == type class proving that the set of *) -(* sets F is a proper filter *) -(* UltraFilter F == type class proving that the set of *) -(* sets F is an ultrafilter *) -(* filter_on T == interface type for sets of sets on T *) -(* that are filters *) -(* FilterType F FF == packs the set of sets F with the proof *) -(* FF of Filter F to build a filter_on T *) -(* structure *) -(* pfilter_on T == interface type for sets of sets on T *) -(* that are proper filters *) -(* PFilterPack F FF == packs the set of sets F with the proof *) -(* FF of ProperFilter F to build a *) -(* pfilter_on T structure *) -(* fmap f F == image of the filter F by the function *) -(* f *) -(* E @[x --> F] == image of the canonical filter *) -(* associated to F by the function *) -(* (fun x => E) *) -(* f @ F == image of the canonical filter *) -(* associated to F by the function f *) -(* fmapi f F == image of the filter F by the relation *) -(* f *) -(* E `@[x --> F] == image of the canonical filter *) -(* associated to F by the relation *) -(* (fun x => E) *) -(* f `@ F == image of the canonical filter *) -(* associated to F by the relation f *) -(* globally A == filter of the sets containing A *) -(* @frechet_filter T := [set S : set T | finite_set (~` S)] *) -(* a.k.a. cofinite filter *) -(* within D F == restriction of the filter F to the *) -(* domain D *) -(* principal_filter x == filter containing every superset of x *) -(* principal_filter_type == alias for choice types with principal *) -(* filters *) -(* subset_filter F D == similar to within D F, but with *) -(* dependent types *) -(* powerset_filter_from F == the filter of downward closed subsets *) -(* of F. *) -(* Enables use of near notation to pick *) -(* suitably small members of F *) -(* in_filter F == interface type for the sets that *) -(* belong to the set of sets F *) -(* InFilter FP == packs a set P with a proof of F P to *) -(* build a in_filter F structure *) -(* ``` *) +(* `filter_from D B` *) +(* ~ set of the supersets of the elements of the family of sets `B` *) +(* whose indices are in the domain `D` This is a filter if *) +(* `(B_i)_(i in D)` forms a filter base. *) +(* *) +(* `filter_prod F G` *) +(* ~ product of the filters `F` and `G` *) +(* *) +(* ``F `=>` G`` *) +(* ~ `G` is included in `F` `F` and `G` are sets of sets. *) +(* *) +(* `\oo` *) +(* ~ "eventually" filter on `nat`: set of predicates on natural *) +(* numbers that are eventually true *) +(* *) +(* `F --> G` *) +(* ~ the canonical filter associated to `G` is included in the *) +(* canonical filter associated to `F` *) +(* *) +(* `lim F` *) +(* ~ limit of the canonical filter associated with `F` if there is *) +(* such a limit, i.e., an element `l` such that the canonical *) +(* filter associated to `l` is a subset of `F` *) +(* *) +(* `[lim F in T]` *) +(* ~ limit of the canonical filter associated to `F` in `T` where *) +(* `T` has type `filteredType U` *) +(* *) +(* `[cvg F in T]` *) +(* ~ the canonical filter associated to `F` converges in `T` *) +(* *) +(* `cvg F` *) +(* ~ same as `[cvg F in T]` where `T` is inferred from the type of *) +(* the canonical filter associated to `F` *) +(* *) +(* `Filter F` *) +(* ~ type class proving that the set of sets `F` is a filter *) +(* *) +(* `ProperFilter F` *) +(* ~ type class proving that the set of sets `F` is a proper filter *) +(* *) +(* `UltraFilter F` *) +(* ~ type class proving that the set of sets `F` is an ultrafilter *) +(* *) +(* `filter_on T` *) +(* ~ interface type for sets of sets on `T` that are filters *) +(* *) +(* `FilterType F FF` *) +(* ~ packs the set of sets `F` with the proof `FF` of `Filter F` to *) +(* build a `filter_on T` structure *) +(* *) +(* `pfilter_on T` *) +(* ~ interface type for sets of sets on `T` that are proper filters *) +(* *) +(* `PFilterPack F FF` *) +(* ~ packs the set of sets `F` with the proof `FF` of *) +(* `ProperFilter F` to build a `pfilter_on T` structure *) +(* *) +(* `fmap f F` *) +(* ~ image of the filter `F` by the function `f` *) +(* *) +(* `E @[x --> F]` *) +(* ~ image of the canonical filter associated to `F` by the function *) +(* `(fun x => E)` *) +(* *) +(* `f @ F` *) +(* ~ image of the canonical filter associated to `F` by the function *) +(* `f` *) +(* *) +(* `fmapi f F` *) +(* ~ image of the filter `F` by the relation `f` *) +(* *) +(* ``E `@[x --> F]`` *) +(* ~ image of the canonical filter associated to `F` by the relation *) +(* `(fun x => E)` *) +(* *) +(* ``f `@ F`` *) +(* ~ image of the canonical filter associated to `F` by the relation *) +(* `f` *) +(* *) +(* `globally A` *) +(* ~ filter of the sets containing `A` *) +(* *) +(* `@frechet_filter T` *) +(* ~ ``[set S : set T | finite_set (~` S)]`` a.k.a. cofinite *) +(* filter *) +(* *) +(* `within D F` *) +(* ~ restriction of the filter `F` to the domain `D` *) +(* *) +(* `principal_filter x` *) +(* ~ filter containing every superset of `x` *) +(* *) +(* `principal_filter_type` *) +(* ~ alias for choice types with principal filters *) +(* *) +(* `subset_filter F D` *) +(* ~ similar to `within D F`, but with dependent types *) +(* *) +(* `powerset_filter_from F` *) +(* ~ the filter of downward closed subsets of `F`. Enables use of *) +(* near notation to pick suitably small members of `F` *) +(* *) +(* `in_filter F` *) +(* ~ interface type for the sets that belong to the set of sets `F` *) +(* *) +(* `InFilter FP` *) +(* ~ packs a set `P` with a proof of `F P` to build a `in_filter F` *) +(* structure *) (* *) (* ## Near notations and tactics *) (* The purpose of the near notations and tactics is to make the manipulation *) @@ -135,26 +180,34 @@ From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval. (* instantiated during the proof process. *) (* *) (* ### Notations *) -(* ``` *) -(* {near F, P} == the property P holds near the *) -(* canonical filter associated to F *) -(* P must have the form forall x, Q x. *) -(* Equivalent to F Q. *) -(* Prefer this notation when P is an *) -(* existing statement to be relativised *) -(* (i.e., has its own definition). *) -(* \forall x \near F, P x <-> F (fun x => P x). *) -(* Prefer this notation when the *) -(* statement forall x, P x does not stand *) -(* alone. *) -(* \near x, P x := \forall y \near x, P y. *) -(* {near F & G, P} == same as {near H, P}, where H is the *) -(* product of the filters F and G *) -(* \forall x \near F & y \near G, P x y := {near F & G, forall x y, P x y} *) -(* \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 *) -(* ``` *) +(* `{near F, P}` *) +(* ~ the property `P` holds near the canonical filter associated to *) +(* `F` `P` must have the form `forall x, Q x`. Equivalent to *) +(* `F Q`. Prefer this notation when `P` is an existing statement *) +(* to be relativised (i.e., has its own definition). *) +(* *) +(* `\forall x \near F, P x` *) +(* ~ `F (fun x => P x)`. Prefer this notation when the statement *) +(* `forall x, P x` does not stand alone. *) +(* *) +(* `\near x, P x` *) +(* ~ `\forall y \near x, P y`. *) +(* *) +(* `{near F & G, P}` *) +(* ~ same as `{near H, P}`, where `H` is the product of the filters *) +(* `F` and `G` *) +(* *) +(* `\forall x \near F & y \near G, P x y` *) +(* ~ `{near F & G, forall x y, P x y}` *) +(* *) +(* `\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. *) diff --git a/classical/fsbigop.v b/classical/fsbigop.v index fa80b125e1..76bcafc9be 100644 --- a/classical/fsbigop.v +++ b/classical/fsbigop.v @@ -8,12 +8,15 @@ From mathcomp Require Import functions cardinality. (**md**************************************************************************) (* # 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 *) -(* ``` *) +(* `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 3a98909ca3..d7bb23151e 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -15,129 +15,202 @@ Add Search Blacklist "_mixin_". (* 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 *) -(* set_inj A B f == f is injective *) -(* set_bij A B f == f is bijective *) +(* `set_fun A B f` *) +(* ~ `f : aT -> rT` is a function with domain `A : set aT` and *) +(* codomain `B : set rT` *) (* *) -(* {fun A >-> B} == type of functions f : aT -> rT from A : set aT *) -(* to B : set rT *) -(* `funS f` is a proof of `set_fun A B f`. *) -(* {oinv aT >-> rT} == type of functions with a partial inverse *) -(* {oinvfun A >-> B} == combination of {fun A >-> B} and *) -(* {oinv aT >-> rT} *) -(* {inv aT >-> rT} == type of functions with an inverse *) -(* f ^-1 == inverse of f : {inv aT >-> rT} *) -(* {invfun A >-> B} == combination of {fun A >-> B} and {inv aT >-> rT} *) -(* {surj A >-> B} == type of surjective functions *) -(* {surjfun A >-> B} == combination of {fun A >-> B} and {surj A >-> B} *) -(* {splitsurj A >-> B} == type of surjective functions with an inverse *) -(* {splitsurjfun A >-> B} == combination of {fun A >-> B} and *) -(* {splitsurj A >-> B} *) -(* {inj A >-> rT} == type of injective functions *) -(* {injfun A >-> B} == combination of {fun A >-> B} and {inj A >-> rT} *) -(* {splitinj A >-> B} == type of injective functions with an inverse *) -(* {splitinjfun A >-> B} == combination of {fun A >-> B} and *) -(* {splitinj A >-> B} *) -(* {bij A >-> B} == combination of {injfun A >-> B} and *) -(* {surjfun A >-> B} *) -(* {splitbij A >-> B} == combination of {splitinj A >-> B} and *) -(* {splitsurj A >-> B} *) -(* 'inj_ f == proof of {in A &, injective f} where f has type *) -(* {splitinj A >-> _} *) -(* ``` *) +(* `set_surj A B f` *) +(* ~ `f` is surjective *) (* *) -(* ``` *) -(* [fun f in A] == the function f from the set A to the set f @` A *) -(* with f : aT -> rT and A : set aT *) -(* This is a notation for funin A f, which is an HB *) -(* alias. *) -(* 'split_ d f == partial injection from aT : Type to rT : Type, *) -(* f : aT -> rT, and d : rT -> aT *) -(* This is a notation for split_ d f which is an HB *) -(* alias. *) -(* split := 'split_(fun=> point) *) -(* @to_setT T == function that associates to x : T a dependent *) -(* pair of x with a proof that x belongs to setT *) -(* (i.e., the type set_type [set: T]) *) -(* incl AB == identity function from T to T, where AB is a *) -(* proof of A `<=` B, with A, B : set T *) -(* inclT A := incl (@subsetT _ _) *) -(* eqincl AB == identity function from T to T, where AB is a *) -(* proof of A = B, with A, B : set T *) -(* mkfun fAB == builds a function {fun A >-> B} given a function *) -(* f : aT -> rT and a proof fAB that *) -(* {homo f : x / A x >-> B x} *) -(* @set_val T A == injection from set_type A to T, where A has *) -(* type set T *) -(* @ssquash T == function of type *) -(* {splitsurj [set: T] >-> [set: $| T |]} *) -(* @finset_val T X == function that turns an element x : X *) -(* (with X : {fset T}) into a dependent pair of x *) -(* with a proof that x belongs to X *) -(* (i.e., the type set_type [set` X]) *) -(* @val_finset T X == function of type [set` X] -> X with X : {fset T} *) -(* that cancels finset_val *) -(* glue XY AB f g == function that behaves as f over X, as g over Y *) -(* XY is a proof that sets X and Y are disjoint, *) -(* AB is a proof that sets A and B are disjoint, *) -(* A and B are intended to be the ranges of f and g *) -(* 'pinv_ d A f == inverse of the function [fun f in A] over *) -(* f @` A, function d outside of f @` A *) -(* This is a notation for pinv_ which is defined as *) -(* the inverse of a partial injection ('split_). *) -(* pinv := 'pinv_(fun=> point) *) -(* ``` *) +(* `set_inj A B f` *) +(* ~ `f` is injective *) +(* *) +(* `set_bij A B f` *) +(* ~ `f` is bijective *) +(* *) +(* `{fun A >-> B}` *) +(* ~ type of functions `f : aT -> rT` from `A : set aT` to `B : set rT` *) +(* `funS f` is a proof of `set_fun A B f` *) +(* *) +(* `{oinv aT >-> rT}` *) +(* ~ type of functions with a partial inverse *) +(* *) +(* `{oinvfun A >-> B}` *) +(* ~ combination of `{fun A >-> B}` and `{oinv aT >-> rT}` *) +(* *) +(* `{inv aT >-> rT}` *) +(* ~ type of functions with an inverse *) +(* *) +(* `f ^-1` *) +(* ~ inverse of `f : {inv aT >-> rT}` *) +(* *) +(* `{invfun A >-> B}` *) +(* ~ combination of `{fun A >-> B}` and `{inv aT >-> rT}` *) +(* *) +(* `{surj A >-> B}` *) +(* ~ type of surjective functions *) +(* *) +(* `{surjfun A >-> B}` *) +(* ~ combination of `{fun A >-> B}` and `{surj A >-> B}` *) +(* *) +(* `{splitsurj A >-> B}` *) +(* ~ type of surjective functions with an inverse *) +(* *) +(* `{splitsurjfun A >-> B}` *) +(* ~ combination of `{fun A >-> B}` and `{splitsurj A >-> B}` *) +(* *) +(* `{inj A >-> rT}` *) +(* ~ type of injective functions *) +(* *) +(* `{injfun A >-> B}` *) +(* ~ combination of `{fun A >-> B}` and `{inj A >-> rT}` *) +(* *) +(* `{splitinj A >-> B}` *) +(* ~ type of injective functions with an inverse *) +(* *) +(* `{splitinjfun A >-> B}` *) +(* ~ combination of `{fun A >-> B}` and `{splitinj A >-> B}` *) +(* *) +(* `{bij A >-> B}` *) +(* ~ combination of `{injfun A >-> B}` and `{surjfun A >-> B}` *) +(* *) +(* `{splitbij A >-> B}` *) +(* ~ combination of `{splitinj A >-> B}` and `{splitsurj A >-> B}` *) +(* *) +(* `'inj_ f` *) +(* ~ proof of `{in A &, injective f}` where `f` has type *) +(* `{splitinj A >-> _}` *) +(* *) +(* `[fun f in A]` *) +(* ~ the function `f` from the set `A` to the set ``f @` A`` with *) +(* `f : aT -> rT` and `A : set aT` *) +(* This is a notation for `funin A f`, which is an HB alias. *) +(* *) +(* `'split_ d f` *) +(* ~ partial injection from `aT : Type` to `rT : Type`, `f : aT -> rT`, *) +(* and `d : rT -> aT` *) +(* This is a notation for `split_ d f` which is an HB alias. *) +(* *) +(* `split` *) +(* ~ `'split_(fun=> point)` *) +(* *) +(* `@to_setT T` *) +(* ~ function that associates to `x : T` a dependent pair of `x` with *) +(* a proof that `x` belongs to `setT` (i.e., the type *) +(* `set_type [set: T]`) *) +(* *) +(* `incl AB` *) +(* ~ identity function from `T` to `T`, where `AB` is a proof of *) +(* ``A `<=` B``, with `A, B : set T` *) +(* *) +(* `inclT A` *) +(* ~ `incl (@subsetT _ _)` *) +(* *) +(* `eqincl AB` *) +(* ~ identity function from `T` to `T`, where `AB` is a proof of *) +(* `A = B`, with `A, B : set T` *) +(* *) +(* `mkfun fAB` *) +(* ~ builds a function `{fun A >-> B}` given a function `f : aT -> rT` *) +(* and a proof `fAB` that `{homo f : x / A x >-> B x}` *) +(* *) +(* `@set_val T A` *) +(* ~ injection from `set_type A` to `T`, where `A` has type `set T` *) +(* *) +(* `@ssquash T` *) +(* ~ function of type `{splitsurj [set: T] >-> [set: $| T |]}` *) +(* *) +(* `@finset_val T X` *) +(* ~ function that turns an element `x : X` (with `X : {fset T}`) into *) +(* a dependent pair of `x` with a proof that `x` belongs to `X` *) +(* (i.e., the type ``set_type [set` X]``) *) +(* *) +(* `@val_finset T X` *) +(* ~ function of type ``[set` X] -> X`` with `X : {fset T}` that *) +(* cancels `finset_val` *) +(* *) +(* `glue XY AB f g` *) +(* ~ function that behaves as `f` over `X`, as `g` over `Y` *) +(* `XY` is a proof that sets `X` and `Y` are disjoint, `AB` is a *) +(* proof that sets `A` and `B` are disjoint, `A` and `B` are *) +(* intended to be the ranges of `f` and `g` *) +(* *) +(* `'pinv_ d A f` *) +(* ~ inverse of the function `[fun f in A]` over ``f @` A``, function *) +(* `d` outside of ``f @` A`` *) +(* This is a notation for `pinv_` which is defined as the inverse *) +(* of a partial injection (`'split_`). *) +(* *) +(* `pinv` *) +(* ~ `'pinv_(fun=> point)` *) (* *) (* ## 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 *) -(* f \_ D := restrict D f *) -(* sigL A f == "left restriction"; given a set A : set U and a *) -(* function f : U -> V, returns the corresponding *) -(* function of type set_type A -> V *) -(* sigR A f == "right restriction"; given a set B : set V and a *) -(* function f : {fun [set: U] >-> B}, returns the *) -(* corresponding function of type U -> set_type B *) -(* sigLR A B f == the function of type set_type A -> set_type B *) -(* corresponding to f : {fun A >-> B} *) -(* valL_ v == function cancelled by sigL A, with A : set U and *) -(* v : V *) -(* valR f == the function of type U -> V corresponding to *) -(* f : U -> set_type B, with B : set V *) -(* valR_fun == the function of type {fun [set: U] >-> B} *) -(* corresponding to f : U -> set_type B, with *) -(* B : set V *) -(* valLR v f == the function of type U -> V corresponding to *) -(* f : set_type A -> set_type B (where v : V), *) -(* i.e., 'valL_ v \o valR_fun *) -(* 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 *) -(* ``` *) +(* `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` *) +(* *) +(* `f \_ D` *) +(* ~ `restrict D f` *) +(* *) +(* `sigL A f` *) +(* ~ "left restriction"; given a set `A : set U` and a function *) +(* `f : U -> V`, returns the corresponding function of type *) +(* `set_type A -> V` *) +(* *) +(* `sigR A f` *) +(* ~ "right restriction"; given a set `B : set V` and a function *) +(* `f : {fun [set: U] >-> B}`, returns the corresponding function *) +(* of type `U -> set_type B` *) +(* *) +(* `sigLR A B f` *) +(* ~ the function of type `set_type A -> set_type B` corresponding to *) +(* `f : {fun A >-> B}` *) +(* *) +(* `valL_ v` *) +(* ~ function cancelled by `sigL A`, with `A : set U` and `v : V` *) +(* *) +(* `valR f` *) +(* ~ the function of type `U -> V` corresponding to *) +(* `f : U -> set_type B`, with `B : set V` *) +(* *) +(* `valR_fun` *) +(* ~ the function of type `{fun [set: U] >-> B}` corresponding to *) +(* `f : U -> set_type B`, with `B : set V` *) +(* *) +(* `valLR v f` *) +(* ~ the function of type `U -> V` corresponding to *) +(* `f : set_type A -> set_type B` (where `v : V`), i.e., *) +(* `'valL_ v \o valR_fun` *) +(* *) +(* `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 `nmodType`, `zmodType`, `ringType`, `comRingType`, and *) +(* `lmodType` structures for functions whose range is `nmodType`, *) +(* `zmodType`, `ringType`, `comRingType`, and `lmodType` resp. *) +(* *) +(* `fctE` *) +(* ~ multi-rule for `fct` *) (* *) -(* ``` *) -(* Section function_space == canonical nmodType, zmodType, ringType, *) -(* comRingType, and lmodType structures for *) -(* functions whose range is nmodType, zmodType, *) -(* ringType, comRingType, and lmodType resp. *) -(* fctE == multi-rule for fct *) -(* ``` *) +(* `linfun E F s` *) +(* ~ membership predicate for linear functions of type `E -> F` with *) +(* scalar operator `s : K -> F -> F` *) +(* `E` and `F` have type `lmodType K`. *) +(* This is used in particular to attach a type of `lmodType` to *) +(* `{linear E -> F | s}`. *) (* *) -(* ``` *) -(* linfun E F s == membership predicate for linear functions of *) -(* type E -> F with scalar operator *) -(* s : K -> F -> F *) -(* E and F have type lmodType K. *) -(* This is used in particular to attach a type of *) -(* lmodType to {linear E -> F | s}. *) -(* linfun_spec f == specification for membership of the linear *) -(* function f *) -(* ``` *) +(* `linfun_spec f` *) +(* ~ specification for membership of the linear function `f` *) (* *) (* *) (* *) diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 2c2c258b22..7e6d142dcc 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -8,11 +8,11 @@ From mathcomp Require Import all_ssreflect_compat finmap algebra. (* This files contains lemmas and definitions recently added in mathcomp, *) (* in order to be able to compile analysis with older versions of mathcomp. *) (* *) -(* ``` *) -(* proj i f == f i, where f : forall i, T i *) -(* dfwith f x == fun j => x if j = i, and f j otherwise *) -(* given x : T i *) -(* ``` *) +(* `proj i f` *) +(* ~ `f i`, where `f : forall i, T i` *) +(* *) +(* `dfwith f x` *) +(* ~ `fun j => x` if `j = i`, and `f j` otherwise, given `x : T i` *) (* *) (******************************************************************************) diff --git a/classical/set_interval.v b/classical/set_interval.v index 486bc42bce..61a4cf1f05 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -11,30 +11,52 @@ From mathcomp Require Import functions. (* *) (* 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) *) -(* set_itv_infty_set0 == multirule to simplify empty intervals *) -(* line_path a b t := (1 - t) * a + t * b, convexity operator over *) -(* a numDomainType *) -(* ndline_path == line_path a b with the constraint that a < b *) -(* 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 *) -(* itv_is_open_unbounded i == i is either `]x, +oo[, `]-oo, x[ or *) -(* `]-oo, +oo[ *) -(* itv_is_oo i == i is `]x, y[ *) -(* itv_open_ends i == i has open endpoints, i.e., it is one of the *) -(* two above *) -(* itv_is_closed_unbounded i == i is either `[x, +oo[, `]-oo, x] or *) -(* `]-oo, +oo[ *) -(* itv_is_cc i == i is `[x, y] *) -(* itv_closed_ends i == i has closed endpoints, i.e., it is one of *) -(* the two above *) -(* is_open_itv A == the set A can be written as an open interval *) -(* open_itv_cover A == the set A can be covered by open 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`) *) +(* *) +(* `set_itv_infty_set0` *) +(* ~ multirule to simplify empty intervals *) +(* *) +(* `line_path a b t` *) +(* ~ `(1 - t) * a + t * b`, convexity operator over a `numDomainType` *) +(* *) +(* `ndline_path` *) +(* ~ `line_path a b` with the constraint that `a < b` *) +(* *) +(* `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 *) +(* *) +(* `itv_is_open_unbounded i` *) +(* ~ `i` is either `` `]x, +oo[ ``, `` `]-oo, x[ `` or `` `]-oo, +oo[ `` *) +(* *) +(* `itv_is_oo i` *) +(* ~ `i` is `` `]x, y[ `` *) +(* *) +(* `itv_open_ends i` *) +(* ~ `i` has open endpoints, i.e., it is one of the two above *) +(* *) +(* `itv_is_closed_unbounded i` *) +(* ~ `i` is either `` `[x, +oo[ ``, `` `]-oo, x] `` or `` `]-oo, +oo[ `` *) +(* *) +(* `itv_is_cc i` *) +(* ~ `i` is `` `[x, y] `` *) +(* *) +(* `itv_closed_ends i` *) +(* ~ `i` has closed endpoints, i.e., it is one of the two above *) +(* *) +(* `is_open_itv A` *) +(* ~ the set `A` can be written as an open interval *) +(* *) +(* `open_itv_cover A` *) +(* ~ the set `A` can be covered by open intervals *) (* *) (* Naming convention for lemmas about intervals: *) (* ``` *) diff --git a/classical/unstable.v b/classical/unstable.v index 9d2432a9c1..2ebdeb2b60 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -13,32 +13,55 @@ From mathcomp Require Import vector archimedean interval matrix. (* Once a result is backported to mathcomp, please move it to mathcomp_extra.v*) (* and mention it in the changelog. *) (* *) -(* ``` *) -(* swap x := (x.2, x.1) *) -(* map_pair f x := (f x.1, f x.2) *) -(* 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 *) -(* decreasing_fun f == the function f is (strictly) decreasing *) -(* nondecreasing_seq u == the sequence u is non-decreasing *) -(* nonincreasing_seq u == the sequence u is non-increasing *) -(* monotonic A f := {in A &, {homo f : x y / x <= y}} \/ *) -(* {in A &, {homo f : x y /~ x <= y}} *) -(* strict_monotonic A f := {in A &, {homo f : x y / x < y}} \/ *) -(* {in A &, {homo f : x y /~ x < y}} *) -(* sigT_fun f := lifts a family of functions f into a function on *) -(* the dependent sum *) -(* prodA x := sends (X * Y) * Z to X * (Y * Z) *) -(* prodAr x := sends X * (Y * Z) to (X * Y) * Z *) -(* isSemiNorm f == f : K -> L is a seminorm *) -(* K is a numDomainType. *) -(* L is a lmodType K. *) -(* The HB class is SemiNorm. *) -(* isNorm f == f : K -> L is a norm *) -(* K is a numDomainType. *) -(* L is a lmodType K. *) -(* The HB class is Norm. *) -(* ``` *) +(* `swap x` *) +(* ~ `(x.2, x.1)` *) +(* *) +(* `map_pair f x` *) +(* ~ `(f x.1, f x.2)` *) +(* *) +(* `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 *) +(* *) +(* `decreasing_fun f` *) +(* ~ the function `f` is (strictly) decreasing *) +(* *) +(* `nondecreasing_seq u` *) +(* ~ the sequence `u` is non-decreasing *) +(* *) +(* `nonincreasing_seq u` *) +(* ~ the sequence `u` is non-increasing *) +(* *) +(* `monotonic A f` *) +(* ~ `{in A &, {homo f : x y / x <= y}} \/ *) +(* {in A &, {homo f : x y /~ x <= y}}` *) +(* *) +(* `strict_monotonic A f` *) +(* ~ `{in A &, {homo f : x y / x < y}} \/ *) +(* {in A &, {homo f : x y /~ x < y}}` *) +(* *) +(* `sigT_fun f` *) +(* ~ lifts a family of functions `f` into a function on the *) +(* dependent sum *) +(* *) +(* `prodA x` *) +(* ~ sends `(X * Y) * Z` to `X * (Y * Z)` *) +(* *) +(* `prodAr x` *) +(* ~ sends `X * (Y * Z)` to `(X * Y) * Z` *) +(* *) +(* `isSemiNorm f` *) +(* ~ `f : K -> L` is a seminorm K is a `numDomainType`. L is a *) +(* `lmodType K`. The HB class is `SemiNorm`. *) +(* *) +(* `isNorm f` *) +(* ~ `f : K -> L` is a norm K is a `numDomainType`. L is a *) +(* `lmodType K`. The HB class is `Norm`. *) (* *) (******************************************************************************) diff --git a/classical/wochoice.v b/classical/wochoice.v index 53b41b0901..52622e79a3 100644 --- a/classical/wochoice.v +++ b/classical/wochoice.v @@ -12,24 +12,49 @@ From mathcomp Require Import boolp contra. (* can be found in `classical_sets.v` but expressed with `Prop` instead of *) (* `bool` (in particular); there is likely to be more sharing in the future. *) (* *) -(* ``` *) -(* nonempty A := exists x, x \in A *) -(* {in <= S, P} == the predicate P holds for all subsets of S *) -(* P has type {pred T} -> Prop for T : predArgType. *) -(* maximal R z == z is a maximal element for the relation R *) -(* minimal R z == z is a minimal element for the relation R *) -(* upper_bound R A z == for all x in A, we have R x z *) -(* lower_bound R A z == for all x in A, we have R z x *) -(* preorder R == R is reflexive and transitive *) -(* partial_order R == R is an antisymmetric preorder *) -(* total_order R == R is a total partial order *) -(* minimum_of R A z := z \in A /\ lower_bound A z *) -(* maximum_of R A z := z \in A /\ upper_bound A z *) -(* well_order R == every non-empty subset has a unique minimum element *) -(* chain R C == the subset C is totally ordered *) -(* := {in C &, total R} *) -(* wo_chain R C := {in <= C, well_order R} *) -(* ``` *) +(* `nonempty A` *) +(* ~ `exists x, x \in A` *) +(* *) +(* `{in <= S, P}` *) +(* ~ the predicate `P` holds for all subsets of `S` *) +(* ~ `P` has type `{pred T} -> Prop` for `T : predArgType` *) +(* *) +(* `maximal R z` *) +(* ~ `z` is a maximal element for the relation `R` *) +(* *) +(* `minimal R z` *) +(* ~ `z` is a minimal element for the relation `R` *) +(* *) +(* `upper_bound R A z` *) +(* ~ for all `x` in `A`, we have `R x z` *) +(* *) +(* `lower_bound R A z` *) +(* ~ for all `x` in `A`, we have `R z x` *) +(* *) +(* `preorder R` *) +(* ~ `R` is reflexive and transitive *) +(* *) +(* `partial_order R` *) +(* ~ `R` is an antisymmetric preorder *) +(* *) +(* `total_order R` *) +(* ~ `R` is a total partial order *) +(* *) +(* `minimum_of R A z` *) +(* ~ `z \in A /\ lower_bound A z` *) +(* *) +(* `maximum_of R A z` *) +(* ~ `z \in A /\ upper_bound A z` *) +(* *) +(* `well_order R` *) +(* ~ every non-empty subset has a unique minimum element *) +(* *) +(* `chain R C` *) +(* ~ the subset `C` is totally ordered *) +(* ~ `:= {in C &, total R}` *) +(* *) +(* `wo_chain R C` *) +(* ~ `{in <= C, well_order R}` *) (* *) (******************************************************************************) diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index 2b11be374a..d16f3508af 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -61,62 +61,102 @@ From mathcomp Require Import mathcomp_extra interval_inference. (* | `maxe x y, mine x y` |==| notation for the maximum/minimum | *) (* *) (* Detailed documentation: *) -(* ``` *) -(* \bar R == coproduct of R and {+oo, -oo}; *) -(* notation for extended (R:Type) *) -(* r%:E == injects real numbers into \bar R *) -(* - x == opposite of x : \bar R *) -(* 0, 1, -1 == 0%R, 1%R%:E, - 1%R%:E *) -(* == %:R%:E with a sequence *) -(* of digits *) -(* - == - %:R%:E with a sequence *) -(* of digits *) -(* +%E, -%E, *%E == addition/opposite/multiplication for extended *) -(* reals *) -(* x^-1, x / y == inverse and division for extended reals *) -(* er_map (f : T -> T') == the \bar T -> \bar T' lifting of f *) -(* sqrte == square root for extended reals *) -(* `| x |%E == the absolute value of x *) -(* x ^+ n == iterated multiplication *) -(* x *+ n == iterated addition *) -(* +%dE, (x *+ n)%dE == dual addition/dual iterated addition for *) -(* extended reals (-oo + +oo = +oo instead of -oo) *) -(* Import DualAddTheory for related lemmas *) -(* x +? y == the addition of the extended real numbers x and *) -(* and y is defined, i.e., it is neither +oo - oo *) -(* nor -oo + oo *) -(* x *? y == the multiplication of the extended real numbers *) -(* x and y is not of the form 0 * +oo or 0 * -oo *) -(* x *^-1? y == the inverse commutes with the product *) -(* (_ <= _)%E, (_ < _)%E, == comparison relations for extended reals *) -(* (_ >= _)%E, (_ > _)%E *) -(* (\sum_(i in A) f i)%E == bigop-like notation in scope %E *) -(* (\prod_(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 *) -(* esg x == sign of x (0, -1, or +1, as an extended real) *) -(* ``` *) +(* `\bar R` *) +(* ~ coproduct of `R` and `{+oo, -oo}` *) +(* ~ notation for `extended (R:Type)` *) +(* *) +(* `r%:E` *) +(* ~ injects real numbers into `\bar R` *) +(* *) +(* `- x` *) +(* ~ opposite of `x : \bar R` *) +(* *) +(* `0, 1, -1` *) +(* ~ `0%R, 1%R%:E, - 1%R%:E` *) +(* *) +(* `` *) +(* ~ `%:R%:E` with `` a sequence of digits *) +(* *) +(* `-` *) +(* ~ `- %:R%:E` with `` a sequence of digits *) +(* *) +(* `+%E, -%E, *%E` *) +(* ~ addition/opposite/multiplication for extended reals *) +(* *) +(* `x^-1, x / y` *) +(* ~ inverse and division for extended reals *) +(* *) +(* `er_map (f : T -> T')` *) +(* ~ the `\bar T -> \bar T'` lifting of `f` *) +(* *) +(* `sqrte` *) +(* ~ square root for extended reals *) +(* *) +(* `` `| x |%E `` *) +(* ~ the absolute value of `x` *) +(* *) +(* `x ^+ n` *) +(* ~ iterated multiplication *) +(* *) +(* `x *+ n` *) +(* ~ iterated addition *) +(* *) +(* `+%dE, (x *+ n)%dE` *) +(* ~ dual addition/dual iterated addition for extended reals *) +(* (`-oo + +oo = +oo` instead of `-oo`) *) +(* ~ Import `DualAddTheory` for related lemmas *) +(* *) +(* `x +? y` *) +(* ~ the addition of the extended real numbers `x` and `y` is *) +(* defined, i.e., it is neither `+oo - oo` nor `-oo + oo` *) +(* *) +(* `x *? y` *) +(* ~ the multiplication of the extended real numbers `x` and `y` *) +(* is not of the form `0 * +oo` or `0 * -oo` *) +(* *) +(* `x *^-1? y` *) +(* ~ the inverse commutes with the product *) +(* *) +(* `(_ <= _)%E, (_ < _)%E, (_ >= _)%E, (_ > _)%E` *) +(* ~ comparison relations for extended reals *) +(* *) +(* `(\sum_(i in A) f i)%E` *) +(* ~ bigop-like notation in scope `%E` *) +(* *) +(* `(\prod_(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 *) +(* *) +(* `esg x` *) +(* ~ sign of `x` (`0`, `-1`, or `+1`, as an extended real) *) (* *) (* ## Signed extended real numbers *) -(* ``` *) -(* {posnum \bar R} == interface type for elements in \bar R that are *) -(* positive, c.f., interval_inference.v, *) -(* notation in scope %E *) -(* {nonneg \bar R} == interface types for elements in \bar R that are *) -(* non-negative, c.f. interval_inference.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 *) -(* ``` *) +(* `{posnum \bar R}` *) +(* ~ interface type for elements in `\bar R` that are positive, *) +(* c.f., `interval_inference.v`, notation in scope `%E` *) +(* *) +(* `{nonneg \bar R}` *) +(* ~ interface types for elements in `\bar R` that are *) +(* non-negative, c.f. `interval_inference.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 *) -(* ``` *) -(* 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] *) -(* ``` *) +(* `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]` *) (******************************************************************************) Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) diff --git a/reals/reals.v b/reals/reals.v index 3e73e62d96..6b87049744 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -12,13 +12,16 @@ (* discrete real archimedean field with in particular a theory of floor and *) (* ceil. *) (* *) -(* ``` *) -(* realType == type of real numbers *) -(* The HB class is Real. *) -(* sup A == where A : set R with R : realType, the supremum of A when *) -(* it exists, 0 otherwise *) -(* inf A := - sup (- A) *) -(* ``` *) +(* `realType` *) +(* ~ type of real numbers *) +(* ~ the HB class is `Real` *) +(* *) +(* `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: *) @@ -26,20 +29,30 @@ (* - 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 *) -(* floor_set x := [set y | Rtoint y /\ y <= x] *) -(* Rfloor x == the floor of x as a real number *) -(* range1 x := [set y |x <= y < x + 1] *) -(* Rceil x == the ceil of x as a real number, i.e., - Rfloor (- x) *) -(* ``` *) +(* `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 *) +(* *) +(* `floor_set x` *) +(* ~ `[set y | Rtoint y /\ y <= x]` *) +(* *) +(* `Rfloor x` *) +(* ~ the floor of `x` as a real number *) +(* *) +(* `range1 x` *) +(* ~ `[set y |x <= y < x + 1]` *) +(* *) +(* `Rceil x` *) +(* ~ the ceil of `x` as a real number, i.e., `- Rfloor (- x)` *) +(* *) +(* `@rational R` *) +(* ~ set of rational numbers of type `R : realType` *) (* *) -(* ``` *) -(* @rational R == set of rational numbers of type R : realType *) -(* @irrational R == the complement of rational R *) -(* ``` *) +(* `@irrational R` *) +(* ~ the complement of `rational R` *) (* *) (******************************************************************************) diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index 3c11addd26..af3f24c466 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -7,11 +7,14 @@ From mathcomp Require Import measure lebesgue_measure measurable_realfun. (**md**************************************************************************) (* # Basic facts about G-delta and F-sigma sets *) (* *) -(* ``` *) -(* Gdelta S == S is countable intersection of open sets *) -(* Gdelta_dense S == S is a countable intersection of dense open sets *) -(* Fsigma S == S is countable union of closed sets *) -(* ``` *) +(* `Gdelta S` *) +(* ~ `S` is countable intersection of open sets *) +(* *) +(* `Gdelta_dense S` *) +(* ~ `S` is a countable intersection of dense open sets *) +(* *) +(* `Fsigma S` *) +(* ~ `S` is countable union of closed sets *) (* *) (******************************************************************************) diff --git a/theories/cantor.v b/theories/cantor.v index f854cf6f2b..be21188a4d 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -12,11 +12,14 @@ From mathcomp Require Import cardinality reals topology. (* 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 *) -(* tree_of T == builds a topological tree with levels (T n) *) -(* ``` *) +(* `cantor_space` *) +(* ~ the Cantor space, with its canonical metric *) +(* *) +(* `cantor_like T` *) +(* ~ `perfect + compact + hausdroff + zero dimensional` *) +(* *) +(* `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. *) diff --git a/theories/convex.v b/theories/convex.v index 7f4e0c7299..50b35b5c75 100644 --- a/theories/convex.v +++ b/theories/convex.v @@ -13,28 +13,31 @@ From mathcomp Require Import reals topology. (* This file provides a small account of convexity using convex spaces, to be *) (* completed with material from InfoTheo. *) (* *) -(* ``` *) -(* convex_quasi_associative == quasi-associativity of the operator of *) -(* convex spaces *) -(* isConvexSpace R T == interface for convex spaces with *) -(* R : numDomainType *) -(* The HB class is ConvexSpace. *) -(* a <| t |> b == convexity operator *) -(* ``` *) +(* `convex_quasi_associative` *) +(* ~ quasi-associativity of the operator of convex spaces *) +(* *) +(* `isConvexSpace R T` *) +(* ~ interface for convex spaces with `R : numDomainType`. The HB *) +(* class is `ConvexSpace`. *) +(* *) +(* `a <| t |> b` *) +(* ~ convexity operator *) (* *) (* For `R : numDomainType`, `E : lmodType R` and `R` itself are shown to be *) (* convex spaces with the following aliases: *) -(* ``` *) -(* convex_lmodType E == E : lmodType R as a convex space *) -(* convex_numDomainType R == R : numDomainType as a convex space *) -(* ``` *) +(* `convex_lmodType E` *) +(* ~ `E : lmodType R` as a convex space *) +(* *) +(* `convex_numDomainType R` *) +(* ~ `R : numDomainType` as a convex space *) +(* *) +(* `convex_set A` *) +(* ~ `A : set M` is a convex set; `M` is an Lmodule over *) +(* `R : numDomainType` *) (* *) -(* ``` *) -(* convex_set A == A : set M is a convex set *) -(* M is an Lmodule over R : numDomainType *) -(* convex_function f == f : E -> R is a convex function *) -(* E is an Lmodule over R : numFieldType *) -(* ``` *) +(* `convex_function f` *) +(* ~ `f : E -> R` is a convex function; `E` is an Lmodule over *) +(* `R : numFieldType` *) (******************************************************************************) Reserved Notation "x <| p |> y" (format "x <| p |> y", at level 49). diff --git a/theories/derive.v b/theories/derive.v index 42d06dbe2a..8207cce8d9 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -18,17 +18,28 @@ From mathcomp Require Import prodnormedzmodule tvs normedtype landau. (* *) (* 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 *) -(* 'D_v f == the directional derivative of f along v *) -(* derivable f a v == the function f is derivable at a with direction v *) -(* The type of f is V -> W with V W : normedModType R *) -(* and R : numFieldType *) -(* f^`() == the derivative of f of domain R *) -(* f^`(n) == the nth derivative of f of domain R *) -(* ``` *) +(* `'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` *) +(* *) +(* `'D_v f` *) +(* ~ the directional derivative of `f` along `v` *) +(* *) +(* `derivable f a v` *) +(* ~ the function `f` is derivable at `a` with direction `v`. The *) +(* type of `f` is `V -> W` with `V W : normedModType R` and *) +(* `R : numFieldType` *) +(* *) +(* ``f^`()`` *) +(* ~ the derivative of `f` of domain `R` *) +(* *) +(* ``f^`(n)`` *) +(* ~ the nth derivative of `f` of domain `R` *) (* *) (* Naming convention in this file: *) (* - lemmas of the form `... -> derivable f x v` are named `derivable*` *) diff --git a/theories/ereal.v b/theories/ereal.v index 0e69d004bb..2ea99ab97a 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -17,36 +17,39 @@ From mathcomp Require Export interval_inference topology constructive_ereal. (* *) (* 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 *) +(* `(\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 *) -(* ``` *) +(* `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 *) -(* ``` *) -(* 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| *) -(* ``` *) +(* `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 *) -(* ``` *) -(* ereal_dnbhs x == filter on extended real numbers that *) -(* corresponds to the deleted neighborhood *) -(* x^' if x is a real number and to *) -(* predicates that are eventually true if x *) -(* is +oo/-oo. *) -(* ereal_nbhs x == same as ereal_dnbhs where dnbhs is *) -(* replaced with nbhs. *) -(* ereal_loc_seq x == sequence that converges to x in the set *) -(* of extended real numbers. *) -(* ``` *) +(* `ereal_dnbhs x` *) +(* ~ filter on extended real numbers that corresponds to the deleted *) +(* neighborhood `x^'` if `x` is a real number and to predicates *) +(* that are eventually true if `x` is `+oo`/`-oo` *) +(* *) +(* `ereal_nbhs x` *) +(* ~ same as `ereal_dnbhs` where `dnbhs` is replaced with `nbhs` *) +(* *) +(* `ereal_loc_seq x` *) +(* ~ sequence that converges to `x` in the set of extended real *) +(* numbers *) (* *) (******************************************************************************) diff --git a/theories/ess_sup_inf.v b/theories/ess_sup_inf.v index 160532919b..cf909875f0 100644 --- a/theories/ess_sup_inf.v +++ b/theories/ess_sup_inf.v @@ -8,11 +8,12 @@ From mathcomp Require Import measure lebesgue_measure measurable_realfun. (**md**************************************************************************) (* # Essential infimum and essential supremum *) (* *) -(* ``` *) -(* ess_sup f == essential supremum of the function f : T -> R where T is a *) -(* semiRingOfSetsType and R is a realType *) -(* ess_inf f == essential infimum *) -(* ``` *) +(* `ess_sup f` *) +(* ~ essential supremum of the function `f : T -> R` where `T` is a *) +(* `semiRingOfSetsType` and `R` is a `realType` *) +(* *) +(* `ess_inf f` *) +(* ~ essential infimum *) (* *) (******************************************************************************) diff --git a/theories/esum.v b/theories/esum.v index a04945c9b5..553c9502fe 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -12,15 +12,18 @@ From mathcomp Require Import topology sequences normedtype numfun. (* 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 *) -(* function whose codomain is included in the extended *) -(* 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 *) -(* ``` *) +(* `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 function whose *) +(* codomain is included in the extended 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 9546f690e1..6514c12918 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -17,20 +17,34 @@ From mathcomp Require Import sequences derive realfun convex. (* *) (* 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) *) +(* `pseries f x` *) +(* ~ `[series f n * x ^ n]_n` *) (* *) -(* expeR x == extended real number-valued exponential function *) -(* ln x == the natural logarithm, in ring_scope *) -(* lne x == the natural logarithm, in ereal_scope *) -(* s `^ r == power function, in ring_scope (assumes s >= 0) *) -(* e `^ r == power function, in ereal_scope (assumes e >= 0) *) -(* riemannR a == sequence n |-> 1 / (n.+1) `^ a where a has a type *) -(* of type realType *) -(* e `^?(r +? s) == validity condition for the distributivity of *) -(* the power of the addition, in ereal_scope *) -(* ``` *) +(* `pseries_diffs f i` *) +(* ~ `(i + 1) * f (i + 1)` *) +(* *) +(* `expeR x` *) +(* ~ extended real number-valued exponential function *) +(* *) +(* `ln x` *) +(* ~ the natural logarithm, in `ring_scope` *) +(* *) +(* `lne x` *) +(* ~ the natural logarithm, in `ereal_scope` *) +(* *) +(* ``s `^ r`` *) +(* ~ power function, in `ring_scope` (assumes `s >= 0`) *) +(* *) +(* ``e `^ r`` *) +(* ~ power function, in `ereal_scope` (assumes `e >= 0`) *) +(* *) +(* `riemannR a` *) +(* ~ sequence ``n |-> 1 / (n.+1) `^ a`` where `a` has a type of type *) +(* `realType` *) +(* *) +(* ``e `^?(r +? s)`` *) +(* ~ validity condition for the distributivity of the power of the *) +(* addition, in `ereal_scope` *) (* *) (******************************************************************************) diff --git a/theories/ftc.v b/theories/ftc.v index 5fed61ad38..790707d007 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -46,9 +46,8 @@ From mathcomp Require Import derive. (* with $F$ increasing and $G$ non-negative *) (* *) (* Detailed contents: *) -(* ``` *) -(* parameterized_integral mu a x f := \int[mu]_(t \in `[a, x] f t) *) -(* ``` *) +(* `parameterized_integral mu a x f` *) +(* ~ ``\int[mu]_(t \in `[a, x] f t)`` *) (* *) (******************************************************************************) diff --git a/theories/hoelder.v b/theories/hoelder.v index 7bd2947449..8b34694edf 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -17,30 +17,39 @@ From mathcomp Require Import lebesgue_integral numfun exp. (* most notably Minkowski's inequality, the convexity of the power function, *) (* and a definition of Lp-spaces. *) (* *) -(* ``` *) -(* 'N[mu]_p[f] == the Lp-norm of f with measure mu *) -(* hoelder_conjugate p == an extended real number q s.t. p^-1 + q^-1 = 1 *) -(* ``` *) +(* `'N[mu]_p[f]` *) +(* ~ the Lp-norm of `f` with measure `mu` *) +(* *) +(* `hoelder_conjugate p` *) +(* ~ an extended real number `q` s.t. `p^-1 + q^-1 = 1` *) (* *) (* Lp-spaces and properties of Lp-norms: *) (* *) -(* ``` *) -(* finite_norm mu p f := the L-norm of real-valued function f is finite *) -(* The parameter p is an extended real. *) -(* LfunType mu p1 == type of measurable functions f with a finite *) -(* L-norm *) -(* p1 is a proof that the extended real number p is *) -(* greater or equal to 1. *) -(* The HB class is Lfunction. *) -(* f \in Lfun == holds for f : LfunType mu p1 *) -(* ae_eq_op f g == boolean version of ae_eq, *) -(* ae_eq_op is canonically an equivalence relation *) -(* {mfun_mu, T1 >-> T2} == the quotient of measurable functions T1 -> T2, *) -(* quotiented by the equivalence relation ae_eq_op *) -(* LspaceType mu p1 == type of the elements of the Lp space for the *) -(* measure mu *) -(* mu.-Lspace p == Lp space as a set *) -(* ``` *) +(* `finite_norm mu p f` *) +(* ~ the L-norm of real-valued function `f` is finite. The *) +(* parameter `p` is an extended real *) +(* *) +(* `LfunType mu p1` *) +(* ~ type of measurable functions `f` with a finite L-norm. `p1` is *) +(* a proof that the extended real number `p` is greater or equal *) +(* to `1`. The HB class is `Lfunction` *) +(* *) +(* `f \in Lfun` *) +(* ~ holds for `f : LfunType mu p1` *) +(* *) +(* `ae_eq_op f g` *) +(* ~ boolean version of `ae_eq`, `ae_eq_op` is canonically an *) +(* equivalence relation *) +(* *) +(* `{mfun_mu, T1 >-> T2}` *) +(* ~ the quotient of measurable functions `T1 -> T2`, quotiented by *) +(* the equivalence relation `ae_eq_op` *) +(* *) +(* `LspaceType mu p1` *) +(* ~ type of the elements of the Lp space for the measure `mu` *) +(* *) +(* `mu.-Lspace p` *) +(* ~ Lp space as a set *) (* *) (******************************************************************************) diff --git a/theories/homotopy_theory/continuous_path.v b/theories/homotopy_theory/continuous_path.v index 7dfccbf51b..61456a60c4 100644 --- a/theories/homotopy_theory/continuous_path.v +++ b/theories/homotopy_theory/continuous_path.v @@ -9,14 +9,17 @@ From mathcomp Require Import cardinality fsbigop reals topology wedge_sigT. (* # Paths *) (* Paths from biPointed spaces. *) (* *) -(* ``` *) -(* mk_path ctsf f0 f1 == constructs a value in `pathType x y` given proofs *) -(* that the endpoints of `f` are `x` and `y` *) -(* reparameterize f phi == the path `f` with a different parameterization *) -(* chain_path f g == the path which follows f, then follows g *) -(* Only makes sense when `f one = g zero`. The *) -(* domain is the wedge of domains of `f` and `g`. *) -(* ``` *) +(* `mk_path ctsf f0 f1` *) +(* ~ constructs a value in `pathType x y` given proofs that the *) +(* endpoints of `f` are `x` and `y` *) +(* *) +(* `reparameterize f phi` *) +(* ~ the path `f` with a different parameterization *) +(* *) +(* `chain_path f g` *) +(* ~ the path which follows `f`, then follows `g`. Only makes sense *) +(* when `f one = g zero`. The domain is the wedge of domains of `f` *) +(* and `g`. *) (* The type `{path i from x to y in T}` is the continuous functions on the *) (* bipointed space i that go from x to y staying in T. It is endowed with *) (* - Topology via the compact-open topology *) diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index 8e6e196cde..68cdbaa5b4 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -13,24 +13,37 @@ From mathcomp Require Import cardinality fsbigop reals topology. (* at a single point. It's classicaly used in the proof that every free group *) (* is a fundamental group of some space. We also will use it as part of our *) (* construction of paths and path concatenation. *) -(* ``` *) -(* wedge_rel p0 x y == x and y are equal, or they are (p0 i) and *) -(* (p0 j) for some i and j *) -(* wedge p0 == the quotient of {i : X i} along `wedge_rel p0` *) -(* wedge_lift i == the lifting of elements of (X i) into the wedge *) -(* pwedge p0 == the wedge of ptopologicalTypes at their designated *) -(* point *) -(* wedge_fun f == lifts a family of functions on each component into *) -(* a function on the wedge, when they all agree at the *) -(* wedge point *) -(* wedge_prod == the mapping from the wedge as a quotient of sums to *) -(* the wedge as a subspace of the product topology. *) -(* It's an embedding when the index is finite. *) -(* bpwedge_shared_pt b == the shared point in the bpwedge. Either zero or one *) -(* depending on `b`. *) -(* bpwedge == wedge of two bipointed spaces gluing zero to one *) -(* bpwedge_lift == wedge_lift specialized to the bipointed wedge *) -(* ``` *) +(* `wedge_rel p0 x y` *) +(* ~ `x` and `y` are equal, or they are `(p0 i)` and `(p0 j)` for *) +(* some `i` and `j` *) +(* *) +(* `wedge p0` *) +(* ~ the quotient of `{i : X i}` along `wedge_rel p0` *) +(* *) +(* `wedge_lift i` *) +(* ~ the lifting of elements of `(X i)` into the wedge *) +(* *) +(* `pwedge p0` *) +(* ~ the wedge of `ptopologicalTypes` at their designated point *) +(* *) +(* `wedge_fun f` *) +(* ~ lifts a family of functions on each component into a function on *) +(* the wedge, when they all agree at the wedge point *) +(* *) +(* `wedge_prod` *) +(* ~ the mapping from the wedge as a quotient of sums to the wedge as *) +(* a subspace of the product topology. It's an embedding when the *) +(* index is finite. *) +(* *) +(* `bpwedge_shared_pt b` *) +(* ~ the shared point in the `bpwedge`. Either zero or one depending *) +(* on `b`. *) +(* *) +(* `bpwedge` *) +(* ~ wedge of two bipointed spaces gluing zero to one *) +(* *) +(* `bpwedge_lift` *) +(* ~ `wedge_lift` specialized to the bipointed wedge *) (* *) (* The type `wedge p0` is endowed with the structures of: *) (* - topology via `quotient_topology` *) diff --git a/theories/independence.v b/theories/independence.v index d65e088e1e..573d1f9e69 100644 --- a/theories/independence.v +++ b/theories/independence.v @@ -13,16 +13,19 @@ From mathcomp Require Import hoelder probability. (**md**************************************************************************) (* # Independence *) (* *) -(* ``` *) -(* independent_events I E == the events E indexed by the set I are *) -(* independent *) -(* The measurability of events is not assumed by *) -(* the definition. *) -(* mutual_independence I F == the set systems F indexed by I are independent *) -(* independent_RVs I X == the random variables X indexed by I are *) -(* independent *) -(* independent_RVs2 X Y == the random variables X and Y are independent *) -(* ``` *) +(* `independent_events I E` *) +(* ~ the events `E` indexed by the set `I` are independent *) +(* ~ the measurability of events is not assumed by the *) +(* definition *) +(* *) +(* `mutual_independence I F` *) +(* ~ the set systems `F` indexed by `I` are independent *) +(* *) +(* `independent_RVs I X` *) +(* ~ the random variables `X` indexed by `I` are independent *) +(* *) +(* `independent_RVs2 X Y` *) +(* ~ the random variables `X` and `Y` are independent *) (* *) (******************************************************************************) diff --git a/theories/kernel.v b/theories/kernel.v index 92c3b2dee0..bd8c5705a8 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -25,54 +25,87 @@ From mathcomp Require Import lebesgue_integral. (* ESOP 2017 *) (* - A. Klenke. Probability theory: A comprehensive course. 2014 *) (* *) -(* ``` *) -(* R.-ker X ~> Y == kernel from X to Y where X and Y are of type *) -(* measurableType *) -(* The HB class is Kernel. *) -(* kseries == countable sum of kernels *) -(* It is declared as an instance of the structure *) -(* Kernel. It will also be shown to be an instance of *) -(* SFiniteKernel if the sum is over s-finite kernels. *) -(* measure_fam_uub k == the kernel k is uniformly upper-bounded *) -(* R.-sfker X ~> Y == s-finite kernel *) -(* The HB class is SFiniteKernel. *) -(* kzero == kernel defined using the mzero measure *) -(* R.-sigmafker X ~> Y == sigma-finite transition kernel *) -(* The HB class is SigmaFiniteTransitionKernel. *) -(* R.-ftker X ~> Y == finite transition kernel *) -(* The HB class is FiniteTransitionKernel. *) -(* R.-fker X ~> Y == finite kernel *) -(* The HB class is FiniteKernel. *) -(* R.-spker X ~> Y == subprobability kernel *) -(* The HB class is SubProbabilityKernel. *) -(* R.-pker X ~> Y == probability kernel *) -(* The HB class is ProbabilityKernel. *) -(* kdirac mf == kernel defined by a measurable function *) -(* kprobability m == kernel defined by a probability measure *) -(* kadd k1 k2 == lifting of the addition of measures to kernels *) -(* knormalize f P := fun x => mnormalize (f x) P *) -(* kcomp l k == "parameterized" composition for kernels *) -(* l has type X -> {measure set Y -> \bar R} *) -(* k has type X * Y -> {measure set Z -> \bar R} *) -(* kcomp l k as type X -> set Z -> \bar R *) -(* l \; k == same as kcomp l k but equipped with the type *) -(* X -> {measure set Z -> \bar R} *) -(* kfcomp k f == composition of a "kernel" and a function *) -(* k has type X -> {measure set Y -> \bar R}. *) -(* kproduct k1 k2 == "parameterized" product of kernels *) -(* k1 has type T0 -> {measure set T1 -> \bar R}. *) -(* k2 has type T0 * T1 -> {measure set T2 -> \bar R}. *) -(* The result has type T0 -> set (T1 * T2) -> \bar R. *) -(* mkproduct k1 k2 == same as kproduct k1 k2 but equipped with the type *) -(* T0 -> {measure set (T1 * T2) -> \bar R} *) -(* kproduct_snd k1 k2 := kproduct k1 (k2 \o snd) *) -(* k2 has T1 -> {measure set T2 -> \bar R} *) -(* It "ignores" the first argument of k2. *) -(* kcomp_noparam k1 k2 := composition of kernels *) -(* k1 has type T0 -> {measure set T1 -> \bar R}. *) -(* k2 has type T1 -> {measure set T2 -> \bar R}. *) -(* The return type is T0 -> set (T1 * T2) -> \bar R *) -(* ``` *) +(* `R.-ker X ~> Y` *) +(* ~ kernel from `X` to `Y` where `X` and `Y` are of type *) +(* `measurableType`. The HB class is `Kernel`. *) +(* *) +(* `kseries` *) +(* ~ countable sum of kernels; it is declared as an instance of the *) +(* structure `Kernel`. It will also be shown to be an instance of *) +(* `SFiniteKernel` if the sum is over s-finite kernels. *) +(* *) +(* `measure_fam_uub k` *) +(* ~ the kernel `k` is uniformly upper-bounded *) +(* *) +(* `R.-sfker X ~> Y` *) +(* ~ s-finite kernel. The HB class is `SFiniteKernel`. *) +(* *) +(* `kzero` *) +(* ~ kernel defined using the `mzero` measure *) +(* *) +(* `R.-sigmafker X ~> Y` *) +(* ~ sigma-finite transition kernel. The HB class is *) +(* `SigmaFiniteTransitionKernel`. *) +(* *) +(* `R.-ftker X ~> Y` *) +(* ~ finite transition kernel. The HB class is *) +(* `FiniteTransitionKernel`. *) +(* *) +(* `R.-fker X ~> Y` *) +(* ~ finite kernel. The HB class is `FiniteKernel`. *) +(* *) +(* `R.-spker X ~> Y` *) +(* ~ subprobability kernel. The HB class is `SubProbabilityKernel`. *) +(* *) +(* `R.-pker X ~> Y` *) +(* ~ probability kernel. The HB class is `ProbabilityKernel`. *) +(* *) +(* `kdirac mf` *) +(* ~ kernel defined by a measurable function *) +(* *) +(* `kprobability m` *) +(* ~ kernel defined by a probability measure *) +(* *) +(* `kadd k1 k2` *) +(* ~ lifting of the addition of measures to kernels *) +(* *) +(* `knormalize f P` *) +(* ~ `fun x => mnormalize (f x) P` *) +(* *) +(* `kcomp l k` *) +(* ~ "parameterized" composition for kernels; `l` has type *) +(* `X -> {measure set Y -> \bar R}`; `k` has type *) +(* `X * Y -> {measure set Z -> \bar R}`; `kcomp l k` as type *) +(* `X -> set Z -> \bar R` *) +(* *) +(* `l \; k` *) +(* ~ same as `kcomp l k` but equipped with the type *) +(* `X -> {measure set Z -> \bar R}` *) +(* *) +(* `kfcomp k f` *) +(* ~ composition of a "kernel" and a function; `k` has type *) +(* `X -> {measure set Y -> \bar R}`. *) +(* *) +(* `kproduct k1 k2` *) +(* ~ "parameterized" product of kernels; `k1` has type *) +(* `T0 -> {measure set T1 -> \bar R}`; `k2` has type *) +(* `T0 * T1 -> {measure set T2 -> \bar R}`; the result has type *) +(* `T0 -> set (T1 * T2) -> \bar R`. *) +(* *) +(* `mkproduct k1 k2` *) +(* ~ same as `kproduct k1 k2` but equipped with the type *) +(* `T0 -> {measure set (T1 * T2) -> \bar R}` *) +(* *) +(* `kproduct_snd k1 k2` *) +(* ~ `kproduct k1 (k2 \o snd)` *) +(* ~ `k2` has `T1 -> {measure set T2 -> \bar R}`; it "ignores" the *) +(* first argument of `k2` *) +(* *) +(* `kcomp_noparam k1 k2` *) +(* ~ composition of kernels; `k1` has type *) +(* `T0 -> {measure set T1 -> \bar R}`; `k2` has type *) +(* `T1 -> {measure set T2 -> \bar R}`; the return type is *) +(* `T0 -> set (T1 * T2) -> \bar R` *) (* *) (******************************************************************************) diff --git a/theories/landau.v b/theories/landau.v index 73c88b3a3d..bf0652e56d 100644 --- a/theories/landau.v +++ b/theories/landau.v @@ -33,63 +33,80 @@ From mathcomp Require Import prodnormedzmodule. (* using filter reasoning. *) (* *) (* ## 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, *) -(* this is the preferred way for statements. *) -(* expands to the equation (f = 'O_F h) *) -(* rewrite from LEFT to RIGHT only *) -(* f = g +O_F h == f is equal to g plus a bigO near F, *) -(* this is the preferred way for statements. *) -(* expands to the equation (f = g + 'O_F h) *) -(* rewrite from LEFT to RIGHT only *) -(* /!\ When you have to prove *) -(* (f =O_F h) or (f = g +O_F h). *) -(* you must (apply: eqOE) as soon as possible in a proof *) -(* in order to turn it into 'a_O_F f with a shelved content *) -(* /!\ under rare circumstances, a hint may do that for you *) -(* [O_F h of f] == returns a function with a bigO canonical structure *) -(* provably equal to f if f is indeed a bigO of h *) -(* provably equal to 0 otherwise *) -(* expands to ('O_F h) *) -(* 'O_F == pattern to match a bigO with a specific F *) -(* '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 *) -(* ``` *) +(* `[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`, this is the preferred way for *) +(* statements. expands to the equation `(f = 'O_F h)` rewrite *) +(* from LEFT to RIGHT only *) +(* *) +(* `f = g +O_F h` *) +(* ~ `f` is equal to `g` plus a bigO near `F`, this is the *) +(* preferred way for statements. expands to the equation *) +(* `(f = g + 'O_F h)` rewrite from LEFT to RIGHT only `/!\` When *) +(* you have to prove `(f =O_F h)` or `(f = g +O_F h)`. you must *) +(* `(apply: eqOE)` as soon as possible in a proof in order to *) +(* turn it into `'a_O_F f` with a shelved content `/!\` under *) +(* rare circumstances, a hint may do that for you *) +(* *) +(* `[O_F h of f]` *) +(* ~ returns a function with a bigO canonical structure provably *) +(* equal to `f` if `f` is indeed a bigO of `h` provably equal to *) +(* `0` otherwise expands to `('O_F h)` *) +(* *) +(* `'O_F` *) +(* ~ pattern to match a bigO with a specific `F` *) +(* *) +(* `'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: *) -(* ``` *) -(* {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. *) -(* ``` *) +(* `{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. *) (* *) (* ## 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) *) -(* ``` *) +(* `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 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 *) -(* 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 *) -(* ``` *) +(* `{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. *) (* *) (* Similar notations available for big-Theta. *) diff --git a/theories/lebesgue_integral_theory/giry.v b/theories/lebesgue_integral_theory/giry.v index 35bee8f840..d3b1cc7b84 100644 --- a/theories/lebesgue_integral_theory/giry.v +++ b/theories/lebesgue_integral_theory/giry.v @@ -7,25 +7,45 @@ From mathcomp Require Import lebesgue_measure lebesgue_integral. (**md**************************************************************************) (* # The Giry monad *) (* *) -(* ``` *) -(* m1 ≡μ m2 == m1 S = m2 S for any measurable set S *) -(* giry T R == the type of subprobability measures over T *) -(* giry_ev P A == the evaluation map `giryM T R -> [0, 1]` *) -(* preimg_giry_ev A == preimage of the sigma-algebra of extended real numbers *) -(* via the function giry_ev ^~ A *) -(* giry_measurable == the sigma-algebra generated by the countable unions of *) -(* preimg_giry_ev *) -(* giry_display == display of giry_measurable *) -(* giry_int mu f := \int[mu]_x f x *) -(* giry_map mf == the map of type giry T1 R -> giry T2 R *) -(* where mf is a proof that f : T1 -> T2 is measurable *) -(* giry_ret x == the unit of the Giry monad, i.e., \d_x *) -(* @giry_join _ T R == the multiplication of the Giry monad *) -(* type : giry (giry T R) R -> giry T R *) -(* giry_bind mu mf == the bind with mu : giry T1 R and f : T1 -> giry T2 R *) -(* giry_prod == product of type *) -(* giry T1 R * giry T2 R -> giry (T1 * T2) R *) -(* ``` *) +(* `m1 ≡μ m2` *) +(* ~ `m1 S = m2 S` for any measurable set `S` *) +(* *) +(* `giry T R` *) +(* ~ the type of subprobability measures over `T` *) +(* *) +(* `giry_ev P A` *) +(* ~ the evaluation map `giryM T R -> [0, 1]` *) +(* *) +(* `preimg_giry_ev A` *) +(* ~ preimage of the sigma-algebra of extended real numbers via *) +(* the function `giry_ev ^~ A` *) +(* *) +(* `giry_measurable` *) +(* ~ the sigma-algebra generated by the countable unions of *) +(* `preimg_giry_ev` *) +(* *) +(* `giry_display` *) +(* ~ display of `giry_measurable` *) +(* *) +(* `giry_int mu f` *) +(* ~ `\int[mu]_x f x` *) +(* *) +(* `giry_map mf` *) +(* ~ the map of type `giry T1 R -> giry T2 R` where `mf` is a proof *) +(* that `f : T1 -> T2` is measurable *) +(* *) +(* `giry_ret x` *) +(* ~ the unit of the Giry monad, i.e., `\d_x` *) +(* *) +(* `@giry_join _ T R` *) +(* ~ the multiplication of the Giry monad, of type *) +(* `giry (giry T R) R -> giry T R` *) +(* *) +(* `giry_bind mu mf` *) +(* ~ the bind with `mu : giry T1 R` and `f : T1 -> giry T2 R` *) +(* *) +(* `giry_prod` *) +(* ~ product of type `giry T1 R * giry T2 R -> giry (T1 * T2) R` *) (* *) (******************************************************************************) diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v index 22edbc7c27..37e83ab62e 100644 --- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v +++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v @@ -16,9 +16,8 @@ From mathcomp Require Import lebesgue_integral_dominated_convergence. (* # The Lebesgue Integral for real-valued functions *) (* *) (* Detailed contents: *) -(* ``` *) -(* Rintegral mu D f := fine (\int[mu]_(x in D) f x). *) -(* ``` *) +(* `Rintegral mu D f` *) +(* ~ `fine (\int[mu]_(x in D) f x)` *) (* *) (* This file recasts lemmas about `integral` to `Rintegral`. It also *) (* established that Continuous functions are dense in $L^1$. *) diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v index ffa046f9a2..dde7a4f8be 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integrable.v +++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v @@ -23,10 +23,9 @@ From mathcomp Require Import lebesgue_integral_nonneg. (* - Daniel Li, Intégration et applications, 2016 *) (* *) (* Detailed contents: *) -(* ``` *) -(* mu.-integrable D f == f is measurable over D and the integral of f *) -(* w.r.t. D is < +oo *) -(* ``` *) +(* `mu.-integrable D f` *) +(* ~ `f` is measurable over `D` and the integral of `f` w.r.t. `D` *) +(* is `< +oo` *) (* *) (******************************************************************************) diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v index a95c9db3ed..118dfa2c2c 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v @@ -28,12 +28,15 @@ From mathcomp Require Import measurable_realfun. (* - Daniel Li, Intégration et applications, 2016 *) (* *) (* Detailed contents: *) -(* ``` *) -(* sintegral mu f == integral of the function f with the measure mu *) -(* \int[mu]_(x in D) f x == integral of the measurable function f over the *) -(* domain D with measure mu *) -(* \int[mu]_x f x := \int[mu]_(x in setT) f x *) -(* ``` *) +(* `sintegral mu f` *) +(* ~ integral of the function `f` with the measure `mu` *) +(* *) +(* `\int[mu]_(x in D) f x` *) +(* ~ integral of the measurable function `f` over the domain `D` *) +(* with measure `mu` *) +(* *) +(* `\int[mu]_x f x` *) +(* ~ `\int[mu]_(x in setT) f x` *) (* *) (******************************************************************************) diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v index 78c7a90d4c..9abeb000aa 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v @@ -26,21 +26,29 @@ From mathcomp Require Import lebesgue_Rintegral. (* Differentiation Theorem in Coq. ITP 2024 *) (* *) (* Detailed contents: *) -(* ``` *) -(* locally_integrable D f == the real number-valued function f is locally *) -(* integrable on D *) -(* iavg f A := "average" of the real-valued function f over *) -(* the set A *) -(* HL_maximal == the Hardy–Littlewood maximal operator *) -(* input: real number-valued function *) -(* output: extended real number-valued function *) -(* davg f x r == "deviated average" of the real-valued function *) -(* f over ball x r *) -(* lim_sup_davg f x := lime_sup (davg f x) 0 *) -(* lebesgue_pt f x == Lebesgue point at x of the real-valued *) -(* function f *) -(* nicely_shrinking x E == the sequence of sets E is nicely shrinking to x *) -(* ``` *) +(* `locally_integrable D f` *) +(* ~ the real number-valued function `f` is locally integrable on `D` *) +(* *) +(* `iavg f A` *) +(* ~ "average" of the real-valued function `f` over the set `A` *) +(* *) +(* `HL_maximal` *) +(* ~ the Hardy–Littlewood maximal operator *) +(* input: real number-valued function *) +(* output: extended real number-valued function *) +(* *) +(* `davg f x r` *) +(* ~ "deviated average" of the real-valued function `f` over *) +(* `ball x r` *) +(* *) +(* `lim_sup_davg f x` *) +(* ~ `lime_sup (davg f x) 0` *) +(* *) +(* `lebesgue_pt f x` *) +(* ~ Lebesgue point at `x` of the real-valued function `f` *) +(* *) +(* `nicely_shrinking x E` *) +(* ~ the sequence of sets `E` is nicely shrinking to `x` *) (* *) (******************************************************************************) diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v index e1bb236551..c4a3f9bfa9 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v @@ -23,16 +23,16 @@ From mathcomp Require Import lebesgue_integral_nonneg lebesgue_integrable. (* Type Theory with Application to Integration. JAR 2023 *) (* *) (* Detailed contents: *) -(* ``` *) -(* m1 \x m2 == product measure over T1 * T2, m1 is a measure *) -(* over T1, and m2 is a sigma finite measure over *) -(* T2 *) -(* product_subprobability P == P.1 \x P.2 where P is a pair of subprobability *) -(* measures *) -(* m1 \x^ m2 == product measure over T1 * T2, m2 is a measure *) -(* over T1, and m1 is a sigma finite measure over *) -(* T2 *) -(* ``` *) +(* `m1 \x m2` *) +(* ~ product measure over `T1 * T2`, `m1` is a measure over `T1`, *) +(* and `m2` is a sigma finite measure over `T2` *) +(* *) +(* `product_subprobability P` *) +(* ~ `P.1 \x P.2` where `P` is a pair of subprobability measures *) +(* *) +(* `m1 \x^ m2` *) +(* ~ product measure over `T1 * T2`, `m2` is a measure over `T1`, *) +(* and `m1` is a sigma finite measure over `T2` *) (* *) (******************************************************************************) diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_under.v b/theories/lebesgue_integral_theory/lebesgue_integral_under.v index 623341da55..79ac42d04b 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_under.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_under.v @@ -15,10 +15,9 @@ From mathcomp Require Import lebesgue_integral_dominated_convergence. (* # Continuity and differentiation under the integral sign *) (* *) (* Detailed contents: *) -(* ``` *) -(* partial1of2 f == first partial derivative of f *) -(* f has type R -> T -> R for R : realType *) -(* ``` *) +(* `partial1of2 f` *) +(* ~ first partial derivative of `f`. `f` has type `R -> T -> R` for *) +(* `R : realType` *) (******************************************************************************) Reserved Notation "'d1 f" (at level 10, f at next level, format "''d1' f"). diff --git a/theories/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v index 39838199fc..b9bdcd16da 100644 --- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v +++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v @@ -18,16 +18,17 @@ From mathcomp Require Import measurable_realfun simple_functions. (* Main reference: *) (* - Daniel Li, Intégration et applications, 2016 *) (* *) -(* ``` *) -(* dyadic_itv n k == the interval *) -(* `[(k%:R * 2 ^- n), (k.+1%:R * 2 ^- n)[ *) -(* approx D f == nondecreasing sequence of functions that *) -(* approximates f over D using dyadic intervals *) -(* It uses the sets dyadic_approx and *) -(* integer_approx. *) -(* nnsfun_approx D f == same as approx D f but as a nnsfun *) -(* approximates f over D using dyadic intervals *) -(* ``` *) +(* `dyadic_itv n k` *) +(* ~ the interval `` `[(k%:R * 2 ^- n), (k.+1%:R * 2 ^- n)[ `` *) +(* *) +(* `approx D f` *) +(* ~ nondecreasing sequence of functions that approximates `f` over *) +(* `D` using dyadic intervals It uses the sets `dyadic_approx` and *) +(* `integer_approx`. *) +(* *) +(* `nnsfun_approx D f` *) +(* ~ same as `approx D f` but as a `nnsfun` approximates `f` over `D` *) +(* using dyadic intervals *) (* *) (******************************************************************************) diff --git a/theories/lebesgue_integral_theory/radon_nikodym.v b/theories/lebesgue_integral_theory/radon_nikodym.v index 46363a4b63..42da4fb865 100644 --- a/theories/lebesgue_integral_theory/radon_nikodym.v +++ b/theories/lebesgue_integral_theory/radon_nikodym.v @@ -24,14 +24,14 @@ From mathcomp Require Import lebesgue_integral_definition lebesgue_integrable (* Stieltjes measure in Coq. Computer Software 41(2) 2024 *) (* *) (* ## Theory *) -(* ``` *) -(* induced_charge intf == charge induced by a function f : T -> \bar R *) -(* R has type realType; T is a measurableType. *) -(* intf is a proof that f is integrable over *) -(* [set: T] *) -(* 'd nu '/d mu == Radon-Nikodym derivative of nu w.r.t. mu *) -(* (the scope is charge_scope) *) -(* ``` *) +(* `induced_charge intf` *) +(* ~ charge induced by a function `f : T -> \bar R` *) +(* ~ `R` has type `realType`; `T` is a `measurableType` *) +(* ~ `intf` is a proof that `f` is integrable over `[set: T]` *) +(* *) +(* `'d nu '/d mu` *) +(* ~ Radon-Nikodym derivative of `nu` w.r.t. `mu` *) +(* (the scope is `charge_scope`) *) (* *) (******************************************************************************) diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index 7aa5da011c..45deb259c1 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -27,23 +27,45 @@ From mathcomp Require Import lebesgue_measure numfun realfun measurable_realfun. (* HBNNSimple) and to instantiate FiniteImage (resp. NonNegFun) locally. *) (* *) (* Detailed contents: *) -(* ```` *) -(* {sfun T >-> R} == type of simple functions *) -(* They form a (potentially zero) ring. *) -(* {nnsfun T >-> R} == type of non-negative simple functions *) -(* indic_sfun mD := mindic _ mD *) -(* cst_sfun r == constant simple function *) -(* cst_nnsfun r == constant simple function *) -(* nnsfun0 := cst_nnsfun 0 *) -(* add_nnsfun f g := f \+ g *) -(* mul_nnsfun f g := f \* g *) -(* max_nnsfun f g := f \max g *) -(* proj_nssfun f mA == projection of the function f to the set A *) -(* mA is a proof that A is measurable *) -(* scale_nnsfun k f == scales f by the non-negative real number k *) -(* sum_nnsfun f n := \big[add_nnsfun/nnsfun0]_(i < n) f i *) -(* bigmax_nnsfun f n := \big[max_nnsfun/nnsfun0]_(i < n) f i *) -(* ```` *) +(* `{sfun T >-> R}` *) +(* ~ type of simple functions; they form a (potentially zero) ring *) +(* *) +(* `{nnsfun T >-> R}` *) +(* ~ type of non-negative simple functions *) +(* *) +(* `indic_sfun mD` *) +(* ~ `mindic _ mD` *) +(* *) +(* `cst_sfun r` *) +(* ~ constant simple function *) +(* *) +(* `cst_nnsfun r` *) +(* ~ constant simple function *) +(* *) +(* `nnsfun0` *) +(* ~ `cst_nnsfun 0` *) +(* *) +(* `add_nnsfun f g` *) +(* ~ `f \+ g` *) +(* *) +(* `mul_nnsfun f g` *) +(* ~ `f \* g` *) +(* *) +(* `max_nnsfun f g` *) +(* ~ `f \max g` *) +(* *) +(* `proj_nssfun f mA` *) +(* ~ projection of the function `f` to the set `A`; `mA` is a proof *) +(* that `A` is measurable *) +(* *) +(* `scale_nnsfun k f` *) +(* ~ scales `f` by the non-negative real number `k` *) +(* *) +(* `sum_nnsfun f n` *) +(* ~ `\big[add_nnsfun/nnsfun0]_(i < n) f i` *) +(* *) +(* `bigmax_nnsfun f n` *) +(* ~ `\big[max_nnsfun/nnsfun0]_(i < n) f i` *) (* *) (******************************************************************************) diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index dd17356bac..dd8f05472c 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -25,16 +25,18 @@ From mathcomp Require Export lebesgue_stieltjes_measure. (* - R. Affeldt, C. Cohen. Measure Construction by Extension in Dependent *) (* Type Theory with Application to Integration. JAR 2023 *) (* *) -(* ``` *) -(* lebesgue_measure == the Lebesgue measure *) -(* completed_lebesgue_measure == the completed Lebesgue measure *) -(* elebesgue_measure == the Lebesgue measure extended to \bar R *) -(* ``` *) +(* `lebesgue_measure` *) +(* ~ the Lebesgue measure *) (* *) -(* ``` *) -(* vitali_cover A B V == V is a Vitali cover of A, here B is a *) -(* collection of non-empty closed balls *) -(* ``` *) +(* `completed_lebesgue_measure` *) +(* ~ the completed Lebesgue measure *) +(* *) +(* `elebesgue_measure` *) +(* ~ the Lebesgue measure extended to `\bar R` *) +(* *) +(* `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 c2eaeb7f75..ca9cb8cc01 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -20,16 +20,17 @@ From mathcomp Require Import realfun. (* - Y. Ishiguro, R. Affeldt. The Radon-Nikodym Theorem and the Lebesgue- *) (* Stieltjes measure in Coq. Computer Software 41(2).2024 *) (* *) -(* ``` *) -(* right_continuous f == the function f is right-continuous *) -(* cumulative R == type of non-decreasing, right-continuous *) -(* functions (with R : numFieldType) *) -(* The HB class is Cumulative. *) -(* instance: idfun *) -(* cumulativeBounded R l r == type of cumulative functions f such that *) -(* f @ -oo --> l and f @ +oo --> r *) -(* The HB class is CumulativeBounded. *) -(* ``` *) +(* `right_continuous f` *) +(* ~ the function `f` is right-continuous *) +(* *) +(* `cumulative R` *) +(* ~ type of non-decreasing, right-continuous functions (with *) +(* `R : numFieldType`). The HB class is `Cumulative`. instance: *) +(* `idfun` *) +(* *) +(* `cumulativeBounded R l r` *) +(* ~ type of cumulative functions `f` such that `f @ -oo --> l` and *) +(* `f @ +oo --> r`. The HB class is `CumulativeBounded` *) (* *) (* The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens, ROpenSets *) (* provide proofs of equivalence between the sigma-algebra generated by *) @@ -38,51 +39,61 @@ From mathcomp Require Import realfun. (* *) (* We distinguish in particular the sigma-algebras generated by ocitv and *) (* and open sets for which we introduce the following definitions/notations: *) -(* ``` *) -(* ocitv_type R == alias for R : realType *) -(* ocitv == set of open-closed intervals ]x, y] where *) -(* x and y are real numbers *) -(* R.-ocitv == display for ocitv_type R *) -(* R.-ocitv.-measurable == semiring of sets of open-closed intervals *) -(* open_type R == alias for R : realType *) -(* R.-open := sigma_display (@open R) *) -(* R.-open.-measurable == sigma-algebra generated by open sets *) -(* ``` *) +(* `ocitv_type R` *) +(* ~ alias for `R : realType` *) +(* *) +(* `ocitv` *) +(* ~ set of open-closed intervals `]x, y]` where `x` and `y` are real *) +(* numbers *) +(* *) +(* `R.-ocitv` *) +(* ~ display for `ocitv_type R` *) +(* *) +(* `R.-ocitv.-measurable` *) +(* ~ semiring of sets of open-closed intervals *) +(* *) +(* `open_type R` *) +(* ~ alias for `R : realType` *) +(* *) +(* `R.-open` *) +(* ~ `sigma_display (@open R)` *) +(* *) +(* `R.-open.-measurable` *) +(* ~ sigma-algebra generated by open sets *) (* The modules `MeasurableRocitv` and `MeasurableRopen` contains resp. the *) (* sigma-algebras generated from ocitv and open sets. They contain similar *) (* definitions: *) -(* ``` *) -(* measurableTypeR R == measurableType generated by *) -(* R.-ocitv or R.-open *) -(* @lebesgue_display R == (measure_)display for the sigma-algebra *) -(* generated by R.-ocitv or R.-open *) -(* @measurableR R == measurable sets generated by *) -(* R.-ocitv or R.-open *) -(* ``` *) +(* `measurableTypeR R` *) +(* ~ `measurableType` generated by `R.-ocitv` or `R.-open` *) +(* *) +(* `@lebesgue_display R` *) +(* ~ `(measure_)display` for the sigma-algebra generated by *) +(* `R.-ocitv` or `R.-open` *) +(* *) +(* `@measurableR R` *) +(* ~ measurable sets generated by `R.-ocitv` or `R.-open` *) (* The module `MeasurableR` contains the default sigma-algebra, which is *) (* `MeasurableRopen`. The latter contains in addition: *) -(* ``` *) -(* ocitv_measure mu == measure over the sigma-algebra *) -(* generated by open sets built out of mu, *) -(* the same measure over the sigma-algebra *) -(* generated by ocitv *) -(* ``` *) +(* `ocitv_measure mu` *) +(* ~ measure over the sigma-algebra generated by open sets built *) +(* out of `mu`, the same measure over the sigma-algebra generated *) +(* by `ocitv` *) (* The last part of the file contains the construction of the Lebesgue- *) (* Stieltjes measure: *) -(* ``` *) -(* wlength f A := f b - f a with the hull of the set of real *) -(* numbers A being delimited by a and b *) -(* ocitv_lebesgue_stieltjes_measure f == Lebesgue-Stieltjes measure for f *) -(* f is a cumulative function. *) -(* The sigma algebra is generated from *) -(* ocitv. *) -(* lebesgue_stieltjes_measure f == Lebesgue-Stieltjes measure for f *) -(* f is a cumulative function. *) -(* The sigma algebra is generated from open *) -(* sets. *) -(* completed_lebesgue_stieltjes_measure f == the completed Lebesgue-Stieltjes *) -(* measure *) -(* ``` *) +(* `wlength f A` *) +(* ~ `f b - f a` with the hull of the set of real numbers `A` being *) +(* delimited by `a` and `b` *) +(* *) +(* `ocitv_lebesgue_stieltjes_measure f` *) +(* ~ Lebesgue-Stieltjes measure for `f`. `f` is a cumulative *) +(* function. The sigma algebra is generated from `ocitv` *) +(* *) +(* `lebesgue_stieltjes_measure f` *) +(* ~ Lebesgue-Stieltjes measure for `f`. `f` is a cumulative *) +(* function. The sigma algebra is generated from open sets *) +(* *) +(* `completed_lebesgue_stieltjes_measure f` *) +(* ~ the completed Lebesgue-Stieltjes measure *) (* *) (******************************************************************************) diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index dd0c4d4963..84721d5f33 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -19,14 +19,15 @@ From mathcomp Require Import lebesgue_stieltjes_measure. (* - Daniel Li, Intégration et applications, 2016 *) (* - Achim Klenke, Probability Theory 2nd edition, 2014 *) (* *) -(* ``` *) -(* completed_algebra_gen == generator of the completed Lebesgue *) -(* sigma-algebra *) -(* 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 *) -(* ``` *) +(* `completed_algebra_gen` *) +(* ~ generator of the completed Lebesgue sigma-algebra *) +(* *) +(* `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` *) (* *) (* The module NGenCInfty provides a proof of equivalence between the *) (* sigma-algebra for natural numbers and the sigma-algebra generated by *) @@ -36,13 +37,20 @@ From mathcomp Require Import lebesgue_stieltjes_measure. (* of equivalence between emeasurable and the sigma-algebras generated by *) (* open rays and closed rays. *) (* *) -(* ``` *) -(* mindic mD := \1_D where mD is a proof that D is measurable *) -(* indic_mfun mD := mindic mD *) -(* scale_mfun k f := k \o* f *) -(* max_mfun f g := f \max g *) -(* min_mfun f g := f \min g *) -(* ``` *) +(* `mindic mD` *) +(* ~ `\1_D`, where `mD` is a proof that `D` is measurable *) +(* *) +(* `indic_mfun mD` *) +(* ~ `mindic mD` *) +(* *) +(* `scale_mfun k f` *) +(* ~ `k \o* f` *) +(* *) +(* `max_mfun f g` *) +(* ~ `f \max g` *) +(* *) +(* `min_mfun f g` *) +(* ~ `f \min g` *) (******************************************************************************) Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) diff --git a/theories/measure_theory/counting_measure.v b/theories/measure_theory/counting_measure.v index dfc735ff08..2445a337fe 100644 --- a/theories/measure_theory/counting_measure.v +++ b/theories/measure_theory/counting_measure.v @@ -8,9 +8,8 @@ From mathcomp Require Import sequences measurable_structure measure_function. (**md**************************************************************************) (* # The Counting Measure *) (* *) -(* ``` *) -(* counting T R == counting measure *) -(* ``` *) +(* `counting T R` *) +(* ~ counting measure *) (******************************************************************************) Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) diff --git a/theories/measure_theory/dirac_measure.v b/theories/measure_theory/dirac_measure.v index 329fb4b861..c7afba0324 100644 --- a/theories/measure_theory/dirac_measure.v +++ b/theories/measure_theory/dirac_measure.v @@ -10,9 +10,8 @@ From mathcomp Require Import measurable_structure measure_function. (**md**************************************************************************) (* # The Dirac Measure *) (* *) -(* ``` *) -(* \d_a == Dirac measure *) -(* ``` *) +(* `\d_a` *) +(* ~ Dirac measure *) (* *) (******************************************************************************) diff --git a/theories/measure_theory/measurable_function.v b/theories/measure_theory/measurable_function.v index 91b1a9bccc..5d6bceb4e1 100644 --- a/theories/measure_theory/measurable_function.v +++ b/theories/measure_theory/measurable_function.v @@ -9,12 +9,15 @@ From mathcomp Require Import measurable_structure. (**md**************************************************************************) (* # Measurable Functions *) (* *) -(* ``` *) -(* measurable_fun D f == the function f with domain D is measurable *) -(* {mfun aT >-> rT} == type of measurable functions *) -(* aT and rT are sigmaRingType's. *) -(* f \in mfun == holds for f : {mfun _ >-> _} *) -(* ``` *) +(* `measurable_fun D f` *) +(* ~ the function `f` with domain `D` is measurable *) +(* *) +(* `{mfun aT >-> rT}` *) +(* ~ type of measurable functions *) +(* ~ `aT` and `rT` are `sigmaRingType`'s. *) +(* *) +(* `f \in mfun` *) +(* ~ holds for `f : {mfun _ >-> _}` *) (* *) (******************************************************************************) diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index 68d12bf18a..531c9654ec 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -17,104 +17,143 @@ From mathcomp Require Import boolp classical_sets functions cardinality reals. (* - Achim Klenke. Probability Theory. 2014 *) (* *) (* ## 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. *) -(* "measurable A" is printed as "d.-measurable A" *) -(* where d is a "display parameter" whose purpose *) -(* is to distinguish different "measurable" *) -(* predicates in the same context. *) -(* The HB class is SemiRingOfSets. *) -(* ringOfSetsType d == the type of rings of sets *) -(* The HB class is RingOfSets. *) -(* sigmaRingType d == the type of sigma-rings (of sets) *) -(* The HB class is SigmaRing. *) -(* algebraOfSetsType d == the type of algebras of sets *) -(* The HB class is AlgebraOfsets. *) -(* measurableType == the type of sigma-algebras *) -(* The HB class is Measurable. *) -(* pmeasurableType == the type of pointed sigma-algebras *) -(* The HB class is PMeasurable. *) -(* ``` *) +(* `semiRingOfSetsType d` *) +(* ~ the type of semirings of sets. The carrier is a set of sets *) +(* `A_i` such that `measurable A_i` holds. `measurable A` is printed *) +(* as `d.-measurable A` where `d` is a "display parameter" whose *) +(* purpose is to distinguish different `measurable` predicates in *) +(* the same context. The HB class is `SemiRingOfSets`. *) +(* *) +(* `ringOfSetsType d` *) +(* ~ the type of rings of sets. The HB class is `RingOfSets`. *) +(* *) +(* `sigmaRingType d` *) +(* ~ the type of sigma-rings (of sets). The HB class is `SigmaRing`. *) +(* *) +(* `algebraOfSetsType d` *) +(* ~ the type of algebras of sets. The HB class is `AlgebraOfsets`. *) +(* *) +(* `measurableType` *) +(* ~ the type of sigma-algebras. The HB class is `Measurable`. *) +(* *) +(* `pmeasurableType` *) +(* ~ the type of pointed sigma-algebras. The HB class is *) +(* `PMeasurable`. *) (* *) (* ## Instances of mathematical structures *) -(* ``` *) -(* discrete_measurable T == alias for the sigma-algebra [set: set T] *) -(* setring G == the set of sets G contains the empty set, is *) -(* closed by union, and difference (it is a ring *) -(* of sets in the sense of ringOfSetsType) *) -(* <> := smallest setring G *) -(* <> is equipped with a structure of ring *) -(* of sets. *) -(* sigma_ring G == the set of sets G forms a sigma-ring *) -(* <> == sigma-ring generated by G *) -(* := smallest sigma_ring G *) -(* sigma_algebra D G == the set of sets G forms a sigma-algebra on D *) -(* <> == sigma-algebra generated by G on D *) -(* := smallest (sigma_algebra D) G *) -(* <> := <> *) -(* <> is equipped with a structure of *) -(* sigma-algebra *) -(* G.-sigma.-measurable A == A is measurable for the sigma-algebra <> *) -(* g_sigma_algebraType G == the measurableType corresponding to <> *) -(* This is an HB alias. *) -(* ``` *) +(* `discrete_measurable T` *) +(* ~ alias for the sigma-algebra `[set: set T]` *) +(* *) +(* `setring G` *) +(* ~ the set of sets `G` contains the empty set, is closed by union, *) +(* and difference (it is a ring of sets in the sense of *) +(* `ringOfSetsType`) *) +(* *) +(* `<>` *) +(* ~ `smallest setring G` *) +(* ~ `<>` is equipped with a structure of ring of sets *) +(* *) +(* `sigma_ring G` *) +(* ~ the set of sets `G` forms a sigma-ring *) +(* *) +(* `<>` *) +(* ~ sigma-ring generated by `G` *) +(* ~ `:= smallest sigma_ring G` *) +(* *) +(* `sigma_algebra D G` *) +(* ~ the set of sets `G` forms a sigma-algebra on `D` *) +(* *) +(* `<>` *) +(* ~ sigma-algebra generated by `G` on `D` *) +(* ~ `:= smallest (sigma_algebra D) G` *) +(* *) +(* `<>` *) +(* ~ `<>` *) +(* ~ `<>` is equipped with a structure of sigma-algebra *) +(* *) +(* `G.-sigma.-measurable A` *) +(* ~ `A` is measurable for the sigma-algebra `<>` *) +(* *) +(* `g_sigma_algebraType G` *) +(* ~ the `measurableType` corresponding to `<>`. This is an HB *) +(* alias. *) (* *) (* ## About sets of sets *) -(* ``` *) -(* setC_closed G == the set of sets G is closed under complement *) -(* setSD_closed G == the set of sets G is closed under proper *) -(* difference *) -(* setD_closed G == the set of sets G is closed under difference *) -(* setY_closed G == the set of sets G is closed under symmetric *) -(* difference *) -(* ndseq_closed G == the set of sets G is closed under non-decreasing *) -(* countable union *) -(* niseq_closed G == the set of sets G is closed under non-increasing *) -(* countable intersection *) -(* trivIset_closed G == the set of sets G is closed under pairwise-disjoint *) -(* countable union *) -(* lambda_system D G == G is a lambda_system of subsets of D *) -(* <> == lambda-system generated by G on D *) -(* <> := <> *) -(* monotone G == G is a monotone set system *) -(* <> == monotone set system generated by G *) -(* := smallest monotone G *) -(* dynkin G == G is a set of sets that form a Dynkin *) -(* system (or a d-system) *) -(* <> == Dynkin system generated by G, i.e., *) -(* smallest dynkin G *) -(* strace G D := [set x `&` D | x in G] *) -(* ``` *) +(* `setC_closed G` *) +(* ~ the set of sets `G` is closed under complement *) +(* *) +(* `setSD_closed G` *) +(* ~ the set of sets `G` is closed under proper difference *) +(* *) +(* `setD_closed G` *) +(* ~ the set of sets `G` is closed under difference *) +(* *) +(* `setY_closed G` *) +(* ~ the set of sets `G` is closed under symmetric difference *) +(* *) +(* `ndseq_closed G` *) +(* ~ the set of sets `G` is closed under non-decreasing countable *) +(* union *) +(* *) +(* `niseq_closed G` *) +(* ~ the set of sets `G` is closed under non-increasing countable *) +(* intersection *) +(* *) +(* `trivIset_closed G` *) +(* ~ the set of sets `G` is closed under pairwise-disjoint countable *) +(* union *) +(* *) +(* `lambda_system D G` *) +(* ~ `G` is a `lambda_system` of subsets of `D` *) +(* *) +(* `<>` *) +(* ~ lambda-system generated by `G` on `D` *) +(* *) +(* `<>` *) +(* ~ `<>` *) +(* *) +(* `monotone G` *) +(* ~ `G` is a monotone set system *) +(* *) +(* `<>` *) +(* ~ monotone set system generated by `G` *) +(* ~ `:= smallest monotone G` *) +(* *) +(* `dynkin G` *) +(* ~ `G` is a set of sets that form a Dynkin system (or a d-system) *) +(* *) +(* `<>` *) +(* ~ Dynkin system generated by `G`, i.e., `smallest dynkin G` *) +(* *) +(* `strace G D` *) +(* ~ ``[set x `&` D | x in G]`` *) (* ## Other measure-theoretic definitions *) (* *) -(* ``` *) -(* g_sigma_algebra_preimage f == sigma-algebra generated by the *) -(* function f *) -(* g_sigma_algebra_preimageType f == the measurableType corresponding to *) -(* g_sigma_algebra_preimage f *) -(* This is an HB alias. *) -(* f.-preimage.-measurable A == A is measurable for *) -(* g_sigma_algebra_preimage f *) -(* ``` *) +(* `g_sigma_algebra_preimage f` *) +(* ~ sigma-algebra generated by the function `f` *) +(* *) +(* `g_sigma_algebra_preimageType f` *) +(* ~ the `measurableType` corresponding to *) +(* `g_sigma_algebra_preimage f`. This is an HB alias. *) +(* *) +(* `f.-preimage.-measurable A` *) +(* ~ `A` is measurable for `g_sigma_algebra_preimage f` *) (* *) (* ## Product of measurable spaces *) -(* ``` *) -(* g_sigma_preimageU 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 semiRingOfSetsType's *) -(* (d1, d2).-prod.-measurable A == A is measurable for the sigma-algebra *) -(* generated from T1 x T2, with T1 and T2 *) -(* semiRingOfSetsType's with resp. display *) -(* d1 and d2 *) -(* g_sigma_preimage n (f : 'I_n -> aT -> rT) == the sigma-algebra over aT *) -(* generated by the projections f *) -(* n.-tuple T is equipped with a *) -(* measurableType using g_sigma_preimage *) -(* and the tnth projections. *) -(* ``` *) +(* `g_sigma_preimageU 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 `semiRingOfSetsType`'s *) +(* *) +(* `(d1, d2).-prod.-measurable A` *) +(* ~ `A` is measurable for the sigma-algebra generated from `T1 x T2`, *) +(* with `T1` and `T2` `semiRingOfSetsType`'s with resp. display `d1` *) +(* and `d2` *) +(* *) +(* `g_sigma_preimage n (f : 'I_n -> aT -> rT)` *) +(* ~ the sigma-algebra over `aT` generated by the projections `f`. *) +(* `n.-tuple T` is equipped with a `measurableType` using *) +(* `g_sigma_preimage` and the `tnth` projections. *) (* *) (******************************************************************************) diff --git a/theories/measure_theory/measure_extension.v b/theories/measure_theory/measure_extension.v index aac951cdb9..90347265fa 100644 --- a/theories/measure_theory/measure_extension.v +++ b/theories/measure_theory/measure_extension.v @@ -19,52 +19,51 @@ From mathcomp Require Import measure_negligible. (* measure being *) (* $\inf_F\{ \sum_{k=0}^\infty \mu(F_k) | X \subseteq \bigcup_k F_k\}.$ *) (* *) -(* ``` *) -(* sigma_subadditive mu == predicate defining sigma-subadditivity *) -(* {outer_measure set T -> \bar R} == type of an outer measure over sets *) -(* of elements of type T : Type where R is *) -(* expected to be a numFieldType *) -(* The HB class is OuterMeasure. *) -(* interfaces: isOuterMeasure, *) -(* isSubsetOuterMeasure *) -(* ``` *) +(* `sigma_subadditive mu` *) +(* ~ predicate defining sigma-subadditivity *) (* *) -(* ``` *) -(* mu.-caratheodory == the set of Caratheodory measurable sets for the *) -(* outer measure mu, i.e., sets A such that *) -(* forall B, mu A = mu (A `&` B) + mu (A `&` ~` B) *) -(* caratheodory_type mu := T, where mu : {outer_measure set T -> \bar R} *) -(* It is a canonical measurableType copy of T. *) -(* The restriction of the outer measure mu to the *) -(* sigma algebra of Caratheodory measurable sets *) -(* is a measure. *) -(* Remark: sets that are negligible for *) -(* this measure are Caratheodory measurable. *) -(* caratheodory_measure mu == measure built out of mu, an outer measure *) -(* mu .-cara.-measurable == sigma-algebra of Caratheodory measurable sets *) -(* ``` *) +(* `{outer_measure set T -> \bar R}` *) +(* ~ type of an outer measure over sets of elements of type *) +(* `T : Type` where `R` is expected to be a `numFieldType`. The HB *) +(* class is `OuterMeasure`. interfaces: `isOuterMeasure`, *) +(* `isSubsetOuterMeasure` *) +(* *) +(* `mu.-caratheodory` *) +(* ~ the set of Caratheodory measurable sets for the outer measure *) +(* `mu`, i.e., sets `A` such that *) +(* ``forall B, mu A = mu (A `&` B) + mu (A `&` ~` B)`` *) +(* *) +(* `caratheodory_type mu` *) +(* ~ `T`, where `mu : {outer_measure set T -> \bar R}`. It is a *) +(* canonical `measurableType` copy of `T`. The restriction of the *) +(* outer measure `mu` to the sigma algebra of Caratheodory *) +(* measurable sets is a measure. Remark: sets that are negligible *) +(* for this measure are Caratheodory measurable. *) +(* *) +(* `caratheodory_measure mu` *) +(* ~ measure built out of `mu`, an outer measure *) +(* *) +(* `mu .-cara.-measurable` *) +(* ~ sigma-algebra of Caratheodory measurable sets *) (* *) (* From a premeasure to an outer measure (Measure Extension Theorem part 1): *) -(* ``` *) -(* measurable_cover X == the set of sequences F such that *) -(* - forall k, F k is measurable *) -(* - X `<=` \bigcup_k (F k) *) -(* mu^* == extension of the measure mu over a semiring of *) -(* sets (it is an outer measure) *) -(* ``` *) +(* `measurable_cover X` *) +(* ~ the set of sequences `F` such that *) +(* - `forall k, F k` is measurable *) +(* - ``X `<=` \bigcup_k (F k)`` *) +(* *) +(* `mu^*` *) +(* ~ extension of the measure `mu` over a semiring of sets (it is an *) +(* outer measure) *) (* *) (* From an outer measure to a measure (Measure Extension Theorem part 2): *) -(* ``` *) -(* measure_extension mu == extension of the content mu over a *) -(* semiring of sets to a measure over the *) -(* generated sigma algebra (requires a proof of *) -(* sigma-sub-additivity) *) -(* ``` *) +(* `measure_extension mu` *) +(* ~ extension of the content `mu` over a semiring of sets to a *) +(* measure over the generated sigma algebra (requires a proof of *) +(* sigma-sub-additivity) *) (* *) -(* ``` *) -(* completed_measure_extension mu == similar to measure_extension but returns *) -(* a complete measure *) -(* ``` *) +(* `completed_measure_extension mu` *) +(* ~ similar to `measure_extension` but returns a complete measure *) (* *) (******************************************************************************) diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v index eba1a7ccdc..13a817912c 100644 --- a/theories/measure_theory/measure_function.v +++ b/theories/measure_theory/measure_function.v @@ -18,89 +18,115 @@ From mathcomp Require Import measurable_structure measurable_function. (* Hierarchy of contents, measures, s-finite/sigma-finite/finite measures, *) (* etc. Also contains a number of details about its implementation. *) (* *) -(* ``` *) -(* subset_sigma_subadditive mu == alternative predicate defining *) -(* sigma-subadditivity *) -(* {content set T -> \bar R} == type of contents *) -(* T is expected to be a semiring of sets and R *) -(* a numFieldType. *) -(* The HB class is Content. *) -(* Content_isMeasure == interface that extends a content to a measure *) -(* with the proof that it is semi_sigma_additive *) -(* {measure set T -> \bar R} == type of (non-negative) measures *) -(* T is expected to be a semiring of sets and *) -(* R is expected to be a numFieldType. *) -(* The HB class is Measure. *) -(* isMeasure == interface corresponding to the "textbook *) -(* definition" of measures *) -(* ``` *) +(* `subset_sigma_subadditive mu` *) +(* ~ alternative predicate defining sigma-subadditivity *) +(* *) +(* `{content set T -> \bar R}` *) +(* ~ type of contents; `T` is expected to be a semiring of sets and *) +(* `R` a `numFieldType`. The HB class is `Content`. *) +(* *) +(* `Content_isMeasure` *) +(* ~ interface that extends a content to a measure with the proof *) +(* that it is `semi_sigma_additive` *) +(* *) +(* `{measure set T -> \bar R}` *) +(* ~ type of (non-negative) measures; `T` is expected to be a *) +(* semiring of sets and `R` is expected to be a `numFieldType`. *) +(* The HB class is `Measure`. *) +(* *) +(* `isMeasure` *) +(* ~ interface corresponding to the "textbook definition" of *) +(* measures *) (* ## Instances of measures *) (* *) -(* ``` *) -(* msum mu n == the measure corresponding to the sum of the measures *) -(* mu_0, ..., mu_{n-1} *) -(* @mzero T R == the zero measure *) -(* measure_add m1 m2 == the measure corresponding to the sum of the *) -(* measures m1 and m2 *) -(* mscale r m == the measure of corresponding to fun A => r * m A *) -(* where r has type {nonneg R} *) -(* mseries mu n == the measure corresponding to the sum of the *) -(* measures mu_n, mu_{n+1}, ... *) -(* pushforward m f == pushforward of a set function m : set T1 -> \bar R *) -(* by f : T1 -> T2; pushforward/image measure if m is *) -(* a measure and f measurable *) -(* ``` *) +(* `msum mu n` *) +(* ~ the measure corresponding to the sum of the measures `mu_0`, *) +(* ..., `mu_{n-1}` *) +(* *) +(* `@mzero T R` *) +(* ~ the zero measure *) +(* *) +(* `measure_add m1 m2` *) +(* ~ the measure corresponding to the sum of the measures `m1` and *) +(* `m2` *) +(* *) +(* `mscale r m` *) +(* ~ the measure of corresponding to `fun A => r * m A` where `r` *) +(* has type `{nonneg R}` *) +(* *) +(* `mseries mu n` *) +(* ~ the measure corresponding to the sum of the measures `mu_n`, *) +(* `mu_{n+1}`, ... *) +(* *) +(* `pushforward m f` *) +(* ~ pushforward of a set function `m : set T1 -> \bar R` by *) +(* `f : T1 -> T2`; pushforward/image measure if `m` is a measure *) +(* and `f` measurable *) +(* *) +(* `G.-ring.-measurable A` *) +(* ~ `A` belongs to the ring of sets `<>` *) +(* *) +(* `fin_num_fun` *) +(* ~ predicate for finite function over measurable sets *) +(* *) +(* `sfinite_measure` *) +(* ~ predicate for s-finite measure functions *) +(* *) +(* `sigma_finite A f` *) +(* ~ the measure function `f` is sigma-finite on the `A : set T` *) +(* with `T` a semiring of sets *) +(* *) +(* `mrestr mu mD` *) +(* ~ restriction of the measure `mu` to a set `D`; `mD` is a proof *) +(* that `D` is measurable *) +(* *) +(* `isSFinite` *) +(* ~ interface for functions that satisfy the `sfinite_measure` *) +(* predicate *) +(* *) +(* `{sfinite_measure set T -> \bar R}` *) +(* ~ type of s-finite measures. The HB class is `SFiniteMeasure`. *) +(* *) +(* `isSigmaFinite` *) +(* ~ interface for functions that satisfy sigma finiteness *) +(* *) +(* `{sigma_finite_content set T -> \bar R}` *) +(* ~ contents that are also sigma finite. The HB class is *) +(* `SigmaFiniteContent`. *) +(* *) +(* `{sigma_finite_measure set T -> \bar R}` *) +(* ~ measures that are also sigma finite. The HB class is *) +(* `SigmaFiniteMeasure`. *) +(* *) +(* `Measure_isSFinite` *) +(* ~ interface that extends a measure to an s-finite measure using *) +(* a sequence of finite measures *) +(* *) +(* `isFinNumFun` *) +(* ~ interface for functions that satisfy the `fin_num_fun` *) +(* predicate *) +(* *) +(* `FinNumFun.type` *) +(* ~ type of functions over semiring of sets returning a `fin_num`. *) +(* The HB class is `FinNumFun`. *) +(* *) +(* `{finite_measure set T -> \bar R}` *) +(* ~ finite measures. The HB class is `FiniteMeasure`. *) (* *) -(* ``` *) -(* G.-ring.-measurable A == A belongs to the ring of sets <> *) -(* ``` *) +(* `Measure_isFinite` *) +(* ~ interface that extends a measure to a finite measure using a *) +(* proof of `fin_num_fun` *) (* *) -(* ``` *) -(* fin_num_fun == predicate for finite function over measurable *) -(* sets *) -(* sfinite_measure == predicate for s-finite measure functions *) -(* sigma_finite A f == the measure function f is sigma-finite on the *) -(* A : set T with T a semiring of sets *) -(* mrestr mu mD == restriction of the measure mu to a set D *) -(* mD is a proof that D is measurable. *) -(* isSFinite == interface for functions that satisfy the *) -(* sfinite_measure predicate *) -(* {sfinite_measure set T -> \bar R} == type of s-finite measures *) -(* The HB class is SFiniteMeasure. *) -(* isSigmaFinite == interface for functions that satisfy *) -(* sigma finiteness *) -(* {sigma_finite_content set T -> \bar R} == contents that are also sigma *) -(* finite *) -(* The HB class is SigmaFiniteContent. *) -(* {sigma_finite_measure set T -> \bar R} == measures that are also sigma *) -(* finite *) -(* The HB class is SigmaFiniteMeasure. *) -(* Measure_isSFinite == interface that extends a measure to an *) -(* s-finite measure using a sequence of finite *) -(* measures *) -(* isFinNumFun == interface for functions that satisfy the *) -(* fin_num_fun predicate *) -(* FinNumFun.type == type of functions over semiring of sets *) -(* returning a fin_num *) -(* The HB class is FinNumFun. *) -(* {finite_measure set T -> \bar R} == finite measures *) -(* The HB class is FiniteMeasure. *) -(* Measure_isFinite == interface that extends a measure to a finite *) -(* measure using a proof of fin_num_fun *) -(* sfinite_measure_seq mu == the sequence of finite measures of the *) -(* s-finite measure mu *) -(* ``` *) +(* `sfinite_measure_seq mu` *) +(* ~ the sequence of finite measures of the s-finite measure `mu` *) (* *) -(* ``` *) -(* mfrestr mD muDoo == finite measure corresponding to the restriction of *) -(* the measure mu over D with mu D < +oo, *) -(* mD : measurable D, muDoo : mu D < +oo *) -(* ``` *) +(* `mfrestr mD muDoo` *) +(* ~ finite measure corresponding to the restriction of the measure *) +(* `mu` over `D` with `mu D < +oo`, `mD : measurable D`, *) +(* `muDoo : mu D < +oo` *) (* *) -(* ``` *) -(* lim_sup_set F == limit superior (or upper limit) of a *) -(* sequence of sets F *) -(* ``` *) +(* `lim_sup_set F` *) +(* ~ limit superior (or upper limit) of a sequence of sets `F` *) (* *) (******************************************************************************) diff --git a/theories/measure_theory/measure_negligible.v b/theories/measure_theory/measure_negligible.v index 1e0ce95855..2b506d29ed 100644 --- a/theories/measure_theory/measure_negligible.v +++ b/theories/measure_theory/measure_negligible.v @@ -13,29 +13,38 @@ From mathcomp Require Import measurable_structure measure_function. (* *) (* NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. *) (* *) -(* ``` *) -(* mu.-negligible A == A is mu negligible *) -(* measure_is_complete mu == the measure mu is complete *) -(* {ae mu, P} == P holds almost everywhere for the measure mu, *) -(* declared as an instance of the type of *) -(* filters *) -(* P must be of the form forall x, Q x. *) -(* Prefer this notation when P is an existing *) -(* statement (i.e., a definition) that needs to *) -(* be relativised. *) -(* The notation used the definition *) -(* `almost_everywhere`. *) -(* \forall x \ae mu, P x == equivalent to {ae mu, forall x, P x} *) -(* Prefer this notation when the statement *) -(* forall x, P x does not stand alone. *) -(* f = g %[ae mu in D ] == f is equal to g almost everywhere in D *) -(* f = g %[ae mu] == f is equal to g almost everywhere *) -(* mu-.null_set == (measure-theoretic) null sets *) -(* m1 `<< m2 == m1 is absolutely continuous w.r.t. m2 or *) -(* m2 dominates m1 *) -(* content_dominates mu nu == forall A, measurable A -> *) -(* mu A = 0 -> nu A = 0 *) -(* ``` *) +(* `mu.-negligible A` *) +(* ~ `A` is `mu` negligible *) +(* *) +(* `measure_is_complete mu` *) +(* ~ the measure `mu` is complete *) +(* *) +(* `{ae mu, P}` *) +(* ~ `P` holds almost everywhere for the measure `mu`, declared as *) +(* an instance of the type of filters `P` must be of the form *) +(* `forall x, Q x`. Prefer this notation when `P` is an existing *) +(* statement (i.e., a definition) that needs to be relativised. *) +(* The notation used the definition `almost_everywhere`. *) +(* *) +(* `\forall x \ae mu, P x` *) +(* ~ equivalent to `{ae mu, forall x, P x}` Prefer this notation *) +(* when the statement `forall x, P x` does not stand alone. *) +(* *) +(* `f = g %[ae mu in D ]` *) +(* ~ `f` is equal to `g` almost everywhere in `D` *) +(* *) +(* `f = g %[ae mu]` *) +(* ~ `f` is equal to `g` almost everywhere *) +(* *) +(* `mu-.null_set` *) +(* ~ (measure-theoretic) null sets *) +(* *) +(* ``m1 `<< m2`` *) +(* ~ `m1` is absolutely continuous w.r.t. `m2` or `m2` dominates *) +(* `m1` *) +(* *) +(* `content_dominates mu nu` *) +(* ~ `forall A, measurable A -> mu A = 0 -> nu A = 0` *) (* *) (******************************************************************************) diff --git a/theories/measure_theory/probability_measure.v b/theories/measure_theory/probability_measure.v index 654deb43e1..cb43b8c8d5 100644 --- a/theories/measure_theory/probability_measure.v +++ b/theories/measure_theory/probability_measure.v @@ -8,34 +8,40 @@ From mathcomp Require Import measurable_structure measure_function dirac_measure (**md**************************************************************************) (* # Probability Measures *) (* *) -(* ``` *) -(* isSubProbability == interface for functions that satisfy the *) -(* property of subprobability *) -(* The HB class is SubProbability. *) -(* subprobability T R == subprobability measure over the *) -(* measurableType T with values in \bar R with *) -(* R : realType *) -(* The HB class is SubProbability. *) -(* Measure_isSubProbability == interface that extends measures to *) -(* subprobability measures *) -(* isProbability == interface for functions that satisfy the *) -(* property of probability measures *) -(* The HB class is Probability. *) -(* probability T R == type of probability measure over the *) -(* measurableType T with values in \bar R *) -(* with R : realType *) -(* Measure_isProbability == interface that extends measures to *) -(* probability measures *) -(* mnormalize mu == normalization of a measure to a probability *) -(* ``` *) +(* `isSubProbability` *) +(* ~ interface for functions that satisfy the property of *) +(* subprobability. The HB class is `SubProbability`. *) (* *) -(* ``` *) -(* mset U r == the set of probability measures mu such that *) -(* mu U < r *) -(* pset == the sets mset U r with U measurable and *) -(* r \in [0,1] *) -(* pprobability == the measurable type generated by pset *) -(* ``` *) +(* `subprobability T R` *) +(* ~ subprobability measure over the `measurableType T` with values *) +(* in `\bar R` with `R : realType`. The HB class is *) +(* `SubProbability`. *) +(* *) +(* `Measure_isSubProbability` *) +(* ~ interface that extends measures to subprobability measures *) +(* *) +(* `isProbability` *) +(* ~ interface for functions that satisfy the property of *) +(* probability measures. The HB class is `Probability`. *) +(* *) +(* `probability T R` *) +(* ~ type of probability measure over the `measurableType T` with *) +(* values in `\bar R` with `R : realType` *) +(* *) +(* `Measure_isProbability` *) +(* ~ interface that extends measures to probability measures *) +(* *) +(* `mnormalize mu` *) +(* ~ normalization of a measure to a probability *) +(* *) +(* `mset U r` *) +(* ~ the set of probability measures `mu` such that `mu U < r` *) +(* *) +(* `pset` *) +(* ~ the sets `mset U r` with `U` measurable and `r \in [0,1]` *) +(* *) +(* `pprobability` *) +(* ~ the measurable type generated by `pset` *) (******************************************************************************) Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) diff --git a/theories/measure_theory/signed_measure.v b/theories/measure_theory/signed_measure.v index e9d02fee29..5d91f3300e 100644 --- a/theories/measure_theory/signed_measure.v +++ b/theories/measure_theory/signed_measure.v @@ -25,52 +25,71 @@ From mathcomp Require Import measure_function measure_negligible. (* reasoning on probabilistic programs. APLAS 2025 *) (* *) (* ## 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 *) -(* The HB class is AdditiveCharge. *) -(* {charge set T -> \bar R} == type of charges over T a semiring of sets *) -(* where R is a numFieldType *) -(* The HB class is Charge. *) -(* isCharge == factory corresponding to the "textbook *) -(* definition" of charges *) -(* ``` *) +(* `{additive_charge set T -> \bar R}` *) +(* ~ notation for additive charges where `T` is a semiring of sets *) +(* and `R` is a `numFieldType`. The HB class is `AdditiveCharge` *) +(* *) +(* `{charge set T -> \bar R}` *) +(* ~ type of charges over `T` a semiring of sets where `R` is a *) +(* `numFieldType`. The HB class is `Charge` *) +(* *) +(* `isCharge` *) +(* ~ factory corresponding to the "textbook definition" of charges *) (* *) (* ## 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 *) -(* where mD is a proof that D is measurable *) -(* crestr0 nu mD == csrestr nu mD that returns 0 for *) -(* non-measurable sets *) -(* czero == zero charge *) -(* cscale r nu == charge nu scaled by a factor r : R *) -(* copp nu == the charge corresponding to the opposite of *) -(* the charges nu *) -(* cadd n1 n2 == the charge corresponding to the sum of *) -(* charges n1 and n2 *) -(* charge_of_finite_measure mu == charge corresponding to a finite measure mu *) -(* ``` *) +(* `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` where `mD` is *) +(* a proof that `D` is measurable *) +(* *) +(* `crestr0 nu mD` *) +(* ~ `csrestr nu mD` that returns `0` for non-measurable sets *) +(* *) +(* `czero` *) +(* ~ zero charge *) +(* *) +(* `cscale r nu` *) +(* ~ charge `nu` scaled by a factor `r : R` *) +(* *) +(* `copp nu` *) +(* ~ the charge corresponding to the opposite of the charges `nu` *) +(* *) +(* `cadd n1 n2` *) +(* ~ the charge corresponding to the sum of charges `n1` and `n2` *) +(* *) +(* `charge_of_finite_measure mu` *) +(* ~ charge corresponding to a finite measure `mu` *) (* *) (* ## 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, *) -(* a positive set and a negative set for the *) -(* charge nu *) -(* jordan_pos nuPN == the charge obtained by restricting the charge *) -(* nu to the positive set P of the Hahn *) -(* decomposition nuPN: hahn_decomposition nu P N *) -(* jordan_neg nuPN == the charge obtained by restricting the charge *) -(* nu to the positive set N of the Hahn *) -(* decomposition nuPN: hahn_decomposition nu P N *) -(* charge_variation nuPN == variation of the charge nu *) -(* := jordan_pos nuPN \+ jordan_neg nuPN *) -(* charge_dominates mu nuPN := content_dominates mu (charge_variation nuPN) *) -(* ``` *) +(* `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`, a positive set *) +(* and a negative set for the charge `nu` *) +(* *) +(* `jordan_pos nuPN` *) +(* ~ the charge obtained by restricting the charge `nu` to the *) +(* positive set `P` of the Hahn decomposition *) +(* `nuPN`: `hahn_decomposition nu P N` *) +(* *) +(* `jordan_neg nuPN` *) +(* ~ the charge obtained by restricting the charge `nu` to the *) +(* positive set `N` of the Hahn decomposition *) +(* `nuPN`: `hahn_decomposition nu P N` *) +(* *) +(* `charge_variation nuPN` *) +(* ~ variation of the charge `nu` *) +(* ~ `:= jordan_pos nuPN \+ jordan_neg nuPN` *) +(* *) +(* `charge_dominates mu nuPN` *) +(* ~ `content_dominates mu (charge_variation nuPN)` *) (* *) (******************************************************************************) diff --git a/theories/normedtype_theory/complete_normed_module.v b/theories/normedtype_theory/complete_normed_module.v index 3df19393c5..fe8d7e6c3c 100644 --- a/theories/normedtype_theory/complete_normed_module.v +++ b/theories/normedtype_theory/complete_normed_module.v @@ -9,11 +9,10 @@ From mathcomp Require Import normed_module. (**md**************************************************************************) (* # Complete normed modules *) (* *) -(* ``` *) -(* completeNormedModType K == interface type for a complete normed *) -(* module structure over a realFieldType K *) -(* The HB class is CompleteNormedModule. *) -(* ``` *) +(* `completeNormedModType K` *) +(* ~ interface type for a complete normed module structure over a *) +(* `realFieldType` `K` *) +(* The HB class is `CompleteNormedModule`. *) (******************************************************************************) Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) diff --git a/theories/normedtype_theory/ereal_normedtype.v b/theories/normedtype_theory/ereal_normedtype.v index 59e9d3ffb2..3c2b6390f0 100644 --- a/theories/normedtype_theory/ereal_normedtype.v +++ b/theories/normedtype_theory/ereal_normedtype.v @@ -13,19 +13,16 @@ From mathcomp Require Import real_interval num_normedtype. (* of normed modules in this directory. *) (* *) (* ## Limit superior and inferior *) -(* ``` *) -(* limf_esup f F, limf_einf f F == limit sup/inferior of f at "filter" F *) -(* f has type X -> \bar R. *) -(* F has type set_system X. *) -(* ``` *) +(* `limf_esup f F, limf_einf f F` *) +(* ~ limit sup/inferior of `f` at "filter" `F` *) +(* ~ `f` has type `X -> \bar R`. *) +(* ~ `F` has type `set_system X`. *) (* *) (* ## Lower semicontinuous *) -(* ``` *) -(* lower_semicontinuous f == the extended real-valued function f is *) -(* lower-semicontinuous. The type of f is *) -(* X -> \bar R with X : topologicalType and *) -(* R : realType *) -(* ``` *) +(* `lower_semicontinuous f` *) +(* ~ the extended real-valued function `f` is lower-semicontinuous. *) +(* The type of `f` is `X -> \bar R` with `X : topologicalType` *) +(* and `R : realType` *) (* *) (******************************************************************************) diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v index 898c47a7bf..21269b6ede 100644 --- a/theories/normedtype_theory/matrix_normedtype.v +++ b/theories/normedtype_theory/matrix_normedtype.v @@ -15,10 +15,9 @@ From mathcomp Require Import normed_module. (* the Heine-Borel theorem, more precisely that a closed and bounded set of *) (* vectors in $\bar{R}^n$ is compact and various lemmas about compact sets. *) (* *) -(* ``` *) -(* mx_norm M == norm of the matrix M *) -(* := \big[maxr/0]_i `|x i.1 i.2| *) -(* ``` *) +(* `mx_norm M` *) +(* ~ norm of the matrix `M` *) +(* ~ ``:= \big[maxr/0]_i `|x i.1 i.2|`` *) (******************************************************************************) Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index d68d5eb3d8..ee37073be8 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -15,54 +15,71 @@ From mathcomp Require Import ereal_normedtype pseudometric_normed_Zmodule. (* We define normed modules. We prove the intermediate value theorem (IVT). *) (* *) (* ## Normed modules *) -(* ``` *) -(* normedModType K == interface type for a normed module *) -(* structure over the numDomainType K *) -(* The HB class is NormedModule. *) -(* subNormedModType R V S == join of *) -(* SubChoice *) -(* NormedModule *) -(* SubLmodule *) -(* SubNormedZmodule *) -(* SubConvexTvs *) -(* normedVectType K == interface type for a normed vectType *) -(* structure over the numDomainType K *) -(* The HB class is NormedVector. *) -(* `|x| == the norm of x (notation from ssrnum.v) *) -(* ``` *) +(* `normedModType K` *) +(* ~ interface type for a normed module structure over the *) +(* `numDomainType` `K` *) +(* ~ The HB class is `NormedModule`. *) +(* *) +(* `subNormedModType R V S` *) +(* ~ join of `SubChoice`, `NormedModule`, `SubLmodule`, *) +(* `SubNormedZmodule`, `SubConvexTvs` *) +(* *) +(* `normedVectType K` *) +(* ~ interface type for a normed `vectType` structure over the *) +(* `numDomainType` `K` *) +(* ~ The HB class is `NormedVector`. *) +(* *) +(* `` `|x| `` *) +(* ~ the norm of `x` (notation from `ssrnum.v`) *) (* *) (* We endow `numFieldType` with the types of norm-related notions (accessible *) (* with `Import numFieldNormedType.Exports`). *) (* *) -(* ``` *) -(* pseudoMetric_normed M == an alias for the pseudometric structure defined *) -(* from a normed module *) -(* M : normedZmodType K with K : numFieldType. *) -(* Lmodule_isNormed M == factory for a normed module defined using *) -(* an L-module M over R : numFieldType *) -(* subLmodule_isSubNormedmodule R V S == light-weight factory that builds a *) -(* SubNormedmodule given a SubLmodule over a *) -(* normedModType *) -(* ``` *) +(* `pseudoMetric_normed M` *) +(* ~ an alias for the pseudometric structure defined from a *) +(* normed module `M : normedZmodType K` with `K : numFieldType`. *) +(* *) +(* `Lmodule_isNormed M` *) +(* ~ factory for a normed module defined using an L-module `M` *) +(* over `R : numFieldType` *) +(* *) +(* `subLmodule_isSubNormedmodule R V S` *) +(* ~ light-weight factory that builds a `SubNormedmodule` given a *) +(* `SubLmodule` over a `normedModType` *) (* ## Hulls *) -(* ``` *) -(* Rhull A == the real interval hull of a set A *) -(* ``` *) +(* `Rhull A` *) +(* ~ the real interval hull of a set `A` *) (* *) (* ## Lipschitz functions *) -(* ``` *) -(* self_sub f x := f x.1 - f x.2 *) -(* lipschitz_on f F == f is lipschitz near F *) -(* k.-lipschitz_on f F == f is k.-lipschitz near F *) -(* k.-lipschitz_A f == f is k.-lipschitz on A *) -(* k.-lipschitz f := k.-lipschitz_setT *) -(* [lipschitz f x | x in A] == f is lipschitz on A *) -(* [locally [lipschitz f x | x in A] == f is locally lipschitz on A *) -(* [locally k.-lipschitz_A f] == f is locally k.-lipschitz on A *) -(* contraction q f == f is q.-lipschitz and q < 1 *) -(* is_contraction f == exists q, f is q.-lipschitz and q < 1 *) +(* `self_sub f x` *) +(* ~ `f x.1 - f x.2` *) +(* *) +(* `lipschitz_on f F` *) +(* ~ `f` is lipschitz near `F` *) +(* *) +(* `k.-lipschitz_on f F` *) +(* ~ `f` is `k.-lipschitz` near `F` *) +(* *) +(* `k.-lipschitz_A f` *) +(* ~ `f` is `k.-lipschitz` on `A` *) +(* *) +(* `k.-lipschitz f` *) +(* ~ `k.-lipschitz_setT` *) +(* *) +(* `[lipschitz f x | x in A]` *) +(* ~ `f` is lipschitz on `A` *) +(* *) +(* `[locally [lipschitz f x | x in A]` *) +(* ~ `f` is locally lipschitz on `A` *) +(* *) +(* `[locally k.-lipschitz_A f]` *) +(* ~ `f` is locally `k.-lipschitz` on `A` *) +(* *) +(* `contraction q f` *) +(* ~ `f` is `q.-lipschitz` and `q < 1` *) (* *) -(* ``` *) +(* `is_contraction f` *) +(* ~ exists `q`, `f` is `q.-lipschitz` and `q < 1` *) (* *) (******************************************************************************) diff --git a/theories/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v index 9457d67f93..47d0afff74 100644 --- a/theories/normedtype_theory/num_normedtype.v +++ b/theories/normedtype_theory/num_normedtype.v @@ -14,29 +14,29 @@ From mathcomp Require Import topology prodnormedzmodule. (* notions of numeric types that are useful to develop the theory of normed *) (* modules in this directory. *) (* *) -(* ``` *) -(* pinfty_nbhs == filter for +oo (for a numFieldType) *) -(* Notation: +oo (ring_scope) *) -(* ninfty_nbhs == filter for -oo (for a numFieldType) *) -(* Notation: -oo (ring_scope) *) -(* is_interval E == the set E is an interval *) -(* bigcup_ointsub U q == union of open real intervals included *) -(* in U and that contain the rational *) -(* number q *) -(* ``` *) +(* `pinfty_nbhs` *) +(* ~ filter for `+oo` (for a `numFieldType`) Notation: `+oo` *) +(* (`ring_scope`) *) (* *) -(* ``` *) -(* f @`[ a , b ], f @`] a , b [ == notations for images of intervals, *) -(* intended for continuous, monotonous *) -(* functions, defined in ring_scope and *) -(* classical_set_scope respectively as: *) -(* f @`[ a , b ] := `[minr (f a) (f b), maxr (f a) (f b)]%O *) -(* f @`] a , b [ := `]minr (f a) (f b), maxr (f a) (f b)[%O *) -(* f @`[ a , b ] := `[minr (f a) (f b), *) -(* maxr (f a) (f b)]%classic *) -(* f @`] a , b [ := `]minr (f a) (f b), *) -(* maxr (f a) (f b)[%classic *) -(* ``` *) +(* `ninfty_nbhs` *) +(* ~ filter for `-oo` (for a `numFieldType`) Notation: `-oo` *) +(* (`ring_scope`) *) +(* *) +(* `is_interval E` *) +(* ~ the set `E` is an interval *) +(* *) +(* `bigcup_ointsub U q` *) +(* ~ union of open real intervals included in `U` and that contain *) +(* the rational number `q` *) +(* *) +(* ``f @`[ a , b ], f @`] a , b [`` *) +(* ~ notations for images of intervals, intended for continuous, *) +(* monotonous functions, defined in `ring_scope` and *) +(* `classical_set_scope` respectively as: *) +(* ~ ``f @`[ a , b ] := `[minr (f a) (f b), maxr (f a) (f b)]%O`` *) +(* ~ ``f @`] a , b [ := `]minr (f a) (f b), maxr (f a) (f b)[%O`` *) +(* ~ ``f @`[ a , b ] := `[minr (f a) (f b), maxr (f a) (f b)]%classic`` *) +(* ~ ``f @`] a , b [ := `]minr (f a) (f b), maxr (f a) (f b)[%classic`` *) (* *) (******************************************************************************) diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 9bacaccb3f..c1778e7dda 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -15,48 +15,62 @@ From mathcomp Require Import prodnormedzmodule num_normedtype. (* *) (* ## Helper functions *) (* To be used in `normed_module.v`. *) -(* ``` *) -(* shift x y == y + x *) -(* center c := shift (- c) *) -(* This is a notation. *) -(* ``` *) +(* `shift x y` *) +(* ~ `y + x` *) +(* *) +(* `center c` *) +(* ~ `shift (- c)` *) +(* ~ This is a notation. *) (* *) (* ## Left and right filters *) -(* ``` *) -(* x^'-, x^'+ == filters on real numbers for predicates *) -(* s.t. nbhs holds on the left/right of x *) -(* ``` *) +(* `x^'-, x^'+` *) +(* ~ filters on real numbers for predicates s.t. `nbhs` holds on the *) +(* left/right of `x` *) (* *) (* ## Normed topological abelian groups *) -(* ``` *) -(* pseudoMetricNormedZmodType R == interface type for a normed topological *) -(* abelian group equipped with a norm *) -(* The HB class is PseudoMetricNormedZmod. *) -(* NormedZmoduleMetric == factory for pseudoMetricNormedZmodType *) -(* based on metric structures *) -(* ``` *) +(* `pseudoMetricNormedZmodType R` *) +(* ~ interface type for a normed topological abelian group equipped *) +(* with a norm *) +(* ~ the HB class is `PseudoMetricNormedZmod` *) +(* *) +(* `NormedZmoduleMetric` *) +(* ~ factory for `pseudoMetricNormedZmodType` based on metric *) +(* structures *) (* *) (* ## Closed balls *) -(* ``` *) -(* closed_ball_ norm x e := [set y | norm (x - y) <= e] *) -(* closed_ball == closure of a ball *) -(* ``` *) +(* `closed_ball_ norm x e` *) +(* ~ `[set y | norm (x - y) <= e]` *) +(* *) +(* `closed_ball` *) +(* ~ closure of a ball *) (* *) (* ## Domination *) -(* ``` *) -(* dominated_by h k f F == `|f| <= k * `|h|, near F *) -(* strictly_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 *) -(* [locally [bounded f x | x in A] == f is locally bounded on A *) -(* bounded_set == set of bounded sets *) -(* := [set A | [bounded x | x in A]] *) -(* bounded_fun == set of functions bounded on their *) -(* whole domain *) -(* := [set f | [bounded f x | x in setT]] *) -(* fun1 : T -> K^o := fun=> 1 *) -(* where K : numFiedlType *) -(* ``` *) +(* `dominated_by h k f F` *) +(* ~ `` `|f| <= k * `|h| ``, near `F` *) +(* *) +(* `strictly_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` *) +(* *) +(* `[locally [bounded f x | x in A]` *) +(* ~ `f` is locally bounded on `A` *) +(* *) +(* `bounded_set` *) +(* ~ set of bounded sets *) +(* ~ `:= [set A | [bounded x | x in A]]` *) +(* *) +(* `bounded_fun` *) +(* ~ set of functions bounded on their whole domain *) +(* ~ `:= [set f | [bounded f x | x in setT]]` *) +(* *) +(* `fun1 : T -> K^o` *) +(* ~ `fun=> 1` *) +(* ~ where `K : numFiedlType` *) (* *) (******************************************************************************) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 41126a781d..8b5f3769b7 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -12,64 +12,92 @@ From mathcomp Require Import pseudometric_normed_Zmodule. (* # Topological vector spaces *) (* *) (* This file introduces locally convex topological vector spaces. *) -(* ``` *) -(* NbhsNmodule == HB class, join of Nbhs and Nmodule *) -(* NbhsZmodule == HB class, join of Nbhs and Zmodule *) -(* NbhsLmodule K == HB class, join of Nbhs and Lmodule over K *) -(* K is a numDomainType. *) -(* PreTopologicalNmodule == HB class, join of Topological and Nmodule *) -(* TopologicalNmodule == HB class, PreTopologicalNmodule with a *) -(* continuous addition *) -(* PreTopologicalZmodule == HB class, join of Topological and Zmodule *) -(* topologicalZmodType == topological abelian group *) -(* TopologicalZmodule == HB class, join of TopologicalNmodule and *) -(* Zmodule with a continuous opposite operator *) -(* preTopologicalLmodType K == topological space and Lmodule over K *) -(* K is a numDomainType *) -(* The HB class is PreTopologicalLmodule. *) -(* topologicalLmodType K == topologicalNmodule and Lmodule over K with a *) -(* continuous scaling operation *) -(* The HB class is TopologicalLmodule. *) -(* PreUniformNmodule == HB class, join of Uniform and Nmodule *) -(* UniformNmodule == HB class, join of Uniform and Nmodule with a *) -(* uniformly continuous addition *) -(* PreUniformZmodule == HB class, join of Uniform and Zmodule *) -(* UniformZmodule == HB class, join of UniformNmodule and Zmodule *) -(* with uniformly continuous opposite operator *) -(* PreUniformLmodule K == HB class, join of Uniform and Lmodule over K *) -(* K is a numDomainType. *) -(* UniformLmodule K == HB class, join of UniformNmodule and Lmodule *) -(* with a uniformly continuous scaling operation *) -(* K is a numFieldType. *) -(* convexTvsType R == interface type for a locally convex *) -(* tvs on a numDomain R *) -(* A convex tvs is constructed over a uniform *) -(* space. *) -(* The HB class is ConvexTvs. *) -(* subConvexTvsType R V S == join of subTopologicalType, convexTvsType, *) -(* and subLmoduleType *) -(* The HB class is SubConvexTvs. *) -(* Instance: in particular, it is shown that a *) -(* sub-Lmodule is a sub-convex TVS. *) -(* PreTopologicalLmod_isConvexTvs == factory allowing the construction of a *) -(* convex tvs from an Lmodule which is also a *) -(* topological space *) -(* {linear_continuous E -> F} == the type of all linear and continuous *) -(* functions between E and F, where E is a *) -(* NbhsLmodule.type and F a NbhsZmodule.type over *) -(* a numDomainType R *) -(* The HB class is called LinearContinuous. *) -(* The notation {linear_continuous E -> F | s} *) -(* also exists. *) -(* lcfun E F s == membership predicate for linear continuous *) -(* functions of type E -> F with scalar operator *) -(* s : K -> F -> F *) -(* E and F have type convexTvsType K. *) -(* This is used in particular to attach a type of *) -(* lmodType to {linear_continuous E -> F | s}. *) -(* lcfun_spec f == specification for membership of the linear *) -(* continuous function f *) -(* ``` *) +(* `NbhsNmodule` *) +(* ~ HB class, join of `Nbhs` and `Nmodule` *) +(* *) +(* `NbhsZmodule` *) +(* ~ HB class, join of `Nbhs` and `Zmodule` *) +(* *) +(* `NbhsLmodule K` *) +(* ~ HB class, join of `Nbhs` and `Lmodule` over `K`. `K` is a *) +(* `numDomainType`. *) +(* *) +(* `PreTopologicalNmodule` *) +(* ~ HB class, join of `Topological` and `Nmodule` *) +(* *) +(* `TopologicalNmodule` *) +(* ~ HB class, `PreTopologicalNmodule` with a continuous addition *) +(* *) +(* `PreTopologicalZmodule` *) +(* ~ HB class, join of `Topological` and `Zmodule` *) +(* *) +(* `topologicalZmodType` *) +(* ~ topological abelian group *) +(* *) +(* `TopologicalZmodule` *) +(* ~ HB class, join of `TopologicalNmodule` and `Zmodule` with a *) +(* continuous opposite operator *) +(* *) +(* `preTopologicalLmodType K` *) +(* ~ topological space and `Lmodule` over `K`. `K` is a *) +(* `numDomainType`. The HB class is `PreTopologicalLmodule`. *) +(* *) +(* `topologicalLmodType K` *) +(* ~ `topologicalNmodule` and `Lmodule` over `K` with a continuous *) +(* scaling operation. The HB class is `TopologicalLmodule`. *) +(* *) +(* `PreUniformNmodule` *) +(* ~ HB class, join of `Uniform` and `Nmodule` *) +(* *) +(* `UniformNmodule` *) +(* ~ HB class, join of `Uniform` and `Nmodule` with a uniformly *) +(* continuous addition *) +(* *) +(* `PreUniformZmodule` *) +(* ~ HB class, join of `Uniform` and `Zmodule` *) +(* *) +(* `UniformZmodule` *) +(* ~ HB class, join of `UniformNmodule` and `Zmodule` with uniformly *) +(* continuous opposite operator *) +(* *) +(* `PreUniformLmodule K` *) +(* ~ HB class, join of `Uniform` and `Lmodule` over `K`. `K` is a *) +(* `numDomainType`. *) +(* *) +(* `UniformLmodule K` *) +(* ~ HB class, join of `UniformNmodule` and `Lmodule` with a uniformly *) +(* continuous scaling operation. `K` is a `numFieldType`. *) +(* *) +(* `convexTvsType R` *) +(* ~ interface type for a locally convex tvs on a numDomain `R`. A *) +(* convex tvs is constructed over a uniform space. The HB class is *) +(* `ConvexTvs`. *) +(* *) +(* `subConvexTvsType R V S` *) +(* ~ join of `subTopologicalType`, `convexTvsType`, and *) +(* `subLmoduleType`. The HB class is `SubConvexTvs`. Instance: in *) +(* particular, it is shown that a sub-Lmodule is a sub-convex TVS. *) +(* *) +(* `PreTopologicalLmod_isConvexTvs` *) +(* ~ factory allowing the construction of a convex tvs from an *) +(* `Lmodule` which is also a topological space *) +(* *) +(* `{linear_continuous E -> F}` *) +(* ~ the type of all linear and continuous functions between `E` and *) +(* `F`, where `E` is a `NbhsLmodule.type` and `F` a *) +(* `NbhsZmodule.type` over a `numDomainType` `R`. The HB class is *) +(* called `LinearContinuous`. The notation *) +(* `{linear_continuous E -> F | s}` also exists. *) +(* *) +(* `lcfun E F s` *) +(* ~ membership predicate for linear continuous functions of type *) +(* `E -> F` with scalar operator `s : K -> F -> F`. `E` and `F` have *) +(* type `convexTvsType K`. This is used in particular to attach a *) +(* type of `lmodType` to `{linear_continuous E -> F | s}`. *) +(* *) +(* `lcfun_spec f` *) +(* ~ specification for membership of the linear continuous function *) +(* `f` *) (* HB instances: *) (* - The type R^o (R : numFieldType) is endowed with the structure of *) (* ConvexTvs. *) diff --git a/theories/normedtype_theory/urysohn.v b/theories/normedtype_theory/urysohn.v index 370392ff28..fa86315a1f 100644 --- a/theories/normedtype_theory/urysohn.v +++ b/theories/normedtype_theory/urysohn.v @@ -12,23 +12,29 @@ From mathcomp Require Import normed_module. (**md**************************************************************************) (* # Urysohn's lemma *) (* *) -(* ``` *) -(* edist == the extended distance function for a *) -(* pseudometric X, from X * X -> \bar R *) -(* edist_inf A == the infimum of distances to the set A *) -(* uniform_separator A B == there is a suitable uniform space and *) -(* entourage separating A and B *) -(* Urysohn A B == a continuous function T -> [0,1] which *) -(* separates A and B when *) -(* `uniform_separator A B` *) -(* completely_regular_space == a space where points and closed sets can *) -(* be separated by a function into R *) -(* completely_regular_uniformity == equips a completely_regular_space with *) -(* the uniformity induced by continuous *) -(* functions into the reals *) -(* note this uniformity is always the only *) -(* choice, so its placed in a module *) -(* ``` *) +(* `edist` *) +(* ~ the extended distance function for a pseudometric `X`, from *) +(* `X * X -> \bar R` *) +(* *) +(* `edist_inf A` *) +(* ~ the infimum of distances to the set `A` *) +(* *) +(* `uniform_separator A B` *) +(* ~ there is a suitable uniform space and entourage separating `A` *) +(* and `B` *) +(* *) +(* `Urysohn A B` *) +(* ~ a continuous function `T -> [0,1]` which separates `A` and `B` *) +(* when `uniform_separator A B` *) +(* *) +(* `completely_regular_space` *) +(* ~ a space where points and closed sets can be separated by a *) +(* function into `R` *) +(* *) +(* `completely_regular_uniformity` *) +(* ~ equips a `completely_regular_space` with the uniformity induced *) +(* by continuous functions into the reals note this uniformity is *) +(* always the only choice, so its placed in a module *) (* *) (******************************************************************************) diff --git a/theories/normedtype_theory/vitali_lemma.v b/theories/normedtype_theory/vitali_lemma.v index 050f6a3005..47016109b2 100644 --- a/theories/normedtype_theory/vitali_lemma.v +++ b/theories/normedtype_theory/vitali_lemma.v @@ -19,16 +19,23 @@ From mathcomp Require Import normed_module. (* *) (* This file also provides the infinite version of Vitali's covering lemma. *) (* *) -(* ``` *) -(* cpoint A == the center of the set A when A is an open ball *) -(* radius A == the radius of the set A when A is an open ball *) -(* Radius A has type {nonneg R} with R a numDomainType. *) -(* is_ball A == boolean predicate that holds when A is an open ball *) -(* k *` A == open ball with center cpoint A and radius k * radius A *) -(* when 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 *) -(* ``` *) +(* `cpoint A` *) +(* ~ the center of the set `A` when `A` is an open ball *) +(* *) +(* `radius A` *) +(* ~ the radius of the set `A` when `A` is an open ball *) +(* ~ `radius A` has type `{nonneg R}` with `R` a `numDomainType` *) +(* *) +(* `is_ball A` *) +(* ~ boolean predicate that holds when `A` is an open ball *) +(* *) +(* ``k *` A`` *) +(* ~ open ball with center `cpoint A` and radius `k * radius A` *) +(* when `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` *) (* *) (******************************************************************************) diff --git a/theories/numfun.v b/theories/numfun.v index 75de0d05ee..9c6e0dbfe2 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -15,26 +15,40 @@ From mathcomp Require Import topology normedtype sequences. (* the fact that numerical functions with a finite image from a (potentially *) (* zero) ring) and theorems such as Tietze's extension theorem. *) (* *) -(* ``` *) -(* itv_partition a b s == s is a partition of the interval `[a, b] *) -(* itv_partitionL s c == the left side of splitting a partition at c *) -(* itv_partitionR s c == the right side of splitting a partition at c *) -(* variation a b f s == the sum of f at all points in the partition s *) -(* variations a b f == the set of all variations of f between a and b *) -(* bounded_variation a b f == all variations of f are bounded *) -(* {nnfun T >-> R} == type of non-negative functions *) -(* f ^\+ == the function formed by the non-negative outputs *) -(* of f and 0 otherwise *) -(* The codomain of f is the real numbers in scope *) -(* ring_scope and the extended real numbers in *) -(* scope ereal_scope. *) -(* Rendered as f ⁺ with company-coq (U+207A). *) -(* f ^\- == the function formed by the non-positive outputs *) -(* of f and 0 o.w. *) -(* Similar to ^\+. *) -(* Rendered as f ⁻ with company-coq (U+207B). *) -(* \1_ A == indicator function 1_A *) -(* ``` *) +(* `itv_partition a b s` *) +(* ~ `s` is a partition of the interval `` `[a, b] `` *) +(* *) +(* `itv_partitionL s c` *) +(* ~ the left side of splitting a partition at `c` *) +(* *) +(* `itv_partitionR s c` *) +(* ~ the right side of splitting a partition at `c` *) +(* *) +(* `variation a b f s` *) +(* ~ the sum of `f` at all points in the partition `s` *) +(* *) +(* `variations a b f` *) +(* ~ the set of all variations of `f` between `a` and `b` *) +(* *) +(* `bounded_variation a b f` *) +(* ~ all variations of `f` are bounded *) +(* *) +(* `{nnfun T >-> R}` *) +(* ~ type of non-negative functions *) +(* *) +(* `f ^\+` *) +(* ~ the function formed by the non-negative outputs of `f` and `0` *) +(* otherwise. The codomain of `f` is the real numbers in scope *) +(* `ring_scope` and the extended real numbers in scope *) +(* `ereal_scope`. Rendered as `f ⁺` with company-coq (U+207A). *) +(* *) +(* `f ^\-` *) +(* ~ the function formed by the non-positive outputs of `f` and `0` *) +(* o.w. Similar to `^\+`. Rendered as `f ⁻` with company-coq *) +(* (U+207B). *) +(* *) +(* `\1_ A` *) +(* ~ indicator function `1_A` *) (* *) (******************************************************************************) diff --git a/theories/probability_theory/bernoulli_distribution.v b/theories/probability_theory/bernoulli_distribution.v index 16a4960c2e..80989c4690 100644 --- a/theories/probability_theory/bernoulli_distribution.v +++ b/theories/probability_theory/bernoulli_distribution.v @@ -13,11 +13,12 @@ From mathcomp Require Import lebesgue_integral kernel. (**md**************************************************************************) (* # Bernoulli distribution *) (* *) -(* ``` *) -(* bernoulli_pmf p == Bernoulli pmf with parameter p : R *) -(* bernoulli_prob p == Bernoulli probability measure when 0 <= p <= 1 *) -(* and \d_false otherwise *) -(* ``` *) +(* `bernoulli_pmf p` *) +(* ~ Bernoulli pmf with parameter `p : R` *) +(* *) +(* `bernoulli_prob p` *) +(* ~ Bernoulli probability measure when `0 <= p <= 1` and `\d_false` *) +(* otherwise *) (* *) (******************************************************************************) diff --git a/theories/probability_theory/beta_distribution.v b/theories/probability_theory/beta_distribution.v index 4db8a20854..1f637c648b 100644 --- a/theories/probability_theory/beta_distribution.v +++ b/theories/probability_theory/beta_distribution.v @@ -17,15 +17,23 @@ From mathcomp Require Import uniform_distribution bernoulli_distribution. (* This file provides basic notions of probability theory. See measure.v for *) (* the type probability T R (a measure that sums to 1). *) (* *) -(* ``` *) -(* XMonemX a b := x ^+ a * x.~ ^+ b *) -(* beta_fun a b := \int[mu]_x (XMonemX a.-1 b.-1 \_`[0,1] x) *) -(* beta_pdf == probability density function for beta *) -(* beta_prob == beta probability measure *) -(* div_beta_fun a b c d := beta_fun (a + c) (b + d) / beta_fun a b *) -(* beta_prob_bernoulli_prob a b c d U := \int[beta_prob a b]_(y \in [0, 1]) *) -(* bernoulli_prob (XMonemX c d) U *) -(* ``` *) +(* `XMonemX a b` *) +(* ~ `x ^+ a * x.~ ^+ b` *) +(* *) +(* `beta_fun a b` *) +(* ~ ``\int[mu]_x (XMonemX a.-1 b.-1 \_`[0,1] x)`` *) +(* *) +(* `beta_pdf` *) +(* ~ probability density function for beta *) +(* *) +(* `beta_prob` *) +(* ~ beta probability measure *) +(* *) +(* `div_beta_fun a b c d` *) +(* ~ `beta_fun (a + c) (b + d) / beta_fun a b` *) +(* *) +(* `beta_prob_bernoulli_prob a b c d U` *) +(* ~ `\int[beta_prob a b]_(y \in [0, 1]) bernoulli_prob (XMonemX c d) U` *) (* *) (******************************************************************************) diff --git a/theories/probability_theory/binomial_distribution.v b/theories/probability_theory/binomial_distribution.v index 357f25af89..085061ef40 100644 --- a/theories/probability_theory/binomial_distribution.v +++ b/theories/probability_theory/binomial_distribution.v @@ -13,14 +13,17 @@ From mathcomp Require Import lebesgue_integral bernoulli_distribution. (**md**************************************************************************) (* # Binomial distribution *) (* *) -(* ``` *) -(* binomial_pmf n p == binomial pmf with parameters n : nat and p : R *) -(* binomial_prob n p == binomial probability measure when 0 <= p <= 1 *) -(* and \d_0%N otherwise *) -(* bin_prob n k p == $\binom{n}{k}p^k (1-p)^(n-k)$ *) -(* Computes a binomial distribution term for *) -(* k successes in n trials with success rate p *) -(* ``` *) +(* `binomial_pmf n p` *) +(* ~ binomial pmf with parameters `n : nat` and `p : R` *) +(* *) +(* `binomial_prob n p` *) +(* ~ binomial probability measure when `0 <= p <= 1` and `\d_0%N` *) +(* otherwise *) +(* *) +(* `bin_prob n k p` *) +(* ~ $\binom{n}{k}p^k (1-p)^(n-k)$ *) +(* ~ Computes a binomial distribution term for `k` successes in *) +(* `n` trials with success rate `p` *) (* *) (******************************************************************************) diff --git a/theories/probability_theory/exponential_distribution.v b/theories/probability_theory/exponential_distribution.v index b6e5fc7000..fd1998ae08 100644 --- a/theories/probability_theory/exponential_distribution.v +++ b/theories/probability_theory/exponential_distribution.v @@ -10,10 +10,11 @@ From mathcomp Require Import lebesgue_measure lebesgue_integral ftc. (**md**************************************************************************) (* # Exponential distribution *) (* *) -(* ``` *) -(* exponential_pdf r == pdf of the exponential distribution with rate r *) -(* exponential_prob r == exponential probability measure *) -(* ``` *) +(* `exponential_pdf r` *) +(* ~ pdf of the exponential distribution with rate `r` *) +(* *) +(* `exponential_prob r` *) +(* ~ exponential probability measure *) (* *) (******************************************************************************) diff --git a/theories/probability_theory/normal_distribution.v b/theories/probability_theory/normal_distribution.v index bbbe300f3f..9b403acb8b 100644 --- a/theories/probability_theory/normal_distribution.v +++ b/theories/probability_theory/normal_distribution.v @@ -11,14 +11,19 @@ From mathcomp Require Import lebesgue_integral ftc gauss_integral. (**md**************************************************************************) (* # Normal distribution *) (* *) -(* ``` *) -(* normal_peak s := (sqrtr (s ^+ 2 * pi *+ 2))^-1 *) -(* normal_fun m s x := expR (- (x - m) ^+ 2 / (s ^+ 2 *+ 2)) *) -(* normal_pdf m s == pdf of the normal distribution with mean m and *) -(* standard deviation s *) -(* Using normal_peak and normal_pdf. *) -(* normal_prob m s == normal probability measure *) -(* ``` *) +(* `normal_peak s` *) +(* ~ `(sqrtr (s ^+ 2 * pi *+ 2))^-1` *) +(* *) +(* `normal_fun m s x` *) +(* ~ `expR (- (x - m) ^+ 2 / (s ^+ 2 *+ 2))` *) +(* *) +(* `normal_pdf m s` *) +(* ~ pdf of the normal distribution with mean `m` and standard *) +(* deviation `s` *) +(* Using `normal_peak` and `normal_pdf`. *) +(* *) +(* `normal_prob m s` *) +(* ~ normal probability measure *) (* *) (******************************************************************************) diff --git a/theories/probability_theory/poisson_distribution.v b/theories/probability_theory/poisson_distribution.v index bd1cf24159..f80603e158 100644 --- a/theories/probability_theory/poisson_distribution.v +++ b/theories/probability_theory/poisson_distribution.v @@ -10,10 +10,11 @@ From mathcomp Require Import lebesgue_integral. (**md**************************************************************************) (* # Poisson distribution *) (* *) -(* ``` *) -(* poisson_pmf r k == pmf of the Poisson distribution with parameter r *) -(* poisson_prob r == Poisson probability measure *) -(* ``` *) +(* `poisson_pmf r k` *) +(* ~ pmf of the Poisson distribution with parameter `r` *) +(* *) +(* `poisson_prob r` *) +(* ~ Poisson probability measure *) (* *) (******************************************************************************) diff --git a/theories/probability_theory/uniform_distribution.v b/theories/probability_theory/uniform_distribution.v index 0f3d60a3bc..2b19cc35c0 100644 --- a/theories/probability_theory/uniform_distribution.v +++ b/theories/probability_theory/uniform_distribution.v @@ -10,11 +10,12 @@ From mathcomp Require Import lebesgue_measure lebesgue_integral. (**md**************************************************************************) (* # Uniform distribution *) (* *) -(* ``` *) -(* uniform_pdf a b == uniform pdf over the interval [a,b] *) -(* uniform_prob a b ab == uniform probability over the interval [a,b] *) -(* where ab0 a proof that 0 < b - a *) -(* ``` *) +(* `uniform_pdf a b` *) +(* ~ uniform pdf over the interval `[a,b]` *) +(* *) +(* `uniform_prob a b ab` *) +(* ~ uniform probability over the interval `[a,b]`, where `ab0` a proof *) +(* that `0 < b - a` *) (* *) (******************************************************************************) diff --git a/theories/realfun.v b/theories/realfun.v index 3aec286fca..cd452ec462 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -16,31 +16,33 @@ From mathcomp Require Import sequences real_interval numfun. (* numbers (e.g., the continuity of the inverse of a continuous function, *) (* L'Hopital's rule). *) (* *) -(* ``` *) +(* `derivable_oo_LRcontinuous f x y` *) +(* ~ `f` is derivable in `` `]x, y[ `` and continuous up to the *) +(* boundary, i.e., `f @ x^'+ --> f x` and `f @ y^'- --> f y` *) (* *) -(* derivable_oo_LRcontinuous f x y == f is derivable in `]x, y[ and *) -(* continuous up to the boundary, i.e., *) -(* f @ x^'+ --> f x and f @ y^'- --> f y *) -(* derivable_oy_Rcontinuous f x == f is derivable in `]x, +oo[ and *) -(* f @ x^'+ --> f x *) -(* derivable_Nyo_Lcontinuous f x == f is derivable in `]-oo, x[ and *) -(* f @ x^'- --> f x *) +(* `derivable_oy_Rcontinuous f x` *) +(* ~ `f` is derivable in `` `]x, +oo[ `` and `f @ x^'+ --> f x` *) (* *) -(* total_variation a b f == the sup over all variations of f from a to b *) -(* neg_tv a f x == the decreasing component of f *) -(* pos_tv a f x == the increasing component of f *) -(* ``` *) +(* `derivable_Nyo_Lcontinuous f x` *) +(* ~ `f` is derivable in `` `]-oo, x[ `` and `f @ x^'- --> f x` *) +(* *) +(* `total_variation a b f` *) +(* ~ the sup over all variations of `f` from `a` to `b` *) +(* *) +(* `neg_tv a f x` *) +(* ~ the decreasing component of `f` *) +(* *) +(* `pos_tv a f x` *) +(* ~ the increasing component of `f` *) (* *) (* Limit superior and inferior for functions: *) -(* ``` *) -(* lime_sup f a/lime_inf f a == limit sup/inferior of the extended real- *) -(* valued function f at point a *) -(* ``` *) +(* `lime_sup f a`/`lime_inf f a` *) +(* ~ limit sup/inferior of the extended real-valued function `f` at *) +(* point `a` *) (* *) (* Discontinuities: *) -(* ``` *) -(* discontinuity f r == r is a discontinuity of function f *) -(* ``` *) +(* `discontinuity f r` *) +(* ~ `r` is a discontinuity of function `f` *) (******************************************************************************) Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) diff --git a/theories/sequences.v b/theories/sequences.v index 52fce143cc..723f2ed206 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -13,62 +13,89 @@ From mathcomp Require Import ereal topology tvs normedtype landau. (* *) (* The purpose of this file is to gather generic definitions and lemmas about *) (* sequences. Incidentally, it defines the exponential function. *) -(* ``` *) -(* increasing_seq u == the sequence u is (strictly) increasing *) -(* decreasing_seq u == the sequence u is (strictly) decreasing *) -(* ``` *) +(* `increasing_seq u` *) +(* ~ the sequence `u` is (strictly) increasing *) +(* *) +(* `decreasing_seq u` *) +(* ~ the sequence `u` is (strictly) decreasing *) (* *) (* ## About sequences of real numbers *) -(* ``` *) -(* [sequence u_n]_n == the sequence of general element u_n *) -(* series u_ == the sequence of partial sums of u_ *) -(* telescope u_ := [sequence u_ n.+1 - u_ n]_n *) -(* harmonic == harmonic sequence *) -(* arithmetic == arithmetic sequence *) -(* geometric == geometric sequence *) -(* also arithmetic_mean, harmonic_mean, *) -(* root_mean_square *) -(* [series u_n]_n == the series of general element u_n *) -(* [normed S] == transforms a series S = [series u_n]_n in its *) -(* normed series [series `|u_n|]_n] (useful to *) -(* represent absolute and normed convergence: *) -(* cvg [norm S_n]) *) -(* exp_coeff n == the sequence of coefficients of the real *) -(* 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 F i` *) +(* ~ `lim (fun n => (\sum_) F i))` where `` can be *) +(* `(i = u_ n *) -(* nondecreasing_cvgn u_ == if u_ is nondecreasing and bounded then u_ *) -(* is convergent and its limit is sup u_n *) -(* nonincreasing_cvgn u_ == if u_ is nonincreasing u_ and bound by below *) -(* then u_ is convergent *) -(* adjacent_seq == adjacent sequences lemma *) -(* cesaro == Cesaro's lemma *) -(* ``` *) +(* `nonincreasing_cvgn_ge u_` *) +(* ~ if `u_` is nonincreasing and convergent then *) +(* `forall n, lim u_ <= u_ n` *) +(* *) +(* `nondecreasing_cvgn_le u_` *) +(* ~ if `u_` is nondecreasing and convergent then *) +(* `forall n, lim u_ >= u_ n` *) +(* *) +(* `nondecreasing_cvgn u_` *) +(* ~ if `u_` is nondecreasing and bounded then `u_` is convergent *) +(* and its limit is `sup u_n` *) +(* *) +(* `nonincreasing_cvgn u_` *) +(* ~ if `u_` is nonincreasing `u_` and bound by below then `u_` is *) +(* convergent *) +(* *) +(* `adjacent_seq` *) +(* ~ adjacent sequences lemma *) +(* *) +(* `cesaro` *) +(* ~ Cesaro's lemma *) (* *) (* ## About sequences of natural numbers *) -(* ``` *) -(* nseries u := fun n => \sum_(0 <= k < n) u k *) -(* where u has type nat^nat *) -(* ``` *) +(* `nseries u` *) +(* ~ `fun n => \sum_(0 <= k < n) u k` where `u` has type `nat^nat` *) (* *) (* ## About sequences of extended real numbers *) -(* ``` *) -(* eseries u := [sequence \sum_(0 <= k < n) u k]_n *) -(* where u has type (\bar R)^nat *) -(* etelescope u := [sequence u n.+1 - u n]_n *) -(* ``` *) +(* `eseries u` *) +(* ~ `[sequence \sum_(0 <= k < n) u k]_n` where `u` has type *) +(* `(\bar R)^nat` *) +(* *) +(* `etelescope u` *) +(* ~ `[sequence u n.+1 - u n]_n` *) (* *) (* Section sequences_ereal contain properties of sequences of extended real *) (* numbers. *) @@ -78,36 +105,48 @@ From mathcomp Require Import ereal topology tvs normedtype landau. (* "npeseries") as part of their identifier *) (* *) (* ## Limit superior and inferior for sequences *) -(* ``` *) -(* sdrop u n := {u_k | k >= n} *) -(* sups u := [sequence sup (sdrop u n)]_n *) -(* infs u := [sequence inf (sdrop u n)]_n *) -(* limn_sup, limn_inf == limit sup/inferior for a sequence of reals *) -(* esups u := [sequence ereal_sup (sdrop u n)]_n *) -(* einfs u := [sequence ereal_inf (sdrop u n)]_n *) -(* limn_esup u, limn_einf == limit sup/inferior for a sequence of *) -(* of extended reals *) -(* ``` *) +(* `sdrop u n` *) +(* ~ `{u_k | k >= n}` *) +(* *) +(* `sups u` *) +(* ~ `[sequence sup (sdrop u n)]_n` *) +(* *) +(* `infs u` *) +(* ~ `[sequence inf (sdrop u n)]_n` *) +(* *) +(* `limn_sup`, `limn_inf` *) +(* ~ limit sup/inferior for a sequence of reals *) (* *) -(* ``` *) -(* adjacent_set L R == L and R are two adjacent sets of real numbers *) -(* cut L R == L and R are two sets of real numbers that form *) -(* a cut *) -(* ``` *) +(* `esups u` *) +(* ~ `[sequence ereal_sup (sdrop u n)]_n` *) +(* *) +(* `einfs u` *) +(* ~ `[sequence ereal_inf (sdrop u n)]_n` *) +(* *) +(* `limn_esup u`, `limn_einf` *) +(* ~ limit sup/inferior for a sequence of extended reals *) +(* *) +(* `adjacent_set L R` *) +(* ~ `L` and `R` are two adjacent sets of real numbers *) +(* *) +(* `cut L R` *) +(* ~ `L` and `R` are two sets of real numbers that form a cut *) (* *) (* ## Bounded functions *) (* This section proves Baire's Theorem, stating that complete normed spaces *) (* are Baire spaces, and Banach-Steinhaus' theorem, stating that between a *) (* complete normed vector space and a normed vector spaces, pointwise bounded *) (* and uniformly bounded subset of functions correspond. *) -(* ``` *) -(* bounded_fun_norm f == a function between normed spaces transforms a *) -(* bounded set into a bounded set *) -(* pointwise_bounded F == F is a set of pointwise bounded functions *) -(* between normed spaces *) -(* uniform_bounded F == F is a set of uniform bounded functions *) -(* between normed spaces *) -(* ``` *) +(* `bounded_fun_norm f` *) +(* ~ a function between normed spaces transforms a bounded set into *) +(* a bounded set *) +(* *) +(* `pointwise_bounded F` *) +(* ~ `F` is a set of pointwise bounded functions between normed *) +(* spaces *) +(* *) +(* `uniform_bounded F` *) +(* ~ `F` is a set of uniform bounded functions between normed spaces *) (******************************************************************************) Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) diff --git a/theories/showcase/pnt.v b/theories/showcase/pnt.v index bb03bcb3d1..9bc685b8a3 100644 --- a/theories/showcase/pnt.v +++ b/theories/showcase/pnt.v @@ -12,9 +12,8 @@ Import Order.POrderTheory GRing.Theory Num.Theory. (* The main theorem proved so far is the divergence of the sum of the *) (* reciprocals of the prime numbers. *) (* *) -(* ``` *) -(* prime_seq == the sequence of prime numbers *) -(* ``` *) +(* `prime_seq` *) +(* ~ the sequence of prime numbers *) (* *) (******************************************************************************) diff --git a/theories/topology_theory/compact.v b/theories/topology_theory/compact.v index 6775a6058d..e35dbb55e0 100644 --- a/theories/topology_theory/compact.v +++ b/theories/topology_theory/compact.v @@ -9,27 +9,44 @@ From mathcomp Require Import uniform_structure pseudometric_structure. (* # Compactness *) (* This file provides various formulations of compactness, and some theory. *) (* *) -(* ``` *) -(* cluster F == set of cluster points of F *) -(* compact == set of compact sets w.r.t. the filter-based *) -(* definition of compactness *) -(* near_covering == a reformulation of covering compact better *) -(* suited for use with `near` *) -(* near_covering_within == equivalent definition of near_covering *) -(* compact_near F == the filter F contains a closed compact set *) -(* precompact A == A is contained in a closed compact set *) -(* locally_compact A == every point in A has a compact (and closed) *) -(* neighborhood *) -(* finite_subset_cover D F A == the family of sets F is a cover of A *) -(* for a finite number of indices in D *) -(* cover_compact == set of compact sets w.r.t. the open *) -(* cover-based definition of compactness *) -(* open_fam_of A D f == the family of f indexed by D restricted to A *) -(* is a family of open sets *) -(* closed_fam_of A D f == the family of f indexed by D restricted to A *) -(* is a family of closed sets *) +(* `cluster F` *) +(* ~ set of cluster points of `F` *) (* *) -(* ``` *) +(* `compact` *) +(* ~ set of compact sets w.r.t. the filter-based definition of *) +(* compactness *) +(* *) +(* `near_covering` *) +(* ~ a reformulation of covering compact better suited for use *) +(* with `near` *) +(* *) +(* `near_covering_within` *) +(* ~ equivalent definition of `near_covering` *) +(* *) +(* `compact_near F` *) +(* ~ the filter `F` contains a closed compact set *) +(* *) +(* `precompact A` *) +(* ~ `A` is contained in a closed compact set *) +(* *) +(* `locally_compact A` *) +(* ~ every point in `A` has a compact (and closed) neighborhood *) +(* *) +(* `finite_subset_cover D F A` *) +(* ~ the family of sets `F` is a cover of `A` for a finite number *) +(* of indices in `D` *) +(* *) +(* `cover_compact` *) +(* ~ set of compact sets w.r.t. the open cover-based definition *) +(* of compactness *) +(* *) +(* `open_fam_of A D f` *) +(* ~ the family of `f` indexed by `D` restricted to `A` is a *) +(* family of open sets *) +(* *) +(* `closed_fam_of A D f` *) +(* ~ the family of `f` indexed by `D` restricted to `A` is a *) +(* family of closed sets *) (******************************************************************************) Import Order.TTheory GRing.Theory Num.Theory. diff --git a/theories/topology_theory/connected.v b/theories/topology_theory/connected.v index 333150b1b3..bc3077eefd 100644 --- a/theories/topology_theory/connected.v +++ b/theories/topology_theory/connected.v @@ -7,12 +7,15 @@ From mathcomp Require Import topology_structure. (* # Connectedness *) (* This file provides connected and its related notions. *) (* *) -(* ``` *) -(* connected A <-> the only non empty subset of A which is *) -(* both open and closed in A is A *) -(* separated A B == the two sets A and B are separated *) -(* connected_component x == the connected component of point x *) -(* ``` *) +(* `connected A` *) +(* ~ the only non empty subset of `A` which is both open and *) +(* closed in `A` is `A` *) +(* *) +(* `separated A B` *) +(* ~ the two sets `A` and `B` are separated *) +(* *) +(* `connected_component x` *) +(* ~ the connected component of point `x` *) (******************************************************************************) Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) diff --git a/theories/topology_theory/discrete_topology.v b/theories/topology_theory/discrete_topology.v index 7b0b1167ee..3b788ea9da 100644 --- a/theories/topology_theory/discrete_topology.v +++ b/theories/topology_theory/discrete_topology.v @@ -6,24 +6,38 @@ From mathcomp Require Import order_topology pseudometric_structure compact. (**md**************************************************************************) (* # Discrete Topology *) -(* ``` *) -(* discreteNbhsType == neighborhoods are principal filters *) -(* discrete_ent == entourages of the discrete uniformity *) -(* topology, equipped with the Uniform *) -(* structure *) -(* discrete_ball == singleton balls for the discrete metric, *) -(* equipped with the Uniform structure *) -(* discreteTopologicalType == types with a discrete topology *) -(* discreteOrderTopologicalType == an order type with the discrete topology *) -(* pdiscreteTopologicalType == pointed type with the discrete topology *) -(* pdiscreteOrderTopologicalType == pointed, ordered, and discrete *) -(* discreteUniformType == a uniform space where the diagonal is an *) -(* entourage *) -(* discretePseudoMetricType == a pseudometric space where the only balls *) -(* are singletons *) -(* discrete_topology T == alias attaching discrete structures for *) -(* topology, uniformity, and pseudometric *) -(* ``` *) +(* `discreteNbhsType` *) +(* ~ neighborhoods are principal filters *) +(* *) +(* `discrete_ent` *) +(* ~ entourages of the discrete uniformity topology, equipped with *) +(* the `Uniform` structure *) +(* *) +(* `discrete_ball` *) +(* ~ singleton balls for the discrete metric, equipped with the *) +(* `Uniform` structure *) +(* *) +(* `discreteTopologicalType` *) +(* ~ types with a discrete topology *) +(* *) +(* `discreteOrderTopologicalType` *) +(* ~ an order type with the discrete topology *) +(* *) +(* `pdiscreteTopologicalType` *) +(* ~ pointed type with the discrete topology *) +(* *) +(* `pdiscreteOrderTopologicalType` *) +(* ~ pointed, ordered, and discrete *) +(* *) +(* `discreteUniformType` *) +(* ~ a uniform space where the diagonal is an entourage *) +(* *) +(* `discretePseudoMetricType` *) +(* ~ a pseudometric space where the only balls are singletons *) +(* *) +(* `discrete_topology T` *) +(* ~ alias attaching discrete structures for topology, uniformity, *) +(* and pseudometric *) (******************************************************************************) Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) diff --git a/theories/topology_theory/function_spaces.v b/theories/topology_theory/function_spaces.v index 84a4634400..11685f9f6d 100644 --- a/theories/topology_theory/function_spaces.v +++ b/theories/topology_theory/function_spaces.v @@ -50,43 +50,69 @@ From mathcomp Require Import product_topology. (* - Cartesian closedness for the category of locally compact topologies *) (* *) (* ## Function space notations *) -(* ``` *) -(* {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 *) -(* {uniform U -> V} := {uniform` [set: U] -> V} *) -(* {uniform A, F --> f} == F converges to f in {uniform A -> V} *) -(* {uniform, F --> f} := {uniform setT, F --> f} *) -(* prod_topology I T == the topology of pointwise convergence on the *) -(* dependent space `forall (i:I), T i` *) -(* arrow_uniform_type U V == the topology of uniform convergence on the *) -(* type `U -> V` *) -(* {ptws U -> V} == prod_topology for the non-dependent product *) -(* separate_points_from_closed f == for a closed set U and point x outside *) -(* some member of the family f, it sends f_i(x) *) -(* outside (closure (f_i @` U)) *) -(* Used together with join_product. *) -(* join_product f == the function (x => f ^~ x) *) -(* When the family f separates points from closed *) -(* sets, join_product is an embedding. *) -(* {ptws, F --> f} == F converges to f in {ptws U -> V} *) -(* {family fam, U -> V} == the supremum of {uniform A -> f} for each A in *) -(* `fam` *) -(* 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} *) -(* {compact_open, U -> V} == compact-open topology *) -(* {compact_open, F --> f} == F converges to f in {compact_open, U -> V} *) -(* eval == the evaluation map for continuous functions *) -(* ``` *) +(* ``{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` *) +(* *) +(* `{uniform U -> V}` *) +(* ~ ``{uniform` [set: U] -> V}`` *) +(* *) +(* `{uniform A, F --> f}` *) +(* ~ `F` converges to `f` in `{uniform A -> V}` *) +(* *) +(* `{uniform, F --> f}` *) +(* ~ `{uniform setT, F --> f}` *) +(* *) +(* `prod_topology I T` *) +(* ~ the topology of pointwise convergence on the dependent space *) +(* `forall (i:I), T i` *) +(* *) +(* `arrow_uniform_type U V` *) +(* ~ the topology of uniform convergence on the type `U -> V` *) +(* *) +(* `{ptws U -> V}` *) +(* ~ `prod_topology` for the non-dependent product *) +(* *) +(* `separate_points_from_closed f` *) +(* ~ for a closed set `U` and point `x` outside some member of the *) +(* family `f`, it sends `f_i(x)` outside ``(closure (f_i @` U))`` *) +(* Used together with `join_product`. *) +(* *) +(* `join_product f` *) +(* ~ the function `(x => f ^~ x)` *) +(* When the family `f` separates points from closed sets, *) +(* `join_product` is an embedding. *) +(* *) +(* `{ptws, F --> f}` *) +(* ~ `F` converges to `f` in `{ptws U -> V}` *) +(* *) +(* `{family fam, U -> V}` *) +(* ~ the supremum of `{uniform A -> f}` for each `A` in `fam` *) +(* 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}` *) +(* *) +(* `{compact_open, U -> V}` *) +(* ~ compact-open topology *) +(* *) +(* `{compact_open, F --> f}` *) +(* ~ `F` converges to `f` in `{compact_open, U -> V}` *) +(* *) +(* `eval` *) +(* ~ the evaluation map for continuous functions *) (* *) (* ## Ascoli's theorem notations *) -(* ``` *) -(* equicontinuous W x == the set (W : X -> Y) is equicontinuous at x *) -(* singletons T := [set [set x] | x in [set: T]] *) -(* pointwise_precompact W == for each (x : X), the set of images *) -(* [f x | f in W] is precompact *) -(* ``` *) +(* `equicontinuous W x` *) +(* ~ the set `(W : X -> Y)` is equicontinuous at `x` *) +(* *) +(* `singletons T` *) +(* ~ `[set [set x] | x in [set: T]]` *) +(* *) +(* `pointwise_precompact W` *) +(* ~ for each `(x : X)`, the set of images `[f x | f in W]` is *) +(* precompact *) (******************************************************************************) Reserved Notation "{ 'uniform`' A -> V }" diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index 943c1210cb..e992c01ee6 100644 --- a/theories/topology_theory/initial_topology.v +++ b/theories/topology_theory/initial_topology.v @@ -19,20 +19,16 @@ From mathcomp Require Import pseudometric_structure. (* way, we reserve "weak topology" for the topology induced on a topological *) (* vector space by its dual. *) (* *) -(* ``` *) -(* initial_topology f == initial topology by a function f : S -> T *) -(* on S *) -(* S must be a choiceType and T a *) -(* topologicalType. *) -(* sub_initial_topology V S U == sub-initial topology generated by the *) -(* \val : U -> V *) -(* U has type subChoiceType S with S : pred V. *) -(* This is a subTopologicalType when V is *) -(* endowed with a topology. *) -(* This is a subConvexTvsType when V is *) -(* endowed with a convexTvsType (and when U is *) -(* subLmodType). *) -(* ``` *) +(* `initial_topology f` *) +(* ~ initial topology by a function `f : S -> T` on `S`. `S` must be a *) +(* `choiceType` and `T` a `topologicalType` *) +(* *) +(* `sub_initial_topology V S U` *) +(* ~ sub-initial topology generated by the `\val : U -> V`. `U` *) +(* has type `subChoiceType S` with `S : pred V`. This is a *) +(* `subTopologicalType` when `V` is endowed with a topology. *) +(* This is a `subConvexTvsType` when `V` is endowed with a *) +(* `convexTvsType` (and when `U` is `subLmodType`) *) (* `initial_topology` is equipped with the structures of: *) (* - uniform space *) (* - pseudometric space (the metric space for initial topologies) *) diff --git a/theories/topology_theory/matrix_topology.v b/theories/topology_theory/matrix_topology.v index 5e6a91d835..b8e93edde4 100644 --- a/theories/topology_theory/matrix_topology.v +++ b/theories/topology_theory/matrix_topology.v @@ -6,11 +6,12 @@ From mathcomp Require Import uniform_structure pseudometric_structure. (**md**************************************************************************) (* # Matrix topology *) -(* ``` *) -(* @mx_ent m n T == entourages for the m x n matrices with *) -(* coefficients of type T *) -(* mx_ball A == balls for the matrix A *) -(* ``` *) +(* `@mx_ent m n T` *) +(* ~ entourages for the `m` x `n` matrices with coefficients of *) +(* type `T` *) +(* *) +(* `mx_ball A` *) +(* ~ balls for the matrix `A` *) (* Matrices `'M[T]_(m, n)` are endowed with the structures of: *) (* - topology *) (* - uniform space *) diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v index d9477e84cb..f795f9ae1b 100644 --- a/theories/topology_theory/metric_structure.v +++ b/theories/topology_theory/metric_structure.v @@ -13,13 +13,12 @@ From mathcomp Require Import num_topology product_topology separation_axioms. (**md**************************************************************************) (* # Metric spaces *) (* *) -(* ``` *) -(* metricType K == metric structure with distance mdist *) -(* The HB class is Metric. *) -(* R^o with R : numFieldType is shown to be a metric space. *) -(* The mixin PseudoMetric_isMetric extends PseudoMetric. *) -(* The factor isMetric just requires a distance. *) -(* ``` *) +(* `metricType K` *) +(* ~ metric structure with distance `mdist` The HB class is *) +(* `Metric`. `R^o` with `R : numFieldType` is shown to be a *) +(* metric space. The mixin `PseudoMetric_isMetric` extends *) +(* `PseudoMetric`. The factor `isMetric` just requires a *) +(* distance. *) (******************************************************************************) Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) diff --git a/theories/topology_theory/order_topology.v b/theories/topology_theory/order_topology.v index 314fe8952e..88c3442498 100644 --- a/theories/topology_theory/order_topology.v +++ b/theories/topology_theory/order_topology.v @@ -9,15 +9,26 @@ From mathcomp Require Import product_topology pseudometric_structure. (**md**************************************************************************) (* # Order topology *) (* *) -(* ``` *) -(* POrderedNbhs == join of Nbhs and isPOrder *) -(* POrderedTopological == join of Topological and isPOrder *) -(* POrderedUniform == join of Uniform and isPOrder *) -(* POrderedPseudoMetric == join of PseudoMetric and isPOrder *) -(* POrderedPointedTopological == join of PointedTopological and isPOrder *) -(* orderTopologicalType == a topology built from intervals *) -(* order_topology T == the induced order topology on T *) -(* ``` *) +(* `POrderedNbhs` *) +(* ~ join of `Nbhs` and `isPOrder` *) +(* *) +(* `POrderedTopological` *) +(* ~ join of `Topological` and `isPOrder` *) +(* *) +(* `POrderedUniform` *) +(* ~ join of `Uniform` and `isPOrder` *) +(* *) +(* `POrderedPseudoMetric` *) +(* ~ join of `PseudoMetric` and `isPOrder` *) +(* *) +(* `POrderedPointedTopological` *) +(* ~ join of `PointedTopological` and `isPOrder` *) +(* *) +(* `orderTopologicalType` *) +(* ~ a topology built from intervals *) +(* *) +(* `order_topology T` *) +(* ~ the induced order topology on `T` *) (******************************************************************************) Import Order.TTheory GRing.Theory Num.Theory. diff --git a/theories/topology_theory/pseudometric_structure.v b/theories/topology_theory/pseudometric_structure.v index ef04f0560f..a2dd93e4b8 100644 --- a/theories/topology_theory/pseudometric_structure.v +++ b/theories/topology_theory/pseudometric_structure.v @@ -13,34 +13,43 @@ From mathcomp Require Import uniform_structure. (* *) (* ## Mathematical structures *) (* ### PseudoMetrics *) -(* ``` *) -(* entourage_ ball == entourages defined using balls *) -(* pseudoMetricType == interface type for pseudo metric space *) -(* structure: a type equipped with balls *) -(* The HB class is PseudoMetric. *) -(* pseudoPMetricType == a pointed pseudoMetric space *) -(* ball x e == ball of center x and radius e *) -(* nbhs_ball_ ball == nbhs defined using the given balls *) -(* nbhs_ball == nbhs defined using balls in a *) -(* pseudometric space *) -(* ``` *) +(* `entourage_ ball` *) +(* ~ entourages defined using balls *) +(* *) +(* `pseudoMetricType` *) +(* ~ interface type for pseudo metric space structure: a type *) +(* equipped with balls The HB class is `PseudoMetric`. *) +(* *) +(* `pseudoPMetricType` *) +(* ~ a pointed `pseudoMetric` space *) +(* *) +(* `ball x e` *) +(* ~ ball of center `x` and radius `e` *) +(* *) +(* `nbhs_ball_ ball` *) +(* ~ `nbhs` defined using the given balls *) +(* *) +(* `nbhs_ball` *) +(* ~ `nbhs` defined using balls in a pseudometric space *) (* ### Factories *) -(* ``` *) -(* Nbhs_isPseudoMetric == factory to build a topological space *) -(* from a mixin for a pseudoMetric space *) -(* ``` *) +(* `Nbhs_isPseudoMetric` *) +(* ~ factory to build a topological space from a mixin for a *) +(* `pseudoMetric` space *) (* ### Complete Pseudometrics *) -(* ``` *) -(* ball_ N == balls defined by the norm/absolute *) -(* value N *) -(* completePseudoMetricType == interface type for a complete *) -(* pseudometric space structure *) -(* The HB class is CompletePseudoMetric. *) -(* cauchy_ex F <-> the set of sets F is a cauchy filter *) -(* (epsilon-delta definition) *) -(* cauchy_ball F <-> the set of sets F is a cauchy filter *) -(* (using the near notations) *) -(* ``` *) +(* `ball_ N` *) +(* ~ balls defined by the norm/absolute value `N` *) +(* *) +(* `completePseudoMetricType` *) +(* ~ interface type for a complete pseudometric space structure. The *) +(* HB class is `CompletePseudoMetric`. *) +(* *) +(* `cauchy_ex F` *) +(* ~ the set of sets `F` is a cauchy filter (epsilon-delta *) +(* definition) *) +(* *) +(* `cauchy_ball F` *) +(* ~ the set of sets `F` is a cauchy filter (using the near *) +(* notations) *) (******************************************************************************) Import Order.TTheory GRing.Theory Num.Theory. diff --git a/theories/topology_theory/quotient_topology.v b/theories/topology_theory/quotient_topology.v index 1a0ac8a22f..129f3336c7 100644 --- a/theories/topology_theory/quotient_topology.v +++ b/theories/topology_theory/quotient_topology.v @@ -6,11 +6,9 @@ From mathcomp Require Import topology_structure. (**md**************************************************************************) (* # quotient topology *) (* *) -(* ``` *) -(* quotient_topology Q == the quotient topology corresponding to *) -(* quotient Q : quotType T where T has type *) -(* topologicalType *) -(* ``` *) +(* `quotient_topology Q` *) +(* ~ the quotient topology corresponding to quotient `Q : quotType T` *) +(* where `T` has type `topologicalType` *) (******************************************************************************) Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) diff --git a/theories/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v index 3039e3ce96..375ba8cea5 100644 --- a/theories/topology_theory/separation_axioms.v +++ b/theories/topology_theory/separation_axioms.v @@ -19,38 +19,49 @@ From mathcomp Require Import connected supremum_topology sigT_topology. (* accessible, uniform, etc). This file also provides related topological *) (* properties like zero dimensional and perfect, and discrete. *) (* *) -(* ``` *) -(* set_nbhs A == filter from open sets containing A *) -(* ``` *) +(* `set_nbhs A` *) +(* ~ filter from open sets containing `A` *) (* *) (* ## The classic separation axioms *) -(* ``` *) -(* kolmogorov_space T == T is a Kolmogorov space (T0) *) -(* accessible_space T == T is an accessible space (T1) *) -(* hausdorff_space T == T is a Hausdorff space (T2) *) -(* close x y == x and y are arbitrarily close w.r.t. open sets *) -(* normal_space T == T is normal (sometimes called T4) *) -(* regular_space T == T is regular (sometimes called T3) *) -(* ``` *) +(* `kolmogorov_space T` *) +(* ~ `T` is a Kolmogorov space (T0) *) +(* *) +(* `accessible_space T` *) +(* ~ `T` is an accessible space (T1) *) +(* *) +(* `hausdorff_space T` *) +(* ~ `T` is a Hausdorff space (T2) *) +(* *) +(* `close x y` *) +(* ~ `x` and `y` are arbitrarily close w.r.t. open sets *) +(* *) +(* `normal_space T` *) +(* ~ `T` is normal (sometimes called T4) *) +(* *) +(* `regular_space T` *) +(* ~ `T` is regular (sometimes called T3) *) (* ## related concepts *) -(* ``` *) -(* totally_disconnected A == the only connected subsets of A are *) -(* empty or singletons *) -(* zero_dimensional T == points are separable by a clopen set *) -(* perfect_set A == A is closed, and every point in A is *) -(* a limit point of A *) -(* ``` *) +(* `totally_disconnected A` *) +(* ~ the only connected subsets of `A` are empty or singletons *) +(* *) +(* `zero_dimensional T` *) +(* ~ points are separable by a clopen set *) +(* *) +(* `perfect_set A` *) +(* ~ `A` is closed, and every point in `A` is a limit point of `A` *) (* ## metrizability for uniform spaces *) -(* ``` *) -(* countable_uniform.type == endows a pseudoMetric on a uniform type whose *) -(* entourage has a countable basis *) -(* sup_pseudometric == the pseudometric induced for the supremum *) -(* of countably many pseudoMetrics *) -(* gauge E == for an entourage E, gauge E is a filter which *) -(* includes `iter n split_ent E`. *) -(* Critically, `gauge E` forms a uniform space *) -(* with a countable uniformity. *) -(* ``` *) +(* `countable_uniform.type` *) +(* ~ endows a pseudoMetric on a uniform type whose entourage has a *) +(* countable basis *) +(* *) +(* `sup_pseudometric` *) +(* ~ the pseudometric induced for the supremum of countably many *) +(* pseudoMetrics *) +(* *) +(* `gauge E` *) +(* ~ for an entourage `E`, `gauge E` is a filter which includes *) +(* `iter n split_ent E`. Critically, `gauge E` forms a uniform *) +(* space with a countable uniformity. *) (******************************************************************************) Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) diff --git a/theories/topology_theory/sigT_topology.v b/theories/topology_theory/sigT_topology.v index 049bbcbb31..8bc69d36b3 100644 --- a/theories/topology_theory/sigT_topology.v +++ b/theories/topology_theory/sigT_topology.v @@ -9,10 +9,9 @@ From mathcomp Require Import topology_structure compact subspace_topology. (* # sigT topology *) (* This file equips the type {i & X i} with its standard topology *) (* *) -(* ``` *) -(* sigT_nbhs x == the neighborhoods of the standard topology on the *) -(* type {i & X i} *) -(* ``` *) +(* `sigT_nbhs x` *) +(* ~ the neighborhoods of the standard topology on the type *) +(* `{i & X i}` *) (******************************************************************************) Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v index 10bd0a0b6a..3817964af4 100644 --- a/theories/topology_theory/subspace_topology.v +++ b/theories/topology_theory/subspace_topology.v @@ -8,26 +8,36 @@ From mathcomp Require Import product_topology. (**md**************************************************************************) (* # 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 *) -(* nbhs_subspace x == filter associated with x : subspace A *) -(* from_subspace A f == function of type `subspace A -> U` given a *) -(* function f of type `A -> U` *) -(* The purpose of this definition is to *) -(* preserve the pretty-printing of the notation *) -(* {within _, continuous _} below. Its use is *) -(* however likely to be later superseded by a *) -(* better (compositional) mechanism. *) -(* {within A, continuous f} := continuous (from_subspace A f)) *) -(* subspace_ent A == subspace entourages *) -(* subspace_ball A == balls of the pseudometric subspace structure *) -(* continuousSubspaceType A B == type of continuous functions from set A to *) -(* set B with domain subspace A *) -(* The HB structure is ContinuousFun. *) -(* ``` *) +(* `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` *) +(* *) +(* `nbhs_subspace x` *) +(* ~ filter associated with `x : subspace A` *) +(* *) +(* `from_subspace A f` *) +(* ~ function of type `subspace A -> U` given a function `f` of type *) +(* `A -> U`. The purpose of this definition is to preserve the *) +(* pretty-printing of the notation `{within _, continuous _}` *) +(* below. Its use is however likely to be later superseded by a *) +(* better (compositional) mechanism. *) +(* *) +(* `{within A, continuous f}` *) +(* ~ `continuous (from_subspace A f))` *) +(* *) +(* `subspace_ent A` *) +(* ~ subspace entourages *) +(* *) +(* `subspace_ball A` *) +(* ~ balls of the pseudometric subspace structure *) +(* *) +(* `continuousSubspaceType A B` *) +(* ~ type of continuous functions from set `A` to set `B` with *) +(* domain `subspace A`. The HB structure is `ContinuousFun`. *) (******************************************************************************) Reserved Notation "{ 'within' A , 'continuous' f }" diff --git a/theories/topology_theory/subtype_topology.v b/theories/topology_theory/subtype_topology.v index e5a025e01b..6ccf16845d 100644 --- a/theories/topology_theory/subtype_topology.v +++ b/theories/topology_theory/subtype_topology.v @@ -20,10 +20,11 @@ From mathcomp Require Import product_topology subspace_topology. (* Note the implicit coercion from sets to `set_val` from `classical_sets.v`. *) (* *) (* This file provides `set_type` with a topology, and some theory. *) -(* ``` *) -(* sigT_of_setX == commutes `set_type` and product topologies *) -(* setX_of_sigT == commutes product and `set_type` topologies *) -(* ``` *) +(* `sigT_of_setX` *) +(* ~ commutes `set_type` and product topologies *) +(* *) +(* `setX_of_sigT` *) +(* ~ commutes product and `set_type` topologies *) (* *) (******************************************************************************) diff --git a/theories/topology_theory/supremum_topology.v b/theories/topology_theory/supremum_topology.v index c4a963df4b..28359365f1 100644 --- a/theories/topology_theory/supremum_topology.v +++ b/theories/topology_theory/supremum_topology.v @@ -6,11 +6,12 @@ From mathcomp Require Import topology_structure uniform_structure. (**md**************************************************************************) (* # Supremum topology *) (* *) -(* ``` *) -(* sup_topology Tc == supremum topology of the family of *) -(* topologicalType structures Tc on T *) -(* sup_ent E == the entourages of the supremum *) -(* ``` *) +(* `sup_topology Tc` *) +(* ~ supremum topology of the family of `topologicalType` *) +(* structures `Tc` on `T` *) +(* *) +(* `sup_ent E` *) +(* ~ the entourages of the supremum *) (* `sup_topology` is equipped with the `Uniform` structure *) (******************************************************************************) diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index d397a26796..7c858c5947 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -12,71 +12,102 @@ From mathcomp Require Export filter. (* *) (* ## Mathematical structures *) (* ### Topology *) -(* ``` *) -(* topologicalType == interface type for topological space *) -(* structure *) -(* the HB class is Topological. *) -(* subTopologicalType S == join of SubNbhs and Topological where S has *) -(* pred V with V a topologicalType *) -(* the HB class is SubTopological. *) -(* ptopologicalType == a pointed topologicalType *) -(* open == set of open sets *) -(* closed == set of closed sets *) -(* clopen U == U is both open and closed *) -(* open_nbhs p == set of open neighbourhoods of p *) -(* basis B == a family of open sets that converges to *) -(* each point *) -(* second_countable T == T has a countable basis *) -(* [locally P] := forall a, A a -> G (within A (nbhs x)) if P *) -(* is convertible to G (globally A) *) -(* U° == all of the points which are locally in U, *) -(* i.e., the largest open set contained in U *) -(* This is a notation for `interior U`. *) -(* closure U == the smallest closed set containing U *) -(* regopen U == U is regular open, *) -(* i.e., equal to the interior of its closure *) -(* regclosed U == U is regular closed, *) -(* i.e., equal to the closure of its interior *) -(* open_of_nbhs B == the open sets induced by neighborhoods *) -(* nbhs_of_open B == the neighborhoods induced by open sets *) -(* x^' == set of neighbourhoods of x where x is *) -(* excluded (a "deleted neighborhood") *) -(* limit_point E == the set of limit points of E *) -(* isolated A == the set of isolated points of A *) -(* dense S == the set (S : set T) is dense in T, with T of *) -(* type topologicalType *) -(* continuousType == type of continuous functions *) -(* The HB structures is Continuous. *) -(* mkcts f_cts == object of type continuousType corresponding to *) -(* the function f (f_cts : continuous f) *) +(* `topologicalType` *) +(* ~ interface type for topological space structure. the HB class *) +(* is `Topological` *) (* *) -(* ``` *) +(* `subTopologicalType S` *) +(* ~ join of `SubNbhs` and `Topological` where `S` has pred `V` *) +(* with `V` a `topologicalType`. the HB class is `SubTopological` *) +(* *) +(* `ptopologicalType` *) +(* ~ a pointed `topologicalType` *) +(* *) +(* `open` *) +(* ~ set of open sets *) +(* *) +(* `closed` *) +(* ~ set of closed sets *) +(* *) +(* `clopen U` *) +(* ~ `U` is both open and closed *) +(* *) +(* `open_nbhs p` *) +(* ~ set of open neighbourhoods of `p` *) +(* *) +(* `basis B` *) +(* ~ a family of open sets that converges to each point *) +(* *) +(* `second_countable T` *) +(* ~ `T` has a countable basis *) +(* *) +(* `[locally P]` *) +(* ~ `forall a, A a -> G (within A (nbhs x))` if `P` is convertible *) +(* to `G (globally A)` *) +(* *) +(* `U°` *) +(* ~ all of the points which are locally in `U`, i.e., the largest *) +(* open set contained in `U`. This is a notation for `interior U` *) +(* *) +(* `closure U` *) +(* ~ the smallest closed set containing `U` *) +(* *) +(* `regopen U` *) +(* ~ `U` is regular open, i.e., equal to the interior of its *) +(* closure *) +(* *) +(* `regclosed U` *) +(* ~ `U` is regular closed, i.e., equal to the closure of its *) +(* interior *) +(* *) +(* `open_of_nbhs B` *) +(* ~ the open sets induced by neighborhoods *) +(* *) +(* `nbhs_of_open B` *) +(* ~ the neighborhoods induced by open sets *) +(* *) +(* `x^'` *) +(* ~ set of neighbourhoods of `x` where `x` is excluded (a *) +(* "deleted neighborhood") *) +(* *) +(* `limit_point E` *) +(* ~ the set of limit points of `E` *) +(* *) +(* `isolated A` *) +(* ~ the set of isolated points of `A` *) +(* *) +(* `dense S` *) +(* ~ the set `(S : set T)` is dense in `T`, with `T` of type *) +(* `topologicalType` *) +(* *) +(* `continuousType` *) +(* ~ type of continuous functions. The HB structures is *) +(* `Continuous` *) +(* *) +(* `mkcts f_cts` *) +(* ~ object of type `continuousType` corresponding to the function *) +(* `f` (`f_cts : continuous f`) *) (* ### Factories *) -(* ``` *) -(* Nbhs_isNbhsTopological == factory for a topology defined by a *) -(* filter *) -(* It builds the mixin for a topological *) -(* space from the properties of nbhs and *) -(* hence assumes that the carrier is a *) -(* filterType. *) -(* isOpenTopological == factory for a topology defined by open *) -(* sets *) -(* It builds the mixin for a topological *) -(* space from the properties of open *) -(* sets, nbhs_of_open must be used to *) -(* declare a filterType. *) -(* isBaseTopological == factory for a topology defined by a *) -(* base of open sets *) -(* It builds the mixin for a topological *) -(* space from the properties of a base of *) -(* open sets; the type of indices must be *) -(* a pointedType *) -(* isSubBaseTopological == factory for a topology defined by a *) -(* subbase of open sets *) -(* It builds the mixin for a topological *) -(* space from a subbase of open sets b *) -(* indexed on domain D *) -(* ``` *) +(* `Nbhs_isNbhsTopological` *) +(* ~ factory for a topology defined by a filter. It builds the *) +(* mixin for a topological space from the properties of `nbhs` *) +(* and hence assumes that the carrier is a `filterType` *) +(* *) +(* `isOpenTopological` *) +(* ~ factory for a topology defined by open sets. It builds the *) +(* mixin for a topological space from the properties of open *) +(* sets, `nbhs_of_open` must be used to declare a `filterType` *) +(* *) +(* `isBaseTopological` *) +(* ~ factory for a topology defined by a base of open sets. It *) +(* builds the mixin for a topological space from the properties *) +(* of a base of open sets; the type of indices must be a *) +(* `pointedType` *) +(* *) +(* `isSubBaseTopological` *) +(* ~ factory for a topology defined by a subbase of open sets. It *) +(* builds the mixin for a topological space from a subbase of *) +(* open sets `b` indexed on domain `D` *) (* *) (******************************************************************************) diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v index f8ec6cb9ae..e48f52623e 100644 --- a/theories/topology_theory/uniform_structure.v +++ b/theories/topology_theory/uniform_structure.v @@ -10,36 +10,46 @@ From mathcomp Require Import topology_structure. (* *) (* ## Mathematical structures *) (* ### Uniform *) -(* ``` *) -(* nbhs_ ent == neighborhoods defined using entourages *) -(* uniformType == interface type for uniform spaces: a *) -(* type equipped with entourages *) -(* The HB class is Uniform. *) -(* puniformType == a pointed and uniform space *) -(* entourage == set of entourages in a uniform space *) -(* split_ent E == when E is an entourage, split_ent E is *) -(* an entourage E' such that E' \o E' is *) -(* included in E when seen as a relation *) -(* countable_uniformity T == T's entourage has a countable base *) -(* This is equivalent to `T` being *) -(* metrizable. *) -(* unif_continuous f == f is uniformly continuous *) -(* entourage_ ball == entourages defined using balls *) -(* ``` *) -(* ## Factories *) -(* ``` *) -(* Nbhs_isUniform == factory to build a topological space *) -(* from a mixin for a uniform space *) +(* `nbhs_ ent` *) +(* ~ neighborhoods defined using entourages *) +(* *) +(* `uniformType` *) +(* ~ interface type for uniform spaces: a type equipped with *) +(* entourages *) +(* ~ the HB class is `Uniform` *) +(* *) +(* `puniformType` *) +(* ~ a pointed and uniform space *) +(* *) +(* `entourage` *) +(* ~ set of entourages in a uniform space *) +(* *) +(* `split_ent E` *) +(* ~ when `E` is an entourage, `split_ent E` is an entourage `E'` *) +(* such that `E' \o E'` is included in `E` when seen as a *) +(* relation *) (* *) -(* ``` *) +(* `countable_uniformity T` *) +(* ~ `T`'s entourage has a countable base *) +(* ~ this is equivalent to `T` being metrizable *) +(* *) +(* `unif_continuous f` *) +(* ~ `f` is uniformly continuous *) +(* *) +(* `entourage_ ball` *) +(* ~ entourages defined using balls *) +(* ## Factories *) +(* `Nbhs_isUniform` *) +(* ~ factory to build a topological space from a mixin for a *) +(* uniform space *) (* ### Complete uniform spaces *) -(* ``` *) -(* cauchy F <-> the set of sets F is a cauchy filter *) -(* (entourage definition) *) -(* completeType == interface type for a complete uniform *) -(* space structure *) -(* The HB class is Complete. *) -(* ``` *) +(* `cauchy F` *) +(* ~ the set of sets `F` is a cauchy filter (entourage *) +(* definition) *) +(* *) +(* `completeType` *) +(* ~ interface type for a complete uniform space structure *) +(* ~ the HB class is `Complete` *) (******************************************************************************) Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) diff --git a/theories/trigo.v b/theories/trigo.v index 8d65b797b9..1593fd58de 100644 --- a/theories/trigo.v +++ b/theories/trigo.v @@ -15,21 +15,44 @@ From mathcomp Require Import measure lebesgue_measure lebesgue_integral ftc. (* 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 *) -(* sin x == the sine function, i.e., lim (series (sin_coeff x)) *) -(* sin_coeff' x == the sequence of odd coefficients of sin x *) -(* cos_coeff x == the sequence of coefficients of cos x *) -(* cos x == the cosine function, i.e., lim (series (cos_coeff x)) *) -(* cos_coeff' x == the sequence of even coefficients of cos x *) -(* pi == pi *) -(* tan x == the tangent function *) -(* acos x == the arccos function *) -(* asin x == the arcsin function *) -(* atan x == the arctangent function *) -(* ``` *) +(* `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` *) +(* *) +(* `sin x` *) +(* ~ the sine function, i.e., `lim (series (sin_coeff x))` *) +(* *) +(* `sin_coeff' x` *) +(* ~ the sequence of odd coefficients of `sin x` *) +(* *) +(* `cos_coeff x` *) +(* ~ the sequence of coefficients of `cos x` *) +(* *) +(* `cos x` *) +(* ~ the cosine function, i.e., `lim (series (cos_coeff x))` *) +(* *) +(* `cos_coeff' x` *) +(* ~ the sequence of even coefficients of `cos x` *) +(* *) +(* `pi` *) +(* ~ `pi` *) +(* *) +(* `tan x` *) +(* ~ the tangent function *) +(* *) +(* `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 *)