changelog progress

CHANGELOG_UNRELEASED.md

@@ -9,11 +9,15 @@
 - new file `nsatz_realType`
 - new file `exp.v`
   + definition `diffs`
-  + lemmas `diffsN`, `diffs_sumE`, `diffs_equiv`, `cvg_diffs_equiv`, `termdiff`
-  + lemmas `expR0`, `expR_gt0`, `expRN`, `expRD`, `expRMm`
+  + lemmas `diffsN`, `diffs_sumE`, `diffs_equiv`, `cvg_diffs_equiv`, `termdiffs`
+  + 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`
   + definition `exp_fun`, notation `^
@@ -23,11 +27,20 @@
 - new file `trigo.v`
   + 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`
   + lemma `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`
-  + lemmas `cos0`
-  + lemmas `continuous_sin`, `continuous_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`
   + definition `pi`
   + lemmas `pihalfE`, `cos2_lt0`, `cos_exists`

theories/exp.v

@@ -350,15 +350,15 @@ have F1 := diffs_equiv Cx.
 by rewrite (cvg_lim _ (F1)).
 Qed.
 
-Let termdiff_P1 m (z h : R) :
+Let termdiffs_P1 m (z h : R) :
   \sum_(0 <= i < m) ((h + z) ^+ (m - i) * z ^+ i - z ^+ m) =
   \sum_(0 <= i < m) z ^+ i * ((h + z) ^+ (m - i) - z ^+ (m - i)).
 Proof.
 rewrite !big_mkord; apply: eq_bigr => i _.
 by rewrite mulrDr mulrN -exprD mulrC addnC subnK // ltnW.
 Qed.
 
-Let termdiff_P2 n (z h : R) :
+Let termdiffs_P2 n (z h : R) :
   h != 0 ->
   ((h + z) ^+ n - (z ^+ n)) / h - n%:R * z ^+ n.-1 =
   h * \sum_(0 <= i < n.-1) z ^+ i *
@@ -373,20 +373,20 @@ rewrite -(big_mkord xpredT (fun i : nat => (h + z) ^+ (n - i) * z ^+ i)).
 rewrite big_nat_recr //= subnn expr0 -addrA -mulrBl.
 rewrite  -add1n natrD opprD addrA subrr sub0r mulNr.
 rewrite mulr_natl -[in X in _ *+ X](subn0 n) -sumr_const_nat -sumrB.
-rewrite termdiff_P1 mulr_sumr !big_mkord; apply: eq_bigr => i _.
+rewrite termdiffs_P1 mulr_sumr !big_mkord; apply: eq_bigr => i _.
 rewrite mulrCA; congr (_ * _).
 rewrite subrXX addrK big_nat_rev /= big_mkord.
 congr (_ * _); apply: eq_bigr => k _.
 by rewrite -!predn_sub subKn // -subnS.
 Qed.
 
-Let termdiff_P3 (z h : R) n K :
+Let termdiffs_P3 (z h : R) n K :
   h != 0 -> `|z| <= K -> `|h + z| <= K ->
     `|((h +z) ^+ n - z ^+ n) / h - n%:R * z ^+ n.-1|
       <= n%:R * n.-1%:R * K ^+ n.-2 * `|h|.
 Proof.
 move=> hNZ zLK zhLk.
-rewrite termdiff_P2// normrM mulrC.
+rewrite termdiffs_P2// normrM mulrC.
 rewrite ler_pmul2r ?normr_gt0//.
 rewrite (le_trans (ler_norm_sum _ _ _))//.
 rewrite -mulrA mulrC -mulrA.
@@ -410,13 +410,13 @@ rewrite -[in X in _ <= X](subnK (_ : j <= d)%nat) -1?ltnS // addnC exprD normrM.
 by rewrite ler_pmul// ?normr_ge0// normrX ler_expn2r// qualifE (le_trans _ zLK).
 Qed.
 
-Lemma termdiff (c : R^nat) K x :
+Lemma termdiffs (c : R^nat) K x :
   cvg (series (fun n => c n * K ^+ n)) ->
   cvg (series (fun n => diffs c n * K ^+ n)) ->
   cvg (series (fun n => diffs (diffs c) n * K ^+ n)) ->
   `|x| < `|K| ->
   is_derive x 1
-    (fun x => lim (series (fun n => c(n) * x ^+ n)))
+    (fun x => lim (series (fun n => c n * x ^+ n)))
     (lim (series (fun n => diffs c n * x ^+ n))).
 Proof.
 move=> Ck CdK CddK xLK; set s := (fun n : nat => _).
@@ -464,8 +464,8 @@ suff Cc :
   apply: le_lt_trans eps_gt0.
   rewrite normr_le0 subr_eq0; apply/eqP.
   have Cs : cvg (series s) by apply: cvg_series_Xn_inside CdK _.
-  have Cs1 := cvg_diffs_equiv (Cs).
-  have Fs1 := diffs_equiv (Cs).
+  have Cs1 := cvg_diffs_equiv Cs.
+  have Fs1 := diffs_equiv Cs.
   set s1 := (fun i => _) in Cs1.
   have Cshx : cvg (series (shx h)).
     apply: cvg_series_Xn_inside Ck _.
@@ -534,7 +534,7 @@ apply: (@lim_cvg_to_0_linear _
 move=> h /andP[h_gt0 hLrBx] n.
 have hNZ : h != 0 by rewrite -normr_gt0.
 rewrite normrM -!mulrA ler_wpmul2l //.
-apply: le_trans (termdiff_P3 _ hNZ (ltW xLr) _) _; last by rewrite !mulrA.
+apply: le_trans (termdiffs_P3 _ hNZ (ltW xLr) _) _; last by rewrite !mulrA.
 apply: le_trans (ler_norm_add _ _) _.
 by rewrite -(subrK `|x| r) ler_add2r ltW.
 Grab Existential Variables. all: end_near. Qed.
