proposition: Lemma Ratan_seq_converging : forall x, (0 <= x <= 1)%R -> Un_cv (Ratan_seq x) 0.
proof: Proof. intros x Hx eps Heps. destruct (archimed (/ eps)) as (HN,_). assert (0 < up (/ eps))%Z. { apply lt_IZR. apply Rlt_trans with (2 := HN). apply Rinv_0_lt_compat. exact Heps. } case_eq (up (/ eps)) ; intros ; rewrite H0 in H ; try discriminate H. rewrite H0 in HN. simpl in HN. pose (N := Pos.to_nat p). fold N in HN. clear H H0. exists N. intros n Hn. unfold Rdist. rewrite Rminus_0_r. unfold Ratan_seq. rewrite Rabs_right. 2:{ apply Rle_ge. unfold Rdiv. apply Rmult_le_pos. { apply pow_le. exact (proj1 Hx). } apply Rlt_le. apply Rinv_0_lt_compat. apply lt_INR_0. lia. } apply Rle_lt_trans with (1 ^ (2 * n + 1) / INR (2 * n + 1))%R. { unfold Rdiv. apply Rmult_le_compat_r. { apply Rlt_le. apply Rinv_0_lt_compat. apply lt_INR_0. lia. } apply pow_incr. exact Hx. } rewrite pow1. apply Rle_lt_trans with (/ INR (2 * N + 1))%R. { unfold Rdiv. rewrite Rmult_1_l. apply Rinv_le_contravar. { apply lt_INR_0. lia. } apply le_INR. lia. } rewrite <- (Rinv_inv eps). apply Rinv_lt_contravar. { apply Rmult_lt_0_compat. { auto with real. } apply lt_INR_0. lia. } apply Rlt_trans with (INR N). { destruct (archimed (/ eps)) as (H,_). assert (0 < up (/ eps))%Z. { apply lt_IZR. apply Rlt_trans with (2 := H). apply Rinv_0_lt_compat. exact Heps. } unfold N. rewrite INR_IZR_INZ, positive_nat_Z. exact HN. } apply lt_INR. lia. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia