fix CHANGELOG

CHANGELOG_UNRELEASED.md

@@ -18,12 +18,119 @@
 
 - in `normedtype.v`:
   + hints for `at_right_proper_filter` and `at_left_proper_filter`
+
+- in `realfun.v`:
+  + notations `nondecreasing_fun`, `nonincreasing_fun`,
+    `increasing_fun`, `decreasing_fun`
+  + lemmas `cvg_addrl`, `cvg_addrr`, `cvg_centerr`, `cvg_shiftr`,
+    `nondecreasing_cvgr`,
+	`nonincreasing_at_right_cvgr`,
+	`nondecreasing_at_right_cvgr`,
+	`nondecreasing_cvge`, `nondecreasing_is_cvge`,
+	`nondecreasing_at_right_cvge`, `nondecreasing_at_right_is_cvge`,
+	`nonincreasing_at_right_cvge`, `nonincreasing_at_right_is_cvge`
+- in `ereal.v`:
+  + lemmas `ereal_sup_le`, `ereal_inf_le`
+
+- in `normedtype.v`:
+  + definition `lower_semicontinuous`
+  + lemma `lower_semicontinuousP`
+
+- in `numfun.v`:
+  + lemma `patch_indic`
+
+- in `lebesgue_measure.v`
+  + lemma `lower_semicontinuous_measurable`
+
+- in `lebesgue_integral.v`:
+  + definition `locally_integrable`
+  + lemmas `integrable_locally`, `locally_integrableN`, `locally_integrableD`,
+    `locally_integrableB`
+  + definition `iavg`
+  + lemmas `iavg0`, `iavg_ge0`, `iavg_restrict`, `iavgD`
+  + definitions `HL_maximal`
+  + lemmas `HL_maximal_ge0`, `HL_maximalT_ge0`,
+    `lower_semicontinuous_HL_maximal`, `measurable_HL_maximal`,
+    `maximal_inequality`
+
+- in file `measure.v`
+  + add lemmas `ae_eq_subset`, `measure_dominates_ae_eq`.
+
+- in `charge.v`
+  + definition `charge_of_finite_measure` (instance of `charge`)
+  + lemmas `dominates_cscalel`, `dominates_cscaler`
+  + definition `cpushforward` (instance of `charge`)
+  + lemma `dominates_pushforward`
+  + lemma `cjordan_posE`
+  + lemma `jordan_posE`
+  + lemma `cjordan_negE`
+  + lemma `jordan_negE`
+  + lemma `Radon_Nikodym_sigma_finite`
+  + lemma `Radon_Nikodym_fin_num`
+  + lemma `Radon_Nikodym_integral`
+  + lemma `ae_eq_Radon_Nikodym_SigmaFinite`
+  + lemma `Radon_Nikodym_change_of_variables`
+  + lemma `Radon_Nikodym_cscale`
+  + lemma `Radon_Nikodym_cadd`
+  + lemma `Radon_Nikodym_chain_rule`
+
 - in `sequences.v`:
