changelog for version 1.2.0

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 `<<sr _ >>`),
+    `monotone` (notation `<<M _ >>`)
+  + 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 `<<m _, _>>` changed to `<<l _, _>>`,
+    notation `<<m _>>` changed to `<<l _>>`
+
+- 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