path: root/theories/Reals/Rpower.v

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*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 Rtrigo1.
Require Import Ranalysis1.
Require Import Exp_prop.
Require Import Rsqrt_def.
Require Import R_sqrt.
Require Import MVT.
Require Import Ranalysis4.
Local Open 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; 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; 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; case (exist_exp (-1)); intros; simpl;
    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; 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; unfold Un_cv in H0;
    intros; elim (H0 _ H1); intros; exists x0; intros;
      unfold R_dist in H2; unfold R_dist;
        replace (/ INR (fact n)) with (1 ^ n / INR (fact n)).
  apply (H2 _ H3).
  unfold Rdiv; rewrite pow1; rewrite Rmult_1_l; reflexivity.
  unfold infinite_sum in e; unfold Un_cv, tg_alt; 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 ; 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_l 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; 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 ; 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; rewrite <- (Rmult_0_r (f y));
    rewrite (Rmult_comm (f 0)); apply Rmult_le_compat_l;
      assumption.
  unfold f; 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; change (continuity (exp - fct_cte y));
    apply continuity_minus;
      [ apply derivable_continuous; apply derivable_exp
        | apply derivable_continuous; apply derivable_const ].
  unfold f; 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; 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; 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 ; apply p.
  red; intro H3; rewrite H3 in H; elim (Rlt_irrefl _ H).
  unfold Rdiv; apply prod_neq_R0.
  assert (H3 := exp_pos x); red; intro H4; rewrite H4 in H3;
    elim (Rlt_irrefl _ H3).
  apply Rinv_neq_0_compat; red; 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; case (Rlt_dec 0 x); intro.
  unfold Rln;
    case (ln_exists (mkposreal x r) (cond_pos (mkposreal x r)));
    intros.
  simpl in e; symmetry ; 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; 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; 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; apply P_Rmin.
  apply Rmult_lt_0_compat.
  assumption.
  apply Rplus_lt_reg_l 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_l with (exp (- eps)).
  rewrite Rplus_0_r; replace (exp (- eps) + (1 - exp (- eps))) with 1;
    [ apply H2 | ring ].
  unfold dist, R_met, R_dist; simpl.
  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_l 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; 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_l 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; 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; 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).

Local Infix "^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.
  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.
  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.
  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.
  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; auto; fold INR.
  intros x H; apply Rpower_O; auto.
  intros n1; case n1.
  intros H x H0; simpl; 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.
  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; apply exp_pos.
  apply sqrt_lt_R0; apply H.
  apply Rmult_eq_reg_l with (INR 2).
  apply exp_inv.
  fold Rpower.
  cut ((x ^R (/ INR 2)) ^R INR 2 = sqrt x ^R INR 2).
  unfold Rpower; auto.
  rewrite Rpower_mult.
  rewrite Rinv_l.
  replace 1 with (INR 1); auto.
  repeat rewrite Rpower_pow; simpl.
  pattern x at 1; 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.
  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).
  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; 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.
  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.
  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; 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.
  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; rewrite Rinv_mult_distr.
  rewrite Rinv_involutive.
  apply Rmult_comm.
  apply Rminus_eq_contra.
  red; intros H2; case HD2.
  symmetry ; apply (ln_inv _ _ HD1 Hy H2).
  apply Rminus_eq_contra; apply (not_eq_sym HD2).
  apply Rinv_neq_0_compat; apply Rminus_eq_contra; red; 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; 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; unfold limit_in;
      simpl; unfold R_dist; intros; elim (H0 _ H);
        intros; exists (pos x); split.
  apply (cond_pos x).
  intros; pattern y at 3; rewrite <- exp_ln.
  pattern x0 at 1; 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 (not_eq_sym (A:=R));
      apply H3.
  elim H2; clear H2; intros _ H2; apply H2.
  assumption.
  red; 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; intros; elim (H0 _ H1);
        intros; elim H2; clear H2; intros; set (alp := Rmin x0 (x / 2));
          assert (H4 : 0 < alp).
  unfold alp; unfold Rmin; case (Rle_dec x0 (x / 2)); intro.
  apply H2.
  unfold Rdiv; apply Rmult_lt_0_compat;
    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
  exists (mkposreal _ H4); intros; pattern h at 2;
    replace h with (x + h - x); [ idtac | ring ].
  apply H3; split.
  unfold D_x; split.
  case (Rcase_abs h); intro.
  assert (H7 : Rabs h < x / 2).
  apply Rlt_le_trans with alp.
  apply H6.
  unfold alp; apply Rmin_r.
  apply Rlt_trans with (x / 2).
  unfold Rdiv; apply Rmult_lt_0_compat;
    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
  rewrite Rabs_left in H7.
  apply Rplus_lt_reg_l with (- h - x / 2).
  replace (- h - x / 2 + x / 2) with (- h); [ idtac | ring ].
  pattern x at 2; 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 (not_eq_sym (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; 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.
  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.
  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; 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.
  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; rewrite Rpower_plus.
  rewrite Rpower_Ropp.
  rewrite Rpower_1; auto.
  rewrite <- Rmult_assoc.
  unfold Rpower.
  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; 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.