proposition: Lemma alternate_series_conv : convergent (fun n => [--][1][^]n[*]x n).
proof: Proof. red in |- *. red in |- *. intros e H. elim (Lim_x e H). intros N' HN'. cut {N : nat | 0 < N | forall m : nat, N <= m -> AbsSmall e (x m)}. intro H0. elim H0; clear H0; intros N HNm HN. exists N; intros. apply AbsSmall_transitive with (x N). apply HN; auto. cut (AbsIR (seq_part_sum (fun n : nat => [--][1][^]n[*]x n) m[-] seq_part_sum (fun n : nat => [--][1][^]n[*]x n) N) [=] AbsIR ( [--][1][^]N[*]Sum N (pred m) y)). intro. apply leEq_wdl with (AbsIR ( [--][1][^]N[*]Sum N (pred m) y)). eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x; apply pos_x. cut ({N < m} + {N = m}); intros. 2: apply le_lt_eq_dec; assumption. apply leEq_wdl with (Max ( [--][1][^]N[*]Sum N (pred m) y) [--] ( [--][1][^]N[*]Sum N (pred m) y)). apply Max_leEq. inversion_clear H2. cut {j : nat & {pred m = N + (j + j)} + {pred m = N + S (j + j)}}. 2: apply even_or_odd_plus_gt; apply le_2; auto. intro. elim H2; intros j Hj. clear H2; inversion_clear Hj. rewrite H2; apply alternate_lemma1. rewrite H2; apply alternate_lemma2. rewrite <- H3. cut (Sum N (pred N) y [=] [0]); [ intro | apply Sum_empty; auto ]. astepl ( [--][1][^]N[*]ZeroR). astepl ZeroR; apply pos_x. astepr ( [--][--] (x N)); apply inv_resp_leEq. apply leEq_transitive with ZeroR. astepr ( [--]ZeroR); apply inv_resp_leEq; apply pos_x. inversion_clear H2. cut {j : nat & {pred m = N + (j + j)} + {pred m = N + S (j + j)}}. 2: apply even_or_odd_plus_gt; apply le_2; auto. intro. elim H2; intros j Hj. clear H2; inversion_clear Hj. rewrite H2; apply alternate_lemma4. rewrite H2; apply alternate_lemma3. rewrite <- H3. cut (Sum N (pred N) y [=] [0]); [ intro | apply Sum_empty; auto ]. astepr ( [--][1][^]N[*]ZeroR). astepr ZeroR; apply leEq_reflexive. simpl in |- *; unfold ABSIR in |- *; apply eq_reflexive_unfolded. apply eq_symmetric_unfolded; assumption. destruct (Nat.Even_or_Odd N) as [HE | HO]. apply AbsIR_wd. eapply eq_transitive_unfolded. apply seq_part_sum_n; auto; apply Nat.lt_le_trans with N; auto. eapply eq_transitive_unfolded. 2: apply Sum_comm_scal'. apply Sum_wd. intro. unfold y in |- *. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply mult_assoc_unfolded. apply mult_wdl. astepl (OneR[*][--][1][^]i). apply mult_wdl. apply eq_symmetric_unfolded; apply inv_one_even_nexp; assumption. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply AbsIR_inv. apply AbsIR_wd. eapply eq_transitive_unfolded. apply seq_part_sum_n; auto; apply Nat.lt_le_trans with N; auto. rstepr ( [--] ( [--][1][^]N) [*]Sum N (pred m) y). eapply eq_transitive_unfolded. 2: apply Sum_comm_scal'. apply Sum_wd. intro. unfold y in |- *. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply mult_assoc_unfolded. apply mult_wdl. astepl (OneR[*][--][1][^]i). now apply mult_wdl; rewrite inv_one_odd_nexp, cg_inv_inv by assumption. exists (S N'); [exact (Nat.lt_0_succ _) |]. intros. astepr (x m[-][0]); apply HN'; auto with arith. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)