# HG changeset patch # User paulson # Date 1720474070 -3600 # Node ID 6dec6b1f31f57e3b5093a6fb0aba1275952b9263 # Parent 532156e8f15f335991a61d62cdf39800e61251a1 Better multiplication and division rules for ln and log diff -r 532156e8f15f -r 6dec6b1f31f5 src/HOL/Analysis/Kronecker_Approximation_Theorem.thy --- a/src/HOL/Analysis/Kronecker_Approximation_Theorem.thy Sun Jul 07 22:25:34 2024 +0100 +++ b/src/HOL/Analysis/Kronecker_Approximation_Theorem.thy Mon Jul 08 22:27:50 2024 +0100 @@ -1157,7 +1157,7 @@ have "ln (real (n + 1) / L) \ 0" using * eventually_at_top_dense by (intro tendsto_lowerbound [OF 0]) auto then have "n+1 \ L" - by (simp add: ln_div) + using \0 < L\ by (simp add: ln_div) then show ?thesis using L_le by linarith qed diff -r 532156e8f15f -r 6dec6b1f31f5 src/HOL/Nonstandard_Analysis/HLog.thy --- a/src/HOL/Nonstandard_Analysis/HLog.thy Sun Jul 07 22:25:34 2024 +0100 +++ b/src/HOL/Nonstandard_Analysis/HLog.thy Mon Jul 08 22:27:50 2024 +0100 @@ -73,7 +73,7 @@ by transfer simp lemma hlog_mult: - "\a x y. 0 < a \ a \ 1 \ (x\0 \ y\0) \ hlog a (x * y) = hlog a x + hlog a y" + "\a x y. hlog a (x * y) = (if x\0 \ y\0 then hlog a x + hlog a y else 0)" by transfer (rule log_mult) lemma hlog_as_starfun: "\a x. 0 < a \ a \ 1 \ hlog a x = ( *f* ln) x / ( *f* ln) a" @@ -111,10 +111,10 @@ lemma hlog_eq_one [simp]: "\a. 0 < a \ a \ 1 \ hlog a a = 1" by transfer (rule log_eq_one) -lemma hlog_inverse: "0 < a \ a \ 1 \ 0 < x \ hlog a (inverse x) = - hlog a x" - by (rule add_left_cancel [of "hlog a x", THEN iffD1]) (simp add: hlog_mult [symmetric]) +lemma hlog_inverse: "\a x. hlog a (inverse x) = - hlog a x" + by transfer (simp add: log_inverse) -lemma hlog_divide: "0 < a \ a \ 1 \ 0 < x \ 0 < y \ hlog a (x / y) = hlog a x - hlog a y" +lemma hlog_divide: "hlog a (x / y) = (if x\0 \ y\0 then hlog a x - hlog a y else 0)" by (simp add: hlog_mult hlog_inverse divide_inverse) lemma hlog_less_cancel_iff [simp]: diff -r 532156e8f15f -r 6dec6b1f31f5 src/HOL/Probability/Information.thy --- a/src/HOL/Probability/Information.thy Sun Jul 07 22:25:34 2024 +0100 +++ b/src/HOL/Probability/Information.thy Mon Jul 08 22:27:50 2024 +0100 @@ -10,15 +10,6 @@ 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 + @@ -554,11 +545,8 @@ 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) + using A B + by (auto simp: f_def field_simps space_pair_measure log_mult log_divide) qed show "0 \ ?M" unfolding M @@ -1097,9 +1085,7 @@ 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 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) + by (auto simp: log_mult log_divide field_simps) then show "integrable ?P (\x. - log b (?f x))" by (subst integrable_real_density) (auto simp: space_pair_measure) @@ -1112,9 +1098,7 @@ apply simp apply (intro integral_cong_AE) using ae1 ae2 ae3 ae4 - 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) + by (auto simp: field_simps log_divide) finally show ?nonneg by simp qed @@ -1214,10 +1198,7 @@ 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 - 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) + by (auto simp: log_divide log_mult field_simps) 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))"] @@ -1230,42 +1211,8 @@ 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 - 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 - + apply(auto simp: field_simps log_divide log_mult) + done from ae I1 I2 show ?eq unfolding conditional_mutual_information_def mi_eq apply (subst mutual_information_distr[OF S TP Px Px_nn Pyz Pyz_nn Pxyz Pxyz_nn]; simp add: space_pair_measure) @@ -1372,14 +1319,8 @@ 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 - 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))" + by (auto simp: log_divide field_simps) + then show "integrable ?P (\x. - log b (?f x))" using Pxyz_nn by (auto simp: integrable_real_density) qed (auto simp: b_gt_1 minus_log_convex) also have "\ = conditional_mutual_information b S T P X Y Z" @@ -1391,10 +1332,7 @@ apply simp apply (intro integral_cong_AE) using ae1 ae2 ae3 ae4 - 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) + by (auto simp: log_divide zero_less_mult_iff field_simps) finally show ?nonneg by simp qed diff -r 532156e8f15f -r 6dec6b1f31f5 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Sun Jul 07 22:25:34 2024 +0100 +++ b/src/HOL/Transcendental.thy Mon Jul 08 22:27:50 2024 +0100 @@ -1626,7 +1626,7 @@ 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" +lemma ln_mult: "ln (x * y) = (if x\0 \ y\0 then ln x + ln y else 0)" for x :: real by (simp add: ln_real_def abs_mult raw_ln_mult) @@ -1642,7 +1642,7 @@ 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" +lemma ln_div: "ln (x/y) = (if x\0 \ y\0 then ln x - ln y else 0)" for x :: real by (simp add: divide_inverse ln_inverse ln_mult) @@ -2121,7 +2121,7 @@ corollary ln_diff_le: "0 < x \ 0 < y \ ln x - ln y \ (x - y) / y" for x :: real - by (simp add: ln_div [symmetric] diff_divide_distrib ln_le_minus_one) +by (metis diff_divide_distrib divide_pos_pos divide_self ln_divide_pos ln_le_minus_one order_less_irrefl) lemma ln_eq_minus_one: fixes x :: real @@ -2510,7 +2510,7 @@ by auto lemma log_mult: - "(x\0 \ y\0) \ log a (x * y) = log a x + log a y" + "log a (x * y) = (if x\0 \ y\0 then log a x + log a y else 0)" by (simp add: log_def ln_mult divide_inverse distrib_right) lemma log_mult_pos: @@ -2541,7 +2541,7 @@ by (simp add: divide_inverse log_inverse) lemma log_divide: - "(x\0 \ y\0) \ log a (x / y) = log a x - log a y" + "log a (x / y) = (if x\0 \ y\0 then log a x - log a y else 0)" by (simp add: diff_divide_distrib ln_div log_def) lemma log_divide_pos: @@ -2839,7 +2839,7 @@ by (metis ln_powr mult_1 powr_inverse_root powr_one' times_divide_eq_left) lemma ln_sqrt: "0 \ x \ ln (sqrt x) = ln x / 2" - by (smt (verit) field_sum_of_halves ln_mult real_sqrt_mult_self) + by (metis (full_types) divide_inverse inverse_eq_divide ln_powr mult.commute of_nat_numeral pos2 root_powr_inverse sqrt_def) lemma log_root: "n > 0 \ a \ 0 \ log b (root n a) = log b a / n" by (simp add: log_def ln_root)