diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2069b520ec..93d0ebef3c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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` diff --git a/theories/exp.v b/theories/exp.v index 323762c918..3ff8e40f7b 100644 --- a/theories/exp.v +++ b/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 *) (* *) (******************************************************************************)