From f3ec99e7dcd918546a6e7815a5c67cd83a424522 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 27 May 2020 03:20:02 +0900 Subject: [PATCH] changelog for version 0.3.0 --- CHANGELOG.md | 76 +++++++++++++++++++++++++++++++++++++++-- CHANGELOG_UNRELEASED.md | 70 ------------------------------------- 2 files changed, 74 insertions(+), 72 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0f1af3f97..92de485e8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,17 +1,89 @@ # Changelog -## [0.3.0] - 2020-05-?? +Last release: [[0.3.0] - 2020-05-26](#030---2020-05-26) -This release is compatible with MathComp version 1.11.0+beta1 +## [0.3.0] - 2020-05-26 + +This release is compatible with MathComp version 1.11.0+beta1. + +The biggest change of this release is compatibility with MathComp +1.11.0. The latter introduces in particular ordered types. The +notation for the norm is now uniform. ### Added +- `sequences.v`: Main theorems about sequences and series, and examples + + Definitions: + * `[sequence E]_n` is a special notation for `fun n => E` + * `series u_` is the sequence of partial sums + * `[normed S]` is the series of absolute values, if S is a series + * `harmonic` is the name of a sequence, + apply `series` to them to get the series. + + Theorems: + * lots of helper lemmas to prove convergence of sequences + * convergence of harmonic sequence + * convergence of a series implies convergence of a sequence + * absolute convergence implies convergence of series +- in `ereal.v`: lemmas about extended reals' arithmetic +- in `normedtype.v`: Definitions and lemmas about generic domination, + boundedness, and lipschitz + + See header for the notations and their localization + + Added a bunch of combinators to extract existential witnesses + + Added `filter_forall` (commutation between a filter and finite forall) +- about extended reals: + + equip extended reals with a structure of topological space + + show that extended reals are hausdorff +- in `topology.v`, predicate `close` +- lemmas about bigmaxr and argmaxr + + `\big[max/x]_P F = F [arg max_P F]` + + similar lemma for `bigmin` +- lemmas for `within` +- add `setICl` (intersection of set with its complement) +- `prodnormedzmodule.v` + + `ProdNormedZmodule` transfered from MathComp + + `nonneg` type for non-negative numbers +- `bigmaxr`/`bigminr` library +- Lemmas `interiorI`, `setCU` (complement of union is intersection of complements), + `setICl`, `nonsubset`, `setC0`, `setCK`, `setCT`, `preimage_setI/U`, lemmas about `image` + ### Changed +- in `Rstruct.v`, `bigmaxr` is now defined using `bigop` +- `inE` now supports `in_setE` and `in_fsetE` +- fix the definition of `le_ereal`, `lt_ereal` +- various generalizations to better use the hierarchy of `ssrnum` (`numDomainType`, + `numFieldType`, `realDomainType`, etc. when possible) in `topology.v`, + `normedtype.v`, `derive.v`, etc. + ### Renamed +- renaming `flim` to `cvg` + + `cvg` corresponds to `_ --> _` + + `lim` corresponds to `lim _` + + `continuous` corresponds to continuity + + some suffixes `_opp`, `_add` ... renamed to `N`, `D`, ... +- big refactoring about naming conventions + + complete the theory of `cvg_`, `is_cvg_` and `lim_` in normedtype.v + with consistent naming schemes + + fixed differential of `inv` which was defined on `1 / x` instead of `x^-1` + + two versions of lemmas on inverse exist + * one in realType (`Rinv_` lemmas), for which we have differential + * a general one `numFieldType` (`inv_` lemmas in normedtype.v, no differential so far, just continuity) + + renamed `cvg_norm` to `cvg_dist` to reuse the name `cvg_norm` for + convergence under the norm +- `Uniform` renamed to `PseudoMetric` +- rename `is_prop` to `is_subset1` + ### Removed +- `sub_trans` (replaced by MathComp's `subrKA`) +- `derive.v` does not require `Reals` anymore +- `Rbar.v` is almost not used anymore + ### Infrastructure +- NIX support + + see `config.nix`, `default.nix` + + for the CI also + ### Misc diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 00c863496..c1ee5bdc8 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -2,84 +2,14 @@ ## [Unreleased] -The biggest change of this release is compatibility with MathComp -1.11.0. The latter introduces in particular ordered types. The -notation for the norm is now uniform. - ### Added -- `sequences.v`: Main theorems about sequences and series, and examples - + Definitions: - * `[sequence E]_n` is a special notation for `fun n => E` - * `series u_` is the sequence of partial sums - * `[normed S]` is the series of absolute values, if S is a series - * `harmonic` is the name of a sequence, - apply `series` to them to get the series. - + Theorems: - * lots of helper lemmas to prove convergence of sequences - * convergence of harmonic sequence - * convergence of a series implies convergence of a sequence - * absolute convergence implies convergence of series -- in `ereal.v`: lemmas about extended reals' arithmetic -- in `normedtype.v`: Definitions and lemmas about generic domination, - boundedness, and lipschitz - + See header for the notations and their localization - + Added a bunch of combinators to extract existential witnesses - + Added `filter_forall` (commutation between a filter and finite forall) -- about extended reals: - + equip extended reals with a structure of topological space - + show that extended reals are hausdorff -- in `topology.v`, predicate `close` -- lemmas about bigmaxr and argmaxr - + `\big[max/x]_P F = F [arg max_P F]` - + similar lemma for `bigmin` -- lemmas for `within` -- add `setICl` (intersection of set with its complement) -- `prodnormedzmodule.v` - + `ProdNormedZmodule` transfered from MathComp - + `nonneg` type for non-negative numbers -- `bigmaxr`/`bigminr` library -- Lemmas `interiorI`, `setCU` (complement of union is intersection of complements), - `setICl`, `nonsubset`, `setC0`, `setCK`, `setCT`, `preimage_setI/U`, lemmas about `image` - ### Changed -- in `Rstruct.v`, `bigmaxr` is now defined using `bigop` -- `inE` now supports `in_setE` and `in_fsetE` -- fix the definition of `le_ereal`, `lt_ereal` -- various generalizations to better use the hierarchy of `ssrnum` (`numDomainType`, - `numFieldType`, `realDomainType`, etc. when possible) in `topology.v`, - `normedtype.v`, `derive.v`, etc. - ### Renamed -- renaming `flim` to `cvg` - + `cvg` corresponds to `_ --> _` - + `lim` corresponds to `lim _` - + `continuous` corresponds to continuity - + some suffixes `_opp`, `_add` ... renamed to `N`, `D`, ... -- big refactoring about naming conventions - + complete the theory of `cvg_`, `is_cvg_` and `lim_` in normedtype.v - with consistent naming schemes - + fixed differential of `inv` which was defined on `1 / x` instead of `x^-1` - + two versions of lemmas on inverse exist - * one in realType (`Rinv_` lemmas), for which we have differential - * a general one `numFieldType` (`inv_` lemmas in normedtype.v, no differential so far, just continuity) - + renamed `cvg_norm` to `cvg_dist` to reuse the name `cvg_norm` for - convergence under the norm -- `Uniform` renamed to `PseudoMetric` -- rename `is_prop` to `is_subset1` - ### Removed -- `sub_trans` (replaced by MathComp's `subrKA`) -- `derive.v` does not require `Reals` anymore -- `Rbar.v` is almost not used anymore - ### Infrastructure -- NIX support - + see `config.nix`, `default.nix` - + for the CI also - ### Misc