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.

Definition and properties of powers.
WARNING: this file is experimental and likely to change in future releases.

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).