← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Reals/Rprod.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

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