proposition: Lemma sum_pow_explicit : forall x, Rabs x < 1 -> sum_pow x = / (1 - x).
proof: Proof. intros x x_in ; eapply Rpser_unique. eapply sum_r_sums ; assumption. apply Rseq_cv_eq_compat with (Vn := fun n => (1 - Rseq_shift (Rseq_pow x) n) / (1 - x)). intro n ; unfold Rseq_shift, Rseq_pow ; rewrite <- partial_sum_pow_explicit ; field. apply Rminus_eq_contra ; intro Hf ; apply (Rlt_irrefl 1) ; rewrite <- Hf, Rabs_R1 in x_in ; assumption. rewrite <- Rmult_1_l ; apply Rseq_cv_mult_compat, Rseq_constant_cv. rewrite <- Rminus_0_r ; apply Rseq_cv_minus_compat. apply Rseq_constant_cv. apply Rseq_cv_shift_compat_reciprocal, Rseq_pow_lt_1_cv_strong ; assumption. Qed.
imports: MyReals MyINR MyNNR Rsequence_def Rsequence_facts Rsequence_cv_facts Rsequence_sums_facts Rsequence_base_facts Rsequence_rewrite_facts Rsequence_usual_facts Rsequence_subsequence PeanoNat Lra Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_cv_facts Rpser_radius_facts Rpser_sums Rpser_derivative Rpser_derivative_facts Rfunction_def Functions Rextensionality Rpow_facts Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity