1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: Rprod.v 9298 2006-10-27 13:05:29Z notin $ i*)
Require Import Compare.
Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
Require Import PartSum.
Require Import Binomial.
Open Local Scope R_scope.
(** TT Ak; 1<=k<=N *)
Boxed Fixpoint prod_f_SO (An:nat -> R) (N:nat) {struct N} : R :=
match N with
| O => 1
| S p => prod_f_SO An p * An (S p)
end.
(**********)
Lemma prod_SO_split :
forall (An:nat -> R) (n k:nat),
(k <= n)%nat ->
prod_f_SO An n =
prod_f_SO An k * prod_f_SO (fun l:nat => An (k + l)%nat) (n - k).
Proof.
intros; induction n as [| n Hrecn].
cut (k = 0%nat);
[ intro; rewrite H0; simpl in |- *; ring | inversion H; reflexivity ].
cut (k = S n \/ (k <= n)%nat).
intro; elim H0; intro.
rewrite H1; simpl in |- *; rewrite <- minus_n_n; simpl in |- *; ring.
replace (S n - k)%nat with (S (n - k)).
simpl in |- *; replace (k + S (n - k))%nat with (S n).
rewrite Hrecn; [ ring | assumption ].
omega.
omega.
omega.
Qed.
(**********)
Lemma prod_SO_pos :
forall (An:nat -> R) (N:nat),
(forall n:nat, (n <= N)%nat -> 0 <= An n) -> 0 <= prod_f_SO An N.
Proof.
intros; induction N as [| N HrecN].
simpl in |- *; left; apply Rlt_0_1.
simpl in |- *; apply Rmult_le_pos.
apply HrecN; intros; apply H; apply le_trans with N;
[ assumption | apply le_n_Sn ].
apply H; apply le_n.
Qed.
(**********)
Lemma prod_SO_Rle :
forall (An Bn:nat -> R) (N:nat),
(forall n:nat, (n <= N)%nat -> 0 <= An n <= Bn n) ->
prod_f_SO An N <= prod_f_SO Bn N.
Proof.
intros; induction N as [| N HrecN].
right; reflexivity.
simpl in |- *; apply Rle_trans with (prod_f_SO An N * Bn (S N)).
apply Rmult_le_compat_l.
apply prod_SO_pos; intros; elim (H n (le_trans _ _ _ H0 (le_n_Sn N))); intros;
assumption.
elim (H (S N) (le_n (S N))); intros; assumption.
do 2 rewrite <- (Rmult_comm (Bn (S N))); apply Rmult_le_compat_l.
elim (H (S N) (le_n (S N))); intros.
apply Rle_trans with (An (S N)); assumption.
apply HrecN; intros; elim (H n (le_trans _ _ _ H0 (le_n_Sn N))); intros;
split; assumption.
Qed.
(** Application to factorial *)
Lemma fact_prodSO :
forall n:nat, INR (fact n) = prod_f_SO (fun k:nat => INR k) n.
Proof.
intro; induction n as [| n Hrecn].
reflexivity.
change (INR (S n * fact n) = prod_f_SO (fun k:nat => INR k) (S n)) in |- *.
rewrite mult_INR; rewrite Rmult_comm; rewrite Hrecn; reflexivity.
Qed.
Lemma le_n_2n : forall n:nat, (n <= 2 * n)%nat.
Proof.
simple induction n.
replace (2 * 0)%nat with 0%nat; [ apply le_n | ring ].
intros; replace (2 * S n0)%nat with (S (S (2 * n0))).
apply le_n_S; apply le_S; assumption.
replace (S (S (2 * n0))) with (2 * n0 + 2)%nat; [ idtac | ring ].
replace (S n0) with (n0 + 1)%nat; [ idtac | ring ].
ring.
Qed.
(** We prove that (N!)^2<=(2N-k)!*k! forall k in [|O;2N|] *)
Lemma RfactN_fact2N_factk :
forall N k:nat,
(k <= 2 * N)%nat ->
Rsqr (INR (fact N)) <= INR (fact (2 * N - k)) * INR (fact k).
Proof.
intros; unfold Rsqr in |- *; repeat rewrite fact_prodSO.
cut ((k <= N)%nat \/ (N <= k)%nat).
intro; elim H0; intro.
rewrite (prod_SO_split (fun l:nat => INR l) (2 * N - k) N).
rewrite Rmult_assoc; apply Rmult_le_compat_l.
apply prod_SO_pos; intros; apply pos_INR.
replace (2 * N - k - N)%nat with (N - k)%nat.
rewrite Rmult_comm; rewrite (prod_SO_split (fun l:nat => INR l) N k).
apply Rmult_le_compat_l.
apply prod_SO_pos; intros; apply pos_INR.
apply prod_SO_Rle; intros; split.
apply pos_INR.
apply le_INR; apply plus_le_compat_r; assumption.
assumption.
omega.
omega.
rewrite <- (Rmult_comm (prod_f_SO (fun l:nat => INR l) k));
rewrite (prod_SO_split (fun l:nat => INR l) k N).
rewrite Rmult_assoc; apply Rmult_le_compat_l.
apply prod_SO_pos; intros; apply pos_INR.
rewrite Rmult_comm;
rewrite (prod_SO_split (fun l:nat => INR l) N (2 * N - k)).
apply Rmult_le_compat_l.
apply prod_SO_pos; intros; apply pos_INR.
replace (N - (2 * N - k))%nat with (k - N)%nat.
apply prod_SO_Rle; intros; split.
apply pos_INR.
apply le_INR; apply plus_le_compat_r.
omega.
omega.
omega.
assumption.
omega.
Qed.
(**********)
Lemma INR_fact_lt_0 : forall n:nat, 0 < INR (fact n).
Proof.
intro; apply lt_INR_0; apply neq_O_lt; red in |- *; intro;
elim (fact_neq_0 n); symmetry in |- *; assumption.
Qed.
(** We have the following inequality : (C 2N k) <= (C 2N N) forall k in [|O;2N|] *)
Lemma C_maj : forall N k:nat, (k <= 2 * N)%nat -> C (2 * N) k <= C (2 * N) N.
Proof.
intros; unfold C in |- *; unfold Rdiv in |- *; apply Rmult_le_compat_l.
apply pos_INR.
replace (2 * N - N)%nat with N.
apply Rmult_le_reg_l with (INR (fact N) * INR (fact N)).
apply Rmult_lt_0_compat; apply INR_fact_lt_0.
rewrite <- Rinv_r_sym.
rewrite Rmult_comm;
apply Rmult_le_reg_l with (INR (fact k) * INR (fact (2 * N - k))).
apply Rmult_lt_0_compat; apply INR_fact_lt_0.
rewrite Rmult_1_r; rewrite <- mult_INR; rewrite <- Rmult_assoc;
rewrite <- Rinv_r_sym.
rewrite Rmult_1_l; rewrite mult_INR; rewrite (Rmult_comm (INR (fact k)));
replace (INR (fact N) * INR (fact N)) with (Rsqr (INR (fact N))).
apply RfactN_fact2N_factk.
assumption.
reflexivity.
rewrite mult_INR; apply prod_neq_R0; apply INR_fact_neq_0.
apply prod_neq_R0; apply INR_fact_neq_0.
omega.
Qed.
|
