Library Coq.Reals.ConstructiveCauchyRealsMult
Require Import QArith.
Require Import Qabs.
Require Import Qround.
Require Import Logic.ConstructiveEpsilon.
Require Export Reals.ConstructiveCauchyReals.
Require CMorphisms.
Local Open Scope CReal_scope.
Fixpoint BoundFromZero (
qn :
nat -> Q) (
k :
nat) (
A :
positive) {
struct k }
:
(forall n:
nat,
le k n -> Qlt (
Qabs (
qn n)) (
Z.pos A # 1)
)
-> { B : positive | forall n:
nat,
Qlt (
Qabs (
qn n)) (
Z.pos B # 1)
}.
Lemma QCauchySeq_bounded (
qn :
nat -> Q) (
cvmod :
positive -> nat)
:
QCauchySeq qn cvmod
-> { A : positive | forall n:
nat,
Qlt (
Qabs (
qn n)) (
Z.pos A # 1)
}.
Lemma CReal_mult_cauchy
:
forall (
xn yn zn :
nat -> Q) (
Ay Az :
positive) (
cvmod :
positive -> nat),
QSeqEquiv xn yn cvmod
-> QCauchySeq zn Pos.to_nat
-> (forall n:
nat,
Qlt (
Qabs (
yn n)) (
Z.pos Ay # 1)
)
-> (forall n:
nat,
Qlt (
Qabs (
zn n)) (
Z.pos Az # 1)
)
-> QSeqEquiv (
fun n:
nat =>
xn n * zn n) (
fun n:
nat =>
yn n * zn n)
(
fun p =>
max (
cvmod (2
* (Pos.max Ay Az) * p)%
positive)
(
Pos.to_nat (2
* (Pos.max Ay Az) * p)%
positive)).
Lemma linear_max :
forall (
p Ax Ay :
positive) (
i :
nat),
le (
Pos.to_nat p)
i
-> (
Init.Nat.max (
Pos.to_nat (2
* Pos.max Ax Ay * p))
(
Pos.to_nat (2
* Pos.max Ax Ay * p))
<= Pos.to_nat (2
* Pos.max Ax Ay)
* i)%
nat.
Definition CReal_mult (
x y :
CReal) :
CReal.
Infix "*" :=
CReal_mult :
CReal_scope.
Lemma CReal_mult_unfold :
forall x y :
CReal,
QSeqEquivEx (
proj1_sig (
CReal_mult x y))
(
fun n :
nat =>
proj1_sig x n * proj1_sig y n)%
Q.
Lemma CReal_mult_assoc_bounded_r :
forall (
xn yn zn :
nat -> Q),
QSeqEquivEx xn yn
-> QSeqEquiv zn zn Pos.to_nat
-> QSeqEquivEx (
fun n =>
xn n * zn n)%
Q (
fun n =>
yn n * zn n)%
Q.
Lemma CReal_mult_assoc :
forall x y z :
CReal,
CRealEq (
CReal_mult (
CReal_mult x y)
z)
(
CReal_mult x (
CReal_mult y z)).
Lemma CReal_mult_comm :
forall x y :
CReal,
CRealEq (
CReal_mult x y) (
CReal_mult y x).
Lemma CReal_mult_proper_l :
forall x y z :
CReal,
CRealEq y z -> CRealEq (
CReal_mult x y) (
CReal_mult x z).
Lemma CReal_mult_lt_0_compat :
forall x y :
CReal,
CRealLt (
inject_Q 0)
x
-> CRealLt (
inject_Q 0)
y
-> CRealLt (
inject_Q 0) (
CReal_mult x y).
Lemma CReal_mult_plus_distr_l :
forall r1 r2 r3 :
CReal,
r1 * (r2 + r3) == (r1 * r2) + (r1 * r3).
Lemma CReal_mult_plus_distr_r :
forall r1 r2 r3 :
CReal,
(r2 + r3) * r1 == (r2 * r1) + (r3 * r1).
Lemma CReal_mult_1_l :
forall r:
CReal, 1
* r == r.
Lemma CReal_isRingExt :
ring_eq_ext CReal_plus CReal_mult CReal_opp CRealEq.
Lemma CReal_isRing :
ring_theory (
inject_Q 0) (
inject_Q 1)
CReal_plus CReal_mult
CReal_minus CReal_opp
CRealEq.
Add Parametric Morphism :
CReal_mult
with signature CRealEq ==> CRealEq ==> CRealEq
as CReal_mult_morph.
Instance CReal_mult_morph_T
:
CMorphisms.Proper
(
CMorphisms.respectful CRealEq (
CMorphisms.respectful CRealEq CRealEq))
CReal_mult.
Add Parametric Morphism :
CReal_opp
with signature CRealEq ==> CRealEq
as CReal_opp_morph.
Instance CReal_opp_morph_T
:
CMorphisms.Proper
(
CMorphisms.respectful CRealEq CRealEq)
CReal_opp.
Add Parametric Morphism :
CReal_minus
with signature CRealEq ==> CRealEq ==> CRealEq
as CReal_minus_morph.
Instance CReal_minus_morph_T
:
CMorphisms.Proper
(
CMorphisms.respectful CRealEq (
CMorphisms.respectful CRealEq CRealEq))
CReal_minus.
Add Ring CRealRing :
CReal_isRing.
Lemma CReal_mult_0_l :
forall r, 0
* r == 0.
Lemma CReal_mult_0_r :
forall r,
r * 0
== 0.
Lemma CReal_mult_1_r :
forall r,
r * 1
== r.
Lemma CReal_opp_mult_distr_l
:
forall r1 r2 :
CReal,
- (r1 * r2) == (- r1) * r2.
Lemma CReal_opp_mult_distr_r
:
forall r1 r2 :
CReal,
- (r1 * r2) == r1 * (- r2).
Lemma CReal_mult_lt_compat_l :
forall x y z :
CReal,
0
< x -> y < z -> x*y < x*z.
Lemma CReal_mult_lt_compat_r :
forall x y z :
CReal,
0
< x -> y < z -> y*x < z*x.
Lemma CReal_mult_eq_reg_l :
forall (
r r1 r2 :
CReal),
r # 0
-> CRealEq (
CReal_mult r r1) (
CReal_mult r r2)
-> CRealEq r1 r2.
Lemma CReal_abs_appart_zero :
forall (
x :
CReal) (
n :
positive),
Qlt (2
#n) (
Qabs (
proj1_sig x (
Pos.to_nat n)))
-> 0
# x.
Lemma CRealArchimedean
:
forall x:
CReal,
{ n:Z & x < inject_Q (
n#1)
< x+2
}.
Definition Rup_pos (
x :
CReal)
:
{ n : positive & x < inject_Q (
Z.pos n # 1)
}.
Lemma CRealLtDisjunctEpsilon :
forall a b c d :
CReal,
(CRealLtProp a b \/ CRealLtProp c d) -> CRealLt a b + CRealLt c d.
Lemma CRealShiftReal :
forall (
x :
CReal) (
k :
nat),
QCauchySeq (
fun n =>
proj1_sig x (
plus n k))
Pos.to_nat.
Lemma CRealShiftEqual :
forall (
x :
CReal) (
k :
nat),
CRealEq x (
exist _ (
fun n =>
proj1_sig x (
plus n k)) (
CRealShiftReal x k)).
Definition CRealNegShift (
x :
CReal)
:
CRealLt x (
inject_Q 0)
-> { y : prod positive CReal | CRealEq x (
snd y)
/\ forall n:
nat,
Qlt (
proj1_sig (
snd y)
n) (-1
# fst y)
}.
Definition CRealPosShift (
x :
CReal)
:
inject_Q 0
< x
-> { y : prod positive CReal | CRealEq x (
snd y)
/\ forall n:
nat,
Qlt (1
# fst y) (
proj1_sig (
snd y)
n)
}.
Lemma CReal_inv_neg :
forall (
yn :
nat -> Q) (
k :
positive),
(QCauchySeq yn Pos.to_nat)
-> (
forall n :
nat,
yn n < -1
# k)%
Q
-> QCauchySeq (
fun n :
nat =>
/ yn (
Pos.to_nat k ^ 2
* n)%
nat)
Pos.to_nat.
Lemma CReal_inv_pos :
forall (
yn :
nat -> Q) (
k :
positive),
(QCauchySeq yn Pos.to_nat)
-> (
forall n :
nat, 1
# k < yn n)%
Q
-> QCauchySeq (
fun n :
nat =>
/ yn (
Pos.to_nat k ^ 2
* n)%
nat)
Pos.to_nat.
Definition CReal_inv (
x :
CReal) (
xnz :
x # 0) :
CReal.
Notation "/ x" := (
CReal_inv x) (
at level 35,
right associativity) :
CReal_scope.
Lemma CReal_inv_0_lt_compat
:
forall (
r :
CReal) (
rnz :
r # 0),
0
< r -> 0
< ((
/ r)
rnz).
Lemma CReal_linear_shift :
forall (
x :
CReal) (
k :
nat),
le 1
k -> QCauchySeq (
fun n =>
proj1_sig x (
k * n)%
nat)
Pos.to_nat.
Lemma CReal_linear_shift_eq :
forall (
x :
CReal) (
k :
nat) (
kPos :
le 1
k),
CRealEq x
(
exist (
fun n :
nat -> Q =>
QCauchySeq n Pos.to_nat)
(
fun n :
nat =>
proj1_sig x (
k * n)%
nat) (
CReal_linear_shift x k kPos)).
Lemma CReal_inv_l :
forall (
r:
CReal) (
rnz :
r # 0),
((
/ r)
rnz) * r == 1.
Lemma CReal_inv_r :
forall (
r:
CReal) (
rnz :
r # 0),
r * ((
/ r)
rnz) == 1.
Lemma CReal_inv_1 :
forall nz : 1
# 0, (
/ 1)
nz == 1.
Lemma CReal_inv_mult_distr :
forall r1 r2 (
r1nz :
r1 # 0) (
r2nz :
r2 # 0) (
rmnz :
(r1*r2) # 0),
(
/ (r1 * r2))
rmnz == (
/ r1)
r1nz * (
/ r2)
r2nz.
Lemma Rinv_eq_compat :
forall x y (
rxnz :
x # 0) (
rynz :
y # 0),
x == y
-> (
/ x)
rxnz == (
/ y)
rynz.
Lemma CReal_mult_lt_reg_l :
forall r r1 r2, 0
< r -> r * r1 < r * r2 -> r1 < r2.
Lemma CReal_mult_lt_reg_r :
forall r r1 r2, 0
< r -> r1 * r < r2 * r -> r1 < r2.
Lemma CReal_mult_eq_reg_r :
forall r r1 r2,
r1 * r == r2 * r -> r # 0
-> r1 == r2.
Lemma CReal_mult_eq_compat_l :
forall r r1 r2,
r1 == r2 -> r * r1 == r * r2.
Lemma CReal_mult_eq_compat_r :
forall r r1 r2,
r1 == r2 -> r1 * r == r2 * r.
Lemma CReal_mult_pos_appart_zero :
forall x y :
CReal, 0
< x * y -> 0
# x.
Fixpoint pow (
r:
CReal) (
n:
nat) :
CReal :=
match n with
|
O => 1
|
S n =>
r * (pow r n)
end.
Lemma CReal_mult_le_compat_l_half :
forall r r1 r2,
0
< r -> r1 <= r2 -> r * r1 <= r * r2.
Lemma CReal_invQ :
forall (
b :
positive) (
pos :
Qlt 0 (
Z.pos b # 1)),
CRealEq (
CReal_inv (
inject_Q (
Z.pos b # 1)) (
inr (
CReal_injectQPos (
Z.pos b # 1)
pos)))
(
inject_Q (1
# b)).
Definition CRealQ_dense (
a b :
CReal)
:
a < b -> { q : Q & a < inject_Q q < b }.
Lemma inject_Q_mult :
forall q r :
Q,
inject_Q (
q * r)
== inject_Q q * inject_Q r.