proposition: Lemma sum_maj1 : forall (fn:nat -> R -> R) (An:nat -> R) (x l1 l2:R) (N:nat), Un_cv (fun n:nat => SP fn n x) l1 -> Un_cv (fun n:nat => sum_f_R0 An n) l2 -> (forall n:nat, Rabs (fn n x) <= An n) -> Rabs (l1 - SP fn N x) <= l2 - sum_f_R0 An N.
proof: Proof. intros; assert (X:{ l:R | Un_cv (fun n => sum_f_R0 (fun l => fn (S N + l)%nat x) n) l }). { exists (l1 - SP fn N x). unfold Un_cv in H; unfold Un_cv; intros. elim (H eps H2); intros N0 H3. unfold Rdist in H3; exists N0; intros. unfold Rdist, SP. replace (sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n - (l1 - sum_f_R0 (fun k:nat => fn k x) N)) with (sum_f_R0 (fun k:nat => fn k x) N + sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n - l1); [ idtac | ring ]. replace (sum_f_R0 (fun k:nat => fn k x) N + sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n) with (sum_f_R0 (fun k:nat => fn k x) (S (N + n))). { unfold SP in H3; apply H3. unfold ge; apply Nat.le_trans with n. - apply H4. - apply Nat.le_trans with (N + n)%nat. + apply Nat.le_add_l. + apply Nat.le_succ_diag_r. } cut (0 <= N)%nat. 2:{ apply Nat.le_0_l. } cut (N < S (N + n))%nat. 2:{ apply Nat.lt_succ_r. apply Nat.le_add_r. } intros; assert (H7 := sigma_split (fun k:nat => fn k x) H6 H5). unfold sigma in H7. do 2 rewrite Nat.sub_0_r in H7. replace (sum_f_R0 (fun k:nat => fn k x) (S (N + n))) with (sum_f_R0 (fun k:nat => fn (0 + k)%nat x) (S (N + n))) by reflexivity. replace (sum_f_R0 (fun k:nat => fn k x) N) with (sum_f_R0 (fun k:nat => fn (0 + k)%nat x) N) by reflexivity. assert ((S (N + n) - S N)%nat = n). { apply INR_eq; rewrite minus_INR. - do 2 rewrite S_INR; rewrite plus_INR; ring. - apply -> Nat.succ_le_mono; apply Nat.le_add_r. } rewrite H8 in H7. apply H7. } assert { l:R | Un_cv (fun n => sum_f_R0 (fun l => An (S N + l)%nat) n) l } as X0. { exists (l2 - sum_f_R0 An N). unfold Un_cv in H0; unfold Un_cv; intros. elim (H0 eps H2); intros N0 H3. unfold Rdist in H3; exists N0; intros. unfold Rdist; replace (sum_f_R0 (fun l:nat => An (S N + l)%nat) n - (l2 - sum_f_R0 An N)) with (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n - l2); [ idtac | ring ]. replace (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n) with (sum_f_R0 An (S (N + n))). 2:{ cut (0 <= N)%nat. 2:{ apply Nat.le_0_l. } cut (N < S (N + n))%nat. 2:{ apply Nat.lt_succ_r. apply Nat.le_add_r. } intros; assert (H7 := sigma_split An H6 H5). unfold sigma in H7. do 2 rewrite Nat.sub_0_r in H7. replace (sum_f_R0 An (S (N + n))) with (sum_f_R0 (fun k:nat => An (0 + k)%nat) (S (N + n))) by reflexivity. replace (sum_f_R0 An N) with (sum_f_R0 (fun k:nat => An (0 + k)%nat) N) by reflexivity. assert ((S (N + n) - S N)%nat = n). { apply INR_eq; rewrite minus_INR. - do 2 rewrite S_INR; rewrite plus_INR; ring. - apply -> Nat.succ_le_mono; apply Nat.le_add_r. } rewrite H8 in H7. apply H7. } apply H3; unfold ge; apply Nat.le_trans with n. - apply H4. - apply Nat.le_trans with (N + n)%nat. + apply Nat.le_add_l. + apply Nat.le_succ_diag_r. } elim X; intros l1N H2. elim X0; intros l2N H3. cut (l1 - SP fn N x = l1N). 1:intro; cut (l2 - sum_f_R0 An N = l2N). { intro; rewrite H4; rewrite H5. apply sum_cv_maj with (fun l:nat => An (S N + l)%nat) (fun (l:nat) (x:R) => fn (S N + l)%nat x) x. - unfold SP; apply H2. - apply H3. - intros; apply H1. } { symmetry ; eapply UL_sequence. { apply H3. } unfold Un_cv in H0; unfold Un_cv; intros; elim (H0 eps H5); intros N0 H6. unfold Rdist in H6; exists N0; intros. unfold Rdist; replace (sum_f_R0 (fun l:nat => An (S N + l)%nat) n - (l2 - sum_f_R0 An N)) with (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n - l2); [ idtac | ring ]. replace (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n) with (sum_f_R0 An (S (N + n))). { apply H6; unfold ge; apply Nat.le_trans with n. - apply H7. - apply Nat.le_trans with (N + n)%nat. + apply Nat.le_add_l. + apply Nat.le_succ_diag_r. } cut (0 <= N)%nat. 2:{ apply Nat.le_0_l. } cut (N < S (N + n))%nat. 2:{ apply Nat.lt_succ_r. apply Nat.le_add_r. } intros; assert (H10 := sigma_split An H9 H8). unfold sigma in H10. do 2 rewrite Nat.sub_0_r in H10. replace (sum_f_R0 An (S (N + n))) with (sum_f_R0 (fun k:nat => An (0 + k)%nat) (S (N + n))) by reflexivity. replace (sum_f_R0 An N) with (sum_f_R0 (fun k:nat => An (0 + k)%nat) N) by reflexivity. cut ((S (N + n) - S N)%nat = n). { intro; rewrite H11 in H10. apply H10. } apply INR_eq; rewrite minus_INR. - do 2 rewrite S_INR; rewrite plus_INR; ring. - apply le_n_S; apply Nat.le_add_r. } symmetry ; eapply UL_sequence. { apply H2. } unfold Un_cv in H; unfold Un_cv; intros. elim (H eps H4); intros N0 H5. unfold Rdist in H5; exists N0; intros. unfold Rdist, SP; replace (sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n - (l1 - sum_f_R0 (fun k:nat => fn k x) N)) with (sum_f_R0 (fun k:nat => fn k x) N + sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n - l1); [ idtac | ring ]. replace (sum_f_R0 (fun k:nat => fn k x) N + sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n) with (sum_f_R0 (fun k:nat => fn k x) (S (N + n))). { unfold SP in H5; apply H5; unfold ge; apply Nat.le_trans with n. - apply H6. - apply Nat.le_trans with (N + n)%nat. + apply Nat.le_add_l. + apply Nat.le_succ_diag_r. } cut (0 <= N)%nat. 2:{ apply Nat.le_0_l. } cut (N < S (N + n))%nat. 2:{ apply Nat.lt_succ_r. apply Nat.le_add_r. } intros; assert (H9 := sigma_split (fun k:nat => fn k x) H8 H7). unfold sigma in H9. do 2 rewrite Nat.sub_0_r in H9. replace (sum_f_R0 (fun k:nat => fn k x) (S (N + n))) with (sum_f_R0 (fun k:nat => fn (0 + k)%nat x) (S (N + n))) by reflexivity. replace (sum_f_R0 (fun k:nat => fn k x) N) with (sum_f_R0 (fun k:nat => fn (0 + k)%nat x) N) by reflexivity. cut ((S (N + n) - S N)%nat = n). { intro; rewrite H10 in H9. apply H9. } apply INR_eq; rewrite minus_INR. - do 2 rewrite S_INR; rewrite plus_INR; ring. - apply le_n_S; apply Nat.le_add_r. Qed.
imports: Rbase Rfunctions Rseries SeqProp Rcomplete PartSum AltSeries Binomial Rsigma Rprod Cauchy_prod Alembert Lra