--- a/src/HOL/Probability/Information.thy Thu Dec 01 14:03:57 2011 +0100
+++ b/src/HOL/Probability/Information.thy Thu Dec 01 14:03:57 2011 +0100
@@ -1009,17 +1009,6 @@
by (simp add: setsum_cartesian_product' distribution_remove_const)
qed
-lemma (in prob_space) distribution_unit[simp]: "distribution (\<lambda>x. ()) {()} = 1"
- unfolding distribution_def using prob_space by auto
-
-lemma (in prob_space) joint_distribution_unit[simp]: "distribution (\<lambda>x. (X x, ())) {(a, ())} = distribution X {a}"
- unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
-
-lemma (in prob_space) setsum_distribution:
- assumes X: "finite_random_variable MX X" shows "(\<Sum>a\<in>space MX. distribution X {a}) = 1"
- using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV \<rparr>" "\<lambda>x. ()" "{()}"]
- using sigma_algebra_Pow[of "UNIV::unit set" "()"] by simp
-
lemma (in information_space) conditional_mutual_information_generic_positive:
assumes X: "finite_random_variable MX X" and Y: "finite_random_variable MY Y" and Z: "finite_random_variable MZ Z"
shows "0 \<le> conditional_mutual_information b MX MY MZ X Y Z"
--- a/src/HOL/Probability/Probability_Measure.thy Thu Dec 01 14:03:57 2011 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Thu Dec 01 14:03:57 2011 +0100
@@ -70,6 +70,12 @@
"joint_distribution X X {(x, x)} = distribution X {x}"
unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
+lemma (in prob_space) distribution_unit[simp]: "distribution (\<lambda>x. ()) {()} = 1"
+ unfolding distribution_def using prob_space by auto
+
+lemma (in prob_space) joint_distribution_unit[simp]: "distribution (\<lambda>x. (X x, ())) {(a, ())} = distribution X {a}"
+ unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
+
lemma (in prob_space) not_empty: "space M \<noteq> {}"
using prob_space empty_measure' by auto
@@ -743,6 +749,11 @@
finite_random_variableD[OF Y(1)]
finite_random_variable_imp_sets[OF Y]] by simp
+lemma (in prob_space) setsum_distribution:
+ assumes X: "finite_random_variable MX X" shows "(\<Sum>a\<in>space MX. distribution X {a}) = 1"
+ using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV \<rparr>" "\<lambda>x. ()" "{()}"]
+ using sigma_algebra_Pow[of "UNIV::unit set" "()"] by simp
+
locale pair_finite_prob_space = M1: finite_prob_space M1 + M2: finite_prob_space M2 for M1 M2
sublocale pair_finite_prob_space \<subseteq> pair_prob_space M1 M2 by default
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Thu Dec 01 14:03:57 2011 +0100
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Thu Dec 01 14:03:57 2011 +0100
@@ -75,13 +75,6 @@
qed
qed
-lemma (in prob_space)
- assumes "finite (X`space M)"
- shows "bij_betw (ordered_variable_partition X) {0..<card (X`space M)} (X`space M)"
- and "\<And>i j. \<lbrakk> i < card (X`space M) ; j < card (X`space M) ; i \<le> j \<rbrakk> \<Longrightarrow>
- distribution X {ordered_variable_partition X i} \<le> distribution X {ordered_variable_partition X j}"
- oops
-
definition (in prob_space)
"order_distribution X i = real (distribution X {ordered_variable_partition X i})"