src/HOL/Probability/Product_Measure.thy
changeset 39096 111756225292
parent 39092 98de40859858
parent 39095 f92b7e2877c2
child 39097 943c7b348524
     1.1 --- a/src/HOL/Probability/Product_Measure.thy	Thu Sep 02 17:12:40 2010 +0200
     1.2 +++ b/src/HOL/Probability/Product_Measure.thy	Thu Sep 02 17:28:00 2010 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  lemma dynkinI:
     1.6    assumes "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
     1.7 -  assumes "space M \<in> sets M" and "\<forall> a \<in> sets M. \<forall> b \<in> sets M. b - a \<in> sets M"
     1.8 +  assumes "space M \<in> sets M" and "\<forall> b \<in> sets M. \<forall> a \<in> sets M. a \<subseteq> b \<longrightarrow> b - a \<in> sets M"
     1.9    assumes "\<And> a. (\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {})
    1.10            \<Longrightarrow> (\<And> i :: nat. a i \<in> sets M) \<Longrightarrow> UNION UNIV a \<in> sets M"
    1.11    shows "dynkin M"
    1.12 @@ -28,13 +28,18 @@
    1.13  
    1.14  lemma dynkin_diff:
    1.15    assumes "dynkin M"
    1.16 -  shows "\<And> a b. \<lbrakk> a \<in> sets M ; b \<in> sets M \<rbrakk> \<Longrightarrow> b - a \<in> sets M"
    1.17 +  shows "\<And> a b. \<lbrakk> a \<in> sets M ; b \<in> sets M ; a \<subseteq> b \<rbrakk> \<Longrightarrow> b - a \<in> sets M"
    1.18  using assms unfolding dynkin_def by auto
    1.19  
    1.20 +lemma dynkin_empty:
    1.21 +  assumes "dynkin M"
    1.22 +  shows "{} \<in> sets M"
    1.23 +using dynkin_diff[OF assms dynkin_space[OF assms] dynkin_space[OF assms]] by auto
    1.24 +
    1.25  lemma dynkin_UN:
    1.26    assumes "dynkin M"
    1.27    assumes "\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}"
    1.28 -  assumes "\<forall> i :: nat. a i \<in> sets M"
    1.29 +  assumes "\<And> i :: nat. a i \<in> sets M"
    1.30    shows "UNION UNIV a \<in> sets M"
    1.31  using assms unfolding dynkin_def sorry
    1.32  
    1.33 @@ -44,7 +49,7 @@
    1.34    shows "dynkin \<lparr> space = A, sets = Pow A \<rparr>"
    1.35  by (rule dynkinI) auto
    1.36  
    1.37 -lemma
    1.38 +lemma dynkin_lemma:
    1.39    fixes D :: "'a algebra"
    1.40    assumes stab: "Int_stable E"
    1.41    and spac: "space E = space D"
    1.42 @@ -60,10 +65,8 @@
    1.43    hence not_empty: "{sets (d :: 'a algebra) | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d} \<noteq> {}"
    1.44      using exI[of "\<lambda> x. space x = space E \<and> dynkin x \<and> sets E \<subseteq> sets x" "\<lparr> space = space E, sets = Pow (space E) \<rparr>", simplified]
    1.45      by auto
    1.46 -
    1.47 -  have "sets_\<delta>E \<subseteq> sets D"
    1.48 +  have \<delta>E_D: "sets_\<delta>E \<subseteq> sets D"
    1.49      unfolding sets_\<delta>E_def using assms by auto
    1.50 -
    1.51    have \<delta>ynkin: "dynkin \<delta>E"
    1.52    proof (rule dynkinI, safe)
    1.53      fix A x assume asm: "A \<in> sets \<delta>E" "x \<in> A"
    1.54 @@ -76,7 +79,7 @@
    1.55        unfolding \<delta>E_def sets_\<delta>E_def
    1.56        using dynkin_space by fastsimp
    1.57    next
    1.58 -    fix a b assume "a \<in> sets \<delta>E" "b \<in> sets \<delta>E"
    1.59 +    fix a b assume "a \<in> sets \<delta>E" "b \<in> sets \<delta>E" "a \<subseteq> b"
    1.60      thus "b - a \<in> sets \<delta>E"
    1.61        unfolding \<delta>E_def sets_\<delta>E_def by (auto intro:dynkin_diff)
    1.62    next
    1.63 @@ -113,21 +116,21 @@
    1.64            unfolding \<delta>E_def by auto
    1.65        qed
    1.66      next
    1.67 -      fix a b assume absm: "a \<in> Dy d" "b \<in> Dy d"
    1.68 +      fix a b assume absm: "a \<in> Dy d" "b \<in> Dy d" "a \<subseteq> b"
    1.69        hence "a \<in> sets \<delta>E" "b \<in> sets \<delta>E"
    1.70          unfolding Dy_def \<delta>E_def by auto
    1.71        hence *: "b - a \<in> sets \<delta>E"
    1.72 -        using dynkin_diff[OF \<delta>ynkin] by auto
    1.73 +        using dynkin_diff[OF \<delta>ynkin] `a \<subseteq> b` by auto
    1.74        have "a \<inter> d \<in> sets \<delta>E" "b \<inter> d \<in> sets \<delta>E"
    1.75          using absm unfolding Dy_def \<delta>E_def by auto
    1.76        hence "(b \<inter> d) - (a \<inter> d) \<in> sets \<delta>E"
    1.77 -        using dynkin_diff[OF \<delta>ynkin] by auto
    1.78 +        using dynkin_diff[OF \<delta>ynkin] `a \<subseteq> b` by auto
    1.79        hence **: "(b - a) \<inter> d \<in> sets \<delta>E" by (auto simp add:Diff_Int_distrib2)
    1.80        thus "b - a \<in> Dy d"
    1.81          using * ** unfolding Dy_def \<delta>E_def by auto
    1.82      next
    1.83        fix a assume aasm: "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}" "\<And>i. a i \<in> Dy d"
    1.84 -      hence "\<forall> i. a i \<in> sets \<delta>E"
    1.85 +      hence "\<And> i. a i \<in> sets \<delta>E"
    1.86          unfolding Dy_def \<delta>E_def by auto
    1.87        from dynkin_UN[OF \<delta>ynkin aasm(1) this]
    1.88        have *: "UNION UNIV a \<in> sets \<delta>E" by auto
    1.89 @@ -176,26 +179,171 @@
    1.90      fix a assume aasm: "a \<in> sets \<delta>E"
    1.91      hence "a \<inter> d \<in> sets \<delta>E"
    1.92        using * dasm unfolding Dy_def \<delta>E_def by auto } note \<delta>E_stab = this
    1.93 -  have "sigma_algebra D"
    1.94 +  { fix A :: "nat \<Rightarrow> 'a set" assume Asm: "range A \<subseteq> sets \<delta>E" "\<And>A. A \<in> sets \<delta>E \<Longrightarrow> A \<subseteq> space \<delta>E"
    1.95 +      "\<And>a. a \<in> sets \<delta>E \<Longrightarrow> space \<delta>E - a \<in> sets \<delta>E"
    1.96 +    "{} \<in> sets \<delta>E" "space \<delta>E \<in> sets \<delta>E"
    1.97 +    let "?A i" = "A i \<inter> (\<Inter> j \<in> {..< i}. space \<delta>E - A j)"
    1.98 +    { fix i :: nat
    1.99 +      have *: "(\<Inter> j \<in> {..< i}. space \<delta>E - A j) \<inter> space \<delta>E \<in> sets \<delta>E"
   1.100 +        apply (induct i)
   1.101 +        using lessThan_Suc Asm \<delta>E_stab apply fastsimp
   1.102 +        apply (subst lessThan_Suc)
   1.103 +        apply (subst INT_insert)
   1.104 +        apply (subst Int_assoc)
   1.105 +        apply (subst \<delta>E_stab)
   1.106 +        using lessThan_Suc Asm \<delta>E_stab Asm
   1.107 +        apply (fastsimp simp add:Int_assoc dynkin_diff[OF \<delta>ynkin])
   1.108 +        prefer 2 apply simp
   1.109 +        apply (rule dynkin_diff[OF \<delta>ynkin, of _ "space \<delta>E", OF _ dynkin_space[OF \<delta>ynkin]])
   1.110 +        using Asm by auto
   1.111 +      have **: "\<And> i. A i \<subseteq> space \<delta>E" using Asm by auto
   1.112 +      have "(\<Inter> j \<in> {..< i}. space \<delta>E - A j) \<subseteq> space \<delta>E \<or> (\<Inter> j \<in> {..< i}. A j) = UNIV \<and> i = 0"
   1.113 +        apply (cases i)
   1.114 +        using Asm ** dynkin_subset[OF \<delta>ynkin, of "A (i - 1)"]
   1.115 +        by auto
   1.116 +      hence Aisets: "?A i \<in> sets \<delta>E"
   1.117 +        apply (cases i)
   1.118 +        using Asm * apply fastsimp
   1.119 +        apply (rule \<delta>E_stab)
   1.120 +        using Asm * **
   1.121 +        by (auto simp add:Int_absorb2)
   1.122 +      have "?A i = disjointed A i" unfolding disjointed_def
   1.123 +      atLeast0LessThan using Asm by auto
   1.124 +      hence "?A i = disjointed A i" "?A i \<in> sets \<delta>E"
   1.125 +        using Aisets by auto
   1.126 +    } note Ai = this
   1.127 +    from dynkin_UN[OF \<delta>ynkin _ this(2)] this disjoint_family_disjointed[of A]
   1.128 +    have "(\<Union> i. ?A i) \<in> sets \<delta>E"
   1.129 +      by (auto simp add:disjoint_family_on_def disjointed_def)
   1.130 +    hence "(\<Union> i. A i) \<in> sets \<delta>E"
   1.131 +      using Ai(1) UN_disjointed_eq[of A] by auto } note \<delta>E_UN = this
   1.132 +  { fix a b assume asm: "a \<in> sets \<delta>E" "b \<in> sets \<delta>E"
   1.133 +    let ?ab = "\<lambda> i. if (i::nat) = 0 then a else if i = 1 then b else {}"
   1.134 +    have *: "(\<Union> i. ?ab i) \<in> sets \<delta>E"
   1.135 +      apply (rule \<delta>E_UN)
   1.136 +      using asm \<delta>E_UN dynkin_empty[OF \<delta>ynkin] 
   1.137 +      dynkin_subset[OF \<delta>ynkin] 
   1.138 +      dynkin_space[OF \<delta>ynkin]
   1.139 +      dynkin_diff[OF \<delta>ynkin] by auto
   1.140 +    have "(\<Union> i. ?ab i) = a \<union> b" apply auto
   1.141 +      apply (case_tac "i = 0")
   1.142 +      apply auto
   1.143 +      apply (case_tac "i = 1")
   1.144 +      by auto
   1.145 +    hence "a \<union> b \<in> sets \<delta>E" using * by auto} note \<delta>E_Un = this
   1.146 +  have "sigma_algebra \<delta>E"
   1.147      apply unfold_locales
   1.148 -    using dynkin_subset[OF dyn]
   1.149 -    using dynkin_diff[OF dyn, of _ "space D", OF _ dynkin_space[OF dyn]]
   1.150 -    using dynkin_diff[OF dyn, of "space D" "space D", OF dynkin_space[OF dyn] dynkin_space[OF dyn]]
   1.151 -    using dynkin_space[OF dyn]
   1.152 -    sorry
   1.153 -(*
   1.154 -  proof auto
   1.155 -    fix A :: "nat \<Rightarrow> 'a set" assume Asm: "range A \<subseteq> sets D" "\<And>A. A \<in> sets D \<Longrightarrow> A \<subseteq> space D"
   1.156 -      "\<And>a. a \<in> sets D \<Longrightarrow> space D - a \<in> sets D"
   1.157 -    "{} \<in> sets D" "space D \<in> sets D"
   1.158 -    let "?A i" = "A i - (\<Inter> j \<in> {..< i}. A j)"
   1.159 -    { fix i :: nat assume "i > 0"
   1.160 -      have "(\<Inter> j \<in> {..< i}. A j) \<in> sets \<delta>E" sorry }
   1.161 -      oops
   1.162 +    using dynkin_subset[OF \<delta>ynkin]
   1.163 +    using dynkin_diff[OF \<delta>ynkin, of _ "space \<delta>E", OF _ dynkin_space[OF \<delta>ynkin]]
   1.164 +    using dynkin_diff[OF \<delta>ynkin, of "space \<delta>E" "space \<delta>E", OF dynkin_space[OF \<delta>ynkin] dynkin_space[OF \<delta>ynkin]]
   1.165 +    using dynkin_space[OF \<delta>ynkin]
   1.166 +    using \<delta>E_UN \<delta>E_Un
   1.167 +    by auto
   1.168 +  from sigma_algebra.sigma_subset[OF this E_\<delta>E] \<delta>E_D subsDE spac
   1.169 +  show ?thesis by (auto simp add:\<delta>E_def sigma_def)
   1.170 +qed
   1.171 +
   1.172 +lemma measure_eq:
   1.173 +  assumes fin: "\<mu> (space M) = \<nu> (space M)" "\<nu> (space M) < \<omega>"
   1.174 +  assumes E: "M = sigma (space E) (sets E)" "Int_stable E"
   1.175 +  assumes eq: "\<And> e. e \<in> sets E \<Longrightarrow> \<mu> e = \<nu> e"
   1.176 +  assumes ms: "measure_space M \<mu>" "measure_space M \<nu>"
   1.177 +  assumes A: "A \<in> sets M"
   1.178 +  shows "\<mu> A = \<nu> A"
   1.179 +proof -
   1.180 +  interpret M: measure_space M \<mu>
   1.181 +    using ms by simp
   1.182 +  interpret M': measure_space M \<nu>
   1.183 +    using ms by simp
   1.184 +
   1.185 +  let ?D_sets = "{A. A \<in> sets M \<and> \<mu> A = \<nu> A}"
   1.186 +  have \<delta>: "dynkin \<lparr> space = space M , sets = ?D_sets \<rparr>"
   1.187 +  proof (rule dynkinI, safe, simp_all)
   1.188 +    fix A x assume "A \<in> sets M \<and> \<mu> A = \<nu> A" "x \<in> A"
   1.189 +    thus "x \<in> space M" using assms M.sets_into_space by auto
   1.190 +  next
   1.191 +    show "\<mu> (space M) = \<nu> (space M)"
   1.192 +      using fin by auto
   1.193 +  next
   1.194 +    fix a b
   1.195 +    assume asm: "a \<in> sets M \<and> \<mu> a = \<nu> a"
   1.196 +      "b \<in> sets M \<and> \<mu> b = \<nu> b" "a \<subseteq> b"
   1.197 +    hence "a \<subseteq> space M"
   1.198 +      using M.sets_into_space by auto
   1.199 +    from M.measure_mono[OF this]
   1.200 +    have "\<mu> a \<le> \<mu> (space M)"
   1.201 +      using asm by auto
   1.202 +    hence afin: "\<mu> a < \<omega>"
   1.203 +      using fin by auto
   1.204 +    have *: "b = b - a \<union> a" using asm by auto
   1.205 +    have **: "(b - a) \<inter> a = {}" using asm by auto
   1.206 +    have iv: "\<mu> (b - a) + \<mu> a = \<mu> b"
   1.207 +      using M.measure_additive[of "b - a" a]
   1.208 +        conjunct1[OF asm(1)] conjunct1[OF asm(2)] * **
   1.209 +      by auto
   1.210 +    have v: "\<nu> (b - a) + \<nu> a = \<nu> b"
   1.211 +      using M'.measure_additive[of "b - a" a]
   1.212 +        conjunct1[OF asm(1)] conjunct1[OF asm(2)] * **
   1.213 +      by auto
   1.214 +    from iv v have "\<mu> (b - a) = \<nu> (b - a)" using asm afin
   1.215 +      pinfreal_add_cancel_right[of "\<mu> (b - a)" "\<nu> a" "\<nu> (b - a)"]
   1.216 +      by auto
   1.217 +    thus "b - a \<in> sets M \<and> \<mu> (b - a) = \<nu> (b - a)"
   1.218 +      using asm by auto
   1.219 +  next
   1.220 +    fix a assume "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}"
   1.221 +      "\<And>i. a i \<in> sets M \<and> \<mu> (a i) = \<nu> (a i)"
   1.222 +    thus "(\<Union>x. a x) \<in> sets M \<and> \<mu> (\<Union>x. a x) = \<nu> (\<Union>x. a x)"
   1.223 +      using M.measure_countably_additive
   1.224 +        M'.measure_countably_additive
   1.225 +        M.countable_UN
   1.226 +      apply (auto simp add:disjoint_family_on_def image_def)
   1.227 +      apply (subst M.measure_countably_additive[symmetric])
   1.228 +      apply (auto simp add:disjoint_family_on_def)
   1.229 +      apply (subst M'.measure_countably_additive[symmetric])
   1.230 +      by (auto simp add:disjoint_family_on_def)
   1.231    qed
   1.232 -*)
   1.233 +  have *: "sets E \<subseteq> ?D_sets"
   1.234 +    using eq E sigma_sets.Basic[of _ "sets E"]
   1.235 +    by (auto simp add:sigma_def)
   1.236 +  have **: "?D_sets \<subseteq> sets M" by auto
   1.237 +  have "M = \<lparr> space = space M , sets = ?D_sets \<rparr>"
   1.238 +    unfolding E(1)
   1.239 +    apply (rule dynkin_lemma[OF E(2)])
   1.240 +    using eq E space_sigma \<delta> sigma_sets.Basic
   1.241 +    by (auto simp add:sigma_def)
   1.242 +  from subst[OF this, of "\<lambda> M. A \<in> sets M", OF A]
   1.243 +  show ?thesis by auto
   1.244 +qed
   1.245  
   1.246 -  show ?thesis sorry
   1.247 +lemma
   1.248 +  assumes sfin: "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And> i :: nat. \<nu> (A i) < \<omega>"
   1.249 +  assumes A: "\<And>  i. \<mu> (A i) = \<nu> (A i)" "\<And> i. A i \<subseteq> A (Suc i)"
   1.250 +  assumes E: "M = sigma (space E) (sets E)" "Int_stable E"
   1.251 +  assumes eq: "\<And> e. e \<in> sets E \<Longrightarrow> \<mu> e = \<nu> e"
   1.252 +  assumes ms: "measure_space (M :: 'a algebra) \<mu>" "measure_space M \<nu>"
   1.253 +  assumes B: "B \<in> sets M"
   1.254 +  shows "\<mu> B = \<nu> B"
   1.255 +proof -
   1.256 +  interpret M: measure_space M \<mu> by (rule ms)
   1.257 +  interpret M': measure_space M \<nu> by (rule ms)
   1.258 +  have *: "M = \<lparr> space = space M, sets = sets M \<rparr>" by auto
   1.259 +  { fix i :: nat
   1.260 +    have **: "M\<lparr> space := A i, sets := op \<inter> (A i) ` sets M \<rparr> =
   1.261 +      \<lparr> space = A i, sets = op \<inter> (A i) ` sets M \<rparr>"
   1.262 +      by auto
   1.263 +    have mu_i: "measure_space \<lparr> space = A i, sets = op \<inter> (A i) ` sets M \<rparr> \<mu>"
   1.264 +      using M.restricted_measure_space[of "A i", simplified **]
   1.265 +        sfin by auto
   1.266 +    have nu_i: "measure_space \<lparr> space = A i, sets = op \<inter> (A i) ` sets M \<rparr> \<nu>"
   1.267 +      using M'.restricted_measure_space[of "A i", simplified **]
   1.268 +        sfin by auto
   1.269 +    let ?M = "\<lparr> space = A i, sets = op \<inter> (A i) ` sets M \<rparr>"
   1.270 +    have "\<mu> (A i \<inter> B) = \<nu> (A i \<inter> B)"
   1.271 +      apply (rule measure_eq[of \<mu> ?M \<nu> "\<lparr> space = space E \<inter> A i, sets = op \<inter> (A i) ` sets E\<rparr>" "A i \<inter> B", simplified])
   1.272 +      using assms nu_i mu_i
   1.273 +      apply (auto simp add:image_def) (* TODO *) sorry
   1.274 +    show ?thesis sorry
   1.275  qed
   1.276  
   1.277  definition prod_sets where
   1.278 @@ -403,45 +551,4 @@
   1.279    unfolding finite_prod_measure_space[OF N, symmetric]
   1.280    using finite_measure_space_finite_prod_measure[OF N] .
   1.281  
   1.282 -lemma (in finite_prob_space) finite_product_measure_space:
   1.283 -  assumes "finite s1" "finite s2"
   1.284 -  shows "finite_measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2)\<rparr> (joint_distribution X Y)"
   1.285 -    (is "finite_measure_space ?M ?D")
   1.286 -proof (rule finite_Pow_additivity_sufficient)
   1.287 -  show "positive ?D"
   1.288 -    unfolding positive_def using assms sets_eq_Pow
   1.289 -    by (simp add: distribution_def)
   1.290 -
   1.291 -  show "additive ?M ?D" unfolding additive_def
   1.292 -  proof safe
   1.293 -    fix x y
   1.294 -    have A: "((\<lambda>x. (X x, Y x)) -` x) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto
   1.295 -    have B: "((\<lambda>x. (X x, Y x)) -` y) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto
   1.296 -    assume "x \<inter> y = {}"
   1.297 -    hence "(\<lambda>x. (X x, Y x)) -` x \<inter> space M \<inter> ((\<lambda>x. (X x, Y x)) -` y \<inter> space M) = {}"
   1.298 -      by auto
   1.299 -    from additive[unfolded additive_def, rule_format, OF A B] this
   1.300 -      finite_measure[OF A] finite_measure[OF B]
   1.301 -    show "?D (x \<union> y) = ?D x + ?D y"
   1.302 -      apply (simp add: distribution_def)
   1.303 -      apply (subst Int_Un_distrib2)
   1.304 -      by (auto simp: real_of_pinfreal_add)
   1.305 -  qed
   1.306 -
   1.307 -  show "finite (space ?M)"
   1.308 -    using assms by auto
   1.309 -
   1.310 -  show "sets ?M = Pow (space ?M)"
   1.311 -    by simp
   1.312 -
   1.313 -  { fix x assume "x \<in> space ?M" thus "?D {x} \<noteq> \<omega>"
   1.314 -    unfolding distribution_def by (auto intro!: finite_measure simp: sets_eq_Pow) }
   1.315 -qed
   1.316 -
   1.317 -lemma (in finite_measure_space) finite_product_measure_space_of_images:
   1.318 -  shows "finite_measure_space \<lparr> space = X ` space M \<times> Y ` space M,
   1.319 -                                sets = Pow (X ` space M \<times> Y ` space M) \<rparr>
   1.320 -                              (joint_distribution X Y)"
   1.321 -  using finite_space by (auto intro!: finite_product_measure_space)
   1.322 -
   1.323 -end
   1.324 \ No newline at end of file
   1.325 +end