From bf1639842517b1735e145839eb542b1dfc5827e2 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 18 Dec 2024 23:13:57 +0100 Subject: [PATCH] changelog for 1.7.1 --- CHANGELOG.md | 118 +++++++++++++++++++++++++++++++++++++++- CHANGELOG_UNRELEASED.md | 106 ------------------------------------ 2 files changed, 117 insertions(+), 107 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a3a1f0e54..c00beb797 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,122 @@ # Changelog -Latest releases: [[1.7.0] - 2024-11-22](#170---2024-11-22) and [[1.6.0] - 2024-10-25](#160---2024-10-25) +Latest releases: [[1.7.1] - 2024-12-19](#171---2024-12-19), [[1.7.0] - 2024-11-22](#170---2024-11-22) and [[1.6.0] - 2024-10-25](#160---2024-10-25) + +## [1.7.1] - 2024-12-19 + +### Added + +- in `num_topology.v`: + + lemma `in_continuous_mksetP` + +- in `normedtype.v`: + + lemmas `continuous_within_itvcyP`, `continuous_within_itvNycP` + +- in `mathcomp_extra.v`: + + lemma `partition_disjoint_bigfcup` +- in `lebesgue_measure.v`: + + lemma `measurable_indicP` + +- in `lebesgue_integral.v`: + + definition `dyadic_approx` (was `Let A`) + + definition `integer_approx` (was `Let B`) + + lemma `measurable_sum` + + lemma `integrable_indic` + + lemmas `integrable_pushforward`, `integral_pushforward` + + lemma `integral_measure_add` + +- in `constructive_ereal.v`: + + notations `\prod` in scope ereal_scope + + lemmas `prode_ge0`, `prode_fin_num` + +- in `probability.v`: + + lemma `expectation_def` + + notation `'M_` + + lemma `integral_distribution` (existing lemma `integral_distribution` has been renamed) + +- in `measure.v`: + + lemma `countable_bigcupT_measurable` + + definition `discrete_measurable` + + lemmas `discrete_measurable0`, `discrete_measurableC`, `discrete_measurableU` + +- in file `realfun.v`: + + lemma `cvg_nbhsP` + +- in `lebesgue_measure.v`: + + lemma `measurable_powRr` + +### Changed + +- in `lebesgue_integrale.v` + + change implicits of `measurable_funP` + +### Renamed + +- in `lebesgue_measure.v`: + + `measurable_fun_indic` -> `measurable_indic` + + `emeasurable_fun_sum` -> `emeasurable_sum` + + `emeasurable_fun_fsum` -> `emeasurable_fsum` + + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum` + +- in `probability.v`: + + `expectationM` -> `expectationZl` + + `integral_distribution` -> `ge0_integral_distribution` + +- in `classical_sets.v`: + + `preimage_itv_o_infty` -> `preimage_itvoy` + + `preimage_itv_c_infty` -> `preimage_itvcy` + + `preimage_itv_infty_o` -> `preimage_itvNyo` + + `preimage_itv_infty_c` -> `preimage_itvNyc` + +- in `constructive_ereal.v`: + + `maxeMr` -> `maxe_pMr` + + `maxeMl` -> `maxe_pMl` + + `mineMr` -> `mine_pMr` + + `mineMl` -> `mine_pMl` + +- file `homotopy_theory/path.v` -> `homotopy_theory/continuous_path.v` + +### Generalized + +- in `sequences.v`: + + lemmas `cvg_restrict`, `cvg_centern`, `cvg_shiftn cvg_shiftS` + +- in `probability.v`: + + definition `random_variable` + + lemmas `notin_range_measure`, `probability_range` + + definition `distribution` + + lemma `probability_distribution`, `integral_distribution` + + mixin `MeasurableFun_isDiscrete` + + structure `discreteMeasurableFun` + + definition `discrete_random_variable` + + lemma `dRV_dom_enum` + + definitions `dRV_dom`, `dRV_enum`, `enum_prob` + + lemmas `distribution_dRV`, `sum_enum_prob` + +- in `lebesgue_integral.v`: + + lemma `measurable_sfunP` + +### Deprecated + +- in file `lebesgue_integral.v`: + + lemma `approximation` + +### Removed + +- in `lebesgue_integral.v`: + + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`) + + notation `measurable_fun_indic` (deprecation since 0.6.3) + +- in `constructive_ereal.v` + + notation `lee_opp` (deprecated since 0.6.5) + + notation `lte_opp` (deprecated since 0.6.5) + +- in `measure.v`: + + `dynkin_setI_bigsetI` (use `big_ind` instead) + +- in `lebesgue_measurable.v`: + + notation `measurable_fun_power_pos` (deprecated since 0.6.3) + + notation `measurable_power_pos` (deprecated since 0.6.4) ## [1.7.0] - 2024-11-22 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c3300c2f6..67bb43c3b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,122 +4,16 @@ ### Added -- in `num_topology.v`: - + lemma `in_continuous_mksetP` - -- in `normedtype.v`: - + lemmas `continuous_within_itvcyP`, `continuous_within_itvNycP` - -- in `mathcomp_extra.v`: - + lemma `partition_disjoint_bigfcup` -- in `lebesgue_measure.v`: - + lemma `measurable_indicP` - -- in `lebesgue_integral.v`: - + definition `dyadic_approx` (was `Let A`) - + definition `integer_approx` (was `Let B`) - + lemma `measurable_sum` - + lemma `integrable_indic` - -- in `constructive_ereal.v`: - + notations `\prod` in scope ereal_scope - + lemmas `prode_ge0`, `prode_fin_num` -- in `probability.v`: - + lemma `expectation_def` - + notation `'M_` - -- in `lebesgue_integral.v`: - + lemmas `integrable_pushforward`, `integral_pushforward` - + lemma `integral_measure_add` - -- in `probability.v` - + lemma `integral_distribution` (existing lemma `integral_distribution` has been renamed) - -- in `measure.v`: - + lemma `countable_bigcupT_measurable` - -- in file `realfun.v`: - + lemma `cvg_nbhsP` - -- in `lebesgue_measure.v`: - + lemma `measurable_powRr` - -- in `measure.v`: - + definition `discrete_measurable` - + lemmas `discrete_measurable0`, `discrete_measurableC`, `discrete_measurableU` - ### Changed -- in `lebesgue_integrale.v` - + change implicits of `measurable_funP` - ### Renamed -- in `lebesgue_measure.v`: - + `measurable_fun_indic` -> `measurable_indic` - + `emeasurable_fun_sum` -> `emeasurable_sum` - + `emeasurable_fun_fsum` -> `emeasurable_fsum` - + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum` -- in `probability.v`: - + `expectationM` -> `expectationZl` - -- in `classical_sets.v`: - + `preimage_itv_o_infty` -> `preimage_itvoy` - + `preimage_itv_c_infty` -> `preimage_itvcy` - + `preimage_itv_infty_o` -> `preimage_itvNyo` - + `preimage_itv_infty_c` -> `preimage_itvNyc` - -- in `constructive_ereal.v`: - + `maxeMr` -> `maxe_pMr` - + `maxeMl` -> `maxe_pMl` - + `mineMr` -> `mine_pMr` - + `mineMl` -> `mine_pMl` - -- in `probability.v`: - + `integral_distribution` -> `ge0_integral_distribution` - -- file `homotopy_theory/path.v` -> `homotopy_theory/continuous_path.v` - ### Generalized -- in `sequences.v`: - + lemmas `cvg_restrict`, `cvg_centern`, `cvg_shiftn cvg_shiftS` - -- in `probability.v`: - + definition `random_variable` - + lemmas `notin_range_measure`, `probability_range` - + definition `distribution` - + lemma `probability_distribution`, `integral_distribution` - + mixin `MeasurableFun_isDiscrete` - + structure `discreteMeasurableFun` - + definition `discrete_random_variable` - + lemma `dRV_dom_enum` - + definitions `dRV_dom`, `dRV_enum`, `enum_prob` - + lemmas `distribution_dRV`, `sum_enum_prob` - -- in `lebesgue_integral.v`: - + lemma `measurable_sfunP` - ### Deprecated -- in file `lebesgue_integral.v`: - + lemma `approximation` - ### Removed -- in `lebesgue_integral.v`: - + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`) - + notation `measurable_fun_indic` (deprecation since 0.6.3) -- in `constructive_ereal.v` - + notation `lee_opp` (deprecated since 0.6.5) - + notation `lte_opp` (deprecated since 0.6.5) -- in `measure.v`: - + `dynkin_setI_bigsetI` (use `big_ind` instead) - -- in `lebesgue_measurable.v`: - + notation `measurable_fun_power_pos` (deprecated since 0.6.3) - + notation `measurable_power_pos` (deprecated since 0.6.4) - ### Infrastructure ### Misc