-  + lemma `invr_cvg0` and `invr_cvg_pinfty`
-  + lemma `cvgPninfty_lt`, `cvgPpinfty_near`, `cvgPninfty_near`,
-    `cvgPpinfty_lt_near` and `cvgPninfty_lt_near`
-- in `classical_sets.v`:
-  + notations `\bigcup_(i < n) F` and `\bigcap_(i < n) F`
+  + lemma `minr_cvg_0_cvg_0`
+  + lemma `mine_cvg_0_cvg_fin_num`
+  + lemma `mine_cvg_minr_cvg`
+  + lemma `mine_cvg_0_cvg_0`
+  + lemma `maxr_cvg_0_cvg_0`
+  + lemma `maxe_cvg_0_cvg_fin_num`
+  + lemma `maxe_cvg_maxr_cvg`
+  + lemma `maxe_cvg_0_cvg_0`
+- in `constructive_ereal.v`
+  + lemma `lee_subgt0Pr`
+
+- in `topology.v`:
+  + lemma `nbhs_dnbhs_neq`
+
+- in `normedtype.v`:
+  + lemma `not_near_at_rightP`
+
+- in `realfun.v`:
+  + lemma `cvg_at_right_left_dnbhs`
+  + lemma `cvg_at_rightP`
+  + lemma `cvg_at_leftP`
+  + lemma `cvge_at_rightP`
+  + lemma `cvge_at_leftP`
+  + lemma `lime_sup`
+  + lemma `lime_inf`
+  + lemma `lime_supE`
+  + lemma `lime_infE`
+  + lemma `lime_infN`
+  + lemma `lime_supN`
+  + lemma `lime_sup_ge0`
+  + lemma `lime_inf_ge0`
+  + lemma `lime_supD`
+  + lemma `lime_sup_le`
+  + lemma `lime_inf_sup`
+  + lemma `lim_lime_inf`
+  + lemma `lim_lime_sup`
+  + lemma `lime_sup_inf_at_right`
+  + lemma `lime_sup_inf_at_left`
+
+- in `normedtype.v`:
+  + lemmas `withinN`, `at_rightN`, `at_leftN`, `cvg_at_leftNP`, `cvg_at_rightNP`
+  + lemma `dnbhsN`
+  + lemma `limf_esup_dnbhsN`
+
+- in `topology.v`:
+  + lemma `dnbhs_ball`
+
+- in `normedtype.v`
+  + definitions `limf_esup`, `limf_einf`
+  + lemmas `limf_esupE`, `limf_einfE`, `limf_esupN`, `limf_einfN`
+
+- in `sequences.v`:
+  + lemmas `limn_esup_lim`, `limn_einf_lim`
+
+- in `realfun.v`:
+  + lemmas `lime_sup_lim`, `lime_inf_lim`
 
 - in `boolp.v`:
   + tactic `eqProp`
@@ -160,133 +267,6 @@
     `absurd : ident(H)`, `absurd : { hyp_list(Hs) } constr(H)`,
 	 `absurd : { hyp_list(Hs) } ident(H)`
 
