remove duplicate theorem setsum_real_distribution
authorhoelzl
Thu Dec 01 14:03:57 2011 +0100 (2011-12-01)
changeset 4571010192f961619
parent 45708 7c8bed80301f
child 45711 a2c32e196d49
remove duplicate theorem setsum_real_distribution
src/HOL/Probability/Information.thy
     1.1 --- a/src/HOL/Probability/Information.thy	Thu Dec 01 13:34:16 2011 +0100
     1.2 +++ b/src/HOL/Probability/Information.thy	Thu Dec 01 14:03:57 2011 +0100
     1.3 @@ -1020,13 +1020,6 @@
     1.4    using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV \<rparr>" "\<lambda>x. ()" "{()}"]
     1.5    using sigma_algebra_Pow[of "UNIV::unit set" "()"] by simp
     1.6  
     1.7 -lemma (in prob_space) setsum_real_distribution:
     1.8 -  fixes MX :: "('c, 'd) measure_space_scheme"
     1.9 -  assumes X: "finite_random_variable MX X" shows "(\<Sum>a\<in>space MX. distribution X {a}) = 1"
    1.10 -  using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV, measure = undefined \<rparr>" "\<lambda>x. ()" "{()}"]
    1.11 -  using sigma_algebra_Pow[of "UNIV::unit set" "\<lparr> measure = undefined \<rparr>"]
    1.12 -  by auto
    1.13 -
    1.14  lemma (in information_space) conditional_mutual_information_generic_positive:
    1.15    assumes X: "finite_random_variable MX X" and Y: "finite_random_variable MY Y" and Z: "finite_random_variable MZ Z"
    1.16    shows "0 \<le> conditional_mutual_information b MX MY MZ X Y Z"
    1.17 @@ -1101,7 +1094,7 @@
    1.18                     setsum_joint_distribution_singleton[OF Y Z]
    1.19            intro!: setsum_cong)
    1.20    also have "log b (\<Sum>z\<in>space MZ. ?dZ {z}) = 0"
    1.21 -    unfolding setsum_real_distribution[OF Z] by simp
    1.22 +    unfolding setsum_distribution[OF Z] by simp
    1.23    finally show ?thesis by simp
    1.24  qed
    1.25