diff options
Diffstat (limited to 'theories7/Reals/Cauchy_prod.v')
| -rw-r--r-- | theories7/Reals/Cauchy_prod.v | 347 |
1 files changed, 347 insertions, 0 deletions
diff --git a/theories7/Reals/Cauchy_prod.v b/theories7/Reals/Cauchy_prod.v new file mode 100644 index 00000000..9442eff0 --- /dev/null +++ b/theories7/Reals/Cauchy_prod.v @@ -0,0 +1,347 @@ +(************************************************************************) +(* 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. |