Merge pull request #383 from thery/exp

Adding some trigonometry in realType

CHANGELOG_UNRELEASED.md

@@ -13,14 +13,102 @@
   + 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`
 - in `ereal.v`:
   + lemmas `muleBr`, `muleBl`
   + lemma `eqe_absl`
   + lemma `lee_pmul`
   + lemmas `cover_restr`, `eqcover_r`
+- 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`
+  + lemmas `derive1_comp`, `derivable_cst`, `derivable_id`, trigger_derive`
+  + 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)
+  + 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`, 
+           `pseries_snd_diffs`
+  + lemmas `expR0`, `expR_ge1Dx`, `exp_coeffE`, `expRE`
+  + 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`,
+    `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`
+  + 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`
+- new file `trigo.v`
+  + lemmas `sqrtvR`, `eqr_div`, `big_nat_mul`, `cvg_series_cvg_series_group`,
+    `lt_sum_lim_series`
+  + definitions `periodic`, `alternating`
+  + lemmas `periodicn`, `alternatingn`
+  + definition `sin_coeff`
+  + lemmas `sin_coeffE`, `sin_coeff_even`, `is_cvg_series_sin_coeff`
+  + definition `sin`
+  + lemmas `sinE`
+  + definition `sin_coeff'`
+  + 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`
+  + 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 `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`, `tanN`, `tanD`, `tan_mulr2n`, `cos2_tan2`
+  + lemmas `tan_pihalf`, `tan_piquarter`, `tanDpi`, `continuous_tan`
+  + lemmas `is_derive_tan`, `derivable_tan`, `ltr_tan`, `tan_inj`
+  + definition `acos`
+  + 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 `asin_def`, `asin_geNpi2`, `asin_lepi2`, `asinK`, `asin_ltpi2`, `asin_gtNpi2`
+  + lemmas `sinK`, `cos_asin`, `continuous_asin`, `is_derive1_asin`
+  + definition `atan`
+  + lemmas `atan_def`, `atan_gtNpi2`, `atan_ltpi2`, `atanK`, `tanK`
+  + lemmas `continuous_atan`, `cos_atan`
+  + instance `is_derive1_atan`
 
 ### Changed
 

_CoqProject

@@ -21,6 +21,9 @@ theories/prodnormedzmodule.v
 theories/normedtype.v
 theories/realfun.v
 theories/sequences.v
+theories/exp.v
+theories/trigo.v
+theories/nsatz_realtype.v
 theories/cardinality.v
 theories/csum.v
 theories/forms.v

theories/derive.v

@@ -895,17 +895,16 @@ move=> dfx dgx; apply: DiffDef; first exact: differentiable_pair.
 by rewrite diff_pair // !diff_val.
 Qed.
 
-Global Instance is_diffM (f g df dg : V -> R) x : 
+Global Instance is_diffM (f g df dg : V -> R) x :
   is_diff x f df -> is_diff x g dg -> is_diff x (f * g) (f x *: dg + g x *: df).
 Proof.
 move=> dfx dgx.
 have -> : f * g = (fun p => p.1 * p.2) \o (fun y => (f y, g y)) by [].
-(* TODO: type class inference should succeed or fail, not leave an evar *) 
-apply: is_diff_eq; do ?exact: is_diff_comp. 
-by rewrite funeqE => ?; rewrite /= [_ * g _]mulrC. 
+(* TODO: type class inference should succeed or fail, not leave an evar *)
+apply: is_diff_eq; do ?exact: is_diff_comp.
+by rewrite funeqE => ?; rewrite /= [_ * g _]mulrC.
 Qed.
 
-
 Lemma diffM (f g : V -> R) x :
   differentiable f x -> differentiable g x ->
   'd (f * g) x = f x \*: 'd g x + g x \*: 'd f x :> (V -> R).
@@ -994,12 +993,6 @@ Proof.
 by move=> df fxn0; apply: differentiable_comp _ (differentiable_Rinv fxn0).
 Qed.
 
-Lemma exprfunE (T : pointedType) (K : ringType) (f : T -> K) n :
-  f ^+ n = (fun x => f x ^+ n).
-Proof.
-by elim: n => [|n ihn]; rewrite funeqE=> ?; [rewrite !expr0|rewrite !exprS ihn].
-Qed.
-
 Global Instance is_diffX (f df : V -> R) n x :
   is_diff x f df -> is_diff x (f ^+ n.+1) (n.+1%:R * f x ^+ n *: df).
 Proof.
@@ -1554,3 +1547,41 @@ apply: (@ler0_derive1_nincr _ (- f)) => t tab; first exact/derivableN/fdrvbl.
 rewrite derive1E deriveN; last exact: fdrvbl.
 by rewrite oppr_le0 -derive1E; apply: dfge0.
 Qed.
+
+Lemma derive1_comp (R : realFieldType) (f g : R -> R) x :
+  derivable f x 1 -> derivable g (f x) 1 ->
+  (g \o f)^`() x = g^`() (f x) * f^`() x.
+Proof.
+move=> /derivable1_diffP df /derivable1_diffP dg.
+rewrite derive1E'; last exact/differentiable_comp.
+rewrite diff_comp // !derive1E' //= -[X in 'd  _ _ X = _]mulr1.
+by rewrite [LHS]linearZ mulrC.
+Qed.
+
+Section is_derive_instances.
+Variables (R : numFieldType) (V : normedModType R).
+
+Lemma derivable_cst (x : V) : derivable (fun=> x) 0 1.
+Proof. exact/derivable1_diffP/differentiable_cst. Qed.
+
+Lemma derivable_id (x v : V) : derivable id x v.
+Proof.
+apply/derivable1P/derivableD; last exact/derivable_cst.
+exact/derivable1_diffP/differentiableZl.
+Qed.
+
+Global Instance is_derive_id (x v : V) : is_derive x v id v.
+Proof.
+apply: (DeriveDef (@derivable_id _ _)).
+by rewrite deriveE// (@diff_lin _ _ _ [linear of idfun]).
+Qed.
+
+Global Instance is_deriveNid (x v : V) : is_derive x v -%R (- v).
+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.
+Proof. by move=> Hi <-. Qed.