# HG changeset patch
# User hoelzl
# Date 1349863944 -7200
# Node ID 0a8adca22974bd527d4601a9bf3c9a9e7f680b62
# Parent  5e5b2da42a69909304c5ad16aaf5a77adeb9383a
simplified entropy_uniform

diff -r 5e5b2da42a69 -r 0a8adca22974 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:23 2012 +0200
+++ b/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:24 2012 +0200
@@ -666,41 +666,75 @@
 
 lemma (in information_space) entropy_distr:
   fixes X :: "'a \<Rightarrow> 'b"
-  assumes "sigma_finite_measure MX" and X: "distributed M MX X f"
+  assumes X: "distributed M MX X f"
   shows "entropy b MX X = - (\<integral>x. f x * log b (f x) \<partial>MX)"
+  unfolding entropy_def KL_divergence_def entropy_density_def comp_def
+proof (subst integral_cong_AE)
+  note D = distributed_measurable[OF X] distributed_borel_measurable[OF X] distributed_AE[OF X]
+  interpret X: prob_space "distr M MX X"
+    using D(1) by (rule prob_space_distr)
+
+  have sf: "sigma_finite_measure (distr M MX X)" by default
+  have ae: "AE x in MX. f x = RN_deriv MX (density MX f) x"
+    using D
+    by (intro RN_deriv_unique_sigma_finite)
+       (auto intro: divide_nonneg_nonneg measure_nonneg
+             simp: distributed_distr_eq_density[symmetric, OF X] sf)
+  show "AE x in distr M MX X. log b (real (RN_deriv MX (distr M MX X) x)) =
+    log b (f x)"
+    unfolding distributed_distr_eq_density[OF X]
+    apply (subst AE_density)
+    using D apply simp
+    using ae apply eventually_elim
+    apply (subst (asm) eq_commute)
+    apply auto
+    done
+  show "- (\<integral> x. log b (f x) \<partial>distr M MX X) = - (\<integral> x. f x * log b (f x) \<partial>MX)"
+    unfolding distributed_distr_eq_density[OF X]
+    using D
+    by (subst integral_density)
+       (auto simp: borel_measurable_ereal_iff)
+qed 
+
+lemma (in prob_space) uniform_distributed_params:
+  assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)"
+  shows "A \<in> sets MX" "measure MX A \<noteq> 0"
 proof -
-  interpret MX: sigma_finite_measure MX by fact
-  from X show ?thesis
-    unfolding entropy_def X[THEN distributed_distr_eq_density]
-    by (subst MX.KL_density[OF b_gt_1]) (simp_all add: distributed_real_AE distributed_real_measurable)
+  interpret X: prob_space "distr M MX X"
+    using distributed_measurable[OF X] by (rule prob_space_distr)
+
+  show "measure MX A \<noteq> 0"
+  proof
+    assume "measure MX A = 0"
+    with X.emeasure_space_1 X.prob_space distributed_distr_eq_density[OF X]
+    show False
+      by (simp add: emeasure_density zero_ereal_def[symmetric])
+  qed
+  with measure_notin_sets[of A MX] show "A \<in> sets MX"
+    by blast
 qed
 
 lemma (in information_space) entropy_uniform:
-  assumes "sigma_finite_measure MX"
-  assumes A: "A \<in> sets MX" "emeasure MX A \<noteq> 0" "emeasure MX A \<noteq> \<infinity>"
-  assumes X: "distributed M MX X (\<lambda>x. 1 / measure MX A * indicator A x)"
+  assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)" (is "distributed _ _ _ ?f")
   shows "entropy b MX X = log b (measure MX A)"
-proof (subst entropy_distr[OF _ X])
-  let ?f = "\<lambda>x. 1 / measure MX A * indicator A x"
-  have "- (\<integral>x. ?f x * log b (?f x) \<partial>MX) = 
-    - (\<integral>x. (log b (1 / measure MX A) / measure MX A) * indicator A x \<partial>MX)"
-    by (auto intro!: integral_cong simp: indicator_def)
-  also have "\<dots> = - log b (inverse (measure MX A))"
-    using A by (subst integral_cmult(2))
-               (simp_all add: measure_def real_of_ereal_eq_0 integral_cmult inverse_eq_divide)
-  also have "\<dots> = log b (measure MX A)"
-    using b_gt_1 A by (subst log_inverse) (auto simp add: measure_def less_le real_of_ereal_eq_0
-                                                          emeasure_nonneg real_of_ereal_pos)
-  finally show "- (\<integral>x. ?f x * log b (?f x) \<partial>MX) = log b (measure MX A)" by simp
-qed fact+
+proof (subst entropy_distr[OF X])
+  have [simp]: "emeasure MX A \<noteq> \<infinity>"
+    using uniform_distributed_params[OF X] by (auto simp add: measure_def)
+  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 measure_nonneg[of MX A] uniform_distributed_params[OF X]
+    by (auto intro!: integral_cong 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 lebesgue_integral_cmult) (auto simp: measure_def)
+qed
 
 lemma (in information_space) entropy_simple_distributed:
   fixes X :: "'a \<Rightarrow> 'b"
   assumes X: "simple_distributed M X f"
   shows "\<H>(X) = - (\<Sum>x\<in>X`space M. f x * log b (f x))"
-proof (subst entropy_distr[OF _ simple_distributed[OF X]])
-  show "sigma_finite_measure (count_space (X ` space M))"
-    using X by (simp add: sigma_finite_measure_count_space_finite simple_distributed_def)
+proof (subst entropy_distr[OF simple_distributed[OF X]])
   show "- (\<integral>x. f x * log b (f x) \<partial>(count_space (X`space M))) = - (\<Sum>x\<in>X ` space M. f x * log b (f x))"
     using X by (auto simp add: lebesgue_integral_count_space_finite)
 qed
