Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Probability/Information.thy
changeset 80034 95b4fb2b5359
parent 79772 817d33f8aa7f 
--- a/src/HOL/Probability/Information.thy	Wed Mar 27 10:54:47 2024 +0100
+++ b/src/HOL/Probability/Information.thy	Wed Mar 27 15:16:09 2024 +0000
@@ -857,7 +857,7 @@
     using int X by (intro entropy_le) auto
   also have "\<dots> \<le> log b (measure MX (space MX))"
     using Px distributed_imp_emeasure_nonzero[OF X]
-    by (intro log_le)
+    by (intro Transcendental.log_mono)
        (auto intro!: finite_measure_mono b_gt_1 less_le[THEN iffD2]
              simp: emeasure_eq_measure cong: conj_cong)
   finally show ?thesis .
@@ -1087,7 +1087,7 @@
     done
 
   have "- log b 1 \<le> - log b (integral\<^sup>L ?P ?f)"
-  proof (intro le_imp_neg_le log_le[OF b_gt_1])
+  proof (intro le_imp_neg_le Transcendental.log_mono[OF b_gt_1])
     have If: "integrable ?P ?f"
       unfolding real_integrable_def
     proof (intro conjI)
@@ -1332,7 +1332,7 @@
     by (auto simp: split_beta')
 
   have "- log b 1 \<le> - log b (integral\<^sup>L ?P ?f)"
-  proof (intro le_imp_neg_le log_le[OF b_gt_1])
+  proof (intro le_imp_neg_le Transcendental.log_mono[OF b_gt_1])
     have If: "integrable ?P ?f"
       using neg fin by (force simp add: real_integrable_def)
     then have "(\<integral>\<^sup>+ x. ?f x \<partial>?P) = (\<integral>x. ?f x \<partial>?P)"
isabelle