proposition: Lemma Rpser_cv_speed_pow_id : forall x : R, Rabs x < 1 -> Un_cv (fun n : nat => INR (S n) * x ^ S n) 0.
proof: Proof. intros x x_bd eps eps_pos. case (Req_or_neq x) ; intro Hx. exists 0%nat ; intros ; unfold R_dist ; rewrite Rminus_0_r ; rewrite Hx ; rewrite pow_i ; [| intuition (auto with arith)] ; rewrite Rmult_0_r ; rewrite Rabs_R0 ; assumption. assert (H : Un_cv (fun n => /INR (S n)) 0). apply cv_infty_cv_0. intro B ; assert (0 <= IZR (up (Rabs B))). apply Rle_trans with (Rabs B) ; [apply Rabs_pos |] ; apply Rge_le ; left ; apply (proj1 (archimed (Rabs B))). assert (H1 : (0 <= up (Rabs B))%Z). apply le_IZR ; assumption. destruct (IZN (up (Rabs B)) H1) as (N, HN) ; exists N ; intros n n_lb ; apply Rlt_le_trans with (INR (S N)). apply Rlt_trans with (IZR (up (Rabs B))). apply Rle_lt_trans with (Rabs B) ; [apply RRle_abs |] ; apply (proj1 (archimed (Rabs B))). rewrite HN. rewrite <- INR_IZR_INZ. intuition (auto with real). intuition (auto with arith real). assert (Rinv_r_pos : 0 < (1 + 1 / Rabs x) / 2 - 1). apply Rlt_Rminus ; apply Rle_lt_trans with ((1 + 1)/2). right ; field. unfold Rdiv ; apply Rmult_lt_compat_r. apply Rinv_0_lt_compat ; intuition (auto with real). apply Rplus_lt_compat_l ; rewrite Rmult_1_l ; rewrite <- Rinv_1 ; apply Rinv_lt_contravar. rewrite Rmult_1_r ; apply Rabs_pos_lt ; assumption. assumption. pose (k := (1 + Rabs x) / 2). assert (k_pos : 0 <= k). unfold k ; replace 0 with (0/2) by field ; unfold Rdiv ; apply Rmult_le_compat_r. left ; apply Rinv_0_lt_compat ; intuition (auto with real). apply Rle_zero_pos_plus1 ; apply Rabs_pos. assert (k_lt_1 : ((1 + Rabs x) / 2) < 1). apply Rlt_le_trans with ((1 + 1) /2). unfold Rdiv ; apply Rmult_lt_compat_r. apply Rinv_0_lt_compat ; intuition (auto with real). apply Rplus_lt_compat_l ; assumption. right ; field. assert (Main : forall M eps, 0 < eps -> 0 < M -> exists N, forall n, (n >= N)%nat -> M * ((1 + Rabs x) / 2) ^ n < eps). clear -k_lt_1 k_pos ; intros M eps eps_pos M_pos ; assert (r_bd : 0 <= (1 + Rabs x) / 2 < 1) by intuition ; destruct (Rseq_pow_lt_1_cv ((1 + Rabs x) / 2) r_bd (eps / M)) as (N, HN). unfold Rdiv ; apply Rmult_lt_0_compat ; [| apply Rinv_0_lt_compat] ; assumption. exists N ; intros n n_lb. apply Rlt_le_trans with (M * (eps / M)). apply Rmult_lt_compat_l. assumption. replace (((1 + Rabs x) / 2) ^ n) with (Rabs (((1 + Rabs x) / 2) ^ n - 0)). apply HN ; assumption. rewrite Rminus_0_r ; apply Rabs_right. apply Rle_ge ; apply pow_le ; assumption. right ; field ; apply Rgt_not_eq ; assumption. destruct (H ((1 + 1 / Rabs x) / 2 - 1) Rinv_r_pos) as (N, HN). assert (Temp : forall M i : nat, (M >= S N)%nat -> Rabs (INR (i + S M) * x ^ (i + S M)) < (1 + Rabs x) / 2 * Rabs (INR (i + M) * x ^ (i + M))). intros M i M_lb. apply Rle_lt_trans with (Rabs ((INR (i + S M) / (INR (i + M))) * ((INR (i + M)) * x ^ (i + S M)))). right ; apply Rabs_eq_compat ; field ; apply Rgt_not_eq ; apply lt_0_INR; lia. replace (i + S M)%nat with (S (i + M))%nat by intuition lia. rewrite <- tech_pow_Rmult. repeat (rewrite Rabs_mult ; rewrite <- Rmult_assoc). apply Rmult_lt_compat_r. apply Rabs_pos_lt ; apply pow_nonzero ; assumption. rewrite Rmult_comm, <- Rmult_assoc. apply Rmult_lt_compat_r. apply Rabs_pos_lt ; apply Rgt_not_eq ; apply lt_0_INR; lia. replace (INR (S (i + M)) / INR (i + M)) with (1 + / INR (i + M)). apply Rlt_le_trans with (Rabs x * (1 + 1 / Rabs x) / 2). unfold Rdiv ; rewrite Rmult_assoc ; apply Rmult_lt_compat_l. apply Rabs_pos_lt ; assumption. rewrite Rabs_right. assert (Temp : forall a b c, b < c - a -> a + b < c). clear ; intros ; lra. apply Temp. replace (/INR (i + M)) with (R_dist (/INR (S (i + pred M))) 0). apply HN ; intuition lia. unfold R_dist ; rewrite Rminus_0_r ; replace (S (i + pred M))%nat with (i + M)%nat. apply Rabs_right ; left ; apply Rinv_0_lt_compat ; apply lt_0_INR; lia. intuition lia. apply Rle_ge ; apply Rle_zero_pos_plus1. left ; apply Rinv_0_lt_compat; apply lt_0_INR; lia. right ; field. apply Rgt_not_eq ; apply Rabs_pos_lt ; assumption. replace (INR (S (i + M))) with (1 + INR (i + M)). field ; apply Rgt_not_eq ; apply lt_0_INR; lia. replace (S (i + M)) with (1 + (i + M))%nat by intuition ; rewrite S_O_plus_INR. intuition. pose (An_0 := Rabs (INR (S N))). assert (An_0_pos : 0 < An_0 * Rabs x ^ (S N)). apply Rmult_lt_0_compat. unfold An_0 ; apply Rabs_pos_lt ; apply Rgt_not_eq ; intuition (auto with *). apply pow_lt ; apply Rabs_pos_lt ; assumption. destruct (Main (An_0 * Rabs x ^ (S N)) eps eps_pos An_0_pos) as (N2, HN2). exists (N2 + S N)%nat ; intros n n_lb. fold k in Temp. assert (Temp2 : forall i : nat, (fun i0 : nat => Rabs (INR (i0 + S N) * x ^ (i0 + S N))) (S i) < k * (fun i0 : nat => Rabs (INR (i0 + S N) * x ^ (i0 + S N))) i). intro i. replace (S i + S N)%nat with (i + S (S N))%nat by ring. apply Temp ; intuition. clear Temp. unfold R_dist, Rminus ; rewrite Ropp_0 ; rewrite Rplus_0_r. assert (Temp : forall m n, (m >= n)%nat -> {p | (m = n + p)%nat}). clear ; intros m n ; induction n ; intro H. exists m ; intuition lia. case (le_lt_eq_dec _ _ H) ; clear H ; intro H. assert (H' : (m >= n)%nat) by intuition lia. destruct (IHn H') as (p, Hp) ; destruct p. exists 0%nat ; apply False_ind ; intuition lia. exists p ; intuition lia. exists 0%nat ; intuition lia. destruct (Temp n (N2 + S N)%nat n_lb) as (p,Hp). rewrite Hp. replace (S (N2 + S N + p))%nat with ((S N2 + p) + S N)%nat by intuition lia. assert (H' := tech4 (fun i : nat => Rabs (INR (i + S N) * x ^ (i + S N))) k (S N2 + p) k_pos Temp2). apply Rle_lt_trans with (Rabs (INR (0 + S N) * x ^ (0 + S N)) * k ^ (S N2 + p)). apply H'. simpl (0 + S N)%nat ; rewrite Rabs_mult ; fold An_0 ; unfold k ; rewrite <- RPow_abs ; apply HN2. intuition (auto with arith). Qed.
imports: Reals MyRIneq Fourier Lia Lra Rsequence_usual_facts