From 051e90db8cabc905ffdb87a68de6e8ff0943e755 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 24 Sep 2024 15:06:16 +0900 Subject: [PATCH] changelog for version 1.4.0 --- CHANGELOG.md | 193 +++++++++++++++++++++++++++++++++++++++- CHANGELOG_UNRELEASED.md | 188 -------------------------------------- INSTALL.md | 2 +- README.md | 5 +- 4 files changed, 196 insertions(+), 192 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 77e7ac33c..259e4240c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,197 @@ # Changelog -Latest releases: [[1.3.1] - 2024-08-09](#131---2024-08-09) and [[1.3.0] - 2024-08-06](#130---2024-08-06) +Latest releases: [[1.4.0] - 2024-09-24](#140---2024-09-24) and [[1.3.1] - 2024-08-09](#131---2024-08-09) + +## [1.4.0] - 2024-09-24 + +### Added + +- in `mathcomp_extra.v`: + + lemmas `invf_ple`, `invf_lep` + +- in `classical_sets.v`: + + scope `relation_scope` with delimiter `relation` + + notation `^-1` in `relation_scope` (used to be a local notation) + + lemma `set_prod_invK` (was a local lemma in `normedtype.v`) + + definition `diagonal`, lemma `diagonalP` + +- in `functions.v`: + + lemmas `mul_funC` + +- in `set_interval.v`: + + lemma `subset_itvSoo` + + new definitions `itv_is_ray`, `itv_is_bd_open`, and `itv_open_ends` + + new lemmas `itv_open_ends_rside`, `itv_open_ends_rinfty`, + `itv_open_ends_lside`, `itv_open_ends_linfty`, + `is_open_itv_itv_is_bd_openP`, `itv_open_endsI`, `itv_setU`, + `itv_setI` + +- in `topology.v`: + + lemma `filterN` + + Structures `PointedFiltered`, `PointedNbhs`, `PointedUniform`, + `PseudoPointedMetric` + + new definition `order_topology` + + new lemmas `discrete_nat`, `rray_open`, `lray_open`, `itv_open`, + `itv_open_ends_open`, `rray_closed`, `lray_closed`, `itv_closed`, + `itv_closure`, `itv_closed_infimums`, `itv_closed_supremums`, + `order_hausdorff`, `clopen_bigcup_clopen`, `zero_dimensional_ray`, + `order_nbhs_itv`, `open_order_weak`, `real_order_nbhsE` + +- in `normedtype.v`: + + lemmas `not_near_inftyP`, `not_near_ninftyP` + + lemma `ninftyN` + + lemma `le_closed_ball` + + lemmas `nbhs_right_ltW`, `cvg_patch` + +- in `derive.v`: + + lemma `derive_id` + + lemmas `exp_derive`, `exp_derive1` + + lemma `derive_cst` + + lemma `deriveMr`, `deriveMl` + +- in `sequences.v`: + + lemma `cvg_geometric_eseries_half` + + theorem `Baire` + + definition `bounded_fun_norm` + + lemma `bounded_landau` + + definition `pointwise_bounded` + + definition `uniform_bounded` + + theorem `Banach_Steinhauss` + +- in `numfun.v`: + + lemma `indicI` + +- in `measure.v`: + + lemma `measurable_neg`, `measurable_or` + +- in `lebesgue_measure.v`: + + definitions `is_open_itv`, `open_itv_cover` + + lemmas `outer_measure_open_itv_cover`, `outer_measure_open_le`, + `outer_measure_open`, `outer_measure_Gdelta`, `negligible_outer_measure` + + lemmas `measurable_fun_eqr`, `measurable_fun_indic`, `measurable_fun_dirac`, + `measurable_fun_addn`, `measurable_fun_maxn`, `measurable_fun_subn`, + `measurable_fun_ltn`, `measurable_fun_leq`, `measurable_fun_eqn` + + module `NGenCInfty` + * definition `G` + * lemmas `measurable_itv_bounded`, `measurableE` + +- in `lebesgue_integral.v`: + + lemma `integralZr` + + lemma `locally_integrableS` + + lemma `integrable_locally_restrict` + + lemma `near_davg` + + lemma `lebesgue_pt_restrict` + +- in `ftc.v`: + + lemmas `integration_by_parts`, `Rintegration_by_parts` + + corollary `continuous_FTC1_closed` + +### Changed + +- in `topology.v`: + + removed the pointed assumptions from `FilteredType`, `Nbhs`, + `TopologicalType`, `UniformType`, and `PseudoMetricType`. + + if you want the original pointed behavior, use the `p` variants + of the types, so `ptopologicalType` instead of `topologicalType`. + + generalized most lemmas to no longer depend on pointedness. + The main exception is for references to `cvg` and `lim` that depend + on `get` for their definition. + + `pointed_principal_filter` becomes `principle_filter_type` and + requires only `choiceType` instead of `pointedType` + + `pointed_discrete_topology` becomes `discrete_topology_type` and + requires only `choiceType` instead of `pointedType` + + renamed lemma `discrete_pointed`to `discrete_space_discrete` + +- in `function_space.v`: + + generalized most lemmas to no longer depend on pointedness. + +- in `normedtype.v`: + + remove superflous parameters in lemmas `not_near_at_rightP` and `not_near_at_leftP` + + lemma `continuous_within_itvP`: change the statement to use the notation `[/\ _, _ & _]` + +- moved from `numfun.v` to `cardinality.v`: + + lemma `fset_set_comp` + +- moved `summability.v` from `theories` to `theories/showcase` + +- in `lebesgue_measure.v`: + + remove redundant hypothesis from lemma `pointwise_almost_uniform` + +- moved from `lebesgue_measure.v` to `set_interval.v`: `is_open_itv`, and + `open_itv_cover` + +- in `lebesgue_integral.v`: + + lemma `nice_lebesgue_differentiation`: change the local integrability hypothesis to + easy application + +- in `ftc.v`: + + lemma `FTC1_lebesgue_pt`, corollaries `FTC1`, `FTC1Ny`: integrability hypothesis weakened + +### Renamed + +- in `set_interval.v`: + + `subset_itvS` -> `subset_itvScc` + +- in `topology.v`: + + in mixin `Nbhs_isUniform_mixin`: + * `entourage_refl_subproof` -> `entourage_diagonal_subproof` + + in factory `Nbhs_isUniform`: + * `entourage_refl` -> `entourage_diagonal` + + in factory `isUniform`: + * `entourage_refl` -> `entourage_diagonal` + +- in `lebesgue_measure.v`: + + `measurable_exprn` -> `exprn_measurable` + + `measurable_mulrl` -> `mulrl_measurable` + + `measurable_mulrr` -> `mulrr_measurable` + + `measurable_fun_pow` -> `measurable_funX` + + `measurable_oppe` -> `oppe_measurable` + + `measurable_abse` -> `abse_measurable` + + `measurable_EFin` -> `EFin_measurable` + + `measurable_oppr` -> `oppr_measurable` + + `measurable_normr` -> `normr_measurable` + + `measurable_fine` -> `fine_measurable` + + `measurable_natmul` -> `natmul_measurable` + +- in `lebesgue_integral.v` + + lemma `integrable_locally` -> `open_integrable_locally` + +### Generalized + +- in `derive.v`: + + lemma `derivable_cst` + +- in `lebesgue_measure.v`: + + lemma `measurable_funX` (was `measurable_fun_pow`) + +- in `lebesgue_integral.v` + + lemma `ge0_integral_closed_ball` + +- in `ftc.v`: + + lemma `continuous_FTC2` (continuity hypothesis weakened) + +### Removed + +- in `lebesgue_measure.v`: + + notation `measurable_fun_sqr` (was deprecated since 0.6.3) + + notation `measurable_fun_exprn` (was deprecated since 0.6.3) + + notation `measurable_funrM` (was deprecated since 0.6.3) + + notation `emeasurable_fun_minus` (was deprecated since 0.6.3) + + notation `measurable_fun_abse` (was deprecated since 0.6.3) + + notation `measurable_fun_EFin` (was deprecated since 0.6.3) + + notation `measurable_funN` (was deprecated since 0.6.3) + + notation `measurable_fun_opp` (was deprecated since 0.6.3) + + notation `measurable_fun_normr` (was deprecated since 0.6.3) + + notation `measurable_fun_fine` (was deprecated since 0.6.3) +- in `topology.v`: + + turned into Let's (inside `HB.builders`): + * lemmas `nbhsE_subproof`, `openE_subproof` + * lemmas `nbhs_pfilter_subproof`, `nbhsE_subproof`, `openE_subproof` + * lemmas `open_fromT`, `open_fromI`, `open_from_bigU` + * lemmas `finI_from_cover`, `finI_from_join` + * lemmas `nbhs_filter`, `nbhs_singleton`, `nbhs_nbhs` + * lemmas `ball_le`, `entourage_filter_subproof`, `ball_sym_subproof`, + `ball_triangle_subproof`, `entourageE_subproof` ## [1.3.1] - 2024-08-09 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2e6c35ed6..67bb43c3b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -3,205 +3,17 @@ ## [Unreleased] ### Added -- in `normedtype.v`: - + lemmas `not_near_inftyP`, `not_near_ninftyP` - -- in `topology.v`: - + lemma `filterN` - -- in `normedtype.v`: - + lemma `ninftyN` - -- in `derive.v`: - + lemma `derive_id` - + lemmas `exp_derive`, `exp_derive1` - + lemma `derive_cst` - + lemma `deriveMr`, `deriveMl` - -- in `functions.v`: - + lemmas `mul_funC` -- in `sequences.v`: - + lemma `cvg_geometric_eseries_half` - -- in `lebesgue_measure.v`: - + definitions `is_open_itv`, `open_itv_cover` - + lemmas `outer_measure_open_itv_cover`, `outer_measure_open_le`, - `outer_measure_open`, `outer_measure_Gdelta`, `negligible_outer_measure` -- in `ftc.v`: - + lemmas `integration_by_parts`, `Rintegration_by_parts` - -- in `classical_sets.v`: - + scope `relation_scope` with delimiter `relation` - + notation `^-1` in `relation_scope` (use to be a local notation) - + lemma `set_prod_invK` (was a local lemma in `normedtype.v`) - + definition `diagonal`, lemma `diagonalP` -- in `mathcomp_extra.v`: - + lemmas `invf_ple`, `invf_lep` - -- in `lebesgue_integral.v`: - + lemma `integralZr` - -- in `normedtype.v`: - + lemma `le_closed_ball` -- in `sequences.v`: - + theorem `Baire` - + definition `bounded_fun_norm` - + lemma `bounded_landau` - + definition `pointwise_bounded` - + definition `uniform_bounded` - + theorem `Banach_Steinhauss` - -- in `topology.v`: - + Structures `PointedFiltered`, `PointedNbhs`, `PointedUniform`, - `PseudoPointedMetric` -- in `measure.v`: - + lemma `measurable_neg`, `measurable_or` - -- in `lebesgue_measure.v`: - + lemmas `measurable_fun_eqr`, `measurable_fun_indic`, `measurable_fun_dirac`, - `measurable_fun_addn`, `measurable_fun_maxn`, `measurable_fun_subn`, `measurable_fun_ltn`, - `measurable_fun_leq`, `measurable_fun_eqn` - + module `NGenCInfty` - * definition `G` - * lemmas `measurable_itv_bounded`, `measurableE` -- in `continuous_FTC1_closed`: - + corollary `continuous_FTC1_closed` - -- in `lebesgue_integral.v`: - + lemma `locally_integrableS` - -- in `normedtype.v`: - + lemmas `nbhs_right_ltW`, `cvg_patch` - -- in `set_interval.v`: - + lemma `subset_itvSoo` - -- in `lebesgue_integral.v`: - + lemma `integrable_locally_restrict` - + lemma `near_davg` - + lemma `lebesgue_pt_restrict` -- in file `set_interval.v`, - + new definitions `itv_is_ray`, `itv_is_bd_open`, and `itv_open_ends`. - + new lemmas `itv_open_ends_rside`, `itv_open_ends_rinfty`, - `itv_open_ends_lside`, `itv_open_ends_linfty`, - `is_open_itv_itv_is_bd_openP`, `itv_open_endsI`, `itv_setU`, and - `itv_setI`. -- in file `topology.v`, - + new definition `order_topology`. - + new lemmas `discrete_nat`, `rray_open`, `lray_open`, `itv_open`, - `itv_open_ends_open`, `rray_closed`, `lray_closed`, `itv_closed`, - `itv_closure`, `itv_closed_infimums`, `itv_closed_supremums`, - `order_hausdorff`, `clopen_bigcup_clopen`, `zero_dimensional_ray`, - `order_nbhs_itv`, `open_order_weak`, and `real_order_nbhsE`. - -- in `numfun.v`: - + lemma `indicI` ### Changed -- in `topology.v`: - + removed the pointed assumptions from `FilteredType`, `Nbhs`, - `TopologicalType`, `UniformType`, and `PseudoMetricType`. - + if you want the original pointed behavior, use the `p` variants - of the types, so `ptopologicalType` instead of `topologicalType`. - + generalized most lemmas to no longer depend on pointedness. - The main exception is for references to `cvg` and `lim` that depend - on `get` for their definition. - + `pointed_principal_filter` becomes `principle_filter_type` and - requires only `choiceType` instead of `pointedType` - + `pointed_discrete_topology` becomes `discrete_topology_type` and - requires only `choiceType` instead of `pointedType` - + renamed lemma `discrete_pointed`to `discrete_space_discrete` -- in `function_space.v`: - + generalized most lemmas to no longer depend on pointedness. -- in `normedtype.v`: - + remove superflous parameters in lemmas `not_near_at_rightP` and `not_near_at_leftP` - -- in `lebesgue_measure.v`: - + remove redundant hypothesis from lemma `pointwise_almost_uniform` - -- moved from `numfun.v` to `cardinality.v`: - + lemma `fset_set_comp` -- in `ftc.v`: - + lemma `FTC1_lebesgue_pt`, corollaries `FTC1`, `FTC1Ny`: integrability hypothesis weakened - -- in `lebesgue_integral.v`: - + lemma `nice_lebesgue_differentiation`: change the local integrability hypothesis to easy application - -- in `normedtype.v`: - + lemma `continuous_within_itvP`: change the statement to use the notation `[/\ _, _ & _]` - -- moved from `lebesgue_measure.v` to `set_interval.v`: `is_open_itv`, and - `open_itv_cover` - -- moved `summability.v` from `theories` to `theories/showcase` ### Renamed -- in `lebesgue_measure.v`: - + `measurable_exprn` -> `exprn_measurable` - + `measurable_mulrl` -> `mulrl_measurable` - + `measurable_mulrr` -> `mulrr_measurable` - + `measurable_fun_pow` -> `measurable_funX` - + `measurable_oppe` -> `oppe_measurable` - + `measurable_abse` -> `abse_measurable` - + `measurable_EFin` -> `EFin_measurable` - + `measurable_oppr` -> `oppr_measurable` - + `measurable_normr` -> `normr_measurable` - + `measurable_fine` -> `fine_measurable` - + `measurable_natmul` -> `natmul_measurable` -- in `topology.v`: - + in mixin `Nbhs_isUniform_mixin`: - * `entourage_refl_subproof` -> `entourage_diagonal_subproof` - + in factory `Nbhs_isUniform`: - * `entourage_refl` -> `entourage_diagonal` - + in factory `isUniform`: - * `entourage_refl` -> `entourage_diagonal` - -- in `set_interval.v`: - + `subset_itvS` -> `subset_itvScc` - -- in `lebesgue_integral.v` - + lemma `integrable_locally` -> `open_integrable_locally` - ### Generalized -- in `derive.v`: - + lemma `derivable_cst` - -- in `lebesgue_measure.v`: - + lemma `measurable_funX` (was `measurable_fun_pow`) - -- in `lebesgue_integral.v` - + lemma `ge0_integral_closed_ball` - -- in `FTC.v`: - + lemma `continuous_FTC2` (continuity hypothesis weakened) - ### Deprecated ### Removed -- in `lebesgue_measure.v`: - + notation `measurable_fun_sqr` (was deprecated since 0.6.3) - + notation `measurable_fun_exprn` (was deprecated since 0.6.3) - + notation `measurable_funrM` (was deprecated since 0.6.3) - + notation `emeasurable_fun_minus` (was deprecated since 0.6.3) - + notation `measurable_fun_abse` (was deprecated since 0.6.3) - + notation `measurable_fun_EFin` (was deprecated since 0.6.3) - + notation `measurable_funN` (was deprecated since 0.6.3) - + notation `measurable_fun_opp` (was deprecated since 0.6.3) - + notation `measurable_fun_normr` (was deprecated since 0.6.3) - + notation `measurable_fun_fine` (was deprecated since 0.6.3) -- in `topology.v`: - + turned into Let's (inside `HB.builders`): - * lemmas `nbhsE_subproof`, `openE_subproof` - * lemmas `nbhs_pfilter_subproof`, `nbhsE_subproof`, `openE_subproof` - * lemmas `open_fromT`, `open_fromI`, `open_from_bigU` - * lemmas `finI_from_cover`, `finI_from_join` - * lemmas `nbhs_filter`, `nbhs_singleton`, `nbhs_nbhs` - * lemmas `ball_le`, `entourage_filter_subproof`, `ball_sym_subproof`, - `ball_triangle_subproof`, `entourageE_subproof` - ### Infrastructure ### Misc diff --git a/INSTALL.md b/INSTALL.md index 24afb8e88..01a19bf45 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.3.1 +$ opam install coq-mathcomp-analysis.1.4.0 ``` 4. Everytime you want to work in this same context, you need to type ``` diff --git a/README.md b/README.md index d3876044b..0114382fa 100644 --- a/README.md +++ b/README.md @@ -82,8 +82,9 @@ We try to preserve backward compatibility as best as we can. ## Documentation -Each file is documented in its header -([documentation for the last version](https://math-comp.github.io/analysis/htmldoc_1_3_1/index.html), using [`coq2html`](https://github.com/xavierleroy/coq2html)). +Each file is documented in its header in ASCII. + +[HTML rendering of the source code](https://math-comp.github.io/analysis/htmldoc_1_4_0/index.html) (using [`coq2html`](https://github.com/xavierleroy/coq2html)). Overview presentations: - [Classical Analysis with Coq](https://perso.crans.org/cohen/CoqWS2018.pdf) (2018)