Library Coq.Reals.Rprod
Require
Import
Compare
.
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
Rseries
.
Require
Import
PartSum
.
Require
Import
Binomial
.
Local
Open
Scope
R_scope
.
TT Ak; 0<=k<=N
Fixpoint
prod_f_R0
(
f
:
nat
->
R
) (
N
:
nat
) :
R
:=
match
N
with
|
O
=>
f
O
|
S
p
=>
prod_f_R0
f
p
*
f
(
S
p
)
end
.
Notation
prod_f_SO
:= (
fun
An
N
=>
prod_f_R0
(
fun
n
=>
An
(
S
n
))
N
).
Lemma
prod_SO_split
:
forall
(
An
:
nat
->
R
) (
n
k
:
nat
),
(
k
<
n
)%
nat
->
prod_f_R0
An
n
=
prod_f_R0
An
k
*
prod_f_R0
(
fun
l
:
nat
=>
An
(
k
+
1
+
l
)%
nat
) (
n
-
k
-
1).
Lemma
prod_SO_pos
:
forall
(
An
:
nat
->
R
) (
N
:
nat
),
(
forall
n
:
nat
, (
n
<=
N
)%
nat
-> 0
<=
An
n
) -> 0
<=
prod_f_R0
An
N
.
Lemma
prod_SO_Rle
:
forall
(
An
Bn
:
nat
->
R
) (
N
:
nat
),
(
forall
n
:
nat
, (
n
<=
N
)%
nat
-> 0
<=
An
n
<=
Bn
n
) ->
prod_f_R0
An
N
<=
prod_f_R0
Bn
N
.
Application to factorial
Lemma
fact_prodSO
:
forall
n
:
nat
,
INR
(
fact
n
)
=
prod_f_R0
(
fun
k
:
nat
=>
(
match
(
eq_nat_dec
k
0)
with
|
left
_
=> 1%
R
|
right
_
=>
INR
k
end
))
n
.
Lemma
le_n_2n
:
forall
n
:
nat
, (
n
<=
2
*
n
)%
nat
.
We prove that (N!)^2<=(2N-k)!*k! forall k in
|
O
;2
N
|
Lemma
RfactN_fact2N_factk
:
forall
N
k
:
nat
,
(
k
<=
2
*
N
)%
nat
->
Rsqr
(
INR
(
fact
N
))
<=
INR
(
fact
(2
*
N
-
k
))
*
INR
(
fact
k
).
Lemma
INR_fact_lt_0
:
forall
n
:
nat
, 0
<
INR
(
fact
n
).
We have the following inequality : (C 2N k) <= (C 2N N) forall k in
|
O
;2
N
|
Lemma
C_maj
:
forall
N
k
:
nat
, (
k
<=
2
*
N
)%
nat
->
C
(2
*
N
)
k
<=
C
(2
*
N
)
N
.