diff options
Diffstat (limited to 'theories7/Reals/Cauchy_prod.v')
| -rw-r--r-- | theories7/Reals/Cauchy_prod.v | 347 |
1 files changed, 0 insertions, 347 deletions
diff --git a/theories7/Reals/Cauchy_prod.v b/theories7/Reals/Cauchy_prod.v deleted file mode 100644 index 9442eff0..00000000 --- a/theories7/Reals/Cauchy_prod.v +++ /dev/null @@ -1,347 +0,0 @@ -(************************************************************************) -(* 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: Cauchy_prod.v,v 1.1.2.1 2004/07/16 19:31:31 herbelin Exp $ i*) - -Require Rbase. -Require Rfunctions. -Require Rseries. -Require PartSum. -V7only [ Import nat_scope. Import Z_scope. Import R_scope. ]. -Open Local Scope R_scope. - -(**********) -Lemma sum_N_predN : (An:nat->R;N:nat) (lt O N) -> (sum_f_R0 An N)==``(sum_f_R0 An (pred N)) + (An N)``. -Intros. -Replace N with (S (pred N)). -Rewrite tech5. -Reflexivity. -Symmetry; Apply S_pred with O; Assumption. -Qed. - -(**********) -Lemma sum_plus : (An,Bn:nat->R;N:nat) (sum_f_R0 [l:nat]``(An l)+(Bn l)`` N)==``(sum_f_R0 An N)+(sum_f_R0 Bn N)``. -Intros. -Induction N. -Reflexivity. -Do 3 Rewrite tech5. -Rewrite HrecN; Ring. -Qed. - -(* The main result *) -Theorem cauchy_finite : (An,Bn:nat->R;N:nat) (lt O N) -> (Rmult (sum_f_R0 An N) (sum_f_R0 Bn N)) == (Rplus (sum_f_R0 [k:nat](sum_f_R0 [p:nat]``(An p)*(Bn (minus k p))`` k) N) (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (plus l k)))*(Bn (minus N l))`` (pred (minus N k))) (pred N))). -Intros; Induction N. -Elim (lt_n_n ? H). -Cut N=O\/(lt O N). -Intro; Elim H0; Intro. -Rewrite H1; Simpl; Ring. -Replace (pred (S N)) with (S (pred N)). -Do 5 Rewrite tech5. -Rewrite Rmult_Rplus_distrl; Rewrite Rmult_Rplus_distr; Rewrite (HrecN H1). -Repeat Rewrite Rplus_assoc; Apply Rplus_plus_r. -Replace (pred (minus (S N) (S (pred N)))) with (O). -Rewrite Rmult_Rplus_distr; Replace (sum_f_R0 [l:nat]``(An (S (plus l (S (pred N)))))*(Bn (minus (S N) l))`` O) with ``(An (S N))*(Bn (S N))``. -Repeat Rewrite <- Rplus_assoc; Do 2 Rewrite <- (Rplus_sym ``(An (S N))*(Bn (S N))``); Repeat Rewrite Rplus_assoc; Apply Rplus_plus_r. -Rewrite <- minus_n_n; Cut N=(1)\/(le (2) N). -Intro; Elim H2; Intro. -Rewrite H3; Simpl; Ring. -Replace (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (plus l k)))*(Bn (minus N l))`` (pred (minus N k))) (pred N)) with (Rplus (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (pred (minus N k)))) (pred (pred N))) (sum_f_R0 [l:nat]``(An (S l))*(Bn (minus N l))`` (pred N))). -Replace (sum_f_R0 [p:nat]``(An p)*(Bn (minus (S N) p))`` N) with (Rplus (sum_f_R0 [l:nat]``(An (S l))*(Bn (minus N l))`` (pred N)) ``(An O)*(Bn (S N))``). -Repeat Rewrite <- Rplus_assoc; Rewrite <- (Rplus_sym (sum_f_R0 [l:nat]``(An (S l))*(Bn (minus N l))`` (pred N))); Repeat Rewrite Rplus_assoc; Apply Rplus_plus_r. -Replace (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (plus l k)))*(Bn (minus (S N) l))`` (pred (minus (S N) k))) (pred N)) with (Rplus (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (minus N k))) (pred N)) (Rmult (Bn (S N)) (sum_f_R0 [l:nat](An (S l)) (pred N)))). -Rewrite (decomp_sum An N H1); Rewrite Rmult_Rplus_distrl; Repeat Rewrite <- Rplus_assoc; Rewrite <- (Rplus_sym ``(An O)*(Bn (S N))``); Repeat Rewrite Rplus_assoc; Apply Rplus_plus_r. -Repeat Rewrite <- Rplus_assoc; Rewrite <- (Rplus_sym (Rmult (sum_f_R0 [i:nat](An (S i)) (pred N)) (Bn (S N)))); Rewrite <- (Rplus_sym (Rmult (Bn (S N)) (sum_f_R0 [i:nat](An (S i)) (pred N)))); Rewrite (Rmult_sym (Bn (S N))); Repeat Rewrite Rplus_assoc; Apply Rplus_plus_r. -Replace (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (minus N k))) (pred N)) with (Rplus (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (pred (minus N k)))) (pred (pred N))) (Rmult (An (S N)) (sum_f_R0 [l:nat](Bn (S l)) (pred N)))). -Rewrite (decomp_sum Bn N H1); Rewrite Rmult_Rplus_distr. -Pose Z := (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (pred (minus N k)))) (pred (pred N))); Pose Z2 := (sum_f_R0 [i:nat](Bn (S i)) (pred N)); Ring. -Rewrite (sum_N_predN [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (minus N k))) (pred N)). -Replace (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (minus N k))) (pred (pred N))) with (sum_f_R0 [k:nat](Rplus (sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (pred (minus N k)))) ``(An (S N))*(Bn (S k))``) (pred (pred N))). -Rewrite (sum_plus [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (pred (minus N k)))) [k:nat]``(An (S N))*(Bn (S k))`` (pred (pred N))). -Repeat Rewrite Rplus_assoc; Apply Rplus_plus_r. -Replace (pred (minus N (pred N))) with O. -Simpl; Rewrite <- minus_n_O. -Replace (S (pred N)) with N. -Replace (sum_f_R0 [k:nat]``(An (S N))*(Bn (S k))`` (pred (pred N))) with (sum_f_R0 [k:nat]``(Bn (S k))*(An (S N))`` (pred (pred N))). -Rewrite <- (scal_sum [l:nat](Bn (S l)) (pred (pred N)) (An (S N))); Rewrite (sum_N_predN [l:nat](Bn (S l)) (pred N)). -Replace (S (pred N)) with N. -Ring. -Apply S_pred with O; Assumption. -Apply lt_pred; Apply lt_le_trans with (2); [Apply lt_n_Sn | Assumption]. -Apply sum_eq; Intros; Apply Rmult_sym. -Apply S_pred with O; Assumption. -Replace (minus N (pred N)) with (1). -Reflexivity. -Pattern 1 N; Replace N with (S (pred N)). -Rewrite <- minus_Sn_m. -Rewrite <- minus_n_n; Reflexivity. -Apply le_n. -Symmetry; Apply S_pred with O; Assumption. -Apply sum_eq; Intros; Rewrite (sum_N_predN [l:nat]``(An (S (S (plus l i))))*(Bn (minus N l))`` (pred (minus N i))). -Replace (S (S (plus (pred (minus N i)) i))) with (S N). -Replace (minus N (pred (minus N i))) with (S i). -Ring. -Rewrite pred_of_minus; Apply INR_eq; Repeat Rewrite minus_INR. -Rewrite S_INR; Ring. -Apply le_trans with (pred (pred N)). -Assumption. -Apply le_trans with (pred N); Apply le_pred_n. -Apply INR_le; Rewrite minus_INR. -Apply Rle_anti_compatibility with ``(INR i)-1``. -Replace ``(INR i)-1+(INR (S O))`` with (INR i); [Idtac | Ring]. -Replace ``(INR i)-1+((INR N)-(INR i))`` with ``(INR N)-(INR (S O))``; [Idtac | Ring]. -Rewrite <- minus_INR. -Apply le_INR; Apply le_trans with (pred (pred N)). -Assumption. -Rewrite <- pred_of_minus; Apply le_pred_n. -Apply le_trans with (2). -Apply le_n_Sn. -Assumption. -Apply le_trans with (pred (pred N)). -Assumption. -Apply le_trans with (pred N); Apply le_pred_n. -Rewrite <- pred_of_minus. -Apply le_trans with (pred N). -Apply le_S_n. -Replace (S (pred N)) with N. -Replace (S (pred (minus N i))) with (minus N i). -Apply simpl_le_plus_l with i; Rewrite le_plus_minus_r. -Apply le_plus_r. -Apply le_trans with (pred (pred N)); [Assumption | Apply le_trans with (pred N); Apply le_pred_n]. -Apply S_pred with O. -Apply simpl_lt_plus_l with i; Rewrite le_plus_minus_r. -Replace (plus i O) with i; [Idtac | Ring]. -Apply le_lt_trans with (pred (pred N)); [Assumption | Apply lt_trans with (pred N); Apply lt_pred_n_n]. -Apply lt_S_n. -Replace (S (pred N)) with N. -Apply lt_le_trans with (2). -Apply lt_n_Sn. -Assumption. -Apply S_pred with O; Assumption. -Assumption. -Apply le_trans with (pred (pred N)). -Assumption. -Apply le_trans with (pred N); Apply le_pred_n. -Apply S_pred with O; Assumption. -Apply le_pred_n. -Apply INR_eq; Rewrite pred_of_minus; Do 3 Rewrite S_INR; Rewrite plus_INR; Repeat Rewrite minus_INR. -Ring. -Apply le_trans with (pred (pred N)). -Assumption. -Apply le_trans with (pred N); Apply le_pred_n. -Apply INR_le. -Rewrite minus_INR. -Apply Rle_anti_compatibility with ``(INR i)-1``. -Replace ``(INR i)-1+(INR (S O))`` with (INR i); [Idtac | Ring]. -Replace ``(INR i)-1+((INR N)-(INR i))`` with ``(INR N)-(INR (S O))``; [Idtac | Ring]. -Rewrite <- minus_INR. -Apply le_INR. -Apply le_trans with (pred (pred N)). -Assumption. -Rewrite <- pred_of_minus. -Apply le_pred_n. -Apply le_trans with (2). -Apply le_n_Sn. -Assumption. -Apply le_trans with (pred (pred N)). -Assumption. -Apply le_trans with (pred N); Apply le_pred_n. -Apply lt_le_trans with (1). -Apply lt_O_Sn. -Apply INR_le. -Rewrite pred_of_minus. -Repeat Rewrite minus_INR. -Apply Rle_anti_compatibility with ``(INR i)-1``. -Replace ``(INR i)-1+(INR (S O))`` with (INR i); [Idtac | Ring]. -Replace ``(INR i)-1+((INR N)-(INR i)-(INR (S O)))`` with ``(INR N)-(INR (S O)) -(INR (S O))``. -Repeat Rewrite <- minus_INR. -Apply le_INR. -Apply le_trans with (pred (pred N)). -Assumption. -Do 2 Rewrite <- pred_of_minus. -Apply le_n. -Apply simpl_le_plus_l with (1). -Rewrite le_plus_minus_r. -Simpl; Assumption. -Apply le_trans with (2); [Apply le_n_Sn | Assumption]. -Apply le_trans with (2); [Apply le_n_Sn | Assumption]. -Ring. -Apply le_trans with (pred (pred N)). -Assumption. -Apply le_trans with (pred N); Apply le_pred_n. -Apply simpl_le_plus_l with i. -Rewrite le_plus_minus_r. -Replace (plus i (1)) with (S i). -Replace N with (S (pred N)). -Apply le_n_S. -Apply le_trans with (pred (pred N)). -Assumption. -Apply le_pred_n. -Symmetry; Apply S_pred with O; Assumption. -Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Reflexivity. -Apply le_trans with (pred (pred N)). -Assumption. -Apply le_trans with (pred N); Apply le_pred_n. -Apply lt_le_trans with (1). -Apply lt_O_Sn. -Apply le_S_n. -Replace (S (pred N)) with N. -Assumption. -Apply S_pred with O; Assumption. -Replace (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (plus l k)))*(Bn (minus (S N) l))`` (pred (minus (S N) k))) (pred N)) with (sum_f_R0 [k:nat](Rplus (sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (minus N k))) ``(An (S k))*(Bn (S N))``) (pred N)). -Rewrite (sum_plus [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (minus N k))) [k:nat]``(An (S k))*(Bn (S N))``). -Apply Rplus_plus_r. -Rewrite scal_sum; Reflexivity. -Apply sum_eq; Intros; Rewrite Rplus_sym; Rewrite (decomp_sum [l:nat]``(An (S (plus l i)))*(Bn (minus (S N) l))`` (pred (minus (S N) i))). -Replace (plus O i) with i; [Idtac | Ring]. -Rewrite <- minus_n_O; Apply Rplus_plus_r. -Replace (pred (pred (minus (S N) i))) with (pred (minus N i)). -Apply sum_eq; Intros. -Replace (minus (S N) (S i0)) with (minus N i0); [Idtac | Reflexivity]. -Replace (plus (S i0) i) with (S (plus i0 i)). -Reflexivity. -Apply INR_eq; Rewrite S_INR; Do 2 Rewrite plus_INR; Rewrite S_INR; Ring. -Cut (minus N i)=(pred (minus (S N) i)). -Intro; Rewrite H5; Reflexivity. -Rewrite pred_of_minus. -Apply INR_eq; Repeat Rewrite minus_INR. -Rewrite S_INR; Ring. -Apply le_trans with N. -Apply le_trans with (pred N). -Assumption. -Apply le_pred_n. -Apply le_n_Sn. -Apply simpl_le_plus_l with i. -Rewrite le_plus_minus_r. -Replace (plus i (1)) with (S i). -Apply le_n_S. -Apply le_trans with (pred N). -Assumption. -Apply le_pred_n. -Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Ring. -Apply le_trans with N. -Apply le_trans with (pred N). -Assumption. -Apply le_pred_n. -Apply le_n_Sn. -Apply le_trans with (pred N). -Assumption. -Apply le_pred_n. -Replace (pred (minus (S N) i)) with (minus (S N) (S i)). -Replace (minus (S N) (S i)) with (minus N i); [Idtac | Reflexivity]. -Apply simpl_lt_plus_l with i. -Rewrite le_plus_minus_r. -Replace (plus i O) with i; [Idtac | Ring]. -Apply le_lt_trans with (pred N). -Assumption. -Apply lt_pred_n_n. -Assumption. -Apply le_trans with (pred N). -Assumption. -Apply le_pred_n. -Rewrite pred_of_minus. -Apply INR_eq; Repeat Rewrite minus_INR. -Repeat Rewrite S_INR; Ring. -Apply le_trans with N. -Apply le_trans with (pred N). -Assumption. -Apply le_pred_n. -Apply le_n_Sn. -Apply simpl_le_plus_l with i. -Rewrite le_plus_minus_r. -Replace (plus i (1)) with (S i). -Apply le_n_S. -Apply le_trans with (pred N). -Assumption. -Apply le_pred_n. -Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Ring. -Apply le_trans with N. -Apply le_trans with (pred N). -Assumption. -Apply le_pred_n. -Apply le_n_Sn. -Apply le_n_S. -Apply le_trans with (pred N). -Assumption. -Apply le_pred_n. -Rewrite Rplus_sym. -Rewrite (decomp_sum [p:nat]``(An p)*(Bn (minus (S N) p))`` N). -Rewrite <- minus_n_O. -Apply Rplus_plus_r. -Apply sum_eq; Intros. -Reflexivity. -Assumption. -Rewrite Rplus_sym. -Rewrite (decomp_sum [k:nat](sum_f_R0 [l:nat]``(An (S (plus l k)))*(Bn (minus N l))`` (pred (minus N k))) (pred N)). -Rewrite <- minus_n_O. -Replace (sum_f_R0 [l:nat]``(An (S (plus l O)))*(Bn (minus N l))`` (pred N)) with (sum_f_R0 [l:nat]``(An (S l))*(Bn (minus N l))`` (pred N)). -Apply Rplus_plus_r. -Apply sum_eq; Intros. -Replace (pred (minus N (S i))) with (pred (pred (minus N i))). -Apply sum_eq; Intros. -Replace (plus i0 (S i)) with (S (plus i0 i)). -Reflexivity. -Apply INR_eq; Rewrite S_INR; Do 2 Rewrite plus_INR; Rewrite S_INR; Ring. -Cut (pred (minus N i))=(minus N (S i)). -Intro; Rewrite H5; Reflexivity. -Rewrite pred_of_minus. -Apply INR_eq. -Repeat Rewrite minus_INR. -Repeat Rewrite S_INR; Ring. -Apply le_trans with (S (pred (pred N))). -Apply le_n_S; Assumption. -Replace (S (pred (pred N))) with (pred N). -Apply le_pred_n. -Apply S_pred with O. -Apply lt_S_n. -Replace (S (pred N)) with N. -Apply lt_le_trans with (2). -Apply lt_n_Sn. -Assumption. -Apply S_pred with O; Assumption. -Apply le_trans with (pred (pred N)). -Assumption. -Apply le_trans with (pred N); Apply le_pred_n. -Apply simpl_le_plus_l with i. -Rewrite le_plus_minus_r. -Replace (plus i (1)) with (S i). -Replace N with (S (pred N)). -Apply le_n_S. -Apply le_trans with (pred (pred N)). -Assumption. -Apply le_pred_n. -Symmetry; Apply S_pred with O; Assumption. -Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Ring. -Apply le_trans with (pred (pred N)). -Assumption. -Apply le_trans with (pred N); Apply le_pred_n. -Apply sum_eq; Intros. -Replace (plus i O) with i; [Reflexivity | Trivial]. -Apply lt_S_n. -Replace (S (pred N)) with N. -Apply lt_le_trans with (2); [Apply lt_n_Sn | Assumption]. -Apply S_pred with O; Assumption. -Inversion H1. -Left; Reflexivity. -Right; Apply le_n_S; Assumption. -Simpl. -Replace (S (pred N)) with N. -Reflexivity. -Apply S_pred with O; Assumption. -Simpl. -Cut (minus N (pred N))=(1). -Intro; Rewrite H2; Reflexivity. -Rewrite pred_of_minus. -Apply INR_eq; Repeat Rewrite minus_INR. -Ring. -Apply lt_le_S; Assumption. -Rewrite <- pred_of_minus; Apply le_pred_n. -Simpl; Symmetry; Apply S_pred with O; Assumption. -Inversion H. -Left; Reflexivity. -Right; Apply lt_le_trans with (1); [Apply lt_n_Sn | Exact H1]. -Qed. |