author hoelzl Thu Dec 01 14:03:57 2011 +0100 (2011-12-01) changeset 45712 852597248663 parent 45711 a2c32e196d49 child 45713 badee348c5fb
moved theorems about distribution to the definition; removed oopsed-lemma
```     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"
```
```     2.1 --- a/src/HOL/Probability/Probability_Measure.thy	Thu Dec 01 14:03:57 2011 +0100
2.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Thu Dec 01 14:03:57 2011 +0100
2.3 @@ -70,6 +70,12 @@
2.4      "joint_distribution X X {(x, x)} = distribution X {x}"
2.5    unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
2.6
2.7 +lemma (in prob_space) distribution_unit[simp]: "distribution (\<lambda>x. ()) {()} = 1"
2.8 +  unfolding distribution_def using prob_space by auto
2.9 +
2.10 +lemma (in prob_space) joint_distribution_unit[simp]: "distribution (\<lambda>x. (X x, ())) {(a, ())} = distribution X {a}"
2.11 +  unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
2.12 +
2.13  lemma (in prob_space) not_empty: "space M \<noteq> {}"
2.14    using prob_space empty_measure' by auto
2.15
2.16 @@ -743,6 +749,11 @@
2.17      finite_random_variableD[OF Y(1)]
2.18      finite_random_variable_imp_sets[OF Y]] by simp
2.19
2.20 +lemma (in prob_space) setsum_distribution:
2.21 +  assumes X: "finite_random_variable MX X" shows "(\<Sum>a\<in>space MX. distribution X {a}) = 1"
2.22 +  using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV \<rparr>" "\<lambda>x. ()" "{()}"]
2.23 +  using sigma_algebra_Pow[of "UNIV::unit set" "()"] by simp
2.24 +
2.25  locale pair_finite_prob_space = M1: finite_prob_space M1 + M2: finite_prob_space M2 for M1 M2
2.26
2.27  sublocale pair_finite_prob_space \<subseteq> pair_prob_space M1 M2 by default
```
```     3.1 --- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Thu Dec 01 14:03:57 2011 +0100
3.2 +++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Thu Dec 01 14:03:57 2011 +0100
3.3 @@ -75,13 +75,6 @@
3.4    qed
3.5  qed
3.6
3.7 -lemma (in prob_space)
3.8 -  assumes "finite (X`space M)"
3.9 -  shows "bij_betw (ordered_variable_partition X) {0..<card (X`space M)} (X`space M)"
3.10 -  and "\<And>i j. \<lbrakk> i < card (X`space M) ; j < card (X`space M) ; i \<le> j \<rbrakk> \<Longrightarrow>
3.11 -    distribution X {ordered_variable_partition X i} \<le> distribution X {ordered_variable_partition X j}"
3.12 -  oops
3.13 -
3.14  definition (in prob_space)
3.15    "order_distribution X i = real (distribution X {ordered_variable_partition X i})"
3.16
```