src/HOL/Probability/Independent_Family.thy
 changeset 50104 de19856feb54 parent 50087 635d73673b5e child 50123 69b35a75caf3
```     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Fri Nov 16 18:49:46 2012 +0100
1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Fri Nov 16 18:45:57 2012 +0100
1.3 @@ -18,9 +18,6 @@
1.4  definition (in prob_space)
1.5    indep_events_def_alt: "indep_events A I \<longleftrightarrow> indep_sets (\<lambda>i. {A i}) I"
1.6
1.7 -lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
1.8 -  by auto
1.9 -
1.10  lemma (in prob_space) indep_events_def:
1.11    "indep_events A I \<longleftrightarrow> (A`I \<subseteq> events) \<and>
1.12      (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j)))"
1.13 @@ -827,31 +824,6 @@
1.14      using I by auto
1.15  qed fact+
1.16
1.17 -lemma prod_algebra_cong:
1.18 -  assumes "I = J" and sets: "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))"
1.19 -  shows "prod_algebra I M = prod_algebra J N"
1.20 -proof -
1.21 -  have space: "\<And>i. i \<in> I \<Longrightarrow> space (M i) = space (N i)"
1.22 -    using sets_eq_imp_space_eq[OF sets] by auto
1.23 -  with sets show ?thesis unfolding `I = J`
1.24 -    by (intro antisym prod_algebra_mono) auto
1.25 -qed
1.26 -
1.27 -lemma space_in_prod_algebra:
1.28 -  "(\<Pi>\<^isub>E i\<in>I. space (M i)) \<in> prod_algebra I M"
1.29 -proof cases
1.30 -  assume "I = {}" then show ?thesis
1.31 -    by (auto simp add: prod_algebra_def image_iff prod_emb_def)
1.32 -next
1.33 -  assume "I \<noteq> {}"
1.34 -  then obtain i where "i \<in> I" by auto
1.35 -  then have "(\<Pi>\<^isub>E i\<in>I. space (M i)) = prod_emb I M {i} (\<Pi>\<^isub>E i\<in>{i}. space (M i))"
1.36 -    by (auto simp: prod_emb_def Pi_iff)
1.37 -  also have "\<dots> \<in> prod_algebra I M"
1.38 -    using `i \<in> I` by (intro prod_algebraI) auto
1.39 -  finally show ?thesis .
1.40 -qed
1.41 -
1.42  lemma (in prob_space) indep_vars_iff_distr_eq_PiM:
1.43    fixes I :: "'i set" and X :: "'i \<Rightarrow> 'a \<Rightarrow> 'b"
1.44    assumes "I \<noteq> {}"
1.45 @@ -972,114 +944,6 @@
1.46      unfolding UNIV_bool by auto
1.47  qed
1.48
1.49 -lemma measurable_bool_case[simp, intro]:
1.50 -  "(\<lambda>(x, y). bool_case x y) \<in> measurable (M \<Otimes>\<^isub>M N) (Pi\<^isub>M UNIV (bool_case M N))"
1.51 -    (is "?f \<in> measurable ?B ?P")
1.52 -proof (rule measurable_PiM_single)
1.53 -  show "?f \<in> space ?B \<rightarrow> (\<Pi>\<^isub>E i\<in>UNIV. space (bool_case M N i))"
1.54 -    by (auto simp: space_pair_measure extensional_def split: bool.split)
1.55 -  fix i A assume "A \<in> sets (case i of True \<Rightarrow> M | False \<Rightarrow> N)"
1.56 -  moreover then have "{\<omega> \<in> space (M \<Otimes>\<^isub>M N). prod_case bool_case \<omega> i \<in> A}
1.57 -    = (case i of True \<Rightarrow> A \<times> space N | False \<Rightarrow> space M \<times> A)"
1.58 -    by (auto simp: space_pair_measure split: bool.split dest!: sets_into_space)
1.59 -  ultimately show "{\<omega> \<in> space (M \<Otimes>\<^isub>M N). prod_case bool_case \<omega> i \<in> A} \<in> sets ?B"
1.60 -    by (auto split: bool.split)
1.61 -qed
1.62 -
1.63 -lemma borel_measurable_indicator':
1.64 -  "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> borel_measurable M"
1.65 -  using measurable_comp[OF _ borel_measurable_indicator, of f M N A] by (auto simp add: comp_def)
1.66 -
1.67 -lemma (in product_sigma_finite) distr_component:
1.68 -  "distr (M i) (Pi\<^isub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^isub>M {i} M" (is "?D = ?P")
1.69 -proof (intro measure_eqI[symmetric])
1.70 -  interpret I: finite_product_sigma_finite M "{i}" by default simp
1.71 -
1.72 -  have eq: "\<And>x. x \<in> extensional {i} \<Longrightarrow> (\<lambda>j\<in>{i}. x i) = x"
1.73 -    by (auto simp: extensional_def restrict_def)
1.74 -
1.75 -  fix A assume A: "A \<in> sets ?P"
1.76 -  then have "emeasure ?P A = (\<integral>\<^isup>+x. indicator A x \<partial>?P)"
1.77 -    by simp
1.78 -  also have "\<dots> = (\<integral>\<^isup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) (x i) \<partial>PiM {i} M)"
1.79 -    by (intro positive_integral_cong) (auto simp: space_PiM indicator_def simp: eq)
1.80 -  also have "\<dots> = emeasure ?D A"
1.81 -    using A by (simp add: product_positive_integral_singleton emeasure_distr)
1.82 -  finally show "emeasure (Pi\<^isub>M {i} M) A = emeasure ?D A" .
1.83 -qed simp
1.84 -
1.85 -lemma pair_measure_eqI:
1.86 -  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
1.87 -  assumes sets: "sets (M1 \<Otimes>\<^isub>M M2) = sets M"
1.88 -  assumes emeasure: "\<And>A B. A \<in> sets M1 \<Longrightarrow> B \<in> sets M2 \<Longrightarrow> emeasure M1 A * emeasure M2 B = emeasure M (A \<times> B)"
1.89 -  shows "M1 \<Otimes>\<^isub>M M2 = M"
1.90 -proof -
1.91 -  interpret M1: sigma_finite_measure M1 by fact
1.92 -  interpret M2: sigma_finite_measure M2 by fact
1.93 -  interpret pair_sigma_finite M1 M2 by default
1.94 -  from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
1.95 -  let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}"
1.96 -  let ?P = "M1 \<Otimes>\<^isub>M M2"
1.97 -  show ?thesis
1.98 -  proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
1.99 -    show "?E \<subseteq> Pow (space ?P)"
1.100 -      using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure)
1.101 -    show "sets ?P = sigma_sets (space ?P) ?E"
1.102 -      by (simp add: sets_pair_measure space_pair_measure)
1.103 -    then show "sets M = sigma_sets (space ?P) ?E"
1.104 -      using sets[symmetric] by simp
1.105 -  next
1.106 -    show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
1.107 -      using F by (auto simp: space_pair_measure)
1.108 -  next
1.109 -    fix X assume "X \<in> ?E"
1.110 -    then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> sets M2" by auto
1.111 -    then have "emeasure ?P X = emeasure M1 A * emeasure M2 B"
1.112 -       by (simp add: M2.emeasure_pair_measure_Times)
1.113 -    also have "\<dots> = emeasure M (A \<times> B)"
1.114 -      using A B emeasure by auto
1.115 -    finally show "emeasure ?P X = emeasure M X"
1.116 -      by simp
1.117 -  qed
1.118 -qed
1.119 -
1.120 -lemma pair_measure_eq_distr_PiM:
1.121 -  fixes M1 :: "'a measure" and M2 :: "'a measure"
1.122 -  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
1.123 -  shows "(M1 \<Otimes>\<^isub>M M2) = distr (Pi\<^isub>M UNIV (bool_case M1 M2)) (M1 \<Otimes>\<^isub>M M2) (\<lambda>x. (x True, x False))"
1.124 -    (is "?P = ?D")
1.125 -proof (rule pair_measure_eqI[OF assms])
1.126 -  interpret B: product_sigma_finite "bool_case M1 M2"
1.127 -    unfolding product_sigma_finite_def using assms by (auto split: bool.split)
1.128 -  let ?B = "Pi\<^isub>M UNIV (bool_case M1 M2)"
1.129 -
1.130 -  have [simp]: "fst \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x True)" "snd \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x False)"
1.131 -    by auto
1.132 -  fix A B assume A: "A \<in> sets M1" and B: "B \<in> sets M2"
1.133 -  have "emeasure M1 A * emeasure M2 B = (\<Prod> i\<in>UNIV. emeasure (bool_case M1 M2 i) (bool_case A B i))"
1.134 -    by (simp add: UNIV_bool ac_simps)
1.135 -  also have "\<dots> = emeasure ?B (Pi\<^isub>E UNIV (bool_case A B))"
1.136 -    using A B by (subst B.emeasure_PiM) (auto split: bool.split)
1.137 -  also have "Pi\<^isub>E UNIV (bool_case A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
1.138 -    using A[THEN sets_into_space] B[THEN sets_into_space]
1.139 -    by (auto simp: Pi_iff all_bool_eq space_PiM split: bool.split)
1.140 -  finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)"
1.141 -    using A B
1.142 -      measurable_component_singleton[of True UNIV "bool_case M1 M2"]
1.143 -      measurable_component_singleton[of False UNIV "bool_case M1 M2"]
1.144 -    by (subst emeasure_distr) (auto simp: measurable_pair_iff)
1.145 -qed simp
1.146 -
1.147 -lemma measurable_Pair:
1.148 -  assumes rvs: "X \<in> measurable M S" "Y \<in> measurable M T"
1.149 -  shows "(\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)"
1.150 -proof -
1.151 -  have [simp]: "fst \<circ> (\<lambda>x. (X x, Y x)) = (\<lambda>x. X x)" "snd \<circ> (\<lambda>x. (X x, Y x)) = (\<lambda>x. Y x)"
1.152 -    by auto
1.153 -  show " (\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)"
1.154 -    by (auto simp: measurable_pair_iff rvs)
1.155 -qed
1.156 -
1.157  lemma (in prob_space) indep_var_distribution_eq:
1.158    "indep_var S X T Y \<longleftrightarrow> random_variable S X \<and> random_variable T Y \<and>
1.159      distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" (is "_ \<longleftrightarrow> _ \<and> _ \<and> ?S \<Otimes>\<^isub>M ?T = ?J")
```