From b82b9c3c201992d1790ca56428b39b85faf88503 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Fri, 24 Feb 2023 17:36:48 +0900 Subject: [PATCH] changelog fo version 0.6.1 (#855) --- CHANGELOG.md | 169 ++++++++++++++++++++++++++++++++++- CHANGELOG_UNRELEASED.md | 190 ---------------------------------------- INSTALL.md | 4 +- 3 files changed, 170 insertions(+), 193 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index d6673e1d6..f75288696 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,173 @@ # Changelog -Lastest releases: [[0.6.0] - 2022-12-14](#060---2022-12-14) and [[0.5.4] - 2022-09-07](#055---2022-09-07) +Lastest releases: [[0.6.1] - 2023-02-24](#061---2023-02-24) and [[0.6.0] - 2022-12-14](#060---2022-12-14) + +## [0.6.1] - 2023-02-24 + +### Added + +- in `mathcomp_extra.v`: + + lemma `add_onemK` + + function `swap` +- in file `boolp.v`, + + new lemma `forallp_asboolPn2`. +- in `classical_sets.v`: + + canonical `unit_pointedType` + + lemmas `setT0`, `set_unit`, `set_bool` + + lemmas `xsection_preimage_snd`, `ysection_preimage_fst` + + lemma `trivIset_mkcond` + + lemmas `xsectionI`, `ysectionI` + + lemma `coverE` + + new lemma `preimage_range`. +- in `constructive_ereal.v`: + + lemmas `EFin_sum_fine`, `sumeN` + + lemmas `adde_defDr`, `adde_def_sum`, `fin_num_sumeN` + + lemma `fin_num_adde_defr`, `adde_defN` + + lemma `oppe_inj` + + lemmas `expeS`, `fin_numX` + + lemmas `adde_def_doppeD`, `adde_def_doppeB` + + lemma `fin_num_sume_distrr` +- in `functions.v`: + + lemma `countable_bijP` + + lemma `patchE` +- in `numfun.v`: + + lemmas `xsection_indic`, `ysection_indic` +- in file `topology.v`, + + new definition `perfect_set`. + + new lemmas `perfectTP`, `perfect_prod`, and `perfect_diagonal`. + + new definitions `countable_uniformity`, `countable_uniformityT`, + `sup_pseudoMetric_mixin`, `sup_pseudoMetricType`, and + `product_pseudoMetricType`. + + new lemmas `countable_uniformityP`, `countable_sup_ent`, and + `countable_uniformity_metric`. + + new definitions `quotient_topology`, and `quotient_open`. + + new lemmas `pi_continuous`, `quotient_continuous`, and + `repr_comp_continuous`. + + new definitions `hausdorff_accessible`, `separate_points_from_closed`, and + `join_product`. + + new lemmas `weak_sep_cvg`, `weak_sep_nbhsE`, `weak_sep_openE`, + `join_product_continuous`, `join_product_open`, `join_product_inj`, and + `join_product_weak`. + + new definition `clopen`. + + new lemmas `clopenI`, `clopenU`, `clopenC`, `clopen0`, `clopenT`, + `clopen_comp`, `connected_closure`, `clopen_separatedP`, and + `clopen_connectedP`. + + new lemmas `powerset_filter_fromP` and `compact_cluster_set1`. +- in `exp.v`: + + lemma `expR_ge0` +- in `measure.v`: + + mixin `isProbability`, structure `Probability`, type `probability` + + lemma `probability_le1` + + definition `discrete_measurable_unit` + + structures `sigma_finite_additive_measure` and `sigma_finite_measure` + + lemmas `measurable_curry`, `measurable_fun_fst`, `measurable_fun_snd`, + `measurable_fun_swap`, `measurable_fun_pair`, `measurable_fun_if_pair` + + lemmas `dirac0`, `diracT` + + lemma `fin_num_fun_sigma_finite` + + structure `FiniteMeasure`, notation `{finite_measure set _ -> \bar _}` + + definition `sfinite_measure_def` + + mixin `Measure_isSFinite_subdef`, structure `SFiniteMeasure`, + notation `{sfinite_measure set _ -> \bar _}` + + mixin `SigmaFinite_isFinite` with field `fin_num_measure`, structure `FiniteMeasure`, + notation `{finite_measure set _ -> \bar _}` + + lemmas `sfinite_measure_sigma_finite`, `sfinite_mzero`, `sigma_finite_mzero` + + factory `Measure_isFinite`, `Measure_isSFinite` + + defintion `sfinite_measure_seq`, lemma `sfinite_measure_seqP` + + mixin `FiniteMeasure_isSubProbability`, structure `SubProbability`, + notation `subprobability` + + factory `Measure_isSubProbability` + + factory `FiniteMeasure_isSubProbability` + + factory `Measure_isSigmaFinite` + + lemmas `fin_num_fun_lty`, `lty_fin_num_fun` + + definition `fin_num_fun` + + structure `FinNumFun` +- in `lebesgue_measure.v`: + + lemma `measurable_fun_opp` +- in `lebesgue_integral.v` + + lemmas `integral0_eq`, `fubini_tonelli` + + product measures now take `{measure _ -> _}` arguments and their + theory quantifies over a `{sigma_finite_measure _ -> _}`. + + notations `\x`, `\x^` for `product_measure1` and `product_measure2` + +### Changed + +- in `fsbigop.v`: + + implicits of `eq_fsbigr` +- in file `topology.v`, + + lemma `compact_near_coveringP` +- in `functions.v`: + + notation `mem_fun_` +- move from `lebesgue_integral.v` to `classical_sets.v` + + lemmas `trivIset_preimage1`, `trivIset_preimage1_in` +- move from `lebesgue_integral.v` to `numfun.v` + + lemmas `fimfunE`, `fimfunEord`, factory `FiniteDecomp` + + lemmas `fimfun_mulr_closed` + + canonicals `fimfun_mul`, `fimfun_ring`, `fimfun_ringType` + + defintion `fimfun_ringMixin` + + lemmas `fimfunM`, `fimfun1`, `fimfun_prod`, `fimfunX`, + `indic_fimfun_subproof`. + + definitions `indic_fimfun`, `scale_fimfun`, `fimfun_comRingMixin` + + canonical `fimfun_comRingType` + + lemma `max_fimfun_subproof` + + mixin `IsNonNegFun`, structure `NonNegFun`, notation `{nnfun _ >-> _}` +- in `measure.v`: + + order of arguments of `isContent`, `Content`, `measure0`, `isMeasure0`, + `Measure`, `isSigmaFinite`, `SigmaFiniteContent`, `SigmaFiniteMeasure` + +### Renamed + +- in `measurable.v`: + + `measurable_fun_comp` -> `measurable_funT_comp` +- in `numfun.v`: + + `IsNonNegFun` -> `isNonNegFun` +- in `lebesgue_integral.v`: + + `IsMeasurableFunP` -> `isMeasurableFun` +- in `measure.v`: + + `{additive_measure _ -> _}` -> `{content _ -> _}` + + `isAdditiveMeasure` -> `isContent` + + `AdditiveMeasure` -> `Content` + + `additive_measure` -> `content` + + `additive_measure_snum_subproof` -> `content_snum_subproof` + + `additive_measure_snum` -> `content_snum` + + `SigmaFiniteAdditiveMeasure` -> `SigmaFiniteContent` + + `sigma_finite_additive_measure` -> `sigma_finite_content` + + `{sigma_finite_additive_measure _ -> _}` -> `{sigma_finite_content _ -> _}` +- in `constructive_ereal.v`: + + `fin_num_adde_def` -> `fin_num_adde_defl` + + `oppeD` -> `fin_num_oppeD` + + `oppeB` -> `fin_num_oppeB` + + `doppeD` -> `fin_num_doppeD` + + `doppeB` -> `fin_num_doppeB` +- in `topology.v`: + + `finSubCover` -> `finite_subset_cover` +- in `sequences.v`: + + `eq_eseries` -> `eq_eseriesr` +- in `esum.v`: + + `summable_nneseries_esum` -> `summable_eseries_esum` + + `summable_nneseries` -> `summable_eseries` + +### Generalized + +- in `classical_sets.v`: + + `xsection_preimage_snd`, `ysection_preimage_fst` +- in `constructive_ereal.v`: + + `oppeD`, `oppeB` +- in `esum.v`: + + lemma `esum_esum` +- in `measure.v` + + lemma `measurable_fun_comp` + + lemma `measure_bigcup` generalized, + + lemma `eq_measure` + + `sigma_finite` generalized from `numFieldType` to `numDomainType` + + `fin_num_fun_sigma_finite` generalized from `measurableType` to `algebraOfSetsType` +- in `lebesgue_integral.v`: + + lemma `measurable_sfunP` + + lemma `integrable_abse` + +### Removed + +- in `esum.v`: + + lemma `fsbig_esum` ## [0.6.0] - 2022-12-14 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 38fc76d31..67bb43c3b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,206 +4,16 @@ ### Added -- in `classical_sets.v`: - + canonical `unit_pointedType` -- in `measure.v`: - + mixin `isProbability`, structure `Probability`, type `probability` - + lemma `probability_le1` - + definition `discrete_measurable_unit` - + structures `sigma_finite_additive_measure` and `sigma_finite_measure` - -- in file `topology.v`, - + new definition `perfect_set`. - + new lemmas `perfectTP`, `perfect_prod`, and `perfect_diagonal`. -- in `constructive_ereal.v`: - + lemmas `EFin_sum_fine`, `sumeN` - + lemmas `adde_defDr`, `adde_def_sum`, `fin_num_sumeN` - + lemma `fin_num_adde_defr`, `adde_defN` - -- in `constructive_ereal.v`: - + lemma `oppe_inj` - -- in `mathcomp_extra.v`: - + lemma `add_onemK` - + function `swap` -- in `classical_sets.v`: - + lemmas `setT0`, `set_unit`, `set_bool` - + lemmas `xsection_preimage_snd`, `ysection_preimage_fst` -- in `exp.v`: - + lemma `expR_ge0` -- in `measure.v` - + lemmas `measurable_curry`, `measurable_fun_fst`, `measurable_fun_snd`, - `measurable_fun_swap`, `measurable_fun_pair`, `measurable_fun_if_pair` - + lemmas `dirac0`, `diracT` - + lemma `fin_num_fun_sigma_finite` -- in `lebesgue_measure.v`: - + lemma `measurable_fun_opp` -- in `lebesgue_integral.v` - + lemmas `integral0_eq`, `fubini_tonelli` - + product measures now take `{measure _ -> _}` arguments and their - theory quantifies over a `{sigma_finite_measure _ -> _}`. - -- in `classical_sets.v`: - + lemma `trivIset_mkcond` -- in `numfun.v`: - + lemmas `xsection_indic`, `ysection_indic` -- in `classical_sets.v`: - + lemmas `xsectionI`, `ysectionI` -- in `lebesgue_integral.v`: - + notations `\x`, `\x^` for `product_measure1` and `product_measure2` - -- in `constructive_ereal.v`: - + lemmas `expeS`, `fin_numX` - -- in `functions.v`: - + lemma `countable_bijP` - + lemma `patchE` - -- in file `topology.v`, - + new definitions `countable_uniformity`, `countable_uniformityT`, - `sup_pseudoMetric_mixin`, `sup_pseudoMetricType`, and - `product_pseudoMetricType`. - + new lemmas `countable_uniformityP`, `countable_sup_ent`, and - `countable_uniformity_metric`. - -- in `constructive_ereal.v`: - + lemmas `adde_def_doppeD`, `adde_def_doppeB` - + lemma `fin_num_sume_distrr` -- in `classical_sets.v`: - + lemma `coverE` - -- in file `topology.v`, - + new definitions `quotient_topology`, and `quotient_open`. - + new lemmas `pi_continuous`, `quotient_continuous`, and - `repr_comp_continuous`. - -- in file `boolp.v`, - + new lemma `forallp_asboolPn2`. -- in file `classical_sets.v`, - + new lemma `preimage_range`. -- in file `topology.v`, - + new definitions `hausdorff_accessible`, `separate_points_from_closed`, and - `join_product`. - + new lemmas `weak_sep_cvg`, `weak_sep_nbhsE`, `weak_sep_openE`, - `join_product_continuous`, `join_product_open`, `join_product_inj`, and - `join_product_weak`. -- in `measure.v`: - + structure `FiniteMeasure`, notation `{finite_measure set _ -> \bar _}` - -- in file `topology.v`, - + new definition `clopen`. - + new lemmas `clopenI`, `clopenU`, `clopenC`, `clopen0`, `clopenT`, - `clopen_comp`, `connected_closure`, `clopen_separatedP`, and - `clopen_connectedP`. - -- in file `topology.v`, - + new lemmas `powerset_filter_fromP` and `compact_cluster_set1`. - -- in `measure.v`: - + definition `sfinite_measure_def` - + mixin `Measure_isSFinite_subdef`, structure `SFiniteMeasure`, - notation `{sfinite_measure set _ -> \bar _}` - + mixin `SigmaFinite_isFinite` with field `fin_num_measure`, structure `FiniteMeasure`, - notation `{finite_measure set _ -> \bar _}` - + lemmas `sfinite_measure_sigma_finite`, `sfinite_mzero`, `sigma_finite_mzero` - + factory `Measure_isFinite`, `Measure_isSFinite` - + defintion `sfinite_measure_seq`, lemma `sfinite_measure_seqP` - + mixin `FiniteMeasure_isSubProbability`, structure `SubProbability`, - notation `subprobability` - + factory `Measure_isSubProbability` - + factory `FiniteMeasure_isSubProbability` - + factory `Measure_isSigmaFinite` - + lemmas `fin_num_fun_lty`, `lty_fin_num_fun` - + definition `fin_num_fun` - + structure `FinNumFun` - ### Changed -- in `fsbigop.v`: - + implicits of `eq_fsbigr` -- move from `lebesgue_integral.v` to `classical_sets.v` - + lemmas `trivIset_preimage1`, `trivIset_preimage1_in` -- move from `lebesgue_integral.v` to `numfun.v` - + lemmas `fimfunE`, `fimfunEord`, factory `FiniteDecomp` - + lemmas `fimfun_mulr_closed` - + canonicals `fimfun_mul`, `fimfun_ring`, `fimfun_ringType` - + defintion `fimfun_ringMixin` - + lemmas `fimfunM`, `fimfun1`, `fimfun_prod`, `fimfunX`, - `indic_fimfun_subproof`. - + definitions `indic_fimfun`, `scale_fimfun`, `fimfun_comRingMixin` - + canonical `fimfun_comRingType` - + lemma `max_fimfun_subproof` - + mixin `IsNonNegFun`, structure `NonNegFun`, notation `{nnfun _ >-> _}` - -- in file `topology.v`, - + lemma `compact_near_coveringP` -- in `functions.v`: - + notation `mem_fun_` -- in `measure.v`: - + order of arguments of `isContent`, `Content`, `measure0`, `isMeasure0`, - `Measure`, `isSigmaFinite`, `SigmaFiniteContent`, `SigmaFiniteMeasure` - ### Renamed -- in `measurable.v`: - + `measurable_fun_comp` -> `measurable_funT_comp` -- in `numfun.v`: - + `IsNonNegFun` -> `isNonNegFun` -- in `lebesgue_integral.v`: - + `IsMeasurableFunP` -> `isMeasurableFun` -- in `measure.v`: - + `{additive_measure _ -> _}` -> `{content _ -> _}` - + `isAdditiveMeasure` -> `isContent` - + `AdditiveMeasure` -> `Content` - + `additive_measure` -> `content` - + `additive_measure_snum_subproof` -> `content_snum_subproof` - + `additive_measure_snum` -> `content_snum` - + `SigmaFiniteAdditiveMeasure` -> `SigmaFiniteContent` - + `sigma_finite_additive_measure` -> `sigma_finite_content` - + `{sigma_finite_additive_measure _ -> _}` -> `{sigma_finite_content _ -> _}` -- in `constructive_ereal.v`: - + `fin_num_adde_def` -> `fin_num_adde_defl` - + `oppeD` -> `fin_num_oppeD` - + `oppeB` -> `fin_num_oppeB` - + `doppeD` -> `fin_num_doppeD` - + `doppeB` -> `fin_num_doppeB` -- in `topology.v`: - + `finSubCover` -> `finite_subset_cover` -- in `sequences.v`: - + `eq_eseries` -> `eq_eseriesr` -- in `esum.v`: - + `summable_nneseries_esum` -> `summable_eseries_esum` - + `summable_nneseries` -> `summable_eseries` - ### Generalized -- in `esum.v`: - + lemma `esum_esum` -- in `measure.v` - + lemma `measurable_fun_comp` -- in `lebesgue_integral.v`: - + lemma `measurable_sfunP` -- in `measure.v`: - + lemma `measure_bigcup` generalized, -- in `classical_sets.v`: - + `xsection_preimage_snd`, `ysection_preimage_fst` -- in `constructive_ereal.v`: - + `oppeD`, `oppeB` -- in `measure.v`: - + lemma `eq_measure` -- in `lebesgue_integral.v`: - + lemma `integrable_abse` - - + `sigma_finite` generalized from `numFieldType` to `numDomainType` - + `fin_num_fun_sigma_finite` generalized from `measurableType` to `algebraOfSetsType` - ### Deprecated ### Removed -- in `esum.v`: - + lemma `fsbig_esum` - ### Infrastructure ### Misc diff --git a/INSTALL.md b/INSTALL.md index 94240d7fc..9b7880007 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -2,7 +2,7 @@ ## Requirements -- [The Coq Proof Assistant version ≥ 8.13](https://coq.inria.fr) +- [The Coq Proof Assistant version ≥ 8.14](https://coq.inria.fr) - [Mathematical Components version ≥ 1.13.0](https://github.com/math-comp/math-comp) - [Finmap library version ≥ 1.5.1](https://github.com/math-comp/finmap) - [Hierarchy builder version >= 1.2.0](https://github.com/math-comp/hierarchy-builder) @@ -47,7 +47,7 @@ $ opam install coq-mathcomp-analysis ``` To install a precise version, type, say ``` -$ opam install coq-mathcomp-analysis.0.6.0 +$ opam install coq-mathcomp-analysis.0.6.1 ``` 4. Everytime you want to work in this same context, you need to type ```