Library Stdlib.Reals.Rpower
From Stdlib Require Import Rbase.
From Stdlib Require Import Rfunctions.
From Stdlib Require Import SeqSeries.
From Stdlib Require Import Rtrigo1.
From Stdlib Require Import Ranalysis1.
From Stdlib Require Import Exp_prop.
From Stdlib Require Import Rsqrt_def.
From Stdlib Require Import R_sqrt.
From Stdlib Require Import Sqrt_reg.
From Stdlib Require Import MVT.
From Stdlib Require Import Ranalysis4.
From Stdlib Require Import Lra.
From Stdlib Require Import Arith.Factorial.
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.