Changelog067 (#1143) (#1145)

* changelog for version 0.6.7

* upd README

CHANGELOG.md

@@ -1,6 +1,196 @@
 # Changelog
 
-Latest releases: [[0.6.6] - 2023-11-14](#066---2023-11-14) and [[0.6.5] - 2023-10-02](#065---2023-10-02)
+Latest releases: [[0.6.7] - 2024-01-09](#067---2024-01-09) and [[0.6.6] - 2023-11-14](#066---2023-11-14)
+
+## [0.6.7] - 2024-01-09
+
+### Added
+
+- in `boolp.v`:
+  + tactic `eqProp`
+  + variant `BoolProp`
+  + lemmas `PropB`, `notB`, `andB`, `orB`, `implyB`, `decide_or`, `not_andE`,
+    `not_orE`, `orCA`, `orAC`, `orACA`, `orNp`, `orpN`, `or3E`, `or4E`, `andCA`,
+	 `andAC`, `andACA`, `and3E`, `and4E`, `and5E`, `implyNp`, `implypN`,
+	 `implyNN`, `or_andr`, `or_andl`, `and_orr`, `and_orl`, `exists2E`,
+	 `inhabitedE`, `inhabited_witness`
+
+- in `topology.v`,
+  + new lemmas `perfect_set2`, and `ent_closure`.
+  + lemma `clopen_surj`
+  + lemma `nbhs_dnbhs_neq`
+  + lemma `dnbhs_ball`
+
+- in `constructive_ereal.v`
+  + lemma `lee_subgt0Pr`
+
+- in `ereal.v`:
+  + lemmas `ereal_sup_le`, `ereal_inf_le`
+
+- in `normedtype.v`:
+  + hints for `at_right_proper_filter` and `at_left_proper_filter`
+  + definition `lower_semicontinuous`
+  + lemma `lower_semicontinuousP`
+  + lemma `not_near_at_rightP`
+  + lemmas `withinN`, `at_rightN`, `at_leftN`, `cvg_at_leftNP`, `cvg_at_rightNP`
+  + lemma `dnbhsN`
+  + lemma `limf_esup_dnbhsN`
+  + definitions `limf_esup`, `limf_einf`
+  + lemmas `limf_esupE`, `limf_einfE`, `limf_esupN`, `limf_einfN`
+
+- in `sequences.v`:
+  + lemma `minr_cvg_0_cvg_0`
+  + lemma `mine_cvg_0_cvg_fin_num`
+  + lemma `mine_cvg_minr_cvg`
+  + lemma `mine_cvg_0_cvg_0`
+  + lemma `maxr_cvg_0_cvg_0`
+  + lemma `maxe_cvg_0_cvg_fin_num`
+  + lemma `maxe_cvg_maxr_cvg`
+  + lemma `maxe_cvg_0_cvg_0`
+  + lemmas `limn_esup_lim`, `limn_einf_lim`
+
+- in file `cantor.v`,
+  + new definitions `cantor_space`, `cantor_like`, `pointed_discrete`, and
+    `tree_of`.
+  + new lemmas `cantor_space_compact`, `cantor_space_hausdorff`,
+    `cantor_zero_dimensional`, `cantor_perfect`, `cantor_like_cantor_space`,
+    `tree_map_props`, `homeomorphism_cantor_like`, and
+    `cantor_like_finite_prod`.
+  + new theorem `cantor_surj`.
+
+- in `numfun.v`:
+  + lemma `patch_indic`
+
+- in `realfun.v`:
+  + notations `nondecreasing_fun`, `nonincreasing_fun`,
+    `increasing_fun`, `decreasing_fun`
+  + lemmas `cvg_addrl`, `cvg_addrr`, `cvg_centerr`, `cvg_shiftr`,
+    `nondecreasing_cvgr`,
+	`nonincreasing_at_right_cvgr`,
+	`nondecreasing_at_right_cvgr`,
+	`nondecreasing_cvge`, `nondecreasing_is_cvge`,
+	`nondecreasing_at_right_cvge`, `nondecreasing_at_right_is_cvge`,
+	`nonincreasing_at_right_cvge`, `nonincreasing_at_right_is_cvge`
+  + lemma `cvg_at_right_left_dnbhs`
+  + lemma `cvg_at_rightP`
+  + lemma `cvg_at_leftP`
+  + lemma `cvge_at_rightP`
+  + lemma `cvge_at_leftP`
+  + lemma `lime_sup`
+  + lemma `lime_inf`
+  + lemma `lime_supE`
+  + lemma `lime_infE`
+  + lemma `lime_infN`
+  + lemma `lime_supN`
+  + lemma `lime_sup_ge0`
+  + lemma `lime_inf_ge0`
+  + lemma `lime_supD`
+  + lemma `lime_sup_le`
+  + lemma `lime_inf_sup`
+  + lemma `lim_lime_inf`
+  + lemma `lim_lime_sup`
+  + lemma `lime_sup_inf_at_right`
+  + lemma `lime_sup_inf_at_left`
+  + lemmas `lime_sup_lim`, `lime_inf_lim`
+
+- in file `measure.v`
+  + add lemmas `ae_eq_subset`, `measure_dominates_ae_eq`.
+
+- in `lebesgue_measure.v`
+  + lemma `lower_semicontinuous_measurable`
+
+- in `lebesgue_integral.v`:
+  + definition `locally_integrable`
+  + lemmas `integrable_locally`, `locally_integrableN`, `locally_integrableD`,
+    `locally_integrableB`
+  + definition `iavg`
+  + lemmas `iavg0`, `iavg_ge0`, `iavg_restrict`, `iavgD`
+  + definitions `HL_maximal`
+  + lemmas `HL_maximal_ge0`, `HL_maximalT_ge0`,
+    `lower_semicontinuous_HL_maximal`, `measurable_HL_maximal`,
+    `maximal_inequality`
+
+- in `charge.v`
+  + definition `charge_of_finite_measure` (instance of `charge`)
+  + lemmas `dominates_cscalel`, `dominates_cscaler`
+  + definition `cpushforward` (instance of `charge`)
+  + lemma `dominates_pushforward`
+  + lemma `cjordan_posE`
+  + lemma `jordan_posE`
+  + lemma `cjordan_negE`
+  + lemma `jordan_negE`
+  + lemma `Radon_Nikodym_sigma_finite`
+  + lemma `Radon_Nikodym_fin_num`
+  + lemma `Radon_Nikodym_integral`
+  + lemma `ae_eq_Radon_Nikodym_SigmaFinite`
+  + lemma `Radon_Nikodym_change_of_variables`
+  + lemma `Radon_Nikodym_cscale`
+  + lemma `Radon_Nikodym_cadd`
+  + lemma `Radon_Nikodym_chain_rule`
+
+### Changed
+
+- in `boolp.v`
+  - lemmas `orC` and `andC` now use `commutative`
+
+- moved from `topology.v` to `mathcomp_extra.v`
+  + definition `monotonous`
+
+- in `normedtype.v`:
+  + lemmas `vitali_lemma_finite` and `vitali_lemma_finite_cover` now returns
+    duplicate-free lists of indices
+
+- in `sequences.v`:
+  + change the implicit arguments of `trivIset_seqDU`
+  + `limn_esup` now defined from `lime_sup`
+  + `limn_einf` now defined from `limn_esup`
+
+- moved from `lebesgue_integral.v` to `measure.v`:
+  + definition `ae_eq`
+  + lemmas
+	`ae_eq0`,
+	`ae_eq_comp`,
+	`ae_eq_funeposneg`,
+	`ae_eq_refl`,
+	`ae_eq_trans`,
+	`ae_eq_sub`,
+	`ae_eq_mul2r`,
+	`ae_eq_mul2l`,
+	`ae_eq_mul1l`,
+	`ae_eq_abse`
+
+- in `charge.v`
+  + definition `jordan_decomp` now uses `cadd` and `cscale`
+  + definition `Radon_Nikodym_SigmaFinite` now in a module `Radon_Nikodym_SigmaFinite` with
+    * definition `f`
+    * lemmas `f_ge0`, `f_fin_num`, `f_integrable`, `f_integral`
+    * lemma `change_of_variables`
+    * lemma `integralM`
+    * lemma `chain_rule`
+
+### Renamed
+
+- in `exp.v`:
+  + `lnX` -> `lnXn`
+
+- in `charge.v`:
+  + `dominates_caddl` -> `dominates_cadd`
+
+### Generalized
+
+- in `lebesgue_measure.v`
+  + an hypothesis of lemma `integral_ae_eq` is weakened
+
+- in `lebesgue_integral.v`
+  + `ge0_integral_bigsetU` generalized from `nat` to `eqType`
+
+### Removed
+
+- in `boolp.v`:
+  + lemma `pdegen`
+
+- in `forms.v`:
+  + lemmas `eq_map_mx`, `map_mx_id`
 
 ## [0.6.6] - 2023-11-14
 

CHANGELOG_UNRELEASED.md

@@ -147,71 +147,15 @@
 	 `inhabitedE`, `inhabited_witness`
 
 ### Changed
-
-- in `normedtype.v`:
-  + lemmas `vitali_lemma_finite` and `vitali_lemma_finite_cover` now returns
-    duplicate-free lists of indices
-
-- moved from `lebesgue_integral.v` to `measure.v`:
-  + definition `ae_eq`
-  + lemmas
-	`ae_eq0`,
-	`ae_eq_comp`,
-	`ae_eq_funeposneg`,
-	`ae_eq_refl`,
-	`ae_eq_trans`,
-	`ae_eq_sub`,
-	`ae_eq_mul2r`,
-	`ae_eq_mul2l`,
-	`ae_eq_mul1l`,
-	`ae_eq_abse`
-
-- in `charge.v`
-  + definition `jordan_decomp` now uses `cadd` and `cscale`
-  + definition `Radon_Nikodym_SigmaFinite` now in a module `Radon_Nikodym_SigmaFinite` with
-    * definition `f`
-    * lemmas `f_ge0`, `f_fin_num`, `f_integrable`, `f_integral`
-    * lemma `change_of_variables`
-    * lemma `integralM`
-    * lemma `chain_rule`
-
-- in `sequences.v`:
-  + change the implicit arguments of `trivIset_seqDU`
-- moved from `topology.v` to `mathcomp_extra.v`
-  + definition `monotonous`
-
-- in `sequences.v`:
-  + `limn_esup` now defined from `lime_sup`
-  + `limn_einf` now defined from `limn_esup`
-
--in `boolp.v`
-  - lemmas `orC` and `andC` now use `commutative`
 
 ### Renamed
 
-- in `exp.v`:
-  + `lnX` -> `lnXn`
-- in `charge.v`:
-  + `dominates_caddl` -> `dominates_cadd`
-
 ### Generalized
 
-- in `lebesgue_integral.v`
-  + `ge0_integral_bigsetU` generalized from `nat` to `eqType`
-- in `lebesgue_measure.v`
-  + an hypothesis of lemma `integral_ae_eq` is weakened
-
 ### Deprecated
 
 ### Removed
 
-- in `forms.v`:
-  + lemmas `eq_map_mx`, `map_mx_id`
-
-- in `boolp.v`:
-  + lemma `pdegen`
-
-
 ### Infrastructure
 
 ### Misc

INSTALL.md

@@ -4,6 +4,7 @@
 
 - [The Coq Proof Assistant version ≥ 8.14](https://coq.inria.fr)
 - [Mathematical Components version ≥ 1.13.0](https://github.com/math-comp/math-comp)
+  + except `coq-mathcomp-solvable` ≥ 1.15.0
 - [Finmap library version ≥ 1.5.1](https://github.com/math-comp/finmap)
 - [Hierarchy builder version >= 1.2.0](https://github.com/math-comp/hierarchy-builder)
 
@@ -47,7 +48,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.0.6.6
+$ opam install coq-mathcomp-analysis.0.6.7
 ```
 4. Everytime you want to work in this same context, you need to type
 ```

README.md

@@ -33,12 +33,12 @@ the Coq proof-assistant and using the Mathematical Components library.
   - Pierre-Yves Strub (initial)
   - Laurent Théry
 - License: [CeCILL-C](LICENSE)
-- Compatible Coq versions: Coq 8.14 to 8.17 (or dev)
+- Compatible Coq versions: Coq 8.14 to 8.18 (or dev)
 - Additional dependencies:
   - [MathComp ssreflect 1.13 or later](https://math-comp.github.io)
   - [MathComp fingroup 1.13 or later](https://math-comp.github.io)
   - [MathComp algebra 1.13 or later](https://math-comp.github.io)
-  - [MathComp solvable 1.13 or later](https://math-comp.github.io)
+  - [MathComp solvable 1.15 or later](https://math-comp.github.io)
   - [MathComp field 1.13 or later](https://math-comp.github.io)
   - [MathComp finmap 1.5.1](https://github.com/math-comp/finmap)
   - [MathComp bigenough 1.0.0](https://github.com/math-comp/bigenough)
@@ -80,7 +80,7 @@ own risk.
 ## Documentation
 
 Each file is documented in its header
-([coqdoc presentation for the last version](https://math-comp.github.io/analysis/htmldoc_0_6_6/index.html)).
+([coqdoc presentation for the last version](https://math-comp.github.io/analysis/htmldoc_0_6_7/index.html)).
 
 Changes are documented in [CHANGELOG.md](CHANGELOG.md) and
 [CHANGELOG_UNRELEASED.md](CHANGELOG_UNRELEASED.md).
@@ -93,6 +93,7 @@ Other work using MathComp-Analysis:
 - [A Formal Classical Proof of Hahn-Banach in Coq](https://lipn.univ-paris13.fr/~kerjean/slides/slidesTYPES19.pdf) (2019)
 - [Semantics of Probabilistic Programs using s-Finite Kernels in Coq](https://hal.inria.fr/hal-03917948/document) (2023)
 - [CoqQ: Foundational Verification of Quantum Programs](https://arxiv.org/pdf/2207.11350.pdf) (2023)
+- [Experimenting with an intrinsically-typed probabilistic programming language in Coq](https://staff.aist.go.jp/reynald.affeldt/documents/syntax-aplas2023.pdf) (2023)
 
 ## Mathematical structures