proposition: Lemma geometric_sum : forall (k:R), Rabs k < 1 -> infinite_sum (fun i:nat => k ^ i) (1 / (1 - k)).
proof: Proof. intros k H0k1. intros eps Heps. assert (Hpos : 0 < eps * (1 - k)). apply Rmult_lt_0_compat ; [apply Heps |]. unfold Rabs in *. destruct (Rcase_abs k) ; lra. destruct (pow_lt_1_zero k H0k1 (eps * (1 - k)) Hpos) as (N, HN). exists N. intros n Hn. rewrite tech3. unfold R_dist, Rdiv. field_simplify ((1 - k ^ S n) * / (1 - k) - 1 * / (1 - k)). rewrite Rabs_div. rewrite Rabs_Ropp. unfold Rabs. destruct (Rcase_abs (-k + 1)) as [H|[H|H]]. assert (H1 : (N >= N)%nat) by intuition. generalize (HN N H1). intros. assert (eps * (1 - k) < 0). replace 0 with (eps * 0) by intuition. apply Rmult_lt_compat_l. apply Heps. lra. lra. replace eps with (eps * (1 - k) * / (-k + 1)). unfold Rdiv. apply Rmult_lt_compat_r. apply Rinv_0_lt_compat. lra. apply HN. intuition. field. intros H3. lra. unfold Rabs in H0k1 ; destruct (Rcase_abs k) ; lra. intro H2. unfold Rabs in H0k1 ; destruct (Rcase_abs k) ; lra. intro H2. unfold Rabs in H0k1 ; destruct (Rcase_abs k) ; lra. intro H2. unfold Rabs in H0k1 ; destruct (Rcase_abs k) ; lra. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Rsequence_subsequence Rpser_usual Reals Rsequence_tactics Rtactic Lra