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