From bd1e2acfdad720a532f42e55d2246ceaa15e2d89 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 14 Nov 2023 13:51:28 +0900 Subject: [PATCH] changelog for version 0.6.6 (#1095) * changelog for version 0.6.6 --- CHANGELOG.md | 231 +++++++++++++++++++++++++++++++++- CHANGELOG_UNRELEASED.md | 241 ------------------------------------ INSTALL.md | 2 +- README.md | 2 +- coq-mathcomp-classical.opam | 2 +- 5 files changed, 233 insertions(+), 245 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1ab785a8f..c53e570a9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,235 @@ # Changelog -Lastest releases: [[0.6.5] - 2023-10-02](#065---2023-10-02) and [[0.6.4] - 2023-08-05](#064---2023-08-05) +Latest releases: [[0.6.6] - 2023-11-14](#066---2023-11-14) and [[0.6.5] - 2023-10-02](#065---2023-10-02) + +## [0.6.6] - 2023-11-14 + +### Added + +- in `mathcomp_extra.v` + + lemmas `ge0_ler_normr`, `gt0_ler_normr`, `le0_ger_normr` and `lt0_ger_normr` + + lemma `leq_ltn_expn` + + lemma `onemV` + +- in `classical_sets.v`: + + lemma `set_cons1` + + lemma `trivIset_bigcup` + + definition `maximal_disjoint_subcollection` + + lemma `ex_maximal_disjoint_subcollection` + + lemmas `mem_not_I`, `trivIsetT_bigcup` + +- in `constructive_ereal.v`: + + lemmas `gt0_fin_numE`, `lt0_fin_numE` + + lemmas `le_er_map`, `er_map_idfun` + +- in `reals.v`: + + lemma `le_inf` + + lemmas `ceilN`, `floorN` + +- in `topology.v`: + + lemmas `closure_eq0`, `separated_open_countable` + +- in `normedtype.v`: + + lemmas `ball0`, `ball_itv`, `closed_ball0`, `closed_ball_itv` + + definitions `cpoint`, `radius`, `is_ball` + + definition `scale_ball`, notation notation ``` *` ``` + + lemmas `sub_scale_ball`, `scale_ball1`, `sub1_scale_ball` + + lemmas `ball_inj`, `radius0`, `cpoint_ball`, `radius_ball_num`, + `radius_ball`, `is_ballP`, `is_ball_ball`, `scale_ball_set0`, + `ballE`, `is_ball_closure`, `scale_ballE`, `cpoint_scale_ball`, + `radius_scale_ball` + + lemmas `vitali_lemma_finite`, `vitali_lemma_finite_cover` + + definition `vitali_collection_partition` + + lemmas `vitali_collection_partition_ub_gt0`, + `ex_vitali_collection_partition`, `cover_vitali_collection_partition`, + `disjoint_vitali_collection_partition` + + lemma `separate_closed_ball_countable` + + lemmas `vitali_lemma_infinite`, `vitali_lemma_infinite_cover` + + lemma `open_subball` + + lemma `closed_disjoint_closed_ball` + + lemma `is_scale_ball` + + lemmas `scale_ball0`, `closure_ball`, `bigcup_ballT` + +- in `sequences.v`: + + lemma `nneseries_tail_cvg` + +- in `exp.v`: + + definition `expeR` + + lemmas `expeR0`, `expeR_ge0`, `expeR_gt0` + + lemmas `expeR_eq0`, `expeRD`, `expeR_ge1Dx` + + lemmas `ltr_expeR`, `ler_expeR`, `expeR_inj`, `expeR_total` + + lemmas `mulr_powRB1`, `fin_num_poweR`, `poweRN`, `poweR_lty`, `lty_poweRy`, `gt0_ler_poweR` + + lemma `expRM` + +- in `measure.v`: + + lemmas `negligibleI`, `negligible_bigsetU`, `negligible_bigcup` + + lemma `probability_setC` + + lemma `measure_sigma_sub_additive_tail` + + lemma `outer_measure_sigma_subadditive_tail` + +- new `lebesgue_stieltjes_measure.v`: + + notation `right_continuous` + + lemmas `right_continuousW`, `nondecreasing_right_continuousP` + + mixin `isCumulative`, structure `Cumulative`, notation `cumulative` + + `idfun` instance of `Cumulative` + + `wlength`, `wlength0`, `wlength_singleton`, `wlength_setT`, `wlength_itv`, + `wlength_finite_fin_num`, `finite_wlength_itv`, `wlength_itv_bnd`, `wlength_infty_bnd`, + `wlength_bnd_infty`, `infinite_wlength_itv`, `wlength_itv_ge0`, `wlength_Rhull`, + `le_wlength_itv`, `le_wlength`, `wlength_semi_additive`, `wlength_ge0`, + `lebesgue_stieltjes_measure_unique` + + content instance of `hlength` + + `cumulative_content_sub_fsum`, + `wlength_sigma_sub_additive`, `wlength_sigma_finite` + + measure instance of `hlength` + + definition `lebesgue_stieltjes_measure` + +- in `lebesgue_measure.v`: + + lemma `lebesgue_measurable_ball` + + lemmas `measurable_closed_ball`, `lebesgue_measurable_closed_ball` + + definition `vitali_cover` + + lemma `vitali_theorem` + +- in `lebesgue_integral.v`: + + `mfun` instances for `expR` and `comp` + + lemma `abse_integralP` + +- in `charge.v`: + + factory `isCharge` + + Notations `.-negative_set`, `.-positive_set` + + lemmas `dominates_cscale`, `Radon_Nikodym_cscale` + + definition `cadd`, lemmas `dominates_caddl`, `Radon_Nikodym_cadd` + +- in `probability.v`: + + definition `mmt_gen_fun`, `chernoff` + +- in `hoelder.v`: + + lemmas `powR_Lnorm`, `minkowski` + +### Changed + +- in `normedtype.v`: + + order of arguments of `squeeze_cvgr` + +- moved from `derive.v` to `normedtype.v`: + + lemmas `cvg_at_rightE`, `cvg_at_leftE` + +- in `measure.v`: + + order of parameters changed in `semi_sigma_additive_is_additive`, + `isMeasure` + +- in `lebesgue_measure.v`: + + are now prefixed with `LebesgueMeasure`: + * `hlength`, `hlength0`, `hlength_singleton`, `hlength_setT`, `hlength_itv`, + `hlength_finite_fin_num`, `hlength_infty_bnd`, + `hlength_bnd_infty`, `hlength_itv_ge0`, `hlength_Rhull`, + `le_hlength_itv`, `le_hlength`, `hlength_ge0`, `hlength_semi_additive`, + `hlength_sigma_sub_additive`, `hlength_sigma_finite`, `lebesgue_measure` + * `finite_hlengthE` renamed to `finite_hlentgh_itv` + * `pinfty_hlength` renamed to `infinite_hlength_itv` + + `lebesgue_measure` now defined with `lebesgue_stieltjes_measure` + + `lebesgue_measure_itv` does not refer to `hlength` anymore + + remove one argument of `lebesgue_regularity_inner_sup` + +- moved from `lebesgue_measure.v` to `lebesgue_stieltjes_measure.v` + + notations `_.-ocitv`, `_.-ocitv.-measurable` + + definitions `ocitv`, `ocitv_display` + + lemmas `is_ocitv`, `ocitv0`, `ocitvP`, `ocitvD`, `ocitvI` + +- in `lebesgue_integral.v`: + + `integral_dirac` now uses the `\d_` notation + + order of arguments in the lemma `le_abse_integral` + +- in `hoelder.v`: + + definition `Lnorm` now `HB.lock`ed + +- in `probability.v`: + + `markov` now uses `Num.nneg` + +### Renamed + +- in `ereal.v`: + + `le_er_map` -> `le_er_map_in` + +- in `sequences.v`: + + `lim_sup` -> `limn_sup` + + `lim_inf` -> `limn_inf` + + `lim_infN` -> `limn_infN` + + `lim_supE` -> `limn_supE` + + `lim_infE` -> `limn_infE` + + `lim_inf_le_lim_sup` -> `limn_inf_sup` + + `cvg_lim_inf_sup` -> `cvg_limn_inf_sup` + + `cvg_lim_supE` -> `cvg_limn_supE` + + `le_lim_supD` -> `le_limn_supD` + + `le_lim_infD` -> `le_limn_infD` + + `lim_supD` -> `limn_supD` + + `lim_infD` -> `limn_infD` + + `LimSup.lim_esup` -> `limn_esup` + + `LimSup.lim_einf` -> `limn_einf` + + `lim_einf_shift` -> `limn_einf_shift` + + `lim_esup_le_cvg` -> `limn_esup_le_cvg` + + `lim_einfN` -> `limn_einfN` + + `lim_esupN` -> `limn_esupN` + + `lim_einf_sup` -> `limn_einf_sup` + + `cvgNy_lim_einf_sup` -> `cvgNy_limn_einf_sup` + + `cvg_lim_einf_sup` -> `cvg_limn_einf_sup` + + `is_cvg_lim_einfE` -> `is_cvg_limn_einfE` + + `is_cvg_lim_esupE` -> `is_cvg_limn_esupE` + + `ereal_nondecreasing_cvg` -> `ereal_nondecreasing_cvgn` + + `ereal_nondecreasing_is_cvg` -> `ereal_nondecreasing_is_cvgn` + + `ereal_nonincreasing_cvg` -> `ereal_nonincreasing_cvgn` + + `ereal_nonincreasing_is_cvg` -> `ereal_nonincreasing_is_cvgn` + + `ereal_nondecreasing_opp` -> `ereal_nondecreasing_oppn` + + `nonincreasing_cvg_ge` -> `nonincreasing_cvgn_ge` + + `nondecreasing_cvg_le` -> `nondecreasing_cvgn_le` + + `nonincreasing_cvg` -> `nonincreasing_cvgn` + + `nondecreasing_cvg` -> `nondecreasing_cvgn` + + `nonincreasing_is_cvg` -> `nonincreasing_is_cvgn` + + `nondecreasing_is_cvg` -> `nondecreasing_is_cvgn` + + `near_nonincreasing_is_cvg` -> `near_nonincreasing_is_cvgn` + + `near_nondecreasing_is_cvg` -> `near_nondecreasing_is_cvgn` + + `nondecreasing_dvg_lt` -> `nondecreasing_dvgn_lt` + +- in `lebesgue_measure.v`: + + `measurable_fun_lim_sup` -> `measurable_fun_limn_sup` + + `measurable_fun_lim_esup` -> `measurable_fun_limn_esup` + +- in `charge.v` + + `isCharge` -> `isSemiSigmaAdditive` + +### Generalized + +- in `classical_sets.v`: + + `set_nil` generalized to `eqType` + +- in `topology.v`: + + `ball_filter` generalized to `realDomainType` + +- in `lebesgue_integral.v`: + + weaken an hypothesis of `integral_ae_eq` + +### Removed + +- `lebesgue_measure_unique` (generalized to `lebesgue_stieltjes_measure_unique`) + +- in `sequences.v`: + + notations `elim_sup`, `elim_inf` + + `LimSup.lim_esup`, `LimSup.lim_einf` + + `elim_inf_shift` + + `elim_sup_le_cvg` + + `elim_infN` + + `elim_supN` + + `elim_inf_sup` + + `cvg_ninfty_elim_inf_sup` + + `cvg_ninfty_einfs` + + `cvg_ninfty_esups` + + `cvg_pinfty_einfs` + + `cvg_pinfty_esups` + + `cvg_elim_inf_sup` + + `is_cvg_elim_infE` + + `is_cvg_elim_supE` + +- in `lebesgue_measure.v`: + + `measurable_fun_elim_sup` ## [0.6.5] - 2023-10-02 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e242107e1..971b02c98 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,257 +4,16 @@ ### Added -- in `constructive_ereal.v`: - + lemmas `gt0_fin_numE`, `lt0_fin_numE` - -- in `charge.v`: - + factory `isCharge` - + Notations `.-negative_set`, `.-positive_set` - -- in `measure.v`: - + lemmas `negligibleI`, `negligible_bigsetU`, `negligible_bigcup` - -- in `reals.v`: - + lemma `le_inf` -- in `constructive_ereal.v`: - + lemmas `le_er_map`, `er_map_idfun` -- new `lebesgue_stieltjes_measure.v`: - + notation `right_continuous` - + lemmas `right_continuousW`, `nondecreasing_right_continuousP` - + mixin `isCumulative`, structure `Cumulative`, notation `cumulative` - + `idfun` instance of `Cumulative` - + `wlength`, `wlength0`, `wlength_singleton`, `wlength_setT`, `wlength_itv`, - `wlength_finite_fin_num`, `finite_wlength_itv`, `wlength_itv_bnd`, `wlength_infty_bnd`, - `wlength_bnd_infty`, `infinite_wlength_itv`, `wlength_itv_ge0`, `wlength_Rhull`, - `le_wlength_itv`, `le_wlength`, `wlength_semi_additive`, `wlength_ge0`, - `lebesgue_stieltjes_measure_unique` - + content instance of `hlength` - + `cumulative_content_sub_fsum`, - `wlength_sigma_sub_additive`, `wlength_sigma_finite` - + measure instance of `hlength` - + definition `lebesgue_stieltjes_measure` -- in `mathcomp_extra.v` - + lemmas `ge0_ler_normr`, `gt0_ler_normr`, `le0_ger_normr` and `lt0_ger_normr` - -- in `probability.v`: - + definition `mmt_gen_fun`, `chernoff` - -- in `lebesgue_integral.v`: - + `mfun` instances for `expR` and `comp` - -- in `charge.v`: - + lemmas `dominates_cscale`, `Radon_Nikodym_cscale` - + definition `cadd`, lemmas `dominates_caddl`, `Radon_Nikodym_cadd` - -- in `lebesgue_integral.v`: - + lemma `abse_integralP` - -- in `classical_sets.v`: - + lemma `set_cons1` - + lemma `trivIset_bigcup` - + definition `maximal_disjoint_subcollection` - + lemma `ex_maximal_disjoint_subcollection` - -- in `mathcomp_extra.v`: - + lemma `leq_ltn_expn` - -- in `lebesgue_measure.v`: - + lemma `lebesgue_measurable_ball` - + lemmas `measurable_closed_ball`, `lebesgue_measurable_closed_ball` - -- in `normedtype.v`: - + lemmas `ball0`, `ball_itv`, `closed_ball0`, `closed_ball_itv` - + definitions `cpoint`, `radius`, `is_ball` - + definition `scale_ball`, notation notation ``` *` ``` - + lemmas `sub_scale_ball`, `scale_ball1`, `sub1_scale_ball` - + lemmas `ball_inj`, `radius0`, `cpoint_ball`, `radius_ball_num`, - `radius_ball`, `is_ballP`, `is_ball_ball`, `scale_ball_set0`, - `ballE`, `is_ball_closure`, `scale_ballE`, `cpoint_scale_ball`, - `radius_scale_ball` - + lemmas `vitali_lemma_finite`, `vitali_lemma_finite_cover` - + definition `vitali_collection_partition` - + lemmas `vitali_collection_partition_ub_gt0`, - `ex_vitali_collection_partition`, `cover_vitali_collection_partition`, - `disjoint_vitali_collection_partition` - + lemma `separate_closed_ball_countable` - + lemmas `vitali_lemma_infinite`, `vitali_lemma_infinite_cover` - -- in `topology.v`: - + lemmas `closure_eq0`, `separated_open_countable` - -- in `exp.v`: - + definition `expeR` - + lemmas `expeR0`, `expeR_ge0`, `expeR_gt0` - + lemmas `expeR_eq0`, `expeRD`, `expeR_ge1Dx` - + lemmas `ltr_expeR`, `ler_expeR`, `expeR_inj`, `expeR_total` - -- in `exp.v`: - + lemmas `mulr_powRB1`, `fin_num_poweR`, `poweRN`, `poweR_lty`, `lty_poweRy`, `gt0_ler_poweR` - -- in `mathcomp_extra.v`: - + lemma `onemV` - -- in `hoelder.v`: - + lemmas `powR_Lnorm`, `minkowski` - + lemma `expRM` - -- in `measure.v`: - + lemma `probability_setC` -- in `classical_sets.v`: - + lemmas `mem_not_I`, `trivIsetT_bigcup` - -- in `lebesgue_measure.v`: - + definition `vitali_cover` - + lemma `vitali_theorem` - -- in `measure.v`: - + lemma `measure_sigma_sub_additive_tail` - + lemma `outer_measure_sigma_subadditive_tail` - -- in `normedtype.v`: - + lemma `open_subball` - + lemma `closed_disjoint_closed_ball` - + lemma `is_scale_ball` - -- in `reals.v`: - + lemmas `ceilN`, `floorN` - -- in `sequences.v`: - + lemma `nneseries_tail_cvg` - -- in `normedtype.v`: - + lemmas `scale_ball0`, `closure_ball`, `bigcup_ballT` - ### Changed - -- in `hoelder.v`: - + definition `Lnorm` now `HB.lock`ed -- in `lebesgue_integral.v`: - + `integral_dirac` now uses the `\d_` notation - -- in `measure.v`: - + order of parameters changed in `semi_sigma_additive_is_additive`, - `isMeasure` - -- in `lebesgue_measure.v`: - + are now prefixed with `LebesgueMeasure`: - * `hlength`, `hlength0`, `hlength_singleton`, `hlength_setT`, `hlength_itv`, - `hlength_finite_fin_num`, `hlength_infty_bnd`, - `hlength_bnd_infty`, `hlength_itv_ge0`, `hlength_Rhull`, - `le_hlength_itv`, `le_hlength`, `hlength_ge0`, `hlength_semi_additive`, - `hlength_sigma_sub_additive`, `hlength_sigma_finite`, `lebesgue_measure` - * `finite_hlengthE` renamed to `finite_hlentgh_itv` - * `pinfty_hlength` renamed to `infinite_hlength_itv` - + `lebesgue_measure` now defined with `lebesgue_stieltjes_measure` - + `lebesgue_measure_itv` does not refer to `hlength` anymore -- moved from `lebesgue_measure.v` to `lebesgue_stieltjes_measure.v` - + notations `_.-ocitv`, `_.-ocitv.-measurable` - + definitions `ocitv`, `ocitv_display` - + lemmas `is_ocitv`, `ocitv0`, `ocitvP`, `ocitvD`, `ocitvI` - -- in `probability.v`: - + `markov` now uses `Num.nneg` -- in `lebesgue_integral.v`: - + order of arguments in the lemma `le_abse_integral` - -- in `lebesgue_measure.v`: - + remove one argument of `lebesgue_regularity_inner_sup` - -- in `normedtype.v`: - + order of arguments of `squeeze_cvgr` - -- moved from `derive.v` to `normedtype.v`: - + lemmas `cvg_at_rightE`, `cvg_at_leftE` ### Renamed -- in `charge.v` - + `isCharge` -> `isSemiSigmaAdditive` - -- in `ereal.v`: - + `le_er_map` -> `le_er_map_in` - -- in `sequences.v`: - + `lim_sup` -> `limn_sup` - + `lim_inf` -> `limn_inf` - + `lim_infN` -> `limn_infN` - + `lim_supE` -> `limn_supE` - + `lim_infE` -> `limn_infE` - + `lim_inf_le_lim_sup` -> `limn_inf_sup` - + `cvg_lim_inf_sup` -> `cvg_limn_inf_sup` - + `cvg_lim_supE` -> `cvg_limn_supE` - + `le_lim_supD` -> `le_limn_supD` - + `le_lim_infD` -> `le_limn_infD` - + `lim_supD` -> `limn_supD` - + `lim_infD` -> `limn_infD` - + `LimSup.lim_esup` -> `limn_esup` - + `LimSup.lim_einf` -> `limn_einf` - + `lim_einf_shift` -> `limn_einf_shift` - + `lim_esup_le_cvg` -> `limn_esup_le_cvg` - + `lim_einfN` -> `limn_einfN` - + `lim_esupN` -> `limn_esupN` - + `lim_einf_sup` -> `limn_einf_sup` - + `cvgNy_lim_einf_sup` -> `cvgNy_limn_einf_sup` - + `cvg_lim_einf_sup` -> `cvg_limn_einf_sup` - + `is_cvg_lim_einfE` -> `is_cvg_limn_einfE` - + `is_cvg_lim_esupE` -> `is_cvg_limn_esupE` - -- in `lebesgue_measure.v`: - + `measurable_fun_lim_sup` -> `measurable_fun_limn_sup` - + `measurable_fun_lim_esup` -> `measurable_fun_limn_esup` - -- in `sequences.v`: - + `ereal_nondecreasing_cvg` -> `ereal_nondecreasing_cvgn` - + `ereal_nondecreasing_is_cvg` -> `ereal_nondecreasing_is_cvgn` - + `ereal_nonincreasing_cvg` -> `ereal_nonincreasing_cvgn` - + `ereal_nonincreasing_is_cvg` -> `ereal_nonincreasing_is_cvgn` - + `ereal_nondecreasing_opp` -> `ereal_nondecreasing_oppn` - + `nonincreasing_cvg_ge` -> `nonincreasing_cvgn_ge` - + `nondecreasing_cvg_le` -> `nondecreasing_cvgn_le` - + `nonincreasing_cvg` -> `nonincreasing_cvgn` - + `nondecreasing_cvg` -> `nondecreasing_cvgn` - + `nonincreasing_is_cvg` -> `nonincreasing_is_cvgn` - + `nondecreasing_is_cvg` -> `nondecreasing_is_cvgn` - + `near_nonincreasing_is_cvg` -> `near_nonincreasing_is_cvgn` - + `near_nondecreasing_is_cvg` -> `near_nondecreasing_is_cvgn` - + `nondecreasing_dvg_lt` -> `nondecreasing_dvgn_lt` - ### Generalized -- in `topology.v`: - + `ball_filter` generalized to `realDomainType` - -- in `lebesgue_integral.v`: - + weaken an hypothesis of `integral_ae_eq` -- in `classical_sets.v`: - + `set_nil` generalized to `eqType` - ### Deprecated ### Removed -- `lebesgue_measure_unique` (generalized to `lebesgue_stieltjes_measure_unique`) - -- in `sequences.v`: - + notations `elim_sup`, `elim_inf` - + `LimSup.lim_esup`, `LimSup.lim_einf` - + `elim_inf_shift` - + `elim_sup_le_cvg` - + `elim_infN` - + `elim_supN` - + `elim_inf_sup` - + `cvg_ninfty_elim_inf_sup` - + `cvg_ninfty_einfs` - + `cvg_ninfty_esups` - + `cvg_pinfty_einfs` - + `cvg_pinfty_esups` - + `cvg_elim_inf_sup` - + `is_cvg_elim_infE` - + `is_cvg_elim_supE` - -- in `lebesgue_measure.v`: - + `measurable_fun_elim_sup` - ### Infrastructure ### Misc diff --git a/INSTALL.md b/INSTALL.md index 618c3c470..673be1e46 100644 --- a/INSTALL.md +++ b/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.5 +$ opam install coq-mathcomp-analysis.0.6.6 ``` 4. Everytime you want to work in this same context, you need to type ``` diff --git a/README.md b/README.md index f1904903d..4527098b4 100644 --- a/README.md +++ b/README.md @@ -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_5/index.html)). +([coqdoc presentation for the last version](https://math-comp.github.io/analysis/htmldoc_0_6_6/index.html)). Changes are documented in [CHANGELOG.md](CHANGELOG.md) and [CHANGELOG_UNRELEASED.md](CHANGELOG_UNRELEASED.md). diff --git a/coq-mathcomp-classical.opam b/coq-mathcomp-classical.opam index 7734509ca..6f8cfb2f7 100644 --- a/coq-mathcomp-classical.opam +++ b/coq-mathcomp-classical.opam @@ -32,7 +32,7 @@ tags: [ "keyword:logic" "keyword:sets" "keyword:set theory" - "keyword:functions" + "keyword:function" "keyword:cardinal" "logpath:mathcomp.classical" ]