Hb queue

CHANGELOG_UNRELEASED.md

@@ -33,6 +33,21 @@
     `wlength_sigma_sub_additive`, `wlength_sigma_finite`
   + measure instance of `hlength`
   + definition `lebesgue_stieltjes_measure`
+- in `mathcomp_extra.v`
+  + lemmas `ge0_ler_normr`, `gt0_ler_normr`, `le0_ger_normr` and `lt0_ger_normr`
+
+- in `probability.v`:
+  + definition `mmt_gen_fun`, `chernoff`
+
+- in `lebesgue_integral.v`:
+  + `mfun` instances for `expR` and `comp`
+
+- in `charge.v`:
+  + lemmas `dominates_cscale`, `Radon_Nikodym_cscale`
+  + definition `cadd`, lemmas `dominates_caddl`, `Radon_Nikodym_cadd`
+
+- in `lebesgue_integral.v`:
+  + lemma `abse_integralP`
 
 ### Changed
 
@@ -60,7 +75,21 @@
   + notations `_.-ocitv`, `_.-ocitv.-measurable`
   + definitions `ocitv`, `ocitv_display`
   + lemmas `is_ocitv`, `ocitv0`, `ocitvP`, `ocitvD`, `ocitvI`
+
+- in `probability.v`:
+  + `markov` now uses `Num.nneg`
+- in `lebesgue_integral.v`:
+  + order of arguments in the lemma `le_abse_integral`
+
+- in `lebesgue_measure.v`:
+  + remove one argument of `lebesgue_regularity_inner_sup`
+
+- in `normedtype.v`:
+  + order of arguments of `squeeze_cvgr`
 
+- moved from `derive.v` to `normedtype.v`:
+  + lemmas `cvg_at_rightE`, `cvg_at_leftE`
+
 ### Renamed
 
 - in `charge.v`
@@ -69,17 +98,69 @@
 - in `ereal.v`:
   + `le_er_map` -> `le_er_map_in`
 
+- in `sequences.v`:
+  + `lim_sup` -> `limn_sup`
+  + `lim_inf` -> `limn_inf`
+  + `lim_infN` -> `limn_infN`
+  + `lim_supE` -> `limn_supE`
+  + `lim_infE` -> `limn_infE`
+  + `lim_inf_le_lim_sup` -> `limn_inf_sup`
+  + `cvg_lim_inf_sup` -> `cvg_limn_inf_sup`
+  + `cvg_lim_supE` -> `cvg_limn_supE`
+  + `le_lim_supD` -> `le_limn_supD`
+  + `le_lim_infD` -> `le_limn_infD`
+  + `lim_supD` -> `limn_supD`
+  + `lim_infD` -> `limn_infD`
+  + `LimSup.lim_esup` -> `limn_esup`
+  + `LimSup.lim_einf` -> `limn_einf`
+  + `lim_einf_shift` -> `limn_einf_shift`
+  + `lim_esup_le_cvg` -> `limn_esup_le_cvg`
+  + `lim_einfN` -> `limn_einfN`
+  + `lim_esupN` -> `limn_esupN`
+  + `lim_einf_sup` -> `limn_einf_sup`
+  + `cvgNy_lim_einf_sup` -> `cvgNy_limn_einf_sup`
+  + `cvg_lim_einf_sup` -> `cvg_limn_einf_sup`
+  + `is_cvg_lim_einfE` -> `is_cvg_limn_einfE`
+  + `is_cvg_lim_esupE` -> `is_cvg_limn_esupE`
+
+- in `lebesgue_measure.v`:
+  + `measurable_fun_lim_sup` -> `measurable_fun_limn_sup`
+  + `measurable_fun_lim_esup` -> `measurable_fun_limn_esup`
+
 ### Generalized
 
 - in `topology.v`:
   + `ball_filter` generalized to `realDomainType`
 
+- in `lebesgue_integral.v`:
+  + weaken an hypothesis of `integral_ae_eq`
+
 ### Deprecated
 
 ### Removed
 
 - `lebesgue_measure_unique` (generalized to `lebesgue_stieltjes_measure_unique`)
 
+- in `sequences.v`:
+  + notations `elim_sup`, `elim_inf`
+  + `LimSup.lim_esup`, `LimSup.lim_einf`
+  + `elim_inf_shift`
+  + `elim_sup_le_cvg`
+  + `elim_infN`
+  + `elim_supN`
+  + `elim_inf_sup`
+  + `cvg_ninfty_elim_inf_sup`
+  + `cvg_ninfty_einfs`
+  + `cvg_ninfty_esups`
+  + `cvg_pinfty_einfs`
+  + `cvg_pinfty_esups`
+  + `cvg_elim_inf_sup`
+  + `is_cvg_elim_infE`
+  + `is_cvg_elim_supE`
+
+- in `lebesgue_measure.v`:
+  + `measurable_fun_elim_sup`
+
 ### Infrastructure
 
 ### Misc

CONTRIBUTING.md

@@ -44,6 +44,24 @@ Landau notations can be written in four shapes:
 
 The outcome is an expression with the normal Leibniz equality `=` and term `'o_F` which is not parsable. See [this paper](https://doi.org/10.6092/issn.1972-5787/8124) for more explanation and the header of the file [landau.v](https://github.com/math-comp/analysis/blob/master/theories/landau.v).
 
+## Deprecation
+
+Deprecations are introduced for breaking changes. For a simple renaming, the pattern is:
+```
+#[deprecated(since="analysis X.Y.Z", note="Use new_definition instead.")]
+Notation old_definition := new_definition (only parsing).
+```
+Note that this needs to be at the top-level (i.e., not inside a section).
+
+When a lemma `lem` is scheduled for deletion, it ought better be renamed `__deprecated__lem`
+(so that it can be blacklisted). The deprecation command then becomes:
+```
+#[deprecated(since="analysis X.Y.Z", note="Use another_lemma instead.")]
+Notation lem := __deprecated__lem (only parsing).
+```
+The `(only parsing)` format is needed so that Coq does not print back the deprecated name
+(for example when displaying error messages, that would be confusing).
+
 ## Naming convention
 
 ### homo and mono notations

classical/cardinality.v

@@ -903,7 +903,7 @@ Lemma __deprecated__bigcup_fset_set T (I : choiceType) (A : set I) (F : I -> set
   finite_set A -> \bigcup_(i in A) F i = \big[setU/set0]_(i <- fset_set A) F i.
 Proof. by move=> /bigsetU_fset_set->. Qed.
 #[deprecated(note="Use -bigsetU_fset_set instead")]
-Notation bigcup_fset_set := __deprecated__bigcup_fset_set.
+Notation bigcup_fset_set := __deprecated__bigcup_fset_set (only parsing).
 
 Lemma bigsetU_fset_set_cond T (I : choiceType) (A : set I) (F : I -> set T)
     (P : pred I) : finite_set A ->
@@ -917,7 +917,7 @@ Lemma __deprecated__bigcup_fset_set_cond T (I : choiceType) (A : set I) (F : I -
   \bigcup_(i in A `&` P) F i = \big[setU/set0]_(i <- fset_set A | P i) F i.
 Proof. by move=> /bigsetU_fset_set_cond->. Qed.
 #[deprecated(note="Use -bigsetU_fset_set_cond instead")]
-Notation bigcup_fset_set_cond := __deprecated__bigcup_fset_set_cond.
+Notation bigcup_fset_set_cond := __deprecated__bigcup_fset_set_cond (only parsing).
 
 Lemma bigsetI_fset_set T (I : choiceType) (A : set I) (F : I -> set T) :
   finite_set A -> \big[setI/setT]_(i <- fset_set A) F i =\bigcap_(i in A) F i.
@@ -929,7 +929,7 @@ Lemma __deprecated__bigcap_fset_set T (I : choiceType) (A : set I) (F : I -> set
   finite_set A -> \bigcap_(i in A) F i = \big[setI/setT]_(i <- fset_set A) F i.
 Proof. by move=> /bigsetI_fset_set->. Qed.
 #[deprecated(note="Use -bigsetI_fset_set instead")]
-Notation bigcap_fset_set := __deprecated__bigcap_fset_set.
+Notation bigcap_fset_set := __deprecated__bigcap_fset_set (only parsing).
 
 Lemma bigsetI_fset_set_cond T (I : choiceType) (A : set I) (F : I -> set T)
     (P : pred I) : finite_set A ->
@@ -1058,7 +1058,7 @@ by under eq_imagel do rewrite /= gE ?inE//; rewrite image_eq.
 Qed.
 
 #[deprecated(note="use countable0 instead")]
-Notation countable_set0 := countable0.
+Notation countable_set0 := countable0 (only parsing).
 
 Lemma countable1 T (x : T) : countable [set x].
 Proof. exact: finite_set_countable. Qed.

classical/classical_sets.v

@@ -467,7 +467,7 @@ apply: contra_notP => /forallNP h.
 by apply/eqP; rewrite predeqE => t; split => // _; apply: contrapT.
 Qed.
 #[deprecated(note="Use setTPn instead")]
-Notation setTP := setTPn.
+Notation setTP := setTPn (only parsing).
 
 Lemma in_set0 (x : T) : (x \in set0) = false. Proof. by rewrite memNset. Qed.
 Lemma in_setT (x : T) : x \in setT. Proof. by rewrite mem_set. Qed.
@@ -1034,9 +1034,9 @@ End basic_lemmas.
 #[global]
 Hint Resolve subsetUl subsetUr subIsetl subIsetr subDsetl subDsetr : core.
 #[deprecated(since="mathcomp-analysis 0.6", note="Use setICl instead.")]
-Notation setvI := setICl.
+Notation setvI := setICl (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6", note="Use setICr instead.")]
-Notation setIv := setICr.
+Notation setIv := setICr (only parsing).
 Arguments setU_id2r {T} C {A B}.
 
 Section set_order.
@@ -1980,13 +1980,13 @@ Proof. by apply: setC_inj; rewrite setC_bigcap setC_bigsetI bigcup_seq. Qed.
 
 End bigcup_seq.
 #[deprecated(since="mathcomp-analysis 0.6.4",note="Use bigcup_seq instead")]
-Notation bigcup_set := bigcup_seq.
+Notation bigcup_set := bigcup_seq (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6.4",note="Use bigcup_seq_cond instead")]
-Notation bigcup_set_cond := bigcup_seq_cond.
+Notation bigcup_set_cond := bigcup_seq_cond (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6.4",note="Use bigcap_seq instead")]
-Notation bigcap_set := bigcap_seq.
+Notation bigcap_set := bigcap_seq (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6.4",note="Use bigcap_seq_cond instead")]
-Notation bigcap_set_cond := bigcap_seq_cond.
+Notation bigcap_set_cond := bigcap_seq_cond (only parsing).
 
 Lemma bigcup_pred [T : finType] [U : Type] (P : {pred T}) (f : T -> set U) :
   \bigcup_(t in [set` P]) f t = \big[setU/set0]_(t in P) f t.
@@ -2528,7 +2528,7 @@ Qed.
 End partitions.
 
 #[deprecated(note="Use trivIset_setIl instead")]
-Notation trivIset_setI := trivIset_setIl.
+Notation trivIset_setI := trivIset_setIl (only parsing).
 
 Definition total_on T (A : set T) (R : T -> T -> Prop) :=
   forall s t, A s -> A t -> R s t \/ R t s.

classical/fsbigop.v

@@ -276,7 +276,7 @@ Proof. by move=> Afin; apply: __deprecated__full_fsbigID; apply: finite_setIl. Q
 Arguments fsbigID {R idx op I} B.
 
 #[deprecated(note="Use fsbigID instead")]
-Notation full_fsbigID := __deprecated__full_fsbigID.
+Notation full_fsbigID := __deprecated__full_fsbigID (only parsing).
 
 Lemma fsbigU (R : Type) (idx : R) (op : Monoid.com_law idx)
     (I : choiceType) (A B : set I) (F : I -> R) :
@@ -425,9 +425,9 @@ Arguments fsbig_image {R idx op I J} _ _.
 Arguments __deprecated__reindex_inside {R idx op I J} _ _.
 Arguments reindex_fsbigT {R idx op I J} _ _.
 #[deprecated(note="use reindex_fsbig, fsbig_image or reindex_fsbigT instead")]
-Notation reindex_inside := __deprecated__reindex_inside.
+Notation reindex_inside := __deprecated__reindex_inside (only parsing).
 #[deprecated(note="use reindex_fsbigT instead")]
-Notation reindex_inside_setT := reindex_fsbigT.
+Notation reindex_inside_setT := reindex_fsbigT (only parsing).
 
 Lemma fsbigN1 (R : eqType) (idx : R) (op : Monoid.com_law idx)
     (T1 T2 : choiceType) (Q : set T2) (f : T1 -> T2 -> R) (x : T1) :

classical/mathcomp_extra.v

@@ -895,3 +895,31 @@ Arguments le_bigmax_seq {d T} x {I r} i0 P.
 (* NB: PR 1079 to MathComp in progress *)
 Lemma gerBl {R : numDomainType} (x y : R) : 0 <= y -> x - y <= x.
 Proof. by move=> y0; rewrite lerBlDl lerDr. Qed.
+
+(* the following appears in MathComp 2.1.0 and MathComp 1.18.0 *)
+Section normr.
+Variable R : realDomainType.
+
+Definition Rnpos : qualifier 0 R := [qualify x : R | x <= 0].
+Lemma nposrE x : (x \is Rnpos) = (x <= 0). Proof. by []. Qed.
+
+Lemma ger0_le_norm :
+  {in Num.nneg &, {mono (@Num.Def.normr _ R) : x y / x <= y}}.
+Proof. by move=> x y; rewrite !nnegrE => x0 y0; rewrite !ger0_norm. Qed.
+
+Lemma gtr0_le_norm :
+  {in Num.pos &, {mono (@Num.Def.normr _ R) : x y / x <= y}}.
+Proof. by move=> x y; rewrite !posrE => /ltW x0 /ltW y0; exact: ger0_le_norm. Qed.
+
+Lemma ler0_ge_norm :
+  {in Rnpos &, {mono (@Num.Def.normr _ R) : x y / x <= y >-> x >= y}}.
+Proof.
+move=> x y; rewrite !nposrE => x0 y0.
+by rewrite !ler0_norm// -subr_ge0 opprK addrC subr_ge0.
+Qed.
+
+Lemma ltr0_ge_norm :
+  {in Num.neg &, {mono (@Num.Def.normr _ R) : x y / x <= y >-> x >= y}}.
+Proof. by move=> x y; rewrite !negrE => /ltW x0 /ltW y0; exact: ler0_ge_norm. Qed.
+
+End normr.

coq-mathcomp-analysis.opam

@@ -29,6 +29,11 @@ tags: [
   "keyword:analysis"
   "keyword:topology"
   "keyword:real numbers"
+  "keyword:differentiation"
+  "keyword:derivative"
+  "keyword:measure theory"
+  "keyword:integration"
+  "keyword:Lebesgue"
   "logpath:mathcomp.analysis"
 ]
 authors: [

coq-mathcomp-classical.opam

@@ -31,6 +31,9 @@ tags: [
   "keyword:classical"
   "keyword:logic"
   "keyword:sets"
+  "keyword:set theory"
+  "keyword:functions"
+  "keyword:cardinal"
   "logpath:mathcomp.classical"
 ]
 authors: [