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")