proposition: Lemma GP_infinite : forall x:R, Rabs x < 1 -> Pser (fun n:nat => 1) x (/ (1 - x)).
proof: Proof. intros; unfold Pser; unfold infinite_sum; intros; elim (Req_dec x 0). - intros; exists 0%nat; intros; rewrite H1; rewrite Rminus_0_r; rewrite Rinv_1; cut (sum_f_R0 (fun n0:nat => 1 * 0 ^ n0) n = 1). + intros; rewrite H3; rewrite Rdist_eq; auto. + elim n; simpl. * ring. * intros; rewrite H3; ring. - intro; cut (0 < eps * (Rabs (1 - x) * Rabs (/ x))). + intro; elim (pow_lt_1_zero x H (eps * (Rabs (1 - x) * Rabs (/ x))) H2); intro N; intros; exists N; intros; cut (sum_f_R0 (fun n0:nat => 1 * x ^ n0) n = sum_f_R0 (fun n0:nat => x ^ n0) n). * intros; rewrite H5; apply (Rmult_lt_reg_l (Rabs (1 - x)) (Rdist (sum_f_R0 (fun n0:nat => x ^ n0) n) (/ (1 - x))) eps). -- apply Rabs_pos_lt. apply Rminus_eq_contra. apply Rlt_dichotomy_converse. right; unfold Rgt. apply (Rle_lt_trans x (Rabs x) 1). ++ apply RRle_abs. ++ assumption. -- unfold Rdist; rewrite <- Rabs_mult. rewrite Rmult_minus_distr_l. cut ((1 - x) * sum_f_R0 (fun n0:nat => x ^ n0) n = - (sum_f_R0 (fun n0:nat => x ^ n0) n * (x - 1))). ++ intro; rewrite H6. rewrite GP_finite. rewrite Rinv_r. ** assert (- (x ^ (n + 1) - 1) - 1 = - x ^ (n + 1)) by ring. rewrite H7. rewrite Rabs_Ropp; replace (n + 1)%nat with (S n) by ring. simpl; rewrite Rabs_mult; apply (Rlt_le_trans (Rabs x * Rabs (x ^ n)) (Rabs x * (eps * (Rabs (1 - x) * Rabs (/ x)))) (Rabs (1 - x) * eps)). { apply Rmult_lt_compat_l. - apply Rabs_pos_lt. assumption. - auto. } replace (Rabs x * (eps * (Rabs (1 - x) * Rabs (/ x)))) with (Rabs x * Rabs (/ x) * (eps * Rabs (1 - x))) by ring. rewrite <- Rabs_mult; rewrite Rinv_r. 2:assumption. rewrite Rabs_R1. replace (1 * (eps * Rabs (1 - x))) with (Rabs (1 - x) * eps) by ring. unfold Rle; right; reflexivity. ** apply Rminus_eq_contra. apply Rlt_dichotomy_converse. right; unfold Rgt. apply (Rle_lt_trans x (Rabs x) 1). { apply RRle_abs. } assumption. ++ ring. * elim n; simpl. -- ring. -- intros; rewrite H5. ring. + apply Rmult_lt_0_compat. * auto. * apply Rmult_lt_0_compat. -- apply Rabs_pos_lt. apply Rminus_eq_contra. apply Rlt_dichotomy_converse. right; unfold Rgt. apply (Rle_lt_trans x (Rabs x) 1). ++ apply RRle_abs. ++ assumption. -- apply Rabs_pos_lt. apply Rinv_neq_0_compat. assumption. Qed.
imports: Rbase Rfunctions Compare