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)"