summaryrefslogtreecommitdiff
path: root/theories/Reals/Cos_plus.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/Reals/Cos_plus.v
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'theories/Reals/Cos_plus.v')
-rw-r--r--theories/Reals/Cos_plus.v96
1 files changed, 48 insertions, 48 deletions
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index 0de639e8..6c08356a 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
- (*i $Id: Cos_plus.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
+ (*i $Id$ i*)
Require Import Rbase.
Require Import Rfunctions.
@@ -111,7 +111,7 @@ Proof.
(Rsum_abs
(fun l:nat =>
(-1) ^ S (l + n) / INR (fact (2 * S (l + n))) * x ^ (2 * S (l + n)) *
- ((-1) ^ (N - l) / INR (fact (2 * (N - l)))) *
+ ((-1) ^ (N - l) / INR (fact (2 * (N - l)))) *
y ^ (2 * (N - l))) (pred (N - n))).
apply Rle_trans with
(sum_f_R0
@@ -745,42 +745,42 @@ Proof.
exact H.
Qed.
-Theorem cos_plus : forall x y:R, cos (x + y) = cos x * cos y - sin x * sin y.
+Theorem cos_plus : forall x y:R, cos (x + y) = cos x * cos y - sin x * sin y.
Proof.
- intros.
- cut (Un_cv (C1 x y) (cos x * cos y - sin x * sin y)).
- cut (Un_cv (C1 x y) (cos (x + y))).
- intros.
- apply UL_sequence with (C1 x y); assumption.
- apply C1_cvg.
- unfold Un_cv in |- *; unfold R_dist in |- *.
- intros.
- assert (H0 := A1_cvg x).
- assert (H1 := A1_cvg y).
- assert (H2 := B1_cvg x).
- assert (H3 := B1_cvg y).
- assert (H4 := CV_mult _ _ _ _ H0 H1).
- assert (H5 := CV_mult _ _ _ _ H2 H3).
+ intros.
+ cut (Un_cv (C1 x y) (cos x * cos y - sin x * sin y)).
+ cut (Un_cv (C1 x y) (cos (x + y))).
+ intros.
+ apply UL_sequence with (C1 x y); assumption.
+ apply C1_cvg.
+ unfold Un_cv in |- *; unfold R_dist in |- *.
+ intros.
+ assert (H0 := A1_cvg x).
+ assert (H1 := A1_cvg y).
+ assert (H2 := B1_cvg x).
+ assert (H3 := B1_cvg y).
+ assert (H4 := CV_mult _ _ _ _ H0 H1).
+ assert (H5 := CV_mult _ _ _ _ H2 H3).
assert (H6 := reste_cv_R0 x y).
unfold Un_cv in H4; unfold Un_cv in H5; unfold Un_cv in H6.
- unfold R_dist in H4; unfold R_dist in H5; unfold R_dist in H6.
+ unfold R_dist in H4; unfold R_dist in H5; unfold R_dist in H6.
cut (0 < eps / 3);
[ intro
| unfold Rdiv in |- *; apply Rmult_lt_0_compat;
- [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ].
- elim (H4 (eps / 3) H7); intros N1 H8.
- elim (H5 (eps / 3) H7); intros N2 H9.
+ [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ].
+ elim (H4 (eps / 3) H7); intros N1 H8.
+ elim (H5 (eps / 3) H7); intros N2 H9.
elim (H6 (eps / 3) H7); intros N3 H10.
- set (N := S (S (max (max N1 N2) N3))).
- exists N.
- intros.
- cut (n = S (pred n)).
- intro; rewrite H12.
- rewrite <- cos_plus_form.
- rewrite <- H12.
+ set (N := S (S (max (max N1 N2) N3))).
+ exists N.
+ intros.
+ cut (n = S (pred n)).
+ intro; rewrite H12.
+ rewrite <- cos_plus_form.
+ rewrite <- H12.
apply Rle_lt_trans with
(Rabs (A1 x n * A1 y n - cos x * cos y) +
- Rabs (sin x * sin y - B1 x (pred n) * B1 y (pred n) + Reste x y (pred n))).
+ Rabs (sin x * sin y - B1 x (pred n) * B1 y (pred n) + Reste x y (pred n))).
replace
(A1 x n * A1 y n - B1 x (pred n) * B1 y (pred n) + Reste x y (pred n) -
(cos x * cos y - sin x * sin y)) with
@@ -788,28 +788,28 @@ Proof.
(sin x * sin y - B1 x (pred n) * B1 y (pred n) + Reste x y (pred n)));
[ apply Rabs_triang | ring ].
replace eps with (eps / 3 + (eps / 3 + eps / 3)).
- apply Rplus_lt_compat.
- apply H8.
- unfold ge in |- *; apply le_trans with N.
- unfold N in |- *.
- apply le_trans with (max N1 N2).
- apply le_max_l.
+ apply Rplus_lt_compat.
+ apply H8.
+ unfold ge in |- *; apply le_trans with N.
+ unfold N in |- *.
+ apply le_trans with (max N1 N2).
+ apply le_max_l.
apply le_trans with (max (max N1 N2) N3).
apply le_max_l.
apply le_trans with (S (max (max N1 N2) N3)); apply le_n_Sn.
- assumption.
+ assumption.
apply Rle_lt_trans with
(Rabs (sin x * sin y - B1 x (pred n) * B1 y (pred n)) +
Rabs (Reste x y (pred n))).
apply Rabs_triang.
apply Rplus_lt_compat.
- rewrite <- Rabs_Ropp.
- rewrite Ropp_minus_distr.
- apply H9.
- unfold ge in |- *; apply le_trans with (max N1 N2).
- apply le_max_r.
- apply le_S_n.
- rewrite <- H12.
+ rewrite <- Rabs_Ropp.
+ rewrite Ropp_minus_distr.
+ apply H9.
+ unfold ge in |- *; apply le_trans with (max N1 N2).
+ apply le_max_r.
+ apply le_S_n.
+ rewrite <- H12.
apply le_trans with N.
unfold N in |- *.
apply le_n_S.
@@ -843,11 +843,11 @@ Proof.
replace (S (pred N)) with N.
assumption.
unfold N in |- *; simpl in |- *; reflexivity.
- cut (0 < N)%nat.
- intro.
- cut (0 < n)%nat.
- intro.
+ cut (0 < N)%nat.
+ intro.
+ cut (0 < n)%nat.
+ intro.
apply S_pred with 0%nat; assumption.
- apply lt_le_trans with N; assumption.
+ apply lt_le_trans with N; assumption.
unfold N in |- *; apply lt_O_Sn.
Qed.