proposition: Lemma harmonic_series_equiv : (sum_f_R0 (fun n => / (S n))) ~ (fun n => ln (S (S n))).
proof: Proof. destruct (Rser_RiemannInt_cv_pos_infty (/(id + fct_cte 1))%F) as [int_f_0_n Hi]; unfold plus_fct, fct_cte, id, inv_fct. intros x Hx. apply continuity_pt_inv. apply (continuity_pt_plus _ _ _ (derivable_continuous id derivable_id x) (derivable_continuous _ (derivable_const 1) x)). auto with *. auto with *. intros x y [Hxpos Hxy]. apply Rle_Rinv; lra. assert (Heq2 : (fun n : nat => ln (INR (S (S n)))) == (fun n : nat => RiemannInt (int_f_0_n (S n)))). intro n. replace (ln (S (S n))) with ((ln (S n + 1)%R - ln (O + 1))). destruct (Rint_inv1 0%nat (S n)) as [Hint Heq]. change (INR O) with 0. auto with *. rewrite <- Heq. apply RiemannInt_P18. auto with *. reflexivity. replace (INR (S n) + 1) with (INR (S (S n))) by trivial. replace (INR 0 + 1) with 1 by (simpl; ring). rewrite ln_1. ring. assert(Rseq_cv_pos_infty (fun n : nat => RiemannInt (int_f_0_n (S n)))) as Hdiv. apply Rseq_cv_pos_infty_eq_compat with (fun n : nat => ln (S (S n))). apply Heq2. apply Rseq_subseq_cv_pos_infty_compat with (fun n => ln n). assert (Hex : is_extractor (fun n => (S (S n)))). constructor. exists (exist _ _ Hex). trivial. apply Rseq_ln_cv. assert(Heq1 : (sum_f_R0 (fun n : nat => (/ (id + fct_cte 1))%F (INR n))) == (sum_f_R0 (fun n : nat => / INR (S n)))). intro n; apply sum_eq; intros k Hk. unfold inv_fct, id, plus_fct, fct_cte. rewrite S_INR. reflexivity. apply Rseq_eq_sym in Heq2. apply (Rseq_equiv_eq_compat _ _ _ _ Heq1 Heq2 (Hi Hdiv)). Qed.
imports: Reals Rseries_def Rseries_facts RiemannInt Lra Rsequence_facts Rsequence_subsequence Riemann_integrable Rintegral