diff -r 5e5b2da42a69 -r 0a8adca22974 src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Wed Oct 10 12:12:23 2012 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Oct 10 12:12:24 2012 +0200
@@ -776,15 +776,16 @@
   assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   assumes pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
   and fin: "integral\<^isup>P M f \<noteq> \<infinity>"
-  shows "(\<forall>A\<in>sets M. (\<integral>\<^isup>+x. f x * indicator A x \<partial>M) = (\<integral>\<^isup>+x. g x * indicator A x \<partial>M))
-    \<longleftrightarrow> (AE x in M. f x = g x)"
-    (is "(\<forall>A\<in>sets M. ?P f A = ?P g A) \<longleftrightarrow> _")
+  shows "density M f = density M g \<longleftrightarrow> (AE x in M. f x = g x)"
 proof (intro iffI ballI)
   fix A assume eq: "AE x in M. f x = g x"
-  then show "?P f A = ?P g A"
-    by (auto intro: positive_integral_cong_AE)
+  with borel show "density M f = density M g"
+    by (auto intro: density_cong)
 next
-  assume eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
+  let ?P = "\<lambda>f A. \<integral>\<^isup>+ x. f x * indicator A x \<partial>M"
+  assume "density M f = density M g"
+  with borel have eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
+    by (simp add: emeasure_density[symmetric])
   from this[THEN bspec, OF top] fin
   have g_fin: "integral\<^isup>P M g \<noteq> \<infinity>" by (simp cong: positive_integral_cong)
   { fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
@@ -844,7 +845,7 @@
     unfolding indicator_def by auto
   have "\<forall>i. AE x in M. ?f (Q i) x = ?f' (Q i) x" using borel Q_fin Q pos
     by (intro finite_density_unique[THEN iffD1] allI)
-       (auto intro!: borel_measurable_ereal_times f Int simp: *)
+       (auto intro!: borel_measurable_ereal_times f measure_eqI Int simp: emeasure_density * subset_eq)
   moreover have "AE x in M. ?f Q0 x = ?f' Q0 x"
   proof (rule AE_I')
     { fix f :: "'a \<Rightarrow> ereal" assume borel: "f \<in> borel_measurable M"
@@ -933,6 +934,41 @@
   shows "density M f = density M f' \<longleftrightarrow> (AE x in M. f x = f' x)"
   using density_unique[OF assms] density_cong[OF f f'] by auto
 
+lemma sigma_finite_density_unique:
+  assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
+  assumes pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
+  and fin: "sigma_finite_measure (density M f)"
+  shows "density M f = density M g \<longleftrightarrow> (AE x in M. f x = g x)"
+proof
+  assume "AE x in M. f x = g x" with borel show "density M f = density M g" 
+    by (auto intro: density_cong)
+next
+  assume eq: "density M f = density M g"
+  interpret f!: sigma_finite_measure "density M f" by fact
+  from f.sigma_finite_incseq guess A . note cover = this
+
+  have "AE x in M. \<forall>i. x \<in> A i \<longrightarrow> f x = g x"
+    unfolding AE_all_countable
+  proof
+    fix i
+    have "density (density M f) (indicator (A i)) = density (density M g) (indicator (A i))"
+      unfolding eq ..
+    moreover have "(\<integral>\<^isup>+x. f x * indicator (A i) x \<partial>M) \<noteq> \<infinity>"
+      using cover(1) cover(3)[of i] borel by (auto simp: emeasure_density subset_eq)
+    ultimately have "AE x in M. f x * indicator (A i) x = g x * indicator (A i) x"
+      using borel pos cover(1) pos
+      by (intro finite_density_unique[THEN iffD1])
+         (auto simp: density_density_eq subset_eq)
+    then show "AE x in M. x \<in> A i \<longrightarrow> f x = g x"
+      by auto
+  qed
+  with AE_space show "AE x in M. f x = g x"
+    apply eventually_elim
+    using cover(2)[symmetric]
+    apply auto
+    done
+qed
+
 lemma (in sigma_finite_measure) sigma_finite_iff_density_finite':
   assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
   shows "sigma_finite_measure (density M f) \<longleftrightarrow> (AE x in M. f x \<noteq> \<infinity>)"
@@ -1076,15 +1112,17 @@
   assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
   and eq: "density M f = N"
   shows "AE x in M. f x = RN_deriv M N x"
-proof (rule density_unique)
-  have ac: "absolutely_continuous M N"
-    using f(1) unfolding eq[symmetric] by (rule absolutely_continuousI_density)
-  have eq2: "sets N = sets M"
-    unfolding eq[symmetric] by simp
-  show "RN_deriv M N \<in> borel_measurable M" "AE x in M. 0 \<le> RN_deriv M N x"
-    "density M f = density M (RN_deriv M N)"
-    using RN_deriv[OF ac eq2] eq by auto
-qed fact+
+  unfolding eq[symmetric]
+  by (intro density_unique_iff[THEN iffD1] f borel_measurable_RN_deriv_density
+            RN_deriv_density_nonneg[THEN AE_I2] density_RN_deriv_density[symmetric])
+
+lemma RN_deriv_unique_sigma_finite:
+  assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
+  and eq: "density M f = N" and fin: "sigma_finite_measure N"
+  shows "AE x in M. f x = RN_deriv M N x"
+  using fin unfolding eq[symmetric]
+  by (intro sigma_finite_density_unique[THEN iffD1] f borel_measurable_RN_deriv_density
+            RN_deriv_density_nonneg[THEN AE_I2] density_RN_deriv_density[symmetric])
 
 lemma (in sigma_finite_measure) RN_deriv_distr:
   fixes T :: "'a \<Rightarrow> 'b"