1.1 --- a/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:35 2012 +0200
     1.2 +++ b/src/HOL/Probability/Information.thy	Wed Oct 10 12:12:36 2012 +0200
     1.3 @@ -1367,6 +1367,20 @@
     1.4    finally show ?thesis ..
     1.5  qed
     1.6  
     1.7 +lemma (in information_space) mutual_information_eq_entropy_conditional_entropy':
     1.8 +  fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real" and Pxy :: "('b \<times> 'c) \<Rightarrow> real"
     1.9 +  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
    1.10 +  assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
    1.11 +  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
    1.12 +  assumes Ix: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Px (fst x)))"
    1.13 +  assumes Iy: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Py (snd x)))"
    1.14 +  assumes Ixy: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Pxy x))"
    1.15 +  shows  "mutual_information b S T X Y = entropy b S X - conditional_entropy b S T X Y"
    1.16 +  using
    1.17 +    mutual_information_eq_entropy_conditional_entropy_distr[OF S T Px Py Pxy Ix Iy Ixy]
    1.18 +    conditional_entropy_eq_entropy[OF S T Py Pxy Ixy Iy]
    1.19 +  by simp
    1.20 +
    1.21  lemma (in information_space) mutual_information_eq_entropy_conditional_entropy:
    1.22    assumes sf_X: "simple_function M X" and sf_Y: "simple_function M Y"
    1.23    shows  "\<I>(X ; Y) = \<H>(X) - \<H>(X | Y)"