# HG changeset patch
# User hoelzl
# Date 1349863956 -7200
# Node ID dd8dffaf84b91ef7e45aeaac0c4efae2cdf9a427
# Parent  f3471f09bb86d0dcd08b198d02ed830249d5af6e
continuous version of mutual_information_eq_entropy_conditional_entropy

diff -r f3471f09bb86 -r dd8dffaf84b9 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:35 2012 +0200
+++ b/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:36 2012 +0200
@@ -1367,6 +1367,20 @@
   finally show ?thesis ..
 qed
 
+lemma (in information_space) mutual_information_eq_entropy_conditional_entropy':
+  fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real" and Pxy :: "('b \<times> 'c) \<Rightarrow> real"
+  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
+  assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
+  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
+  assumes Ix: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Px (fst x)))"
+  assumes Iy: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Py (snd x)))"
+  assumes Ixy: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Pxy x))"
+  shows  "mutual_information b S T X Y = entropy b S X - conditional_entropy b S T X Y"
+  using
+    mutual_information_eq_entropy_conditional_entropy_distr[OF S T Px Py Pxy Ix Iy Ixy]
+    conditional_entropy_eq_entropy[OF S T Py Pxy Ixy Iy]
+  by simp
+
 lemma (in information_space) mutual_information_eq_entropy_conditional_entropy:
   assumes sf_X: "simple_function M X" and sf_Y: "simple_function M Y"
   shows  "\<I>(X ; Y) = \<H>(X) - \<H>(X | Y)"