changelog for version 0.6.5

CHANGELOG.md

@@ -1,6 +1,99 @@
 # Changelog
 
-Lastest releases: [[0.6.4] - 2023-08-05](#064---2023-08-05) and [[0.6.3] - 2023-06-21](#063---2023-06-21)
+Lastest releases: [[0.6.5] - 2023-10-02](#065---2023-10-02) and [[0.6.4] - 2023-08-05](#064---2023-08-05)
+
+## [0.6.5] - 2023-10-02
+
+### Added
+
+- in `mathcomp_extra.v`:
+  + lemmas `le_bigmax_seq`, `bigmax_sup_seq`
+  + lemma `gerBl`
+- in `classical_sets.v`:
+  + lemma `setU_id2r`
+- in `ereal.v`:
+  + lemmas `uboundT`, `supremumsT`, `supremumT`, `ereal_supT`, `range_oppe`,
+    `ereal_infT`
+- in `constructive_ereal.v`:
+  + lemma `eqe_pdivr_mull`
+  + lemma `bigmaxe_fin_num`
+- in file `topology.v`,
+  + new definition `regular_space`.
+  + new lemma `ent_closure`.
+- in `normedtype.v`:
+  + lemmas `open_itvoo_subset`, `open_itvcc_subset`
+  + new lemmas `normal_openP`, `uniform_regular`,
+    `regular_openP`, and `pseudometric_normal`.
+- in `sequences.v`:
+  + lemma `cvge_harmonic`
+- in `convex.v`:
+  + lemmas `conv_gt0`, `convRE`
+  + definition `convex_function`
+- in `exp.v`:
+  + lemmas `concave_ln`, `conjugate_powR`
+  + lemmas `ln_le0`, `ger_powR`, `ler1_powR`, `le1r_powR`, `ger1_powR`,
+    `ge1r_powR`, `ge1r_powRZ`, `le1r_powRZ`
+  + lemma `gt0_ltr_powR`
+  + lemma `powR_injective`
+- in `measure.v`:
+  + lemmas `outer_measure_subadditive`, `outer_measureU2`
+  + definition `ess_sup`, lemma `ess_sup_ge0`
+- in `lebesgue_measure.v`:
+  + lemma `compact_measurable`
+  + declare `lebesgue_measure` as a `SigmaFinite` instance
+  + lemma `lebesgue_regularity_inner_sup`
+  + lemma `measurable_ball`
+  + lemma `measurable_mulrr`
+- in `lebesgue_integral.v`,
+  + new lemmas `integral_le_bound`, `continuous_compact_integrable`, and
+    `lebesgue_differentiation_continuous`.
+  + new lemmas `simple_bounded`, `measurable_bounded_integrable`,
+    `compact_finite_measure`, `approximation_continuous_integrable`
+  + lemma `ge0_integral_count`
+- in `kernel.v`:
+  + `kseries` is now an instance of `Kernel_isSFinite_subdef`
+- new file `hoelder.v`:
+  + definition `Lnorm`, notations `'N[mu]_p[f]`, `'N_p[f]`
+  + lemmas `Lnorm1`, `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0`
+  + lemma `hoelder`
+  + lemmas `Lnorm_counting`, `hoelder2`, `convex_powR`
+
+### Changed
+
+- in `cardinality.v`:
+  + implicits of `fimfunP`
+- in `constructive_ereal.v`:
+  + `lee_adde` renamed to `lee_addgt0Pr` and turned into a reflect
+  + `lee_dadde` renamed to `lee_daddgt0Pr` and turned into a reflect
+- in `exp.v`:
+  + `gt0_ler_powR` now uses `Num.nneg`
+- removed dependency in `Rstruct.v` on `normedtype.v`:
+- added dependency in `normedtype.v` on `Rstruct.v`:
+- `mnormalize` moved from `kernel.v` to `measure.v` and generalized
+- in `measure.v`:
+  + implicits of `measurable_fst` and `measurable_snd`
+- in `lebesgue_integral.v`
+  + rewrote `negligible_integral` to replace the positivity condition
+    with an integrability condition, and added `ge0_negligible_integral`.
+  + implicits of `integral_le_bound`
+
+### Renamed
+
+- in `constructive_ereal.v`:
+  + `lee_opp` -> `leeN2`
+  + `lte_opp` -> `lteN2`
+- in `normedtype.v`:
+  + `normal_urysohnP` -> `normal_separatorP`.
+- in `exp.v`:
+  + `gt0_ler_powR` -> `ge0_ler_powR`
+
+### Removed
+
+- in `signed.v`:
+  + specific notation for `2%:R`,
+    now subsumed by number notations in MC >= 1.15
+    Note that when importing ssrint, `2` now denotes `2%:~R` rather than `2%:R`,
+    which are convertible but don't have the same head constant.
 
 ## [0.6.4] - 2023-08-05
 

CHANGELOG_UNRELEASED.md

@@ -4,138 +4,16 @@
 
 ### Added
 
-- in `kernel.v`:
-  + `kseries` is now an instance of `Kernel_isSFinite_subdef`
-- in `classical_sets.v`:
-  + lemma `setU_id2r`
-- in `lebesgue_measure.v`:
-  + lemma `compact_measurable`
-
-- in `measure.v`:
-  + lemmas `outer_measure_subadditive`, `outer_measureU2`
-
-- in `lebesgue_measure.v`:
-  + declare `lebesgue_measure` as a `SigmaFinite` instance
-  + lemma `lebesgue_regularity_inner_sup`
-- in `convex.v`:
-  + lemmas `conv_gt0`, `convRE`
-
-- in `exp.v`:
-  + lemmas `concave_ln`, `conjugate_powR`
-
-- in file `lebesgue_integral.v`,
-  + new lemmas `integral_le_bound`, `continuous_compact_integrable`, and 
-    `lebesgue_differentiation_continuous`.
-
-- in `normedtype.v`:
-  + lemmas `open_itvoo_subset`, `open_itvcc_subset`
-
-- in `lebesgue_measure.v`:
-  + lemma `measurable_ball`
-
-- in file `normedtype.v`,
-  + new lemmas `normal_openP`, `uniform_regular`,
-    `regular_openP`, and `pseudometric_normal`.
-- in file `topology.v`,
-  + new definition `regular_space`.
-  + new lemma `ent_closure`.
-
-- in `lebesgue_measure.v`:
-  + lemma `measurable_mulrr`
-
-- in `constructive_ereal.v`:
-  + lemma `eqe_pdivr_mull`
-
-- new file `hoelder.v`:
-  + definition `Lnorm`, notations `'N[mu]_p[f]`, `'N_p[f]`
-  + lemmas `Lnorm1`, `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0`
-  + lemma `hoelder`
-
-- in file `lebesgue_integral.v`,
-  + new lemmas `simple_bounded`, `measurable_bounded_integrable`, 
-    `compact_finite_measure`, `approximation_continuous_integrable`
-
-- in `sequences.v`:
-  + lemma `cvge_harmonic`
-
-- in `mathcomp_extra.v`:
-  + lemmas `le_bigmax_seq`, `bigmax_sup_seq`
-
-- in `constructive_ereal.v`:
-  + lemma `bigmaxe_fin_num`
-- in `ereal.v`:
-  + lemmas `uboundT`, `supremumsT`, `supremumT`, `ereal_supT`, `range_oppe`,
-    `ereal_infT`
-
-- in `measure.v`:
-  + definition `ess_sup`, lemma `ess_sup_ge0`
-- in `convex.v`:
-  + definition `convex_function`
-
-- in `exp.v`:
-  + lemmas `ln_le0`, `ger_powR`, `ler1_powR`, `le1r_powR`, `ger1_powR`,
-    `ge1r_powR`, `ge1r_powRZ`, `le1r_powRZ`
-
-- in `hoelder.v`:
-  + lemmas `Lnorm_counting`, `hoelder2`, `convex_powR`
-
-- in `lebesgue_integral.v`:
-  + lemma `ge0_integral_count`
-
-- in `exp.v`:
-  + lemma `gt0_ltr_powR`
-  + lemma `powR_injective`
-- in `mathcomp_extra.v`:
-  + lemma `gerBl`
-
 ### Changed
 
-- `mnormalize` moved from `kernel.v` to `measure.v` and generalized
-- in `constructive_ereal.v`:
-  + `lee_adde` renamed to `lee_addgt0Pr` and turned into a reflect
-  + `lee_dadde` renamed to `lee_daddgt0Pr` and turned into a reflect
-- in `lebesgue_integral.v`
-  + rewrote `negligible_integral` to replace the positivity condition
-    with an integrability condition, and added `ge0_negligible_integral`.
-
-- removed dependency in `Rstruct.v` on `normedtype.v`:
-- added dependency in `normedtype.v` on `Rstruct.v`:
-
-- in `cardinality.v`:
-  + implicits of `fimfunP`
-
-- in `lebesgue_integral.v`:
-  + implicits of `integral_le_bound`
-
-- in `measure.v`:
-  + implicits of `measurable_fst` and `measurable_snd`
-- in `exp.v`:
-  + `gt0_ler_powR` now uses `Num.nneg`
-
 ### Renamed
 
-- in `normedtype.v`: 
-  + `normal_urysohnP` -> `normal_separatorP`.
-
-- in `constructive_ereal.v`:
-  + `lee_opp` -> `leeN2`
-  + `lte_opp` -> `lteN2`
-
-- in `exp.v`:
-  + `gt0_ler_powR` -> `ge0_ler_powR`
-
 ### Generalized
 
 ### Deprecated
 
 ### Removed
 
-- in `signed.v`:
-  + specific notation for `2%:R`,
-    now subsumed by number notations in MC >= 1.15
-    Note that when importing ssrint, `2` now denotes `2%:~R` rather than `2%:R`,
-    which are convertible but don't have the same head constant.
-
 ### Infrastructure
 
 ### Misc

INSTALL.md

@@ -47,7 +47,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.0.6.4
+$ opam install coq-mathcomp-analysis.0.6.5
 ```
 4. Everytime you want to work in this same context, you need to type
 ```