diff --git a/CHANGELOG.md b/CHANGELOG.md index a56942f52..a3c8a618e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,165 @@ # Changelog -Latest releases: [[1.0.0] - 2024-01-26](#100---2024-01-26) and [[0.7.0] - 2024-01-19](#070---2024-01-19) +Latest releases: [[1.1.0] - 2024-03-31](#110---2024-03-31) and [[1.0.0] - 2024-01-26](#100---2024-01-26) + +## [1.1.0] - 2024-03-31 + +### Added + +- in `mathcomp_extra.v` + + lemma `invf_plt` + +- in `contra.v`: + + in module `Internals` + * variant `equivT` + * definitions `equivT_refl`, `equivT_transl`, `equivT_sym`, `equivT_trans`, + `equivT_transr`, `equivT_Prop`, `equivT_LR` (hint view), `equivT_RL` (hint view) + + definition `notP` + + hint view for `move/` and `apply/` for `Internals.equivT_LR`, `Internals.equivT_RL` + +- in `set_interval.v` + + lemmas `setDitv1r`, `setDitv1l` + + lemmas `set_itvxx`, `itv_bndbnd_setU` + +- in `reals.v` + + lemma `abs_ceil_ge` + +- in `topology.v`: + + lemmas `nbhs_infty_ger`, `nbhs0_ltW`, `nbhs0_lt` + +- file `function_spaces.v` + +- in `normedtype.v` + + lemma `closed_ball_ball` + + lemma `ball_open_nbhs` + + new definition `completely_regular_space`. + + new lemmas `point_uniform_separator`, and + `uniform_completely_regular`. + +- in `exp.v` + + lemma `ln_lt0` + + lemma `expRM_natr` + +- in `numfun.v` + + lemma `cvg_indic` + +- in `lebesgue_integral.v` + + lemma `ge0_integralZr` + + lemma `locally_integrable_indic` + + definition `davg`, + lemmas `davg0`, `davg_ge0`, `davgD`, `continuous_cvg_davg` + + definition `lim_sup_davg`, + lemmas `lim_sup_davg_ge0`, `lim_sup_davg_le`, + `continuous_lim_sup_davg`, `lim_sup_davgB`, `lim_sup_davgT_HL_maximal` + + definition `lebesgue_pt`, + lemma `continuous_lebesgue_pt` + + lemma `integral_setU_EFin` + + lemmas `integral_set1`, `ge0_integral_closed_ball`, `integral_setD1_EFin`, + `integral_itv_bndo_bndc`, `integral_itv_obnd_cbnd` + + lemma `lebesgue_differentiation` + + lemma `lebesgue_density` + + definition `nicely_shrinking`, + lemmas `nicely_shrinking_gt0`, `nicely_shrinking_lty`, `nice_lebesgue_differentiation` + +- new file `ftc.v`: + - lemmas `FTC1`, `continuous_FTC1` + +### Changed + +- moved from `topology.v` to `function_spaces.v`: `prod_topology`, + `product_topology_def`, `proj_continuous`, `dfwith_continuous`, + `proj_open`, `hausdorff_product`, `tychonoff`, `perfect_prod`, + `perfect_diagonal`, `zero_dimension_prod`, `totally_disconnected_prod`, + `separate_points_from_closed`, `weak_sep_cvg`, `weak_sep_nbhsE`, + `weak_sep_openE`, `join_product`, `join_product_continuous`, + `join_product_open`, `join_product_inj`, `join_product_weak`, `fct_ent`, + `fct_ent_filter`, `fct_ent_refl`, `fct_ent_inv`, `fct_ent_split`, + `cvg_fct_entourageP`, `fun_complete`, `fct_ball`, `fct_ball_center`, + `fct_ball_sym`, `fct_ball_triangle`, `fct_entourage`, `cvg_switch_1`, + `cvg_switch_2`, `cvg_switch`, `uniform_fun`, `uniform_nbhs`, + `uniform_entourage`, `restricted_cvgE`, `pointwise_cvgE`, + `uniform_fun_family`, `uniform_set1`, `uniform_subset_nbhs`, + `uniform_subset_cvg`, `pointwise_uniform_cvg`, `cvg_sigL`, `eq_in_close`, + `hausdorrf_close_eq_in`, `uniform_restrict_cvg`, `uniform_nbhsT`, + `cvg_uniformU`, `cvg_uniform_set0`, `fam_cvgP`, `family_cvg_subset`, + `family_cvg_finite_covers`, `fam_cvgE`, `fam_nbhs`, `fam_compact_nbhs`, + `compact_open`, `compact_openK`, `compact_openK_nbhs`, + `compact_open_of_nbhs`, `compact_open_def`, `compact_open_cvgP`, + `compact_open_open`, `compact_open_fam_compactP`, `compactly_in`, + `compact_cvg_within_compact`, `uniform_limit_continuous`, + `uniform_limit_continuous_subspace`, `singletons`, + `pointwise_cvg_family_singleton`, `pointwise_cvg_compact_family`, + `pointwise_cvgP`, `equicontinuous`, `equicontinuous_subset`, + `equicontinuous_subset_id`, `equicontinuous_continuous_for`, + `equicontinuous_continuous`, `pointwise_precompact`, + `pointwise_precompact_subset`, `pointwise_precompact_precompact`, + `uniform_pointwise_compact`, `precompact_pointwise_precompact`, + `pointwise_cvg_entourage`, `equicontinuous_closure`, `small_ent_sub`, + `pointwise_compact_cvg`, `pointwise_compact_closure`, + `pointwise_precompact_equicontinuous`, `compact_equicontinuous`, + `precompact_equicontinuous`, `Ascoli`, `continuous_curry`, + `continuous_uncurry_regular`, `continuous_uncurry`, `curry_continuous`, and + `uncurry_continuous`. + +- moved from `cantor.v` to `topology.v`: + + lemma `discrete_bool_compact` + + definition `pointed_principal_filter` + + definition `pointed_discrete_topology` + + lemma `discrete_pointed` + +- in `measure.v`: + + lemma `sigma_finiteP` generalized to an equivalence and changed to use `[/\ ..., .. & ....]` + +- move from `kernel.v` to `measure.v` + + definition `mset`, `pset`, `pprobability` + + lemmas `lt0_mset`, `gt1_mset` + +### Renamed + +- in `constructive_ereal.v`: + + `lee_addl` -> `leeDl` + + `lee_addr` -> `leeDr` + + `lee_add2l` -> `leeD2l` + + `lee_add2r` -> `leeD2r` + + `lee_add` -> `leeD` + + `lee_sub` -> `leeB` + + `lee_add2lE` -> `leeD2lE` + + `lte_add2lE` -> `lteD2lE` + + `lee_oppl` -> `leeNl` + + `lee_oppr` -> `leeNr` + + `lte_oppr` -> `lteNr` + + `lte_oppl` -> `lteNl` + + `lte_add` -> `lteD` + + `lte_addl` -> `lteDl` + + `lte_addr` -> `lteDr` + +- in `exp.v`: + + `expRMm` -> `expRM_natl` + +- in `measure.v`: + + `Measure_isSFinite_subdef` -> `isSFinite` + + `sfinite_measure_subdef` -> `s_finite` + + `SigmaFinite_isFinite` -> `isFinite` + + `FiniteMeasure_isSubProbability` -> `isSubProbability` + +- in `lebesgue_integral.v` + + `integral_setU` -> `ge0_integral_setU` + + `subset_integral` -> `ge0_subset_integral` + +### Generalized + +- in `realfun.v` + + lemma `lime_sup_le` + +### Removed + +- in `topology.v`: + + definition `pointwise_fun` + + module `PtwsFun` + +- in `mathcomp_extra.v`: + + notations `eqLHS` and `eqRHS` + (they are `eqbLHS` and `eqbRHS` in mathcomp since 1.15.0) ## [1.0.0] - 2024-01-26 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e67d62027..67bb43c3b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,168 +4,16 @@ ### Added -- in `exp.v` - + lemma `ln_lt0` - -- in `lebesgue_integral.v` - + lemma `ge0_integralZr` -- file `function_spaces.v` -- in `mathcomp_extra.v` - + lemma `invf_plt` - -- in `set_interval.v` - + lemmas `setDitv1r`, `setDitv1l` - + lemmas `set_itvxx`, `itv_bndbnd_setU` - -- in `reals.v` - + lemma `abs_ceil_ge` - -- in `topology.v`: - + lemmas `nbhs_infty_ger`, `nbhs0_ltW`, `nbhs0_lt` - -- in `normedtype.v` - + lemma `closed_ball_ball` - -- in `numfun.v` - + lemma `cvg_indic` - -- in `lebesgue_integral.v` - + lemma `locally_integrable_indic` - + definition `davg`, - lemmas `davg0`, `davg_ge0`, `davgD`, `continuous_cvg_davg` - + definition `lim_sup_davg`, - lemmas `lim_sup_davg_ge0`, `lim_sup_davg_le`, - `continuous_lim_sup_davg`, `lim_sup_davgB`, `lim_sup_davgT_HL_maximal` - + definition `lebesgue_pt`, - lemma `continuous_lebesgue_pt` - + lemma `integral_setU_EFin` - + lemmas `integral_set1`, `ge0_integral_closed_ball`, `integral_setD1_EFin`, - `integral_itv_bndo_bndc`, `integral_itv_obnd_cbnd` - + lemma `lebesgue_differentiation` - + lemma `lebesgue_density` - + definition `nicely_shrinking`, - lemmas `nicely_shrinking_gt0`, `nicely_shrinking_lty`, `nice_lebesgue_differentiation` - -- in `normedtype.v`: - + lemma `ball_open_nbhs` - -- new file `ftc.v`: - - lemmas `FTC1`, `continuous_FTC1` - -- in file `normedtype.v`, - + new definition `completely_regular_space`. - + new lemmas `point_uniform_separator`, and - `uniform_completely_regular`. - -- in `contra.v`: - + in module `Internals` - * variant `equivT` - * definitions `equivT_refl`, `equivT_transl`, `equivT_sym`, `equivT_trans`, - `equivT_transr`, `equivT_Prop`, `equivT_LR` (hint view), `equivT_RL` (hint view) - + definition `notP` - + hint view for `move/` and `apply/` for `Internals.equivT_LR`, `Internals.equivT_RL` - -- in `exp.v`: - + lemma `expRM_natr` - ### Changed -- moved from `topology.v` to `function_spaces.v`: `prod_topology`, - `product_topology_def`, `proj_continuous`, `dfwith_continuous`, - `proj_open`, `hausdorff_product`, `tychonoff`, `perfect_prod`, - `perfect_diagonal`, `zero_dimension_prod`, `totally_disconnected_prod`, - `separate_points_from_closed`, `weak_sep_cvg`, `weak_sep_nbhsE`, - `weak_sep_openE`, `join_product`, `join_product_continuous`, - `join_product_open`, `join_product_inj`, `join_product_weak`, `fct_ent`, - `fct_ent_filter`, `fct_ent_refl`, `fct_ent_inv`, `fct_ent_split`, - `cvg_fct_entourageP`, `fun_complete`, `fct_ball`, `fct_ball_center`, - `fct_ball_sym`, `fct_ball_triangle`, `fct_entourage`, `cvg_switch_1`, - `cvg_switch_2`, `cvg_switch`, `uniform_fun`, `uniform_nbhs`, - `uniform_entourage`, `restricted_cvgE`, `pointwise_cvgE`, - `uniform_fun_family`, `uniform_set1`, `uniform_subset_nbhs`, - `uniform_subset_cvg`, `pointwise_uniform_cvg`, `cvg_sigL`, `eq_in_close`, - `hausdorrf_close_eq_in`, `uniform_restrict_cvg`, `uniform_nbhsT`, - `cvg_uniformU`, `cvg_uniform_set0`, `fam_cvgP`, `family_cvg_subset`, - `family_cvg_finite_covers`, `fam_cvgE`, `fam_nbhs`, `fam_compact_nbhs`, - `compact_open`, `compact_openK`, `compact_openK_nbhs`, - `compact_open_of_nbhs`, `compact_open_def`, `compact_open_cvgP`, - `compact_open_open`, `compact_open_fam_compactP`, `compactly_in`, - `compact_cvg_within_compact`, `uniform_limit_continuous`, - `uniform_limit_continuous_subspace`, `singletons`, - `pointwise_cvg_family_singleton`, `pointwise_cvg_compact_family`, - `pointwise_cvgP`, `equicontinuous`, `equicontinuous_subset`, - `equicontinuous_subset_id`, `equicontinuous_continuous_for`, - `equicontinuous_continuous`, `pointwise_precompact`, - `pointwise_precompact_subset`, `pointwise_precompact_precompact`, - `uniform_pointwise_compact`, `precompact_pointwise_precompact`, - `pointwise_cvg_entourage`, `equicontinuous_closure`, `small_ent_sub`, - `pointwise_compact_cvg`, `pointwise_compact_closure`, - `pointwise_precompact_equicontinuous`, `compact_equicontinuous`, - `precompact_equicontinuous`, `Ascoli`, `continuous_curry`, - `continuous_uncurry_regular`, `continuous_uncurry`, `curry_continuous`, and - `uncurry_continuous`. - -- move from `kernel.v` to `measure.v` - + definition `mset`, `pset`, `pprobability` - + lemmas `lt0_mset`, `gt1_mset` - -- in `measure.v`: - + lemma `sigma_finiteP` generalized to an equivalence and changed to use `[/\ ..., .. & ....]` - -- moved from `cantor.v` to `topology.v`: - + lemma `discrete_bool_compact` - + definition `pointed_principal_filter` - + definition `pointed_discrete_topology` - + lemma `discrete_pointed` ### Renamed -- in `constructive_ereal.v`: - + `lee_addl` -> `leeDl` - + `lee_addr` -> `leeDr` - + `lee_add2l` -> `leeD2l` - + `lee_add2r` -> `leeD2r` - + `lee_add` -> `leeD` - + `lee_sub` -> `leeB` - + `lee_add2lE` -> `leeD2lE` - + `lte_add2lE` -> `lteD2lE` - + `lee_oppl` -> `leeNl` - + `lee_oppr` -> `leeNr` - + `lte_oppr` -> `lteNr` - + `lte_oppl` -> `lteNl` - + `lte_add` -> `lteD` - + `lte_addl` -> `lteDl` - + `lte_addr` -> `lteDr` - -- in `lebesgue_integral.v` - + `integral_setU` -> `ge0_integral_setU` - + `subset_integral` -> `ge0_subset_integral` - -- in `measure.v`: - + `Measure_isSFinite_subdef` -> `isSFinite` - + `sfinite_measure_subdef` -> `s_finite` - + `SigmaFinite_isFinite` -> `isFinite` - + `FiniteMeasure_isSubProbability` -> `isSubProbability` - -- in `exp.v`: - + `expRMm` -> `expRM_natl` - ### Generalized -- in `realfun.v` - + lemma `lime_sup_le` - ### Deprecated ### Removed -- in `topology.v`: - + definition `pointwise_fun` - + module `PtwsFun` - -- in `mathcomp_extra.v`: - + notations `eqLHS` and `eqRHS` - (they are `eqbLHS` and `eqbRHS` in mathcomp since 1.15.0) - ### Infrastructure ### Misc diff --git a/INSTALL.md b/INSTALL.md index d3b05ba62..157096836 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.0.0 +$ opam install coq-mathcomp-analysis.1.1.0 ``` 4. Everytime you want to work in this same context, you need to type ``` @@ -71,12 +71,12 @@ using [proof general for emacs](https://github.com/ProofGeneral/PG) ## Break-down of phase 3 of the installation procedure step by step -With the example of Coq 8.16.0 and MathComp 2.0.0. For other versions, update the +With the example of Coq 8.18.0 and MathComp 2.0.0. For other versions, update the version numbers accordingly. -1. Install Coq 8.16.0 +1. Install Coq 8.18.0 ``` -$ opam install coq.8.16.0 +$ opam install coq.8.18.0 ``` 2. Install the Mathematical Components ``` diff --git a/Makefile.common b/Makefile.common index b91ceb5aa..9d4b257d1 100644 --- a/Makefile.common +++ b/Makefile.common @@ -126,3 +126,17 @@ doc: __always__ Makefile.coq doc-clean: rm -rf _build_doc/ + +coq2html: + ../coq2html/coq2html \ + -fragile-mathcomp-break \ + -title "Mathcomp Analysis" \ + -d html/ -base mathcomp -Q theories analysis \ + -coqlib https://coq.inria.fr/doc/V8.18.0/stdlib/ \ + -external https://math-comp.github.io/htmldoc/ mathcomp.ssreflect \ + -external https://math-comp.github.io/htmldoc/ mathcomp.algebra \ + classical/*.v classical/*.glob \ + theories/*.v theories/*.glob + +coq2html-clean: + rm -f */*.glob diff --git a/README.md b/README.md index 60e861c4c..d38d1db0b 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_1_0_0/index.html)). +([`coq2html`](https://github.com/xavierleroy/coq2html) [documentation for the last version](https://math-comp.github.io/analysis/htmldoc_1_1_0/index.html)). Changes are documented in [CHANGELOG.md](CHANGELOG.md) and [CHANGELOG_UNRELEASED.md](CHANGELOG_UNRELEASED.md).