proposition: Lemma Cauchy_crit_Rseq_pps : forall An r, Cv_radius_weak An r -> forall x, Rabs x < r -> Cauchy_crit (Rseq_pps An x).
proof: Proof. intros An r rho x x_ub eps eps_pos. assert (r_pos : 0 < r). apply Rle_lt_trans with (Rabs x) ; [apply Rabs_pos | assumption]. assert (r_neq : 0 <> r) by (apply Rlt_not_eq ; assumption). assert (Hrew_abs : Rabs (x / r) = Rabs x / r). unfold Rdiv ; rewrite Rabs_mult ; apply Rmult_eq_compat_l ; apply Rabs_right ; apply Rgt_ge ; apply Rlt_gt ; apply Rinv_0_lt_compat ; apply Rle_lt_trans with (Rabs x) ; [apply Rabs_pos | assumption]. assert (Rabsx_r_lt_1 : Rabs x / r < 1). rewrite <- (Rinv_r r) ; [| symmetry ; assumption] ; unfold Rdiv ; apply Rmult_lt_compat_r ; [apply Rinv_0_lt_compat |] ; assumption. destruct (Req_or_neq x) as [x_eq | x_neq]. exists O ; intros ; subst ; do 2 rewrite Rseq_pps_0_simpl ; rewrite R_dist_eq ; assumption. assert (Temp : forall m n, (m < n)%nat -> R_dist (Rseq_pps An x n) (Rseq_pps An x m) = Rabs (Rseq_sum (Rseq_shifts (gt_pser An x) (S (Nat.min m n))) ((Nat.max m n) - S (Nat.min m n)))). intros m n m_neq_n ; unfold R_dist ; apply Rabs_eq_compat ; replace (Nat.max m n) with n. replace (Nat.min m n) with m. rewrite Rseq_sum_shifts_compat ; unfold Rseq_shifts ; replace (S m + (n - S m))%nat with n by lia ; reflexivity. symmetry ; apply Nat.min_l ; intuition (auto with arith). symmetry ; apply Nat.max_r ; intuition (auto with arith). assert (Hrew : forall m n, m <> n -> R_dist (Rseq_pps An x n) (Rseq_pps An x m) = Rabs (Rseq_sum (Rseq_shifts (gt_pser An x) (S (Nat.min m n))) ((Nat.max m n) - S (Nat.min m n)))). intros m n m_neq_n ; unfold R_dist ; destruct (le_lt_dec m n) as [mlen | nltm]. assert (mltn : (m < n)%nat) by (clear -m_neq_n mlen ; lia) ; apply Temp ; assumption. rewrite Rabs_minus_sym, Nat.min_comm, Nat.max_comm ; apply Temp ; assumption. clear Temp. assert (Hineq : exists M, forall m n, m <> n -> R_dist (Rseq_pps An x n) (Rseq_pps An x m) <= M * Rseq_sum (Rseq_shifts (pow (Rabs x / r)) (S (Nat.min m n))) ((Nat.max m n) - S (Nat.min m n))). destruct rho as [B HB] ; exists B ; intros m n m_neq_n ; rewrite Hrew ; [| assumption]. assert (Temp : forall k n, Rabs (Rseq_sum (Rseq_shifts (gt_pser An x) k) n) <= B * Rseq_sum (Rseq_shifts (pow (Rabs x / r)) k) n). clear - r_neq r_pos Hrew_abs HB; intros k n ; induction n. simpl ; do 2 rewrite Rseq_shifts_O ; rewrite <- (Rmult_1_r (gt_pser An x k)), <- (Rinv_r (r ^ k)), <- Rmult_assoc, Rabs_mult, <- pow_inv ; [| apply pow_nonzero ; symmetry ; assumption]. apply Rle_trans with (Rabs (gt_pser An r k) * Rabs (x ^ k) * Rabs ((/ r) ^ k)). right ; repeat rewrite <- Rabs_mult ; apply Rabs_eq_compat ; unfold gt_pser, Rseq_mult ; ring. apply Rle_trans with ((gt_abs_pser An r k) * (Rabs x / r) ^ k). right ; rewrite Rmult_assoc ; apply Rmult_eq_compat_l ; rewrite <- Hrew_abs, <- Rabs_mult, <- Rpow_mult_distr, RPow_abs ; reflexivity. apply Rmult_le_compat_r ; [| apply HB ; exists k ; reflexivity]. apply pow_le ; unfold Rdiv ; apply Rle_mult_inv_pos ; [apply Rabs_pos | assumption]. apply Rle_trans with (Rabs (Rseq_sum (Rseq_shifts (gt_pser An x) k) n) + Rabs (Rseq_shifts (gt_pser An x) k (S n))). simpl ; apply Rabs_triang. apply Rle_trans with (B * Rseq_sum (Rseq_shifts (pow (Rabs x / r)) k) n + B * (Rseq_shifts (pow (Rabs x / r)) k) (S n)). apply Rplus_le_compat ; [apply IHn |]. apply Rle_trans with (gt_abs_pser An r (k + S n) * ((Rabs x / r) ^ (k + S n))). right ; unfold Rseq_shifts, gt_abs_pser, gt_pser, Rseq_mult, Rseq_abs. repeat rewrite Rabs_mult ; repeat rewrite Rmult_assoc ; apply Rmult_eq_compat_l ; rewrite <- Hrew_abs, RPow_abs, <- Rabs_mult ; apply Rabs_eq_compat ; unfold Rdiv ; rewrite Rpow_mult_distr, pow_inv ; field ; apply pow_nonzero ; symmetry ; assumption. apply Rmult_le_compat_r ; [| apply HB ; exists (k + S n)%nat ; reflexivity]. unfold Rseq_shifts, Rdiv ; apply pow_le ; apply Rle_mult_inv_pos ; [apply Rabs_pos | assumption]. right ; simpl ; symmetry ; apply Rmult_plus_distr_l. apply Temp. assert (Main : exists M : R, forall m n : nat, m <> n -> R_dist (Rseq_pps An x n) (Rseq_pps An x m) <= M * ((Rabs x / r) ^ (S (Nat.min m n)) * (1 - (Rabs x / r) ^ (S (Nat.max m n - S (Nat.min m n)))) / (1 - (Rabs x / r)))). destruct Hineq as [B HB] ; exists B ; intros m n m_neq_n. specialize (HB m n m_neq_n) ; unfold Rseq_shifts in HB ; rewrite sum_pow in HB ; [apply HB | apply Rlt_not_eq ; assumption]. clear Hineq Hrew. assert (Final : exists M : R, 0 < M /\ forall m n : nat, m <> n -> R_dist (Rseq_pps An x n) (Rseq_pps An x m) <= (Rabs x / r) ^ S (Nat.min m n) * (M * 2 / (1 - Rabs x / r))). destruct Main as [B HB] ; exists (Rmax B 1) ; split ; [apply Rlt_le_trans with 1 ; [lra | apply RmaxLess2] | intros m n m_neq_n]. assert (Temp : (1 - (Rabs x / r) ^ S (Nat.max m n - S (Nat.min m n))) <= 2). apply Rle_trans with (Rabs (1 - (Rabs x / r) ^ S (Nat.max m n - S (Nat.min m n)))) ; [apply RRle_abs |]. apply Rle_trans with (Rabs 1 + Rabs (- (Rabs x / r) ^ S (Nat.max m n - S (Nat.min m n)))) ; [apply Rabs_triang | rewrite Rabs_R1 ; apply Rplus_le_compat_l]. rewrite Rabs_Ropp ; rewrite <- RPow_abs ; rewrite <- Hrew_abs ; rewrite Rabs_Rabsolu ; replace R1 with (1 ^ S (Nat.max m n - S (Nat.min m n))) ; [apply pow_le_compat | apply pow1]. apply Rabs_pos. apply Rlt_le ; rewrite Hrew_abs ; assumption. apply Rle_trans with (B * ((Rabs x / r) ^ S (Nat.min m n) * (1 - (Rabs x / r) ^ S (Nat.max m n - S (Nat.min m n))) / (1 - Rabs x / r))) ; [apply HB ; assumption |]. clear HB ; rewrite Rmult_comm ; unfold Rdiv ; repeat (rewrite Rmult_assoc) ; apply Rmult_le_compat_l ; [ unfold Rdiv in Hrew_abs ; rewrite <- Hrew_abs ; rewrite RPow_abs ; apply Rabs_pos |]. apply Rle_trans with ((1 - (Rabs x * / r) ^ S (Nat.max m n - S (Nat.min m n))) * (/ (1 - Rabs x * / r) * (Rmax B 1))). apply Rmult_le_compat_l. unfold Rdiv in Hrew_abs ; rewrite <- Hrew_abs, RPow_abs. apply Rlt_le ; apply Rgt_minus. rewrite <- RPow_abs. case (Req_or_neq x) ; intro H. rewrite H ; rewrite Rmult_0_l ; rewrite Rabs_R0 ; rewrite pow_i ; intuition. replace 1 with (1 ^ S (Nat.max m n - S (Nat.min m n))). apply pow_lt_compat. apply Rabs_pos. unfold Rdiv in Rabsx_r_lt_1 ; rewrite Hrew_abs ; assumption. intuition (auto with arith). apply pow1. apply Rmult_le_compat_l. apply Rlt_le ; apply Rinv_0_lt_compat. apply Rgt_minus ; intuition. apply RmaxLess1. rewrite <- Rmult_assoc. rewrite Rmult_comm. apply Rmult_le_compat_l ; [apply Rle_trans with 1 ; [intuition (auto with real) | apply RmaxLess2] |]. apply Rmult_le_compat_r. apply Rlt_le ; apply Rinv_0_lt_compat. apply Rgt_minus ; intuition. assumption. elim Final ; intros M HM ; destruct HM as (M_pos, HM). rewrite <- Hrew_abs in Rabsx_r_lt_1. assert (y_pos : 0 < eps / (4 * M) * (1 - Rabs x / r)). apply Rmult_lt_0_compat. unfold Rdiv ; apply Rmult_lt_0_compat. assumption. apply Rinv_0_lt_compat ; lra. apply Rgt_minus ; rewrite <- Hrew_abs ; assumption. elim (pow_lt_1_zero (x/r) Rabsx_r_lt_1 (eps / (4 * M) * (1 - (Rabs x / r))) y_pos) ; intros N HN ; exists N ; intros n m n_lb m_lb. case (eq_nat_dec m n); intro s. rewrite s ; rewrite R_dist_eq ; assumption. apply Rle_lt_trans with ((Rabs x / r) ^ S (Nat.min m n) * (M * 2 / (1 - Rabs x / r))). apply HM ; intuition. assert (Temp : (S (Nat.min m n) >= N)%nat). destruct N. intuition (auto with arith). apply le_n_S. case (Nat.min_dec m n) ; intro H ; rewrite H ; apply Nat.le_trans with (S N) ; intuition. apply Rlt_trans with ((eps / (4 * M) * (1 - Rabs x / r)) * ((M * 2 / (1 - Rabs x / r)))). apply Rmult_lt_compat_r. apply Rmult_lt_0_compat. lra. apply Rinv_0_lt_compat. apply Rgt_minus ; rewrite <- Hrew_abs ; assumption. rewrite <- Hrew_abs ; rewrite RPow_abs ; rewrite Hrew_abs ; apply HN ; assumption. replace (eps / (4 * M) * (1 - Rabs x / r) * (M * 2 / (1 - Rabs x / r))) with (eps * (/2 * (/(2*M) * (2*M) * ((1 - Rabs x / r) / (1 - Rabs x / r))))). replace (/ (2 * M) * (2 * M)) with 1. rewrite Rmult_1_l ; unfold Rdiv ; rewrite Rinv_r. lra. apply Rgt_not_eq ; apply Rgt_minus ; unfold Rdiv in Hrew_abs ; rewrite <- Hrew_abs ; assumption. symmetry ; apply Rinv_l ; apply Rgt_not_eq ; lra. field ; split ; [|split]. apply Rgt_not_eq ; apply Rle_lt_trans with (Rabs x) ; [apply Rabs_pos | assumption]. apply Rgt_not_eq ; apply Rgt_minus ; assumption. apply Rgt_not_eq ; assumption. Qed.
imports: Reals Rsequence_def Rpser_def Rpser_def_simpl Rpser_base_facts Rsequence_facts Rsequence_sums_facts Rsequence_rewrite_facts Rpow_facts Lra PeanoNat MyRIneq MyNeq Rinterval RFsequence RFsequence_facts Tactics