proposition: Lemma cn_maj : forall n N, (n <= N)%nat -> Rabs (cn (Z_of_nat n) N) <= / (INR (N - n + 1)).
proof: Proof. intros. destruct n. simpl; rewrite cn_zero_zero. unfold Rabs. destruct (Rcase_abs 0); left; replace (- 0) with 0 by ring; apply Rinv_0_lt_compat; INR_solve. unfold Z_of_nat. rewrite cn_pos with n N; [|assumption]. rewrite Rabs_mult; rewrite pow_1_abs; rewrite Rmult_1_l. replace (sum_f_R0 (fun j : nat => (-1) ^ (j + N - n) * / INR (j + N - n)) (S (2 * n))) with ((-1) ^ (N - n) * sum_f_R0 (fun j : nat => (-1) ^ j * / INR (j + N - n)) (S (2 * n))). 2:rewrite scal_sum. 2:apply Rseq_sum_ext; intro. 2:replace (n0 + N - n)%nat with (n0 + (N - n))%nat by lia. 2:rewrite Rdef_pow_add; ring. rewrite Rabs_mult; rewrite pow_1_abs; rewrite Rmult_1_l. cut (forall i, Rabs (sum_f_R0 (fun j : nat => (-1) ^ j * / INR (j + N - n)) i) <= / INR (N - S n + 1)) ;[intuition | ]. replace (N - S n + 1)%nat with (N - n)%nat by lia. pose (N - n)%nat as k; fold k. assert (kpos : (0 < k)%nat) by (unfold k; lia). pose (fun j => / INR (j + k)) as Un. intro i; replace (sum_f_R0 (fun j => (-1) ^ j * / INR (j + N - n)) i) with (sum_f_R0 (fun j => (-1) ^ j * / INR (j + k)) i) by (apply Rseq_sum_ext; intro; trivial; inject; unfold k; lia). replace (sum_f_R0 (fun j => (-1) ^ j * / INR (j + k)) i) with (sum_f_R0 (tg_alt Un) i) by (apply Rseq_sum_ext; intro; trivial). replace (/ INR k) with (Un O) by trivial. edestruct (alt_bounding Un). intro; unfold Un. apply Rle_Rinv; INR_solve. intro; unfold Un; apply Rlt_le; apply Rinv_0_lt_compat; INR_solve. assert (0 <= sum_f_R0 (tg_alt Un) i) by apply H0. rewrite Rabs_pos_eq by apply H2. apply H1. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith