fixes

- formatting, documentation, changelog, rebase

CHANGELOG_UNRELEASED.md

@@ -13,98 +13,34 @@
   + lemma `EFinB`
   + lemmas `mule_eq0`, `mule_lt0_lt0`, `mule_gt0_lt0`, `mule_lt0_gt0`,
     `pmule_rge0`, `pmule_lge0`, `nmule_lge0`, `nmule_rge0`,
-    `pmule_rgt0`, `pmule_lgt0`, `nmule_lgt0`, `nmule_rgt0`,
+    `pmule_rgt0`, `pmule_lgt0`, `nmule_lgt0`, `nmule_rgt0`
 - in `measure.v`:
   + hints for `measurable0` and `measurableT`
-  + notation `x +? y` for `adde_def x y`
-- in `normedtypes.v`:
-  + lemma `is_intervalPlt`
-  + lemma `cvg_sub0`
-  + lemma `cvg_zero`
-- in `sequences.v`:
-  + lemmas `lt_lim`, `nondecreasing_dvg_lt`, `ereal_lim_sum`
 - in `ereal.v`:
   + lemmas `muleBr`, `muleBl`
   + lemma `eqe_absl`
   + lemma `lee_pmul`
   + lemmas `cover_restr`, `eqcover_r`
-  + lemmas `ge0_adde_def`, `onee_neq0`, `mule0`, `mul0e`
-  + lemmas `mulrEDr`, `mulrEDl`, `ge0_muleDr`, `ge0_muleDl`
-  + lemmas `ge0_sume_distrl`, `ge0_sume_distrr`
-  + lemmas `mulEFin`, `mule_neq0`, `mule_ge0`, `muleA`
-  + lemma `muleE`
-  + lemmas `muleN`, `mulNe`, `muleNN`, `gee_pmull`, `lee_mul01Pr`
-  + lemmas `lte_pdivr_mull`, `lte_pdivr_mulr`, `lte_pdivl_mull`, `lte_pdivl_mulr`,
-    `lte_ndivl_mulr`, `lte_ndivl_mull`, `lte_ndivr_mull`, `lte_ndivr_mulr`
-  + lemmas `lee_pdivr_mull`, `lee_pdivr_mulr`, `lee_pdivl_mull`, `lee_pdivl_mulr`,
-    `lee_ndivl_mulr`, `lee_ndivl_mull`, `lee_ndivr_mull`, `lee_ndivr_mulr`
-  + lemmas `mulrpinfty`, `mulrninfty`, `mulpinftyr`, `mulninftyr`, `mule_gt0`
-  + definition `mulrinfty`
-  + lemmas `mulN1e`, `muleN1`
-  + lemmas `mule_ninfty_pinfty`, `mule_pinfty_ninfty`, `mule_pinfty_pinfty`
-  + lemmas `mule_le0_ge0`, `mule_ge0_le0`, `pmule_rle0`, `pmule_lle0`,
-    `nmule_lle0`, `nmule_rle0`
-  + lemma `sube0`
-- in `normedtype.v`:
-  + lemma `mule_continuous`
-- in `cardinality.v`:
-  + definition `nat_of_pair`, lemma `nat_of_pair_inj`
-- in `topology.v`
-  + lemma `le_bigmax`
-- in `real.v`:
-  + lemmas `floor1`, `floor_neq0`
-- in `sequences.v`:
-  + lemmas `ereal_nondecreasing_opp`, `ereal_nondecreasing_is_cvg`, `ereal_nonincreasing_cvg`,
-    `ereal_nonincreasing_is_cvg`
-- in `normedtype.v`:
-  + lemmas `ereal_is_cvgN`, `ereal_cvgZr`, `ereal_is_cvgZr`, `ereal_cvgZl`, `ereal_is_cvgZl`,
-    `ereal_limZr`, `ereal_limZl`, `ereal_limN`
-- in `topology.v`:
-  + definition `monotonous`
-  + lemma `and_prop_in`
-  + lemmas `mem_inc_segment`, `mem_dec_segment`
-  + lemmas `ltr_distlC`, `ler_distlC`
-  + lemmas `subset_ball_prop_in_itv`, `subset_ball_prop_in_itvcc`
-- in `normedtype.v`:
-  + lemma `bound_itvE`
-  + lemmas `nearN`, `near_in_itv`
-  + lemmas `itvxx`, `itvxxP`, `subset_itv_oo_cc`
-  + lemma `at_right_in_segment`
-  + notations ``f @`[a, b]``, ``g @`]a , b[``
-  + lemmas `mono_mem_image_segment`, `mono_mem_image_itvoo`, `mono_surj_image_segment`,
-    `inc_segment_image`, `dec_segment_image`, `inc_surj_image_segment`, `dec_surj_image_segment`,
-    `inc_surj_image_segmentP`, `dec_surj_image_segmentP`, ``mono_surj_image_segmentP``
-- in `cardinality.v`:
-  + lemmas `surjectiveE`, `surj_image_eq`, `can_surjective`
-- file `realfun.v`:
-  + lemmas `itv_continuous_inj_le`, `itv_continuous_inj_ge`, `itv_continuous_inj_mono`
-  + lemmas `segment_continuous_inj_le`, `segment_continuous_inj_ge`,
-    `segment_can_le`, `segment_can_ge`, `segment_can_mono`
-  + lemmas `segment_continuous_surjective`, `segment_continuous_le_surjective`,
-    `segment_continuous_ge_surjective`
-  + lemmas `continuous_inj_image_segment`, `continuous_inj_image_segmentP`,
-    `segment_continuous_can_sym`, `segment_continuous_le_can_sym`, `segment_continuous_ge_can_sym`,
-    `segment_inc_surj_continuous`, `segment_dec_surj_continuous`, `segment_mono_surj_continuous`
-  + lemmas `segment_can_le_continuous`, `segment_can_ge_continuous`, `segment_can_continuous`
-  + lemmas `near_can_continuousAcan_sym`, `near_can_continuous`, `near_continuous_can_sym`
-  + lemmas `exp_continuous`, `sqr_continuous`, `sqrt_continuous`.
-  + lemma `is_derive1_caratheodory`, `is_derive_inverse`
-  + instance `is_derive1_comp`, `is_deriveV`
-
-- new file `nsatz_realType`
+- in `topology.v` : 
+  + lemmas `cstE`, `compE`, `opprfunE`, `addrfunE`, `mulrfunE`, `scalrfunE`, `exprfunE`
+  + multi-rule `fctE`
 - in `normedtype.v`
   + lemmas `continuous_shift`, `continuous_withinNshiftx`
--in `derive.v`
+- in `derive.v`
   + lemmas `derive1_comp`, `derivable_cst`, `derivable_id`, trigger_derive`
-  + instance `is_derive_id`, `is_derive_Nid`
+  + instances `is_derive_id`, `is_derive_Nid`
+- in `sequences.v`:
+  + lemmas `cvg_series_bounded`, `cvg_to_0_linear`, `lim_cvg_to_0_linear`.
+  + lemma `cvg_sub0`
+  + lemma `cvg_zero`
+- file `realfun.v`:
+  + lemma `is_derive1_caratheodory`, `is_derive_0_is_cst`
+  + instance `is_derive1_comp`
+  + lemmas `is_deriveV`, `is_derive_inverse`
+- new file `nsatz_realType`
 - new file `exp.v`
   + lemma `normr_nneg` (hint)
-  + lemmas `seriesN`, `seriesZr`, `seriesD`, `is_cvg_seriesN`, `lim_seriesN`, `is_cvg_seriesZr`,
-    `lim_seriesZr`, `is_cvg_seriesD`, `lim_seriesD`, `is_cvg_seriesB`, `lim_seriesB`,
-    `lim_series_norm`, `lim_series_le`, `cvg_to_0_linear`, `lim_cvg_to_0_linear`
-  + lemma `continuous_ln`
-  + instance `is_derive1_ln`
-  + definition `pseries`, `pseries_diffs`
+  + definitions `pseries`, `pseries_diffs`
   + facts `is_cvg_pseries_inside_norm`, `is_cvg_pseries_inside`
   + lemmas `pseries_diffsN`, `pseries_diffs_inv_fact`, `pseries_diffs_sumE`,
            `pseries_diffs_equiv`, `is_cvg_pseries_diffs_equiv`, 
@@ -113,13 +49,15 @@
   + instance `is_derive_expR`
   + lemmas `derivable_expR`, `continuous_expR`, `expRxDyMexpx`, `expRxMexpNx_1`
   + lemmas `pexpR_gt1`, `expR_gt0`, `expRN`, `expRD`, `expRMm`
-  + lemmas `expR_gt1`, `expR_lt1, `expRB`, `ltr_expR`, `ler_expR`, `expR_inj`,
+  + lemmas `expR_gt1`, `expR_lt1`, `expRB`, `ltr_expR`, `ler_expR`, `expR_inj`,
     `expR_total_gt1`, `expR_total`
   + definition `ln`
   + fact `ln0`
   + lemmas `expK`, `lnK`, `ln1`, `lnM`, `ln_inj`, `lnV`, `ln_div`, `ltr_ln`, `ler_ln`, `lnX`
   + lemmas `le_ln1Dx`, `ln_sublinear`, `ln_ge0`, `ln_gt0`
-  + definition `exp_fun`, notation `^
+  + lemma `continuous_ln`
+  + instance `is_derive1_ln`
+  + definition `exp_fun`, notation `` `^ ``
   + lemmas `exp_fun_gt0`, `exp_funr1`, `exp_funr0`, `exp_fun1`, `ler_exp_fun`,
     `exp_funD`, `exp_fun_inv`, `exp_fun_mulrn`
   + definition `riemannR`, lemmas `riemannR_gt0`, `dvg_riemannR`
@@ -133,32 +71,44 @@
   + definition `sin`
   + lemmas `sinE`
   + definition `sin_coeff'`
-  + lemmas `sin_coeff'E`, `cvg_sin_coeff'`, `diffs_sin`, `series_sin_coeff0`
-  + lemma `sin0`
+  + lemmas `sin_coeff'E`, `cvg_sin_coeff'`, `diffs_sin`, `series_sin_coeff0`, `sin0`
   + definition `cos_coeff`
   + lemmas `cos_ceff_2_0`, `cos_coeff_2_2`, `cos_coeff_2_4`, `cos_coeffE`, `is_cvg_series_cos_coeff`
   + definition `cos`
   + lemma `cosE`
   + definition `cos_coeff'`
   + lemmas `cos_coeff'E`, `cvg_cos_coeff'`, `diffs_cos`, `series_cos_coeff0`, `cos0`
-  + lemmas `is_derive_sin`, `derivable_sin`, `continuous_sin`, `is_derive_cos`, `derivable_cos`, `continuous_cos`
-  + lemmas `cos2Dsin2`, `cosD`, `sinN`, `sinB`
+  + instance `is_derive_sin`
+  + lemmas `derivable_sin`, `continuous_sin`, `is_derive_cos`, `derivable_cos`, `continuous_cos`
+  + lemmas `cos2Dsin2`, `cos_max`, `cos_geN1`, `cos_le1`, `sin_max`, `sin_geN1`, `sin_le1`
+  + fact `sinD_cosD`
+  + lemmas `sinD`, `cosD`
+  + lemmas `sin2cos2`, `cos2sin2`, `sin_mulr2n`, `cos_mulr2n`
+  + fact `sinN_cosN`
+  + lemmas `sinN`, `cosN`
+  + lemmas `sin_sg`, `cos_sg`, `cosB`, `sinB`
+  + lemmas `norm_cos_eq1`, `norm_sin_eq1`, `cos1sin0`, `sin0cos1`, `cos_norm`
   + definition `pi`
   + lemmas `pihalfE`, `cos2_lt0`, `cos_exists`
-  + lemmas `pi_gt0`, `pi_ge0`
+  + lemmas `sin2_gt0`, `cos_pihalf_uniq`, `pihalf_02_cos_pihalf`, `pihalf_02`, `pi_gt0`, `pi_ge0`
+  + lemmas `sin_gt0_pihalf`, `cos_gt0_pihalf`, `cos_pihalf`, `sin_pihalf`, `cos_ge0_pihalf`, `cospi`, `sinpi`
+  + lemmas `cos2pi`, `sin2pi`, `sinDpi`, `cosDpi`, `sinD2pi`, `cosD2pi`
+  + lemmas `cosDpihalf`, `cosBpihalf`, `sinDpihalf`, `sinBpihalf`, `sin_ge0_pi`
   + lemmas `ltr_cos`, `ltr_sin`, `cos_inj`, `sin_inj`
   + definition `tan`
-  + lemmas `tan0`, `tanpi`
-  + lemmas `tanN`, `tanD`, `tan_mulr2n`, `cos2_tan2`
+  + lemmas `tan0`, `tanpi`, `tanN`, `tanD`, `tan_mulr2n`, `cos2_tan2`
   + lemmas `tan_pihalf`, `tan_piquarter`, `tanDpi`, `continuous_tan`
-  + instance `is_derive_tan`
-  + lemmas `derivable_tan`, `ltr_tan`, `tan_inj`
+  + lemmas `is_derive_tan`, `derivable_tan`, `ltr_tan`, `tan_inj`
   + definition `acos`
-  + lemmas `acosK`, `cosK`
+  + lemmas `acos_def`, `acos_ge0`, `acos_lepi`, `acosK`, `acos_gt0`, `acos_ltpi`
+  + lemmas `cosK`, `sin_acos`, `near_lift`, `continuous_acos`, `is_derive1_acos`
   + definition `asin`
-  + lemmas `asinK`, `sinK`
+  + lemmas `asin_def`, `asin_geNpi2`, `asin_lepi2`, `asinK`, `asin_ltpi2`, `asin_gtNpi2`
+  + lemmas `sinK`, `cos_asin`, `continuous_asin`, `is_derive1_asin`
   + definition `atan`
-  + lemmas `atanK`, `tanK`
+  + lemmas `atan_def`, `atan_gtNpi2`, `atan_ltpi2`, `atanK`, `tanK`
+  + lemmas `continuous_atan`, `cos_atan`
+  + instance `is_derive1_atan`
 
 ### Changed
 
@@ -191,16 +141,6 @@
   + `cvgNminfty` -> `cvgNninfty`
   + `cvgPminfty` -> `cvgPninfty`
   + `ler_cvg_minfty` -> `ler_cvg_ninfty`
-  + generalize `nondecreasing_seqP`, `nonincreasing_seqP`, `increasing_seqP`,
-    `decreasing_seqP` to equivalences
-  + generalize `lee_lim`, `ereal_cvgD_pinfty_fin`, `ereal_cvgD_ninfty_fin`,
-    `ereal_cvgD`, `ereal_limD`, `ereal_pseries0`, `eq_ereal_pseries` from `realType` to `realFieldType`
-- in `sequences.v`:
-  + lemmas `cvg_series_bounded`, `cvg_to_0_linear`, `lim_cvg_to_0_linear`.
-- in `topology.v`:
-  + replace `closed_cvg_loc` and `closed_cvg` by a more general lemma `closed_cvg`
-- move from `sequences.v` to `normedtype.v` and generalize from `nat` to `T : topologicalType`
-  + lemmas `ereal_cvgN`
 - in `normedtype.v`:
   + `nbhs_pinfty_gt` -> `nbhs_pinfty_gt_pos`
   + `nbhs_pinfty_ge` -> `nbhs_pinfty_ge_pos`
@@ -225,17 +165,6 @@
   + lemma `has_ub_lbN`
 - in `sequences.v`:
   + lemma `ereal_is_cvgD`
-  + lemma `ereal_pseries_pred0` moved from `csum.v`, minor generalization
-- in `landau.v`:
-  + lemma `cvg_shift` renamed to `cvg_comp_shift` and moved to `normedtype.v`
-- moved from `landau.v` to `normedtype.v`:
-  + lemmas `comp_shiftK`, `comp_centerK`, `shift0`, `center0`, `near_shift`,
-    `cvg_shift`
-- move from `derive.v` to `topology.v`: `exprfunE`
-  + replace `closed_cvg_loc` and `closed_cvg` by a more general lemma `closed_cvg`
-- in `topology.v` : 
-  + lemmas `cstE`, `compE`, `opprfunE`, `addrfunE`, `mulrfunE`, `scalrfunE`
-  + multi-rule `fctE`
 
 ### Changed
 

theories/derive.v

@@ -1581,7 +1581,6 @@ Proof. by apply: is_deriveN. Qed.
 
 End is_derive_instances.
 
-
 (* Trick to trigger type class resolution *)
 Lemma trigger_derive (R : realType) (f : R -> R) x x1 y1 :
   is_derive x 1 f x1 -> x1 = y1 -> is_derive x 1 f y1.