diff options
Diffstat (limited to 'theories/Reals/Cauchy_prod.v')
| -rw-r--r-- | theories/Reals/Cauchy_prod.v | 458 |
1 files changed, 458 insertions, 0 deletions
diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v new file mode 100644 index 00000000..41a6284f --- /dev/null +++ b/theories/Reals/Cauchy_prod.v @@ -0,0 +1,458 @@ +(************************************************************************) +(* 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.10.2.1 2004/07/16 19:31:10 herbelin Exp $ i*) + +Require Import Rbase. +Require Import Rfunctions. +Require Import Rseries. +Require Import PartSum. +Open Local Scope R_scope. + +(**********) +Lemma sum_N_predN : + forall (An:nat -> R) (N:nat), + (0 < N)%nat -> sum_f_R0 An N = sum_f_R0 An (pred N) + An N. +intros. +replace N with (S (pred N)). +rewrite tech5. +reflexivity. +symmetry in |- *; apply S_pred with 0%nat; assumption. +Qed. + +(**********) +Lemma sum_plus : + forall (An Bn:nat -> R) (N:nat), + sum_f_R0 (fun l:nat => An l + Bn l) N = sum_f_R0 An N + sum_f_R0 Bn N. +intros. +induction N as [| N HrecN]. +reflexivity. +do 3 rewrite tech5. +rewrite HrecN; ring. +Qed. + +(* The main result *) +Theorem cauchy_finite : + forall (An Bn:nat -> R) (N:nat), + (0 < N)%nat -> + sum_f_R0 An N * sum_f_R0 Bn N = + sum_f_R0 (fun k:nat => sum_f_R0 (fun p:nat => An p * Bn (k - p)%nat) k) N + + sum_f_R0 + (fun k:nat => + sum_f_R0 (fun l:nat => An (S (l + k)) * Bn (N - l)%nat) + (pred (N - k))) (pred N). +intros; induction N as [| N HrecN]. +elim (lt_irrefl _ H). +cut (N = 0%nat \/ (0 < N)%nat). +intro; elim H0; intro. +rewrite H1; simpl in |- *; ring. +replace (pred (S N)) with (S (pred N)). +do 5 rewrite tech5. +rewrite Rmult_plus_distr_r; rewrite Rmult_plus_distr_l; rewrite (HrecN H1). +repeat rewrite Rplus_assoc; apply Rplus_eq_compat_l. +replace (pred (S N - S (pred N))) with 0%nat. +rewrite Rmult_plus_distr_l; + replace + (sum_f_R0 (fun l:nat => An (S (l + S (pred N))) * Bn (S N - l)%nat) 0) with + (An (S N) * Bn (S N)). +repeat rewrite <- Rplus_assoc; + do 2 rewrite <- (Rplus_comm (An (S N) * Bn (S N))); + repeat rewrite Rplus_assoc; apply Rplus_eq_compat_l. +rewrite <- minus_n_n; cut (N = 1%nat \/ (2 <= N)%nat). +intro; elim H2; intro. +rewrite H3; simpl in |- *; ring. +replace + (sum_f_R0 + (fun k:nat => + sum_f_R0 (fun l:nat => An (S (l + k)) * Bn (N - l)%nat) (pred (N - k))) + (pred N)) with + (sum_f_R0 + (fun k:nat => + sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat) + (pred (pred (N - k)))) (pred (pred N)) + + sum_f_R0 (fun l:nat => An (S l) * Bn (N - l)%nat) (pred N)). +replace (sum_f_R0 (fun p:nat => An p * Bn (S N - p)%nat) N) with + (sum_f_R0 (fun l:nat => An (S l) * Bn (N - l)%nat) (pred N) + + An 0%nat * Bn (S N)). +repeat rewrite <- Rplus_assoc; + rewrite <- + (Rplus_comm (sum_f_R0 (fun l:nat => An (S l) * Bn (N - l)%nat) (pred N))) + ; repeat rewrite Rplus_assoc; apply Rplus_eq_compat_l. +replace + (sum_f_R0 + (fun k:nat => + sum_f_R0 (fun l:nat => An (S (l + k)) * Bn (S N - l)%nat) + (pred (S N - k))) (pred N)) with + (sum_f_R0 + (fun k:nat => + sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat) + (pred (N - k))) (pred N) + + Bn (S N) * sum_f_R0 (fun l:nat => An (S l)) (pred N)). +rewrite (decomp_sum An N H1); rewrite Rmult_plus_distr_r; + repeat rewrite <- Rplus_assoc; rewrite <- (Rplus_comm (An 0%nat * Bn (S N))); + repeat rewrite Rplus_assoc; apply Rplus_eq_compat_l. +repeat rewrite <- Rplus_assoc; + rewrite <- + (Rplus_comm (sum_f_R0 (fun i:nat => An (S i)) (pred N) * Bn (S N))) + ; + rewrite <- + (Rplus_comm (Bn (S N) * sum_f_R0 (fun i:nat => An (S i)) (pred N))) + ; rewrite (Rmult_comm (Bn (S N))); repeat rewrite Rplus_assoc; + apply Rplus_eq_compat_l. +replace + (sum_f_R0 + (fun k:nat => + sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat) + (pred (N - k))) (pred N)) with + (sum_f_R0 + (fun k:nat => + sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat) + (pred (pred (N - k)))) (pred (pred N)) + + An (S N) * sum_f_R0 (fun l:nat => Bn (S l)) (pred N)). +rewrite (decomp_sum Bn N H1); rewrite Rmult_plus_distr_l. +set + (Z := + sum_f_R0 + (fun k:nat => + sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat) + (pred (pred (N - k)))) (pred (pred N))); + set (Z2 := sum_f_R0 (fun i:nat => Bn (S i)) (pred N)); + ring. +rewrite + (sum_N_predN + (fun k:nat => + sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat) + (pred (N - k))) (pred N)). +replace + (sum_f_R0 + (fun k:nat => + sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat) + (pred (N - k))) (pred (pred N))) with + (sum_f_R0 + (fun k:nat => + sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat) + (pred (pred (N - k))) + An (S N) * Bn (S k)) ( + pred (pred N))). +rewrite + (sum_plus + (fun k:nat => + sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat) + (pred (pred (N - k)))) (fun k:nat => An (S N) * Bn (S k)) + (pred (pred N))). +repeat rewrite Rplus_assoc; apply Rplus_eq_compat_l. +replace (pred (N - pred N)) with 0%nat. +simpl in |- *; rewrite <- minus_n_O. +replace (S (pred N)) with N. +replace (sum_f_R0 (fun k:nat => An (S N) * Bn (S k)) (pred (pred N))) with + (sum_f_R0 (fun k:nat => Bn (S k) * An (S N)) (pred (pred N))). +rewrite <- (scal_sum (fun l:nat => Bn (S l)) (pred (pred N)) (An (S N))); + rewrite (sum_N_predN (fun l:nat => Bn (S l)) (pred N)). +replace (S (pred N)) with N. +ring. +apply S_pred with 0%nat; assumption. +apply lt_pred; apply lt_le_trans with 2%nat; [ apply lt_n_Sn | assumption ]. +apply sum_eq; intros; apply Rmult_comm. +apply S_pred with 0%nat; assumption. +replace (N - pred N)%nat with 1%nat. +reflexivity. +pattern N at 1 in |- *; replace N with (S (pred N)). +rewrite <- minus_Sn_m. +rewrite <- minus_n_n; reflexivity. +apply le_n. +symmetry in |- *; apply S_pred with 0%nat; assumption. +apply sum_eq; intros; + rewrite + (sum_N_predN (fun l:nat => An (S (S (l + i))) * Bn (N - l)%nat) + (pred (N - i))). +replace (S (S (pred (N - i) + i))) with (S N). +replace (N - pred (N - i))%nat 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 Rplus_le_reg_l with (INR i - 1). +replace (INR i - 1 + INR 1) with (INR i); [ idtac | ring ]. +replace (INR i - 1 + (INR N - INR i)) with (INR N - INR 1); [ 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%nat. +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 (N - i))) with (N - i)%nat. +apply (fun p n m:nat => plus_le_reg_l n m p) 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 0%nat. +apply plus_lt_reg_l with i; rewrite le_plus_minus_r. +replace (i + 0)%nat 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%nat. +apply lt_n_Sn. +assumption. +apply S_pred with 0%nat; assumption. +assumption. +apply le_trans with (pred (pred N)). +assumption. +apply le_trans with (pred N); apply le_pred_n. +apply S_pred with 0%nat; 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 Rplus_le_reg_l with (INR i - 1). +replace (INR i - 1 + INR 1) with (INR i); [ idtac | ring ]. +replace (INR i - 1 + (INR N - INR i)) with (INR N - INR 1); [ 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%nat. +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%nat. +apply lt_O_Sn. +apply INR_le. +rewrite pred_of_minus. +repeat rewrite minus_INR. +apply Rplus_le_reg_l with (INR i - 1). +replace (INR i - 1 + INR 1) with (INR i); [ idtac | ring ]. +replace (INR i - 1 + (INR N - INR i - INR 1)) with (INR N - INR 1 - INR 1). +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 (fun p n m:nat => plus_le_reg_l n m p) with 1%nat. +rewrite le_plus_minus_r. +simpl in |- *; assumption. +apply le_trans with 2%nat; [ apply le_n_Sn | assumption ]. +apply le_trans with 2%nat; [ 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 (fun p n m:nat => plus_le_reg_l n m p) with i. +rewrite le_plus_minus_r. +replace (i + 1)%nat 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 in |- *; apply S_pred with 0%nat; 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%nat. +apply lt_O_Sn. +apply le_S_n. +replace (S (pred N)) with N. +assumption. +apply S_pred with 0%nat; assumption. +replace + (sum_f_R0 + (fun k:nat => + sum_f_R0 (fun l:nat => An (S (l + k)) * Bn (S N - l)%nat) + (pred (S N - k))) (pred N)) with + (sum_f_R0 + (fun k:nat => + sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat) + (pred (N - k)) + An (S k) * Bn (S N)) (pred N)). +rewrite + (sum_plus + (fun k:nat => + sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat) + (pred (N - k))) (fun k:nat => An (S k) * Bn (S N))) + . +apply Rplus_eq_compat_l. +rewrite scal_sum; reflexivity. +apply sum_eq; intros; rewrite Rplus_comm; + rewrite + (decomp_sum (fun l:nat => An (S (l + i)) * Bn (S N - l)%nat) + (pred (S N - i))). +replace (0 + i)%nat with i; [ idtac | ring ]. +rewrite <- minus_n_O; apply Rplus_eq_compat_l. +replace (pred (pred (S N - i))) with (pred (N - i)). +apply sum_eq; intros. +replace (S N - S i0)%nat with (N - i0)%nat; [ idtac | reflexivity ]. +replace (S i0 + i)%nat with (S (i0 + i)). +reflexivity. +apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; rewrite S_INR; ring. +cut ((N - i)%nat = pred (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 (fun p n m:nat => plus_le_reg_l n m p) with i. +rewrite le_plus_minus_r. +replace (i + 1)%nat 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 (S N - i)) with (S N - S i)%nat. +replace (S N - S i)%nat with (N - i)%nat; [ idtac | reflexivity ]. +apply plus_lt_reg_l with i. +rewrite le_plus_minus_r. +replace (i + 0)%nat 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 (fun p n m:nat => plus_le_reg_l n m p) with i. +rewrite le_plus_minus_r. +replace (i + 1)%nat 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_comm. +rewrite (decomp_sum (fun p:nat => An p * Bn (S N - p)%nat) N). +rewrite <- minus_n_O. +apply Rplus_eq_compat_l. +apply sum_eq; intros. +reflexivity. +assumption. +rewrite Rplus_comm. +rewrite + (decomp_sum + (fun k:nat => + sum_f_R0 (fun l:nat => An (S (l + k)) * Bn (N - l)%nat) (pred (N - k))) + (pred N)). +rewrite <- minus_n_O. +replace (sum_f_R0 (fun l:nat => An (S (l + 0)) * Bn (N - l)%nat) (pred N)) + with (sum_f_R0 (fun l:nat => An (S l) * Bn (N - l)%nat) (pred N)). +apply Rplus_eq_compat_l. +apply sum_eq; intros. +replace (pred (N - S i)) with (pred (pred (N - i))). +apply sum_eq; intros. +replace (i0 + S i)%nat with (S (i0 + i)). +reflexivity. +apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; rewrite S_INR; ring. +cut (pred (N - i) = (N - S i)%nat). +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 0%nat. +apply lt_S_n. +replace (S (pred N)) with N. +apply lt_le_trans with 2%nat. +apply lt_n_Sn. +assumption. +apply S_pred with 0%nat; assumption. +apply le_trans with (pred (pred N)). +assumption. +apply le_trans with (pred N); apply le_pred_n. +apply (fun p n m:nat => plus_le_reg_l n m p) with i. +rewrite le_plus_minus_r. +replace (i + 1)%nat 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 in |- *; apply S_pred with 0%nat; 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 (i + 0)%nat with i; [ reflexivity | trivial ]. +apply lt_S_n. +replace (S (pred N)) with N. +apply lt_le_trans with 2%nat; [ apply lt_n_Sn | assumption ]. +apply S_pred with 0%nat; assumption. +inversion H1. +left; reflexivity. +right; apply le_n_S; assumption. +simpl in |- *. +replace (S (pred N)) with N. +reflexivity. +apply S_pred with 0%nat; assumption. +simpl in |- *. +cut ((N - pred N)%nat = 1%nat). +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 in |- *; symmetry in |- *; apply S_pred with 0%nat; assumption. +inversion H. +left; reflexivity. +right; apply lt_le_trans with 1%nat; [ apply lt_n_Sn | exact H1 ]. +Qed.
\ No newline at end of file |