moved theorems about distribution to the definition; removed oopsed-lemma
authorhoelzl
Thu Dec 01 14:03:57 2011 +0100 (2011-12-01)
changeset 45712852597248663
parent 45711 a2c32e196d49
child 45713 badee348c5fb
moved theorems about distribution to the definition; removed oopsed-lemma
src/HOL/Probability/Information.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
     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