diff --git a/CHANGELOG.md b/CHANGELOG.md index 8b6fb90ff..1ab785a8f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,99 @@ # Changelog -Lastest releases: [[0.6.4] - 2023-08-05](#064---2023-08-05) and [[0.6.3] - 2023-06-21](#063---2023-06-21) +Lastest releases: [[0.6.5] - 2023-10-02](#065---2023-10-02) and [[0.6.4] - 2023-08-05](#064---2023-08-05) + +## [0.6.5] - 2023-10-02 + +### Added + +- in `mathcomp_extra.v`: + + lemmas `le_bigmax_seq`, `bigmax_sup_seq` + + lemma `gerBl` +- in `classical_sets.v`: + + lemma `setU_id2r` +- in `ereal.v`: + + lemmas `uboundT`, `supremumsT`, `supremumT`, `ereal_supT`, `range_oppe`, + `ereal_infT` +- in `constructive_ereal.v`: + + lemma `eqe_pdivr_mull` + + lemma `bigmaxe_fin_num` +- in file `topology.v`, + + new definition `regular_space`. + + new lemma `ent_closure`. +- in `normedtype.v`: + + lemmas `open_itvoo_subset`, `open_itvcc_subset` + + new lemmas `normal_openP`, `uniform_regular`, + `regular_openP`, and `pseudometric_normal`. +- in `sequences.v`: + + lemma `cvge_harmonic` +- in `convex.v`: + + lemmas `conv_gt0`, `convRE` + + definition `convex_function` +- in `exp.v`: + + lemmas `concave_ln`, `conjugate_powR` + + lemmas `ln_le0`, `ger_powR`, `ler1_powR`, `le1r_powR`, `ger1_powR`, + `ge1r_powR`, `ge1r_powRZ`, `le1r_powRZ` + + lemma `gt0_ltr_powR` + + lemma `powR_injective` +- in `measure.v`: + + lemmas `outer_measure_subadditive`, `outer_measureU2` + + definition `ess_sup`, lemma `ess_sup_ge0` +- in `lebesgue_measure.v`: + + lemma `compact_measurable` + + declare `lebesgue_measure` as a `SigmaFinite` instance + + lemma `lebesgue_regularity_inner_sup` + + lemma `measurable_ball` + + lemma `measurable_mulrr` +- in `lebesgue_integral.v`, + + new lemmas `integral_le_bound`, `continuous_compact_integrable`, and + `lebesgue_differentiation_continuous`. + + new lemmas `simple_bounded`, `measurable_bounded_integrable`, + `compact_finite_measure`, `approximation_continuous_integrable` + + lemma `ge0_integral_count` +- in `kernel.v`: + + `kseries` is now an instance of `Kernel_isSFinite_subdef` +- new file `hoelder.v`: + + definition `Lnorm`, notations `'N[mu]_p[f]`, `'N_p[f]` + + lemmas `Lnorm1`, `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0` + + lemma `hoelder` + + lemmas `Lnorm_counting`, `hoelder2`, `convex_powR` + +### Changed + +- in `cardinality.v`: + + implicits of `fimfunP` +- in `constructive_ereal.v`: + + `lee_adde` renamed to `lee_addgt0Pr` and turned into a reflect + + `lee_dadde` renamed to `lee_daddgt0Pr` and turned into a reflect +- in `exp.v`: + + `gt0_ler_powR` now uses `Num.nneg` +- removed dependency in `Rstruct.v` on `normedtype.v`: +- added dependency in `normedtype.v` on `Rstruct.v`: +- `mnormalize` moved from `kernel.v` to `measure.v` and generalized +- in `measure.v`: + + implicits of `measurable_fst` and `measurable_snd` +- in `lebesgue_integral.v` + + rewrote `negligible_integral` to replace the positivity condition + with an integrability condition, and added `ge0_negligible_integral`. + + implicits of `integral_le_bound` + +### Renamed + +- in `constructive_ereal.v`: + + `lee_opp` -> `leeN2` + + `lte_opp` -> `lteN2` +- in `normedtype.v`: + + `normal_urysohnP` -> `normal_separatorP`. +- in `exp.v`: + + `gt0_ler_powR` -> `ge0_ler_powR` + +### Removed + +- in `signed.v`: + + specific notation for `2%:R`, + now subsumed by number notations in MC >= 1.15 + Note that when importing ssrint, `2` now denotes `2%:~R` rather than `2%:R`, + which are convertible but don't have the same head constant. ## [0.6.4] - 2023-08-05 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 3aacf7fb5..67bb43c3b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,138 +4,16 @@ ### Added -- in `kernel.v`: - + `kseries` is now an instance of `Kernel_isSFinite_subdef` -- in `classical_sets.v`: - + lemma `setU_id2r` -- in `lebesgue_measure.v`: - + lemma `compact_measurable` - -- in `measure.v`: - + lemmas `outer_measure_subadditive`, `outer_measureU2` - -- in `lebesgue_measure.v`: - + declare `lebesgue_measure` as a `SigmaFinite` instance - + lemma `lebesgue_regularity_inner_sup` -- in `convex.v`: - + lemmas `conv_gt0`, `convRE` - -- in `exp.v`: - + lemmas `concave_ln`, `conjugate_powR` - -- in file `lebesgue_integral.v`, - + new lemmas `integral_le_bound`, `continuous_compact_integrable`, and - `lebesgue_differentiation_continuous`. - -- in `normedtype.v`: - + lemmas `open_itvoo_subset`, `open_itvcc_subset` - -- in `lebesgue_measure.v`: - + lemma `measurable_ball` - -- in file `normedtype.v`, - + new lemmas `normal_openP`, `uniform_regular`, - `regular_openP`, and `pseudometric_normal`. -- in file `topology.v`, - + new definition `regular_space`. - + new lemma `ent_closure`. - -- in `lebesgue_measure.v`: - + lemma `measurable_mulrr` - -- in `constructive_ereal.v`: - + lemma `eqe_pdivr_mull` - -- new file `hoelder.v`: - + definition `Lnorm`, notations `'N[mu]_p[f]`, `'N_p[f]` - + lemmas `Lnorm1`, `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0` - + lemma `hoelder` - -- in file `lebesgue_integral.v`, - + new lemmas `simple_bounded`, `measurable_bounded_integrable`, - `compact_finite_measure`, `approximation_continuous_integrable` - -- in `sequences.v`: - + lemma `cvge_harmonic` - -- in `mathcomp_extra.v`: - + lemmas `le_bigmax_seq`, `bigmax_sup_seq` - -- in `constructive_ereal.v`: - + lemma `bigmaxe_fin_num` -- in `ereal.v`: - + lemmas `uboundT`, `supremumsT`, `supremumT`, `ereal_supT`, `range_oppe`, - `ereal_infT` - -- in `measure.v`: - + definition `ess_sup`, lemma `ess_sup_ge0` -- in `convex.v`: - + definition `convex_function` - -- in `exp.v`: - + lemmas `ln_le0`, `ger_powR`, `ler1_powR`, `le1r_powR`, `ger1_powR`, - `ge1r_powR`, `ge1r_powRZ`, `le1r_powRZ` - -- in `hoelder.v`: - + lemmas `Lnorm_counting`, `hoelder2`, `convex_powR` - -- in `lebesgue_integral.v`: - + lemma `ge0_integral_count` - -- in `exp.v`: - + lemma `gt0_ltr_powR` - + lemma `powR_injective` -- in `mathcomp_extra.v`: - + lemma `gerBl` - ### Changed -- `mnormalize` moved from `kernel.v` to `measure.v` and generalized -- in `constructive_ereal.v`: - + `lee_adde` renamed to `lee_addgt0Pr` and turned into a reflect - + `lee_dadde` renamed to `lee_daddgt0Pr` and turned into a reflect -- in `lebesgue_integral.v` - + rewrote `negligible_integral` to replace the positivity condition - with an integrability condition, and added `ge0_negligible_integral`. - -- removed dependency in `Rstruct.v` on `normedtype.v`: -- added dependency in `normedtype.v` on `Rstruct.v`: - -- in `cardinality.v`: - + implicits of `fimfunP` - -- in `lebesgue_integral.v`: - + implicits of `integral_le_bound` - -- in `measure.v`: - + implicits of `measurable_fst` and `measurable_snd` -- in `exp.v`: - + `gt0_ler_powR` now uses `Num.nneg` - ### Renamed -- in `normedtype.v`: - + `normal_urysohnP` -> `normal_separatorP`. - -- in `constructive_ereal.v`: - + `lee_opp` -> `leeN2` - + `lte_opp` -> `lteN2` - -- in `exp.v`: - + `gt0_ler_powR` -> `ge0_ler_powR` - ### Generalized ### Deprecated ### Removed -- in `signed.v`: - + specific notation for `2%:R`, - now subsumed by number notations in MC >= 1.15 - Note that when importing ssrint, `2` now denotes `2%:~R` rather than `2%:R`, - which are convertible but don't have the same head constant. - ### Infrastructure ### Misc diff --git a/INSTALL.md b/INSTALL.md index 96a381c80..618c3c470 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.4 +$ opam install coq-mathcomp-analysis.0.6.5 ``` 4. Everytime you want to work in this same context, you need to type ```