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.225 +        M.countable_UN
1.226 +      apply (auto simp add:disjoint_family_on_def image_def)
1.228 +      apply (auto simp add:disjoint_family_on_def)
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.287 -  show "positive ?D"
1.288 -    unfolding positive_def using assms sets_eq_Pow
1.289 -    by (simp add: distribution_def)
1.290 -
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.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
```