author hoelzl Tue Mar 22 18:53:05 2011 +0100 (2011-03-22) changeset 42066 6db76c88907a parent 42065 2b98b4c2e2f1 child 42067 66c8281349ec
generalized Caratheodory from algebra to ring_of_sets
```     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Tue Mar 22 16:44:57 2011 +0100
1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue Mar 22 18:53:05 2011 +0100
1.3 @@ -148,7 +148,7 @@
1.4
1.5  lemma (in algebra) lambda_system_empty:
1.6    "positive M f \<Longrightarrow> {} \<in> lambda_system M f"
1.7 -  by (auto simp add: positive_def lambda_system_eq algebra_def)
1.8 +  by (auto simp add: positive_def lambda_system_eq)
1.9
1.10  lemma lambda_system_sets:
1.11    "x \<in> lambda_system M f \<Longrightarrow> x \<in> sets M"
1.12 @@ -456,7 +456,7 @@
1.14  qed
1.15
1.19    shows "increasing M f"
1.20  proof (auto simp add: increasing_def)
1.21 @@ -472,7 +472,7 @@
1.22    finally show "f x \<le> f y" by simp
1.23  qed
1.24
1.27    assumes posf: "positive M f" and ca: "countably_additive M f"
1.30 @@ -506,7 +506,7 @@
1.31               simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def)
1.32  qed
1.33
1.34 -lemma (in algebra) inf_measure_agrees:
1.35 +lemma (in ring_of_sets) inf_measure_agrees:
1.36    assumes posf: "positive M f" and ca: "countably_additive M f"
1.37        and s: "s \<in> sets M"
1.38    shows "Inf (measure_set M f s) = f s"
1.39 @@ -575,7 +575,7 @@
1.40                inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def])
1.41  qed (rule inf_measure_pos[OF posf])
1.42
1.43 -lemma (in algebra) inf_measure_positive:
1.44 +lemma (in ring_of_sets) inf_measure_positive:
1.45    assumes p: "positive M f" and "{} \<in> sets M"
1.46    shows "positive M (\<lambda>x. Inf (measure_set M f x))"
1.47  proof (unfold positive_def, intro conjI ballI)
1.48 @@ -583,7 +583,7 @@
1.49    fix A assume "A \<in> sets M"
1.50  qed (rule inf_measure_pos[OF p])
1.51
1.52 -lemma (in algebra) inf_measure_increasing:
1.53 +lemma (in ring_of_sets) inf_measure_increasing:
1.54    assumes posf: "positive M f"
1.55    shows "increasing \<lparr> space = space M, sets = Pow (space M) \<rparr>
1.56                      (\<lambda>x. Inf (measure_set M f x))"
1.57 @@ -593,7 +593,7 @@
1.58  apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast)
1.59  done
1.60
1.61 -lemma (in algebra) inf_measure_le:
1.62 +lemma (in ring_of_sets) inf_measure_le:
1.63    assumes posf: "positive M f" and inc: "increasing M f"
1.64        and x: "x \<in> {r . \<exists>A. range A \<subseteq> sets M \<and> s \<subseteq> (\<Union>i. A i) \<and> (\<Sum>i. f (A i)) = r}"
1.65    shows "Inf (measure_set M f s) \<le> x"
1.66 @@ -620,73 +620,63 @@
1.67      by (blast intro: y order_trans [OF _ ley] posf complete_lattice_class.Inf_lower)
1.68  qed
1.69
1.70 -lemma (in algebra) inf_measure_close:
1.71 +lemma (in ring_of_sets) inf_measure_close:
1.72    fixes e :: extreal
1.73 -  assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (space M)"
1.74 +  assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (space M)" and "Inf (measure_set M f s) \<noteq> \<infinity>"
1.75    shows "\<exists>A. range A \<subseteq> sets M \<and> disjoint_family A \<and> s \<subseteq> (\<Union>i. A i) \<and>
1.76                 (\<Sum>i. f (A i)) \<le> Inf (measure_set M f s) + e"
1.77 -proof (cases "Inf (measure_set M f s) = \<infinity>")
1.78 -  case False
1.79 -  then have fin: "\<bar>Inf (measure_set M f s)\<bar> \<noteq> \<infinity>"
1.80 +proof -
1.81 +  from `Inf (measure_set M f s) \<noteq> \<infinity>` have fin: "\<bar>Inf (measure_set M f s)\<bar> \<noteq> \<infinity>"
1.82      using inf_measure_pos[OF posf, of s] by auto
1.83    obtain l where "l \<in> measure_set M f s" "l \<le> Inf (measure_set M f s) + e"
1.84      using Inf_extreal_close[OF fin e] by auto
1.85    thus ?thesis
1.86      by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
1.87 -next
1.88 -  case True
1.89 -  have "measure_set M f s \<noteq> {}"
1.90 -    by (metis emptyE ss inf_measure_nonempty [of _ f, OF posf top _ empty_sets])
1.91 -  then obtain l where "l \<in> measure_set M f s" by auto
1.92 -  moreover from True have "l \<le> Inf (measure_set M f s) + e" by simp
1.93 -  ultimately show ?thesis
1.94 -    by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
1.95  qed
1.96
1.99    assumes posf: "positive M f" and inc: "increasing M f"
1.100    shows "countably_subadditive (| space = space M, sets = Pow (space M) |)
1.101                    (\<lambda>x. Inf (measure_set M f x))"
1.103 -proof (safe, simp, rule extreal_le_epsilon, safe)
1.104 -  fix A :: "nat \<Rightarrow> 'a set" and e :: extreal
1.105 -  let "?outer n" = "Inf (measure_set M f (A n))"
1.107 +  fix A :: "nat \<Rightarrow> 'a set"
1.108 +  let "?outer B" = "Inf (measure_set M f B)"
1.109    assume A: "range A \<subseteq> Pow (space M)"
1.110       and disj: "disjoint_family A"
1.111       and sb: "(\<Union>i. A i) \<subseteq> space M"
1.112 -     and e: "0 < e"
1.113 -  hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
1.114 -                   A n \<subseteq> (\<Union>i. BB n i) \<and>
1.115 -                   (\<Sum>i. f (BB n i)) \<le> ?outer n + e * (1/2)^(Suc n)"
1.116 -    apply (safe intro!: choice inf_measure_close [of f, OF posf])
1.117 -    using e sb by (cases e) (auto simp add: not_le mult_pos_pos one_extreal_def)
1.118 -  then obtain BB
1.119 -    where BB: "\<And>n. (range (BB n) \<subseteq> sets M)"
1.120 +
1.121 +  { fix e :: extreal assume e: "0 < e" and "\<forall>i. ?outer (A i) \<noteq> \<infinity>"
1.122 +    hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
1.123 +        A n \<subseteq> (\<Union>i. BB n i) \<and> (\<Sum>i. f (BB n i)) \<le> ?outer (A n) + e * (1/2)^(Suc n)"
1.124 +      apply (safe intro!: choice inf_measure_close [of f, OF posf])
1.125 +      using e sb by (auto simp: extreal_zero_less_0_iff one_extreal_def)
1.126 +    then obtain BB
1.127 +      where BB: "\<And>n. (range (BB n) \<subseteq> sets M)"
1.128        and disjBB: "\<And>n. disjoint_family (BB n)"
1.129        and sbBB: "\<And>n. A n \<subseteq> (\<Union>i. BB n i)"
1.130 -      and BBle: "\<And>n. (\<Sum>i. f (BB n i)) \<le> ?outer n + e * (1/2)^(Suc n)"
1.131 -    by auto blast
1.132 -  have sll: "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> suminf ?outer + e"
1.133 +      and BBle: "\<And>n. (\<Sum>i. f (BB n i)) \<le> ?outer (A n) + e * (1/2)^(Suc n)"
1.134 +      by auto blast
1.135 +    have sll: "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n)) + e"
1.136      proof -
1.137        have sum_eq_1: "(\<Sum>n. e*(1/2) ^ Suc n) = e"
1.138          using suminf_half_series_extreal e
1.139          by (simp add: extreal_zero_le_0_iff zero_le_divide_extreal suminf_cmult_extreal)
1.140        have "\<And>n i. 0 \<le> f (BB n i)" using posf[unfolded positive_def] BB by auto
1.141        then have "\<And>n. 0 \<le> (\<Sum>i. f (BB n i))" by (rule suminf_0_le)
1.142 -      then have "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer n + e*(1/2) ^ Suc n)"
1.143 +      then have "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n) + e*(1/2) ^ Suc n)"
1.144          by (rule suminf_le_pos[OF BBle])
1.145 -      also have "... = suminf ?outer + e"
1.146 +      also have "... = (\<Sum>n. ?outer (A n)) + e"
1.147          using sum_eq_1 inf_measure_pos[OF posf] e
1.149        finally show ?thesis .
1.150      qed
1.151 -  def C \<equiv> "(split BB) o prod_decode"
1.152 -  have C: "!!n. C n \<in> sets M"
1.153 -    apply (rule_tac p="prod_decode n" in PairE)
1.154 -    apply (simp add: C_def)
1.155 -    apply (metis BB subsetD rangeI)
1.156 -    done
1.157 -  have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
1.158 +    def C \<equiv> "(split BB) o prod_decode"
1.159 +    have C: "!!n. C n \<in> sets M"
1.160 +      apply (rule_tac p="prod_decode n" in PairE)
1.161 +      apply (simp add: C_def)
1.162 +      apply (metis BB subsetD rangeI)
1.163 +      done
1.164 +    have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
1.165      proof (auto simp add: C_def)
1.166        fix x i
1.167        assume x: "x \<in> A i"
1.168 @@ -695,23 +685,39 @@
1.169        thus "\<exists>i. x \<in> split BB (prod_decode i)"
1.170          by (metis prod_encode_inverse prod.cases)
1.171      qed
1.172 -  have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
1.173 -    by (rule ext)  (auto simp add: C_def)
1.174 -  moreover have "suminf ... = (\<Sum>n. \<Sum>i. f (BB n i))" using BBle
1.175 -    using BB posf[unfolded positive_def]
1.176 -    by (force intro!: suminf_extreal_2dimen simp: o_def)
1.177 -  ultimately have Csums: "(\<Sum>i. f (C i)) = (\<Sum>n. \<Sum>i. f (BB n i))" by (simp add: o_def)
1.178 -  have "Inf (measure_set M f (\<Union>i. A i)) \<le> (\<Sum>n. \<Sum>i. f (BB n i))"
1.179 -    apply (rule inf_measure_le [OF posf(1) inc], auto)
1.180 -    apply (rule_tac x="C" in exI)
1.181 -    apply (auto simp add: C sbC Csums)
1.182 -    done
1.183 -  also have "... \<le> (\<Sum>n. Inf (measure_set M f (A n))) + e" using sll
1.184 -    by blast
1.185 -  finally show "Inf (measure_set M f (\<Union>i. A i)) \<le> suminf ?outer + e" .
1.186 +    have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
1.187 +      by (rule ext)  (auto simp add: C_def)
1.188 +    moreover have "suminf ... = (\<Sum>n. \<Sum>i. f (BB n i))" using BBle
1.189 +      using BB posf[unfolded positive_def]
1.190 +      by (force intro!: suminf_extreal_2dimen simp: o_def)
1.191 +    ultimately have Csums: "(\<Sum>i. f (C i)) = (\<Sum>n. \<Sum>i. f (BB n i))" by (simp add: o_def)
1.192 +    have "?outer (\<Union>i. A i) \<le> (\<Sum>n. \<Sum>i. f (BB n i))"
1.193 +      apply (rule inf_measure_le [OF posf(1) inc], auto)
1.194 +      apply (rule_tac x="C" in exI)
1.195 +      apply (auto simp add: C sbC Csums)
1.196 +      done
1.197 +    also have "... \<le> (\<Sum>n. ?outer (A n)) + e" using sll
1.198 +      by blast
1.199 +    finally have "?outer (\<Union>i. A i) \<le> (\<Sum>n. ?outer (A n)) + e" . }
1.200 +  note for_finite_Inf = this
1.201 +
1.202 +  show "?outer (\<Union>i. A i) \<le> (\<Sum>n. ?outer (A n))"
1.203 +  proof cases
1.204 +    assume "\<forall>i. ?outer (A i) \<noteq> \<infinity>"
1.205 +    with for_finite_Inf show ?thesis
1.206 +      by (intro extreal_le_epsilon) auto
1.207 +  next
1.208 +    assume "\<not> (\<forall>i. ?outer (A i) \<noteq> \<infinity>)"
1.209 +    then have "\<exists>i. ?outer (A i) = \<infinity>"
1.210 +      by auto
1.211 +    then have "(\<Sum>n. ?outer (A n)) = \<infinity>"
1.212 +      using suminf_PInfty[OF inf_measure_pos, OF posf]
1.213 +      by metis
1.214 +    then show ?thesis by simp
1.215 +  qed
1.216  qed
1.217
1.218 -lemma (in algebra) inf_measure_outer:
1.219 +lemma (in ring_of_sets) inf_measure_outer:
1.220    "\<lbrakk> positive M f ; increasing M f \<rbrakk>
1.221     \<Longrightarrow> outer_measure_space \<lparr> space = space M, sets = Pow (space M) \<rparr>
1.222                            (\<lambda>x. Inf (measure_set M f x))"
1.223 @@ -719,12 +725,10 @@
1.224    by (simp add: outer_measure_space_def inf_measure_empty
1.226
1.227 -(*MOVE UP*)
1.228 -
1.229 -lemma (in algebra) algebra_subset_lambda_system:
1.230 +lemma (in ring_of_sets) algebra_subset_lambda_system:
1.231    assumes posf: "positive M f" and inc: "increasing M f"
1.233 -  shows "sets M \<subseteq> lambda_system (| space = space M, sets = Pow (space M) |)
1.234 +  shows "sets M \<subseteq> lambda_system \<lparr> space = space M, sets = Pow (space M) \<rparr>
1.235                                  (\<lambda>x. Inf (measure_set M f x))"
1.236  proof (auto dest: sets_into_space
1.237              simp add: algebra.lambda_system_eq [OF algebra_Pow])
1.238 @@ -735,50 +739,42 @@
1.239      by blast
1.240    have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
1.241          \<le> Inf (measure_set M f s)"
1.242 -    proof (rule extreal_le_epsilon, intro allI impI)
1.243 -      fix e :: extreal
1.244 -      assume e: "0 < e"
1.245 -      from inf_measure_close [of f, OF posf e s]
1.246 -      obtain A where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
1.247 -                 and sUN: "s \<subseteq> (\<Union>i. A i)"
1.248 -                 and l: "(\<Sum>i. f (A i)) \<le> Inf (measure_set M f s) + e"
1.249 -        by auto
1.250 -      have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
1.251 -                      (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
1.252 -        by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
1.253 -      have  [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)"
1.255 -           (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
1.256 -      { fix u
1.257 -        assume u: "u \<in> sets M"
1.258 -        have [simp]: "\<And>n. f (A n \<inter> u) \<le> f (A n)"
1.259 -          by (simp add: increasingD [OF inc] u Int range_subsetD [OF A])
1.260 -        have 2: "Inf (measure_set M f (s \<inter> u)) \<le> (\<Sum>i. f (A i \<inter> u))"
1.261 -          proof (rule complete_lattice_class.Inf_lower)
1.262 -            show "(\<Sum>i. f (A i \<inter> u)) \<in> measure_set M f (s \<inter> u)"
1.263 -              apply (simp add: measure_set_def)
1.264 -              apply (rule_tac x="(\<lambda>z. z \<inter> u) o A" in exI)
1.265 -              apply (auto simp add: disjoint_family_subset [OF disj] o_def)
1.266 -              apply (blast intro: u range_subsetD [OF A])
1.267 -              apply (blast dest: subsetD [OF sUN])
1.268 -              done
1.269 -          qed
1.270 -      } note lesum = this
1.271 -      have [simp]: "\<And>i. A i \<inter> (space M - x) = A i - x" using A sets_into_space by auto
1.272 -      have inf1: "Inf (measure_set M f (s\<inter>x)) \<le> (\<Sum>i. f (A i \<inter> x))"
1.273 -        and inf2: "Inf (measure_set M f (s \<inter> (space M - x)))
1.274 -                   \<le> (\<Sum>i. f (A i \<inter> (space M - x)))"
1.275 -        by (metis Diff lesum top x)+
1.276 -      hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
1.277 -           \<le> (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))"
1.279 -      also have "... \<le> (\<Sum>i. f (A i))" using posf[unfolded positive_def] A x
1.280 -        by (subst suminf_add_extreal[symmetric]) auto
1.281 -      also have "... \<le> Inf (measure_set M f s) + e"
1.282 -        by (rule l)
1.283 -      finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
1.284 -        \<le> Inf (measure_set M f s) + e" .
1.285 +  proof cases
1.286 +    assume "Inf (measure_set M f s) = \<infinity>" then show ?thesis by simp
1.287 +  next
1.288 +    assume fin: "Inf (measure_set M f s) \<noteq> \<infinity>"
1.289 +    then have "measure_set M f s \<noteq> {}"
1.290 +      by (auto simp: top_extreal_def)
1.291 +    show ?thesis
1.292 +    proof (rule complete_lattice_class.Inf_greatest)
1.293 +      fix r assume "r \<in> measure_set M f s"
1.294 +      then obtain A where A: "disjoint_family A" "range A \<subseteq> sets M" "s \<subseteq> (\<Union>i. A i)"
1.295 +        and r: "r = (\<Sum>i. f (A i))" unfolding measure_set_def by auto
1.296 +      have "Inf (measure_set M f (s \<inter> x)) \<le> (\<Sum>i. f (A i \<inter> x))"
1.297 +        unfolding measure_set_def
1.298 +      proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\<lambda>i. A i \<inter> x"])
1.299 +        from A(1) show "disjoint_family (\<lambda>i. A i \<inter> x)"
1.300 +          by (rule disjoint_family_on_bisimulation) auto
1.301 +      qed (insert x A, auto)
1.302 +      moreover
1.303 +      have "Inf (measure_set M f (s - x)) \<le> (\<Sum>i. f (A i - x))"
1.304 +        unfolding measure_set_def
1.305 +      proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\<lambda>i. A i - x"])
1.306 +        from A(1) show "disjoint_family (\<lambda>i. A i - x)"
1.307 +          by (rule disjoint_family_on_bisimulation) auto
1.308 +      qed (insert x A, auto)
1.309 +      ultimately have "Inf (measure_set M f (s \<inter> x)) + Inf (measure_set M f (s - x)) \<le>
1.310 +          (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))" by (rule add_mono)
1.311 +      also have "\<dots> = (\<Sum>i. f (A i \<inter> x) + f (A i - x))"
1.312 +        using A(2) x posf by (subst suminf_add_extreal) (auto simp: positive_def)
1.313 +      also have "\<dots> = (\<Sum>i. f (A i))"
1.314 +        using A x
1.316 +           (auto intro!: arg_cong[where f=suminf] arg_cong[where f=f])
1.317 +      finally show "Inf (measure_set M f (s \<inter> x)) + Inf (measure_set M f (s - x)) \<le> r"
1.318 +        using r by simp
1.319      qed
1.320 +  qed
1.321    moreover
1.322    have "Inf (measure_set M f s)
1.323         \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
1.324 @@ -805,7 +801,7 @@
1.326       blast
1.327
1.328 -theorem (in algebra) caratheodory:
1.329 +theorem (in ring_of_sets) caratheodory:
1.330    assumes posf: "positive M f" and ca: "countably_additive M f"
1.331    shows "\<exists>\<mu> :: 'a set \<Rightarrow> extreal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and>
1.332              measure_space \<lparr> space = space M, sets = sets (sigma M), measure = \<mu> \<rparr>"
```
```     2.1 --- a/src/HOL/Probability/Measure.thy	Tue Mar 22 16:44:57 2011 +0100
2.2 +++ b/src/HOL/Probability/Measure.thy	Tue Mar 22 18:53:05 2011 +0100
2.3 @@ -107,10 +107,7 @@
2.4  qed
2.5