From 084d85a8bff34f83ac2f7d59da5e25838c6c5c48 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 18 Dec 2024 23:13:57 +0100 Subject: [PATCH 1/2] changelog for 1.8.0 --- CHANGELOG.md | 118 +++++++++++++++++++++++++++++++++++++++- CHANGELOG_UNRELEASED.md | 106 ------------------------------------ 2 files changed, 117 insertions(+), 107 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a3a1f0e54..6b9f6bff1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,122 @@ # 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 `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` + + lemmas `integrable_pushforward`, `integral_pushforward` + + lemma `integral_measure_add` + +- in `constructive_ereal.v`: + + notations `\prod` in scope ereal_scope + + lemmas `prode_ge0`, `prode_fin_num` + +- in `probability.v`: + + lemma `expectation_def` + + notation `'M_` + + lemma `integral_distribution` (existing lemma `integral_distribution` has been renamed) + +- in `measure.v`: + + lemma `countable_bigcupT_measurable` + + definition `discrete_measurable` + + lemmas `discrete_measurable0`, `discrete_measurableC`, `discrete_measurableU` + +- in file `realfun.v`: + + lemma `cvg_nbhsP` + +- in `lebesgue_measure.v`: + + lemma `measurable_powRr` + +### 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` + + `integral_distribution` -> `ge0_integral_distribution` + +- 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` + +### 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) ## [1.7.0] - 2024-11-22 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c3300c2f6..67bb43c3b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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 From f09488a0ad5a1ed7ea1a2c7fe434d92481df9299 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 19 Dec 2024 08:34:06 +0900 Subject: [PATCH 2/2] fix --- CHANGELOG.md | 69 ++++++++++++++++++++++++++-------------------------- INSTALL.md | 2 +- README.md | 2 +- 3 files changed, 36 insertions(+), 37 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6b9f6bff1..9c4c1d90d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,16 +6,30 @@ Latest releases: [[1.8.0] - 2024-12-19](#180---2024-12-19), [[1.7.0] - 2024-11-2 ### 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 `mathcomp_extra.v`: - + lemma `partition_disjoint_bigfcup` +- 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`) @@ -25,42 +39,17 @@ Latest releases: [[1.8.0] - 2024-12-19](#180---2024-12-19), [[1.7.0] - 2024-11-2 + lemmas `integrable_pushforward`, `integral_pushforward` + lemma `integral_measure_add` -- in `constructive_ereal.v`: - + notations `\prod` in scope ereal_scope - + lemmas `prode_ge0`, `prode_fin_num` - - in `probability.v`: + lemma `expectation_def` + notation `'M_` + lemma `integral_distribution` (existing lemma `integral_distribution` has been renamed) -- in `measure.v`: - + lemma `countable_bigcupT_measurable` - + definition `discrete_measurable` - + lemmas `discrete_measurable0`, `discrete_measurableC`, `discrete_measurableU` - -- in file `realfun.v`: - + lemma `cvg_nbhsP` - -- in `lebesgue_measure.v`: - + lemma `measurable_powRr` - ### 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` - + `integral_distribution` -> `ge0_integral_distribution` +### Renamed - in `classical_sets.v`: + `preimage_itv_o_infty` -> `preimage_itvoy` @@ -76,11 +65,24 @@ Latest releases: [[1.8.0] - 2024-12-19](#180---2024-12-19), [[1.7.0] - 2024-11-2 - 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` @@ -93,9 +95,6 @@ Latest releases: [[1.8.0] - 2024-12-19](#180---2024-12-19), [[1.7.0] - 2024-11-2 + 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`: @@ -103,10 +102,6 @@ Latest releases: [[1.8.0] - 2024-12-19](#180---2024-12-19), [[1.7.0] - 2024-11-2 ### 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) @@ -118,6 +113,10 @@ Latest releases: [[1.8.0] - 2024-12-19](#180---2024-12-19), [[1.7.0] - 2024-11-2 + 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 ### Added diff --git a/INSTALL.md b/INSTALL.md index 92391bb48..993edc462 100644 --- a/INSTALL.md +++ b/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 ``` diff --git a/README.md b/README.md index 336a25e70..489fe27d5 100644 --- a/README.md +++ b/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: