src/HOL/Probability/Information.thy
 changeset 39092 98de40859858 parent 38656 d5d342611edb child 39097 943c7b348524
```     1.1 --- a/src/HOL/Probability/Information.thy	Fri Aug 27 16:23:51 2010 +0200
1.2 +++ b/src/HOL/Probability/Information.thy	Thu Sep 02 17:12:40 2010 +0200
1.3 @@ -359,6 +359,48 @@
1.4    "(\<Sum>x\<in>A \<times> B. f x) = (\<Sum>x\<in>A. setsum (\<lambda>y. f (x, y)) B)"
1.5    unfolding setsum_cartesian_product by simp
1.6
1.7 +lemma (in finite_information_space) mutual_information_generic_eq:
1.8 +  assumes MX: "finite_measure_space MX (distribution X)"
1.9 +  assumes MY: "finite_measure_space MY (distribution Y)"
1.10 +  shows "mutual_information b MX MY X Y = (\<Sum> (x,y) \<in> space MX \<times> space MY.
1.11 +      real (joint_distribution X Y {(x,y)}) *
1.12 +      log b (real (joint_distribution X Y {(x,y)}) /
1.13 +      (real (distribution X {x}) * real (distribution Y {y}))))"
1.14 +proof -
1.15 +  let ?P = "prod_measure_space MX MY"
1.16 +  let ?\<mu> = "prod_measure MX (distribution X) MY (distribution Y)"
1.17 +  let ?\<nu> = "joint_distribution X Y"
1.18 +  interpret X: finite_measure_space MX "distribution X" by fact
1.19 +  moreover interpret Y: finite_measure_space MY "distribution Y" by fact
1.20 +  have fms: "finite_measure_space MX (distribution X)"
1.21 +            "finite_measure_space MY (distribution Y)" by fact+
1.22 +  have fms_P: "finite_measure_space ?P ?\<mu>"
1.23 +    by (rule X.finite_measure_space_finite_prod_measure) fact
1.24 +  then interpret P: finite_measure_space ?P ?\<mu> .
1.25 +  have fms_P': "finite_measure_space ?P ?\<nu>"
1.26 +      using finite_product_measure_space[of "space MX" "space MY"]
1.27 +        X.finite_space Y.finite_space sigma_prod_sets_finite[OF X.finite_space Y.finite_space]
1.28 +        X.sets_eq_Pow Y.sets_eq_Pow
1.29 +      by (simp add: prod_measure_space_def sigma_def)
1.30 +  then interpret P': finite_measure_space ?P ?\<nu> .
1.31 +  { fix x assume "x \<in> space ?P"
1.32 +    hence in_MX: "{fst x} \<in> sets MX" "{snd x} \<in> sets MY" using X.sets_eq_Pow Y.sets_eq_Pow
1.33 +      by (auto simp: prod_measure_space_def)
1.34 +    assume "?\<mu> {x} = 0"
1.35 +    with X.finite_prod_measure_times[OF fms(2), of "{fst x}" "{snd x}"] in_MX
1.36 +    have "distribution X {fst x} = 0 \<or> distribution Y {snd x} = 0"
1.37 +      by (simp add: prod_measure_space_def)
1.38 +    hence "joint_distribution X Y {x} = 0"
1.39 +      by (cases x) (auto simp: distribution_order) }
1.40 +  note measure_0 = this
1.41 +  show ?thesis
1.42 +    unfolding Let_def mutual_information_def
1.43 +    using measure_0 fms_P fms_P' MX MY P.absolutely_continuous_def
1.44 +    by (subst P.KL_divergence_eq_finite)
1.45 +       (auto simp add: prod_measure_space_def prod_measure_times_finite
1.46 +         finite_prob_space_eq setsum_cartesian_product' real_of_pinfreal_mult[symmetric])
1.47 +qed
1.48 +
1.49  lemma (in finite_information_space)
1.50    assumes MX: "finite_prob_space MX (distribution X)"
1.51    assumes MY: "finite_prob_space MY (distribution Y)"
```