@@ -593,7 +593,7 @@ pose s1 n := diffs (fun n => n`!%:R^-1) n * x ^+ n.
 rewrite expRE /=.
 rewrite (_ : (fun n => _) = s1); last first.
   by apply/funext => i; rewrite /s1 diffs_inv_fact.
-apply: (@termdiff _ _ (`|x| + 1)).
+apply: (@termdiffs _ _ (`|x| + 1)).
 - rewrite -exp_coeffE; apply: is_cvg_series_exp_coeff.
 - rewrite (_ : (fun n : nat => _) = exp_coeff (`|x| + 1)).
     by apply: is_cvg_series_exp_coeff.

theories/trigo.v

@@ -80,7 +80,7 @@ by rewrite /ball /= distrC.
 Grab Existential Variables. all: end_near. Qed.
 
 Lemma SER_PAIR (R : realFieldType) (f : R ^nat) : cvg (series f) ->
- series (fun n => \sum_(n.*2 <= i < n.*2 + 2) f i) --> lim (series f).
+  series (fun n => \sum_(n.*2 <= i < n.*2 + 2) f i) --> lim (series f).
 Proof.
 move=> cf; rewrite [X in series X --> _](_ : _ =
     (fun n => \sum_(n * 2 <= k < n.+1 * 2) f k)); last first.
@@ -146,12 +146,9 @@ Implicit Types x : R.
 Definition sin_coeff x :=
    [sequence  (odd n)%:R * (-1) ^+ n.-1./2 * x ^+ n / n`!%:R]_n.
 
-Lemma sin_coeffE x :
-  sin_coeff x = (fun n => (fun n => (odd n)%:R * (-1) ^+ n.-1./2 *
-                                    (n`!%:R)^-1) n * x ^+ n).
-Proof.
-by apply/funext => i; rewrite /sin_coeff /= -!mulrA [_ / _]mulrC.
-Qed.
+Lemma sin_coeffE x : sin_coeff x =
+  (fun n => (fun n => (odd n)%:R * (-1) ^+ n.-1./2 * (n`!%:R)^-1) n * x ^+ n).
+Proof. by apply/funext => i; rewrite /sin_coeff /= -!mulrA [_ / _]mulrC. Qed.
 
 Lemma sin_coeff_even n x : sin_coeff x n.*2 = 0.
 Proof. by rewrite /sin_coeff /= odd_double /= !mul0r. Qed.
@@ -459,7 +456,7 @@ Lemma cos_mulr2n a : cos (a *+ 2) = cos a ^+2 *+ 2 - 1.
 Proof. by rewrite mulr2n cosD -!expr2 sin2cos2 opprB addrA mulr2n. Qed.
 
 Lemma sinN_aux x :
-    (sin (- x ) + sin x) ^+ 2 + (cos (- x) - cos x) ^+ 2 = 0.
+  (sin (- x ) + sin x) ^+ 2 + (cos (- x) - cos x) ^+ 2 = 0.
 Proof.
 pose f := (sin \o -%R + sin)^+2 + (cos \o -%R - cos )^+2.
 apply: etrans (_ : f x = 0); first by [].
@@ -644,7 +641,6 @@ wlog : x / 0 <= x => [Hw|x_ge0].
   case: (leP 0 x) => [/Hw//| x_lt_0].
   rewrite -{-1}[x]opprK ltr_oppl andbC [-- _ < _]ltr_oppl cosN.
   by apply: Hw => //; rewrite oppr_cp0 ltW.
-have /andP[pi2_gt0 pi2L2] := pihalf_02.
 move=> /andP[x_gt0 xLpi2]; case: (ler0P (cos x)) => // cx_le0.
 have /IVT[]// : minr (cos 0) (cos x) <= 0 <= maxr (cos 0) (cos x).
   by rewrite cos0 /minr /maxr !ifN ?cx_le0 //= -leNgt (le_trans cx_le0).
@@ -653,6 +649,7 @@ move=> x1 /itvP Hx1 cx1_eq0.
 suff x1E : x1 = pi/2.
   have : x1 < pi / 2 by apply: le_lt_trans xLpi2; rewrite Hx1.
   by rewrite x1E ltxx.
+have /andP[pi2_gt0 pi2L2] := pihalf_02.
 apply: cos_pihalf_uniq=> //; last by (case cos_pihalf' => _ ->).
   by rewrite Hx1 ltW // (lt_trans _ pi2L2) // (le_lt_trans _ xLpi2) // Hx1.
 by rewrite !ltW.