fix changelog

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -47,16 +47,13 @@
   + definitions `next_prime`, `prime_seq`
   + lemmas `leq_prime_seq`, `mem_prime_seq`
   + theorem `dvg_sum_inv_prime_seq`
-- in `probability.v`:
-  + lemmas `eq_bernoulli`, `eq_bernoulliV2`
+
+
 - file `mathcomp_extra.v`
   + lemmas `ge_trunc`, `lt_succ_trunc`, `trunc_ge_nat`, `trunc_lt_nat`
 
-- file `Rstruct.v`
-  + lemma `Pos_to_natE` (from `mathcomp_extra.v`)
-  + lemmas `RabsE`, `RdistE`, `sum_f_R0E`, `factE`
-
-- new file `internal_Eqdep_dec.v` (don't use, internal, to be removed)
+- in `measure.v`:
+  + lemma `preimage_set_system_compS`
 
 - in `numfun.v`:
   + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-`
@@ -68,7 +65,7 @@
 
 - in `measure.v`:
   + lemma `preimage_class_comp`
-  + defintions `preimage_display`, `g_sigma_algebra_preimageType`, `g_sigma_algebra_preimage`,
+  + definitions `preimage_display`, `g_sigma_algebra_preimageType`, `g_sigma_algebra_preimage`,
     notations `.-preimage`, `.-preimage.-measurable`
 
 - in `measurable_realfun.v`:
@@ -88,44 +85,6 @@
   + lemma `expectationM_ge0`, `integrable_expectationM`, `independent_integrableM`,
     ` expectation_prod`
 
-- in `numfun.v`
-  + lemmas `funeposE`, `funenegE`, `funepos_comp`, `funeneg_comp`
-
-- in `classical_sets.v`:
-  + lemmas `xsectionE`, `ysectionE`
-
-- file `constructive_ereal.v`:
-  + definition `iter_mule`
-  + lemma `prodEFin`
-
-- file `exp.v`:
-  + lemma `expR_sum`
-
-- file `lebesgue_integral.v`:
-  + lemma `measurable_fun_le`
-
-- in `trigo.v`:
-  + lemma `integral0oo_atan`
-
-- in `measure.v`:
-  + lemmas `mnormalize_id`, `measurable_fun_eqP`
-
-- in `ftc.v`:
-  + lemma `integrable_locally`
-
-- in `constructive_ereal.v`:
-  + lemma `EFin_bigmax`
-
-- in `mathcomp_extra.v`:
-  + lemmas `inr_inj`, `inl_inj`
-
-- in `classical_sets.v`:
-  + lemmas `in_set1`, `inr_in_set_inr`, `inl_in_set_inr`, `mem_image`, `mem_range`, `image_f`
-  + lemmas `inr_in_set_inl`, `inl_in_set_inl`
-
-- in `lebesgue_integral_approximation.v`:
-  + lemma `measurable_prod`
-
 ### Changed
 
 - in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`:
@@ -141,56 +100,6 @@
 
 ### Renamed
 
-- in `kernel.v`:
-  + `isFiniteTransition` -> `isFiniteTransitionKernel`
-- in `lebesgue_integral.v`:
-  + `fubini1a` -> `integrable12ltyP`
-  + `fubini1b` -> `integrable21ltyP`
-  + `measurable_funP` -> `measurable_funPT` (field of `isMeasurableFun` mixin)
-
-- in `mathcomp_extra.v`
-  + `comparable_min_le_min` -> `comparable_le_min2`
-  + `comparable_max_le_max` -> `comparable_le_max2`
-  + `min_le_min` -> `le_min2`
-  + `max_le_max` -> `le_max2`
-  + `real_sqrtC` -> `sqrtC_real`
-- in `measure.v`
-  + `preimage_class` -> `preimage_set_system`
-  + `image_class` -> `image_set_system`
-  + `preimage_classes` -> `g_sigma_preimageU`
-  + `preimage_class_measurable_fun` -> `preimage_set_system_measurable_fun`
-  + `sigma_algebra_preimage_class` -> `sigma_algebra_preimage`
-  + `sigma_algebra_image_class` -> `sigma_algebra_image`
-  + `sigma_algebra_preimage_classE` -> `g_sigma_preimageE`
-  + `preimage_classes_comp` -> `g_sigma_preimageU_comp`
-  
-### 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 `pseudometric_normed_Zmodule.v`:
@@ -212,45 +121,6 @@
 
 - in file `all_reals.v`
   + export of `interval_inference` (now in mathcomp-algebra, but not automatically exported)
-- file `mathcomp_extra.v`
-  + lemma `Pos_to_natE` (moved to `Rstruct.v`)
-  + lemma `deg_le2_ge0` (available as `deg_le2_poly_ge0` in `ssrnum.v`
-    since MathComp 2.1.0)
-- in `sequences.v`:
-  + notations `nneseries_pred0`, `eq_nneseries`, `nneseries0`,
-    `ereal_cvgPpinfty`, `ereal_cvgPninfty` (were deprecated since 0.6.0)
-- in `topology_structure.v`:
-  + lemma `closureC`
-
-- in file `lebesgue_integral.v`:
-  + lemma `approximation`
-
-### Removed
-
-- in `lebesgue_integral.v`:
-  + definition `cst_mfun`
-  + lemma `mfun_cst`
-
-- in `cardinality.v`:
-  + lemma `cst_fimfun_subproof`
-
-- in `lebesgue_integral.v`:
-  + lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead)
-  + lemma `cst_nnfun_subproof` (turned into a `Let`)
-  + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead)
-
-- 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