changelog for 1.8.0

CHANGELOG.md

@@ -1,6 +1,121 @@
 # Changelog
 
-Latest releases: [[1.7.0] - 2024-11-22](#170---2024-11-22) and [[1.6.0] - 2024-10-25](#160---2024-10-25)
+Latest releases: [[1.8.0] - 2024-12-19](#180---2024-12-19), [[1.7.0] - 2024-11-22](#170---2024-11-22) and [[1.6.0] - 2024-10-25](#160---2024-10-25)
+
+## [1.8.0] - 2024-12-19
+
+### Added
+
+- in `mathcomp_extra.v`:
+  + lemma `partition_disjoint_bigfcup`
+
+- in `constructive_ereal.v`:
+  + notations `\prod` in scope ereal_scope
+  + lemmas `prode_ge0`, `prode_fin_num`
+
+- in `num_topology.v`:
+  + lemma `in_continuous_mksetP`
+
+- in `normedtype.v`:
+  + lemmas `continuous_within_itvcyP`, `continuous_within_itvNycP`
+
+- in file `realfun.v`:
+  + lemma `cvg_nbhsP`
+
+- in `measure.v`:
+  + lemma `countable_bigcupT_measurable`
+  + definition `discrete_measurable`
+  + lemmas `discrete_measurable0`, `discrete_measurableC`, `discrete_measurableU`
+
+- in `lebesgue_measure.v`:
+  + lemma `measurable_indicP`
+  + lemma `measurable_powRr`
+
+- in `lebesgue_integral.v`:
+  + definition `dyadic_approx` (was `Let A`)
+  + definition `integer_approx` (was `Let B`)
+  + lemma `measurable_sum`
+  + lemma `integrable_indic`
+  + lemmas `integrable_pushforward`, `integral_pushforward`
+  + lemma `integral_measure_add`
+
+- in `probability.v`:
+  + lemma `expectation_def`
+  + notation `'M_`
+  + lemma `integral_distribution` (existing lemma `integral_distribution` has been renamed)
+
+### Changed
+
+- in `lebesgue_integrale.v`
+  + change implicits of `measurable_funP`
+
+### Renamed
+
+- in `classical_sets.v`:
+  + `preimage_itv_o_infty` -> `preimage_itvoy`
+  + `preimage_itv_c_infty` -> `preimage_itvcy`
+  + `preimage_itv_infty_o` -> `preimage_itvNyo`
+  + `preimage_itv_infty_c` -> `preimage_itvNyc`
+
+- in `constructive_ereal.v`:
+  + `maxeMr` -> `maxe_pMr`
+  + `maxeMl` -> `maxe_pMl`
+  + `mineMr` -> `mine_pMr`
+  + `mineMl` -> `mine_pMl`
+
+- file `homotopy_theory/path.v` -> `homotopy_theory/continuous_path.v`
+
+- in `lebesgue_measure.v`:
+  + `measurable_fun_indic` -> `measurable_indic`
+  + `emeasurable_fun_sum` -> `emeasurable_sum`
+  + `emeasurable_fun_fsum` -> `emeasurable_fsum`
+  + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum`
+
+- in `probability.v`:
+  + `expectationM` -> `expectationZl`
+  + `integral_distribution` -> `ge0_integral_distribution`
+
+### Generalized
+
+- in `sequences.v`:
+  + lemmas `cvg_restrict`, `cvg_centern`, `cvg_shiftn cvg_shiftS`
+
+- in `lebesgue_integral.v`:
+  + lemma `measurable_sfunP`
+
+- in `probability.v`:
+  + definition `random_variable`
+  + lemmas `notin_range_measure`, `probability_range`
+  + definition `distribution`
+  + lemma `probability_distribution`, `integral_distribution`
+  + mixin `MeasurableFun_isDiscrete`
+  + structure `discreteMeasurableFun`
+  + definition `discrete_random_variable`
+  + lemma `dRV_dom_enum`
+  + definitions `dRV_dom`, `dRV_enum`, `enum_prob`
+  + lemmas `distribution_dRV`, `sum_enum_prob`
+
+### Deprecated
+
+- in file `lebesgue_integral.v`:
+  + lemma `approximation`
+
+### Removed
+
+- in `constructive_ereal.v`
+  + notation `lee_opp` (deprecated since 0.6.5)
+  + notation `lte_opp` (deprecated since 0.6.5)
+
+- in `measure.v`:
+  + `dynkin_setI_bigsetI` (use `big_ind` instead)
+
+- in `lebesgue_measurable.v`:
+  + notation `measurable_fun_power_pos` (deprecated since 0.6.3)
+  + notation `measurable_power_pos` (deprecated since 0.6.4)
+
+- in `lebesgue_integral.v`:
+  + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`)
+  + notation `measurable_fun_indic` (deprecation since 0.6.3)
 
 ## [1.7.0] - 2024-11-22
 

CHANGELOG_UNRELEASED.md

@@ -4,122 +4,16 @@
 
 ### Added
 
-- in `num_topology.v`:
-  + lemma `in_continuous_mksetP`
-
-- in `normedtype.v`:
-  + lemmas `continuous_within_itvcyP`, `continuous_within_itvNycP`
-
-- in `mathcomp_extra.v`:
-  + lemma `partition_disjoint_bigfcup`
-- in `lebesgue_measure.v`:
-  + lemma `measurable_indicP`
-
-- in `lebesgue_integral.v`:
-  + definition `dyadic_approx` (was `Let A`)
-  + definition `integer_approx` (was `Let B`)
-  + lemma `measurable_sum`
-  + lemma `integrable_indic`
-
-- in `constructive_ereal.v`:
-  + notations `\prod` in scope ereal_scope
-  + lemmas `prode_ge0`, `prode_fin_num`
-- in `probability.v`:
-  + lemma `expectation_def`
-  + notation `'M_`
-
-- in `lebesgue_integral.v`:
-  + lemmas `integrable_pushforward`, `integral_pushforward`
-  + lemma `integral_measure_add`
-
-- in `probability.v`
-  + lemma `integral_distribution` (existing lemma `integral_distribution` has been renamed)
-
-- in `measure.v`:
-  + lemma `countable_bigcupT_measurable`
-
-- in file `realfun.v`:
-  + lemma `cvg_nbhsP`
-
-- in `lebesgue_measure.v`:
-  + lemma `measurable_powRr`
-
-- in `measure.v`:
-  + definition `discrete_measurable`
-  + lemmas `discrete_measurable0`, `discrete_measurableC`, `discrete_measurableU`
-
 ### Changed
 
-- in `lebesgue_integrale.v`
-  + change implicits of `measurable_funP`
-
 ### Renamed
 
-- in `lebesgue_measure.v`:
-  + `measurable_fun_indic` -> `measurable_indic`
-  + `emeasurable_fun_sum` -> `emeasurable_sum`
-  + `emeasurable_fun_fsum` -> `emeasurable_fsum`
-  + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum`
-- in `probability.v`:
-  + `expectationM` -> `expectationZl`
-
-- in `classical_sets.v`:
-  + `preimage_itv_o_infty` -> `preimage_itvoy`
-  + `preimage_itv_c_infty` -> `preimage_itvcy`
-  + `preimage_itv_infty_o` -> `preimage_itvNyo`
-  + `preimage_itv_infty_c` -> `preimage_itvNyc`
-
-- in `constructive_ereal.v`:
-  + `maxeMr` -> `maxe_pMr`
-  + `maxeMl` -> `maxe_pMl`
-  + `mineMr` -> `mine_pMr`
-  + `mineMl` -> `mine_pMl`
-
-- in `probability.v`:
-  + `integral_distribution` -> `ge0_integral_distribution`
-
-- file `homotopy_theory/path.v` -> `homotopy_theory/continuous_path.v`
-
 ### Generalized
 
-- in `sequences.v`:
-  + lemmas `cvg_restrict`, `cvg_centern`, `cvg_shiftn cvg_shiftS`
-
-- in `probability.v`:
-  + definition `random_variable`
-  + lemmas `notin_range_measure`, `probability_range`
-  + definition `distribution`
-  + lemma `probability_distribution`, `integral_distribution`
-  + mixin `MeasurableFun_isDiscrete`
-  + structure `discreteMeasurableFun`
-  + definition `discrete_random_variable`
-  + lemma `dRV_dom_enum`
-  + definitions `dRV_dom`, `dRV_enum`, `enum_prob`
-  + lemmas `distribution_dRV`, `sum_enum_prob`
-
-- in `lebesgue_integral.v`:
-  + lemma `measurable_sfunP`
-
 ### Deprecated
 
-- in file `lebesgue_integral.v`:
-  + lemma `approximation`
-
 ### Removed
 
-- in `lebesgue_integral.v`:
-  + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`)
-  + notation `measurable_fun_indic` (deprecation since 0.6.3)
-- in `constructive_ereal.v`
-  + notation `lee_opp` (deprecated since 0.6.5)
-  + notation `lte_opp` (deprecated since 0.6.5)
-- in `measure.v`:
-  + `dynkin_setI_bigsetI` (use `big_ind` instead)
-
-- in `lebesgue_measurable.v`:
-  + notation `measurable_fun_power_pos` (deprecated since 0.6.3)
-  + notation `measurable_power_pos` (deprecated since 0.6.4)
-
 ### Infrastructure
 
 ### Misc

INSTALL.md

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

README.md

@@ -88,7 +88,7 @@ We try to preserve backward compatibility as best as we can.
 
 Each file is documented in its header in ASCII.
 
-[HTML rendering of the source code](https://math-comp.github.io/analysis/htmldoc_1_7_0/index.html) (using a fork of [`coq2html`](https://github.com/xavierleroy/coq2html)).
+[HTML rendering of the source code](https://math-comp.github.io/analysis/htmldoc_1_8_0/index.html) (using a fork of [`coq2html`](https://github.com/xavierleroy/coq2html)).
 It includes inheritance diagrams for the mathematical structures that MathComp-Analysis adds on top of MathComp's ones.
 
 Overview presentations: