Modifications and rearrangements to remove the action that sin (PI/2) = 1

Beware that the definition of PI changes in the process

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15425 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 146 deletions

diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index 100e0818a..c01e82272 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -15,152 +15,6 @@ Require Import PSeries_reg.
 Open Local Scope nat_scope.
 Open Local Scope R_scope.
 
-Lemma CVN_R_cos :
-  forall fn:nat -> R -> R,
-    fn = (fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N)) * x ^ (2 * N)) ->
-    CVN_R fn.
-Proof.
-  unfold CVN_R in |- *; intros.
-  cut ((r:R) <> 0).
-  intro hyp_r; unfold CVN_r in |- *.
-  exists (fun n:nat => / INR (fact (2 * n)) * r ^ (2 * n)).
-  cut
-    { l:R |
-        Un_cv
-        (fun n:nat =>
-          sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k)) * r ^ (2 * k)))
-          n) l }.
-  intro X; elim X; intros.
-  exists x.
-  split.
-  apply p.
-  intros; rewrite H; unfold Rdiv in |- *; do 2 rewrite Rabs_mult.
-  rewrite pow_1_abs; rewrite Rmult_1_l.
-  cut (0 < / INR (fact (2 * n))).
-  intro; rewrite (Rabs_right _ (Rle_ge _ _ (Rlt_le _ _ H1))).
-  apply Rmult_le_compat_l.
-  left; apply H1.
-  rewrite <- RPow_abs; apply pow_maj_Rabs.
-  rewrite Rabs_Rabsolu.
-  unfold Boule in H0; rewrite Rminus_0_r in H0.
-  left; apply H0.
-  apply Rinv_0_lt_compat; apply INR_fact_lt_0.
-  apply Alembert_C2.
-  intro; apply Rabs_no_R0.
-  apply prod_neq_R0.
-  apply Rinv_neq_0_compat.
-  apply INR_fact_neq_0.
-  apply pow_nonzero; assumption.
-  assert (H0 := Alembert_cos).
-  unfold cos_n in H0; unfold Un_cv in H0; unfold Un_cv in |- *; intros.
-  cut (0 < eps / Rsqr r).
-  intro; elim (H0 _ H2); intros N0 H3.
-  exists N0; intros.
-  unfold R_dist in |- *; assert (H5 := H3 _ H4).
-  unfold R_dist in H5;
-    replace
-    (Rabs
-      (Rabs (/ INR (fact (2 * S n)) * r ^ (2 * S n)) /
-        Rabs (/ INR (fact (2 * n)) * r ^ (2 * n)))) with
-    (Rsqr r *
-      Rabs ((-1) ^ S n / INR (fact (2 * S n)) / ((-1) ^ n / INR (fact (2 * n))))).
-  apply Rmult_lt_reg_l with (/ Rsqr r).
-  apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption.
-  pattern (/ Rsqr r) at 1 in |- *; replace (/ Rsqr r) with (Rabs (/ Rsqr r)).
-  rewrite <- Rabs_mult; rewrite Rmult_minus_distr_l; rewrite Rmult_0_r;
-    rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_l; rewrite <- (Rmult_comm eps); apply H5.
-  unfold Rsqr in |- *; apply prod_neq_R0; assumption.
-  rewrite Rabs_Rinv.
-  rewrite Rabs_right.
-  reflexivity.
-  apply Rle_ge; apply Rle_0_sqr.
-  unfold Rsqr in |- *; apply prod_neq_R0; assumption.
-  rewrite (Rmult_comm (Rsqr r)); unfold Rdiv in |- *; repeat rewrite Rabs_mult;
-    rewrite Rabs_Rabsolu; rewrite pow_1_abs; rewrite Rmult_1_l;
-      repeat rewrite Rmult_assoc; apply Rmult_eq_compat_l.
-  rewrite Rabs_Rinv.
-  rewrite Rabs_mult; rewrite (pow_1_abs n); rewrite Rmult_1_l;
-    rewrite <- Rabs_Rinv.
-  rewrite Rinv_involutive.
-  rewrite Rinv_mult_distr.
-  rewrite Rabs_Rinv.
-  rewrite Rinv_involutive.
-  rewrite (Rmult_comm (Rabs (Rabs (r ^ (2 * S n))))); rewrite Rabs_mult;
-    rewrite Rabs_Rabsolu; rewrite Rmult_assoc; apply Rmult_eq_compat_l.
-  rewrite Rabs_Rinv.
-  do 2 rewrite Rabs_Rabsolu; repeat rewrite Rabs_right.
-  replace (r ^ (2 * S n)) with (r ^ (2 * n) * r * r).
-  repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
-  unfold Rsqr in |- *; ring.
-  apply pow_nonzero; assumption.
-  replace (2 * S n)%nat with (S (S (2 * n))).
-  simpl in |- *; ring.
-  ring.
-  apply Rle_ge; apply pow_le; left; apply (cond_pos r).
-  apply Rle_ge; apply pow_le; left; apply (cond_pos r).
-  apply Rabs_no_R0; apply pow_nonzero; assumption.
-  apply Rabs_no_R0; apply INR_fact_neq_0.
-  apply INR_fact_neq_0.
-  apply Rabs_no_R0; apply Rinv_neq_0_compat; apply INR_fact_neq_0.
-  apply Rabs_no_R0; apply pow_nonzero; assumption.
-  apply INR_fact_neq_0.
-  apply Rinv_neq_0_compat; apply INR_fact_neq_0.
-  apply prod_neq_R0.
-  apply pow_nonzero; discrR.
-  apply Rinv_neq_0_compat; apply INR_fact_neq_0.
-  unfold Rdiv in |- *; apply Rmult_lt_0_compat.
-  apply H1.
-  apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption.
-  assert (H0 := cond_pos r); red in |- *; intro; rewrite H1 in H0;
-    elim (Rlt_irrefl _ H0).
-Qed.
-
-(**********)
-Lemma continuity_cos : continuity cos.
-Proof.
-  set (fn := fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N)) * x ^ (2 * N)).
-  cut (CVN_R fn).
-  intro; cut (forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }).
-  intro cv; cut (forall n:nat, continuity (fn n)).
-  intro; cut (forall x:R, cos x = SFL fn cv x).
-  intro; cut (continuity (SFL fn cv) -> continuity cos).
-  intro; apply H1.
-  apply SFL_continuity; assumption.
-  unfold continuity in |- *; unfold continuity_pt in |- *;
-    unfold continue_in in |- *; unfold limit1_in in |- *;
-      unfold limit_in in |- *; simpl in |- *; unfold R_dist in |- *;
-        intros.
-  elim (H1 x _ H2); intros.
-  exists x0; intros.
-  elim H3; intros.
-  split.
-  apply H4.
-  intros; rewrite (H0 x); rewrite (H0 x1); apply H5; apply H6.
-  intro; unfold cos, SFL in |- *.
-  case (cv x); case (exist_cos (Rsqr x)); intros.
-  symmetry  in |- *; eapply UL_sequence.
-  apply u.
-  unfold cos_in in c; unfold infinite_sum in c; unfold Un_cv in |- *; intros.
-  elim (c _ H0); intros N0 H1.
-  exists N0; intros.
-  unfold R_dist in H1; unfold R_dist, SP in |- *.
-  replace (sum_f_R0 (fun k:nat => fn k x) n) with
-  (sum_f_R0 (fun i:nat => cos_n i * Rsqr x ^ i) n).
-  apply H1; assumption.
-  apply sum_eq; intros.
-  unfold cos_n, fn in |- *; apply Rmult_eq_compat_l.
-  unfold Rsqr in |- *; rewrite pow_sqr; reflexivity.
-  intro; unfold fn in |- *;
-    replace (fun x:R => (-1) ^ n / INR (fact (2 * n)) * x ^ (2 * n)) with
-    (fct_cte ((-1) ^ n / INR (fact (2 * n))) * pow_fct (2 * n))%F;
-    [ idtac | reflexivity ].
-  apply continuity_mult.
-  apply derivable_continuous; apply derivable_const.
-  apply derivable_continuous; apply (derivable_pow (2 * n)).
-  apply CVN_R_CVS; apply X.
-  apply CVN_R_cos; unfold fn in |- *; reflexivity.
-Qed.
 
 (**********)
 Lemma continuity_sin : continuity sin.