1.1 --- a/src/HOL/Probability/Product_Measure.thy Thu Aug 26 11:33:36 2010 +0200
1.2 +++ b/src/HOL/Probability/Product_Measure.thy Thu Aug 26 13:17:58 2010 +0200
1.3 @@ -2,6 +2,254 @@
1.4 imports Lebesgue_Integration
1.5 begin
1.6
1.7 +definition dynkin
1.8 +where "dynkin M =
1.9 + ((\<forall> A \<in> sets M. A \<subseteq> space M) \<and>
1.10 + space M \<in> sets M \<and> (\<forall> a \<in> sets M. \<forall> b \<in> sets M. b - a \<in> sets M) \<and>
1.11 + (\<forall> a. (\<forall> i j :: nat. i \<noteq> j \<longrightarrow> a i \<inter> a j = {}) \<and>
1.12 + (\<forall> i :: nat. a i \<in> sets M) \<longrightarrow> UNION UNIV a \<in> sets M))"
1.13 +
1.14 +lemma dynkinI:
1.15 + assumes "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
1.16 + assumes "space M \<in> sets M" and "\<forall> a \<in> sets M. \<forall> b \<in> sets M. b - a \<in> sets M"
1.17 + assumes "\<And> a. (\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {})
1.18 + \<Longrightarrow> (\<And> i :: nat. a i \<in> sets M) \<Longrightarrow> UNION UNIV a \<in> sets M"
1.19 + shows "dynkin M"
1.20 +using assms unfolding dynkin_def by auto
1.21 +
1.22 +lemma dynkin_subset:
1.23 + assumes "dynkin M"
1.24 + shows "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
1.25 +using assms unfolding dynkin_def by auto
1.26 +
1.27 +lemma dynkin_space:
1.28 + assumes "dynkin M"
1.29 + shows "space M \<in> sets M"
1.30 +using assms unfolding dynkin_def by auto
1.31 +
1.32 +lemma dynkin_diff:
1.33 + assumes "dynkin M"
1.34 + shows "\<And> a b. \<lbrakk> a \<in> sets M ; b \<in> sets M \<rbrakk> \<Longrightarrow> b - a \<in> sets M"
1.35 +using assms unfolding dynkin_def by auto
1.36 +
1.37 +lemma dynkin_UN:
1.38 + assumes "dynkin M"
1.39 + assumes "\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}"
1.40 + assumes "\<forall> i :: nat. a i \<in> sets M"
1.41 + shows "UNION UNIV a \<in> sets M"
1.42 +using assms unfolding dynkin_def by auto
1.43 +
1.44 +definition Int_stable
1.45 +where "Int_stable M = (\<forall> a \<in> sets M. (\<forall> b \<in> sets M. a \<inter> b \<in> sets M))"
1.46 +
1.47 +lemma dynkin_trivial:
1.48 + shows "dynkin \<lparr> space = A, sets = Pow A \<rparr>"
1.49 +by (rule dynkinI) auto
1.50 +
1.51 +lemma
1.52 + assumes stab: "Int_stable E"
1.53 + and spac: "space E = space D"
1.54 + and subsED: "sets E \<subseteq> sets D"
1.55 + and subsDE: "sets D \<subseteq> sigma_sets (space E) (sets E)"
1.56 + and dyn: "dynkin D"
1.57 + shows "sigma (space E) (sets E) = D"
1.58 +proof -
1.59 + def sets_\<delta>E == "\<Inter> {sets d | d :: 'a algebra. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
1.60 + def \<delta>E == "\<lparr> space = space E, sets = sets_\<delta>E \<rparr>"
1.61 + have "\<lparr> space = space E, sets = Pow (space E) \<rparr> \<in> {d | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
1.62 + using dynkin_trivial spac subsED dynkin_subset[OF dyn] by fastsimp
1.63 + hence not_empty: "{sets (d :: 'a algebra) | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d} \<noteq> {}"
1.64 + 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.65 + by auto
1.66 +
1.67 + have "sets_\<delta>E \<subseteq> sets D"
1.68 + unfolding sets_\<delta>E_def using assms by auto
1.69 +
1.70 + have \<delta>ynkin: "dynkin \<delta>E"
1.71 + proof (rule dynkinI, safe)
1.72 + fix A x assume asm: "A \<in> sets \<delta>E" "x \<in> A"
1.73 + { fix d :: "('a, 'b) algebra_scheme" assume "A \<in> sets d" "dynkin d \<and> space d = space E"
1.74 + hence "A \<subseteq> space d"
1.75 + using dynkin_subset by auto }
1.76 + show "x \<in> space \<delta>E" using asm
1.77 + unfolding \<delta>E_def sets_\<delta>E_def using not_empty
1.78 + proof auto
1.79 + fix x A fix d :: "'a algebra"
1.80 + assume asm: "\<forall>x. (\<exists>d :: 'a algebra. x = sets d \<and>
1.81 + dynkin d \<and>
1.82 + space d = space E \<and>
1.83 + sets E \<subseteq> sets d) \<longrightarrow>
1.84 + A \<in> x" "x \<in> A"
1.85 + and asm': "space d = space E" "dynkin d" "sets E \<subseteq> sets d"
1.86 + have "A \<in> sets d"
1.87 + apply (rule impE[OF spec[OF asm(1), of "sets d"]])
1.88 + using exI[of _ d] asm' by auto
1.89 + thus "x \<in> space E" using asm' dynkin_subset[OF asm'(2), of A] asm(2) by auto
1.90 + qed
1.91 + next
1.92 + show "space \<delta>E \<in> sets \<delta>E"
1.93 + unfolding \<delta>E_def sets_\<delta>E_def
1.94 + using dynkin_space by fastsimp
1.95 + next
1.96 + fix a b assume "a \<in> sets \<delta>E" "b \<in> sets \<delta>E"
1.97 + thus "b - a \<in> sets \<delta>E"
1.98 + unfolding \<delta>E_def sets_\<delta>E_def by (auto intro:dynkin_diff)
1.99 + next
1.100 + fix a assume asm: "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}" "\<And>i. a i \<in> sets \<delta>E"
1.101 + thus "UNION UNIV a \<in> sets \<delta>E"
1.102 + unfolding \<delta>E_def sets_\<delta>E_def apply (auto intro!:dynkin_UN[OF _ asm(1)])
1.103 + by blast
1.104 + qed
1.105 + def Dy == "\<lambda> d. {A | A. A \<in> sets_\<delta>E \<and> A \<inter> d \<in> sets_\<delta>E}"
1.106 + { fix d assume dasm: "d \<in> sets_\<delta>E"
1.107 + have "dynkin \<lparr> space = space E, sets = Dy d \<rparr>"
1.108 + proof (rule dynkinI, auto)
1.109 + fix A x assume "A \<in> Dy d" "x \<in> A"
1.110 + thus "x \<in> space E" unfolding Dy_def sets_\<delta>E_def using not_empty
1.111 + proof auto fix x A fix da :: "'a algebra"
1.112 + assume asm: "x \<in> A"
1.113 + "\<forall>x. (\<exists>d :: 'a algebra. x = sets d \<and>
1.114 + dynkin d \<and> space d = space E \<and>
1.115 + sets E \<subseteq> sets d) \<longrightarrow> A \<in> x"
1.116 + "\<forall>x. (\<exists>d. x = sets d \<and>
1.117 + dynkin d \<and> space d = space E \<and>
1.118 + sets E \<subseteq> sets d) \<longrightarrow> A \<inter> d \<in> x"
1.119 + "space da = space E" "dynkin da"
1.120 + "sets E \<subseteq> sets da"
1.121 + have "A \<in> sets da"
1.122 + apply (rule impE[OF spec[OF asm(2)], of "sets da"])
1.123 + apply (rule exI[of _ da])
1.124 + using exI[of _ da] asm(4,5,6) by auto
1.125 + thus "x \<in> space E" using dynkin_subset[OF asm(5)] asm by auto
1.126 + qed
1.127 + next
1.128 + show "space E \<in> Dy d"
1.129 + unfolding Dy_def \<delta>E_def sets_\<delta>E_def
1.130 + proof auto
1.131 + fix d assume asm: "dynkin d" "space d = space E" "sets E \<subseteq> sets d"
1.132 + hence "space d \<in> sets d" using dynkin_space[OF asm(1)] by auto
1.133 + thus "space E \<in> sets d" using asm by auto
1.134 + next
1.135 + fix da :: "'a algebra" assume asm: "dynkin da" "space da = space E" "sets E \<subseteq> sets da"
1.136 + have d: "d = space E \<inter> d"
1.137 + using dasm dynkin_subset[OF asm(1)] asm(2) dynkin_subset[OF \<delta>ynkin]
1.138 + unfolding \<delta>E_def by auto
1.139 + hence "space E \<inter> d \<in> sets \<delta>E" unfolding \<delta>E_def
1.140 + using dasm by auto
1.141 + have "sets \<delta>E \<subseteq> sets da" unfolding \<delta>E_def sets_\<delta>E_def using asm
1.142 + by auto
1.143 + thus "space E \<inter> d \<in> sets da" using dasm asm d dynkin_subset[OF \<delta>ynkin]
1.144 + unfolding \<delta>E_def by auto
1.145 + qed
1.146 + next
1.147 + fix a b assume absm: "a \<in> Dy d" "b \<in> Dy d"
1.148 + hence "a \<in> sets \<delta>E" "b \<in> sets \<delta>E"
1.149 + unfolding Dy_def \<delta>E_def by auto
1.150 + hence *: "b - a \<in> sets \<delta>E"
1.151 + using dynkin_diff[OF \<delta>ynkin] by auto
1.152 + have "a \<inter> d \<in> sets \<delta>E" "b \<inter> d \<in> sets \<delta>E"
1.153 + using absm unfolding Dy_def \<delta>E_def by auto
1.154 + hence "(b \<inter> d) - (a \<inter> d) \<in> sets \<delta>E"
1.155 + using dynkin_diff[OF \<delta>ynkin] by auto
1.156 + hence **: "(b - a) \<inter> d \<in> sets \<delta>E" by (auto simp add:Diff_Int_distrib2)
1.157 + thus "b - a \<in> Dy d"
1.158 + using * ** unfolding Dy_def \<delta>E_def by auto
1.159 + next
1.160 + 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.161 + hence "\<forall> i. a i \<in> sets \<delta>E"
1.162 + unfolding Dy_def \<delta>E_def by auto
1.163 + from dynkin_UN[OF \<delta>ynkin aasm(1) this]
1.164 + have *: "UNION UNIV a \<in> sets \<delta>E" by auto
1.165 + from aasm
1.166 + have aE: "\<forall> i. a i \<inter> d \<in> sets \<delta>E"
1.167 + unfolding Dy_def \<delta>E_def by auto
1.168 + from aasm
1.169 + have "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> (a i \<inter> d) \<inter> (a j \<inter> d) = {}" by auto
1.170 + from dynkin_UN[OF \<delta>ynkin this]
1.171 + have "UNION UNIV (\<lambda> i. a i \<inter> d) \<in> sets \<delta>E"
1.172 + using aE by auto
1.173 + hence **: "UNION UNIV a \<inter> d \<in> sets \<delta>E" by auto
1.174 + from * ** show "UNION UNIV a \<in> Dy d" unfolding Dy_def \<delta>E_def by auto
1.175 + qed } note Dy_nkin = this
1.176 + have E_\<delta>E: "sets E \<subseteq> sets \<delta>E"
1.177 + unfolding \<delta>E_def sets_\<delta>E_def by auto
1.178 + { fix d assume dasm: "d \<in> sets \<delta>E"
1.179 + { fix e assume easm: "e \<in> sets E"
1.180 + hence deasm: "e \<in> sets \<delta>E"
1.181 + unfolding \<delta>E_def sets_\<delta>E_def by auto
1.182 + have subset: "Dy e \<subseteq> sets \<delta>E"
1.183 + unfolding Dy_def \<delta>E_def by auto
1.184 + { fix e' assume e'asm: "e' \<in> sets E"
1.185 + have "e' \<inter> e \<in> sets E"
1.186 + using easm e'asm stab unfolding Int_stable_def by auto
1.187 + hence "e' \<inter> e \<in> sets \<delta>E"
1.188 + unfolding \<delta>E_def sets_\<delta>E_def by auto
1.189 + hence "e' \<in> Dy e" using e'asm unfolding Dy_def \<delta>E_def sets_\<delta>E_def by auto }
1.190 + hence E_Dy: "sets E \<subseteq> Dy e" by auto
1.191 + have "\<lparr> space = space E, sets = Dy e \<rparr> \<in> {d | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
1.192 + using Dy_nkin[OF deasm[unfolded \<delta>E_def, simplified]] E_\<delta>E E_Dy by auto
1.193 + hence "sets_\<delta>E \<subseteq> Dy e"
1.194 + unfolding sets_\<delta>E_def
1.195 + proof auto fix x
1.196 + assume asm: "\<forall>xa. (\<exists>d :: 'a algebra. xa = sets d \<and>
1.197 + dynkin d \<and>
1.198 + space d = space E \<and>
1.199 + sets E \<subseteq> sets d) \<longrightarrow>
1.200 + x \<in> xa"
1.201 + "dynkin \<lparr>space = space E, sets = Dy e\<rparr>"
1.202 + "sets E \<subseteq> Dy e"
1.203 + show "x \<in> Dy e"
1.204 + apply (rule impE[OF spec[OF asm(1), of "Dy e"]])
1.205 + apply (rule exI[of _ "\<lparr>space = space E, sets = Dy e\<rparr>"])
1.206 + using asm by auto
1.207 + qed
1.208 + hence "sets \<delta>E = Dy e" using subset unfolding \<delta>E_def by auto
1.209 + hence "d \<inter> e \<in> sets \<delta>E"
1.210 + using dasm easm deasm unfolding Dy_def \<delta>E_def by auto
1.211 + hence "e \<in> Dy d" using deasm
1.212 + unfolding Dy_def \<delta>E_def
1.213 + by (auto simp add:Int_commute) }
1.214 + hence "sets E \<subseteq> Dy d" by auto
1.215 + hence "sets \<delta>E \<subseteq> Dy d" using Dy_nkin[OF dasm[unfolded \<delta>E_def, simplified]]
1.216 + unfolding \<delta>E_def sets_\<delta>E_def
1.217 + proof auto
1.218 + fix x
1.219 + assume asm: "sets E \<subseteq> Dy d"
1.220 + "dynkin \<lparr>space = space E, sets = Dy d\<rparr>"
1.221 + "\<forall>xa. (\<exists>d :: 'a algebra. xa = sets d \<and> dynkin d \<and>
1.222 + space d = space E \<and> sets E \<subseteq> sets d) \<longrightarrow> x \<in> xa"
1.223 + show "x \<in> Dy d"
1.224 + apply (rule impE[OF spec[OF asm(3), of "Dy d"]])
1.225 + apply (rule exI[of _ "\<lparr>space = space E, sets = Dy d\<rparr>"])
1.226 + using asm by auto
1.227 + qed
1.228 + hence *: "sets \<delta>E = Dy d"
1.229 + unfolding Dy_def \<delta>E_def by auto
1.230 + fix a assume aasm: "a \<in> sets \<delta>E"
1.231 + hence "a \<inter> d \<in> sets \<delta>E"
1.232 + using * dasm unfolding Dy_def \<delta>E_def by auto } note \<delta>E_stab = this
1.233 + have "sigma_algebra D"
1.234 + apply unfold_locales
1.235 + using dynkin_subset[OF dyn]
1.236 + using dynkin_diff[OF dyn, of _ "space D", OF _ dynkin_space[OF dyn]]
1.237 + using dynkin_diff[OF dyn, of "space D" "space D", OF dynkin_space[OF dyn] dynkin_space[OF dyn]]
1.238 + using dynkin_space[OF dyn]
1.239 + proof auto
1.240 + 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.241 + "\<And>a. a \<in> sets D \<Longrightarrow> space D - a \<in> sets D"
1.242 + "{} \<in> sets D" "space D \<in> sets D"
1.243 + let "?A i" = "A i - (\<Inter> j \<in> {..< i}. A j)"
1.244 + { fix i :: nat assume "i > 0"
1.245 + have "(\<Inter> j \<in> {..< i}. A j) \<in> sets \<delta>E"
1.246 + apply (induct i)
1.247 + apply auto
1.248 + }
1.249 + from dynkin_UN
1.250 + qed
1.251 +qed
1.252 +
1.253 +lemma
1.254 +(*
1.255 definition prod_sets where
1.256 "prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"
1.257
1.258 @@ -153,4 +401,5 @@
1.259 unfolding finite_prod_measure_space[OF N, symmetric]
1.260 using finite_measure_space_finite_prod_measure[OF N] .
1.261
1.262 +*)
1.263 end
1.264 \ No newline at end of file