Library Coq.Reals.Abstract.ConstructivePower

Require Import QArith Qabs.
Require Import ConstructiveReals.
Require Import ConstructiveRealsMorphisms.
Require Import ConstructiveAbs.
Require Import ConstructiveLimits.
Require Import ConstructiveSum.

Local Open Scope ConstructiveReals.

Fixpoint CRpow {R : ConstructiveReals} (r:CRcarrier R) (n:nat) : CRcarrier R :=
  match n with
    | O => 1
    | S n => r * (CRpow r n)
  end.

Lemma CRpow_ge_one : forall {R : ConstructiveReals} (x : CRcarrier R) (n : nat),
    1 <= x
    -> 1 <= CRpow x n.

Lemma CRpow_ge_zero : forall {R : ConstructiveReals} (x : CRcarrier R) (n : nat),
    0 <= x
    -> 0 <= CRpow x n.

Lemma CRpow_gt_zero : forall {R : ConstructiveReals} (x : CRcarrier R) (n : nat),
    0 < x
    -> 0 < CRpow x n.

Lemma CRpow_mult : forall {R : ConstructiveReals} (x y : CRcarrier R) (n:nat),
    CRpow x n * CRpow y n == CRpow (x*y) n.

Lemma CRpow_one : forall {R : ConstructiveReals} (n:nat),
    @CRpow R 1 n == 1.

Lemma CRpow_proper : forall {R : ConstructiveReals} (x y : CRcarrier R) (n : nat),
    x == y -> CRpow x n == CRpow y n.

Lemma CRpow_inv : forall {R : ConstructiveReals} (x : CRcarrier R) (xPos : 0 < x) (n : nat),
    CRpow (CRinv R x (inr xPos)) n
    == CRinv R (CRpow x n) (inr (CRpow_gt_zero x n xPos)).

Lemma CRpow_plus_distr : forall {R : ConstructiveReals} (x : CRcarrier R) (n p:nat),
    CRpow x n * CRpow x p == CRpow x (n+p).

Lemma CR_double : forall {R : ConstructiveReals} (x:CRcarrier R),
    CR_of_Q R 2 * x == x + x.

Lemma GeoCvZero : forall {R : ConstructiveReals},
    CR_cv R (fun n:nat => CRpow (CR_of_Q R (1#2)) n) 0.

Lemma GeoFiniteSum : forall {R : ConstructiveReals} (n:nat),
    CRsum (CRpow (CR_of_Q R (1#2))) n == CR_of_Q R 2 - CRpow (CR_of_Q R (1#2)) n.

Lemma GeoHalfBelowTwo : forall {R : ConstructiveReals} (n:nat),
    CRsum (CRpow (CR_of_Q R (1#2))) n < CR_of_Q R 2.

Lemma GeoHalfTwo : forall {R : ConstructiveReals},
    series_cv (fun n => CRpow (CR_of_Q R (1#2)) n) (CR_of_Q R 2).