Library Stdlib.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.
Definition P_Rmin_stt (P:R -> Prop) x y := Rmin_case x y P.
#[deprecated(since="8.16", note="Use Rmin_case instead.")]
Notation P_Rmin := P_Rmin_stt.
Lemma exp_le_3 : exp 1 <= 3.
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, x <> 0 -> 1 + x < exp x.
Lemma exp_ineq1_le (x : R) : 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.
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.
Properties of Rpower
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.
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_depr : forall x y:R, x <> 0 -> y <> 0 -> / (x / y) = y / x.
#[deprecated(since="8.16",note="Use Rinv_div.")]
Notation Rinv_Rdiv := Rinv_Rdiv_depr.
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.