-### Changed
-- in `topology.v`
-  + definition `fct_restrictedUniformType` changed to use `weak_uniformType`
-  + definition `family_cvg_topologicalType` changed to use `sup_uniformType`
-
-- in `constructive_ereal.v`:
-  + lemmas `lee_paddl`, `lte_paddl`, `lee_paddr`, `lte_paddr`,
-    `lte_spaddr`, `lee_pdaddl`, `lte_pdaddl`, `lee_pdaddr`,
-    `lte_pdaddr`, `lte_spdaddr` generalized to `realDomainType`
-- in `constructive_ereal.v`:
-  + generalize `lte_addl`, `lte_addr`, `gte_subl`, `gte_subr`,
-    `lte_daddl`, `lte_daddr`, `gte_dsubl`, `gte_dsubr`
-- in `topology.v`:
-  + lemmas `continuous_subspace0`, `continuous_subspace1`
-
-- in `realfun.v`:
-  + notations `nondecreasing_fun`, `nonincreasing_fun`,
-    `increasing_fun`, `decreasing_fun`
-  + lemmas `cvg_addrl`, `cvg_addrr`, `cvg_centerr`, `cvg_shiftr`,
-    `nondecreasing_cvgr`,
-	`nonincreasing_at_right_cvgr`,
-	`nondecreasing_at_right_cvgr`,
-	`nondecreasing_cvge`, `nondecreasing_is_cvge`,
-	`nondecreasing_at_right_cvge`, `nondecreasing_at_right_is_cvge`,
-	`nonincreasing_at_right_cvge`, `nonincreasing_at_right_is_cvge`
-- in `ereal.v`:
-  + lemmas `ereal_sup_le`, `ereal_inf_le`
-
-- in `normedtype.v`:
-  + definition `lower_semicontinuous`
-  + lemma `lower_semicontinuousP`
-
-- in `numfun.v`:
-  + lemma `patch_indic`
-
-- in `lebesgue_measure.v`
-  + lemma `lower_semicontinuous_measurable`
-
-- in `lebesgue_integral.v`:
-  + definition `locally_integrable`
-  + lemmas `integrable_locally`, `locally_integrableN`, `locally_integrableD`,
-    `locally_integrableB`
-  + definition `iavg`
-  + lemmas `iavg0`, `iavg_ge0`, `iavg_restrict`, `iavgD`
-  + definitions `HL_maximal`
-  + lemmas `HL_maximal_ge0`, `HL_maximalT_ge0`,
-    `lower_semicontinuous_HL_maximal`, `measurable_HL_maximal`,
-    `maximal_inequality`
-
-- in file `measure.v`
-  + add lemmas `ae_eq_subset`, `measure_dominates_ae_eq`.
-
-- in `charge.v`
-  + definition `charge_of_finite_measure` (instance of `charge`)
-  + lemmas `dominates_cscalel`, `dominates_cscaler`
-  + definition `cpushforward` (instance of `charge`)
-  + lemma `dominates_pushforward`
-  + lemma `cjordan_posE`
-  + lemma `jordan_posE`
-  + lemma `cjordan_negE`
-  + lemma `jordan_negE`
-  + lemma `Radon_Nikodym_sigma_finite`
-  + lemma `Radon_Nikodym_fin_num`
-  + lemma `Radon_Nikodym_integral`
-  + lemma `ae_eq_Radon_Nikodym_SigmaFinite`
-  + lemma `Radon_Nikodym_change_of_variables`
-  + lemma `Radon_Nikodym_cscale`
-  + lemma `Radon_Nikodym_cadd`
-  + lemma `Radon_Nikodym_chain_rule`
-
-- in `sequences.v`:
-  + lemma `minr_cvg_0_cvg_0`
-  + lemma `mine_cvg_0_cvg_fin_num`
-  + lemma `mine_cvg_minr_cvg`
-  + lemma `mine_cvg_0_cvg_0`
-  + lemma `maxr_cvg_0_cvg_0`
-  + lemma `maxe_cvg_0_cvg_fin_num`
-  + lemma `maxe_cvg_maxr_cvg`
-  + lemma `maxe_cvg_0_cvg_0`
-- in `constructive_ereal.v`
-  + lemma `lee_subgt0Pr`
-
-- in `topology.v`:
-  + lemma `nbhs_dnbhs_neq`
-
-- in `normedtype.v`:
-  + lemma `not_near_at_rightP`
-
-- in `realfun.v`:
-  + lemma `cvg_at_right_left_dnbhs`
-  + lemma `cvg_at_rightP`
-  + lemma `cvg_at_leftP`
-  + lemma `cvge_at_rightP`
-  + lemma `cvge_at_leftP`
-  + lemma `lime_sup`
-  + lemma `lime_inf`
-  + lemma `lime_supE`
-  + lemma `lime_infE`
-  + lemma `lime_infN`
-  + lemma `lime_supN`
-  + lemma `lime_sup_ge0`
-  + lemma `lime_inf_ge0`
-  + lemma `lime_supD`
-  + lemma `lime_sup_le`
-  + lemma `lime_inf_sup`
-  + lemma `lim_lime_inf`
-  + lemma `lim_lime_sup`
-  + lemma `lime_sup_inf_at_right`
-  + lemma `lime_sup_inf_at_left`
-
-- in `normedtype.v`:
-  + lemmas `withinN`, `at_rightN`, `at_leftN`, `cvg_at_leftNP`, `cvg_at_rightNP`
-  + lemma `dnbhsN`
-  + lemma `limf_esup_dnbhsN`
-
-- in `topology.v`:
-  + lemma `dnbhs_ball`
-
-- in `normedtype.v`
-  + definitions `limf_esup`, `limf_einf`
-  + lemmas `limf_esupE`, `limf_einfE`, `limf_esupN`, `limf_einfN`
-
-- in `sequences.v`:
-  + lemmas `limn_esup_lim`, `limn_einf_lim`
-
-- in `realfun.v`:
-  + lemmas `lime_sup_lim`, `lime_inf_lim`
 
 - in `boolp.v`:
   + tactic `eqProp`
@@ -340,7 +320,7 @@
 
 -in `boolp.v`
   - lemmas `orC` and `andC` now use `commutative`
-
+  
 ### Renamed
 
 - in `exp.v`: