fix changelog, doc

CHANGELOG_UNRELEASED.md

@@ -27,80 +27,13 @@
   + new lemmas `pointwise_almost_uniform`, and 
     `ae_pointwise_almost_uniform`.
 
-- in `exp.v`:
-  + lemmas `power_posrM`, `gt0_ler_power_pos`,
-    `gt0_power_pos`, `norm_power_pos`, `lt0_norm_power_pos`,
-    `power_posB`
-  + lemmas `powere_posrM`, `powere_posAC`, `gt0_powere_pos`,
-    `powere_pos_eqy`, `eqy_powere_pos`, `powere_posD`, `powere_posB`
-
 - in `mathcomp_extra.v`:
   + definition `min_fun`, notation `\min`
 - in `classical_sets.v`:
   + lemmas `set_predC`, `preimage_true`, `preimage_false`
 - in `lebesgue_measure.v`:
   + lemmas `measurable_fun_ltr`, `measurable_minr`
-  + lemmas `set_eq_le`, `set_neq_lt`,
-  + new lemma `trivIset1`.
-- in `set_interval.v`:
-  + lemma `set_lte_bigcup`
-- in `lebesgue_integral.v`:
-  + lemmas `emeasurable_fun_lt`, `emeasurable_fun_le`, `emeasurable_fun_eq`,
-    `emeasurable_fun_neq`
-  + lemma `integral_ae_eq`
-- in file `kernel.v`,
-  + new definitions `kseries`, `measure_fam_uub`, `kzero`, `kdirac`,
-    `prob_pointed`, `mset`, `pset`, `pprobability`, `kprobability`, `kadd`,
-    `mnormalize`, `knormalize`, `kcomp`, and `mkcomp`.
-  + new lemmas `eq_kernel`, `measurable_fun_kseries`, `integral_kseries`,
-    `measure_fam_uubP`, `eq_sfkernel`, `kzero_uub`,
-    `sfinite_kernel`, `sfinite_kernel_measure`, `finite_kernel_measure`,
-    `measurable_prod_subset_xsection_kernel`,
-    `measurable_fun_xsection_finite_kernel`,
-    `measurable_fun_xsection_integral`,
-    `measurable_fun_integral_finite_kernel`,
-    `measurable_fun_integral_sfinite_kernel`, `lt0_mset`, `gt1_mset`,
-    `kernel_measurable_eq_cst`, `kernel_measurable_neq_cst`, `kernel_measurable_fun_eq_cst`,
-    `measurable_fun_kcomp_finite`, `mkcomp_sfinite`,
-    `measurable_fun_mkcomp_sfinite`, `measurable_fun_preimage_integral`,
-    `measurable_fun_integral_kernel`, and `integral_kcomp`.
-  + lemma `measurable_fun_mnormalize`
-- in `ereal.v`:
-  + lemmas `compreDr`, `compreN`
-- in `constructive_ereal.v`:
-  + lemmas `lee_sqr`, `lte_sqr`, `lee_sqrE`, `lte_sqrE`, `sqre_ge0`,
-    `EFin_expe`, `sqreD`, `sqredD`
-- in `probability.v`
-  + definition of `covariance`
-  + lemmas `expectation_sum`, `covarianceE`, `covarianceC`,
-    `covariance_fin_num`, `covariance_cst_l`, `covariance_cst_r`,
-    `covarianceZl`, `covarianceZr`, `covarianceNl`, `covarianceNr`,
-    `covarianceNN`, `covarianceDl`, `covarianceDr`, `covarianceBl`,
-    `covarianceBr`, `variance_fin_num`, `varianceZ`, `varianceN`,
-    `varianceD`, `varianceB`, `varianceD_cst_l`, `varianceD_cst_r`,
-    `varianceB_cst_l`, `varianceB_cst_r`
-- in `functions.v`:
-  + lemma `sumrfctE`
-- in `lebesgue_integral.v`:
-  + lemma `integrable_sum`
-- in `probability.v`
-  + lemma `cantelli`
 
-- in `measure.v`:
-  + lemmas `measurable_pair1`, `measurable_pair2`
-  + lemma `covariance_le`
-- in `mathcomp_extra.v`
-  + definition `coefE` (will be in MC 2.1/1.18)
-  + lemmas `deg2_poly_canonical`, `deg2_poly_factor`, `deg2_poly_min`,
-    `deg2_poly_minE`, `deg2_poly_ge0`, `Real.deg2_poly_factor`,
-    `deg_le2_poly_delta_ge0`, `deg_le2_poly_ge0`
-    (will be in MC 2.1/1.18)
-  + lemma `deg_le2_ge0`
-  + new lemmas `measurable_subring`, and `semiring_sigma_additive`.
-  + added factory `Content_SubSigmaAdditive_isMeasure`
-
-- in `lebesgue_integral.v`:
-  + lemmas `integrableP`, `measurable_int`
 - in `exp.v`:
   + lemmas `power_posrM`, `gt0_ler_power_pos`,
     `gt0_power_pos`, `norm_power_pos`, `lt0_norm_power_pos`,
@@ -121,53 +54,6 @@
 - in `boolp.v`:
   + `mextentionality` -> `mextensionality`
   + `extentionality` -> `extensionality`
-- in `derive.v`:
-  + `Rmult_rev` -> `mulr_rev`
-  + `rev_Rmult` -> `rev_mulr`
-  + `Rmult_is_linear` -> `mulr_is_linear`
-  + `Rmult_linear` -> `mulr_linear`
-  + `Rmult_rev_is_linear` -> `mulr_rev_is_linear`
-  + `Rmult_rev_linear` -> `mulr_rev_linear`
-  + `Rmult_bilinear` -> `mulr_bilinear`
-  + `is_diff_Rmult` -> `is_diff_mulr`
-- in `lebesgue_measure.v`
-  + `measurable_funN` -> `measurable_oppr`
-  + `emeasurable_fun_minus` -> `measurable_oppe`
-  + `measurable_fun_abse` -> `measurable_abse`
-  + `measurable_EFin` -> `measurable_image_EFin`
-  + `measurable_fun_EFin` -> `measurable_EFin`
-  + `measurable_fine` -> `measurable_image_fine`
-  + `measurable_fun_fine` -> `measurable_fine`
-  + `measurable_fun_normr` -> `measurable_normr`
-  + `measurable_fun_exprn` -> `measurable_exprn`
-  + `emeasurable_fun_max` -> `measurable_maxe`
-  + `emeasurable_fun_min` -> `measurable_mine`
-  + `measurable_fun_max` -> `measurable_maxr`
-  + `measurable_fun_er_map` -> `measurable_er_map`
-  + `emeasurable_fun_funepos` -> `measurable_funepos`
-  + `emeasurable_fun_funeneg` -> `measurable_funeneg`
-  + `measurable_funrM` -> `measurable_mulrl`
-- in `measure.v`:
-  + `measurable_fun_id` -> `measurable_id`
-  + `measurable_fun_cst` -> `measurable_cst`
-  + `measurable_fun_comp` -> `measurable_comp`
-  + `measurable_funT_comp` -> `measurableT_comp`
-  + `measurable_fun_fst` -> `measurable_fst`
-  + `measurable_fun_snd` -> `measurable_snd`
-  + `measurable_fun_swap` -> `measurable_swap`
-  + `measurable_fun_pair` -> `measurable_fun_prod`
-  + `isMeasure0` -> ``Content_isMeasure`
-- in `lebesgue_integral.v`:
-  + `measurable_fun_indic` -> `measurable_indic`
-- in `measure.v`:
-  + `Hahn_ext` -> `measure_extension`
-  + `Hahn_ext_ge0` -> `measure_extension_ge0`
-  + `Hahn_ext_sigma_additive` -> `measure_extension_semi_sigma_additive`
-  + `Hahn_ext_unique` -> `measure_extension_unique`
-  + `RingOfSets_from_semiRingOfSets` -> `SemiRingOfSets_isRingOfSets`
-  + `AlgebraOfSets_from_RingOfSets` -> `RingOfSets_isAlgebraOfSets`
-  + `Measurable_from_algebraOfSets` -> `AlgebraOfSets_isMeasurable`
-  + `ring_sigma_additive` -> `ring_semi_sigma_additive`
 - in `exp.v`:
   + `expK` -> `expRK`
 
@@ -180,9 +66,6 @@
 
 ### Deprecated
 
-- in `lebesgue_measure.v`:
-  + lemma `measurable_fun_sqr` (use `measurable_exprn` instead)
-  + lemma `measurable_fun_opp` (use `measurable_oppr` instead)
 - in `exp.v`:
   + lemmas `convex_expR`, `ler_power_pos`
 

theories/exp.v

@@ -24,7 +24,7 @@ Require Import itv convex.
 (*              e `^ r == power function, in ereal_scope (assumes e >= 0)     *)
 (*          riemannR a == sequence n |-> 1 / (n.+1) `^ a where a has a type   *)
 (*                        of type realType                                    *)
-(*       e `^?(r +? s) == validity condition for the distrubutivity of        *)
+(*       e `^?(r +? s) == validity condition for the distributivity of        *)
 (*                        the power of the addition, in ereal_scope           *)
 (*                                                                            *)
 (******************************************************************************)