--- a/src/HOL/NthRoot.thy Wed Jul 03 21:54:17 2024 +0200
+++ b/src/HOL/NthRoot.thy Fri Jul 05 21:58:40 2024 +0100
@@ -166,10 +166,10 @@
by (simp add: odd_pos sgn_real_def power_0_left split: if_split_asm)
lemma real_root_pos_unique: "0 < n \<Longrightarrow> 0 \<le> y \<Longrightarrow> y ^ n = x \<Longrightarrow> root n x = y"
- using root_sgn_power[of n y] by (auto simp add: le_less power_0_left)
+ using real_root_power_cancel by blast
lemma odd_real_root_unique: "odd n \<Longrightarrow> y ^ n = x \<Longrightarrow> root n x = y"
- by (erule subst, rule odd_real_root_power_cancel)
+ using odd_real_root_power_cancel by blast
lemma real_root_one [simp]: "0 < n \<Longrightarrow> root n 1 = 1"
by (simp add: real_root_pos_unique)
--- a/src/HOL/Transcendental.thy Wed Jul 03 21:54:17 2024 +0200
+++ b/src/HOL/Transcendental.thy Fri Jul 05 21:58:40 2024 +0100
@@ -1561,28 +1561,55 @@
lemma powr_0 [simp]: "0 powr z = 0"
by (simp add: powr_def)
-
+text \<open>We totalise @{term ln} over all reals exactly as done in Mathlib\<close>
instantiation real :: ln
begin
+definition raw_ln_real :: "real \<Rightarrow> real"
+ where "raw_ln_real x \<equiv> (THE u. exp u = x)"
+
definition ln_real :: "real \<Rightarrow> real"
- where "ln_real x = (THE u. exp u = x)"
+ where "ln_real \<equiv> \<lambda>x. if x=0 then 0 else raw_ln_real \<bar>x\<bar>"
instance
- by intro_classes (simp add: ln_real_def)
+ by intro_classes (simp add: ln_real_def raw_ln_real_def)
end
lemma powr_eq_0_iff [simp]: "w powr z = 0 \<longleftrightarrow> w = 0"
by (simp add: powr_def)
+lemma raw_ln_exp [simp]: "raw_ln_real (exp x) = x"
+ by (simp add: raw_ln_real_def)
+
+lemma exp_raw_ln [simp]: "0 < x \<Longrightarrow> exp (raw_ln_real x) = x"
+ by (auto dest: exp_total)
+
+lemma raw_ln_unique: "exp y = x \<Longrightarrow> raw_ln_real x = y"
+ by auto
+
+lemma abs_raw_ln: "x \<noteq> 0 \<Longrightarrow> raw_ln_real\<bar>x\<bar> = ln x"
+ by (simp add: ln_real_def)
+
+lemma ln_0 [simp]: "ln (0::real) = 0"
+ by (simp add: ln_real_def)
+
+lemma ln_minus [simp]: "ln (-x) = ln x"
+ for x :: real
+ by (simp add: ln_real_def)
+
lemma ln_exp [simp]: "ln (exp x) = x"
for x :: real
by (simp add: ln_real_def)
+lemma exp_ln_abs:
+ fixes x::real
+ shows "x \<noteq> 0 \<Longrightarrow> exp (ln x) = \<bar>x\<bar>"
+ by (simp add: ln_real_def)
+
lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x"
for x :: real
- by (auto dest: exp_total)
+ using exp_ln_abs by fastforce
lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x"
for x :: real
@@ -1590,26 +1617,40 @@
lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y"
for x :: real
- by (erule subst) (rule ln_exp)
-
-lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
+ by auto
+
+lemma ln_unique': "exp y = \<bar>x\<bar> \<Longrightarrow> ln x = y"
for x :: real
- by (rule ln_unique) (simp add: exp_add)
-
-lemma ln_prod: "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i > 0) \<Longrightarrow> ln (prod f I) = sum (\<lambda>x. ln(f x)) I"
+ by (metis abs_raw_ln abs_zero exp_not_eq_zero raw_ln_exp)
+
+lemma raw_ln_mult: "x>0 \<Longrightarrow> y>0 \<Longrightarrow> raw_ln_real (x * y) = raw_ln_real x + raw_ln_real y"
+ by (metis exp_add exp_ln raw_ln_exp)
+
+lemma ln_mult: "(x\<noteq>0 \<longleftrightarrow> y\<noteq>0) \<Longrightarrow> ln (x * y) = ln x + ln y"
+ for x :: real
+ by (simp add: ln_real_def abs_mult raw_ln_mult)
+
+lemma ln_prod: "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<noteq> 0) \<Longrightarrow> ln (prod f I) = sum (\<lambda>x. ln(f x)) I"
for f :: "'a \<Rightarrow> real"
by (induct I rule: finite_induct) (auto simp: ln_mult prod_pos)
-lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
+lemma ln_inverse: "ln (inverse x) = - ln x"
+ for x :: real
+ by (smt (verit) inverse_nonzero_iff_nonzero ln_mult ln_one ln_real_def right_inverse)
+
+lemma ln_div: "(x\<noteq>0 \<longleftrightarrow> y\<noteq>0) \<Longrightarrow> ln (x/y) = ln x - ln y"
for x :: real
- by (rule ln_unique) (simp add: exp_minus)
-
-lemma ln_div: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
- for x :: real
- by (rule ln_unique) (simp add: exp_diff)
-
-lemma ln_realpow: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
- by (rule ln_unique) (simp add: exp_of_nat_mult)
+ by (simp add: divide_inverse ln_inverse ln_mult)
+
+lemma ln_realpow: "ln (x^n) = real n * ln x"
+proof (cases "x=0")
+ case True
+ then show ?thesis by (auto simp: power_0_left)
+next
+ case False
+ then show ?thesis
+ by (induction n) (auto simp: ln_mult distrib_right)
+qed
lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
for x :: real
@@ -1677,32 +1718,36 @@
for x :: real
by simp
-lemma ln_neg_is_const: "x \<le> 0 \<Longrightarrow> ln x = (THE x. False)"
+lemma ln_neg: "ln (-x) = ln x"
for x :: real
- by (auto simp: ln_real_def intro!: arg_cong[where f = The])
+ by simp
lemma powr_eq_one_iff [simp]:
"a powr x = 1 \<longleftrightarrow> x = 0" if "a > 1" for a x :: real
using that by (auto simp: powr_def split: if_splits)
+text \<open>A consequence of our "totalising" of ln\<close>
+lemma uminus_powr_eq: "(-a) powr x = a powr x" for x::real
+ by (simp add: powr_def)
+
+lemma isCont_ln_pos:
+ fixes x :: real
+ assumes "x > 0"
+ shows "isCont ln x"
+ by (metis assms exp_ln isCont_exp isCont_inverse_function ln_exp)
+
lemma isCont_ln:
fixes x :: real
assumes "x \<noteq> 0"
shows "isCont ln x"
proof (cases "0 < x")
- case True
- then have "isCont ln (exp (ln x))"
- by (intro isCont_inverse_function[where d = "\<bar>x\<bar>" and f = exp]) auto
- with True show ?thesis
- by simp
-next
case False
- with \<open>x \<noteq> 0\<close> show "isCont ln x"
- unfolding isCont_def
- by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\<lambda>_. ln 0"])
- (auto simp: ln_neg_is_const not_less eventually_at dist_real_def
- intro!: exI[of _ "\<bar>x\<bar>"])
-qed
+ then have "isCont (ln o uminus) x"
+ using isCont_minus [OF continuous_ident] assms continuous_at_compose isCont_ln_pos
+ by force
+ then show ?thesis
+ using isCont_cong by force
+qed (simp add: isCont_ln_pos)
lemma tendsto_ln [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) \<longlongrightarrow> ln a) F"
for a :: real
@@ -2042,7 +2087,7 @@
have "x * ln y - x * ln x = x * (ln y - ln x)"
by (simp add: algebra_simps)
also have "\<dots> = x * ln (y / x)"
- by (simp only: ln_div a b)
+ using a b ln_div by force
also have "y / x = (x + (y - x)) / x"
by simp
also have "\<dots> = 1 + (y - x) / x"
@@ -2279,37 +2324,32 @@
where "log a x = ln x / ln a"
lemma tendsto_log [tendsto_intros]:
- "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < b \<Longrightarrow>
+ "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> b\<noteq>0 \<Longrightarrow>
((\<lambda>x. log (f x) (g x)) \<longlongrightarrow> log a b) F"
unfolding log_def by (intro tendsto_intros) auto
lemma continuous_log:
assumes "continuous F f"
and "continuous F g"
- and "0 < f (Lim F (\<lambda>x. x))"
+ and "f (Lim F (\<lambda>x. x)) > 0"
and "f (Lim F (\<lambda>x. x)) \<noteq> 1"
- and "0 < g (Lim F (\<lambda>x. x))"
+ and "g (Lim F (\<lambda>x. x)) \<noteq> 0"
shows "continuous F (\<lambda>x. log (f x) (g x))"
- using assms unfolding continuous_def by (rule tendsto_log)
+ using assms by (simp add: continuous_def tendsto_log)
lemma continuous_at_within_log[continuous_intros]:
assumes "continuous (at a within s) f"
and "continuous (at a within s) g"
and "0 < f a"
and "f a \<noteq> 1"
- and "0 < g a"
+ and "g a \<noteq> 0"
shows "continuous (at a within s) (\<lambda>x. log (f x) (g x))"
using assms unfolding continuous_within by (rule tendsto_log)
-lemma isCont_log[continuous_intros, simp]:
- assumes "isCont f a" "isCont g a" "0 < f a" "f a \<noteq> 1" "0 < g a"
- shows "isCont (\<lambda>x. log (f x) (g x)) a"
- using assms unfolding continuous_at by (rule tendsto_log)
-
lemma continuous_on_log[continuous_intros]:
- assumes "continuous_on s f" "continuous_on s g"
- and "\<forall>x\<in>s. 0 < f x" "\<forall>x\<in>s. f x \<noteq> 1" "\<forall>x\<in>s. 0 < g x"
- shows "continuous_on s (\<lambda>x. log (f x) (g x))"
+ assumes "continuous_on S f" "continuous_on S g"
+ and "\<forall>x\<in>S. 0 < f x" "\<forall>x\<in>S. f x \<noteq> 1" "\<forall>x\<in>S. g x \<noteq> 0"
+ shows "continuous_on S (\<lambda>x. log (f x) (g x))"
using assms unfolding continuous_on_def by (fast intro: tendsto_log)
lemma exp_powr_real:
@@ -2328,31 +2368,30 @@
declare powr_one_gt_zero_iff [THEN iffD2, simp]
lemma powr_diff:
- fixes w:: "'a::{ln,real_normed_field}" shows "w powr (z1 - z2) = w powr z1 / w powr z2"
+ fixes w:: "'a::{ln,real_normed_field}"
+ shows "w powr (z1 - z2) = w powr z1 / w powr z2"
by (simp add: powr_def algebra_simps exp_diff)
-lemma powr_mult: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> (x * y) powr a = (x powr a) * (y powr a)"
+lemma powr_mult: "(x * y) powr a = (x powr a) * (y powr a)"
for a x y :: real
by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
lemma prod_powr_distrib:
fixes x :: "'a \<Rightarrow> real"
- assumes "\<And>i. i\<in>I \<Longrightarrow> x i \<ge> 0"
shows "(prod x I) powr r = (\<Prod>i\<in>I. x i powr r)"
- using assms
by (induction I rule: infinite_finite_induct) (auto simp add: powr_mult prod_nonneg)
lemma powr_ge_pzero [simp]: "0 \<le> x powr y"
for x y :: real
by (simp add: powr_def)
-lemma powr_non_neg[simp]: "\<not>a powr x < 0" for a x::real
+lemma powr_non_neg[simp]: "\<not> a powr x < 0" for a x::real
using powr_ge_pzero[of a x] by arith
-lemma inverse_powr: "\<And>y::real. 0 \<le> y \<Longrightarrow> inverse y powr a = inverse (y powr a)"
+lemma inverse_powr: "\<And>y::real. inverse y powr a = inverse (y powr a)"
by (simp add: exp_minus ln_inverse powr_def)
-lemma powr_divide: "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
+lemma powr_divide: "(x / y) powr a = (x powr a) / (y powr a)"
for a b x :: real
by (simp add: divide_inverse powr_mult inverse_powr)
@@ -2364,13 +2403,17 @@
for x :: real
by (auto simp: powr_add)
+lemma powr_mult_base': "abs x * x powr y = x powr (1 + y)"
+ for x :: real
+ by (smt (verit) powr_mult_base uminus_powr_eq)
+
lemma powr_powr: "(x powr a) powr b = x powr (a * b)"
for a b x :: real
by (simp add: powr_def)
lemma powr_power:
fixes z:: "'a::{real_normed_field,ln}"
- shows "z \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> (z powr u) ^ n = z powr (of_nat n * u)"
+ shows "z \<noteq> 0 \<Longrightarrow> (z powr u) ^ n = z powr (of_nat n * u)"
by (induction n) (auto simp: algebra_simps powr_add)
lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a"
@@ -2385,8 +2428,17 @@
for a x :: "'a::{ln,real_normed_field}"
by (simp add: divide_inverse powr_minus)
-lemma powr_sum: "x \<noteq> 0 \<Longrightarrow> finite A \<Longrightarrow> x powr sum f A = (\<Prod>y\<in>A. x powr f y)"
- by (simp add: powr_def exp_sum sum_distrib_right)
+lemma powr_sum:
+ assumes "x \<noteq> 0"
+ shows "x powr sum f A = (\<Prod>y\<in>A. x powr f y)"
+proof (cases "finite A")
+ case True
+ with assms show ?thesis
+ by (simp add: powr_def exp_sum sum_distrib_right)
+next
+ case False
+ with assms show ?thesis by auto
+qed
lemma divide_powr_uminus: "a / b powr c = a * b powr (- c)"
for a b c :: real
@@ -2427,7 +2479,7 @@
fixes x::real shows "1 - x < exp (-x) \<longleftrightarrow> x \<noteq> 0"
by (smt (verit) exp_minus_ge exp_eq_one_iff exp_gt_zero ln_eq_minus_one ln_exp)
-lemma log_ln: "ln x = log (exp(1)) x"
+lemma log_ln: "ln x = log (exp 1) x"
by (simp add: log_def)
lemma DERIV_log:
@@ -2454,7 +2506,7 @@
by auto
lemma log_mult:
- "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a (x * y) = log a x + log a y"
+ "(x\<noteq>0 \<longleftrightarrow> y\<noteq>0) \<Longrightarrow> log a (x * y) = log a x + log a y"
by (simp add: log_def ln_mult divide_inverse distrib_right)
lemma log_eq_div_ln_mult_log:
@@ -2488,12 +2540,14 @@
for a x::real
by (meson not_less powr_gt_zero)
-lemma log_add_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log b x + y = log b (x * b powr y)"
- and add_log_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> y + log b x = log b (b powr y * x)"
- and log_minus_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log b x - y = log b (x * b powr -y)"
- and minus_log_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> y - log b x = log b (b powr y / x)"
+lemma log_add_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> x\<noteq>0 \<Longrightarrow> log b x + y = log b (x * b powr y)"
+ and add_log_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> x\<noteq>0 \<Longrightarrow> y + log b x = log b (b powr y * x)"
+ and log_minus_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> x\<noteq>0 \<Longrightarrow> log b x - y = log b (x * b powr -y)"
by (simp_all add: log_mult log_divide)
+lemma minus_log_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> x\<noteq>0 \<Longrightarrow> y - log b x = log b (b powr y / x)"
+ by (simp add: diff_divide_eq_iff ln_div log_def powr_def)
+
lemma log_less_cancel_iff [simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a x < log a y \<longleftrightarrow> x < y"
using powr_less_cancel_iff [of a] powr_log_cancel [of a x] powr_log_cancel [of a y]
by (metis less_eq_real_def less_trans not_le zero_less_one)
@@ -2611,11 +2665,11 @@
qed
lemma less_log2_of_power: "2 ^ n < m \<Longrightarrow> n < log 2 m" for m n :: nat
-using less_log_of_power[of 2] by simp
+ using less_log_of_power[of 2] by simp
lemma gr_one_powr[simp]:
fixes x y :: real shows "\<lbrakk> x > 1; y > 0 \<rbrakk> \<Longrightarrow> 1 < x powr y"
-by(simp add: less_powr_iff)
+ by(simp add: less_powr_iff)
lemma log_pow_cancel [simp]:
"a > 0 \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log a (a ^ b) = b"
@@ -2648,7 +2702,7 @@
lemma ceiling_log_nat_eq_powr_iff:
fixes b n k :: nat
- shows "\<lbrakk> b \<ge> 2; k > 0 \<rbrakk> \<Longrightarrow> ceiling (log b (real k)) = int n + 1 \<longleftrightarrow> (b^n < k \<and> k \<le> b^(n+1))"
+ shows "\<lbrakk> b \<ge> 2; k > 0 \<rbrakk> \<Longrightarrow> \<lceil>log b (real k)\<rceil> = int n + 1 \<longleftrightarrow> (b^n < k \<and> k \<le> b^(n+1))"
using ceiling_log_eq_powr_iff
by (auto simp: powr_add powr_realpow of_nat_power[symmetric] of_nat_mult[symmetric] ac_simps
simp del: of_nat_power of_nat_mult)
@@ -2681,7 +2735,7 @@
lemma ceiling_log2_div2:
assumes "n \<ge> 2"
- shows "ceiling(log 2 (real n)) = ceiling(log 2 ((n-1) div 2 + 1)) + 1"
+ shows "\<lceil>log 2 (real n)\<rceil> = \<lceil>log 2 ((n-1) div 2 + 1)\<rceil> + 1"
proof cases
assume "n=2" thus ?thesis by simp
next
@@ -2739,36 +2793,47 @@
for x :: real
using powr_realpow [of x 1] by simp
-lemma powr_neg_one: "0 < x \<Longrightarrow> x powr - 1 = 1/x"
+lemma powr_one' [simp]: "x powr 1 = \<bar>x\<bar>"
+ for x :: real
+ by (simp add: ln_real_def powr_def)
+
+lemma powr_neg_one: "0 < x \<Longrightarrow> x powr -1 = 1/x"
for x :: real
using powr_int [of x "- 1"] by simp
+lemma powr_neg_one' [simp]: "x powr -1 = 1/\<bar>x\<bar>"
+ for x :: real
+ by (simp add: powr_minus_divide)
+
lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr - numeral n = 1/x ^ numeral n"
for x :: real
using powr_int [of x "- numeral n"] by simp
-lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
- by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
-
-lemma ln_powr: "x \<noteq> 0 \<Longrightarrow> ln (x powr y) = y * ln x"
+lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> root n x = x powr (1/n)"
+ by (simp add: exp_divide_power_eq powr_def real_root_pos_unique)
+
+lemma powr_inverse_root: "0 < n \<Longrightarrow> x powr (1/n) = \<bar>root n x\<bar>"
+ by (metis abs_ge_zero mult_1 powr_one' powr_powr real_root_abs root_powr_inverse)
+
+lemma ln_powr [simp]: "ln (x powr y) = y * ln x"
for x :: real
by (simp add: powr_def)
-lemma ln_root: "n > 0 \<Longrightarrow> b > 0 \<Longrightarrow> ln (root n b) = ln b / n"
- by (simp add: root_powr_inverse ln_powr)
-
-lemma ln_sqrt: "0 < x \<Longrightarrow> ln (sqrt x) = ln x / 2"
- by (simp add: ln_powr ln_powr[symmetric] mult.commute)
-
-lemma log_root: "n > 0 \<Longrightarrow> a > 0 \<Longrightarrow> log b (root n a) = log b a / n"
+lemma ln_root: "n > 0 \<Longrightarrow> ln (root n b) = ln b / n"
+ by (metis ln_powr mult_1 powr_inverse_root powr_one' times_divide_eq_left)
+
+lemma ln_sqrt: "0 \<le> x \<Longrightarrow> ln (sqrt x) = ln x / 2"
+ by (smt (verit) field_sum_of_halves ln_mult real_sqrt_mult_self)
+
+lemma log_root: "n > 0 \<Longrightarrow> a \<ge> 0 \<Longrightarrow> log b (root n a) = log b a / n"
by (simp add: log_def ln_root)
-lemma log_powr: "x \<noteq> 0 \<Longrightarrow> log b (x powr y) = y * log b x"
- by (simp add: log_def ln_powr)
+lemma log_powr: "log b (x powr y) = y * log b x"
+ by (simp add: log_def)
(* [simp] is not worth it, interferes with some proofs *)
-lemma log_nat_power: "0 < x \<Longrightarrow> log b (x^n) = real n * log b x"
- by (simp add: log_powr powr_realpow [symmetric])
+lemma log_nat_power: "0 \<le> x \<Longrightarrow> log b (x^n) = real n * log b x"
+ by (simp add: ln_realpow log_def)
lemma log_of_power_eq:
assumes "m = b ^ n" "b > 1"
@@ -2780,7 +2845,7 @@
qed
lemma log2_of_power_eq: "m = 2 ^ n \<Longrightarrow> n = log 2 m" for m n :: nat
-using log_of_power_eq[of _ 2] by simp
+ using log_of_power_eq[of _ 2] by simp
lemma log_base_change: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log b x = log a x / log a b"
by (simp add: log_def)
@@ -2791,7 +2856,7 @@
lemma log_base_powr: "a \<noteq> 0 \<Longrightarrow> log (a powr b) x = log a x / b"
by (simp add: log_def ln_powr)
-lemma log_base_root: "n > 0 \<Longrightarrow> b > 0 \<Longrightarrow> log (root n b) x = n * (log b x)"
+lemma log_base_root: "n > 0 \<Longrightarrow> log (root n b) x = n * (log b x)"
by (simp add: log_def ln_root)
lemma ln_bound: "0 < x \<Longrightarrow> ln x \<le> x" for x :: real
@@ -2828,19 +2893,19 @@
using less_eq_real_def powr_less_mono2 that by auto
lemma powr01_less_one:
- fixes a::real
- assumes "0 < a" "a < 1"
- shows "a powr e < 1 \<longleftrightarrow> e>0"
+ fixes x::real
+ assumes "0 < x" "x < 1"
+ shows "x powr a < 1 \<longleftrightarrow> a>0"
proof
- show "a powr e < 1 \<Longrightarrow> e>0"
+ show "x powr a < 1 \<Longrightarrow> a>0"
using assms not_less_iff_gr_or_eq powr_less_mono2_neg by fastforce
- show "e>0 \<Longrightarrow> a powr e < 1"
+ show "a>0 \<Longrightarrow> x powr a < 1"
by (metis assms less_eq_real_def powr_less_mono2 powr_one_eq_one)
qed
-lemma powr_le1: "0 \<le> a \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> x powr a \<le> 1"
+lemma powr_le1: "0 \<le> a \<Longrightarrow> \<bar>x\<bar> \<le> 1 \<Longrightarrow> x powr a \<le> 1"
for x :: real
- using powr_mono2 by fastforce
+ by (smt (verit, best) powr_mono2 powr_one_eq_one uminus_powr_eq)
lemma powr_mono2':
fixes a x y :: real
@@ -2875,7 +2940,7 @@
lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
for x :: real
- unfolding powr_def exp_inj_iff by simp
+ by (metis log_powr_cancel)
lemma powr_half_sqrt: "0 \<le> x \<Longrightarrow> x powr (1/2) = sqrt x"
by (simp add: powr_def root_powr_inverse sqrt_def)
@@ -2979,12 +3044,6 @@
shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x))"
using assms unfolding continuous_within by (rule tendsto_powr)
-lemma isCont_powr[continuous_intros, simp]:
- fixes f g :: "_ \<Rightarrow> real"
- assumes "isCont f a" "isCont g a" "f a \<noteq> 0"
- shows "isCont (\<lambda>x. (f x) powr g x) a"
- using assms unfolding continuous_at by (rule tendsto_powr)
-
lemma continuous_on_powr[continuous_intros]:
fixes f g :: "_ \<Rightarrow> real"
assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. f x \<noteq> 0"
@@ -3020,20 +3079,20 @@
qed
lemma has_derivative_const_powr [derivative_intros]:
- assumes "\<And>x. (f has_derivative f') (at x)" "a \<noteq> (0::real)"
+ fixes a::real
+ assumes "\<And>x. (f has_derivative f') (at x)"
shows "((\<lambda>x. a powr (f x)) has_derivative (\<lambda>y. f' y * ln a * a powr (f x))) (at x)"
using assms
apply (simp add: powr_def)
- apply (rule assms derivative_eq_intros refl)+
- done
+ using DERIV_compose_FDERIV DERIV_exp has_derivative_mult_left by blast
lemma has_real_derivative_const_powr [derivative_intros]:
+ fixes a::real
assumes "\<And>x. (f has_real_derivative f' x) (at x)"
- "a \<noteq> (0::real)"
shows "((\<lambda>x. a powr (f x)) has_real_derivative (f' x * ln a * a powr (f x))) (at x)"
using assms
apply (simp add: powr_def)
- apply (rule assms derivative_eq_intros refl | simp)+
+ apply (rule assms impI derivative_eq_intros refl | simp)+
done
lemma DERIV_powr:
@@ -6847,7 +6906,7 @@
lemma artanh_minus_real [simp]:
assumes "abs x < 1"
shows "artanh (-x::real) = -artanh x"
- using assms by (simp add: artanh_def ln_div field_simps)
+ by (smt (verit) artanh_def assms field_sum_of_halves ln_div)
lemma sinh_less_cosh_real: "sinh (x :: real) < cosh x"
by (simp add: sinh_def cosh_def)