summaryrefslogtreecommitdiff
path: root/theories/Reals/Cos_rel.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /theories/Reals/Cos_rel.v
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'theories/Reals/Cos_rel.v')
-rw-r--r--theories/Reals/Cos_rel.v420
1 files changed, 420 insertions, 0 deletions
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
new file mode 100644
index 00000000..9f76a5ad
--- /dev/null
+++ b/theories/Reals/Cos_rel.v
@@ -0,0 +1,420 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: Cos_rel.v,v 1.12.2.1 2004/07/16 19:31:10 herbelin Exp $ i*)
+
+Require Import Rbase.
+Require Import Rfunctions.
+Require Import SeqSeries.
+Require Import Rtrigo_def.
+Open Local Scope R_scope.
+
+Definition A1 (x:R) (N:nat) : R :=
+ sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * x ^ (2 * k)) N.
+
+Definition B1 (x:R) (N:nat) : R :=
+ sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * x ^ (2 * k + 1))
+ N.
+
+Definition C1 (x y:R) (N:nat) : R :=
+ sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * (x + y) ^ (2 * k)) N.
+
+Definition Reste1 (x y:R) (N:nat) : R :=
+ sum_f_R0
+ (fun k:nat =>
+ sum_f_R0
+ (fun l:nat =>
+ (-1) ^ S (l + k) / INR (fact (2 * S (l + k))) *
+ x ^ (2 * S (l + k)) * ((-1) ^ (N - l) / INR (fact (2 * (N - l)))) *
+ y ^ (2 * (N - l))) (pred (N - k))) (pred N).
+
+Definition Reste2 (x y:R) (N:nat) : R :=
+ sum_f_R0
+ (fun k:nat =>
+ sum_f_R0
+ (fun l:nat =>
+ (-1) ^ S (l + k) / INR (fact (2 * S (l + k) + 1)) *
+ x ^ (2 * S (l + k) + 1) *
+ ((-1) ^ (N - l) / INR (fact (2 * (N - l) + 1))) *
+ y ^ (2 * (N - l) + 1)) (pred (N - k))) (
+ pred N).
+
+Definition Reste (x y:R) (N:nat) : R := Reste2 x y N - Reste1 x y (S N).
+
+(* Here is the main result that will be used to prove that (cos (x+y))=(cos x)(cos y)-(sin x)(sin y) *)
+Theorem cos_plus_form :
+ forall (x y:R) (n:nat),
+ (0 < n)%nat ->
+ A1 x (S n) * A1 y (S n) - B1 x n * B1 y n + Reste x y n = C1 x y (S n).
+intros.
+unfold A1, B1 in |- *.
+rewrite
+ (cauchy_finite (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * x ^ (2 * k))
+ (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * y ^ (2 * k)) (
+ S n)).
+rewrite
+ (cauchy_finite
+ (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * x ^ (2 * k + 1))
+ (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * y ^ (2 * k + 1)) n H)
+ .
+unfold Reste in |- *.
+replace
+ (sum_f_R0
+ (fun k:nat =>
+ sum_f_R0
+ (fun l:nat =>
+ (-1) ^ S (l + k) / INR (fact (2 * S (l + k))) *
+ x ^ (2 * S (l + k)) *
+ ((-1) ^ (S n - l) / INR (fact (2 * (S n - l))) *
+ y ^ (2 * (S n - l)))) (pred (S n - k))) (
+ pred (S n))) with (Reste1 x y (S n)).
+replace
+ (sum_f_R0
+ (fun k:nat =>
+ sum_f_R0
+ (fun l:nat =>
+ (-1) ^ S (l + k) / INR (fact (2 * S (l + k) + 1)) *
+ x ^ (2 * S (l + k) + 1) *
+ ((-1) ^ (n - l) / INR (fact (2 * (n - l) + 1)) *
+ y ^ (2 * (n - l) + 1))) (pred (n - k))) (
+ pred n)) with (Reste2 x y n).
+ring.
+replace
+ (sum_f_R0
+ (fun k:nat =>
+ sum_f_R0
+ (fun p:nat =>
+ (-1) ^ p / INR (fact (2 * p)) * x ^ (2 * p) *
+ ((-1) ^ (k - p) / INR (fact (2 * (k - p))) * y ^ (2 * (k - p))))
+ k) (S n)) with
+ (sum_f_R0
+ (fun k:nat =>
+ (-1) ^ k / INR (fact (2 * k)) *
+ sum_f_R0
+ (fun l:nat => C (2 * k) (2 * l) * x ^ (2 * l) * y ^ (2 * (k - l))) k)
+ (S n)).
+set
+ (sin_nnn :=
+ fun n:nat =>
+ match n with
+ | O => 0
+ | S p =>
+ (-1) ^ S p / INR (fact (2 * S p)) *
+ sum_f_R0
+ (fun l:nat =>
+ C (2 * S p) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (p - l))) p
+ end).
+replace
+ (-
+ sum_f_R0
+ (fun k:nat =>
+ sum_f_R0
+ (fun p:nat =>
+ (-1) ^ p / INR (fact (2 * p + 1)) * x ^ (2 * p + 1) *
+ ((-1) ^ (k - p) / INR (fact (2 * (k - p) + 1)) *
+ y ^ (2 * (k - p) + 1))) k) n) with (sum_f_R0 sin_nnn (S n)).
+rewrite <- sum_plus.
+unfold C1 in |- *.
+apply sum_eq; intros.
+induction i as [| i Hreci].
+simpl in |- *.
+rewrite Rplus_0_l.
+replace (C 0 0) with 1.
+unfold Rdiv in |- *; rewrite Rinv_1.
+ring.
+unfold C in |- *.
+rewrite <- minus_n_n.
+simpl in |- *.
+unfold Rdiv in |- *; rewrite Rmult_1_r; rewrite Rinv_1; ring.
+unfold sin_nnn in |- *.
+rewrite <- Rmult_plus_distr_l.
+apply Rmult_eq_compat_l.
+rewrite binomial.
+set (Wn := fun i0:nat => C (2 * S i) i0 * x ^ i0 * y ^ (2 * S i - i0)).
+replace
+ (sum_f_R0
+ (fun l:nat => C (2 * S i) (2 * l) * x ^ (2 * l) * y ^ (2 * (S i - l)))
+ (S i)) with (sum_f_R0 (fun l:nat => Wn (2 * l)%nat) (S i)).
+replace
+ (sum_f_R0
+ (fun l:nat =>
+ C (2 * S i) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (i - l))) i) with
+ (sum_f_R0 (fun l:nat => Wn (S (2 * l))) i).
+rewrite Rplus_comm.
+apply sum_decomposition.
+apply sum_eq; intros.
+unfold Wn in |- *.
+apply Rmult_eq_compat_l.
+replace (2 * S i - S (2 * i0))%nat with (S (2 * (i - i0))).
+reflexivity.
+apply INR_eq.
+rewrite S_INR; rewrite mult_INR.
+repeat rewrite minus_INR.
+rewrite mult_INR; repeat rewrite S_INR.
+rewrite mult_INR; repeat rewrite S_INR; ring.
+replace (2 * S i)%nat with (S (S (2 * i))).
+apply le_n_S.
+apply le_trans with (2 * i)%nat.
+apply (fun m n p:nat => mult_le_compat_l p n m); assumption.
+apply le_n_Sn.
+apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
+ ring.
+assumption.
+apply sum_eq; intros.
+unfold Wn in |- *.
+apply Rmult_eq_compat_l.
+replace (2 * S i - 2 * i0)%nat with (2 * (S i - i0))%nat.
+reflexivity.
+apply INR_eq.
+rewrite mult_INR.
+repeat rewrite minus_INR.
+rewrite mult_INR; repeat rewrite S_INR.
+rewrite mult_INR; repeat rewrite S_INR; ring.
+apply (fun m n p:nat => mult_le_compat_l p n m); assumption.
+assumption.
+rewrite <- (Ropp_involutive (sum_f_R0 sin_nnn (S n))).
+apply Ropp_eq_compat.
+replace (- sum_f_R0 sin_nnn (S n)) with (-1 * sum_f_R0 sin_nnn (S n));
+ [ idtac | ring ].
+rewrite scal_sum.
+rewrite decomp_sum.
+replace (sin_nnn 0%nat) with 0.
+rewrite Rmult_0_l; rewrite Rplus_0_l.
+replace (pred (S n)) with n; [ idtac | reflexivity ].
+apply sum_eq; intros.
+rewrite Rmult_comm.
+unfold sin_nnn in |- *.
+rewrite scal_sum.
+rewrite scal_sum.
+apply sum_eq; intros.
+unfold Rdiv in |- *.
+repeat rewrite Rmult_assoc.
+rewrite (Rmult_comm (/ INR (fact (2 * S i)))).
+repeat rewrite <- Rmult_assoc.
+rewrite <- (Rmult_comm (/ INR (fact (2 * S i)))).
+repeat rewrite <- Rmult_assoc.
+replace (/ INR (fact (2 * S i)) * C (2 * S i) (S (2 * i0))) with
+ (/ INR (fact (2 * i0 + 1)) * / INR (fact (2 * (i - i0) + 1))).
+replace (S (2 * i0)) with (2 * i0 + 1)%nat; [ idtac | ring ].
+replace (S (2 * (i - i0))) with (2 * (i - i0) + 1)%nat; [ idtac | ring ].
+replace ((-1) ^ S i) with (-1 * (-1) ^ i0 * (-1) ^ (i - i0)).
+ring.
+simpl in |- *.
+pattern i at 2 in |- *; replace i with (i0 + (i - i0))%nat.
+rewrite pow_add.
+ring.
+symmetry in |- *; apply le_plus_minus; assumption.
+unfold C in |- *.
+unfold Rdiv in |- *; repeat rewrite <- Rmult_assoc.
+rewrite <- Rinv_l_sym.
+rewrite Rmult_1_l.
+rewrite Rinv_mult_distr.
+replace (S (2 * i0)) with (2 * i0 + 1)%nat;
+ [ apply Rmult_eq_compat_l | ring ].
+replace (2 * S i - (2 * i0 + 1))%nat with (2 * (i - i0) + 1)%nat.
+reflexivity.
+apply INR_eq.
+rewrite plus_INR; rewrite mult_INR; repeat rewrite minus_INR.
+rewrite plus_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; ring.
+replace (2 * i0 + 1)%nat with (S (2 * i0)).
+replace (2 * S i)%nat with (S (S (2 * i))).
+apply le_n_S.
+apply le_trans with (2 * i)%nat.
+apply (fun m n p:nat => mult_le_compat_l p n m); assumption.
+apply le_n_Sn.
+apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
+ ring.
+apply INR_eq; rewrite S_INR; rewrite plus_INR; rewrite mult_INR;
+ repeat rewrite S_INR; ring.
+assumption.
+apply INR_fact_neq_0.
+apply INR_fact_neq_0.
+apply INR_fact_neq_0.
+reflexivity.
+apply lt_O_Sn.
+apply sum_eq; intros.
+rewrite scal_sum.
+apply sum_eq; intros.
+unfold Rdiv in |- *.
+repeat rewrite <- Rmult_assoc.
+rewrite <- (Rmult_comm (/ INR (fact (2 * i)))).
+repeat rewrite <- Rmult_assoc.
+replace (/ INR (fact (2 * i)) * C (2 * i) (2 * i0)) with
+ (/ INR (fact (2 * i0)) * / INR (fact (2 * (i - i0)))).
+replace ((-1) ^ i) with ((-1) ^ i0 * (-1) ^ (i - i0)).
+ring.
+pattern i at 2 in |- *; replace i with (i0 + (i - i0))%nat.
+rewrite pow_add.
+ring.
+symmetry in |- *; apply le_plus_minus; assumption.
+unfold C in |- *.
+unfold Rdiv in |- *; repeat rewrite <- Rmult_assoc.
+rewrite <- Rinv_l_sym.
+rewrite Rmult_1_l.
+rewrite Rinv_mult_distr.
+replace (2 * i - 2 * i0)%nat with (2 * (i - i0))%nat.
+reflexivity.
+apply INR_eq.
+rewrite mult_INR; repeat rewrite minus_INR.
+do 2 rewrite mult_INR; repeat rewrite S_INR; ring.
+apply (fun m n p:nat => mult_le_compat_l p n m); assumption.
+assumption.
+apply INR_fact_neq_0.
+apply INR_fact_neq_0.
+apply INR_fact_neq_0.
+unfold Reste2 in |- *; apply sum_eq; intros.
+apply sum_eq; intros.
+unfold Rdiv in |- *; ring.
+unfold Reste1 in |- *; apply sum_eq; intros.
+apply sum_eq; intros.
+unfold Rdiv in |- *; ring.
+apply lt_O_Sn.
+Qed.
+
+Lemma pow_sqr : forall (x:R) (i:nat), x ^ (2 * i) = (x * x) ^ i.
+intros.
+assert (H := pow_Rsqr x i).
+unfold Rsqr in H; exact H.
+Qed.
+
+Lemma A1_cvg : forall x:R, Un_cv (A1 x) (cos x).
+intro.
+assert (H := exist_cos (x * x)).
+elim H; intros.
+assert (p_i := p).
+unfold cos_in in p.
+unfold cos_n, infinit_sum in p.
+unfold R_dist in p.
+cut (cos x = x0).
+intro.
+rewrite H0.
+unfold Un_cv in |- *; unfold R_dist in |- *; intros.
+elim (p eps H1); intros.
+exists x1; intros.
+unfold A1 in |- *.
+replace
+ (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * x ^ (2 * k)) n) with
+ (sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i)) * (x * x) ^ i) n).
+apply H2; assumption.
+apply sum_eq.
+intros.
+replace ((x * x) ^ i) with (x ^ (2 * i)).
+reflexivity.
+apply pow_sqr.
+unfold cos in |- *.
+case (exist_cos (Rsqr x)).
+unfold Rsqr in |- *; intros.
+unfold cos_in in p_i.
+unfold cos_in in c.
+apply uniqueness_sum with (fun i:nat => cos_n i * (x * x) ^ i); assumption.
+Qed.
+
+Lemma C1_cvg : forall x y:R, Un_cv (C1 x y) (cos (x + y)).
+intros.
+assert (H := exist_cos ((x + y) * (x + y))).
+elim H; intros.
+assert (p_i := p).
+unfold cos_in in p.
+unfold cos_n, infinit_sum in p.
+unfold R_dist in p.
+cut (cos (x + y) = x0).
+intro.
+rewrite H0.
+unfold Un_cv in |- *; unfold R_dist in |- *; intros.
+elim (p eps H1); intros.
+exists x1; intros.
+unfold C1 in |- *.
+replace
+ (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * (x + y) ^ (2 * k)) n)
+ with
+ (sum_f_R0
+ (fun i:nat => (-1) ^ i / INR (fact (2 * i)) * ((x + y) * (x + y)) ^ i) n).
+apply H2; assumption.
+apply sum_eq.
+intros.
+replace (((x + y) * (x + y)) ^ i) with ((x + y) ^ (2 * i)).
+reflexivity.
+apply pow_sqr.
+unfold cos in |- *.
+case (exist_cos (Rsqr (x + y))).
+unfold Rsqr in |- *; intros.
+unfold cos_in in p_i.
+unfold cos_in in c.
+apply uniqueness_sum with (fun i:nat => cos_n i * ((x + y) * (x + y)) ^ i);
+ assumption.
+Qed.
+
+Lemma B1_cvg : forall x:R, Un_cv (B1 x) (sin x).
+intro.
+case (Req_dec x 0); intro.
+rewrite H.
+rewrite sin_0.
+unfold B1 in |- *.
+unfold Un_cv in |- *; unfold R_dist in |- *; intros; exists 0%nat; intros.
+replace
+ (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * 0 ^ (2 * k + 1))
+ n) with 0.
+unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption.
+induction n as [| n Hrecn].
+simpl in |- *; ring.
+rewrite tech5; rewrite <- Hrecn.
+simpl in |- *; ring.
+unfold ge in |- *; apply le_O_n.
+assert (H0 := exist_sin (x * x)).
+elim H0; intros.
+assert (p_i := p).
+unfold sin_in in p.
+unfold sin_n, infinit_sum in p.
+unfold R_dist in p.
+cut (sin x = x * x0).
+intro.
+rewrite H1.
+unfold Un_cv in |- *; unfold R_dist in |- *; intros.
+cut (0 < eps / Rabs x);
+ [ intro
+ | unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+ [ assumption | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ] ].
+elim (p (eps / Rabs x) H3); intros.
+exists x1; intros.
+unfold B1 in |- *.
+replace
+ (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * x ^ (2 * k + 1))
+ n) with
+ (x *
+ sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i + 1)) * (x * x) ^ i) n).
+replace
+ (x *
+ sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i + 1)) * (x * x) ^ i) n -
+ x * x0) with
+ (x *
+ (sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i + 1)) * (x * x) ^ i) n -
+ x0)); [ idtac | ring ].
+rewrite Rabs_mult.
+apply Rmult_lt_reg_l with (/ Rabs x).
+apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption.
+rewrite <- Rmult_assoc.
+rewrite <- Rinv_l_sym.
+rewrite Rmult_1_l; rewrite <- (Rmult_comm eps); unfold Rdiv in H4; apply H4;
+ assumption.
+apply Rabs_no_R0; assumption.
+rewrite scal_sum.
+apply sum_eq.
+intros.
+rewrite pow_add.
+rewrite pow_sqr.
+simpl in |- *.
+ring.
+unfold sin in |- *.
+case (exist_sin (Rsqr x)).
+unfold Rsqr in |- *; intros.
+unfold sin_in in p_i.
+unfold sin_in in s.
+assert
+ (H1 := uniqueness_sum (fun i:nat => sin_n i * (x * x) ^ i) x0 x1 p_i s).
+rewrite H1; reflexivity.
+Qed. \ No newline at end of file