diff --git a/CHANGELOG.md b/CHANGELOG.md index a3a1f0e54..9c4c1d90d 100644 --- a/CHANGELOG.md +++ b/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 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 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: