--- a/src/HOL/Analysis/Gamma_Function.thy Sat Jul 06 11:18:31 2024 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy Sat Jul 06 12:51:43 2024 +0100
@@ -2756,7 +2756,7 @@
exp (z * of_real (\<Sum>k = 1..n. ln (1 + 1 / real_of_nat k)))"
by (subst exp_sum [symmetric]) (simp_all add: sum_distrib_left)
also have "(\<Sum>k=1..n. ln (1 + 1 / of_nat k) :: real) = ln (\<Prod>k=1..n. 1 + 1 / real_of_nat k)"
- by (subst ln_prod [symmetric]) (auto intro!: add_pos_nonneg)
+ by (subst ln_prod [symmetric]) (auto simp: divide_simps)
also have "(\<Prod>k=1..n. 1 + 1 / of_nat k :: real) = (\<Prod>k=1..n. (of_nat k + 1) / of_nat k)"
by (intro prod.cong) (simp_all add: field_split_simps)
also have "(\<Prod>k=1..n. (of_nat k + 1) / of_nat k :: real) = of_nat n + 1"
--- a/src/HOL/Analysis/Infinite_Products.thy Sat Jul 06 11:18:31 2024 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy Sat Jul 06 12:51:43 2024 +0100
@@ -1630,10 +1630,12 @@
proof -
have "p > 0"
using assms unfolding prod_defs by (metis LIMSEQ_prod_nonneg less_eq_real_def)
- then show ?thesis
- using assms continuous_on_ln [of "{0<..}" "\<lambda>x. x"]
- using continuous_on_tendsto_compose [of "{0<..}" ln "(\<lambda>n. prod f {..n})" p]
- by (auto simp: prod_defs sums_def_le ln_prod order_tendstoD)
+ moreover have "\<And>x. f x \<noteq> 0"
+ by (smt (verit, best) "0")
+ ultimately show ?thesis
+ using assms continuous_on_ln [of "{0<..}" "\<lambda>x. x"]
+ using continuous_on_tendsto_compose [of "{0<..}" ln "(\<lambda>n. prod f {..n})" p]
+ by (auto simp: prod_defs sums_def_le ln_prod order_tendstoD)
qed
lemma summable_ln_real:
--- a/src/HOL/Analysis/Kronecker_Approximation_Theorem.thy Sat Jul 06 11:18:31 2024 +0200
+++ b/src/HOL/Analysis/Kronecker_Approximation_Theorem.thy Sat Jul 06 12:51:43 2024 +0100
@@ -1144,7 +1144,7 @@
finally have "(n + 1) / L \<le> (p+1) powr (n/p)"
by (simp add: divide_simps)
then have "ln ((n + 1) / L) \<le> ln (real (p + 1) powr (real n / real p))"
- by simp
+ by (simp add: flip: ln_powr)
also have "\<dots> \<le> (n/p) * ln(p+1)"
by (simp add: powr_def)
finally have "ln ((n + 1) / L) \<le> (n/p) * ln(p+1) \<and> L > 0"
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy Sat Jul 06 11:18:31 2024 +0200
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Sat Jul 06 12:51:43 2024 +0100
@@ -405,7 +405,7 @@
have "0 < ln (real k) + ln \<delta>"
using \<delta>01(1) \<open>0 < k\<close> k\<delta>(1) ln_gt_zero ln_mult by fastforce
then have "real (NN e) * ln (1 / (real k * \<delta>)) < ln e"
- using k\<delta>(1) NN(2) [of e] that by (simp add: ln_div divide_simps)
+ using k\<delta>(1) NN(2) [of e] \<open>0 < \<delta>\<close> \<open>0 < k\<close> that by (simp add: ln_div divide_simps)
then have "exp (real (NN e) * ln (1 / (real k * \<delta>))) < e"
by (metis exp_less_mono exp_ln that)
then show ?thesis
--- a/src/HOL/Complex_Analysis/Great_Picard.thy Sat Jul 06 11:18:31 2024 +0200
+++ b/src/HOL/Complex_Analysis/Great_Picard.thy Sat Jul 06 12:51:43 2024 +0100
@@ -94,7 +94,7 @@
proof -
have "ln (1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) - ln (real n + sqrt ((real n)\<^sup>2 - 1)) =
ln ((1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) / (real n + sqrt ((real n)\<^sup>2 - 1)))"
- by (simp add: \<open>0 < n\<close> Schottky_lemma1 add_pos_nonneg ln_div [symmetric])
+ by (simp add: \<open>0 < n\<close> Schottky_lemma1 add_pos_nonneg ln_divide_pos [symmetric])
also have "... \<le> 3"
proof (cases "n = 1")
case True
--- a/src/HOL/Decision_Procs/Approximation_Bounds.thy Sat Jul 06 11:18:31 2024 +0200
+++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy Sat Jul 06 12:51:43 2024 +0100
@@ -2861,7 +2861,8 @@
hence B: "0 < real_of_float ?divl" by auto
have "ln ?divl \<le> ln (1 / x)" unfolding ln_le_cancel_iff[OF B A] using float_divl[of _ 1 x] by auto
- hence "ln x \<le> - ln ?divl" unfolding nonzero_inverse_eq_divide[OF \<open>real_of_float x \<noteq> 0\<close>, symmetric] ln_inverse[OF \<open>0 < real_of_float x\<close>] by auto
+ hence "ln x \<le> - ln ?divl"
+ by (simp add: \<open>real_of_float x \<noteq> 0\<close> ln_div)
from this ub_ln_lb_ln_bounds'[OF A', THEN conjunct1, THEN le_imp_neg_le]
have "?ln \<le> - the (lb_ln prec ?divl)" unfolding uminus_float.rep_eq by (rule order_trans)
} moreover
@@ -2871,7 +2872,8 @@
hence B: "0 < real_of_float ?divr" by auto
have "ln (1 / x) \<le> ln ?divr" unfolding ln_le_cancel_iff[OF A B] using float_divr[of 1 x] by auto
- hence "- ln ?divr \<le> ln x" unfolding nonzero_inverse_eq_divide[OF \<open>real_of_float x \<noteq> 0\<close>, symmetric] ln_inverse[OF \<open>0 < real_of_float x\<close>] by auto
+ hence "- ln ?divr \<le> ln x"
+ by (simp add: \<open>real_of_float x \<noteq> 0\<close> ln_div)
from ub_ln_lb_ln_bounds'[OF A', THEN conjunct2, THEN le_imp_neg_le] this
have "- the (ub_ln prec ?divr) \<le> ?ln" unfolding uminus_float.rep_eq by (rule order_trans)
}
--- a/src/HOL/Nonstandard_Analysis/HLog.thy Sat Jul 06 11:18:31 2024 +0200
+++ b/src/HOL/Nonstandard_Analysis/HLog.thy Sat Jul 06 12:51:43 2024 +0100
@@ -73,7 +73,7 @@
by transfer simp
lemma hlog_mult:
- "\<And>a x y. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a (x * y) = hlog a x + hlog a y"
+ "\<And>a x y. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> (x\<noteq>0 \<longleftrightarrow> y\<noteq>0) \<Longrightarrow> hlog a (x * y) = hlog a x + hlog a y"
by transfer (rule log_mult)
lemma hlog_as_starfun: "\<And>a x. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a x = ( *f* ln) x / ( *f* ln) a"
--- a/src/HOL/NthRoot.thy Sat Jul 06 11:18:31 2024 +0200
+++ b/src/HOL/NthRoot.thy Sat Jul 06 12:51:43 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/Probability/Information.thy Sat Jul 06 11:18:31 2024 +0200
+++ b/src/HOL/Probability/Information.thy Sat Jul 06 12:51:43 2024 +0100
@@ -10,47 +10,22 @@
Independent_Family
begin
+
+lemma log_mult_nz:
+ "x\<noteq>0 \<Longrightarrow> 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_divide_nz:
+ "x\<noteq>0 \<Longrightarrow> y\<noteq>0 \<Longrightarrow> log a (x / y) = log a x - log a y"
+ by (simp add: diff_divide_distrib ln_div log_def)
+
subsection "Information theory"
locale information_space = prob_space +
fixes b :: real assumes b_gt_1: "1 < b"
-context information_space
-begin
-
text \<open>Introduce some simplification rules for logarithm of base \<^term>\<open>b\<close>.\<close>
-
-lemma log_neg_const:
- assumes "x \<le> 0"
- shows "log b x = log b 0"
-proof -
- { fix u :: real
- have "x \<le> 0" by fact
- also have "0 < exp u"
- using exp_gt_zero .
- finally have "exp u \<noteq> x"
- by auto }
- then show "log b x = log b 0"
- by (simp add: log_def ln_real_def)
-qed
-
-lemma log_mult_eq:
- "log b (A * B) = (if 0 < A * B then log b \<bar>A\<bar> + log b \<bar>B\<bar> else log b 0)"
- using log_mult[of "\<bar>A\<bar>" "\<bar>B\<bar>"] b_gt_1 log_neg_const[of "A * B"]
- by (auto simp: zero_less_mult_iff mult_le_0_iff)
-
-lemma log_inverse_eq:
- "log b (inverse B) = (if 0 < B then - log b B else log b 0)"
- using ln_inverse log_def log_neg_const by force
-
-lemma log_divide_eq:
- "log b (A / B) = (if 0 < A * B then (log b \<bar>A\<bar>) - log b \<bar>B\<bar> else log b 0)"
- unfolding divide_inverse log_mult_eq log_inverse_eq abs_inverse
- by (auto simp: zero_less_mult_iff mult_le_0_iff)
-
-lemmas log_simps = log_mult_eq log_inverse_eq log_divide_eq
-
-end
+lemmas log_simps = log_mult log_inverse log_divide
subsection "Kullback$-$Leibler divergence"
@@ -575,10 +550,16 @@
by (auto intro: distributed_real_measurable measurable_fst'' measurable_snd''
intro!: borel_measurable_times borel_measurable_log borel_measurable_divide)
ultimately have int: "integrable (S \<Otimes>\<^sub>M T) f"
- apply (rule integrable_cong_AE_imp)
- using A B
- by (auto simp: f_def log_divide_eq log_mult_eq field_simps space_pair_measure Px_nn Py_nn Pxy_nn
- less_le)
+ proof (rule integrable_cong_AE_imp)
+ show "AE x in S \<Otimes>\<^sub>M
+ T. Pxy x * log b (Pxy x) - Pxy x * log b (Px (fst x)) - Pxy x * log b (Py (snd x))
+ = f x"
+ using A B unfolding f_def
+
+ apply (auto simp: f_def field_simps space_pair_measure Px_nn Py_nn Pxy_nn
+ less_le )
+ by (smt (verit, del_insts) AE_I2 distrib_left log_divide log_mult mult_eq_0_iff)
+ qed
show "0 \<le> ?M" unfolding M
proof (intro ST.KL_density_density_nonneg)
@@ -828,7 +809,7 @@
have "integrable MX (\<lambda>x. Px x * log b (1 / Px x)) =
integrable MX (\<lambda>x. - Px x * log b (Px x))"
using Px
- by (intro integrable_cong_AE) (auto simp: log_divide_eq less_le)
+ by (intro integrable_cong_AE) (auto simp: log_divide_pos log_recip)
then show "integrable (distr M MX X) (\<lambda>x. - log b (1 / Px x))"
unfolding distributed_distr_eq_density[OF X]
using Px int
@@ -836,7 +817,7 @@
qed (auto simp: minus_log_convex[OF b_gt_1])
also have "\<dots> = (\<integral> x. log b (Px x) \<partial>distr M MX X)"
unfolding distributed_distr_eq_density[OF X] using Px
- by (intro integral_cong_AE) (auto simp: AE_density log_divide_eq)
+ by (intro integral_cong_AE) (auto simp: AE_density log_divide_pos)
also have "\<dots> = - entropy b MX X"
unfolding distributed_distr_eq_density[OF X] using Px
by (subst entropy_distr[OF X]) (auto simp: integral_density)
@@ -872,7 +853,7 @@
have eq: "(\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
(\<integral> x. (- log b (measure MX A) / measure MX A) * indicator A x \<partial>MX)"
using uniform_distributed_params[OF X]
- by (intro Bochner_Integration.integral_cong) (auto split: split_indicator simp: log_divide_eq zero_less_measure_iff)
+ by (intro Bochner_Integration.integral_cong) (auto split: split_indicator simp: log_divide_pos zero_less_measure_iff)
show "- (\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
log b (measure MX A)"
unfolding eq using uniform_distributed_params[OF X]
@@ -1116,9 +1097,9 @@
have "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>x. Pxyz x * - log b (?f x))"
apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3])
using ae1 ae2 ae3 ae4
- apply (auto simp: log_divide_eq log_mult_eq zero_le_mult_iff zero_less_mult_iff zero_less_divide_iff field_simps
- less_le space_pair_measure)
- done
+ apply (auto simp: log_divide log_mult zero_le_mult_iff zero_less_mult_iff zero_less_divide_iff field_simps
+ less_le space_pair_measure split: prod.split)
+ by (smt (verit, best) AE_I2 fst_conv log_divide mult_cancel_left mult_minus_right snd_conv)
then
show "integrable ?P (\<lambda>x. - log b (?f x))"
by (subst integrable_real_density) (auto simp: space_pair_measure)
@@ -1131,9 +1112,9 @@
apply simp
apply (intro integral_cong_AE)
using ae1 ae2 ae3 ae4
- apply (auto simp: log_divide_eq zero_less_mult_iff zero_less_divide_iff field_simps
- space_pair_measure less_le)
- done
+ apply (auto simp: zero_less_mult_iff zero_less_divide_iff field_simps
+ space_pair_measure less_le split: prod.split)
+ by (smt (verit, best) AE_I2 fst_conv log_divide mult_eq_0_iff mult_minus_right snd_conv)
finally show ?nonneg
by simp
qed
@@ -1233,8 +1214,10 @@
ultimately have I1: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z))))"
apply (rule integrable_cong_AE_imp)
using ae1 ae4 Px_nn Pyz_nn Pxyz_nn
- by (auto simp: log_divide_eq log_mult_eq field_simps zero_less_mult_iff space_pair_measure less_le)
-
+ apply (auto simp: log_divide log_mult field_simps zero_less_mult_iff space_pair_measure less_le
+ split: prod.split)
+ apply (intro AE_I2)
+ by (smt (verit, best) distrib_left divide_eq_0_iff fst_conv log_mult mult.commute nonzero_mult_div_cancel_left snd_conv times_divide_eq_right)
have "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P)
(\<lambda>x. Pxyz x * log b (Pxz (fst x, snd (snd x))) - Pxyz x * log b (Px (fst x)) - Pxyz x * log b (Pz (snd (snd x))))"
using finite_entropy_integrable_transform[OF Fxz Pxyz Pxyz_nn, of "\<lambda>x. (fst x, snd (snd x))"]
@@ -1247,7 +1230,41 @@
ultimately have I2: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z)))"
apply (rule integrable_cong_AE_imp)
using ae1 ae2 ae3 ae4 Px_nn Pz_nn Pxz_nn Pyz_nn Pxyz_nn
- by (auto simp: log_divide_eq log_mult_eq field_simps zero_less_mult_iff less_le space_pair_measure)
+ apply(auto simp: field_simps zero_less_mult_iff less_le space_pair_measure split: prod.split)
+ apply (intro AE_I2)
+ apply clarify
+ proof -
+ fix a :: 'c and aa :: 'd and ba :: 'e and x1 :: 'c and ab :: 'd and baa :: 'e
+ assume a1: "Pxz (fst (x1, ab, baa), snd (snd (x1, ab, baa))) = 0 \<longrightarrow> Pxyz (x1, ab, baa) = 0"
+ assume a2: "Pz (snd (snd (x1, ab, baa))) = 0 \<longrightarrow> Pxyz (x1, ab, baa) = 0"
+ assume a3: "Px (fst (x1, ab, baa)) = 0 \<longrightarrow> Pxyz (x1, ab, baa) = 0"
+ have f4: "\<forall>r ra rb. (ra::real) * (rb + r) = rb * ra + ra * r"
+ by (simp add: vector_space_over_itself.scale_right_distrib)
+ have f5: "0 \<noteq> Px x1 \<or> 0 = Pxyz (x1, ab, baa)"
+ using a3 by auto
+ have f6: "0 \<noteq> Pz baa \<or> 0 = Pxyz (x1, ab, baa)"
+ using a2 by force
+ have f7: "\<forall>r. (0::real) = 0 * r"
+ by simp
+ have "0 = Px x1 * Pz baa \<longrightarrow> Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1) + log b (Pz baa) + log b (Pxz (x1, baa) / (Px x1 * Pz baa)))"
+ using f6 f5 by simp
+ moreover
+ { assume "0 \<noteq> Px x1 * Pz baa"
+ moreover
+ { assume "0 \<noteq> Px x1 * Pz baa \<and> 0 \<noteq> Pxyz (x1, ab, baa)"
+ then have "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1 * Pz baa) + log b (Pxz (x1, baa) / (Px x1 * Pz baa))) \<and> 0 \<noteq> Pxz (x1, baa) / (Px x1 * Pz baa)"
+ using a1 by (metis (no_types) divide_eq_0_iff fst_eqD log_mult_nz mult.commute nonzero_eq_divide_eq snd_eqD)
+ moreover
+ { assume "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1) + (log b 0 + log b 0)) \<and> 0 \<noteq> Pxz (x1, baa) / (Px x1 * Pz baa) \<and> Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = log b (Px x1) * Pxyz (x1, ab, baa) + Pxyz (x1, ab, baa) * log b (Pz baa * (Pxz (x1, baa) / (Px x1 * Pz baa)))"
+ then have "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = log b (Px x1) * Pxyz (x1, ab, baa) + (log b (Pz baa) * Pxyz (x1, ab, baa) + Pxyz (x1, ab, baa) * log b (Pxz (x1, baa) / (Px x1 * Pz baa)))"
+ using f7 f4 by (metis (no_types) divide_eq_0_iff log_mult_nz mult.commute) }
+ ultimately have "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1) + log b (Pz baa) + log b (Pxz (x1, baa) / (Px x1 * Pz baa))) \<or> Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = log b (Px x1) * Pxyz (x1, ab, baa) + (log b (Pz baa) * Pxyz (x1, ab, baa) + Pxyz (x1, ab, baa) * log b (Pxz (x1, baa) / (Px x1 * Pz baa)))"
+ using f4 by (simp add: log_mult_nz) }
+ ultimately have "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1) + log b (Pz baa) + log b (Pxz (x1, baa) / (Px x1 * Pz baa))) \<or> Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1) + log b (Pz baa)) + Pxyz (x1, ab, baa) * log b (Pxz (x1, baa) / (Px x1 * Pz baa)) \<or> Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = log b (Px x1) * Pxyz (x1, ab, baa) + (log b (Pz baa) * Pxyz (x1, ab, baa) + Pxyz (x1, ab, baa) * log b (Pxz (x1, baa) / (Px x1 * Pz baa)))"
+ using f7 by (metis (no_types)) }
+ ultimately show "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = log b (Px x1) * Pxyz (x1, ab, baa) + (log b (Pz baa) * Pxyz (x1, ab, baa) + Pxyz (x1, ab, baa) * log b (Pxz (x1, baa) / (Px x1 * Pz baa)))"
+ by argo
+ qed
from ae I1 I2 show ?eq
unfolding conditional_mutual_information_def mi_eq
@@ -1355,8 +1372,12 @@
have "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>x. Pxyz x * - log b (?f x))"
apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3])
using Pz_nn Pxz_nn Pyz_nn Pxyz_nn ae2 ae3 ae4
- by (auto simp: log_divide_eq log_mult_eq zero_le_mult_iff zero_less_mult_iff
- zero_less_divide_iff field_simps space_pair_measure less_le)
+ apply (auto simp: log_divide_nz log_mult_nz zero_le_mult_iff zero_less_mult_iff
+ zero_less_divide_iff field_simps space_pair_measure less_le split: prod.split)
+ apply (intro AE_I2)
+ apply (auto simp: )
+ by (smt (verit, best) log_divide minus_mult_minus mult_minus_left no_zero_divisors)
+
then
show "integrable ?P (\<lambda>x. - log b (?f x))"
using Pxyz_nn by (auto simp: integrable_real_density)
@@ -1370,9 +1391,10 @@
apply simp
apply (intro integral_cong_AE)
using ae1 ae2 ae3 ae4
- apply (auto simp: log_divide_eq zero_less_mult_iff zero_less_divide_iff
- field_simps space_pair_measure less_le integral_cong_AE)
- done
+ apply (auto simp: log_divide_pos zero_less_mult_iff zero_less_divide_iff
+ field_simps space_pair_measure less_le integral_cong_AE split: prod.split)
+ apply (intro AE_I2)
+ by (metis divide_divide_eq_right log_recip mult_1 mult_minus_right)
finally show ?nonneg
by simp
qed
@@ -1632,9 +1654,6 @@
apply (subst conditional_entropy_eq[OF Py Pxy])
apply (auto intro!: sum.cong simp: Pxxy_eq sum_negf[symmetric] eq sum.reindex[OF inj]
log_simps zero_less_mult_iff zero_le_mult_iff field_simps mult_less_0_iff AE_count_space)
- using Py[THEN simple_distributed] Pxy[THEN simple_distributed]
- apply (auto simp add: not_le AE_count_space less_le antisym
- simple_distributed_nonneg[OF Py] simple_distributed_nonneg[OF Pxy])
done
qed
--- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy Sat Jul 06 11:18:31 2024 +0200
+++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy Sat Jul 06 12:51:43 2024 +0100
@@ -3323,7 +3323,7 @@
from assms have "eventually (\<lambda>x. b x > 0) at_top"
by (simp add: basis_wf_Cons filterlim_at_top_dense)
moreover have "(\<lambda>a. inverse (a powr 1)) \<in> o(\<lambda>a. a powr e')" if "e' > -1" for e' :: real
- using that by (simp add: landau_o.small.inverse_eq2 powr_add [symmetric] one_smallo_powr)
+ using that by (simp add: landau_o.small.inverse_eq2 one_smallo_powr flip: powr_one' powr_add)
ultimately show ?thesis using assms
by (auto simp: expands_to.simps basis_wf_Cons powr_minus
elim: eventually_mono
--- a/src/HOL/Transcendental.thy Sat Jul 06 11:18:31 2024 +0200
+++ b/src/HOL/Transcendental.thy Sat Jul 06 12:51:43 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,48 @@
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_mult_pos: "x>0 \<Longrightarrow> y>0 \<Longrightarrow> ln (x * y) = ln x + ln y"
+ for x :: real
+ by (simp add: 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 (simp add: divide_inverse ln_inverse ln_mult)
+
+lemma ln_divide_pos: "x>0 \<Longrightarrow> y>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 +1726,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 +2095,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 +2332,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 +2376,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 +2411,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 +2436,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 +2487,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 +2514,11 @@
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_mult_pos:
+ "x>0 \<Longrightarrow> y>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:
@@ -2474,11 +2538,19 @@
lemma log_eq_one [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log a a = 1"
by (simp add: log_def)
-lemma log_inverse: "0 < x \<Longrightarrow> log a (inverse x) = - log a x"
- using ln_inverse log_def by auto
-
-lemma log_divide: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a (x/y) = log a x - log a y"
- by (simp add: log_mult divide_inverse log_inverse)
+lemma log_inverse: "log a (inverse x) = - log a x"
+ by (simp add: ln_inverse log_def)
+
+lemma log_recip: "log a (1/x) = - log a x"
+ by (simp add: divide_inverse log_inverse)
+
+lemma log_divide:
+ "(x\<noteq>0 \<longleftrightarrow> y\<noteq>0) \<Longrightarrow> log a (x / y) = log a x - log a y"
+ by (simp add: diff_divide_distrib ln_div log_def)
+
+lemma log_divide_pos:
+ "x>0 \<Longrightarrow> y>0 \<Longrightarrow> log a (x / y) = log a x - log a y"
+ using log_divide by auto
lemma powr_gt_zero [simp]: "0 < x powr a \<longleftrightarrow> x \<noteq> 0"
for a x :: real
@@ -2488,12 +2560,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 +2685,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 +2722,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 +2755,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 +2813,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 +2865,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 +2876,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 +2913,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 +2960,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 +3064,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 +3099,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 +6926,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)