Library Coq.Reals.Rpower
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).
Lemma exp_le_3 : exp 1 <= 3.
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.
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 Rpower (x y:R) := exp (y * ln x).
Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope.
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.
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)).