From d64e9df02884ed1a100efce56f07dd9b448fac7d Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Wed, 9 Oct 2024 09:55:32 +0900 Subject: [PATCH] changelog for version 1.5.0 (#1344) * changelog for version 1.5.0 --- CHANGELOG.md | 315 ++++++++++++++++++++++++++++++++++++++-- CHANGELOG_UNRELEASED.md | 288 ------------------------------------ INSTALL.md | 2 +- README.md | 2 +- 4 files changed, 308 insertions(+), 299 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 259e4240c..0a4027f90 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,303 @@ # Changelog -Latest releases: [[1.4.0] - 2024-09-24](#140---2024-09-24) and [[1.3.1] - 2024-08-09](#131---2024-08-09) +Latest releases: [[1.5.0] - 2024-10-09](#131---2024-08-09) and [[1.4.0] - 2024-09-24](#140---2024-09-24) + +## [1.5.0] - 2024-10-09 + +### Added + +- in `mathcomp_extra.v`: + + lemma `bij_forall` + +- in `classical_sets.v`: + + lemma `not_setD1` + +- in file `classical_orders.v` (new file), + + new definitions `big_lexi_order`, `same_prefix`, `first_diff`, + `big_lexi_le`, and `start_with`. + + new lemmas `same_prefix0`, `same_prefix_sym`, `same_prefix_leq`, + `same_prefix_refl`, `same_prefix_trans`, `first_diff_sym`, + `first_diff_unique`, `first_diff_SomeP`, `first_diff_NoneP`, + `first_diff_lt`, `first_diff_eq`, `first_diff_dfwith`, + `big_lexi_le_reflexive`, `big_lexi_le_anti`, `big_lexi_le_trans`, + `big_lexi_le_total`, `start_with_prefix`, `leEbig_lexi_order`, + `big_lexi_order_prefix_lt`, `big_lexi_order_prefix_gt`, + `big_lexi_order_between`, and `big_lexi_order_interval_prefix`. + +- in `filter.v` (new file): + + lemma `in_nearW` + +- in `topology.v`: + + lemma `open_in_nearW` + +- new file `separation_axioms.v` + +- in `normedtype.v`: + + lemma `cvgyNP` + + lemma `limf_esup_ge0` + + lemma `nbhs_left_ltBl` + + lemma `within_continuous_continuous` + +- in `sequences.v`: + + lemma `nneseries_split_cond` + + lemma `subset_lee_nneseries` + +- in `exp.v`: + + lemma `expR_gt1Dx` + +- in `derive.v`: + + lemma `exprn_derivable` + +- in `realfun.v`: + + lemmas `cvg_pinftyP`, `cvg_ninftyP` + +- in `measure.v`: + + lemma `measurable_fun_set1` + + lemma `measurable_fun_set0` + +- in `lebesgue_measure.v`: + + lemma `vitali_coverS` + + lemma `vitali_theorem_corollary` + + lemmas `measurable_fun_itv_co`, `measurable_fun_itv_oc`, `measurable_fun_itv_cc` + +- in `lebesgue_integral.v`: + + lemma `integral_itv_bndoo` + +- in `ftc.v`: + + lemmas `increasing_image_oo`, `decreasing_image_oo`, + `increasing_cvg_at_right_comp`, `increasing_cvg_at_left_comp`, + `decreasing_cvg_at_right_comp`, `decreasing_cvg_at_left_comp`, + + lemma `eq_integral_itv_bounded`. + + lemmas `integration_by_substitution_decreasing`, + `integration_by_substitution_oppr`, + `integration_by_substitution_increasing` + +### Changed + +- `theories/topology.v` split into `classical/filter.v` and `theories/topology.v` + +- moved from `topology.v` to `filter.v` + + definition `set_system`, coercion `set_system_to_set` + + mixin `isFiltered`, structures `Filtered`, `PointedFiltered` + (with resp. types `filteredType` and `pfilteredType`) + + mixin `selfFiltered` + + factory `hasNbhs` + + structures `Nbhs`, `PointedNbhs` + (with resp. types `nbhsType`, `pnbhsType`) + + definitions `filter_from`, `filter_prod` + + definitions `prop_near1`, `prop_near2` + + notations `{near _, _}`, `\forall _ \near _, _`, `near _, _`, + `{near _ & _, _}`, `\forall _ \near _ & _, _`, `\forall _ & _ \near _, _`, + `\near _ & _, _` + + lemmas `nearE`, `eq_near`, `nbhs_filterE` + + module `NbhsFilter` (with definition `nbhs_simpl`) + + definition `cvg_to`, notation ```_ `=>` _``` + + lemmas `cvg_refl`, `cvg_trans`, notation `_ --> _` + + definitions `type_of_filter`, `lim_in`, `lim` + + notations `[lim _ in _]`, `[cvg _ in _]`, `cvg` + + definition `eventually`, notation `\oo` + + lemmas `cvg_prod`, `cvg_in_ex`, `cvg_ex`, `cvg_inP`, `cvgP`, `cvg_in_toP`, + `cvg_toP`, `dvg_inP`, `dvgP`, `cvg_inNpoint`, `cvgNpoint` + + lemmas `nbhs_nearE`, `near_nbhs`, `near2_curry`, `near2_pair`, `filter_of_nearI` + + definition `near2E` + + module `NearNbhs` (with (re)definition `near_simpl` and ltac `near_simpl`) + + lemma `near_swap` + + classes `Filter` + + lemmas `filter_setT`, `filterP_strong` + + structure `filter_on` + + definition `filter_class` + + coercion `filter_filter'` + + structure `pfilter_on` + + definition `pfilter_class` + + canonical `pfilter_filter_on` + + coercion `pfilter_filter_on` + + definiton `PFilterType` + + instances `filter_on_Filter`, `pfilter_on_ProperFilter` + + lemma `nbhs_filter_onE`, `near_filter_onE` + + definition and canonical `trivial_filter_on` + + lemmas `filter_nbhsT`, `nearT`, `filter_not_empty_ex` + + lemma `filter_ex_subproof`, definition `filter_ex` + + lemma `filter_getP` + + record `in_filter` + + module type `in_filter`, module `PropInFilter`, notation `prop_of`, definition `prop_ofE`, + notation `_ \is_near _`, definition `is_nearE` + + lemma `prop_ofP` + + definition `in_filterT` + + canonical `in_filterI` + + lemma `filter_near_of` + + fact `near_key` + + lemmas `mark_near`, `near_acc`, `near_skip_subproof` + + tactic notations `near=>`, `near:`, `near do _` + + ltacs `just_discharge_near`, `near_skip`, `under_near`, `end_near`, `done` + + lemmas `have_near`, `near`, `nearW`, `filterE`, `filter_app`, `filter_app2`, + `filter_app3`, `filterS2`, `filterS3`, `filter_const`, `in_filter_from`, + `near_andP`, `nearP_dep`, `filter2P`, `filter_ex2`, `filter_fromP`, `filter_fromTP`, + `filter_from_filter`, `filter_fromT_filter`, `filter_from_proper`, `filter_bigI`, + `filter_forall`, `filter_imply` + + definition `fmap` + + lemma `fmapE` + + notations `_ @[_ --> _]`, `_ @[_ \oo]`, `_ @ _`, `limn`, `cvgn` + + instances `fmap_filter`, `fmap_proper_filter` + + definition `fmapi`, notations `_ `@[_ --> _]`, `_ `@ _` + + lemma `fmapiE` + + instances `fmapi_filter`. `fmapi_proper_filter` + + lemmas `cvg_id`, `fmap_comp`, `appfilter`, `cvg_app`, `cvgi_app`, `cvg_comp`, + `cvgi_comp`, `near_eq_cvg`, `eq_cvg`, `eq_is_cvg_in`, `eq_is_cvg`, `neari_eq_loc`, + `cvg_near_const` + + definition `continuous_at`, notation `continuous` + + lemma `near_fun` + + definition `globally`, lemma `globally0`, instances `globally_filter`, `globally_properfilter` + + definition `frechet_filter`, instances `frechet_properfilter`, `frechet_properfilter_nat` + + definition `at_point`, instance `at_point_filter` + + instances `filter_prod_filter`, `filter_prod_proper`, canonical `prod_filter_on` + + lemmas `filter_prod1`, `filter_prod2` + + definition `in_filter_prod` + + lemmas `near_pair`, `cvg_cst`, `cvg_snd`, `near_map`, `near_map2`, `near_mapi`, + `filter_pair_set`, `filter_pair_near_of` + + module export `NearMap` + + lemmas `filterN`, `cvg_pair`, `cvg_comp2` + + definition `cvg_to_comp_2` + + definition `within`, lemmas `near_withinE`, `withinT`, `near_withinT`, `cvg_within`, + `withinET`, instance `within_filter`, canonical `within_filter_on`, + lemma `filter_bigI_within` + + definition `subset_filter`, instance `subset_filter_filter`, lemma `subset_filter_proper` + + definition `powerset_filter_from`, instance `powerset_filter_from_filter` + + lemmas `near_small_set`, `small_set_sub`, `near_powerset_filter_fromP`, + `powerset_filter_fromP`, `near_powerset_map`, `near_powerset_map_monoE` + + definitions `principal_filter`, `principal_filter_type` + + lemmas `principal_filterP`, `principal_filter_proper` + + class `UltraFilter`, lemma `ultraFilterLemma` + + lemmas `filter_image`, `proper_image`, `principal_filter_ultra`, `in_ultra_setVsetC`, + `ultra_image` + + instance `smallest_filter_filter` + + fixpoint `filterI_iter` + + lemmas `filterI_iter_sub`, `filterI_iterE` + + definition `finI_from` + + lemmas `finI_from_cover`, `finI_from1`, `finI_from_countable`, `finI_fromI`, + `filterI_iter_finI`, `filterI_iter_finI` + + definition `finI` + + lemmas `finI_filter`, `filter_finI`, `meets_globallyl`, `meets_globallyr`, + `meetsxx`, `proper_meetsxx` + + instance `eventually_filter`, canonicals `eventually_filterType`, `eventually_pfilterType` + +- changed when moved from `topology.v` to `filter.v` + + `Build_ProperFilter` -> `Build_ProperFilter_ex` + + `ProperFilter'` -> `ProperFilter` + + remove notation `ProperFilter` + +- moved from `topology.v` to `mathcomp_extra.v`: + + lemma `and_prop_in` + + lemmas `mem_inc_segment`, `mem_inc_segment` + +- moved from `topology.v` to `boolp.v`: + + lemmas `bigmax_geP`, `bigmax_gtP`, `bigmin_leP`, `bigmin_ltP` + +- moved from `topology.v` to `separation_axioms.v`: `set_nbhs`, `set_nbhsP`, + `accessible_space`, `kolmogorov_space`, `hausdorff_space`, + `compact_closed`, `discrete_hausdorff`, `compact_cluster_set1`, + `compact_precompact`, `open_hausdorff`, `hausdorff_accessible`, + `accessible_closed_set1`, `accessible_kolmogorov`, + `accessible_finite_set_closed`, `subspace_hausdorff`, `order_hausdorff`, + `ball_hausdorff`, `Rhausdorff`, `close`, `closeEnbhs`, `closeEonbhs`, + `close_sym`, `cvg_close`, `close_refl`, `cvgx_close`, `cvgi_close`, + `cvg_toi_locally_close`, `closeE`, `close_eq`, `cvg_unique`, `cvg_eq`, + `cvgi_unique`, `close_cvg`, `lim_id`, `lim_near_cst`, `lim_cst`, + `entourage_close`, `close_trans`, `close_cvgxx`, `cvg_closeP`, + `ball_close`, `normal_space`, `regular_space`, `compact_regular`, + `uniform_regular`, `totally_disconnected`, `zero_dimensional`, + `discrete_zero_dimension`, `zero_dimension_totally_disconnected`, + `zero_dimensional_ray`, `type`, `countable_uniform_bounded`, + `countable_uniform`, `sup_pseudometric`, `countable_uniformityT`, `gauge`, + `iter_split_ent`, `gauge_ent`, `gauge_filter`, `gauge_refl`, `gauge_inv`, + `gauge_split`, `gauge_countable_uniformity`, `uniform_pseudometric_sup`, + `perfect_set`, `perfectTP`, and `perfectTP_ex`. + +- in `numfun.v`: + + lemma `gt0_funeposM` renamed to `ge0_funeposM` + and hypothesis weakened from strict to large inequality + + lemma `gt0_funenegM` renamed to `ge0_funenegM` + and hypothesis weakened from strict to large inequality + + lemma `lt0_funeposM` renamed to `le0_funeposM` + and hypothesis weakened from strict to large inequality + + lemma `lt0_funenegM` renamed to `le0_funenegM` + and hypothesis weakened from strict to large inequality + +### Renamed + +- in file `topology.v` -> `separation_axioms.v` + + `totally_disconnected_cvg` -> `zero_dimensional_cvg`. + + `perfect_set2` -> `perfectTP_ex` + +### Generalized + +- in `constructive_ereal.v`: + + lemmas `maxeMr`, `maxeMl`, `mineMr`, `mineMr`: + hypothesis weakened from strict inequality to large inequality + +- in `sequences.v`: + + lemma `eseries_mkcond` + + lemma `nneseries_tail_cvg` + +- in `exp.v`: + + lemmas `expR_ge1Dx` and `expeR_ge1Dx` (remove hypothesis) + + lemma `le_ln1Dx` (weaken hypothesis) + +- in `derive.v`: + + lemma `derivableX` + +- in `lebesgue_integral.v`: + + lemma `integral_setD1_EFin` + + lemmas `integral_itv_bndo_bndc`, `integral_itv_obnd_cbnd` + + lemmas `Rintegral_itv_bndo_bndc`, `Rintegral_itv_obnd_cbnd` + +### Deprecated + +- in `separation_axioms.v`: + + definition `cvg_toi_locally_close` + +- in `realfun.v`: + + lemma `lime_sup_ge0` + +### Removed + +- in `constructive_ereal.v`: + + notation `lte_spaddr` (deprecated since 0.6) + + notation `gte_opp` (deprecated since 0.6.0) + + lemmas `daddooe`, `daddeoo` + + notations `desum_ninftyP`, `desum_ninfty`, `desum_pinftyP`, `desum_pinfty` (deprecated since 0.6.0) + + notation `eq_pinftyP` (deprecated since 0.6.0) + +- in `topology.v`: + + notation `[filteredType _ of _]` + + definition `fmap_proper_filter'` + + definition `filter_map_proper_filter'` + + definition `filter_prod_proper'` + +- in `normedtype.v`: + + notation `normmZ` (deprecated since 0.6.0) + + notation `nbhs_image_ERFin` (deprecated since 0.6.0) + + notations `ereal_limrM`, `ereal_limMr`, `ereal_limN` (deprecated since 0.6.0) + + notation `norm_cvgi_map_lim` (deprecated since 0.6.0) + + notations `ereal_cvgN`, `ereal_is_cvgN`, `ereal_cvgrM`, `ereal_is_cvgrM`, + `ereal_cvgMr`, `ereal_is_cvgMr`, `ereal_cvgM` (deprecated since 0.6.0) + + notation `cvg_dist`, lemma `__deprecated__cvg_dist` (deprecated since 0.6.0) + + notation `cvg_dist2`, lemma `__deprecated__cvg_dist2` (deprecated since 0.6.0) + + notation `cvg_dist0`, lemma `__deprecated__cvg_dist0` (deprecated since 0.6.0) + + notation `ler0_addgt0P`, lemma `__deprecated__ler0_addgt0P` (deprecated since 0.6.0) + + notation `cvg_bounded_real`, lemma `__deprecated__cvg_bounded_real` (deprecated since 0.6.0) + + notation `linear_continuous0`, lemma `__deprecated__linear_continuous0` (deprecated since 0.6.0) + +- in `sequences.v`: + + notation `nneseries_mkcond` (was deprecated since 0.6.0) + + notation `squeeze`, lemma `__deprecated__squeeze` (deprecated since 0.6.0) + + notation `cvgPpinfty`, lemma `__deprecated__cvgPpinfty` (deprecated since 0.6.0) + + notation `cvgNpinfty`, lemma `__deprecated__cvgNpinfty` (deprecated since 0.6.0) + + notation `cvgNninfty`, lemma `__deprecated__cvgNninfty` (deprecated since 0.6.0) + + notation `cvgPninfty`, lemma `__deprecated__cvgPninfty` (deprecated since 0.6.0) + + notation `ger_cvg_pinfty`, lemma `__deprecated__ger_cvg_pinfty` (deprecated since 0.6.0) + + notation `ler_cvg_ninfty`, lemma `__deprecated__ler_cvg_ninfty` (deprecated since 0.6.0) + + notation `lim_ge`, lemma `__deprecated__lim_ge` (deprecated since 0.6.0) + + notation `lim_le`, lemma `__deprecated__lim_le` (deprecated since 0.6.0) ## [1.4.0] - 2024-09-24 @@ -28,7 +325,7 @@ Latest releases: [[1.4.0] - 2024-09-24](#140---2024-09-24) and [[1.3.1] - 2024-0 - in `topology.v`: + lemma `filterN` - + Structures `PointedFiltered`, `PointedNbhs`, `PointedUniform`, + + Structures `PointedFiltered`, `PointedNbhs`, `PointedUniform`, `PseudoPointedMetric` + new definition `order_topology` + new lemmas `discrete_nat`, `rray_open`, `lray_open`, `itv_open`, @@ -40,7 +337,7 @@ Latest releases: [[1.4.0] - 2024-09-24](#140---2024-09-24) and [[1.3.1] - 2024-0 - in `normedtype.v`: + lemmas `not_near_inftyP`, `not_near_ninftyP` + lemma `ninftyN` - + lemma `le_closed_ball` + + lemma `le_closed_ball` + lemmas `nbhs_right_ltW`, `cvg_patch` - in `derive.v`: @@ -89,22 +386,22 @@ Latest releases: [[1.4.0] - 2024-09-24](#140---2024-09-24) and [[1.3.1] - 2024-0 ### Changed - in `topology.v`: - + removed the pointed assumptions from `FilteredType`, `Nbhs`, + + 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 + + `pointed_principal_filter` becomes `principle_filter_type` and requires only `choiceType` instead of `pointedType` - + `pointed_discrete_topology` becomes `discrete_topology_type` and + + `pointed_discrete_topology` becomes `discrete_topology_type` and requires only `choiceType` instead of `pointedType` - + renamed lemma `discrete_pointed`to `discrete_space_discrete` - + + 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 `[/\ _, _ & _]` diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1aeb19d66..67bb43c3b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,304 +4,16 @@ ### Added -- in `realfun.v`: - + lemmas `cvg_pinftyP`, `cvg_ninftyP` - -- in `mathcomp_extra.v`: - + lemma `bij_forall` - -- in `normedtype.v`: - + lemma `cvgyNP` - -- in `realfun.v`: - + lemmas `cvg_pinftyP`, `cvg_ninftyP` - -- in `filter.v` (new file): - + lemma `in_nearW` - -- in `topology.v`: - + lemma `open_in_nearW` - -- in `classical_sets.v`: - + lemma `not_setD1` - -- in `measure.v`: - + lemma `measurable_fun_set1` -- in file `classical_orders.v`, - + new definitions `big_lexi_order`, `same_prefix`, `first_diff`, - `big_lexi_le`, and `start_with`. - + new lemmas `same_prefix0`, `same_prefix_sym`, `same_prefix_leq`, - `same_prefix_refl`, `same_prefix_trans`, `first_diff_sym`, - `first_diff_unique`, `first_diff_SomeP`, `first_diff_NoneP`, - `first_diff_lt`, `first_diff_eq`, `first_diff_dfwith`, - `big_lexi_le_reflexive`, `big_lexi_le_anti`, `big_lexi_le_trans`, - `big_lexi_le_total`, `start_with_prefix`, `leEbig_lexi_order`, - `big_lexi_order_prefix_lt`, `big_lexi_order_prefix_gt`, - `big_lexi_order_between`, and `big_lexi_order_interval_prefix`. - -- in `exp.v`: - + lemma `expR_gt1Dx` - -- in `derive.v`: - + lemma `exprn_derivable` -- in `sequences.v`: - + lemma `nneseries_split_cond` - + lemma `subset_lee_nneseries` - -- in `lebesgue_measure.v`: - + lemma `vitali_coverS` - + lemma `vitali_theorem_corollary` - -- in `normedtype.v`: - + lemma `limf_esup_ge0` -- in `normedtype.v`: - + lemma `nbhs_left_ltBl` - + lemma `within_continuous_continuous` - -- in `measure.v`: - + lemma `measurable_fun_set0` - -- in `lebesgue_measure.v`: - + lemmas `measurable_fun_itv_co`, `measurable_fun_itv_oc`, `measurable_fun_itv_cc` - -- in `lebesgue_integral.v`: - + lemma `integral_itv_bndoo` - -- in `ftc.v`: - + lemmas `increasing_image_oo`, `decreasing_image_oo`, - `increasing_cvg_at_right_comp`, `increasing_cvg_at_left_comp`, - `decreasing_cvg_at_right_comp`, `decreasing_cvg_at_left_comp`, - + lemma `eq_integral_itv_bounded`. - + lemmas `integration_by_substitution_decreasing`, - `integration_by_substitution_oppr`, - `integration_by_substitution_increasing` - ### Changed -- in `numfun.v`: - + lemma `gt0_funeposM` renamed to `ge0_funeposM` - and hypothesis weakened from strict to large inequality - + lemma `gt0_funenegM` renamed to `ge0_funenegM` - and hypothesis weakened from strict to large inequality - + lemma `lt0_funeposM` renamed to `le0_funeposM` - and hypothesis weakened from strict to large inequality - + lemma `lt0_funenegM` renamed to `le0_funenegM` - and hypothesis weakened from strict to large inequality - -- `theories/topology.v` split into `classical/filter.v` and `theories/topology.v` - -- moved from `topology.v` to `filter.v` - + definition `set_system`, coercion `set_system_to_set` - + mixin `isFiltered`, structures `Filtered`, `PointedFiltered` - (with resp. types `filteredType` and `pfilteredType`) - + mixin `selfFiltered` - + factory `hasNbhs` - + structures `Nbhs`, `PointedNbhs` - (with resp. types `nbhsType`, `pnbhsType`) - + definitions `filter_from`, `filter_prod` - + definitions `prop_near1`, `prop_near2` - + notations `{near _, _}`, `\forall _ \near _, _`, `near _, _`, - `{near _ & _, _}`, `\forall _ \near _ & _, _`, `\forall _ & _ \near _, _`, - `\near _ & _, _` - + lemmas `nearE`, `eq_near`, `nbhs_filterE` - + module `NbhsFilter` (with definition `nbhs_simpl`) - + definition `cvg_to`, notation ```_ `=>` _``` - + lemmas `cvg_refl`, `cvg_trans`, notation `_ --> _` - + definitions `type_of_filter`, `lim_in`, `lim` - + notations `[lim _ in _]`, `[cvg _ in _]`, `cvg` - + definition `eventually`, notation `\oo` - + lemmas `cvg_prod`, `cvg_in_ex`, `cvg_ex`, `cvg_inP`, `cvgP`, `cvg_in_toP`, - `cvg_toP`, `dvg_inP`, `dvgP`, `cvg_inNpoint`, `cvgNpoint` - + lemmas `nbhs_nearE`, `near_nbhs`, `near2_curry`, `near2_pair`, `filter_of_nearI` - + definition `near2E` - + module `NearNbhs` (with (re)definition `near_simpl` and ltac `near_simpl`) - + lemma `near_swap` - + classes `Filter` - + lemmas `filter_setT`, `filterP_strong` - + structure `filter_on` - + definition `filter_class` - + coercion `filter_filter'` - + structure `pfilter_on` - + definition `pfilter_class` - + canonical `pfilter_filter_on` - + coercion `pfilter_filter_on` - + definiton `PFilterType` - + instances `filter_on_Filter`, `pfilter_on_ProperFilter` - + lemma `nbhs_filter_onE`, `near_filter_onE` - + definition and canonical `trivial_filter_on` - + lemmas `filter_nbhsT`, `nearT`, `filter_not_empty_ex` - + lemma `filter_ex_subproof`, definition `filter_ex` - + lemma `filter_getP` - + record `in_filter` - + module type `in_filter`, module `PropInFilter`, notation `prop_of`, definition `prop_ofE`, - notation `_ \is_near _`, definition `is_nearE` - + lemma `prop_ofP` - + definition `in_filterT` - + canonical `in_filterI` - + lemma `filter_near_of` - + fact `near_key` - + lemmas `mark_near`, `near_acc`, `near_skip_subproof` - + tactic notations `near=>`, `near:`, `near do _` - + ltacs `just_discharge_near`, `near_skip`, `under_near`, `end_near`, `done` - + lemmas `have_near`, `near`, `nearW`, `filterE`, `filter_app`, `filter_app2`, - `filter_app3`, `filterS2`, `filterS3`, `filter_const`, `in_filter_from`, - `near_andP`, `nearP_dep`, `filter2P`, `filter_ex2`, `filter_fromP`, `filter_fromTP`, - `filter_from_filter`, `filter_fromT_filter`, `filter_from_proper`, `filter_bigI`, - `filter_forall`, `filter_imply` - + definition `fmap` - + lemma `fmapE` - + notations `_ @[_ --> _]`, `_ @[_ \oo]`, `_ @ _`, `limn`, `cvgn` - + instances `fmap_filter`, `fmap_proper_filter` - + definition `fmapi`, notations `_ `@[_ --> _]`, `_ `@ _` - + lemma `fmapiE` - + instances `fmapi_filter`. `fmapi_proper_filter` - + lemmas `cvg_id`, `fmap_comp`, `appfilter`, `cvg_app`, `cvgi_app`, `cvg_comp`, - `cvgi_comp`, `near_eq_cvg`, `eq_cvg`, `eq_is_cvg_in`, `eq_is_cvg`, `neari_eq_loc`, - `cvg_near_const` - + definition `continuous_at`, notation `continuous` - + lemma `near_fun` - + definition `globally`, lemma `globally0`, instances `globally_filter`, `globally_properfilter` - + definition `frechet_filter`, instances `frechet_properfilter`, `frechet_properfilter_nat` - + definition `at_point`, instance `at_point_filter` - + instances `filter_prod_filter`, `filter_prod_proper`, canonical `prod_filter_on` - + lemmas `filter_prod1`, `filter_prod2` - + definition `in_filter_prod` - + lemmas `near_pair`, `cvg_cst`, `cvg_snd`, `near_map`, `near_map2`, `near_mapi`, - `filter_pair_set`, `filter_pair_near_of` - + module export `NearMap` - + lemmas `filterN`, `cvg_pair`, `cvg_comp2` - + definition `cvg_to_comp_2` - + definition `within`, lemmas `near_withinE`, `withinT`, `near_withinT`, `cvg_within`, - `withinET`, instance `within_filter`, canonical `within_filter_on`, - lemma `filter_bigI_within` - + definition `subset_filter`, instance `subset_filter_filter`, lemma `subset_filter_proper` - + definition `powerset_filter_from`, instance `powerset_filter_from_filter` - + lemmas `near_small_set`, `small_set_sub`, `near_powerset_filter_fromP`, - `powerset_filter_fromP`, `near_powerset_map`, `near_powerset_map_monoE` - + definitions `principal_filter`, `principal_filter_type` - + lemmas `principal_filterP`, `principal_filter_proper` - + class `UltraFilter`, lemma `ultraFilterLemma` - + lemmas `filter_image`, `proper_image`, `principal_filter_ultra`, `in_ultra_setVsetC`, - `ultra_image` - + instance `smallest_filter_filter` - + fixpoint `filterI_iter` - + lemmas `filterI_iter_sub`, `filterI_iterE` - + definition `finI_from` - + lemmas `finI_from_cover`, `finI_from1`, `finI_from_countable`, `finI_fromI`, - `filterI_iter_finI`, `filterI_iter_finI` - + definition `finI` - + lemmas `finI_filter`, `filter_finI`, `meets_globallyl`, `meets_globallyr`, - `meetsxx`, `proper_meetsxx` - -- changed when moved from `topology.v` to `filter.v` - + `Build_ProperFilter` -> `Build_ProperFilter_ex` - + `ProperFilter'` -> `ProperFilter` - + remove notation `ProperFilter` - -- moved from `topology.v` to `mathcomp_extra.v`: - + lemma `and_prop_in` - + lemmas `mem_inc_segment`, `mem_inc_segment` - -- moved from `topology.v` to `boolp.v`: - + lemmas `bigmax_geP`, `bigmax_gtP`, `bigmin_leP`, `bigmin_ltP` - -- moved from `topology.v` to `separation_axioms.v`: `set_nbhs`, `set_nbhsP`, - `accessible_space`, `kolmogorov_space`, `hausdorff_space`, - `compact_closed`, `discrete_hausdorff`, `compact_cluster_set1`, - `compact_precompact`, `open_hausdorff`, `hausdorff_accessible`, - `accessible_closed_set1`, `accessible_kolmogorov`, - `accessible_finite_set_closed`, `subspace_hausdorff`, `order_hausdorff`, - `ball_hausdorff`, `Rhausdorff`, `close`, `closeEnbhs`, `closeEonbhs`, - `close_sym`, `cvg_close`, `close_refl`, `cvgx_close`, `cvgi_close`, - `cvg_toi_locally_close`, `closeE`, `close_eq`, `cvg_unique`, `cvg_eq`, - `cvgi_unique`, `close_cvg`, `lim_id`, `lim_near_cst`, `lim_cst`, - `entourage_close`, `close_trans`, `close_cvgxx`, `cvg_closeP`, - `ball_close`, `normal_space`, `regular_space`, `compact_regular`, - `uniform_regular`, `totally_disconnected`, `zero_dimensional`, - `discrete_zero_dimension`, `zero_dimension_totally_disconnected`, - `zero_dimensional_ray`, `type`, `countable_uniform_bounded`, - `countable_uniform`, `sup_pseudometric`, `countable_uniformityT`, `gauge`, - `iter_split_ent`, `gauge_ent`, `gauge_filter`, `gauge_refl`, `gauge_inv`, - `gauge_split`, `gauge_countable_uniformity`, `uniform_pseudometric_sup`, - `perfect_set`, `perfectTP`, and `perfectTP_ex`. ### Renamed -- in file `topology.v` -> `separation_axioms.v` - + `totally_disconnected_cvg` -> `zero_dimensional_cvg`. - + `perfect_set2` -> `perfectTP_ex` - ### Generalized -- in `constructive_ereal.v`: - + lemmas `maxeMr`, `maxeMl`, `mineMr`, `mineMr`: - hypothesis weakened from strict inequality to large inequality -- in `lebesgue_integral.v`: - + lemma `integral_setD1_EFin` - + lemmas `integral_itv_bndo_bndc`, `integral_itv_obnd_cbnd` - + lemmas `Rintegral_itv_bndo_bndc`, `Rintegral_itv_obnd_cbnd` - -- in `exp.v`: - + lemmas `expR_ge1Dx` and `expeR_ge1Dx` (remove hypothesis) - + lemma `le_ln1Dx` (weaken hypothesis) - -- in `sequences.v`: - + lemma `eseries_mkcond` - + lemma `nneseries_tail_cvg` - -- in `derive.v`: - + lemma `derivableX` - ### Deprecated -- in `separation_axioms.v`: - + definition `cvg_toi_locally_close` -- in `realfun.v`: - + lemma `lime_sup_ge0` - ### Removed -- in `topology.v`: - + notation `[filteredType _ of _]` - + definition `fmap_proper_filter'` - + definition `filter_map_proper_filter'` - + definition `filter_prod_proper'` -- in `sequences.v`: - + notation `nneseries_mkcond` (was deprecated since 0.6.0) - -- in `constructive_ereal.v`: - + notation `lte_spaddr` (deprecated since 0.6) - -- in `normedtype.v`: - + notation `normmZ` (deprecated since 0.6.0) - + notation `nbhs_image_ERFin` (deprecated since 0.6.0) - + notations `ereal_limrM`, `ereal_limMr`, `ereal_limN` (deprecated since 0.6.0) - + notation `norm_cvgi_map_lim` (deprecated since 0.6.0) - + notations `ereal_cvgN`, `ereal_is_cvgN`, `ereal_cvgrM`, `ereal_is_cvgrM`, - `ereal_cvgMr`, `ereal_is_cvgMr`, `ereal_cvgM` (deprecated since 0.6.0) - + notation `cvg_dist`, lemma `__deprecated__cvg_dist` (deprecated since 0.6.0) - + notation `cvg_dist2`, lemma `__deprecated__cvg_dist2` (deprecated since 0.6.0) - + notation `cvg_dist0`, lemma `__deprecated__cvg_dist0` (deprecated since 0.6.0) - + notation `ler0_addgt0P`, lemma `__deprecated__ler0_addgt0P` (deprecated since 0.6.0) - + notation `cvg_bounded_real`, lemma `__deprecated__cvg_bounded_real` (deprecated since 0.6.0) - + notation `linear_continuous0`, lemma `__deprecated__linear_continuous0` (deprecated since 0.6.0) - -- in `constructive_ereal.v`: - + notation `gte_opp` (deprecated since 0.6.0) - + lemmas `daddooe`, `daddeoo` - + notations `desum_ninftyP`, `desum_ninfty`, `desum_pinftyP`, `desum_pinfty` (deprecated since 0.6.0) - + notation `eq_pinftyP` (deprecated since 0.6.0) - -- in `sequences.v`: - + notation `squeeze`, lemma `__deprecated__squeeze` (deprecated since 0.6.0) - + notation `cvgPpinfty`, lemma `__deprecated__cvgPpinfty` (deprecated since 0.6.0) - + notation `cvgNpinfty`, lemma `__deprecated__cvgNpinfty` (deprecated since 0.6.0) - + notation `cvgNninfty`, lemma `__deprecated__cvgNninfty` (deprecated since 0.6.0) - + notation `cvgPninfty`, lemma `__deprecated__cvgPninfty` (deprecated since 0.6.0) - + notation `ger_cvg_pinfty`, lemma `__deprecated__ger_cvg_pinfty` (deprecated since 0.6.0) - + notation `ler_cvg_ninfty`, lemma `__deprecated__ler_cvg_ninfty` (deprecated since 0.6.0) - + notation `lim_ge`, lemma `__deprecated__lim_ge` (deprecated since 0.6.0) - + notation `lim_le`, lemma `__deprecated__lim_le` (deprecated since 0.6.0) - ### Infrastructure ### Misc diff --git a/INSTALL.md b/INSTALL.md index 01a19bf45..6ed4a24d7 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.4.0 +$ opam install coq-mathcomp-analysis.1.5.0 ``` 4. Everytime you want to work in this same context, you need to type ``` diff --git a/README.md b/README.md index 0114382fa..9a5d5b8db 100644 --- a/README.md +++ b/README.md @@ -84,7 +84,7 @@ We try to preserve backward compatibility as best as we can. 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)). +[HTML rendering of the source code](https://math-comp.github.io/analysis/htmldoc_1_5_0/index.html) (using [`coq2html`](https://github.com/xavierleroy/coq2html)). Overview presentations: - [Classical Analysis with Coq](https://perso.crans.org/cohen/CoqWS2018.pdf) (2018)