summaryrefslogtreecommitdiff
path: root/theories/Reals/Rpower.v
blob: adf53ef906a0140dbce546eebea6fcd516506279 (plain)
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
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
(************************************************************************)
(*  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: Rpower.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
(*i Due to L.Thery i*) 

(************************************************************)
(* Definitions of log and Rpower : R->R->R; main properties *)
(************************************************************)

Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Rtrigo.
Require Import Ranalysis1.
Require Import Exp_prop.
Require Import Rsqrt_def.
Require Import R_sqrt.
Require Import MVT.
Require Import Ranalysis4.
Open Local Scope R_scope.

Lemma P_Rmin : forall (P:R -> Prop) (x y:R), P x -> P y -> P (Rmin x y).
Proof.
  intros P x y H1 H2; unfold Rmin in |- *; case (Rle_dec x y); intro;
    assumption.
Qed.

Lemma exp_le_3 : exp 1 <= 3.
Proof.
  assert (exp_1 : exp 1 <> 0).
  assert (H0 := exp_pos 1); red in |- *; intro; rewrite H in H0;
    elim (Rlt_irrefl _ H0).
  apply Rmult_le_reg_l with (/ exp 1).
  apply Rinv_0_lt_compat; apply exp_pos.
  rewrite <- Rinv_l_sym.
  apply Rmult_le_reg_l with (/ 3).
  apply Rinv_0_lt_compat; prove_sup0.
  rewrite Rmult_1_r; rewrite <- (Rmult_comm 3); rewrite <- Rmult_assoc;
    rewrite <- Rinv_l_sym.
  rewrite Rmult_1_l; replace (/ exp 1) with (exp (-1)).
  unfold exp in |- *; case (exist_exp (-1)); intros; simpl in |- *;
    unfold exp_in in e;
      assert (H := alternated_series_ineq (fun i:nat => / INR (fact i)) x 1).
  cut
    (sum_f_R0 (tg_alt (fun i:nat => / INR (fact i))) (S (2 * 1)) <= x <=
      sum_f_R0 (tg_alt (fun i:nat => / INR (fact i))) (2 * 1)).
  intro; elim H0; clear H0; intros H0 _; simpl in H0; unfold tg_alt in H0;
    simpl in H0.
  replace (/ 3) with
  (1 * / 1 + -1 * 1 * / 1 + -1 * (-1 * 1) * / 2 +
    -1 * (-1 * (-1 * 1)) * / (2 + 1 + 1 + 1 + 1)).
  apply H0.
  repeat rewrite Rinv_1; repeat rewrite Rmult_1_r;
    rewrite Ropp_mult_distr_l_reverse; rewrite Rmult_1_l;
      rewrite Ropp_involutive; rewrite Rplus_opp_r; rewrite Rmult_1_r;
        rewrite Rplus_0_l; rewrite Rmult_1_l; apply Rmult_eq_reg_l with 6.
  rewrite Rmult_plus_distr_l; replace (2 + 1 + 1 + 1 + 1) with 6.
  rewrite <- (Rmult_comm (/ 6)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym.
  rewrite Rmult_1_l; replace 6 with 6.
  do 2 rewrite Rmult_assoc; rewrite <- Rinv_r_sym.
  rewrite Rmult_1_r; rewrite (Rmult_comm 3); rewrite <- Rmult_assoc;
    rewrite <- Rinv_r_sym.
  ring.
  discrR.
  discrR.
  ring.
  discrR.
  ring.
  discrR.
  apply H.
  unfold Un_decreasing in |- *; intros;
    apply Rmult_le_reg_l with (INR (fact n)).
  apply INR_fact_lt_0.
  apply Rmult_le_reg_l with (INR (fact (S n))).
  apply INR_fact_lt_0.
  rewrite <- Rinv_r_sym.
  rewrite Rmult_1_r; rewrite Rmult_comm; rewrite Rmult_assoc;
    rewrite <- Rinv_l_sym.
  rewrite Rmult_1_r; apply le_INR; apply fact_le; apply le_n_Sn.
  apply INR_fact_neq_0.
  apply INR_fact_neq_0.
  assert (H0 := cv_speed_pow_fact 1); unfold Un_cv in |- *; unfold Un_cv in H0;
    intros; elim (H0 _ H1); intros; exists x0; intros; 
      unfold R_dist in H2; unfold R_dist in |- *;
        replace (/ INR (fact n)) with (1 ^ n / INR (fact n)).
  apply (H2 _ H3).
  unfold Rdiv in |- *; rewrite pow1; rewrite Rmult_1_l; reflexivity.
  unfold infinite_sum in e; unfold Un_cv, tg_alt in |- *; intros; elim (e _ H0);
    intros; exists x0; intros;
      replace (sum_f_R0 (fun i:nat => (-1) ^ i * / INR (fact i)) n) with
      (sum_f_R0 (fun i:nat => / INR (fact i) * (-1) ^ i) n).
  apply (H1 _ H2).
  apply sum_eq; intros; apply Rmult_comm.
  apply Rmult_eq_reg_l with (exp 1).
  rewrite <- exp_plus; rewrite Rplus_opp_r; rewrite exp_0;
    rewrite <- Rinv_r_sym.
  reflexivity.
  assumption.
  assumption.
  discrR.
  assumption.
Qed.

(******************************************************************)
(** *                     Properties of  Exp                      *)
(******************************************************************)

Theorem exp_increasing : forall x y:R, x < y -> exp x < exp y.
Proof.
  intros x y H.
  assert (H0 : derivable exp).
  apply derivable_exp.
  assert (H1 := positive_derivative _ H0).
  unfold strict_increasing in H1.
  apply H1.
  intro.
  replace (derive_pt exp x0 (H0 x0)) with (exp x0).
  apply exp_pos.
  symmetry  in |- *; apply derive_pt_eq_0.
  apply (derivable_pt_lim_exp x0).
  apply H.
Qed.

Theorem exp_lt_inv : forall x y:R, exp x < exp y -> x < y.
Proof.
  intros x y H; case (Rtotal_order x y); [ intros H1 | intros [H1| H1] ].
  assumption.
  rewrite H1 in H; elim (Rlt_irrefl _ H).
  assert (H2 := exp_increasing _ _ H1).
  elim (Rlt_irrefl _ (Rlt_trans _ _ _ H H2)).
Qed.

Lemma exp_ineq1 : forall x:R, 0 < x -> 1 + x < exp x.
Proof.
  intros; apply Rplus_lt_reg_r with (- exp 0); rewrite <- (Rplus_comm (exp x));
    assert (H0 := MVT_cor1 exp 0 x derivable_exp H); elim H0; 
      intros; elim H1; intros; unfold Rminus in H2; rewrite H2; 
        rewrite Ropp_0; rewrite Rplus_0_r;
          replace (derive_pt exp x0 (derivable_exp x0)) with (exp x0).
  rewrite exp_0; rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l;
    pattern x at 1 in |- *; rewrite <- Rmult_1_r; rewrite (Rmult_comm (exp x0));
      apply Rmult_lt_compat_l.
  apply H.
  rewrite <- exp_0; apply exp_increasing; elim H3; intros; assumption.
  symmetry  in |- *; apply derive_pt_eq_0; apply derivable_pt_lim_exp.
Qed.

Lemma ln_exists1 : forall y:R, 1 <= y -> { z:R | y = exp z }.
Proof.
  intros; set (f := fun x:R => exp x - y).
  assert (H0 : 0 < y) by (apply Rlt_le_trans with 1; auto with real).
  cut (f 0 <= 0); [intro H1|].
  cut (continuity f); [intro H2|].
  cut (0 <= f y); [intro H3|].
  cut (f 0 * f y <= 0); [intro H4|].
  pose proof (IVT_cor f 0 y H2 (Rlt_le _ _ H0) H4) as (t,(_,H7));
    exists t; unfold f in H7; apply Rminus_diag_uniq_sym; exact H7.
  pattern 0 at 2 in |- *; rewrite <- (Rmult_0_r (f y));
    rewrite (Rmult_comm (f 0)); apply Rmult_le_compat_l; 
      assumption.
  unfold f in |- *; apply Rplus_le_reg_l with y; left;
    apply Rlt_trans with (1 + y).
  rewrite <- (Rplus_comm y); apply Rplus_lt_compat_l; apply Rlt_0_1.
  replace (y + (exp y - y)) with (exp y); [ apply (exp_ineq1 y H0) | ring ].
  unfold f in |- *; change (continuity (exp - fct_cte y)) in |- *;
    apply continuity_minus;
      [ apply derivable_continuous; apply derivable_exp
        | apply derivable_continuous; apply derivable_const ].
  unfold f in |- *; rewrite exp_0; apply Rplus_le_reg_l with y;
    rewrite Rplus_0_r; replace (y + (1 - y)) with 1; [ apply H | ring ].
Qed.

(**********)
Lemma ln_exists : forall y:R, 0 < y -> { z:R | y = exp z }.
Proof.
  intros; case (Rle_dec 1 y); intro.
  apply (ln_exists1 _ r).
  assert (H0 : 1 <= / y).
  apply Rmult_le_reg_l with y.
  apply H.
  rewrite <- Rinv_r_sym.
  rewrite Rmult_1_r; left; apply (Rnot_le_lt _ _ n).
  red in |- *; intro; rewrite H0 in H; elim (Rlt_irrefl _ H).
  destruct (ln_exists1 _ H0) as (x,p); exists (- x);
    apply Rmult_eq_reg_l with (exp x / y).
  unfold Rdiv in |- *; rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
  rewrite Rmult_1_r; rewrite <- (Rmult_comm (/ y)); rewrite Rmult_assoc;
    rewrite <- exp_plus; rewrite Rplus_opp_r; rewrite exp_0; 
      rewrite Rmult_1_r; symmetry  in |- *; apply p.
  red in |- *; intro H3; rewrite H3 in H; elim (Rlt_irrefl _ H).
  unfold Rdiv in |- *; apply prod_neq_R0.
  assert (H3 := exp_pos x); red in |- *; intro H4; rewrite H4 in H3;
    elim (Rlt_irrefl _ H3).
  apply Rinv_neq_0_compat; red in |- *; intro H3; rewrite H3 in H;
    elim (Rlt_irrefl _ H).
Qed.

(* Definition of log R+* -> R *)
Definition Rln (y:posreal) : R :=
  let (a,_) := ln_exists (pos y) (cond_pos y) in a.

(* Extension on R *)
Definition ln (x:R) : R :=
  match Rlt_dec 0 x with
    | left a => Rln (mkposreal x a)
    | right a => 0
  end.

Lemma exp_ln : forall x:R, 0 < x -> exp (ln x) = x.
Proof.
  intros; unfold ln in |- *; case (Rlt_dec 0 x); intro.
  unfold Rln in |- *;
    case (ln_exists (mkposreal x r) (cond_pos (mkposreal x r))); 
    intros.
  simpl in e; symmetry  in |- *; apply e.
  elim n; apply H.
Qed.

Theorem exp_inv : forall x y:R, exp x = exp y -> x = y.
Proof.
  intros x y H; case (Rtotal_order x y); [ intros H1 | intros [H1| H1] ]; auto;
    assert (H2 := exp_increasing _ _ H1); rewrite H in H2;
      elim (Rlt_irrefl _ H2).
Qed.

Theorem exp_Ropp : forall x:R, exp (- x) = / exp x.
Proof.
  intros x; assert (H : exp x <> 0).
  assert (H := exp_pos x); red in |- *; intro; rewrite H0 in H;
    elim (Rlt_irrefl _ H).
  apply Rmult_eq_reg_l with (r := exp x).
  rewrite <- exp_plus; rewrite Rplus_opp_r; rewrite exp_0.
  apply Rinv_r_sym.
  apply H.
  apply H.
Qed.

(******************************************************************)
(** *                     Properties of  Ln                       *)
(******************************************************************)

Theorem ln_increasing : forall x y:R, 0 < x -> x < y -> ln x < ln y.
Proof.
  intros x y H H0; apply exp_lt_inv.
  repeat rewrite exp_ln. 
  apply H0.
  apply Rlt_trans with x; assumption.
  apply H.
Qed.

Theorem ln_exp : forall x:R, ln (exp x) = x.
Proof.
  intros x; apply exp_inv.
  apply exp_ln.
  apply exp_pos.
Qed.

Theorem ln_1 : ln 1 = 0.
Proof.
  rewrite <- exp_0; rewrite ln_exp; reflexivity.
Qed.

Theorem ln_lt_inv : forall x y:R, 0 < x -> 0 < y -> ln x < ln y -> x < y.
Proof.
  intros x y H H0 H1; rewrite <- (exp_ln x); try rewrite <- (exp_ln y).
  apply exp_increasing; apply H1.
  assumption. 
  assumption.
Qed.

Theorem ln_inv : forall x y:R, 0 < x -> 0 < y -> ln x = ln y -> x = y.
Proof.
  intros x y H H0 H'0; case (Rtotal_order x y); [ intros H1 | intros [H1| H1] ];
    auto.
  assert (H2 := ln_increasing _ _ H H1); rewrite H'0 in H2;
    elim (Rlt_irrefl _ H2).
  assert (H2 := ln_increasing _ _ H0 H1); rewrite H'0 in H2;
    elim (Rlt_irrefl _ H2).
Qed.

Theorem ln_mult : forall x y:R, 0 < x -> 0 < y -> ln (x * y) = ln x + ln y.
Proof.
  intros x y H H0; apply exp_inv.
  rewrite exp_plus.
  repeat rewrite exp_ln.
  reflexivity.
  assumption.
  assumption.
  apply Rmult_lt_0_compat; assumption.
Qed.

Theorem ln_Rinv : forall x:R, 0 < x -> ln (/ x) = - ln x.
Proof.
  intros x H; apply exp_inv; repeat rewrite exp_ln || rewrite exp_Ropp.
  reflexivity.
  assumption. 
  apply Rinv_0_lt_compat; assumption.
Qed.

Theorem ln_continue :
  forall y:R, 0 < y -> continue_in ln (fun x:R => 0 < x) y.
Proof.
  intros y H.
  unfold continue_in, limit1_in, limit_in in |- *; intros eps Heps.
  cut (1 < exp eps); [ intros H1 | idtac ].
  cut (exp (- eps) < 1); [ intros H2 | idtac ].
  exists (Rmin (y * (exp eps - 1)) (y * (1 - exp (- eps)))); split.
  red in |- *; apply P_Rmin.
  apply Rmult_lt_0_compat.
  assumption.
  apply Rplus_lt_reg_r with 1.
  rewrite Rplus_0_r; replace (1 + (exp eps - 1)) with (exp eps);
    [ apply H1 | ring ].
  apply Rmult_lt_0_compat.
  assumption.
  apply Rplus_lt_reg_r with (exp (- eps)).
  rewrite Rplus_0_r; replace (exp (- eps) + (1 - exp (- eps))) with 1;
    [ apply H2 | ring ].
  unfold dist, R_met, R_dist in |- *; simpl in |- *.
  intros x [[H3 H4] H5].
  cut (y * (x * / y) = x).
  intro Hxyy. 
  replace (ln x - ln y) with (ln (x * / y)).
  case (Rtotal_order x y); [ intros Hxy | intros [Hxy| Hxy] ].
  rewrite Rabs_left.
  apply Ropp_lt_cancel; rewrite Ropp_involutive.
  apply exp_lt_inv.
  rewrite exp_ln.
  apply Rmult_lt_reg_l with (r := y).
  apply H.
  rewrite Hxyy.
  apply Ropp_lt_cancel.
  apply Rplus_lt_reg_r with (r := y).
  replace (y + - (y * exp (- eps))) with (y * (1 - exp (- eps)));
  [ idtac | ring ].
  replace (y + - x) with (Rabs (x - y)).
  apply Rlt_le_trans with (1 := H5); apply Rmin_r.
  rewrite Rabs_left; [ ring | idtac ].
  apply (Rlt_minus _ _ Hxy).
  apply Rmult_lt_0_compat; [ apply H3 | apply (Rinv_0_lt_compat _ H) ].
  rewrite <- ln_1.
  apply ln_increasing.
  apply Rmult_lt_0_compat; [ apply H3 | apply (Rinv_0_lt_compat _ H) ].
  apply Rmult_lt_reg_l with (r := y).
  apply H.
  rewrite Hxyy; rewrite Rmult_1_r; apply Hxy.
  rewrite Hxy; rewrite Rinv_r.
  rewrite ln_1; rewrite Rabs_R0; apply Heps.
  red in |- *; intro; rewrite H0 in H; elim (Rlt_irrefl _ H).
  rewrite Rabs_right.
  apply exp_lt_inv.
  rewrite exp_ln.
  apply Rmult_lt_reg_l with (r := y).
  apply H.
  rewrite Hxyy.
  apply Rplus_lt_reg_r with (r := - y).
  replace (- y + y * exp eps) with (y * (exp eps - 1)); [ idtac | ring ].
  replace (- y + x) with (Rabs (x - y)).
  apply Rlt_le_trans with (1 := H5); apply Rmin_l.
  rewrite Rabs_right; [ ring | idtac ].
  left; apply (Rgt_minus _ _ Hxy).
  apply Rmult_lt_0_compat; [ apply H3 | apply (Rinv_0_lt_compat _ H) ].
  rewrite <- ln_1.
  apply Rgt_ge; red in |- *; apply ln_increasing.
  apply Rlt_0_1.
  apply Rmult_lt_reg_l with (r := y).
  apply H.
  rewrite Hxyy; rewrite Rmult_1_r; apply Hxy.
  rewrite ln_mult.
  rewrite ln_Rinv.
  ring.
  assumption.
  assumption.
  apply Rinv_0_lt_compat; assumption.
  rewrite (Rmult_comm x); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym.
  ring.
  red in |- *; intro; rewrite H0 in H; elim (Rlt_irrefl _ H).
  apply Rmult_lt_reg_l with (exp eps).
  apply exp_pos.
  rewrite <- exp_plus; rewrite Rmult_1_r; rewrite Rplus_opp_r; rewrite exp_0;
    apply H1.
  rewrite <- exp_0.
  apply exp_increasing; apply Heps.
Qed.

(******************************************************************)
(** *                     Definition of  Rpower                   *)
(******************************************************************)

Definition Rpower (x y:R) := exp (y * ln x).

Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope.

(******************************************************************)
(** *                     Properties of  Rpower                   *)
(******************************************************************)

(** Note: [Rpower] is prolongated to [1] on negative real numbers and
    it thus does not extend integer power. The next two lemmas, which
    hold for integer power, accidentally hold on negative real numbers
    as a side effect of the default value taken on negative real
    numbers. Contrastingly, the lemmas that do not hold for the
    integer power of a negative number are stated for [Rpower] on the
    positive numbers only (even if they accidentally hold due to the
    default value of [Rpower] on the negative side, as it is the case
    for [Rpower_O]). *)

Theorem Rpower_plus : forall x y z:R, z ^R (x + y) = z ^R x * z ^R y.
Proof.
  intros x y z; unfold Rpower in |- *.
  rewrite Rmult_plus_distr_r; rewrite exp_plus; auto.
Qed.

Theorem Rpower_mult : forall x y z:R, (x ^R y) ^R z = x ^R (y * z).
Proof.
  intros x y z; unfold Rpower in |- *.
  rewrite ln_exp.
  replace (z * (y * ln x)) with (y * z * ln x).
  reflexivity.
  ring.
Qed.

Theorem Rpower_O : forall x:R, 0 < x -> x ^R 0 = 1.
Proof.
  intros x _; unfold Rpower in |- *.
  rewrite Rmult_0_l; apply exp_0.
Qed.

Theorem Rpower_1 : forall x:R, 0 < x -> x ^R 1 = x.
Proof.
  intros x H; unfold Rpower in |- *.
  rewrite Rmult_1_l; apply exp_ln; apply H.
Qed.

Theorem Rpower_pow : forall (n:nat) (x:R), 0 < x -> x ^R INR n = x ^ n.
Proof.
  intros n; elim n; simpl in |- *; auto; fold INR in |- *.
  intros x H; apply Rpower_O; auto.
  intros n1; case n1.
  intros H x H0; simpl in |- *; rewrite Rmult_1_r; apply Rpower_1; auto.
  intros n0 H x H0; rewrite Rpower_plus; rewrite H; try rewrite Rpower_1;
    try apply Rmult_comm || assumption.
Qed.

Theorem Rpower_lt :
  forall x y z:R, 1 < x -> 0 <= y -> y < z -> x ^R y < x ^R z.
Proof.
  intros x y z H H0 H1.
  unfold Rpower in |- *.
  apply exp_increasing.
  apply Rmult_lt_compat_r.
  rewrite <- ln_1; apply ln_increasing.
  apply Rlt_0_1.
  apply H.
  apply H1.
Qed.

Theorem Rpower_sqrt : forall x:R, 0 < x -> x ^R (/ 2) = sqrt x.
Proof.
  intros x H.
  apply ln_inv.
  unfold Rpower in |- *; apply exp_pos.
  apply sqrt_lt_R0; apply H.
  apply Rmult_eq_reg_l with (INR 2).
  apply exp_inv.
  fold Rpower in |- *.
  cut ((x ^R (/ 2)) ^R INR 2 = sqrt x ^R INR 2).
  unfold Rpower in |- *; auto.
  rewrite Rpower_mult.
  rewrite Rinv_l.
  replace 1 with (INR 1); auto.
  repeat rewrite Rpower_pow; simpl in |- *.
  pattern x at 1 in |- *; rewrite <- (sqrt_sqrt x (Rlt_le _ _ H)).
  ring.
  apply sqrt_lt_R0; apply H.
  apply H.
  apply not_O_INR; discriminate.
  apply not_O_INR; discriminate.
Qed.

Theorem Rpower_Ropp : forall x y:R, x ^R (- y) = / x ^R y.
Proof.
  unfold Rpower in |- *.
  intros x y; rewrite Ropp_mult_distr_l_reverse.
  apply exp_Ropp.
Qed.

Theorem Rle_Rpower :
  forall e n m:R, 1 < e -> 0 <= n -> n <= m -> e ^R n <= e ^R m.
Proof.
  intros e n m H H0 H1; case H1.
  intros H2; left; apply Rpower_lt; assumption.
  intros H2; rewrite H2; right; reflexivity.
Qed.

Theorem ln_lt_2 : / 2 < ln 2.
Proof.
  apply Rmult_lt_reg_l with (r := 2).
  prove_sup0.
  rewrite Rinv_r.
  apply exp_lt_inv.
  apply Rle_lt_trans with (1 := exp_le_3).
  change (3 < 2 ^R 2) in |- *.
  repeat rewrite Rpower_plus; repeat rewrite Rpower_1.
  repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l;
    repeat rewrite Rmult_1_l.
  pattern 3 at 1 in |- *; rewrite <- Rplus_0_r; replace (2 + 2) with (3 + 1);
    [ apply Rplus_lt_compat_l; apply Rlt_0_1 | ring ].
  prove_sup0.
  discrR.
Qed.

(*****************************************)
(** * Differentiability of Ln and Rpower *)
(*****************************************)

Theorem limit1_ext :
  forall (f g:R -> R) (D:R -> Prop) (l x:R),
    (forall x:R, D x -> f x = g x) -> limit1_in f D l x -> limit1_in g D l x.
Proof.
  intros f g D l x H; unfold limit1_in, limit_in in |- *.
  intros H0 eps H1; case (H0 eps); auto.
  intros x0 [H2 H3]; exists x0; split; auto.
  intros x1 [H4 H5]; rewrite <- H; auto.
Qed.

Theorem limit1_imp :
  forall (f:R -> R) (D D1:R -> Prop) (l x:R),
    (forall x:R, D1 x -> D x) -> limit1_in f D l x -> limit1_in f D1 l x.
Proof.
  intros f D D1 l x H; unfold limit1_in, limit_in in |- *.
  intros H0 eps H1; case (H0 eps H1); auto.
  intros alpha [H2 H3]; exists alpha; split; auto.
  intros d [H4 H5]; apply H3; split; auto.
Qed.

Theorem Rinv_Rdiv : forall x y:R, x <> 0 -> y <> 0 -> / (x / y) = y / x.
Proof.
  intros x y H1 H2; unfold Rdiv in |- *; rewrite Rinv_mult_distr.
  rewrite Rinv_involutive.
  apply Rmult_comm.
  assumption.
  assumption.
  apply Rinv_neq_0_compat; assumption.
Qed.

Theorem Dln : forall y:R, 0 < y -> D_in ln Rinv (fun x:R => 0 < x) y.
Proof.
  intros y Hy; unfold D_in in |- *.
  apply limit1_ext with
    (f := fun x:R => / ((exp (ln x) - exp (ln y)) / (ln x - ln y))).
  intros x [HD1 HD2]; repeat rewrite exp_ln.
  unfold Rdiv in |- *; rewrite Rinv_mult_distr.
  rewrite Rinv_involutive.
  apply Rmult_comm.
  apply Rminus_eq_contra.
  red in |- *; intros H2; case HD2.
  symmetry  in |- *; apply (ln_inv _ _ HD1 Hy H2).
  apply Rminus_eq_contra; apply (sym_not_eq HD2).
  apply Rinv_neq_0_compat; apply Rminus_eq_contra; red in |- *; intros H2;
    case HD2; apply ln_inv; auto.
  assumption.
  assumption.
  apply limit_inv with
    (f := fun x:R => (exp (ln x) - exp (ln y)) / (ln x - ln y)).
  apply limit1_imp with
    (f := fun x:R => (fun x:R => (exp x - exp (ln y)) / (x - ln y)) (ln x))
    (D := Dgf (D_x (fun x:R => 0 < x) y) (D_x (fun x:R => True) (ln y)) ln).
  intros x [H1 H2]; split.
  split; auto.
  split; auto.
  red in |- *; intros H3; case H2; apply ln_inv; auto.
  apply limit_comp with
    (l := ln y) (g := fun x:R => (exp x - exp (ln y)) / (x - ln y)) (f := ln).
  apply ln_continue; auto.
  assert (H0 := derivable_pt_lim_exp (ln y)); unfold derivable_pt_lim in H0;
    unfold limit1_in in |- *; unfold limit_in in |- *; 
      simpl in |- *; unfold R_dist in |- *; intros; elim (H0 _ H); 
        intros; exists (pos x); split.
  apply (cond_pos x).
  intros; pattern y at 3 in |- *; rewrite <- exp_ln.
  pattern x0 at 1 in |- *; replace x0 with (ln y + (x0 - ln y));
    [ idtac | ring ].
  apply H1.
  elim H2; intros H3 _; unfold D_x in H3; elim H3; clear H3; intros _ H3;
    apply Rminus_eq_contra; apply (sym_not_eq (A:=R)); 
      apply H3.
  elim H2; clear H2; intros _ H2; apply H2.
  assumption.
  red in |- *; intro; rewrite H in Hy; elim (Rlt_irrefl _ Hy).
Qed.

Lemma derivable_pt_lim_ln : forall x:R, 0 < x -> derivable_pt_lim ln x (/ x).
Proof.
  intros; assert (H0 := Dln x H); unfold D_in in H0; unfold limit1_in in H0;
    unfold limit_in in H0; simpl in H0; unfold R_dist in H0;
      unfold derivable_pt_lim in |- *; intros; elim (H0 _ H1); 
        intros; elim H2; clear H2; intros; set (alp := Rmin x0 (x / 2));
          assert (H4 : 0 < alp).
  unfold alp in |- *; unfold Rmin in |- *; case (Rle_dec x0 (x / 2)); intro.
  apply H2.
  unfold Rdiv in |- *; apply Rmult_lt_0_compat;
    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
  exists (mkposreal _ H4); intros; pattern h at 2 in |- *;
    replace h with (x + h - x); [ idtac | ring ].
  apply H3; split.
  unfold D_x in |- *; split.
  case (Rcase_abs h); intro.
  assert (H7 : Rabs h < x / 2).
  apply Rlt_le_trans with alp.
  apply H6.
  unfold alp in |- *; apply Rmin_r.
  apply Rlt_trans with (x / 2).
  unfold Rdiv in |- *; apply Rmult_lt_0_compat;
    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
  rewrite Rabs_left in H7.
  apply Rplus_lt_reg_r with (- h - x / 2).
  replace (- h - x / 2 + x / 2) with (- h); [ idtac | ring ].
  pattern x at 2 in |- *; rewrite double_var.
  replace (- h - x / 2 + (x / 2 + x / 2 + h)) with (x / 2); [ apply H7 | ring ].
  apply r.
  apply Rplus_lt_le_0_compat; [ assumption | apply Rge_le; apply r ].
  apply (sym_not_eq (A:=R)); apply Rminus_not_eq; replace (x + h - x) with h;
    [ apply H5 | ring ].
  replace (x + h - x) with h;
  [ apply Rlt_le_trans with alp;
    [ apply H6 | unfold alp in |- *; apply Rmin_l ]
    | ring ].
Qed.

Theorem D_in_imp :
  forall (f g:R -> R) (D D1:R -> Prop) (x:R),
    (forall x:R, D1 x -> D x) -> D_in f g D x -> D_in f g D1 x.
Proof.
  intros f g D D1 x H; unfold D_in in |- *.
  intros H0; apply limit1_imp with (D := D_x D x); auto.
  intros x1 [H1 H2]; split; auto.
Qed.

Theorem D_in_ext :
  forall (f g h:R -> R) (D:R -> Prop) (x:R),
    f x = g x -> D_in h f D x -> D_in h g D x.
Proof.
  intros f g h D x H; unfold D_in in |- *.
  rewrite H; auto.
Qed.

Theorem Dpower :
  forall y z:R,
    0 < y ->
    D_in (fun x:R => x ^R z) (fun x:R => z * x ^R (z - 1)) (
      fun x:R => 0 < x) y.
Proof.
  intros y z H;
    apply D_in_imp with (D := Dgf (fun x:R => 0 < x) (fun x:R => True) ln).
  intros x H0; repeat split.
  assumption.
  apply D_in_ext with (f := fun x:R => / x * (z * exp (z * ln x))).
  unfold Rminus in |- *; rewrite Rpower_plus; rewrite Rpower_Ropp;
    rewrite (Rpower_1 _ H); unfold Rpower; ring.
  apply Dcomp with
    (f := ln)
    (g := fun x:R => exp (z * x))
    (df := Rinv)
    (dg := fun x:R => z * exp (z * x)).
  apply (Dln _ H).
  apply D_in_imp with
    (D := Dgf (fun x:R => True) (fun x:R => True) (fun x:R => z * x)).
  intros x H1; repeat split; auto.
  apply
    (Dcomp (fun _:R => True) (fun _:R => True) (fun x => z) exp
      (fun x:R => z * x) exp); simpl in |- *.
  apply D_in_ext with (f := fun x:R => z * 1).
  apply Rmult_1_r.
  apply (Dmult_const (fun x => True) (fun x => x) (fun x => 1)); apply Dx.
  assert (H0 := derivable_pt_lim_D_in exp exp (z * ln y)); elim H0; clear H0;
    intros _ H0; apply H0; apply derivable_pt_lim_exp.
Qed.

Theorem derivable_pt_lim_power :
  forall x y:R,
    0 < x -> derivable_pt_lim (fun x => x ^R y) x (y * x ^R (y - 1)).
Proof.
  intros x y H.
  unfold Rminus in |- *; rewrite Rpower_plus.
  rewrite Rpower_Ropp.
  rewrite Rpower_1; auto.
  rewrite <- Rmult_assoc.
  unfold Rpower in |- *.
  apply derivable_pt_lim_comp with (f1 := ln) (f2 := fun x => exp (y * x)).
  apply derivable_pt_lim_ln; assumption.
  rewrite (Rmult_comm y).
  apply derivable_pt_lim_comp with (f1 := fun x => y * x) (f2 := exp).
  pattern y at 2 in |- *; replace y with (0 * ln x + y * 1).
  apply derivable_pt_lim_mult with (f1 := fun x:R => y) (f2 := fun x:R => x).
  apply derivable_pt_lim_const with (a := y).
  apply derivable_pt_lim_id.
  ring.
  apply derivable_pt_lim_exp.
Qed.