Library Coq.Reals.Rpower




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).

Lemma exp_le_3 : exp 1 <= 3.

Properties of Exp


Theorem exp_increasing : forall x y:R, x < y -> exp x < exp y.

Theorem exp_lt_inv : forall x y:R, exp x < exp y -> x < y.

Lemma exp_ineq1 : forall x:R, 0 < x -> 1 + x < exp x.

Lemma ln_exists1 : forall y:R, 1 <= y -> { z:R | y = exp z }.

Lemma ln_exists : forall y:R, 0 < y -> { z:R | y = exp z }.

Definition Rln (y:posreal) : R :=
  let (a,_) := ln_exists (pos y) (cond_pos y) in a.

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.

Theorem exp_inv : forall x y:R, exp x = exp y -> x = y.

Theorem exp_Ropp : forall x:R, exp (- x) = / exp x.

Properties of Ln


Theorem ln_increasing : forall x y:R, 0 < x -> x < y -> ln x < ln y.

Theorem ln_exp : forall x:R, ln (exp x) = x.

Theorem ln_1 : ln 1 = 0.

Theorem ln_lt_inv : forall x y:R, 0 < x -> 0 < y -> ln x < ln y -> x < y.

Theorem ln_inv : forall x y:R, 0 < x -> 0 < y -> ln x = ln y -> x = y.

Theorem ln_mult : forall x y:R, 0 < x -> 0 < y -> ln (x * y) = ln x + ln y.

Theorem ln_Rinv : forall x:R, 0 < x -> ln (/ x) = - ln x.

Theorem ln_continue :
  forall y:R, 0 < y -> continue_in ln (fun x:R => 0 < x) y.

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.

Theorem Rpower_mult : forall x y z:R, (x ^R y) ^R z = x ^R (y * z).

Theorem Rpower_O : forall x:R, 0 < x -> x ^R 0 = 1.

Theorem Rpower_1 : forall x:R, 0 < x -> x ^R 1 = x.

Theorem Rpower_pow : forall (n:nat) (x:R), 0 < x -> x ^R INR n = x ^ n.

Theorem Rpower_lt :
  forall x y z:R, 1 < x -> 0 <= y -> y < z -> x ^R y < x ^R z.

Theorem Rpower_sqrt : forall x:R, 0 < x -> x ^R (/ 2) = sqrt x.

Theorem Rpower_Ropp : forall x y:R, x ^R (- y) = / x ^R y.

Theorem Rle_Rpower :
  forall e n m:R, 1 < e -> 0 <= n -> n <= m -> e ^R n <= e ^R m.

Theorem ln_lt_2 : / 2 < ln 2.

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.

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.

Theorem Rinv_Rdiv : forall x y:R, x <> 0 -> y <> 0 -> / (x / y) = y / x.

Theorem Dln : forall y:R, 0 < y -> D_in ln Rinv (fun x:R => 0 < x) y.

Lemma derivable_pt_lim_ln : forall x:R, 0 < x -> derivable_pt_lim ln x (/ x).

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.

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.

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.

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)).