src/HOL/Probability/Information.thy
changeset 45712 852597248663
parent 45710 10192f961619
child 45777 c36637603821
     1.1 --- a/src/HOL/Probability/Information.thy	Thu Dec 01 14:03:57 2011 +0100
     1.2 +++ b/src/HOL/Probability/Information.thy	Thu Dec 01 14:03:57 2011 +0100
     1.3 @@ -1009,17 +1009,6 @@
     1.4      by (simp add: setsum_cartesian_product' distribution_remove_const)
     1.5  qed
     1.6  
     1.7 -lemma (in prob_space) distribution_unit[simp]: "distribution (\<lambda>x. ()) {()} = 1"
     1.8 -  unfolding distribution_def using prob_space by auto
     1.9 -
    1.10 -lemma (in prob_space) joint_distribution_unit[simp]: "distribution (\<lambda>x. (X x, ())) {(a, ())} = distribution X {a}"
    1.11 -  unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
    1.12 -
    1.13 -lemma (in prob_space) setsum_distribution:
    1.14 -  assumes X: "finite_random_variable MX X" shows "(\<Sum>a\<in>space MX. distribution X {a}) = 1"
    1.15 -  using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV \<rparr>" "\<lambda>x. ()" "{()}"]
    1.16 -  using sigma_algebra_Pow[of "UNIV::unit set" "()"] by simp
    1.17 -
    1.18  lemma (in information_space) conditional_mutual_information_generic_positive:
    1.19    assumes X: "finite_random_variable MX X" and Y: "finite_random_variable MY Y" and Z: "finite_random_variable MZ Z"
    1.20    shows "0 \<le> conditional_mutual_information b MX MY MZ X Y Z"