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 Sqrt_reg.
Require Import MVT.
Require Import Ranalysis4.
Require Import Lra.
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


Lemma exp_neq_0 : forall x:R, exp x <> 0.

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.

Definition Rlog x y := (ln y)/(ln x).

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.

Lemma ln_neq_0 : forall x:R, x <> 1 -> 0 < x -> ln x <> 0.

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

Lemma ln_pow : forall (x : R), 0 < x -> forall (n : nat), ln (x^n) = (INR n)*(ln x).

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

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, Rpower z (x + y) = Rpower z x * Rpower z y.

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

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

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

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

Lemma Rpower_nonzero : forall (x : R) (n : nat), 0 < x -> Rpower x (INR n) <> 0.

Theorem Rpower_lt :
  forall x y z:R, 1 < x -> y < z -> Rpower x y < Rpower x z.

Lemma Rpower_Rlog : forall x y:R, x <> 1 -> 0 < x -> 0 < y -> Rpower x (Rlog x y) = y.

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

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

Lemma powerRZ_Rpower x z : (0 < x)%R -> powerRZ x z = Rpower x (IZR z).

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

Lemma ln_Rpower : forall x y:R, ln (Rpower x y) = y * ln x.

Lemma Rlog_pow : forall (x : R) (n : nat), x <> 1 -> 0 < x -> Rlog x (x^n) = INR n.

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 => Rpower x z) (fun x:R => z * Rpower x (z - 1)) (
      fun x:R => 0 < x) y.

Theorem derivable_pt_lim_power :
  forall x y:R,
    0 < x -> derivable_pt_lim (fun x => Rpower x y) x (y * Rpower x (y - 1)).


Lemma Rpower_mult_distr :
  forall x y z, 0 < x -> 0 < y ->
   Rpower x z * Rpower y z = Rpower (x * y) z.

Lemma Rlt_Rpower_l a b c: 0 < c -> 0 < a < b -> Rpower a c < Rpower b c.

Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> Rpower a c <= Rpower b c.


Definition arcsinh x := ln (x + sqrt (x ^ 2 + 1)).

Lemma arcsinh_sinh : forall x, arcsinh (sinh x) = x.

Lemma sinh_arcsinh x : sinh (arcsinh x) = x.

Lemma derivable_pt_lim_arcsinh :
  forall x, derivable_pt_lim arcsinh x (/sqrt (x ^ 2 + 1)).

Lemma arcsinh_lt : forall x y, x < y -> arcsinh x < arcsinh y.

Lemma arcsinh_le : forall x y, x <= y -> arcsinh x <= arcsinh y.

Lemma arcsinh_0 : arcsinh 0 = 0.