# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1720266691 -3600
# Node ID 5c691b178e08a8a0911cd686aa60744fe10ff6a5
# Parent  b0d590e755927d00ed628403ea141b966da45e1a
Totalisation of ln and therefore log and powr

diff -r b0d590e75592 -r 5c691b178e08 src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Fri Jul 05 21:59:43 2024 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy	Sat Jul 06 12:51:31 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"
diff -r b0d590e75592 -r 5c691b178e08 src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Fri Jul 05 21:59:43 2024 +0100
+++ b/src/HOL/Analysis/Infinite_Products.thy	Sat Jul 06 12:51:31 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: 
diff -r b0d590e75592 -r 5c691b178e08 src/HOL/Analysis/Kronecker_Approximation_Theorem.thy
--- a/src/HOL/Analysis/Kronecker_Approximation_Theorem.thy	Fri Jul 05 21:59:43 2024 +0100
+++ b/src/HOL/Analysis/Kronecker_Approximation_Theorem.thy	Sat Jul 06 12:51:31 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"
diff -r b0d590e75592 -r 5c691b178e08 src/HOL/Analysis/Weierstrass_Theorems.thy
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Fri Jul 05 21:59:43 2024 +0100
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Sat Jul 06 12:51:31 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
diff -r b0d590e75592 -r 5c691b178e08 src/HOL/Complex_Analysis/Great_Picard.thy
--- a/src/HOL/Complex_Analysis/Great_Picard.thy	Fri Jul 05 21:59:43 2024 +0100
+++ b/src/HOL/Complex_Analysis/Great_Picard.thy	Sat Jul 06 12:51:31 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
diff -r b0d590e75592 -r 5c691b178e08 src/HOL/Decision_Procs/Approximation_Bounds.thy
--- a/src/HOL/Decision_Procs/Approximation_Bounds.thy	Fri Jul 05 21:59:43 2024 +0100
+++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy	Sat Jul 06 12:51:31 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)
   }
diff -r b0d590e75592 -r 5c691b178e08 src/HOL/Nonstandard_Analysis/HLog.thy
--- a/src/HOL/Nonstandard_Analysis/HLog.thy	Fri Jul 05 21:59:43 2024 +0100
+++ b/src/HOL/Nonstandard_Analysis/HLog.thy	Sat Jul 06 12:51:31 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"
diff -r b0d590e75592 -r 5c691b178e08 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Fri Jul 05 21:59:43 2024 +0100
+++ b/src/HOL/Probability/Information.thy	Sat Jul 06 12:51:31 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
 
diff -r b0d590e75592 -r 5c691b178e08 src/HOL/Real_Asymp/Multiseries_Expansion.thy
--- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy	Fri Jul 05 21:59:43 2024 +0100
+++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy	Sat Jul 06 12:51:31 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
diff -r b0d590e75592 -r 5c691b178e08 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri Jul 05 21:59:43 2024 +0100
+++ b/src/HOL/Transcendental.thy	Sat Jul 06 12:51:31 2024 +0100
@@ -1630,6 +1630,10 @@
   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)
@@ -1642,6 +1646,10 @@
   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 (simp add: divide_inverse ln_inverse ln_mult)
+
 lemma ln_realpow: "ln (x^n) = real n * ln x"
 proof (cases "x=0")
   case True
@@ -2509,6 +2517,10 @@
   "(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:
   "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log a x = (ln b/ln a) * log b x"
   by (simp add: log_def divide_inverse)
@@ -2526,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