proposition: Lemma GeometricCovergenceLemma : forall (n:positive) (e:Qpos), /(proj1_sig e*(1 - a)) <= inject_Z (Zpos n) -> a^Zpos n <= proj1_sig e.
proof: Proof. destruct (Qle_lt_or_eq _ _ Ha0) as [Ha0'|Ha0']. - intros n e H. assert (0 < a^Zpos n). { assert (X:0 < proj1_sig (Qpos_power (exist _ _ Ha0') (Zpos n))%Qpos) by auto with *. exact X. } apply Qmult_lt_0_le_reg_r with ((/proj1_sig e)*/(a^Zpos n)). apply (Qle_lt_trans _ (0 * (/a^Zpos n))). rewrite Qmult_0_l. apply Qle_refl. apply Qmult_lt_r. apply Qinv_lt_0_compat; exact H0. apply Qinv_lt_0_compat, Qpos_ispos. assert (0 < proj1_sig e) by (apply Qpos_ispos). rewrite (Qmult_assoc (proj1_sig e)), Qmult_inv_r, Qmult_1_l. 2: apply Qpos_nonzero. setoid_replace (a ^ Zpos n * (/ proj1_sig e * / a ^ Zpos n)) with (/proj1_sig e) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; field). 2: split. 2: apply Qpos_nonzero. 2: auto with *. rewrite -> Qlt_minus_iff in Ha1. change (0<1-a) in Ha1. rewrite -> Qle_minus_iff in H. apply Qle_trans with (1 + inject_Z (Zpos n) * (/a -1)). + rewrite -> Qle_minus_iff. setoid_replace (1 + inject_Z (Zpos n) * (/ a - 1) + - / proj1_sig e) with (1+(1 - a)*((inject_Z (Zpos n)*(1-a)*/a + (inject_Z (Zpos n) +-(/(proj1_sig e*(1 - a))))))) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; field). 2: split; auto with *. apply (Qle_trans _ (1+0)). discriminate. apply Qplus_le_r. repeat apply Qmult_le_0_compat; simpl; auto with *. assert (0 <= 1-a) by auto with *. apply (Qle_trans _ (0+0)). discriminate. apply Qplus_le_compat. 2: exact H. apply Qmult_le_0_compat. apply Qmult_le_0_compat. discriminate. exact H2. apply Qlt_le_weak, Qinv_lt_0_compat, Ha0'. + clear -n Ha0'. induction n using Pind. simpl. setoid_replace (1 + inject_Z 1 * (/ a - 1)) with (/a) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). apply Qle_refl. rewrite Zpos_succ_morphism. unfold Z.succ. rewrite -> Qpower_plus;[|auto with *]. rewrite -> Qinv_mult_distr. rewrite -> Q.Zplus_Qplus. apply Qle_trans with ((1 + inject_Z (Zpos n) * (/ a - 1))*/a). rewrite -> Qle_minus_iff. setoid_replace ( (1 + inject_Z (Z.pos n) * (/ a - 1)) * / a + - (1 + (inject_Z (Z.pos n) + inject_Z 1) * (/ a - 1))) with (inject_Z (Zpos n)*(/a -1)^2) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). apply Qmult_le_0_compat. discriminate. unfold Qle. rewrite Z.mul_0_l. simpl. rewrite Z.mul_1_r. apply Z.square_nonneg. apply Qmult_le_compat_r. assumption. apply Qinv_le_0_compat; auto with *. - intros n e _. rewrite <- Ha0'. rewrite -> Qpower_0; auto with *. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRstreams CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax Coq.QArith.Qpower Coq.QArith.Qabs Coq.ZArith.Zdiv