src/HOL/Probability/Information.thy

 header {*Information theory*}
 
 theory Information
 imports
   Independent_Family
-  Distributions
   "~~/src/HOL/Library/Convex"
 begin
 
 lemma log_le: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log a x \<le> log a y"
   by (subst log_le_cancel_iff) auto

     by (intro integral_cong) (auto split: split_indicator simp: log_divide_eq)
   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]
     by (subst integral_mult_right) (auto simp: measure_def)
-qed
-
-lemma (in information_space) entropy_exponential:
-  assumes D: "distributed M lborel X (exponential_density l)"
-  shows "entropy b lborel X = log b (exp 1 / l)"
-proof -
-  have l[simp, arith]: "0 < l" by (rule exponential_distributed_params[OF D])
- 
-  have [simp]: "integrable lborel (exponential_density l)"
-    using distributed_integrable[OF D, of "\<lambda>_. 1"] by simp
-
-  have [simp]: "integral\<^sup>L lborel (exponential_density l) = 1"
-    using distributed_integral[OF D, of "\<lambda>_. 1"] by (simp add: prob_space)
-    
-  have [simp]: "integrable lborel (\<lambda>x. exponential_density l x * x)"
-    using erlang_ith_moment_integrable[OF l D, of 1] distributed_integrable[OF D, of "\<lambda>x. x"] by simp
-
-  have [simp]: "integral\<^sup>L lborel (\<lambda>x. exponential_density l x * x) = 1 / l"
-    using erlang_ith_moment[OF l D, of 1] distributed_integral[OF D, of "\<lambda>x. x"] by simp
-    
-  have "entropy b lborel X = - (\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel)"
-    using D by (rule entropy_distr)
-  also have "(\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel) = 
-    (\<integral> x. (ln l * exponential_density l x - l * (exponential_density l x * x)) / ln b \<partial>lborel)"
-    by (intro integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps)
-  also have "\<dots> = (ln l - 1) / ln b"
-    by simp
-  finally show ?thesis
-    by (simp add: log_def divide_simps ln_div)
 qed
 
 lemma (in information_space) entropy_simple_distributed:
   "simple_distributed M X f \<Longrightarrow> \<H>(X) = - (\<Sum>x\<in>X`space M. f x * log b (f x))"
   by (subst entropy_distr[OF simple_distributed])