# HG changeset patch # User paulson # Date 1720266703 -3600 # Node ID 35442f748ec8603e4f45c4208b063ffb1f34b4b7 # Parent d3b96e19ccc7fc471c97e5cfb375c9c42cc01e9f# Parent 5c691b178e08a8a0911cd686aa60744fe10ff6a5 merged diff -r d3b96e19ccc7 -r 35442f748ec8 src/HOL/Analysis/Gamma_Function.thy --- 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 (\k = 1..n. ln (1 + 1 / real_of_nat k)))" by (subst exp_sum [symmetric]) (simp_all add: sum_distrib_left) also have "(\k=1..n. ln (1 + 1 / of_nat k) :: real) = ln (\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 "(\k=1..n. 1 + 1 / of_nat k :: real) = (\k=1..n. (of_nat k + 1) / of_nat k)" by (intro prod.cong) (simp_all add: field_split_simps) also have "(\k=1..n. (of_nat k + 1) / of_nat k :: real) = of_nat n + 1" diff -r d3b96e19ccc7 -r 35442f748ec8 src/HOL/Analysis/Infinite_Products.thy --- 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<..}" "\x. x"] - using continuous_on_tendsto_compose [of "{0<..}" ln "(\n. prod f {..n})" p] - by (auto simp: prod_defs sums_def_le ln_prod order_tendstoD) + moreover have "\x. f x \ 0" + by (smt (verit, best) "0") + ultimately show ?thesis + using assms continuous_on_ln [of "{0<..}" "\x. x"] + using continuous_on_tendsto_compose [of "{0<..}" ln "(\n. prod f {..n})" p] + by (auto simp: prod_defs sums_def_le ln_prod order_tendstoD) qed lemma summable_ln_real: diff -r d3b96e19ccc7 -r 35442f748ec8 src/HOL/Analysis/Kronecker_Approximation_Theorem.thy --- 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 \ (p+1) powr (n/p)" by (simp add: divide_simps) then have "ln ((n + 1) / L) \ ln (real (p + 1) powr (real n / real p))" - by simp + by (simp add: flip: ln_powr) also have "\ \ (n/p) * ln(p+1)" by (simp add: powr_def) finally have "ln ((n + 1) / L) \ (n/p) * ln(p+1) \ L > 0" diff -r d3b96e19ccc7 -r 35442f748ec8 src/HOL/Analysis/Weierstrass_Theorems.thy --- 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 \" using \01(1) \0 < k\ k$1) ln_gt_zero ln_mult by fastforce then have "real (NN e) * ln (1 / (real k * $) < ln e" - using k$1) NN(2) [of e] that by (simp add: ln_div divide_simps) + using k\(1) NN(2) [of e] \0 < \\ \0 < k\ that by (simp add: ln_div divide_simps) then have "exp (real (NN e) * ln (1 / (real k * $)) < e" by (metis exp_less_mono exp_ln that) then show ?thesis diff -r d3b96e19ccc7 -r 35442f748ec8 src/HOL/Complex_Analysis/Great_Picard.thy --- 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: \0 < n\ Schottky_lemma1 add_pos_nonneg ln_div [symmetric]) + by (simp add: \0 < n\ Schottky_lemma1 add_pos_nonneg ln_divide_pos [symmetric]) also have "... \ 3" proof (cases "n = 1") case True diff -r d3b96e19ccc7 -r 35442f748ec8 src/HOL/Decision_Procs/Approximation_Bounds.thy --- 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 \ ln (1 / x)" unfolding ln_le_cancel_iff[OF B A] using float_divl[of _ 1 x] by auto - hence "ln x \ - ln ?divl" unfolding nonzero_inverse_eq_divide[OF \real_of_float x \ 0\, symmetric] ln_inverse[OF \0 < real_of_float x\] by auto + hence "ln x \ - ln ?divl" + by (simp add: \real_of_float x \ 0\ ln_div) from this ub_ln_lb_ln_bounds'[OF A', THEN conjunct1, THEN le_imp_neg_le] have "?ln \ - 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) \ ln ?divr" unfolding ln_le_cancel_iff[OF A B] using float_divr[of 1 x] by auto - hence "- ln ?divr \ ln x" unfolding nonzero_inverse_eq_divide[OF \real_of_float x \ 0\, symmetric] ln_inverse[OF \0 < real_of_float x\] by auto + hence "- ln ?divr \ ln x" + by (simp add: \real_of_float x \ 0\ ln_div) from ub_ln_lb_ln_bounds'[OF A', THEN conjunct2, THEN le_imp_neg_le] this have "- the (ub_ln prec ?divr) \ ?ln" unfolding uminus_float.rep_eq by (rule order_trans) } diff -r d3b96e19ccc7 -r 35442f748ec8 src/HOL/Nonstandard_Analysis/HLog.thy --- 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: - "\a x y. 0 < a \ a \ 1 \ 0 < x \ 0 < y \ hlog a (x * y) = hlog a x + hlog a y" + "\a x y. 0 < a \ a \ 1 \ (x\0 \ y\0) \ hlog a (x * y) = hlog a x + hlog a y" by transfer (rule log_mult) lemma hlog_as_starfun: "\a x. 0 < a \ a \ 1 \ hlog a x = ( *f* ln) x / ( *f* ln) a" diff -r d3b96e19ccc7 -r 35442f748ec8 src/HOL/NthRoot.thy --- 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 \ 0 \ y \ y ^ n = x \ 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 \ y ^ n = x \ 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 \ root n 1 = 1" by (simp add: real_root_pos_unique) diff -r d3b96e19ccc7 -r 35442f748ec8 src/HOL/Probability/Information.thy --- 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\0 \ y\0 \ 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\0 \ y\0 \ 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 \Introduce some simplification rules for logarithm of base \<^term>\b\.\ - -lemma log_neg_const: - assumes "x \ 0" - shows "log b x = log b 0" -proof - - { fix u :: real - have "x \ 0" by fact - also have "0 < exp u" - using exp_gt_zero . - finally have "exp u \ 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 \A\ + log b \B\ else log b 0)" - using log_mult[of "\A\" "\B\"] 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 \A\) - log b \B\ 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 \\<^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 \\<^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 \ ?M" unfolding M proof (intro ST.KL_density_density_nonneg) @@ -828,7 +809,7 @@ have "integrable MX (\x. Px x * log b (1 / Px x)) = integrable MX (\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) (\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 "\ = (\ x. log b (Px x) \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 "\ = - 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: "(\ x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \MX) = (\ x. (- log b (measure MX A) / measure MX A) * indicator A x \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 "- (\ x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \MX) = log b (measure MX A)" unfolding eq using uniform_distributed_params[OF X] @@ -1116,9 +1097,9 @@ have "integrable (S \\<^sub>M T \\<^sub>M P) (\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 (\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 \\<^sub>M T \\<^sub>M P) (\(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 \\<^sub>M T \\<^sub>M P) (\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 "\x. (fst x, snd (snd x))"] @@ -1247,7 +1230,41 @@ ultimately have I2: "integrable (S \\<^sub>M T \\<^sub>M P) (\(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 \ Pxyz (x1, ab, baa) = 0" + assume a2: "Pz (snd (snd (x1, ab, baa))) = 0 \ Pxyz (x1, ab, baa) = 0" + assume a3: "Px (fst (x1, ab, baa)) = 0 \ Pxyz (x1, ab, baa) = 0" + have f4: "\r ra rb. (ra::real) * (rb + r) = rb * ra + ra * r" + by (simp add: vector_space_over_itself.scale_right_distrib) + have f5: "0 \ Px x1 \ 0 = Pxyz (x1, ab, baa)" + using a3 by auto + have f6: "0 \ Pz baa \ 0 = Pxyz (x1, ab, baa)" + using a2 by force + have f7: "\r. (0::real) = 0 * r" + by simp + have "0 = Px x1 * Pz baa \ 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 \ Px x1 * Pz baa" + moreover + { assume "0 \ Px x1 * Pz baa \ 0 \ 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))) \ 0 \ 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)) \ 0 \ Pxz (x1, baa) / (Px x1 * Pz baa) \ 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))) \ 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))) \ 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)) \ 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 \\<^sub>M T \\<^sub>M P) (\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 (\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 diff -r d3b96e19ccc7 -r 35442f748ec8 src/HOL/Real_Asymp/Multiseries_Expansion.thy --- 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 (\x. b x > 0) at_top" by (simp add: basis_wf_Cons filterlim_at_top_dense) moreover have "(\a. inverse (a powr 1)) \ o(\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 diff -r d3b96e19ccc7 -r 35442f748ec8 src/HOL/Transcendental.thy --- 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 \We totalise @{term ln} over all reals exactly as done in Mathlib\ instantiation real :: ln begin +definition raw_ln_real :: "real \ real" + where "raw_ln_real x \ (THE u. exp u = x)" + definition ln_real :: "real \ real" - where "ln_real x = (THE u. exp u = x)" + where "ln_real \ \x. if x=0 then 0 else raw_ln_real \x\" 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 \ 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 \ exp (raw_ln_real x) = x" + by (auto dest: exp_total) + +lemma raw_ln_unique: "exp y = x \ raw_ln_real x = y" + by auto + +lemma abs_raw_ln: "x \ 0 \ raw_ln_real\x\ = 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 \ 0 \ exp (ln x) = \x\" + by (simp add: ln_real_def) + lemma exp_ln [simp]: "0 < x \ 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 \ 0 < x" for x :: real @@ -1590,26 +1617,48 @@ lemma ln_unique: "exp y = x \ ln x = y" for x :: real - by (erule subst) (rule ln_exp) - -lemma ln_mult: "0 < x \ 0 < y \ ln (x * y) = ln x + ln y" + by auto + +lemma ln_unique': "exp y = \x\ \ ln x = y" for x :: real - by (rule ln_unique) (simp add: exp_add) - -lemma ln_prod: "finite I \ (\i. i \ I \ f i > 0) \ ln (prod f I) = sum (\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 \ y>0 \ 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\0 \ y\0) \ 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 \ y>0 \ ln (x * y) = ln x + ln y" + for x :: real + by (simp add: ln_mult) + +lemma ln_prod: "finite I \ (\i. i \ I \ f i \ 0) \ ln (prod f I) = sum (\x. ln(f x)) I" for f :: "'a \ real" by (induct I rule: finite_induct) (auto simp: ln_mult prod_pos) -lemma ln_inverse: "0 < x \ 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\0 \ y\0) \ 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 \ y>0 \ ln (x/y) = ln x - ln y" for x :: real - by (rule ln_unique) (simp add: exp_minus) - -lemma ln_div: "0 < x \ 0 < y \ ln (x / y) = ln x - ln y" - for x :: real - by (rule ln_unique) (simp add: exp_diff) - -lemma ln_realpow: "0 < x \ 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 \ 0 < y \ ln x < ln y \ x < y" for x :: real @@ -1677,32 +1726,36 @@ for x :: real by simp -lemma ln_neg_is_const: "x \ 0 \ 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 \ x = 0" if "a > 1" for a x :: real using that by (auto simp: powr_def split: if_splits) +text \A consequence of our "totalising" of ln\ +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 \ 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 = "\x\" and f = exp]) auto - with True show ?thesis - by simp -next case False - with \x \ 0\ show "isCont ln x" - unfolding isCont_def - by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\_. ln 0"]) - (auto simp: ln_neg_is_const not_less eventually_at dist_real_def - intro!: exI[of _ "\x\"]) -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 \ a) F \ a \ 0 \ ((\x. ln (f x)) \ 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 "\ = 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 "\ = 1 + (y - x) / x" @@ -2279,37 +2332,32 @@ where "log a x = ln x / ln a" lemma tendsto_log [tendsto_intros]: - "(f \ a) F \ (g \ b) F \ 0 < a \ a \ 1 \ 0 < b \ + "(f \ a) F \ (g \ b) F \ 0 < a \ a \ 1 \ b\0 \ ((\x. log (f x) (g x)) \ 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 (\x. x))" + and "f (Lim F (\x. x)) > 0" and "f (Lim F (\x. x)) \ 1" - and "0 < g (Lim F (\x. x))" + and "g (Lim F (\x. x)) \ 0" shows "continuous F (\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 \ 1" - and "0 < g a" + and "g a \ 0" shows "continuous (at a within s) (\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 \ 1" "0 < g a" - shows "isCont (\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 "\x\s. 0 < f x" "\x\s. f x \ 1" "\x\s. 0 < g x" - shows "continuous_on s (\x. log (f x) (g x))" + assumes "continuous_on S f" "continuous_on S g" + and "\x\S. 0 < f x" "\x\S. f x \ 1" "\x\S. g x \ 0" + shows "continuous_on S (\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 \ x \ 0 \ y \ (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 \ real" - assumes "\i. i\I \ x i \ 0" shows "(prod x I) powr r = (\i\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 \ x powr y" for x y :: real by (simp add: powr_def) -lemma powr_non_neg[simp]: "\a powr x < 0" for a x::real +lemma powr_non_neg[simp]: "\ a powr x < 0" for a x::real using powr_ge_pzero[of a x] by arith -lemma inverse_powr: "\y::real. 0 \ y \ inverse y powr a = inverse (y powr a)" +lemma inverse_powr: "\y::real. inverse y powr a = inverse (y powr a)" by (simp add: exp_minus ln_inverse powr_def) -lemma powr_divide: "\0 \ x; 0 \ y\ \ (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 \ 0 \ n \ 0 \ (z powr u) ^ n = z powr (of_nat n * u)" + shows "z \ 0 \ (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 \ 0 \ finite A \ x powr sum f A = (\y\A. x powr f y)" - by (simp add: powr_def exp_sum sum_distrib_right) +lemma powr_sum: + assumes "x \ 0" + shows "x powr sum f A = (\y\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) \ x \ 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 \ 0 < y \ log a (x * y) = log a x + log a y" + "(x\0 \ y\0) \ 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 \ y>0 \ 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 \ a \ 1 \ log a a = 1" by (simp add: log_def) -lemma log_inverse: "0 < x \ log a (inverse x) = - log a x" - using ln_inverse log_def by auto - -lemma log_divide: "0 < x \ 0 < y \ 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\0 \ y\0) \ 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 \ y>0 \ log a (x / y) = log a x - log a y" + using log_divide by auto lemma powr_gt_zero [simp]: "0 < x powr a \ x \ 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 \ b \ 1 \ 0 < x \ log b x + y = log b (x * b powr y)" - and add_log_eq_powr: "0 < b \ b \ 1 \ 0 < x \ y + log b x = log b (b powr y * x)" - and log_minus_eq_powr: "0 < b \ b \ 1 \ 0 < x \ log b x - y = log b (x * b powr -y)" - and minus_log_eq_powr: "0 < b \ b \ 1 \ 0 < x \ y - log b x = log b (b powr y / x)" +lemma log_add_eq_powr: "0 < b \ b \ 1 \ x\0 \ log b x + y = log b (x * b powr y)" + and add_log_eq_powr: "0 < b \ b \ 1 \ x\0 \ y + log b x = log b (b powr y * x)" + and log_minus_eq_powr: "0 < b \ b \ 1 \ x\0 \ 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 \ b \