From 9c311a9344f3af02fbb12101b24482846d64e8ea Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Thu, 6 Jun 2024 15:32:48 +0900 Subject: [PATCH] changelog for version 1.2.0 (#1239) * changelog for version 1.2.0 --- CHANGELOG.md | 266 ++++++++++++++++- CHANGELOG_UNRELEASED.md | 279 ------------------ INSTALL.md | 2 +- README.md | 8 +- ..._fimfun.png => hierarchy_fimfun.1.1.0.png} | Bin ...ions.png => hierarchy_functions.1.1.0.png} | Bin ..._kernel.png => hierarchy_kernel.1.1.0.png} | Bin ...rchy_main.png => hierarchy_main.1.1.0.png} | Bin ...easure.png => hierarchy_measure.1.1.0.png} | Bin 9 files changed, 270 insertions(+), 285 deletions(-) rename etc/{hierarchy_fimfun.png => hierarchy_fimfun.1.1.0.png} (100%) rename etc/{hierarchy_functions.png => hierarchy_functions.1.1.0.png} (100%) rename etc/{hierarchy_kernel.png => hierarchy_kernel.1.1.0.png} (100%) rename etc/{hierarchy_main.png => hierarchy_main.1.1.0.png} (100%) rename etc/{hierarchy_measure.png => hierarchy_measure.1.1.0.png} (100%) diff --git a/CHANGELOG.md b/CHANGELOG.md index a3c8a618e..39ec923e9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,270 @@ # Changelog -Latest releases: [[1.1.0] - 2024-03-31](#110---2024-03-31) and [[1.0.0] - 2024-01-26](#100---2024-01-26) +Latest releases: [[1.2.0] - 2024-06-06](#120---2024-06-06) and [[1.1.0] - 2024-03-31](#110---2024-03-31) + +## [1.2.0] - 2024-06-06 + +### Added + +- in file `mathcomp_extra.v`: + + module `Order` + * definitions `disp_t`, `default_display` + + lemma `Pos_to_natE` + +- in `classical_sets.v`: + + lemma `bigcup_recl` + + notations `\bigcup_(i >= n) F i` and `\bigcap_(i >= n) F i` + + lemmas `bigcup_addn`, `bigcap_addn` + + lemmas `setD_bigcup`, `nat_nonempty` + + hint `nat_nonempty` + + lemma `bigcup_bigsetU_bigcup` + + lemmas `setDUD`, `setIDAC` + +- in `Rstruct.v`: + + lemma `IZRposE` + +- in `signed.v`: + + lemma `onem_nonneg_proof`, definition `onem_nonneg` + +- in `esum.v`: + + lemma `nneseries_sum_bigcup` + +- in `normedtype.v`: + + lemma `not_near_at_leftP` + +- in `sequences.v`: + + lemma `nneseries_recl` + + lemma `nneseries_addn` + +- in `realfun.v` + + lemmas `total_variation_nondecreasing`, `total_variation_bounded_variation` + +- in `measure.v`: + + definition `subset_sigma_subadditive` + + factory `isSubsetOuterMeasure` + + structure `SigmaRing`, notation `sigmaRingType` + + factory `isSigmaRing` + + lemma `bigcap_measurable` for `sigmaRingType` + + lemma `setDI_semi_setD_closed` + + lemmas `powerset_lambda_system`, `lambda_system_smallest`, `sigmaRingType_lambda_system` + + definitions `niseq_closed`, `sigma_ring` (notation `<>`), + `monotone` (notation `<>`) + + lemmas `smallest_sigma_ring`, `sigma_ring_monotone`, `g_sigma_ring_monotone`, + `sub_g_sigma_ring`, `setring_monotone_sigma_ring`, `g_monotone_monotone`, + `g_monotone_setring`, `g_monotone_g_sigma_ring`, `monotone_setring_sub_g_sigma_ring` + + lemmas `powerset_sigma_ring`, `g_sigma_ring_strace`, `setI_g_sigma_ring`, + `subset_strace` + + lemma `measurable_and` + + lemma `measurableID` + + lemma `strace_sigma_ring` + +- in `lebesgue_measure.v`: + + lemma `measurable_fun_ler` + + lemmas `measurable_natmul`, `measurable_fun_pow` + +- in `lebesgue_integral.v`: + + lemmas `integrableMl`, `integrableMr` + +- in `probability.v`: + + definition `bernoulli_pmf` + + lemmas `bernoulli_pmf_ge0`, `bernoulli_pmf1`, `measurable_bernoulli_pmf` + + definition `bernoulli` (equipped with the `probability` structure) + + lemmas `bernoulli_dirac`, `bernoulliE`, `integral_bernoulli`, `measurable_bernoulli`, + `measurable_bernoulli2` + + definition `binomial_pmf` + + lemmas `binomial_pmf_ge0`, `measurable_binomial_pmf` + + definitions `binomial_prob` (equipped with the `probability` structure), `bin_prob` + + lemmas `bin_prob0`, `bin_prob1`, `binomial_msum`, `binomial_probE`, `integral_binomial`, + `integral_binomial_prob`, `measurable_binomial_prob` + + definition `uniform_pdf` + + lemmas `measurable_uniform_pdf`, `integral_uniform_pdf`, `integral_uniform_pdf1` + + definition `uniform_prob` (equipped with the `probability` structure) + + lemmas `dominates_uniform_prob`, `integral_uniform` + +- new file `theories/all_analysis.v` + +### Changed + +- in `forms.v`: + + notation ``` u ``_ _ ``` + +- in `sequences.v`: + + definition `expR` is now HB.locked + + equality reversed in lemma `eq_bigcup_seqD` + + `eq_bigsetU_seqD` renamed to `nondecreasing_bigsetU_seqD` + and equality reversed + +- in `trigo.v`: + + definitions `sin`, `cos`, `acos`, `asin`, `atan` are now HB.locked + +- in `measure.v`: + + change the hypothesis of `measurable_fun_bool` + + mixin `AlgebraOfSets_isMeasurable` renamed to `hasMeasurableCountableUnion` + and made to inherit from `SemiRingOfSets` + + rm hypo and variable in lemma `smallest_monotone_classE` + and rename to `smallest_lambda_system` + + rm hypo in lemma `monotone_class_g_salgebra` and renamed + to `g_salgebra_lambda_system` + + rm hypo in lemma `monotone_class_subset` and renamed to + `lambda_system_subset` + + notation `<>` changed to `<>`, + notation `<>` changed to `<>` + +- moved from `lebesgue_measure.v` to `measure.v`: + + definition `strace` + + lemma `sigma_algebra_strace` + +### Renamed + +- in `classical_sets.v`: + + `notin_set` -> `notin_setE` + +- in `constructive_ereal.v`: + + `gee_pmull` -> `gee_pMl` + + `gee_addl` -> `geeDl` + + `gee_addr` -> `geeDr` + + `gte_addl` -> `gteDl` + + `gte_addr` -> `gteDr` + + `lte_subl_addr` -> `lteBlDr` + + `lte_subl_addl` -> `lteBlDl` + + `lte_subr_addr` -> `lteBrDr` + + `lte_subr_addl` -> `lteBrDl` + + `lee_subl_addr` -> `leeBlDr` + + `lee_subl_addl` -> `leeBlDl` + + `lee_subr_addr` -> `leeBrDr` + + `lee_subr_addl` -> `leeBrDl` + + `num_lee_maxr` -> `num_lee_max` + + `num_lee_maxl` -> `num_gee_max` + + `num_lee_minr` -> `num_lee_min` + + `num_lee_minl` -> `num_gee_min` + + `num_lte_maxr` -> `num_lte_max` + + `num_lte_maxl` -> `num_gte_max` + + `num_lte_minr` -> `num_lte_min` + + `num_lte_minl` -> `num_gte_min` + +- in `signed.v`: + + `num_le_maxr` -> `num_le_max` + + `num_le_maxl` -> `num_ge_max` + + `num_le_minr` -> `num_le_min` + + `num_le_minl` -> `num_ge_min` + + `num_lt_maxr` -> `num_lt_max` + + `num_lt_maxl` -> `num_gt_max` + + `num_lt_minr` -> `num_lt_min` + + `num_lt_minl` -> `num_gt_min` + +- in `measure.v`: + + `sub_additive` -> `subadditive` + + `sigma_sub_additive` -> `measurable_subset_sigma_subadditive` + + `content_sub_additive` -> `content_subadditive` + + `ring_sigma_sub_additive` -> `ring_sigma_subadditive` + + `Content_SubSigmaAdditive_isMeasure` -> `Content_SigmaSubAdditive_isMeasure` + + `measure_sigma_sub_additive` -> `measure_sigma_subadditive` + + `measure_sigma_sub_additive_tail` -> `measure_sigma_subadditive_tail` + + `bigcap_measurable` -> `bigcap_measurableType` + + `monotone_class` -> `lambda_system` + + `monotone_class_g_salgebra` -> `g_sigma_algebra_lambda_system` + + `smallest_monotone_classE` -> `smallest_lambda_system` + + `dynkin_monotone` -> `dynkin_lambda_system` + + `dynkin_g_dynkin` -> `g_dynkin_dynkin` + + `salgebraType` -> `g_sigma_algebraType` + + `g_salgebra_measure_unique_trace` -> `g_sigma_algebra_measure_unique_trace` + + `g_salgebra_measure_unique_cover` -> `g_sigma_algebra_measure_unique_cover` + + `g_salgebra_measure_unique` -> `g_sigma_algebra_measure_unique` + + `setI_closed_gdynkin_salgebra` -> `setI_closed_g_dynkin_g_sigma_algebra` + +- in `lebesgue_integral.v`: + + `integral_measure_add` -> `ge0_integral_measure_add` + + `integral_pushforward` -> `ge0_integral_pushforward` + +### Generalized + +- in `Rstruct.v`: + + lemmas `RinvE`, `RdivE` + +- in `constructive_ereal.v`: + + `gee_pMl` (was `gee_pmull`) + +- in `sequences.v`: + + lemmas `eseries0`, `nneseries_split` + +- in `measure.v`: + + lemmas `outer_measure_subadditive`, `outer_measureU2` (from `semiRingOfSetType` to `Type`) + + lemmas `caratheodory_measurable_mu_ext`, `measurableM`, `measure_dominates_trans`, `ess_sup_ge0` + definitions `preimage_classes`, `measure_dominates`, `ess_sup` + (from `measurableType` to `semiRingOfSetsType`) + + lemmas ` measurable_prod_measurableType`, `measurable_prod_g_measurableTypeR` (from `measurableType` to `algebraOfSetsType`) + + from `measurableType` to `sigmaRingType` + * lemmas `bigcup_measurable`, `bigcapT_measurable` + * definition `measurable_fun` + * lemmas `measurable_id`, `measurable_comp`, `eq_measurable_fun`, `measurable_cst`, + `measurable_fun_bigcup`, `measurable_funU`, `measurable_funS`, `measurable_fun_if` + * lemmas `semi_sigma_additiveE`, `sigma_additive_is_additive`, `measure_sigma_additive` + * definitions `pushforward`, `dirac` + * lemmas `diracE`, `dirac0`, `diracT`, `finite_card_sum`, `finite_card_dirac`, `infinite_card_dirac` + * definitions `msum`, `measure_add`, `mscale`, `mseries`, `mrestr` + * lemmas `msum_mzero`, `measure_addE` + * definition `sfinite_measure` + * mixin `isSFinite`, structure `SFiniteMeasure` + * structure `FiniteMeasure` + * factory `Measure_isSFinite` + * lemma `negligible_bigcup` + * definition `ae_eq` + * lemmas `ae_eq0`, `ae_eq_comp`, `ae_eq_funeposneg`, `ae_eq_refl`, `ae_eq_sym`, + `ae_eq_trans`, `ae_eq_sub`, `ae_eq_mul2r`, `ae_eq_mul2l`, `ae_eq_mul1l`, + `ae_eq_abse`, `ae_eq_subset` + + from `measurableType` to `sigmaRingType` and from `realType` to `realFieldType` + * definition `mzero` + + from `realType` to `realFieldType`: + * lemma `sigma_finite_mzero` + +- in `lebesgue_measure.v`: + + from `measurableType` to `sigmaRingType` + * section `measurable_fun_measurable` + +- in `lebesgue_integral.v`: + + lemma `ge0_integral_bigcup` + + lemma `ge0_emeasurable_fun_sum` + + from `measurableType` to `sigmaRingType` + * mixin `isMeasurableFun` + * structure `SimpleFun` + * structure `NonNegSimpleFun` + * sections `fimfun_bin`, `mfun_pred`, `sfun_pred`, `simple_bounded` + * lemmas `nnfun_muleindic_ge0`, `mulemu_ge0`, `nnsfun_mulemu_ge0` + * section `sintegral_lemmas` + * lemma `eq_sintegral` + * section `sintegralrM` + +- in `probability.v`: + + lemma `markov` + +### Deprecated + +- in `classical_sets.v`: + + `notin_set` (use `notin_setE` instead) + +### Removed + +- in `forms.v` + + canonical `rev_mulmx` + + structure `revop` + +- in `reals.v` + + lemma `inf_lower_bound` (use `inf_lb` instead) + +- in `derive.v`: + + definition `mulr_rev` + + canonical `rev_mulr` + + lemmas `mulr_is_linear`, `mulr_rev_is_linear` + +- in `measure.v`: + + lemmas `prod_salgebra_set0`, `prod_salgebra_setC`, `prod_salgebra_bigcup` + (use `measurable0`, `measurableC`, `measurable_bigcup` instead) + +- in `lebesgue_measure.v`: + + lemmas `stracexx`, `strace_measurable` + +- in `lebesgue_integral.v`: + + `integrablerM`, `integrableMr` (were deprecated since version 0.6.4) ## [1.1.0] - 2024-03-31 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 72f18a1b0..67bb43c3b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,295 +4,16 @@ ### Added -- in `classical_sets.v`: - + lemma `bigcup_recl` - -- in `sequences.v`: - + lemma `nneseries_recl` - -- in file `mathcomp_extra.v`: - + module `Order` - * definitions `disp_t`, `default_display` - -- in `measure.v`: - + definition `subset_sigma_subadditive` - + factory `isSubsetOuterMeasure` - -- in file `classical_sets.v` - + notations `\bigcup_(i >= n) F i` and `\bigcap_(i >= n) F i` - + lemmas `bigcup_addn`, `bigcap_addn` - -- in file `sequences.v` - + lemma `nneseries_addn` -- in `lebesgue_integral.v`: - + lemmas `integrableMl`, `integrableMr` - -- in `realfun.v` - + lemmas `total_variation_nondecreasing`, `total_variation_bounded_variation` -- new file `theories/all_analysis.v` - -- in `normedtype.v`: - + lemma `not_near_at_leftP` -- in `classical_sets.v`: - + lemmas `setD_bigcup`, `nat_nonempty` - + hint `nat_nonempty` - -- in `measure.v`: - + structure `SigmaRing`, notation `sigmaRingType` - + factory `isSigmaRing` - + lemma `bigcap_measurable` for `sigmaRingType` - + lemma `setDI_semi_setD_closed` - + lemmas `powerset_lambda_system`, `lambda_system_smallest`, `sigmaRingType_lambda_system` - + definitions `niseq_closed`, `sigma_ring` (notation `<>`), - `monotone` (notation `<>`) - + lemmas `smallest_sigma_ring`, `sigma_ring_monotone`, `g_sigma_ring_monotone`, - `sub_g_sigma_ring`, `setring_monotone_sigma_ring`, `g_monotone_monotone`, - `g_monotone_setring`, `g_monotone_g_sigma_ring`, `monotone_setring_sub_g_sigma_ring` - -- in `classical_sets.v`: - + lemma `bigcup_bigsetU_bigcup` - + lemmas `setDUD`, `setIDAC` - -- in `measure.v`: - + lemmas `powerset_sigma_ring`, `g_sigma_ring_strace`, `setI_g_sigma_ring`, - `subset_strace` - -- in `lebesgue_measure.v`: - + lemma `measurable_fun_ler` - -- in `measure.v`: - + lemma `measurable_and` - -- in `signed.v`: - + lemma `onem_nonneg_proof`, definition `onem_nonneg` - -- in `esum.v`: - + lemma `nneseries_sum_bigcup` - -- in `lebesgue_measurable.v`: - + lemmas `measurable_natmul`, `measurable_fun_pow` - -- in `probability.v`: - + definition `bernoulli_pmf` - + lemmas `bernoulli_pmf_ge0`, `bernoulli_pmf1`, `measurable_bernoulli_pmf` - + definition `bernoulli` (equipped with the `probability` structure) - + lemmas `bernoulli_dirac`, `bernoulliE`, `integral_bernoulli`, `measurable_bernoulli`, - `measurable_bernoulli2` - + definition `binomial_pmf` - + lemmas `binomial_pmf_ge0`, `measurable_binomial_pmf` - + definitions `binomial_prob` (equipped with the `probability` structure), `bin_prob` - + lemmas `bin_prob0`, `bin_prob1`, `binomial_msum`, `binomial_probE`, `integral_binomial`, - `integral_binomial_prob`, `measurable_binomial_prob` - + definition `uniform_pdf` - + lemmas `measurable_uniform_pdf`, `integral_uniform_pdf`, `integral_uniform_pdf1` - + definition `uniform_prob` (equipped with the `probability` structure) - + lemmas `dominates_uniform_prob`, `integral_uniform` - -- in `measure.v`: - + lemma `measurableID` - -- in `mathcomp_extra.v`: - + lemma `Pos_to_natE` - -- in `Rstruct.v`: - + lemma `IZRposE` - -- in `measure.v`: - + lemma `strace_sigma_ring` - ### Changed -- in `forms.v`: - + notation ``` u ``_ _ ``` - -- in `trigo.v`: - + definitions `sin`, `cos`, `acos`, `asin`, `atan` are now HB.locked -- in `sequences.v`: - + definition `expR` is now HB.locked - -- in `measure.v`: - + change the hypothesis of `measurable_fun_bool` - + mixin `AlgebraOfSets_isMeasurable` renamed to `hasMeasurableCountableUnion` - and made to inherit from `SemiRingOfSets` - -- in `measure.v`: - + rm hypo and variable in lemma `smallest_monotone_classE` - and rename to `smallest_lambda_system` - + rm hypo in lemma `monotone_class_g_salgebra` and renamed - to `g_salgebra_lambda_system` - + rm hypo in lemma `monotone_class_subset` and renamed to - `lambda_system_subset` - + notation `<>` changed to `<>`, - notation `<>` changed to `<>` - -- moved from `lebesgue_measure.v` to `measure.v`: - + definition `strace` - + lemma `sigma_algebra_strace` - -- in `sequences.v`: - + equality reversed in lemma `eq_bigcup_seqD` -- in `sequences.v`: - + `eq_bigsetU_seqD` renamed to `nondecreasing_bigsetU_seqD` - and equality reversed - ### Renamed -- in `constructive_ereal.v`: - + `gee_pmull` -> `gee_pMl` - + `gee_addl` -> `geeDl` - + `gee_addr` -> `geeDr` - + `gte_addl` -> `gteDl` - + `gte_addr` -> `gteDr` - + `lte_subl_addr` -> `lteBlDr` - + `lte_subl_addl` -> `lteBlDl` - + `lte_subr_addr` -> `lteBrDr` - + `lte_subr_addl` -> `lteBrDl` - + `lee_subl_addr` -> `leeBlDr` - + `lee_subl_addl` -> `leeBlDl` - + `lee_subr_addr` -> `leeBrDr` - + `lee_subr_addl` -> `leeBrDl` - -- in `measure.v`: - + `sub_additive` -> `subadditive` - + `sigma_sub_additive` -> `measurable_subset_sigma_subadditive` - + `content_sub_additive` -> `content_subadditive` - + `ring_sigma_sub_additive` -> `ring_sigma_subadditive` - + `Content_SubSigmaAdditive_isMeasure` -> `Content_SigmaSubAdditive_isMeasure` - + `measure_sigma_sub_additive` -> `measure_sigma_subadditive` - + `measure_sigma_sub_additive_tail` -> `measure_sigma_subadditive_tail` - -- in `classical_sets.v`: - + `notin_set` -> `notin_setE` - -- in `signed.v`: - + `num_le_maxr` -> `num_le_max` - + `num_le_maxl` -> `num_ge_max` - + `num_le_minr` -> `num_le_min` - + `num_le_minl` -> `num_ge_min` - + `num_lt_maxr` -> `num_lt_max` - + `num_lt_maxl` -> `num_gt_max` - + `num_lt_minr` -> `num_lt_min` - + `num_lt_minl` -> `num_gt_min` - -- in `constructive_ereal.v`: - + `num_lee_maxr` -> `num_lee_max` - + `num_lee_maxl` -> `num_gee_max` - + `num_lee_minr` -> `num_lee_min` - + `num_lee_minl` -> `num_gee_min` - + `num_lte_maxr` -> `num_lte_max` - + `num_lte_maxl` -> `num_gte_max` - + `num_lte_minr` -> `num_lte_min` - + `num_lte_minl` -> `num_gte_min` -- in `measure.v`: - + `bigcap_measurable` -> `bigcap_measurableType` - -- in `lebesgue_integral.v`: - + `integral_measure_add` -> `ge0_integral_measure_add` - + `integral_pushforward` -> `ge0_integral_pushforward` -- in `measure.v`: - + `monotone_class` -> `lambda_system` - + `monotone_class_g_salgebra` -> `g_sigma_algebra_lambda_system` - + `smallest_monotone_classE` -> `smallest_lambda_system` - + `dynkin_monotone` -> `dynkin_lambda_system` - + `dynkin_g_dynkin` -> `g_dynkin_dynkin` - + `salgebraType` -> `g_sigma_algebraType` - + `g_salgebra_measure_unique_trace` -> `g_sigma_algebra_measure_unique_trace` - + `g_salgebra_measure_unique_cover` -> `g_sigma_algebra_measure_unique_cover` - + `g_salgebra_measure_unique` -> `g_sigma_algebra_measure_unique` - + `setI_closed_gdynkin_salgebra` -> `setI_closed_g_dynkin_g_sigma_algebra` - ### Generalized -- in `Rstruct.v`: - + lemmas `RinvE`, `RdivE` - -- in `constructive_ereal.v`: - + `gee_pMl` (was `gee_pmull`) - -- in `sequences.v`: - + lemmas `eseries0`, `nneseries_split` - -- in `lebesgue_integral.v`: - + lemma `ge0_integral_bigcup` -- in `measure.v`: - + lemmas `outer_measure_subadditive`, `outer_measureU2` (from `semiRingOfSetType` to `Type`) - + lemmas `caratheodory_measurable_mu_ext`, `measurableM`, `measure_dominates_trans`, `ess_sup_ge0` - definitions `preimage_classes`, `measure_dominates`, `ess_sup` - (from `measurableType` to `semiRingOfSetsType`) - + lemmas ` measurable_prod_measurableType`, `measurable_prod_g_measurableTypeR` (from `measurableType` to `algebraOfSetsType`) - -- in `lebesgue_integral.v`: - + lemma `ge0_emeasurable_fun_sum` - -- in `probability.v`: - + lemma `markov` -- in `measure.v`: - + from `measurableType` to `sigmaRingType` - * lemmas `bigcup_measurable`, `bigcapT_measurable` - * definition `measurable_fun` - * lemmas `measurable_id`, `measurable_comp`, `eq_measurable_fun`, `measurable_cst`, - `measurable_fun_bigcup`, `measurable_funU`, `measurable_funS`, `measurable_fun_if` - * lemmas `semi_sigma_additiveE`, `sigma_additive_is_additive`, `measure_sigma_additive` - * definitions `pushforward`, `dirac` - * lemmas `diracE`, `dirac0`, `diracT`, `finite_card_sum`, `finite_card_dirac`, `infinite_card_dirac` - * definitions `msum`, `measure_add`, `mscale`, `mseries`, `mrestr` - * lemmas `msum_mzero`, `measure_addE` - * definition `sfinite_measure` - * mixin `isSFinite`, structure `SFiniteMeasure` - * structure `FiniteMeasure` - * factory `Measure_isSFinite` - * lemma `negligible_bigcup` - * definition `ae_eq` - * lemmas `ae_eq0`, `ae_eq_comp`, `ae_eq_funeposneg`, `ae_eq_refl`, `ae_eq_sym`, - `ae_eq_trans`, `ae_eq_sub`, `ae_eq_mul2r`, `ae_eq_mul2l`, `ae_eq_mul1l`, - `ae_eq_abse`, `ae_eq_subset` - + from `measurableType` to `sigmaRingType` and from `realType` to `realFieldType` - * definition `mzero` - + from `realType` to `realFieldType`: - * lemma `sigma_finite_mzero` - -- in `lebesgue_integral.v`: - + from `measurableType` to `sigmaRingType` - * mixin `isMeasurableFun` - * structure `SimpleFun` - * structure `NonNegSimpleFun` - * sections `fimfun_bin`, `mfun_pred`, `sfun_pred`, `simple_bounded` - * lemmas `nnfun_muleindic_ge0`, `mulemu_ge0`, `nnsfun_mulemu_ge0` - * section `sintegral_lemmas` - * lemma `eq_sintegral` - * section `sintegralrM` - -- in `lebesgue_measure.v`: - + from `measurableType` to `sigmaRingType` - * section `measurable_fun_measurable` - ### Deprecated -- in `classical_sets.v`: - + `notin_set` (use `notin_setE` instead) - ### Removed -- in `lebesgue_integral.v`: - + `integrablerM`, `integrableMr` (were deprecated since version 0.6.4) - -- in `measure.v`: - + lemmas `prod_salgebra_set0`, `prod_salgebra_setC`, `prod_salgebra_bigcup` - (use `measurable0`, `measurableC`, `measurable_bigcup` instead) -- in `derive.v`: - + definition `mulr_rev` - + canonical `rev_mulr` - + lemmas `mulr_is_linear`, `mulr_rev_is_linear` - -- in `forms.v` - + canonical `rev_mulmx` - + structure `revop` - -- in `reals.v` - + lemma `inf_lower_bound` (use `inf_lb` instead) -- in `lebesgue_measure.v`: - + lemmas `stracexx`, `strace_measurable` - ### Infrastructure ### Misc diff --git a/INSTALL.md b/INSTALL.md index fa0f98e2b..d1cb34484 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.1.0 +$ opam install coq-mathcomp-analysis.1.2.0 ``` 4. Everytime you want to work in this same context, you need to type ``` diff --git a/README.md b/README.md index 7b5f14dae..74b99abd9 100644 --- a/README.md +++ b/README.md @@ -84,7 +84,7 @@ We try to preserve backward compatibility as best as we can. ## Documentation Each file is documented in its header -([`coq2html`](https://github.com/xavierleroy/coq2html) [documentation for the last version](https://math-comp.github.io/analysis/htmldoc_1_1_0/index.html)). +([documentation for the last version](https://math-comp.github.io/analysis/htmldoc_1_2_0/index.html), using [`coq2html`](https://github.com/xavierleroy/coq2html)). Overview presentation: [Classical Analysis with Coq](https://perso.crans.org/cohen/CoqWS2018.pdf) (2018) @@ -99,19 +99,19 @@ Other work using MathComp-Analysis: ## Mathematical structures MathComp-Analysis adds mathematical structures on top of MathComp's ones. -The following inheritance diagram displays the resulting hiearchy +The following inheritance diagram displays the resulting hierarchy as of version 1.1.0 (excluding most MathComp structures). The structures introduced by MathComp-Analysis are highlighted. (See `topology.v`, `normedtype.v`, `reals.v`, `measure.v`.) -Main_inheritance_graph +Main_inheritance_graph ### Hierarchies of functions | Functions | Functions with a finite image | Measures | Kernels | |:----------:|:-----------------------------:|:--------:|:-------:| -| Functions | Functions_with_a_finite_image | Measures | Kernels | +| Functions | Functions_with_a_finite_image | Measures | Kernels | | (see `functions.v`) | (see `cardinality.v`, `lebesgue_integral.v`) | (see `measure.v`, `charge.v`) | (see `kernel.v`) | ## Development information diff --git a/etc/hierarchy_fimfun.png b/etc/hierarchy_fimfun.1.1.0.png similarity index 100% rename from etc/hierarchy_fimfun.png rename to etc/hierarchy_fimfun.1.1.0.png diff --git a/etc/hierarchy_functions.png b/etc/hierarchy_functions.1.1.0.png similarity index 100% rename from etc/hierarchy_functions.png rename to etc/hierarchy_functions.1.1.0.png diff --git a/etc/hierarchy_kernel.png b/etc/hierarchy_kernel.1.1.0.png similarity index 100% rename from etc/hierarchy_kernel.png rename to etc/hierarchy_kernel.1.1.0.png diff --git a/etc/hierarchy_main.png b/etc/hierarchy_main.1.1.0.png similarity index 100% rename from etc/hierarchy_main.png rename to etc/hierarchy_main.1.1.0.png diff --git a/etc/hierarchy_measure.png b/etc/hierarchy_measure.1.1.0.png similarity index 100% rename from etc/hierarchy_measure.png rename to etc/hierarchy_measure.1.1.0.png