fix CHANGELOG

CHANGELOG_UNRELEASED.md

@@ -11,12 +11,119 @@
   + `sigma_finite_measure` HB instance on `lebesgue_measure`
 - 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 `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`:
-  + 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`
+  + lemmas `limn_esup_lim`, `limn_einf_lim`
+
+- in `realfun.v`:
+  + lemmas `lime_sup_lim`, `lime_inf_lim`
 
 - in `boolp.v`:
   + tactic `eqProp`
@@ -226,6 +333,14 @@
   + lemma `continuous_uncurry`
   + lemma `curry_continuous`
   + lemma `uncurry_continuous`
+- in `boolp.v`:
+  + tactic `eqProp`
+  + variant `BoolProp`
+  + lemmas `PropB`, `notB`, `andB`, `orB`, `implyB`, `decide_or`, `not_andE`,
+    `not_orE`, `orCA`, `orAC`, `orACA`, `orNp`, `orpN`, `or3E`, `or4E`, `andCA`,
+	 `andAC`, `andACA`, `and3E`, `and4E`, `and5E`, `implyNp`, `implypN`,
+	 `implyNN`, `or_andr`, `or_andl`, `and_orr`, `and_orl`, `exists2E`,
+	 `inhabitedE`, `inhabited_witness`
 
 ### Changed
 
@@ -235,7 +350,7 @@
 
 -in `boolp.v`
   - lemmas `orC` and `andC` now use `commutative`
-
+  
 ### Renamed
 
 ### Generalized