proposition: Lemma GeoHalfTwo : forall {R : ConstructiveReals}, series_cv (fun n => CRpow (CR_of_Q R (1#2)) n) (CR_of_Q R 2).
proof: Proof. intro R. apply (CR_cv_eq _ (fun n => CR_of_Q R 2 - CRpow (CR_of_Q R (1 # 2)) n)). - intro n. rewrite GeoFiniteSum. reflexivity. - assert (forall n:nat, INR n < CRpow (CR_of_Q R 2) n). { induction n. - unfold INR; simpl. apply CRzero_lt_one. - apply (CRlt_le_trans _ (CRpow (CR_of_Q R 2) n + 1)). + unfold INR. rewrite Nat2Z.inj_succ, <- Z.add_1_l. rewrite (CR_of_Q_morph R _ (1 + (Z.of_nat n #1))). 2: symmetry; apply Qinv_plus_distr. rewrite CR_of_Q_plus. rewrite CRplus_comm. apply CRplus_lt_compat_r, IHn. + setoid_replace (CRpow (CR_of_Q R 2) (S n)) with (CRpow (CR_of_Q R 2) n + CRpow (CR_of_Q R 2) n). * apply CRplus_le_compat. -- apply CRle_refl. -- apply CRpow_ge_one. apply CR_of_Q_le. discriminate. * rewrite <- CR_double. reflexivity. } intros n. exists (Pos.to_nat n). intros. setoid_replace (CR_of_Q R 2 - CRpow (CR_of_Q R (1 # 2)) i - CR_of_Q R 2) with (- CRpow (CR_of_Q R (1 # 2)) i). + rewrite CRabs_opp. rewrite CRabs_right. * assert (0 < CR_of_Q R 2). { apply CR_of_Q_lt. reflexivity. } rewrite (CRpow_proper _ (CRinv R (CR_of_Q R 2) (inr H1))). -- rewrite CRpow_inv. apply CRlt_asym. apply (CRmult_lt_reg_l (CRpow (CR_of_Q R 2) i)). ++ apply CRpow_gt_zero, H1. ++ rewrite CRinv_r. apply (CRmult_lt_reg_r (CR_of_Q R (Z.pos n#1))). ** apply CR_of_Q_lt. reflexivity. ** rewrite CRmult_1_l, CRmult_assoc. rewrite <- CR_of_Q_mult. rewrite (CR_of_Q_morph R ((1 # n) * (Z.pos n # 1)) 1). 2: reflexivity. rewrite CRmult_1_r. apply (CRle_lt_trans _ (INR i)). 2: apply H. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. destruct i. { exfalso. inversion H0. pose proof (Pos2Nat.is_pos n). rewrite H3 in H2. inversion H2. } apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. apply (Nat.le_trans _ _ _ H0). rewrite SuccNat2Pos.id_succ. apply Nat.le_refl. -- apply (CRmult_eq_reg_l (CR_of_Q R 2)). ++ right. exact H1. ++ rewrite CRinv_r. rewrite <- CR_of_Q_mult. setoid_replace (2 * (1 # 2))%Q with 1%Q. ** reflexivity. ** reflexivity. * apply CRlt_asym, CRpow_gt_zero. apply CR_of_Q_lt. reflexivity. + unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_l. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits ConstructiveSum