Module FormalML.CertRL.LM.R_compl
Require
Export
Reals
Coquelicot.Coquelicot
.
Open
Scope
R_scope
.
Section
RC
.
If a degree-2 polynomial is always nonnegative, its dicriminant is nonpositive
Lemma
discr_neg
:
forall
a
b
c
,
(
forall
x
, 0 <=
a
*
x
*
x
+
b
*
x
+
c
) ->
b
*
b
-4*
a
*
c
<= 0.
intros
.
case
(
Req_dec
a
0);
intros
H
'.
cut
(
b
=0).
intros
H1
;
rewrite
H
';
rewrite
H1
.
right
;
ring
.
case
(
Req_dec
b
0);
trivial
;
intros
.
absurd
(0 <=
a
*((-
c
-1)/
b
)*((-
c
-1)/
b
)+
b
*((-
c
-1)/
b
)+
c
).
2:
apply
H
.
apply
Rlt_not_le
.
rewrite
H
';
apply
Rle_lt_trans
with
(-1).
right
;
field
;
trivial
.
apply
Ropp_lt_gt_0_contravar
;
apply
Rlt_gt
;
auto
with
real
.
assert
(0 <=
c
).
apply
Rle_trans
with
(
a
*0*0+
b
*0+
c
);[
idtac
|
right
;
ring
].
apply
H
.
assert
(0 <
a
).
cut
(0 <=
a
).
intros
T
;
case
T
;
auto
with
real
.
intros
T
';
absurd
(
a
=0);
auto
.
case
(
Req_dec
b
0);
intros
.
case
(
Rle_or_lt
0
a
);
trivial
;
intros
.
absurd
(0 <=
a
*
sqrt
((
c
+1)/(-
a
)) *
sqrt
((
c
+1)/(-
a
)) +
b
*
sqrt
((
c
+1)/(-
a
))+
c
).
2:
apply
H
.
apply
Rlt_not_le
.
rewrite
H1
;
ring_simplify
( 0 *
sqrt
((
c
+ 1) / -
a
)).
rewrite
Rmult_assoc
.
rewrite
sqrt_sqrt
.
apply
Rle_lt_trans
with
(-1).
right
;
field
;
auto
with
real
.
apply
Ropp_lt_gt_0_contravar
;
apply
Rlt_gt
;
auto
with
real
.
unfold
Rdiv
;
apply
Rmult_le_pos
;
auto
with
real
.
case
H0
;
intros
.
apply
Rmult_le_reg_l
with
(
c
*
c
/(
b
*
b
)).
unfold
Rdiv
;
apply
Rmult_lt_0_compat
.
apply
Rmult_lt_0_compat
;
trivial
.
apply
Rinv_0_lt_compat
.
fold
(
Rsqr
b
);
auto
with
real
.
ring_simplify
.
apply
Rle_trans
with
(
a
*(-
c
/
b
)*(-
c
/
b
)+
b
*(-
c
/
b
)+
c
).
apply
H
.
right
;
field
;
trivial
.
apply
Rmult_le_reg_l
with
(
b
*
b
).
fold
(
Rsqr
b
);
auto
with
real
.
ring_simplify
.
apply
Rle_trans
with
(
Rsqr
b
);
auto
with
real
.
apply
Rplus_le_reg_l
with
(-
Rsqr
b
);
ring_simplify
.
apply
Rle_trans
with
(
a
*(-
b
)*(-
b
)+
b
*(-
b
)+
c
).
apply
H
.
rewrite
<-
H2
;
unfold
Rsqr
;
right
;
ring
.
case
(
Rle_or_lt
(
b
*
b
- 4 *
a
*
c
) 0);
trivial
.
intros
H2
.
absurd
( 0 <=
a
* (-
b
/(2*
a
)) * (-
b
/(2*
a
)) +
b
* (-
b
/(2*
a
)) +
c
).
apply
Rlt_not_le
.
replace
(
a
* (-
b
/ (2*
a
)) * (-
b
/ (2*
a
)) +
b
* (-
b
/ (2*
a
)) +
c
)
with
(-
b
*
b
/(4*
a
)+
c
).
apply
Rmult_lt_reg_l
with
(4*
a
).
repeat
apply
Rmult_lt_0_compat
;
auto
with
real
.
apply
Rplus_lt_reg_r
with
(
b
*
b
-4*
a
*
c
).
apply
Rle_lt_trans
with
0%
R
.
right
;
field
;
auto
.
apply
Rlt_le_trans
with
(1:=
H2
);
right
;
ring
.
field
;
auto
.
apply
H
.
Qed.
Lemma
contraction_lt_any
:
forall
k
d
, 0 <=
k
< 1 -> 0 <
d
->
exists
N
,
pow
k
N
<
d
.
Proof.
intros
k
d
Hk
Hd
.
case
(
proj1
Hk
);
intros
Hk
'.
(* 0 < k *)
assert
(
ln
k
< 0).
rewrite
<-
ln_1
.
apply
ln_increasing
;
try
apply
Hk
;
assumption
.
exists
(
Z.abs_nat
(
up
(
ln
d
/
ln
k
))).
apply
ln_lt_inv
;
try
assumption
.
now
apply
pow_lt
.
rewrite
<-
Rpower_pow
;
trivial
.
unfold
Rpower
.
rewrite
ln_exp
.
apply
Rmult_lt_reg_l
with
(- /
ln
k
).
apply
Ropp_gt_lt_0_contravar
.
now
apply
Rinv_lt_0_compat
.
apply
Rle_lt_trans
with
(-(
INR
(
Z.abs_nat
(
up
(
ln
d
/
ln
k
))))).
right
;
field
.
now
apply
Rlt_not_eq
.
rewrite
Ropp_mult_distr_l_reverse
.
apply
Ropp_lt_contravar
.
generalize
(
archimed
(
ln
d
/
ln
k
));
intros
(
Y1
,
_
).
rewrite
Rmult_comm
.
apply
Rlt_le_trans
with
(1:=
Y1
).
generalize
(
up
(
ln
d
/
ln
k
));
clear
;
intros
x
.
rewrite
INR_IZR_INZ
,
Zabs2Nat.id_abs
.
apply
IZR_le
.
case
(
Zabs_spec
x
);
intros
(
T1
,
T2
);
rewrite
T2
;
auto
with
zarith
.
(* k = 0 *)
exists
1%
nat
.
rewrite
<-
Hk
';
simpl
.
now
rewrite
Rmult_0_l
.
Qed.
Lemma
contraction_lt_any
':
forall
k
d
, 0 <=
k
< 1 -> 0 <
d
->
exists
N
, (0 <
N
)%
nat
/\
pow
k
N
<
d
.
Proof.
intros
k
d
H1
H2
.
destruct
(
contraction_lt_any
k
d
H1
H2
)
as
(
N
,
HN
).
case_eq
N
.
intros
H3
;
exists
1%
nat
;
split
.
now
apply
le_n
.
rewrite
H3
in
HN
;
simpl
in
HN
.
simpl
;
rewrite
Rmult_1_r
.
now
apply
Rlt_trans
with
1.
intros
m
Hm
.
exists
N
;
split
;
try
assumption
.
rewrite
Hm
.
now
auto
with
arith
.
Qed.
Lemma
Rinv_le_cancel
:
forall
x
y
:
R
, 0 <
y
-> /
y
<= /
x
->
x
<=
y
.
Proof.
intros
x
y
H1
H2
.
case
(
Req_dec
x
0);
intros
Hx
.
rewrite
Hx
;
now
left
.
destruct
H2
.
left
;
now
apply
Rinv_lt_cancel
.
right
;
rewrite
<-
Rinv_involutive
.
2:
now
apply
Rgt_not_eq
.
rewrite
H
.
now
apply
sym_eq
,
Rinv_involutive
.
Qed.
Lemma
Rlt_R1_pow
:
forall
x
n
, 0 <=
x
< 1 -> (0 <
n
)%
nat
->
x
^
n
< 1.
Proof.
intros
x
n
(
Hx1
,
Hx2
)
Hn
.
case
(
Req_dec
x
0);
intros
H
'.
rewrite
H
',
pow_i
;
try
assumption
.
apply
Rlt_0_1
.
apply
Rinv_lt_cancel
.
apply
Rlt_0_1
.
rewrite
Rinv_1
.
rewrite
Rinv_pow
;
try
assumption
.
apply
Rlt_pow_R1
;
try
assumption
.
rewrite
<-
Rinv_1
.
apply
Rinv_lt_contravar
;
try
assumption
.
rewrite
Rmult_1_r
.
destruct
Hx1
;
trivial
.
contradict
H
;
now
apply
not_eq_sym
.
Qed.
Lemma
Rle_pow_le
:
forall
(
x
:
R
) (
m
n
:
nat
), 0 <
x
<= 1 -> (
m
<=
n
)%
nat
->
x
^
n
<=
x
^
m
.
Proof.
intros
x
m
n
(
Hx1
,
Hx2
)
H
.
apply
Rinv_le_cancel
.
now
apply
pow_lt
.
rewrite
2!
Rinv_pow
;
try
now
apply
Rgt_not_eq
.
apply
Rle_pow
;
try
assumption
.
rewrite
<-
Rinv_1
.
apply
Rinv_le_contravar
;
try
assumption
.
Qed.
Lemma
is_finite_betw
:
forall
x
y
z
,
Rbar_le
(
Finite
x
)
y
->
Rbar_le
y
(
Finite
z
) ->
is_finite
y
.
Proof.
intros
x
y
z
;
destruct
y
;
easy
.
Qed.
Lemma
Rplus_plus_reg_l
:
forall
(
a
b
c
:
R
),
b
=
c
->
plus
a
b
=
a
+
c
.
Proof.
intros
.
rewrite
H
.
reflexivity
.
Qed.
Lemma
Rplus_plus_reg_r
:
forall
a
b
c
,
b
=
c
->
plus
b
a
=
c
+
a
.
Proof.
intros
.
rewrite
H
.
reflexivity
.
Qed.
Context
{
E
:
NormedModule
R_AbsRing
}.
Lemma
norm_scal_R
:
forall
l
(
x
:
E
),
norm
(
scal
l
x
) =
abs
l
*
norm
x
.
Proof.
intros
l
x
.
apply
Rle_antisym
;
try
apply
norm_scal
.
case
(
Req_dec
l
0);
intros
V
.
rewrite
V
;
unfold
abs
;
simpl
.
rewrite
Rabs_R0
,
Rmult_0_l
.
apply
norm_ge_0
.
apply
Rmult_le_reg_l
with
(
abs
(/
l
)).
unfold
abs
;
simpl
.
apply
Rabs_pos_lt
.
now
apply
Rinv_neq_0_compat
.
apply
Rle_trans
with
(
norm
x
).
rewrite
<-
Rmult_assoc
.
unfold
abs
;
simpl
.
rewrite
<-
Rabs_mult
.
rewrite
Rinv_l
;
trivial
.
rewrite
Rabs_R1
,
Rmult_1_l
.
apply
Rle_refl
.
apply
Rle_trans
with
(
norm
(
scal
(/
l
) (
scal
l
x
))).
right
;
apply
f_equal
.
rewrite
scal_assoc
.
apply
trans_eq
with
(
scal
one
x
).
apply
sym_eq
,
scal_one
.
apply
f_equal2
;
trivial
.
unfold
one
,
mult
;
simpl
.
now
field
.
apply
(
norm_scal
(/
l
) (
scal
l
x
)).
Qed.
Lemma
sum_n_eq_zero
:
forall
m
(
L
:
nat
->
E
),
(
forall
i
, (
i
<=
m
)%
nat
->
L
i
=
zero
) ->
sum_n
L
m
=
zero
.
Proof.
intros
m
L
H
.
apply
trans_eq
with
(
sum_n
(
fun
n
=>
zero
)
m
).
now
apply
sum_n_ext_loc
.
clear
;
induction
m
.
now
rewrite
sum_O
.
rewrite
sum_Sn
,
IHm
.
apply
plus_zero_l
.
Qed.
End
RC
.