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
(************************************************************************)
9
(*i $Id: Rfunctions.v 10762 2008-04-06 16:57:31Z herbelin $ i*)
11
(*i Some properties about pow and sum have been made with John Harrison i*)
12
(*i Some Lemmas (about pow and powerRZ) have been done by Laurent Thery i*)
14
(********************************************************)
15
(** Definition of the sum functions *)
17
(********************************************************)
18
Require Export ArithRing.
21
Require Export Rpow_def.
23
Require Export Rbasic_fun.
25
Require Export SplitAbsolu.
26
Require Export SplitRmult.
27
Require Export ArithProp.
29
Require Import Zpower.
30
Open Local Scope nat_scope.
31
Open Local Scope R_scope.
33
(*******************************)
34
(** * Lemmas about factorial *)
35
(*******************************)
37
Lemma INR_fact_neq_0 : forall n:nat, INR (fact n) <> 0.
39
intro; red in |- *; intro; apply (not_O_INR (fact n) (fact_neq_0 n));
44
Lemma fact_simpl : forall n:nat, fact (S n) = (S n * fact n)%nat.
51
forall n:nat, / INR (fact (S n)) * / / INR (fact n) = / INR (S n).
53
intro; rewrite (Rinv_involutive (INR (fact n)) (INR_fact_neq_0 n));
54
unfold fact at 1 in |- *; cbv beta iota in |- *; fold fact in |- *;
55
rewrite (mult_INR (S n) (fact n));
56
rewrite (Rinv_mult_distr (INR (S n)) (INR (fact n))).
57
rewrite (Rmult_assoc (/ INR (S n)) (/ INR (fact n)) (INR (fact n)));
58
rewrite (Rinv_l (INR (fact n)) (INR_fact_neq_0 n));
59
apply (let (H1, H2) := Rmult_ne (/ INR (S n)) in H1).
60
apply not_O_INR; auto.
64
(*******************************)
66
(*******************************)
69
Infix "^" := pow : R_scope.
71
Lemma pow_O : forall x:R, x ^ 0 = 1.
76
Lemma pow_1 : forall x:R, x ^ 1 = x.
78
simpl in |- *; auto with real.
81
Lemma pow_add : forall (x:R) (n m:nat), x ^ (n + m) = x ^ n * x ^ m.
83
intros x n; elim n; simpl in |- *; auto with real.
84
intros n0 H' m; rewrite H'; auto with real.
87
Lemma pow_nonzero : forall (x:R) (n:nat), x <> 0 -> x ^ n <> 0.
89
intro; simple induction n; simpl in |- *.
90
intro; red in |- *; intro; apply R1_neq_R0; assumption.
91
intros; red in |- *; intro; elim (Rmult_integral x (x ^ n0) H1).
96
Hint Resolve pow_O pow_1 pow_add pow_nonzero: real.
99
forall (x:R) (n m:nat), x <> 0 -> x ^ n = x ^ (n + m) * / x ^ m.
101
intros x n; elim n; simpl in |- *; auto with real.
103
rewrite Rmult_assoc; rewrite <- H'; auto.
106
Lemma pow_lt : forall (x:R) (n:nat), 0 < x -> 0 < x ^ n.
108
intros x n; elim n; simpl in |- *; auto with real.
109
intros n0 H' H'0; replace 0 with (x * 0); auto with real.
111
Hint Resolve pow_lt: real.
113
Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n.
115
intros x n; elim n; simpl in |- *; auto with real.
116
intros H' H'0; elimtype False; omega.
118
simpl in |- *; rewrite Rmult_1_r; auto.
119
intros n1 H' H'0 H'1.
120
replace 1 with (1 * 1); auto with real.
121
apply Rlt_trans with (r2 := x * 1); auto with real.
122
apply Rmult_lt_compat_l; auto with real.
123
apply Rlt_trans with (r2 := 1); auto with real.
124
apply H'; auto with arith.
126
Hint Resolve Rlt_pow_R1: real.
128
Lemma Rlt_pow : forall (x:R) (n m:nat), 1 < x -> (n < m)%nat -> x ^ n < x ^ m.
130
intros x n m H' H'0; replace m with (m - n + n)%nat.
132
pattern (x ^ n) at 1 in |- *; replace (x ^ n) with (1 * x ^ n);
135
repeat rewrite (fun y:R => Rmult_comm y (x ^ n));
136
rewrite <- Rmult_minus_distr_l.
137
replace 0 with (x ^ n * 0); auto with real.
138
apply Rmult_lt_compat_l; auto with real.
139
apply pow_lt; auto with real.
140
apply Rlt_trans with (r2 := 1); auto with real.
141
apply Rlt_minus; auto with real.
142
apply Rlt_pow_R1; auto with arith.
143
apply plus_lt_reg_l with (p := n); auto with arith.
144
rewrite le_plus_minus_r; auto with arith; rewrite <- plus_n_O; auto.
145
rewrite plus_comm; auto with arith.
147
Hint Resolve Rlt_pow: real.
150
Lemma tech_pow_Rmult : forall (x:R) (n:nat), x * x ^ n = x ^ S n.
152
simple induction n; simpl in |- *; trivial.
156
Lemma tech_pow_Rplus :
157
forall (x:R) (a n:nat), x ^ a + INR n * x ^ a = INR (S n) * x ^ a.
159
intros; pattern (x ^ a) at 1 in |- *;
160
rewrite <- (let (H1, H2) := Rmult_ne (x ^ a) in H1);
161
rewrite (Rmult_comm (INR n) (x ^ a));
162
rewrite <- (Rmult_plus_distr_l (x ^ a) 1 (INR n));
163
rewrite (Rplus_comm 1 (INR n)); rewrite <- (S_INR n);
167
Lemma poly : forall (n:nat) (x:R), 0 < x -> 1 + INR n * x <= (1 + x) ^ n.
170
simpl in |- *; cut (1 + 0 * x = 1).
171
intro; rewrite H0; unfold Rle in |- *; right; reflexivity.
173
intros; unfold pow in |- *; fold pow in |- *;
175
(Rle_trans (1 + INR (S n0) * x) ((1 + x) * (1 + INR n0 * x))
176
((1 + x) * (1 + x) ^ n0)).
177
cut ((1 + x) * (1 + INR n0 * x) = 1 + INR (S n0) * x + INR n0 * (x * x)).
178
intro; rewrite H1; pattern (1 + INR (S n0) * x) at 1 in |- *;
179
rewrite <- (let (H1, H2) := Rplus_ne (1 + INR (S n0) * x) in H1);
180
apply Rplus_le_compat_l; elim n0; intros.
181
simpl in |- *; rewrite Rmult_0_l; unfold Rle in |- *; right; auto.
182
unfold Rle in |- *; left; generalize Rmult_gt_0_compat; unfold Rgt in |- *;
183
intro; fold (Rsqr x) in |- *;
184
apply (H3 (INR (S n1)) (Rsqr x) (lt_INR_0 (S n1) (lt_O_Sn n1)));
186
apply (Rlt_0_sqr x (Rlt_dichotomy_converse x 0 (or_intror (x < 0) H))).
187
rewrite (S_INR n0); ring.
188
unfold Rle in H0; elim H0; intro.
189
unfold Rle in |- *; left; apply Rmult_lt_compat_l.
190
rewrite Rplus_comm; apply (Rle_lt_0_plus_1 x (Rlt_le 0 x H)).
192
rewrite H1; unfold Rle in |- *; right; trivial.
195
Lemma Power_monotonic :
196
forall (x:R) (m n:nat),
197
Rabs x > 1 -> (m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n).
199
intros x m n H; induction n as [| n Hrecn]; intros; inversion H0.
200
unfold Rle in |- *; right; reflexivity.
201
unfold Rle in |- *; right; reflexivity.
202
apply (Rle_trans (Rabs (x ^ m)) (Rabs (x ^ n)) (Rabs (x ^ S n))).
203
apply Hrecn; assumption.
204
simpl in |- *; rewrite Rabs_mult.
205
pattern (Rabs (x ^ n)) at 1 in |- *.
206
rewrite <- Rmult_1_r.
207
rewrite (Rmult_comm (Rabs x) (Rabs (x ^ n))).
208
apply Rmult_le_compat_l.
211
apply Rlt_le; assumption.
214
Lemma RPow_abs : forall (x:R) (n:nat), Rabs x ^ n = Rabs (x ^ n).
216
intro; simple induction n; simpl in |- *.
217
apply sym_eq; apply Rabs_pos_eq; apply Rlt_le; apply Rlt_0_1.
218
intros; rewrite H; apply sym_eq; apply Rabs_mult.
222
Lemma Pow_x_infinity :
226
exists N : nat, (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) >= b).
228
intros; elim (archimed (b * / (Rabs x - 1))); intros; clear H1;
229
cut (exists N : nat, INR N >= b * / (Rabs x - 1)).
230
intro; elim H1; clear H1; intros; exists x0; intros;
231
apply (Rge_trans (Rabs (x ^ n)) (Rabs (x ^ x0)) b).
232
apply Rle_ge; apply Power_monotonic; assumption.
233
rewrite <- RPow_abs; cut (Rabs x = 1 + (Rabs x - 1)).
235
apply (Rge_trans ((1 + (Rabs x - 1)) ^ x0) (1 + INR x0 * (Rabs x - 1)) b).
236
apply Rle_ge; apply poly; fold (Rabs x - 1 > 0) in |- *; apply Rgt_minus;
238
apply (Rge_trans (1 + INR x0 * (Rabs x - 1)) (INR x0 * (Rabs x - 1)) b).
239
apply Rle_ge; apply Rlt_le; rewrite (Rplus_comm 1 (INR x0 * (Rabs x - 1)));
240
pattern (INR x0 * (Rabs x - 1)) at 1 in |- *;
241
rewrite <- (let (H1, H2) := Rplus_ne (INR x0 * (Rabs x - 1)) in H1);
242
apply Rplus_lt_compat_l; apply Rlt_0_1.
243
cut (b = b * / (Rabs x - 1) * (Rabs x - 1)).
244
intros; rewrite H4; apply Rmult_ge_compat_r.
245
apply Rge_minus; unfold Rge in |- *; left; assumption.
247
rewrite Rmult_assoc; rewrite Rinv_l.
249
apply Rlt_dichotomy_converse; right; apply Rgt_minus; assumption.
251
cut ((0 <= up (b * / (Rabs x - 1)))%Z \/ (up (b * / (Rabs x - 1)) <= 0)%Z).
252
intros; elim H1; intro.
253
elim (IZN (up (b * / (Rabs x - 1))) H2); intros; exists x0;
255
(Rge_trans (INR x0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))).
256
rewrite INR_IZR_INZ; apply IZR_ge; omega.
257
unfold Rge in |- *; left; assumption.
260
(Rge_trans (INR 0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))).
261
rewrite INR_IZR_INZ; apply IZR_ge; simpl in |- *; omega.
262
unfold Rge in |- *; left; assumption.
266
Lemma pow_ne_zero : forall n:nat, n <> 0%nat -> 0 ^ n = 0.
270
intros; elim H; reflexivity.
271
intros; simpl in |- *; apply Rmult_0_l.
274
Lemma Rinv_pow : forall (x:R) (n:nat), x <> 0 -> / x ^ n = (/ x) ^ n.
276
intros; elim n; simpl in |- *.
278
intro m; intro; rewrite Rinv_mult_distr.
279
rewrite H0; reflexivity; assumption.
281
apply pow_nonzero; assumption.
284
Lemma pow_lt_1_zero :
289
exists N : nat, (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) < y).
291
intros; elim (Req_dec x 0); intro.
292
exists 1%nat; rewrite H1; intros n GE; rewrite pow_ne_zero.
293
rewrite Rabs_R0; assumption.
295
cut (Rabs (/ x) > 1).
296
intros; elim (Pow_x_infinity (/ x) H2 (/ y + 1)); intros N.
297
exists N; intros; rewrite <- (Rinv_involutive y).
298
rewrite <- (Rinv_involutive (Rabs (x ^ n))).
299
apply Rinv_lt_contravar.
300
apply Rmult_lt_0_compat.
301
apply Rinv_0_lt_compat.
303
apply Rinv_0_lt_compat.
307
rewrite <- Rabs_Rinv.
309
apply (Rlt_le_trans (/ y) (/ y + 1) (Rabs ((/ x) ^ n))).
310
pattern (/ y) at 1 in |- *.
311
rewrite <- (let (H1, H2) := Rplus_ne (/ y) in H1).
312
apply Rplus_lt_compat_l.
323
apply Rlt_dichotomy_converse.
324
right; unfold Rgt in |- *; assumption.
325
rewrite <- (Rinv_involutive 1).
327
unfold Rgt in |- *; apply Rinv_lt_contravar.
328
apply Rmult_lt_0_compat.
331
rewrite Rinv_1; apply Rlt_0_1.
332
rewrite Rinv_1; assumption.
334
red in |- *; intro; apply R1_neq_R0; assumption.
337
Lemma pow_R1 : forall (r:R) (n:nat), r ^ n = 1 -> Rabs r = 1 \/ n = 0%nat.
340
case (Req_dec (Rabs r) 1); auto; intros H'1.
341
case (Rdichotomy _ _ H'1); intros H'2.
342
generalize H'; case n; auto.
344
cut (r <> 0); [ intros Eq1 | idtac ].
345
cut (Rabs r <> 0); [ intros Eq2 | apply Rabs_no_R0 ]; auto.
346
absurd (Rabs (/ r) ^ 0 < Rabs (/ r) ^ S n0); auto.
347
replace (Rabs (/ r) ^ S n0) with 1.
348
simpl in |- *; apply Rlt_irrefl; auto.
349
rewrite Rabs_Rinv; auto.
350
rewrite <- Rinv_pow; auto.
351
rewrite RPow_abs; auto.
352
rewrite H'0; rewrite Rabs_right; auto with real rorders.
353
apply Rlt_pow; auto with arith.
354
rewrite Rabs_Rinv; auto.
355
apply Rmult_lt_reg_l with (r := Rabs r).
356
case (Rabs_pos r); auto.
357
intros H'3; case Eq2; auto.
358
rewrite Rmult_1_r; rewrite Rinv_r; auto with real.
359
red in |- *; intro; absurd (r ^ S n0 = 1); auto.
360
simpl in |- *; rewrite H; rewrite Rmult_0_l; auto with real.
361
generalize H'; case n; auto.
363
cut (r <> 0); [ intros Eq1 | auto with real ].
364
cut (Rabs r <> 0); [ intros Eq2 | apply Rabs_no_R0 ]; auto.
365
absurd (Rabs r ^ 0 < Rabs r ^ S n0); auto with real arith.
366
repeat rewrite RPow_abs; rewrite H'0; simpl in |- *; auto with real.
367
red in |- *; intro; absurd (r ^ S n0 = 1); auto.
368
simpl in |- *; rewrite H; rewrite Rmult_0_l; auto with real.
371
Lemma pow_Rsqr : forall (x:R) (n:nat), x ^ (2 * n) = Rsqr x ^ n.
373
intros; induction n as [| n Hrecn].
375
replace (2 * S n)%nat with (S (S (2 * n))).
376
replace (x ^ S (S (2 * n))) with (x * x * x ^ (2 * n)).
377
rewrite Hrecn; reflexivity.
382
Lemma pow_le : forall (a:R) (n:nat), 0 <= a -> 0 <= a ^ n.
384
intros; induction n as [| n Hrecn].
385
simpl in |- *; left; apply Rlt_0_1.
386
simpl in |- *; apply Rmult_le_pos; assumption.
390
Lemma pow_1_even : forall n:nat, (-1) ^ (2 * n) = 1.
392
intro; induction n as [| n Hrecn].
394
replace (2 * S n)%nat with (2 + 2 * n)%nat by ring.
395
rewrite pow_add; rewrite Hrecn; simpl in |- *; ring.
399
Lemma pow_1_odd : forall n:nat, (-1) ^ S (2 * n) = -1.
401
intro; replace (S (2 * n)) with (2 * n + 1)%nat by ring.
402
rewrite pow_add; rewrite pow_1_even; simpl in |- *; ring.
406
Lemma pow_1_abs : forall n:nat, Rabs ((-1) ^ n) = 1.
408
intro; induction n as [| n Hrecn].
409
simpl in |- *; apply Rabs_R1.
410
replace (S n) with (n + 1)%nat; [ rewrite pow_add | ring ].
412
rewrite Hrecn; rewrite Rmult_1_l; simpl in |- *; rewrite Rmult_1_r;
413
rewrite Rabs_Ropp; apply Rabs_R1.
416
Lemma pow_mult : forall (x:R) (n1 n2:nat), x ^ (n1 * n2) = (x ^ n1) ^ n2.
418
intros; induction n2 as [| n2 Hrecn2].
419
simpl in |- *; replace (n1 * 0)%nat with 0%nat; [ reflexivity | ring ].
420
replace (n1 * S n2)%nat with (n1 * n2 + n1)%nat.
421
replace (S n2) with (n2 + 1)%nat by ring.
422
do 2 rewrite pow_add.
429
Lemma pow_incr : forall (x y:R) (n:nat), 0 <= x <= y -> x ^ n <= y ^ n.
432
induction n as [| n Hrecn].
436
apply Rle_trans with (y * x ^ n).
437
do 2 rewrite <- (Rmult_comm (x ^ n)).
438
apply Rmult_le_compat_l.
439
apply pow_le; assumption.
441
apply Rmult_le_compat_l.
442
apply Rle_trans with x; assumption.
446
Lemma pow_R1_Rle : forall (x:R) (k:nat), 1 <= x -> 1 <= x ^ k.
449
induction k as [| k Hreck].
452
apply Rle_trans with (x * 1).
453
rewrite Rmult_1_r; assumption.
454
apply Rmult_le_compat_l.
455
left; apply Rlt_le_trans with 1; [ apply Rlt_0_1 | assumption ].
460
forall (x:R) (m n:nat), 1 <= x -> (m <= n)%nat -> x ^ m <= x ^ n.
463
replace n with (n - m + m)%nat.
466
pattern (x ^ m) at 1 in |- *; rewrite <- Rmult_1_r.
467
apply Rmult_le_compat_l.
468
apply pow_le; left; apply Rlt_le_trans with 1; [ apply Rlt_0_1 | assumption ].
469
apply pow_R1_Rle; assumption.
471
symmetry in |- *; apply le_plus_minus; assumption.
474
Lemma pow1 : forall n:nat, 1 ^ n = 1.
476
intro; induction n as [| n Hrecn].
478
simpl in |- *; rewrite Hrecn; rewrite Rmult_1_r; reflexivity.
481
Lemma pow_Rabs : forall (x:R) (n:nat), x ^ n <= Rabs x ^ n.
483
intros; induction n as [| n Hrecn].
485
simpl in |- *; case (Rcase_abs x); intro.
486
apply Rle_trans with (Rabs (x * x ^ n)).
489
apply Rmult_le_compat_l.
491
right; symmetry in |- *; apply RPow_abs.
492
pattern (Rabs x) at 1 in |- *; rewrite (Rabs_right x r);
493
apply Rmult_le_compat_l.
494
apply Rge_le; exact r.
498
Lemma pow_maj_Rabs : forall (x y:R) (n:nat), Rabs y <= x -> y ^ n <= x ^ n.
500
intros; cut (0 <= x).
501
intro; apply Rle_trans with (Rabs y ^ n).
503
induction n as [| n Hrecn].
505
simpl in |- *; apply Rle_trans with (x * Rabs y ^ n).
506
do 2 rewrite <- (Rmult_comm (Rabs y ^ n)).
507
apply Rmult_le_compat_l.
508
apply pow_le; apply Rabs_pos.
510
apply Rmult_le_compat_l.
513
apply Rle_trans with (Rabs y); [ apply Rabs_pos | exact H ].
516
(*******************************)
518
(*******************************)
519
(*i Due to L.Thery i*)
522
generalize (refl_equal name); pattern name at -1 in |- *; case name.
524
Definition powerRZ (x:R) (n:Z) :=
527
| Zpos p => x ^ nat_of_P p
528
| Zneg p => / x ^ nat_of_P p
531
Infix Local "^Z" := powerRZ (at level 30, right associativity) : R_scope.
534
forall (x:Z) (n:nat), (0 <= x)%Z -> (0 <= Zpower_nat x n)%Z.
536
induction n; unfold Zpower_nat in |- *; simpl in |- *; auto with zarith.
539
Lemma powerRZ_O : forall x:R, x ^Z 0 = 1.
544
Lemma powerRZ_1 : forall x:R, x ^Z Zsucc 0 = x.
546
simpl in |- *; auto with real.
549
Lemma powerRZ_NOR : forall (x:R) (z:Z), x <> 0 -> x ^Z z <> 0.
551
destruct z; simpl in |- *; auto with real.
555
forall (x:R) (n m:Z), x <> 0 -> x ^Z (n + m) = x ^Z n * x ^Z m.
557
intro x; destruct n as [| n1| n1]; destruct m as [| m1| m1]; simpl in |- *;
560
rewrite nat_of_P_plus_morphism; auto with real.
562
case_eq ((n1 ?= m1)%positive Datatypes.Eq); simpl in |- *; auto with real.
563
intros H' H'0; rewrite Pcompare_Eq_eq with (1 := H'); auto with real.
564
intros H' H'0; rewrite (nat_of_P_minus_morphism m1 n1); auto with real.
565
rewrite (pow_RN_plus x (nat_of_P m1 - nat_of_P n1) (nat_of_P n1));
567
rewrite plus_comm; rewrite le_plus_minus_r; auto with real.
568
rewrite Rinv_mult_distr; auto with real.
569
rewrite Rinv_involutive; auto with real.
571
apply nat_of_P_lt_Lt_compare_morphism; auto.
573
intros H' H'0; rewrite (nat_of_P_minus_morphism n1 m1); auto with real.
574
rewrite (pow_RN_plus x (nat_of_P n1 - nat_of_P m1) (nat_of_P m1));
576
rewrite plus_comm; rewrite le_plus_minus_r; auto with real.
578
change (nat_of_P n1 > nat_of_P m1)%nat in |- *.
579
apply nat_of_P_gt_Gt_compare_morphism; auto.
581
case_eq ((n1 ?= m1)%positive Datatypes.Eq); simpl in |- *; auto with real.
582
intros H' H'0; rewrite Pcompare_Eq_eq with (1 := H'); auto with real.
583
intros H' H'0; rewrite (nat_of_P_minus_morphism m1 n1); auto with real.
584
rewrite (pow_RN_plus x (nat_of_P m1 - nat_of_P n1) (nat_of_P n1));
586
rewrite plus_comm; rewrite le_plus_minus_r; auto with real.
588
apply nat_of_P_lt_Lt_compare_morphism; auto.
590
intros H' H'0; rewrite (nat_of_P_minus_morphism n1 m1); auto with real.
591
rewrite (pow_RN_plus x (nat_of_P n1 - nat_of_P m1) (nat_of_P m1));
593
rewrite plus_comm; rewrite le_plus_minus_r; auto with real.
594
rewrite Rinv_mult_distr; auto with real.
596
change (nat_of_P n1 > nat_of_P m1)%nat in |- *.
597
apply nat_of_P_gt_Gt_compare_morphism; auto.
599
rewrite nat_of_P_plus_morphism; auto with real.
600
intros H'; rewrite pow_add; auto with real.
601
apply Rinv_mult_distr; auto.
602
apply pow_nonzero; auto.
603
apply pow_nonzero; auto.
605
Hint Resolve powerRZ_O powerRZ_1 powerRZ_NOR powerRZ_add: real.
607
Lemma Zpower_nat_powerRZ :
608
forall n m:nat, IZR (Zpower_nat (Z_of_nat n) m) = INR n ^Z Z_of_nat m.
610
intros n m; elim m; simpl in |- *; auto with real.
611
intros m1 H'; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; simpl in |- *.
612
replace (Zpower_nat (Z_of_nat n) (S m1)) with
613
(Z_of_nat n * Zpower_nat (Z_of_nat n) m1)%Z.
614
rewrite mult_IZR; auto with real.
615
repeat rewrite <- INR_IZR_INZ; simpl in |- *.
616
rewrite H'; simpl in |- *.
617
case m1; simpl in |- *; auto with real.
618
intros m2; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto.
619
unfold Zpower_nat in |- *; auto.
622
Lemma powerRZ_lt : forall (x:R) (z:Z), 0 < x -> 0 < x ^Z z.
624
intros x z; case z; simpl in |- *; auto with real.
626
Hint Resolve powerRZ_lt: real.
628
Lemma powerRZ_le : forall (x:R) (z:Z), 0 < x -> 0 <= x ^Z z.
630
intros x z H'; apply Rlt_le; auto with real.
632
Hint Resolve powerRZ_le: real.
634
Lemma Zpower_nat_powerRZ_absolu :
635
forall n m:Z, (0 <= m)%Z -> IZR (Zpower_nat n (Zabs_nat m)) = IZR n ^Z m.
637
intros n m; case m; simpl in |- *; auto with zarith.
638
intros p H'; elim (nat_of_P p); simpl in |- *; auto with zarith.
639
intros n0 H'0; rewrite <- H'0; simpl in |- *; auto with zarith.
640
rewrite <- mult_IZR; auto.
641
intros p H'; absurd (0 <= Zneg p)%Z; auto with zarith.
644
Lemma powerRZ_R1 : forall n:Z, 1 ^Z n = 1.
646
intros n; case n; simpl in |- *; auto.
647
intros p; elim (nat_of_P p); simpl in |- *; auto; intros n0 H'; rewrite H';
649
intros p; elim (nat_of_P p); simpl in |- *.
651
intros n1 H'; rewrite Rinv_mult_distr; try rewrite Rinv_1; try rewrite H';
655
(*******************************)
656
(* For easy interface *)
657
(*******************************)
658
(* decimal_exp r z is defined as r 10^z *)
660
Definition decimal_exp (r:R) (z:Z) : R := (r * 10 ^Z z).
663
(*******************************)
664
(** * Sum of n first naturals *)
665
(*******************************)
667
Boxed Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) {struct n} : nat :=
670
| S n' => (sum_nat_f_O f n' + f (S n'))%nat
674
Definition sum_nat_f (s n:nat) (f:nat -> nat) : nat :=
675
sum_nat_f_O (fun x:nat => f (x + s)%nat) (n - s).
678
Definition sum_nat_O (n:nat) : nat := sum_nat_f_O (fun x:nat => x) n.
681
Definition sum_nat (s n:nat) : nat := sum_nat_f s n (fun x:nat => x).
683
(*******************************)
685
(*******************************)
687
Fixpoint sum_f_R0 (f:nat -> R) (N:nat) {struct N} : R :=
690
| S i => sum_f_R0 f i + f (S i)
694
Definition sum_f (s n:nat) (f:nat -> R) : R :=
695
sum_f_R0 (fun x:nat => f (x + s)%nat) (n - s).
698
forall (x:R) (n:nat),
699
sum_f_R0 (fun n:nat => x ^ n) n * (x - 1) = x ^ (n + 1) - 1.
701
intros; induction n as [| n Hrecn]; simpl in |- *.
703
rewrite Rmult_plus_distr_r; rewrite Hrecn; cut ((n + 1)%nat = S n).
704
intro H; rewrite H; simpl in |- *; ring.
708
Lemma sum_f_R0_triangle :
709
forall (x:nat -> R) (n:nat),
710
Rabs (sum_f_R0 x n) <= sum_f_R0 (fun i:nat => Rabs (x i)) n.
712
intro; simple induction n; simpl in |- *.
713
unfold Rle in |- *; right; reflexivity.
716
(Rle_trans (Rabs (sum_f_R0 x m + x (S m)))
717
(Rabs (sum_f_R0 x m) + Rabs (x (S m)))
718
(sum_f_R0 (fun i:nat => Rabs (x i)) m + Rabs (x (S m)))).
721
rewrite (Rplus_comm (sum_f_R0 (fun i:nat => Rabs (x i)) m) (Rabs (x (S m))));
722
apply Rplus_le_compat_l; assumption.
725
(*******************************)
726
(** * Distance in R *)
727
(*******************************)
730
Definition R_dist (x y:R) : R := Rabs (x - y).
733
Lemma R_dist_pos : forall x y:R, R_dist x y >= 0.
735
intros; unfold R_dist in |- *; unfold Rabs in |- *; case (Rcase_abs (x - y));
737
unfold Rge in |- *; left; apply (Ropp_gt_lt_0_contravar (x - y) l).
742
Lemma R_dist_sym : forall x y:R, R_dist x y = R_dist y x.
744
unfold R_dist in |- *; intros; split_Rabs; try ring.
745
generalize (Ropp_gt_lt_0_contravar (y - x) r); intro;
746
rewrite (Ropp_minus_distr y x) in H; generalize (Rlt_asym (x - y) 0 r0);
747
intro; unfold Rgt in H; elimtype False; auto.
748
generalize (minus_Rge y x r); intro; generalize (minus_Rge x y r0); intro;
749
generalize (Rge_antisym x y H0 H); intro; rewrite H1;
754
Lemma R_dist_refl : forall x y:R, R_dist x y = 0 <-> x = y.
756
unfold R_dist in |- *; intros; split_Rabs; split; intros.
757
rewrite (Ropp_minus_distr x y) in H; apply sym_eq;
758
apply (Rminus_diag_uniq y x H).
759
rewrite (Ropp_minus_distr x y); generalize (sym_eq H); intro;
760
apply (Rminus_diag_eq y x H0).
761
apply (Rminus_diag_uniq x y H).
762
apply (Rminus_diag_eq x y H).
765
Lemma R_dist_eq : forall x:R, R_dist x x = 0.
767
unfold R_dist in |- *; intros; split_Rabs; intros; ring.
771
Lemma R_dist_tri : forall x y z:R, R_dist x y <= R_dist x z + R_dist z y.
773
intros; unfold R_dist in |- *; replace (x - y) with (x - z + (z - y));
774
[ apply (Rabs_triang (x - z) (z - y)) | ring ].
779
forall a b c d:R, R_dist (a + c) (b + d) <= R_dist a b + R_dist c d.
781
intros; unfold R_dist in |- *;
782
replace (a + c - (b + d)) with (a - b + (c - d)).
783
exact (Rabs_triang (a - b) (c - d)).
787
(*******************************)
788
(** * Infinite Sum *)
789
(*******************************)
791
Definition infinite_sum (s:nat -> R) (l:R) : Prop :=
795
(forall n:nat, (n >= N)%nat -> R_dist (sum_f_R0 s n) l < eps).
797
(** Compatibility with previous versions *)
798
Notation infinit_sum := infinite_sum (only parsing).
added
removed
theories/Reals/Rfunctions.v
