proposition: Lemma CV_ALT : forall Un:nat -> R, Un_decreasing Un -> positivity_seq Un -> Un_cv Un 0 -> { l:R | Un_cv (fun N:nat => sum_f_R0 (tg_alt Un) N) l }.
proof: Proof. intros. assert (H2 := CV_ALT_step0 _ H). assert (H3 := CV_ALT_step4 _ H H0). destruct (growing_cv _ H2 H3) as (x,p). exists x. unfold Un_cv; unfold Rdist; unfold Un_cv in H1; unfold Rdist in H1; unfold Un_cv in p; unfold Rdist in p. intros; cut (0 < eps / 2); [ intro | unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. elim (H1 (eps / 2) H5); intros N2 H6. elim (p (eps / 2) H5); intros N1 H7. set (N := max (S (2 * N1)) N2). exists N; intros. assert (H9 := even_odd_cor n). elim H9; intros P H10. assert (N1 <= P)%nat. { elim H10; intro; apply le_double. - rewrite <- H11; apply Nat.le_trans with N. + unfold N; apply Nat.le_trans with (S (2 * N1)); [ apply Nat.le_succ_diag_r | apply Nat.le_max_l ]. + assumption. - apply Nat.lt_succ_r. rewrite <- H11. apply Nat.lt_le_trans with N. + unfold N; apply Nat.lt_le_trans with (S (2 * N1)). * apply Nat.lt_succ_diag_r. * apply Nat.le_max_l. + assumption. } elim H10; intro. - replace (sum_f_R0 (tg_alt Un) n - x) with (sum_f_R0 (tg_alt Un) (S n) - x + - tg_alt Un (S n)). + apply Rle_lt_trans with (Rabs (sum_f_R0 (tg_alt Un) (S n) - x) + Rabs (- tg_alt Un (S n))). * apply Rabs_triang. * rewrite <-(Rplus_half_diag eps); apply Rplus_lt_compat. -- rewrite H12; apply H7; assumption. -- rewrite Rabs_Ropp; unfold tg_alt; rewrite Rabs_mult; rewrite pow_1_abs; rewrite Rmult_1_l; unfold Rminus in H6; rewrite Ropp_0 in H6; rewrite <- (Rplus_0_r (Un (S n))); apply H6. unfold ge; apply Nat.le_trans with n. ++ apply Nat.le_trans with N; [ unfold N; apply Nat.le_max_r | assumption ]. ++ apply Nat.le_succ_diag_r. + rewrite tech5; ring. - rewrite H12; apply Rlt_trans with (eps / 2). + apply H7; assumption. + unfold Rdiv; apply Rmult_lt_reg_l with 2. * prove_sup0. * rewrite (Rmult_comm 2); rewrite Rmult_assoc; rewrite Rinv_l; [ rewrite Rmult_1_r | discrR ]. rewrite <-Rplus_diag. pattern eps at 1; rewrite <- (Rplus_0_r eps); apply Rplus_lt_compat_l; assumption. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra