New theory Probability, which contains a development of measure theory
authorpaulson
Wed Oct 28 11:42:31 2009 +0000 (2009-10-28)
changeset 332717be66dee1a5a
parent 33270 320a1d67b9ae
child 33272 73a0c804840f
New theory Probability, which contains a development of measure theory
NEWS
src/HOL/IsaMakefile
src/HOL/Library/FuncSet.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Measure.thy
src/HOL/Probability/Probability.thy
src/HOL/Probability/ROOT.ML
src/HOL/Probability/SeriesPlus.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Product_Type.thy
src/HOL/SEQ.thy
src/HOL/Series.thy
src/HOL/SupInf.thy
     1.1 --- a/NEWS	Tue Oct 27 14:46:03 2009 +0000
     1.2 +++ b/NEWS	Wed Oct 28 11:42:31 2009 +0000
     1.3 @@ -67,6 +67,8 @@
     1.4  
     1.5  * New theory SupInf of the supremum and infimum operators for sets of reals.
     1.6  
     1.7 +* New theory Probability containing a development of measure theory, eventually leading to Lebesgue integration and probability.
     1.8 +
     1.9  * Split off prime number ingredients from theory GCD
    1.10  to theory Number_Theory/Primes;
    1.11  
     2.1 --- a/src/HOL/IsaMakefile	Tue Oct 27 14:46:03 2009 +0000
     2.2 +++ b/src/HOL/IsaMakefile	Wed Oct 28 11:42:31 2009 +0000
     2.3 @@ -51,6 +51,7 @@
     2.4    HOL-Nominal-Examples \
     2.5    HOL-Number_Theory \
     2.6    HOL-Old_Number_Theory \
     2.7 +  HOL-Probability \
     2.8    HOL-Prolog \
     2.9    HOL-SET_Protocol \
    2.10    HOL-SMT-Examples \
    2.11 @@ -1060,6 +1061,18 @@
    2.12    Multivariate_Analysis/Convex_Euclidean_Space.thy
    2.13  	@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis
    2.14  
    2.15 +## HOL-Probability
    2.16 +
    2.17 +HOL-Probability: HOL $(LOG)/HOL-Probability.gz
    2.18 +
    2.19 +$(LOG)/HOL-Probability.gz: $(OUT)/HOL Probability/ROOT.ML \
    2.20 +  Probability/Probability.thy \
    2.21 +  Probability/Sigma_Algebra.thy \
    2.22 +  Probability/SeriesPlus.thy \
    2.23 +  Probability/Caratheodory.thy \
    2.24 +  Probability/Measure.thy
    2.25 +	$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Probability
    2.26 +
    2.27  ## HOL-Nominal
    2.28  
    2.29  HOL-Nominal: HOL $(OUT)/HOL-Nominal
     3.1 --- a/src/HOL/Library/FuncSet.thy	Tue Oct 27 14:46:03 2009 +0000
     3.2 +++ b/src/HOL/Library/FuncSet.thy	Wed Oct 28 11:42:31 2009 +0000
     3.3 @@ -101,6 +101,19 @@
     3.4  lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B"
     3.5  by auto
     3.6  
     3.7 +lemma prod_final:
     3.8 +  assumes 1: "fst \<circ> f \<in> Pi A B" and 2: "snd \<circ> f \<in> Pi A C"
     3.9 +  shows "f \<in> (\<Pi> z \<in> A. B z \<times> C z)"
    3.10 +proof (rule Pi_I) 
    3.11 +  fix z
    3.12 +  assume z: "z \<in> A" 
    3.13 +  have "f z = (fst (f z), snd (f z))" 
    3.14 +    by simp
    3.15 +  also have "...  \<in> B z \<times> C z"
    3.16 +    by (metis SigmaI PiE o_apply 1 2 z) 
    3.17 +  finally show "f z \<in> B z \<times> C z" .
    3.18 +qed
    3.19 +
    3.20  
    3.21  subsection{*Composition With a Restricted Domain: @{term compose}*}
    3.22  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Probability/Caratheodory.thy	Wed Oct 28 11:42:31 2009 +0000
     4.3 @@ -0,0 +1,993 @@
     4.4 +header {*Caratheodory Extension Theorem*}
     4.5 +
     4.6 +theory Caratheodory
     4.7 +  imports Sigma_Algebra SupInf SeriesPlus
     4.8 +
     4.9 +begin
    4.10 +
    4.11 +text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
    4.12 +
    4.13 +subsection {* Measure Spaces *}
    4.14 +
    4.15 +text {*A measure assigns a nonnegative real to every measurable set. 
    4.16 +       It is countably additive for disjoint sets.*}
    4.17 +
    4.18 +record 'a measure_space = "'a algebra" +
    4.19 +  measure:: "'a set \<Rightarrow> real"
    4.20 +
    4.21 +definition
    4.22 +  disjoint_family  where
    4.23 +  "disjoint_family A \<longleftrightarrow> (\<forall>m n. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
    4.24 +
    4.25 +definition
    4.26 +  positive  where
    4.27 +  "positive M f \<longleftrightarrow> f {} = (0::real) & (\<forall>x \<in> sets M. 0 \<le> f x)"
    4.28 +
    4.29 +definition
    4.30 +  additive  where
    4.31 +  "additive M f \<longleftrightarrow> 
    4.32 +    (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {} 
    4.33 +    \<longrightarrow> f (x \<union> y) = f x + f y)"
    4.34 +
    4.35 +definition
    4.36 +  countably_additive  where
    4.37 +  "countably_additive M f \<longleftrightarrow> 
    4.38 +    (\<forall>A. range A \<subseteq> sets M \<longrightarrow> 
    4.39 +         disjoint_family A \<longrightarrow>
    4.40 +         (\<Union>i. A i) \<in> sets M \<longrightarrow> 
    4.41 +         (\<lambda>n. f (A n))  sums  f (\<Union>i. A i))"
    4.42 +
    4.43 +definition
    4.44 +  increasing  where
    4.45 +  "increasing M f \<longleftrightarrow> (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<subseteq> y \<longrightarrow> f x \<le> f y)"
    4.46 +
    4.47 +definition
    4.48 +  subadditive  where
    4.49 +  "subadditive M f \<longleftrightarrow> 
    4.50 +    (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {} 
    4.51 +    \<longrightarrow> f (x \<union> y) \<le> f x + f y)"
    4.52 +
    4.53 +definition
    4.54 +  countably_subadditive  where
    4.55 +  "countably_subadditive M f \<longleftrightarrow> 
    4.56 +    (\<forall>A. range A \<subseteq> sets M \<longrightarrow> 
    4.57 +         disjoint_family A \<longrightarrow>
    4.58 +         (\<Union>i. A i) \<in> sets M \<longrightarrow> 
    4.59 +         summable (f o A) \<longrightarrow>
    4.60 +         f (\<Union>i. A i) \<le> suminf (\<lambda>n. f (A n)))"
    4.61 +
    4.62 +definition
    4.63 +  lambda_system where
    4.64 +  "lambda_system M f = 
    4.65 +    {l. l \<in> sets M & (\<forall>x \<in> sets M. f (l \<inter> x) + f ((space M - l) \<inter> x) = f x)}"
    4.66 +
    4.67 +definition
    4.68 +  outer_measure_space where
    4.69 +  "outer_measure_space M f  \<longleftrightarrow> 
    4.70 +     positive M f & increasing M f & countably_subadditive M f"
    4.71 +
    4.72 +definition
    4.73 +  measure_set where
    4.74 +  "measure_set M f X =
    4.75 +     {r . \<exists>A. range A \<subseteq> sets M & disjoint_family A & X \<subseteq> (\<Union>i. A i) & (f \<circ> A) sums r}"
    4.76 +
    4.77 +
    4.78 +locale measure_space = sigma_algebra +
    4.79 +  assumes positive: "!!a. a \<in> sets M \<Longrightarrow> 0 \<le> measure M a"
    4.80 +      and empty_measure [simp]: "measure M {} = (0::real)"
    4.81 +      and ca: "countably_additive M (measure M)"
    4.82 +
    4.83 +subsection {* Basic Lemmas *}
    4.84 +
    4.85 +lemma positive_imp_0: "positive M f \<Longrightarrow> f {} = 0"
    4.86 +  by (simp add: positive_def) 
    4.87 +
    4.88 +lemma positive_imp_pos: "positive M f \<Longrightarrow> x \<in> sets M \<Longrightarrow> 0 \<le> f x"
    4.89 +  by (simp add: positive_def) 
    4.90 +
    4.91 +lemma increasingD:
    4.92 +     "increasing M f \<Longrightarrow> x \<subseteq> y \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M \<Longrightarrow> f x \<le> f y"
    4.93 +  by (auto simp add: increasing_def)
    4.94 +
    4.95 +lemma subadditiveD:
    4.96 +     "subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M 
    4.97 +      \<Longrightarrow> f (x \<union> y) \<le> f x + f y"
    4.98 +  by (auto simp add: subadditive_def)
    4.99 +
   4.100 +lemma additiveD:
   4.101 +     "additive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M 
   4.102 +      \<Longrightarrow> f (x \<union> y) = f x + f y"
   4.103 +  by (auto simp add: additive_def)
   4.104 +
   4.105 +lemma countably_additiveD:
   4.106 +  "countably_additive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A 
   4.107 +   \<Longrightarrow> (\<Union>i. A i) \<in> sets M \<Longrightarrow> (\<lambda>n. f (A n))  sums  f (\<Union>i. A i)"
   4.108 +  by (simp add: countably_additive_def) 
   4.109 +
   4.110 +lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
   4.111 +  by blast
   4.112 +
   4.113 +lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
   4.114 +  by blast
   4.115 +
   4.116 +lemma disjoint_family_subset:
   4.117 +     "disjoint_family A \<Longrightarrow> (!!x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
   4.118 +  by (force simp add: disjoint_family_def) 
   4.119 +
   4.120 +subsection {* A Two-Element Series *}
   4.121 +
   4.122 +definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "
   4.123 +  where "binaryset A B = (\<lambda>\<^isup>x. {})(0 := A, Suc 0 := B)"
   4.124 +
   4.125 +lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"
   4.126 +  apply (simp add: binaryset_def) 
   4.127 +  apply (rule set_ext) 
   4.128 +  apply (auto simp add: image_iff) 
   4.129 +  done
   4.130 +
   4.131 +lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
   4.132 +  by (simp add: UNION_eq_Union_image range_binaryset_eq) 
   4.133 +
   4.134 +lemma LIMSEQ_binaryset: 
   4.135 +  assumes f: "f {} = 0"
   4.136 +  shows  "(\<lambda>n. \<Sum>i = 0..<n. f (binaryset A B i)) ----> f A + f B"
   4.137 +proof -
   4.138 +  have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) = (\<lambda>n. f A + f B)"
   4.139 +    proof 
   4.140 +      fix n
   4.141 +      show "(\<Sum>i\<Colon>nat = 0\<Colon>nat..<Suc (Suc n). f (binaryset A B i)) = f A + f B"
   4.142 +	by (induct n)  (auto simp add: binaryset_def f) 
   4.143 +    qed
   4.144 +  moreover
   4.145 +  have "... ----> f A + f B" by (rule LIMSEQ_const) 
   4.146 +  ultimately
   4.147 +  have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) ----> f A + f B" 
   4.148 +    by metis
   4.149 +  hence "(\<lambda>n. \<Sum>i = 0..< n+2. f (binaryset A B i)) ----> f A + f B"
   4.150 +    by simp
   4.151 +  thus ?thesis by (rule LIMSEQ_offset [where k=2])
   4.152 +qed
   4.153 +
   4.154 +lemma binaryset_sums:
   4.155 +  assumes f: "f {} = 0"
   4.156 +  shows  "(\<lambda>n. f (binaryset A B n)) sums (f A + f B)"
   4.157 +    by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f]) 
   4.158 +
   4.159 +lemma suminf_binaryset_eq:
   4.160 +     "f {} = 0 \<Longrightarrow> suminf (\<lambda>n. f (binaryset A B n)) = f A + f B"
   4.161 +  by (metis binaryset_sums sums_unique)
   4.162 +
   4.163 +
   4.164 +subsection {* Lambda Systems *}
   4.165 +
   4.166 +lemma (in algebra) lambda_system_eq:
   4.167 +    "lambda_system M f = 
   4.168 +        {l. l \<in> sets M & (\<forall>x \<in> sets M. f (x \<inter> l) + f (x - l) = f x)}"
   4.169 +proof -
   4.170 +  have [simp]: "!!l x. l \<in> sets M \<Longrightarrow> x \<in> sets M \<Longrightarrow> (space M - l) \<inter> x = x - l"
   4.171 +    by (metis Diff_eq Int_Diff Int_absorb1 Int_commute sets_into_space)
   4.172 +  show ?thesis
   4.173 +    by (auto simp add: lambda_system_def) (metis Diff_Compl Int_commute)+
   4.174 +qed
   4.175 +
   4.176 +lemma (in algebra) lambda_system_empty:
   4.177 +    "positive M f \<Longrightarrow> {} \<in> lambda_system M f"
   4.178 +  by (auto simp add: positive_def lambda_system_eq) 
   4.179 +
   4.180 +lemma lambda_system_sets:
   4.181 +    "x \<in> lambda_system M f \<Longrightarrow> x \<in> sets M"
   4.182 +  by (simp add:  lambda_system_def)
   4.183 +
   4.184 +lemma (in algebra) lambda_system_Compl:
   4.185 +  fixes f:: "'a set \<Rightarrow> real"
   4.186 +  assumes x: "x \<in> lambda_system M f"
   4.187 +  shows "space M - x \<in> lambda_system M f"
   4.188 +  proof -
   4.189 +    have "x \<subseteq> space M"
   4.190 +      by (metis sets_into_space lambda_system_sets x)
   4.191 +    hence "space M - (space M - x) = x"
   4.192 +      by (metis double_diff equalityE) 
   4.193 +    with x show ?thesis
   4.194 +      by (force simp add: lambda_system_def)
   4.195 +  qed
   4.196 +
   4.197 +lemma (in algebra) lambda_system_Int:
   4.198 +  fixes f:: "'a set \<Rightarrow> real"
   4.199 +  assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
   4.200 +  shows "x \<inter> y \<in> lambda_system M f"
   4.201 +  proof -
   4.202 +    from xl yl show ?thesis
   4.203 +      proof (auto simp add: positive_def lambda_system_eq Int)
   4.204 +	fix u
   4.205 +	assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M"
   4.206 +           and fx: "\<forall>z\<in>sets M. f (z \<inter> x) + f (z - x) = f z"
   4.207 +           and fy: "\<forall>z\<in>sets M. f (z \<inter> y) + f (z - y) = f z"
   4.208 +	have "u - x \<inter> y \<in> sets M"
   4.209 +	  by (metis Diff Diff_Int Un u x y)
   4.210 +	moreover
   4.211 +	have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
   4.212 +	moreover
   4.213 +	have "u - x \<inter> y - y = u - y" by blast
   4.214 +	ultimately
   4.215 +	have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
   4.216 +	  by force
   4.217 +	have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) 
   4.218 +              = (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)"
   4.219 +	  by (simp add: ey) 
   4.220 +	also have "... =  (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
   4.221 +	  by (simp add: Int_ac) 
   4.222 +	also have "... = f (u \<inter> y) + f (u - y)"
   4.223 +	  using fx [THEN bspec, of "u \<inter> y"] Int y u
   4.224 +	  by force
   4.225 +	also have "... = f u"
   4.226 +	  by (metis fy u) 
   4.227 +	finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
   4.228 +      qed
   4.229 +  qed
   4.230 +
   4.231 +
   4.232 +lemma (in algebra) lambda_system_Un:
   4.233 +  fixes f:: "'a set \<Rightarrow> real"
   4.234 +  assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
   4.235 +  shows "x \<union> y \<in> lambda_system M f"
   4.236 +proof -
   4.237 +  have "(space M - x) \<inter> (space M - y) \<in> sets M"
   4.238 +    by (metis Diff_Un Un compl_sets lambda_system_sets xl yl) 
   4.239 +  moreover
   4.240 +  have "x \<union> y = space M - ((space M - x) \<inter> (space M - y))"
   4.241 +    by auto  (metis subsetD lambda_system_sets sets_into_space xl yl)+
   4.242 +  ultimately show ?thesis
   4.243 +    by (metis lambda_system_Compl lambda_system_Int xl yl) 
   4.244 +qed
   4.245 +
   4.246 +lemma (in algebra) lambda_system_algebra:
   4.247 +    "positive M f \<Longrightarrow> algebra (M (|sets := lambda_system M f|))"
   4.248 +  apply (auto simp add: algebra_def) 
   4.249 +  apply (metis lambda_system_sets set_mp sets_into_space)
   4.250 +  apply (metis lambda_system_empty)
   4.251 +  apply (metis lambda_system_Compl)
   4.252 +  apply (metis lambda_system_Un) 
   4.253 +  done
   4.254 +
   4.255 +lemma (in algebra) lambda_system_strong_additive:
   4.256 +  assumes z: "z \<in> sets M" and disj: "x \<inter> y = {}"
   4.257 +      and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
   4.258 +  shows "f (z \<inter> (x \<union> y)) = f (z \<inter> x) + f (z \<inter> y)"
   4.259 +  proof -
   4.260 +    have "z \<inter> x = (z \<inter> (x \<union> y)) \<inter> x" using disj by blast
   4.261 +    moreover
   4.262 +    have "z \<inter> y = (z \<inter> (x \<union> y)) - x" using disj by blast
   4.263 +    moreover 
   4.264 +    have "(z \<inter> (x \<union> y)) \<in> sets M"
   4.265 +      by (metis Int Un lambda_system_sets xl yl z) 
   4.266 +    ultimately show ?thesis using xl yl
   4.267 +      by (simp add: lambda_system_eq)
   4.268 +  qed
   4.269 +
   4.270 +lemma (in algebra) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x"
   4.271 +  by (metis Int_absorb1 sets_into_space)
   4.272 +
   4.273 +lemma (in algebra) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x"
   4.274 +  by (metis Int_absorb2 sets_into_space)
   4.275 +
   4.276 +lemma (in algebra) lambda_system_additive:
   4.277 +     "additive (M (|sets := lambda_system M f|)) f"
   4.278 +  proof (auto simp add: additive_def)
   4.279 +    fix x and y
   4.280 +    assume disj: "x \<inter> y = {}"
   4.281 +       and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
   4.282 +    hence  "x \<in> sets M" "y \<in> sets M" by (blast intro: lambda_system_sets)+
   4.283 +    thus "f (x \<union> y) = f x + f y" 
   4.284 +      using lambda_system_strong_additive [OF top disj xl yl]
   4.285 +      by (simp add: Un)
   4.286 +  qed
   4.287 +
   4.288 +
   4.289 +lemma (in algebra) countably_subadditive_subadditive:
   4.290 +  assumes f: "positive M f" and cs: "countably_subadditive M f"
   4.291 +  shows  "subadditive M f"
   4.292 +proof (auto simp add: subadditive_def) 
   4.293 +  fix x y
   4.294 +  assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
   4.295 +  hence "disjoint_family (binaryset x y)"
   4.296 +    by (auto simp add: disjoint_family_def binaryset_def) 
   4.297 +  hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow> 
   4.298 +         (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow> 
   4.299 +         summable (f o (binaryset x y)) \<longrightarrow>
   4.300 +         f (\<Union>i. binaryset x y i) \<le> suminf (\<lambda>n. f (binaryset x y n))"
   4.301 +    using cs by (simp add: countably_subadditive_def) 
   4.302 +  hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow> 
   4.303 +         summable (f o (binaryset x y)) \<longrightarrow>
   4.304 +         f (x \<union> y) \<le> suminf (\<lambda>n. f (binaryset x y n))"
   4.305 +    by (simp add: range_binaryset_eq UN_binaryset_eq)
   4.306 +  thus "f (x \<union> y) \<le>  f x + f y" using f x y binaryset_sums
   4.307 +    by (auto simp add: Un sums_iff positive_def o_def) 
   4.308 +qed 
   4.309 +
   4.310 +
   4.311 +definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set "
   4.312 +  where "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
   4.313 +
   4.314 +lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
   4.315 +proof (induct n)
   4.316 +  case 0 show ?case by simp
   4.317 +next
   4.318 +  case (Suc n)
   4.319 +  thus ?case by (simp add: atLeastLessThanSuc disjointed_def) 
   4.320 +qed
   4.321 +
   4.322 +lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
   4.323 +  apply (rule UN_finite2_eq [where k=0]) 
   4.324 +  apply (simp add: finite_UN_disjointed_eq) 
   4.325 +  done
   4.326 +
   4.327 +lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
   4.328 +  by (auto simp add: disjointed_def)
   4.329 +
   4.330 +lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
   4.331 +  by (simp add: disjoint_family_def) 
   4.332 +     (metis neq_iff Int_commute less_disjoint_disjointed)
   4.333 +
   4.334 +lemma disjointed_subset: "disjointed A n \<subseteq> A n"
   4.335 +  by (auto simp add: disjointed_def)
   4.336 +
   4.337 +
   4.338 +lemma (in algebra) UNION_in_sets:
   4.339 +  fixes A:: "nat \<Rightarrow> 'a set"
   4.340 +  assumes A: "range A \<subseteq> sets M "
   4.341 +  shows  "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
   4.342 +proof (induct n)
   4.343 +  case 0 show ?case by simp
   4.344 +next
   4.345 +  case (Suc n) 
   4.346 +  thus ?case
   4.347 +    by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff)
   4.348 +qed
   4.349 +
   4.350 +lemma (in algebra) range_disjointed_sets:
   4.351 +  assumes A: "range A \<subseteq> sets M "
   4.352 +  shows  "range (disjointed A) \<subseteq> sets M"
   4.353 +proof (auto simp add: disjointed_def) 
   4.354 +  fix n
   4.355 +  show "A n - (\<Union>i\<in>{0..<n}. A i) \<in> sets M" using UNION_in_sets
   4.356 +    by (metis A Diff UNIV_I disjointed_def image_subset_iff)
   4.357 +qed
   4.358 +
   4.359 +lemma sigma_algebra_disjoint_iff: 
   4.360 +     "sigma_algebra M \<longleftrightarrow> 
   4.361 +      algebra M &
   4.362 +      (\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow> 
   4.363 +           (\<Union>i::nat. A i) \<in> sets M)"
   4.364 +proof (auto simp add: sigma_algebra_iff)
   4.365 +  fix A :: "nat \<Rightarrow> 'a set"
   4.366 +  assume M: "algebra M"
   4.367 +     and A: "range A \<subseteq> sets M"
   4.368 +     and UnA: "\<forall>A. range A \<subseteq> sets M \<longrightarrow>
   4.369 +               disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
   4.370 +  hence "range (disjointed A) \<subseteq> sets M \<longrightarrow>
   4.371 +         disjoint_family (disjointed A) \<longrightarrow>
   4.372 +         (\<Union>i. disjointed A i) \<in> sets M" by blast
   4.373 +  hence "(\<Union>i. disjointed A i) \<in> sets M"
   4.374 +    by (simp add: algebra.range_disjointed_sets M A disjoint_family_disjointed) 
   4.375 +  thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq)
   4.376 +qed
   4.377 +
   4.378 +
   4.379 +lemma (in algebra) additive_sum:
   4.380 +  fixes A:: "nat \<Rightarrow> 'a set"
   4.381 +  assumes f: "positive M f" and ad: "additive M f"
   4.382 +      and A: "range A \<subseteq> sets M"
   4.383 +      and disj: "disjoint_family A"
   4.384 +  shows  "setsum (f o A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)"
   4.385 +proof (induct n)
   4.386 +  case 0 show ?case using f by (simp add: positive_def) 
   4.387 +next
   4.388 +  case (Suc n) 
   4.389 +  have "A n \<inter> (\<Union>i\<in>{0..<n}. A i) = {}" using disj 
   4.390 +    by (auto simp add: disjoint_family_def neq_iff) blast
   4.391 +  moreover 
   4.392 +  have "A n \<in> sets M" using A by blast 
   4.393 +  moreover have "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
   4.394 +    by (metis A UNION_in_sets atLeast0LessThan)
   4.395 +  moreover 
   4.396 +  ultimately have "f (A n \<union> (\<Union>i\<in>{0..<n}. A i)) = f (A n) + f(\<Union>i\<in>{0..<n}. A i)"
   4.397 +    using ad UNION_in_sets A by (auto simp add: additive_def) 
   4.398 +  with Suc.hyps show ?case using ad
   4.399 +    by (auto simp add: atLeastLessThanSuc additive_def) 
   4.400 +qed
   4.401 +
   4.402 +
   4.403 +lemma countably_subadditiveD:
   4.404 +  "countably_subadditive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow>
   4.405 +   (\<Union>i. A i) \<in> sets M \<Longrightarrow> summable (f o A) \<Longrightarrow> f (\<Union>i. A i) \<le> suminf (f o A)" 
   4.406 +  by (auto simp add: countably_subadditive_def o_def)
   4.407 +
   4.408 +lemma (in algebra) increasing_additive_summable:
   4.409 +  fixes A:: "nat \<Rightarrow> 'a set"
   4.410 +  assumes f: "positive M f" and ad: "additive M f"
   4.411 +      and inc: "increasing M f"
   4.412 +      and A: "range A \<subseteq> sets M"
   4.413 +      and disj: "disjoint_family A"
   4.414 +  shows  "summable (f o A)"
   4.415 +proof (rule pos_summable) 
   4.416 +  fix n
   4.417 +  show "0 \<le> (f \<circ> A) n" using f A
   4.418 +    by (force simp add: positive_def)
   4.419 +  next
   4.420 +  fix n
   4.421 +  have "setsum (f \<circ> A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)"
   4.422 +    by (rule additive_sum [OF f ad A disj]) 
   4.423 +  also have "... \<le> f (space M)" using space_closed A
   4.424 +    by (blast intro: increasingD [OF inc] UNION_in_sets top) 
   4.425 +  finally show "setsum (f \<circ> A) {0..<n} \<le> f (space M)" .
   4.426 +qed
   4.427 +
   4.428 +lemma lambda_system_positive:
   4.429 +     "positive M f \<Longrightarrow> positive (M (|sets := lambda_system M f|)) f"
   4.430 +  by (simp add: positive_def lambda_system_def) 
   4.431 +
   4.432 +lemma lambda_system_increasing:
   4.433 +   "increasing M f \<Longrightarrow> increasing (M (|sets := lambda_system M f|)) f"
   4.434 +  by (simp add: increasing_def lambda_system_def) 
   4.435 +
   4.436 +lemma (in algebra) lambda_system_strong_sum:
   4.437 +  fixes A:: "nat \<Rightarrow> 'a set"
   4.438 +  assumes f: "positive M f" and a: "a \<in> sets M"
   4.439 +      and A: "range A \<subseteq> lambda_system M f"
   4.440 +      and disj: "disjoint_family A"
   4.441 +  shows  "(\<Sum>i = 0..<n. f (a \<inter>A i)) = f (a \<inter> (\<Union>i\<in>{0..<n}. A i))"
   4.442 +proof (induct n)
   4.443 +  case 0 show ?case using f by (simp add: positive_def) 
   4.444 +next
   4.445 +  case (Suc n) 
   4.446 +  have 2: "A n \<inter> UNION {0..<n} A = {}" using disj
   4.447 +    by (force simp add: disjoint_family_def neq_iff) 
   4.448 +  have 3: "A n \<in> lambda_system M f" using A
   4.449 +    by blast
   4.450 +  have 4: "UNION {0..<n} A \<in> lambda_system M f"
   4.451 +    using A algebra.UNION_in_sets [OF local.lambda_system_algebra [OF f]] 
   4.452 +    by simp
   4.453 +  from Suc.hyps show ?case
   4.454 +    by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4])
   4.455 +qed
   4.456 +
   4.457 +
   4.458 +lemma (in sigma_algebra) lambda_system_caratheodory:
   4.459 +  assumes oms: "outer_measure_space M f"
   4.460 +      and A: "range A \<subseteq> lambda_system M f"
   4.461 +      and disj: "disjoint_family A"
   4.462 +  shows  "(\<Union>i. A i) \<in> lambda_system M f & (f \<circ> A)  sums  f (\<Union>i. A i)"
   4.463 +proof -
   4.464 +  have pos: "positive M f" and inc: "increasing M f" 
   4.465 +   and csa: "countably_subadditive M f" 
   4.466 +    by (metis oms outer_measure_space_def)+
   4.467 +  have sa: "subadditive M f"
   4.468 +    by (metis countably_subadditive_subadditive csa pos) 
   4.469 +  have A': "range A \<subseteq> sets (M(|sets := lambda_system M f|))" using A 
   4.470 +    by simp
   4.471 +  have alg_ls: "algebra (M(|sets := lambda_system M f|))"
   4.472 +    by (rule lambda_system_algebra [OF pos]) 
   4.473 +  have A'': "range A \<subseteq> sets M"
   4.474 +     by (metis A image_subset_iff lambda_system_sets)
   4.475 +  have sumfA: "summable (f \<circ> A)" 
   4.476 +    by (metis algebra.increasing_additive_summable [OF alg_ls]
   4.477 +          lambda_system_positive lambda_system_additive lambda_system_increasing
   4.478 +          A' oms outer_measure_space_def disj)
   4.479 +  have U_in: "(\<Union>i. A i) \<in> sets M"
   4.480 +    by (metis A countable_UN image_subset_iff lambda_system_sets)
   4.481 +  have U_eq: "f (\<Union>i. A i) = suminf (f o A)" 
   4.482 +    proof (rule antisym)
   4.483 +      show "f (\<Union>i. A i) \<le> suminf (f \<circ> A)"
   4.484 +	by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA]) 
   4.485 +      show "suminf (f \<circ> A) \<le> f (\<Union>i. A i)"
   4.486 +	by (rule suminf_le [OF sumfA]) 
   4.487 +           (metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right
   4.488 +	          lambda_system_positive lambda_system_additive 
   4.489 +                  subset_Un_eq increasingD [OF inc] A' A'' UNION_in_sets U_in) 
   4.490 +    qed
   4.491 +  {
   4.492 +    fix a 
   4.493 +    assume a [iff]: "a \<in> sets M" 
   4.494 +    have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
   4.495 +    proof -
   4.496 +      have summ: "summable (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)" using pos A'' 
   4.497 +	apply -
   4.498 +	apply (rule summable_comparison_test [OF _ sumfA]) 
   4.499 +	apply (rule_tac x="0" in exI) 
   4.500 +	apply (simp add: positive_def) 
   4.501 +	apply (auto simp add: )
   4.502 +	apply (subst abs_of_nonneg)
   4.503 +	apply (metis A'' Int UNIV_I a image_subset_iff)
   4.504 +	apply (blast intro:  increasingD [OF inc] a)   
   4.505 +	done
   4.506 +      show ?thesis
   4.507 +      proof (rule antisym)
   4.508 +	have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
   4.509 +	  by blast
   4.510 +	moreover 
   4.511 +	have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
   4.512 +	  by (auto simp add: disjoint_family_def) 
   4.513 +	moreover 
   4.514 +	have "a \<inter> (\<Union>i. A i) \<in> sets M"
   4.515 +	  by (metis Int U_in a)
   4.516 +	ultimately 
   4.517 +	have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
   4.518 +	  using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ
   4.519 +	  by (simp add: o_def) 
   4.520 +	moreover 
   4.521 +	have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)  \<le> f a - f (a - (\<Union>i. A i))"
   4.522 +	  proof (rule suminf_le [OF summ])
   4.523 +	    fix n
   4.524 +	    have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
   4.525 +	      by (metis A'' UNION_in_sets) 
   4.526 +	    have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
   4.527 +	      by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a) 
   4.528 +	    have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
   4.529 +	      using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]]
   4.530 +	      by (simp add: A) 
   4.531 +	    hence eq_fa: "f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i)) = f a"
   4.532 +	      by (simp add: lambda_system_eq UNION_in Diff_Compl a)
   4.533 +	    have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
   4.534 +	      by (blast intro: increasingD [OF inc] Diff UNION_eq_Union_image 
   4.535 +                               UNION_in U_in a) 
   4.536 +	    thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>i. A i))"
   4.537 +	      using eq_fa
   4.538 +	      by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos 
   4.539 +                            a A disj)
   4.540 +	  qed
   4.541 +	ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a" 
   4.542 +	  by arith
   4.543 +      next
   4.544 +	have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))" 
   4.545 +	  by (blast intro:  increasingD [OF inc] a U_in)
   4.546 +	also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
   4.547 +	  by (blast intro: subadditiveD [OF sa] Int Diff U_in) 
   4.548 +	finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
   4.549 +        qed
   4.550 +     qed
   4.551 +  }
   4.552 +  thus  ?thesis
   4.553 +    by (simp add: lambda_system_eq sums_iff U_eq U_in sumfA)
   4.554 +qed
   4.555 +
   4.556 +lemma (in sigma_algebra) caratheodory_lemma:
   4.557 +  assumes oms: "outer_measure_space M f"
   4.558 +  shows "measure_space (|space = space M, sets = lambda_system M f, measure = f|)"
   4.559 +proof -
   4.560 +  have pos: "positive M f" 
   4.561 +    by (metis oms outer_measure_space_def)
   4.562 +  have alg: "algebra (|space = space M, sets = lambda_system M f, measure = f|)"
   4.563 +    using lambda_system_algebra [OF pos]
   4.564 +    by (simp add: algebra_def) 
   4.565 +  then moreover 
   4.566 +  have "sigma_algebra (|space = space M, sets = lambda_system M f, measure = f|)"
   4.567 +    using lambda_system_caratheodory [OF oms]
   4.568 +    by (simp add: sigma_algebra_disjoint_iff) 
   4.569 +  moreover 
   4.570 +  have "measure_space_axioms (|space = space M, sets = lambda_system M f, measure = f|)" 
   4.571 +    using pos lambda_system_caratheodory [OF oms]
   4.572 +    by (simp add: measure_space_axioms_def positive_def lambda_system_sets 
   4.573 +                  countably_additive_def o_def) 
   4.574 +  ultimately 
   4.575 +  show ?thesis
   4.576 +    by intro_locales (auto simp add: sigma_algebra_def) 
   4.577 +qed
   4.578 +
   4.579 +
   4.580 +lemma (in algebra) inf_measure_nonempty:
   4.581 +  assumes f: "positive M f" and b: "b \<in> sets M" and a: "a \<subseteq> b"
   4.582 +  shows "f b \<in> measure_set M f a"
   4.583 +proof -
   4.584 +  have "(f \<circ> (\<lambda>i. {})(0 := b)) sums setsum (f \<circ> (\<lambda>i. {})(0 := b)) {0..<1::nat}"
   4.585 +    by (rule series_zero)  (simp add: positive_imp_0 [OF f]) 
   4.586 +  also have "... = f b" 
   4.587 +    by simp
   4.588 +  finally have "(f \<circ> (\<lambda>i. {})(0 := b)) sums f b" .
   4.589 +  thus ?thesis using a
   4.590 +    by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"] 
   4.591 +             simp add: measure_set_def disjoint_family_def b split_if_mem2) 
   4.592 +qed  
   4.593 +
   4.594 +lemma (in algebra) inf_measure_pos0:
   4.595 +     "positive M f \<Longrightarrow> x \<in> measure_set M f a \<Longrightarrow> 0 \<le> x"
   4.596 +apply (auto simp add: positive_def measure_set_def sums_iff intro!: suminf_ge_zero)
   4.597 +apply blast
   4.598 +done
   4.599 +
   4.600 +lemma (in algebra) inf_measure_pos:
   4.601 +  shows "positive M f \<Longrightarrow> x \<subseteq> space M \<Longrightarrow> 0 \<le> Inf (measure_set M f x)"
   4.602 +apply (rule Inf_greatest)
   4.603 +apply (metis emptyE inf_measure_nonempty top)
   4.604 +apply (metis inf_measure_pos0) 
   4.605 +done
   4.606 +
   4.607 +lemma (in algebra) additive_increasing:
   4.608 +  assumes posf: "positive M f" and addf: "additive M f" 
   4.609 +  shows "increasing M f"
   4.610 +proof (auto simp add: increasing_def) 
   4.611 +  fix x y
   4.612 +  assume xy: "x \<in> sets M" "y \<in> sets M" "x \<subseteq> y"
   4.613 +  have "f x \<le> f x + f (y-x)" using posf
   4.614 +    by (simp add: positive_def) (metis Diff xy)
   4.615 +  also have "... = f (x \<union> (y-x))" using addf
   4.616 +    by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy) 
   4.617 +  also have "... = f y"
   4.618 +    by (metis Un_Diff_cancel Un_absorb1 xy)
   4.619 +  finally show "f x \<le> f y" .
   4.620 +qed
   4.621 +
   4.622 +lemma (in algebra) countably_additive_additive:
   4.623 +  assumes posf: "positive M f" and ca: "countably_additive M f" 
   4.624 +  shows "additive M f"
   4.625 +proof (auto simp add: additive_def) 
   4.626 +  fix x y
   4.627 +  assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
   4.628 +  hence "disjoint_family (binaryset x y)"
   4.629 +    by (auto simp add: disjoint_family_def binaryset_def) 
   4.630 +  hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow> 
   4.631 +         (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow> 
   4.632 +         f (\<Union>i. binaryset x y i) = suminf (\<lambda>n. f (binaryset x y n))"
   4.633 +    using ca
   4.634 +    by (simp add: countably_additive_def) (metis UN_binaryset_eq sums_unique) 
   4.635 +  hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow> 
   4.636 +         f (x \<union> y) = suminf (\<lambda>n. f (binaryset x y n))"
   4.637 +    by (simp add: range_binaryset_eq UN_binaryset_eq)
   4.638 +  thus "f (x \<union> y) = f x + f y" using posf x y
   4.639 +    by (simp add: Un suminf_binaryset_eq positive_def)
   4.640 +qed 
   4.641 + 
   4.642 +lemma (in algebra) inf_measure_agrees:
   4.643 +  assumes posf: "positive M f" and ca: "countably_additive M f" 
   4.644 +      and s: "s \<in> sets M"  
   4.645 +  shows "Inf (measure_set M f s) = f s"
   4.646 +proof (rule Inf_eq) 
   4.647 +  fix z
   4.648 +  assume z: "z \<in> measure_set M f s"
   4.649 +  from this obtain A where 
   4.650 +    A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
   4.651 +    and "s \<subseteq> (\<Union>x. A x)" and sm: "summable (f \<circ> A)"
   4.652 +    and si: "suminf (f \<circ> A) = z"
   4.653 +    by (auto simp add: measure_set_def sums_iff) 
   4.654 +  hence seq: "s = (\<Union>i. A i \<inter> s)" by blast
   4.655 +  have inc: "increasing M f"
   4.656 +    by (metis additive_increasing ca countably_additive_additive posf)
   4.657 +  have sums: "(\<lambda>i. f (A i \<inter> s)) sums f (\<Union>i. A i \<inter> s)"
   4.658 +    proof (rule countably_additiveD [OF ca]) 
   4.659 +      show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s
   4.660 +	by blast
   4.661 +      show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
   4.662 +	by (auto simp add: disjoint_family_def)
   4.663 +      show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s
   4.664 +	by (metis UN_extend_simps(4) s seq)
   4.665 +    qed
   4.666 +  hence "f s = suminf (\<lambda>i. f (A i \<inter> s))"
   4.667 +    by (metis Int_commute UN_simps(4) seq sums_iff) 
   4.668 +  also have "... \<le> suminf (f \<circ> A)" 
   4.669 +    proof (rule summable_le [OF _ _ sm]) 
   4.670 +      show "\<forall>n. f (A n \<inter> s) \<le> (f \<circ> A) n" using A s
   4.671 +	by (force intro: increasingD [OF inc]) 
   4.672 +      show "summable (\<lambda>i. f (A i \<inter> s))" using sums
   4.673 +	by (simp add: sums_iff) 
   4.674 +    qed
   4.675 +  also have "... = z" by (rule si) 
   4.676 +  finally show "f s \<le> z" .
   4.677 +next
   4.678 +  fix y
   4.679 +  assume y: "!!u. u \<in> measure_set M f s \<Longrightarrow> y \<le> u"
   4.680 +  thus "y \<le> f s"
   4.681 +    by (blast intro: inf_measure_nonempty [OF posf s subset_refl])
   4.682 +qed
   4.683 +
   4.684 +lemma (in algebra) inf_measure_empty:
   4.685 +  assumes posf: "positive M f"
   4.686 +  shows "Inf (measure_set M f {}) = 0"
   4.687 +proof (rule antisym)
   4.688 +  show "0 \<le> Inf (measure_set M f {})"
   4.689 +    by (metis empty_subsetI inf_measure_pos posf) 
   4.690 +  show "Inf (measure_set M f {}) \<le> 0"
   4.691 +    by (metis Inf_lower empty_sets inf_measure_pos0 inf_measure_nonempty posf
   4.692 +              positive_imp_0 subset_refl) 
   4.693 +qed
   4.694 +
   4.695 +lemma (in algebra) inf_measure_positive:
   4.696 +  "positive M f \<Longrightarrow> 
   4.697 +   positive (| space = space M, sets = Pow (space M) |)
   4.698 +                  (\<lambda>x. Inf (measure_set M f x))"
   4.699 +  by (simp add: positive_def inf_measure_empty inf_measure_pos) 
   4.700 +
   4.701 +lemma (in algebra) inf_measure_increasing:
   4.702 +  assumes posf: "positive M f"
   4.703 +  shows "increasing (| space = space M, sets = Pow (space M) |)
   4.704 +                    (\<lambda>x. Inf (measure_set M f x))"
   4.705 +apply (auto simp add: increasing_def) 
   4.706 +apply (rule Inf_greatest, metis emptyE inf_measure_nonempty top posf)
   4.707 +apply (rule Inf_lower) 
   4.708 +apply (clarsimp simp add: measure_set_def, blast) 
   4.709 +apply (blast intro: inf_measure_pos0 posf)
   4.710 +done
   4.711 +
   4.712 +
   4.713 +lemma (in algebra) inf_measure_le:
   4.714 +  assumes posf: "positive M f" and inc: "increasing M f" 
   4.715 +      and x: "x \<in> {r . \<exists>A. range A \<subseteq> sets M & s \<subseteq> (\<Union>i. A i) & (f \<circ> A) sums r}"
   4.716 +  shows "Inf (measure_set M f s) \<le> x"
   4.717 +proof -
   4.718 +  from x
   4.719 +  obtain A where A: "range A \<subseteq> sets M" and ss: "s \<subseteq> (\<Union>i. A i)" 
   4.720 +             and sm: "summable (f \<circ> A)" and xeq: "suminf (f \<circ> A) = x"
   4.721 +    by (auto simp add: sums_iff)
   4.722 +  have dA: "range (disjointed A) \<subseteq> sets M"
   4.723 +    by (metis A range_disjointed_sets)
   4.724 +  have "\<forall>n. \<bar>(f o disjointed A) n\<bar> \<le> (f \<circ> A) n"
   4.725 +    proof (auto)
   4.726 +      fix n
   4.727 +      have "\<bar>f (disjointed A n)\<bar> = f (disjointed A n)" using posf dA
   4.728 +	by (auto simp add: positive_def image_subset_iff)
   4.729 +      also have "... \<le> f (A n)" 
   4.730 +	by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
   4.731 +      finally show "\<bar>f (disjointed A n)\<bar> \<le> f (A n)" .
   4.732 +    qed
   4.733 +  from Series.summable_le2 [OF this sm]
   4.734 +  have sda:  "summable (f o disjointed A)"  
   4.735 +             "suminf (f o disjointed A) \<le> suminf (f \<circ> A)"
   4.736 +    by blast+
   4.737 +  hence ley: "suminf (f o disjointed A) \<le> x"
   4.738 +    by (metis xeq) 
   4.739 +  from sda have "(f \<circ> disjointed A) sums suminf (f \<circ> disjointed A)"
   4.740 +    by (simp add: sums_iff) 
   4.741 +  hence y: "suminf (f o disjointed A) \<in> measure_set M f s"
   4.742 +    apply (auto simp add: measure_set_def)
   4.743 +    apply (rule_tac x="disjointed A" in exI) 
   4.744 +    apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA)
   4.745 +    done
   4.746 +  show ?thesis
   4.747 +    by (blast intro: Inf_lower y order_trans [OF _ ley] inf_measure_pos0 posf)
   4.748 +qed
   4.749 +
   4.750 +lemma (in algebra) inf_measure_close:
   4.751 +  assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (space M)"
   4.752 +  shows "\<exists>A l. range A \<subseteq> sets M & disjoint_family A & s \<subseteq> (\<Union>i. A i) & 
   4.753 +               (f \<circ> A) sums l & l \<le> Inf (measure_set M f s) + e"
   4.754 +proof -
   4.755 +  have " measure_set M f s \<noteq> {}" 
   4.756 +    by (metis emptyE ss inf_measure_nonempty [OF posf top])
   4.757 +  hence "\<exists>l \<in> measure_set M f s. l < Inf (measure_set M f s) + e" 
   4.758 +    by (rule Inf_close [OF _ e])
   4.759 +  thus ?thesis 
   4.760 +    by (auto simp add: measure_set_def, rule_tac x=" A" in exI, auto)
   4.761 +qed
   4.762 +
   4.763 +lemma (in algebra) inf_measure_countably_subadditive:
   4.764 +  assumes posf: "positive M f" and inc: "increasing M f" 
   4.765 +  shows "countably_subadditive (| space = space M, sets = Pow (space M) |)
   4.766 +                  (\<lambda>x. Inf (measure_set M f x))"
   4.767 +proof (auto simp add: countably_subadditive_def o_def, rule field_le_epsilon)
   4.768 +  fix A :: "nat \<Rightarrow> 'a set" and e :: real
   4.769 +    assume A: "range A \<subseteq> Pow (space M)"
   4.770 +       and disj: "disjoint_family A"
   4.771 +       and sb: "(\<Union>i. A i) \<subseteq> space M"
   4.772 +       and sum1: "summable (\<lambda>n. Inf (measure_set M f (A n)))"
   4.773 +       and e: "0 < e"
   4.774 +    have "!!n. \<exists>B l. range B \<subseteq> sets M \<and> disjoint_family B \<and> A n \<subseteq> (\<Union>i. B i) \<and>
   4.775 +                    (f o B) sums l \<and>
   4.776 +                    l \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
   4.777 +      apply (rule inf_measure_close [OF posf])
   4.778 +      apply (metis e half mult_pos_pos zero_less_power) 
   4.779 +      apply (metis UNIV_I UN_subset_iff sb)
   4.780 +      done
   4.781 +    hence "\<exists>BB ll. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
   4.782 +                       A n \<subseteq> (\<Union>i. BB n i) \<and> (f o BB n) sums ll n \<and>
   4.783 +                       ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
   4.784 +      by (rule choice2)
   4.785 +    then obtain BB ll
   4.786 +      where BB: "!!n. (range (BB n) \<subseteq> sets M)"
   4.787 +        and disjBB: "!!n. disjoint_family (BB n)" 
   4.788 +        and sbBB: "!!n. A n \<subseteq> (\<Union>i. BB n i)"
   4.789 +        and BBsums: "!!n. (f o BB n) sums ll n"
   4.790 +        and ll: "!!n. ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
   4.791 +      by auto blast
   4.792 +    have llpos: "!!n. 0 \<le> ll n"
   4.793 +	by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero 
   4.794 +              range_subsetD BB) 
   4.795 +    have sll: "summable ll &
   4.796 +               suminf ll \<le> suminf (\<lambda>n. Inf (measure_set M f (A n))) + e"
   4.797 +      proof -
   4.798 +	have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)"
   4.799 +	  by (rule sums_mult [OF power_half_series]) 
   4.800 +	hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)"
   4.801 +	  and eqe:  "(\<Sum>n. e * (1 / 2) ^ n / 2) = e"
   4.802 +	  by (auto simp add: sums_iff) 
   4.803 +	have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) +
   4.804 +                 suminf (\<lambda>n. e * (1/2)^(Suc n)) =
   4.805 +                 suminf (\<lambda>n. Inf (measure_set M f (A n)) + e * (1/2)^(Suc n))"
   4.806 +	  by (rule suminf_add [OF sum1 sum0]) 
   4.807 +	have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n"
   4.808 +	  by (metis ll llpos abs_of_nonneg)
   4.809 +	have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))"
   4.810 +	  by (rule summable_add [OF sum1 sum0]) 
   4.811 +	have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)"
   4.812 +	  using Series.summable_le2 [OF 1 2] by auto
   4.813 +	also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + 
   4.814 +                         (\<Sum>n. e * (1 / 2) ^ Suc n)"
   4.815 +	  by (metis 0) 
   4.816 +	also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + e"
   4.817 +	  by (simp add: eqe) 
   4.818 +	finally show ?thesis using  Series.summable_le2 [OF 1 2] by auto
   4.819 +      qed
   4.820 +    def C \<equiv> "(split BB) o nat_to_nat2"
   4.821 +    have C: "!!n. C n \<in> sets M"
   4.822 +      apply (rule_tac p="nat_to_nat2 n" in PairE)
   4.823 +      apply (simp add: C_def)
   4.824 +      apply (metis BB subsetD rangeI)  
   4.825 +      done
   4.826 +    have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
   4.827 +      proof (auto simp add: C_def)
   4.828 +	fix x i
   4.829 +	assume x: "x \<in> A i"
   4.830 +	with sbBB [of i] obtain j where "x \<in> BB i j"
   4.831 +	  by blast	  
   4.832 +	thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
   4.833 +	  by (metis nat_to_nat2_surj internal_split_def prod.cases 
   4.834 +                prod_case_split surj_f_inv_f)
   4.835 +      qed 
   4.836 +    have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> nat_to_nat2"
   4.837 +      by (rule ext)  (auto simp add: C_def) 
   4.838 +    also have "... sums suminf ll" 
   4.839 +      proof (rule suminf_2dimen)
   4.840 +	show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB 
   4.841 +	  by (force simp add: positive_def)
   4.842 +	show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB
   4.843 +	  by (force simp add: o_def)
   4.844 +	show "summable ll" using sll
   4.845 +	  by auto
   4.846 +      qed
   4.847 +    finally have Csums: "(f \<circ> C) sums suminf ll" .
   4.848 +    have "Inf (measure_set M f (\<Union>i. A i)) \<le> suminf ll"
   4.849 +      apply (rule inf_measure_le [OF posf inc], auto)
   4.850 +      apply (rule_tac x="C" in exI)
   4.851 +      apply (auto simp add: C sbC Csums) 
   4.852 +      done
   4.853 +    also have "... \<le> (\<Sum>n. Inf (measure_set M f (A n))) + e" using sll
   4.854 +      by blast
   4.855 +    finally show "Inf (measure_set M f (\<Union>i. A i)) \<le> 
   4.856 +          (\<Sum>n. Inf (measure_set M f (A n))) + e" .
   4.857 +qed
   4.858 +
   4.859 +lemma (in algebra) inf_measure_outer:
   4.860 +  "positive M f \<Longrightarrow> increasing M f 
   4.861 +   \<Longrightarrow> outer_measure_space (| space = space M, sets = Pow (space M) |)
   4.862 +                          (\<lambda>x. Inf (measure_set M f x))"
   4.863 +  by (simp add: outer_measure_space_def inf_measure_positive
   4.864 +                inf_measure_increasing inf_measure_countably_subadditive) 
   4.865 +
   4.866 +(*MOVE UP*)
   4.867 +
   4.868 +lemma (in algebra) algebra_subset_lambda_system:
   4.869 +  assumes posf: "positive M f" and inc: "increasing M f" 
   4.870 +      and add: "additive M f"
   4.871 +  shows "sets M \<subseteq> lambda_system (| space = space M, sets = Pow (space M) |)
   4.872 +                                (\<lambda>x. Inf (measure_set M f x))"
   4.873 +proof (auto dest: sets_into_space 
   4.874 +            simp add: algebra.lambda_system_eq [OF algebra_Pow]) 
   4.875 +  fix x s
   4.876 +  assume x: "x \<in> sets M"
   4.877 +     and s: "s \<subseteq> space M"
   4.878 +  have [simp]: "!!x. x \<in> sets M \<Longrightarrow> s \<inter> (space M - x) = s-x" using s 
   4.879 +    by blast
   4.880 +  have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   4.881 +        \<le> Inf (measure_set M f s)"
   4.882 +    proof (rule field_le_epsilon) 
   4.883 +      fix e :: real
   4.884 +      assume e: "0 < e"
   4.885 +      from inf_measure_close [OF posf e s]
   4.886 +      obtain A l where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
   4.887 +                   and sUN: "s \<subseteq> (\<Union>i. A i)" and fsums: "(f \<circ> A) sums l"
   4.888 +	           and l: "l \<le> Inf (measure_set M f s) + e"
   4.889 +	by auto
   4.890 +      have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
   4.891 +                      (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
   4.892 +	by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
   4.893 +      have  [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)"
   4.894 +	by (subst additiveD [OF add, symmetric])
   4.895 + 	   (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
   4.896 +      have fsumb: "summable (f \<circ> A)"
   4.897 +	by (metis fsums sums_iff) 
   4.898 +      { fix u
   4.899 +	assume u: "u \<in> sets M"
   4.900 +	have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> f (A n)"
   4.901 +	  by (simp add: positive_imp_pos [OF posf]  increasingD [OF inc] 
   4.902 +                        u Int  range_subsetD [OF A]) 
   4.903 +	have 1: "summable (f o (\<lambda>z. z\<inter>u) o A)" 
   4.904 +          by (rule summable_comparison_test [OF _ fsumb]) simp
   4.905 +	have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)"
   4.906 +          proof (rule Inf_lower) 
   4.907 +            show "suminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)"
   4.908 +              apply (simp add: measure_set_def) 
   4.909 +              apply (rule_tac x="(\<lambda>z. z \<inter> u) o A" in exI) 
   4.910 +              apply (auto simp add: disjoint_family_subset [OF disj])
   4.911 +              apply (blast intro: u range_subsetD [OF A]) 
   4.912 +              apply (blast dest: subsetD [OF sUN])
   4.913 +              apply (metis 1 o_assoc sums_iff) 
   4.914 +              done
   4.915 +          next
   4.916 +            show "\<And>x. x \<in> measure_set M f (s \<inter> u) \<Longrightarrow> 0 \<le> x"
   4.917 +              by (blast intro: inf_measure_pos0 [OF posf]) 
   4.918 +            qed
   4.919 +          note 1 2
   4.920 +      } note lesum = this
   4.921 +      have sum1: "summable (f o (\<lambda>z. z\<inter>x) o A)"
   4.922 +        and inf1: "Inf (measure_set M f (s\<inter>x)) \<le> suminf (f o (\<lambda>z. z\<inter>x) o A)"
   4.923 +        and sum2: "summable (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
   4.924 +        and inf2: "Inf (measure_set M f (s \<inter> (space M - x))) 
   4.925 +                   \<le> suminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
   4.926 +	by (metis Diff lesum top x)+
   4.927 +      hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   4.928 +           \<le> suminf (f o (\<lambda>s. s\<inter>x) o A) + suminf (f o (\<lambda>s. s-x) o A)"
   4.929 +	by (simp add: x)
   4.930 +      also have "... \<le> suminf (f o A)" using suminf_add [OF sum1 sum2] 
   4.931 +	by (simp add: x) (simp add: o_def) 
   4.932 +      also have "... \<le> Inf (measure_set M f s) + e"
   4.933 +	by (metis fsums l sums_unique) 
   4.934 +      finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   4.935 +        \<le> Inf (measure_set M f s) + e" .
   4.936 +    qed
   4.937 +  moreover 
   4.938 +  have "Inf (measure_set M f s)
   4.939 +       \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
   4.940 +    proof -
   4.941 +    have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))"
   4.942 +      by (metis Un_Diff_Int Un_commute)
   4.943 +    also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))" 
   4.944 +      apply (rule subadditiveD) 
   4.945 +      apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow 
   4.946 +	       inf_measure_positive inf_measure_countably_subadditive posf inc)
   4.947 +      apply (auto simp add: subsetD [OF s])  
   4.948 +      done
   4.949 +    finally show ?thesis .
   4.950 +    qed
   4.951 +  ultimately 
   4.952 +  show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   4.953 +        = Inf (measure_set M f s)"
   4.954 +    by (rule order_antisym)
   4.955 +qed
   4.956 +
   4.957 +lemma measure_down:
   4.958 +     "measure_space N \<Longrightarrow> sigma_algebra M \<Longrightarrow> sets M \<subseteq> sets N \<Longrightarrow>
   4.959 +      (measure M = measure N) \<Longrightarrow> measure_space M"
   4.960 +  by (simp add: measure_space_def measure_space_axioms_def positive_def 
   4.961 +                countably_additive_def) 
   4.962 +     blast
   4.963 +
   4.964 +theorem (in algebra) caratheodory:
   4.965 +  assumes posf: "positive M f" and ca: "countably_additive M f" 
   4.966 +  shows "\<exists>MS :: 'a measure_space. 
   4.967 +             (\<forall>s \<in> sets M. measure MS s = f s) \<and>
   4.968 +             ((|space = space MS, sets = sets MS|) = sigma (space M) (sets M)) \<and>
   4.969 +             measure_space MS" 
   4.970 +  proof -
   4.971 +    have inc: "increasing M f"
   4.972 +      by (metis additive_increasing ca countably_additive_additive posf) 
   4.973 +    let ?infm = "(\<lambda>x. Inf (measure_set M f x))"
   4.974 +    def ls \<equiv> "lambda_system (|space = space M, sets = Pow (space M)|) ?infm"
   4.975 +    have mls: "measure_space (|space = space M, sets = ls, measure = ?infm|)"
   4.976 +      using sigma_algebra.caratheodory_lemma
   4.977 +              [OF sigma_algebra_Pow  inf_measure_outer [OF posf inc]]
   4.978 +      by (simp add: ls_def)
   4.979 +    hence sls: "sigma_algebra (|space = space M, sets = ls, measure = ?infm|)"
   4.980 +      by (simp add: measure_space_def) 
   4.981 +    have "sets M \<subseteq> ls" 
   4.982 +      by (simp add: ls_def)
   4.983 +         (metis ca posf inc countably_additive_additive algebra_subset_lambda_system)
   4.984 +    hence sgs_sb: "sigma_sets (space M) (sets M) \<subseteq> ls" 
   4.985 +      using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"]
   4.986 +      by simp
   4.987 +    have "measure_space (|space = space M, 
   4.988 +                          sets = sigma_sets (space M) (sets M),
   4.989 +                          measure = ?infm|)"
   4.990 +      by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets) 
   4.991 +         (simp_all add: sgs_sb space_closed)
   4.992 +    thus ?thesis
   4.993 +      by (force simp add: sigma_def inf_measure_agrees [OF posf ca]) 
   4.994 +qed
   4.995 +
   4.996 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Probability/Measure.thy	Wed Oct 28 11:42:31 2009 +0000
     5.3 @@ -0,0 +1,916 @@
     5.4 +header {*Measures*}
     5.5 +
     5.6 +theory Measure
     5.7 +  imports Caratheodory FuncSet
     5.8 +begin
     5.9 +
    5.10 +text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
    5.11 +
    5.12 +definition prod_sets where
    5.13 +  "prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"
    5.14 +
    5.15 +lemma prod_setsI: "x \<in> A \<Longrightarrow> y \<in> B \<Longrightarrow> (x \<times> y) \<in> prod_sets A B"
    5.16 +  by (auto simp add: prod_sets_def) 
    5.17 +
    5.18 +definition
    5.19 +  closed_cdi  where
    5.20 +  "closed_cdi M \<longleftrightarrow>
    5.21 +   sets M \<subseteq> Pow (space M) &
    5.22 +   (\<forall>s \<in> sets M. space M - s \<in> sets M) &
    5.23 +   (\<forall>A. (range A \<subseteq> sets M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow>
    5.24 +        (\<Union>i. A i) \<in> sets M) &
    5.25 +   (\<forall>A. (range A \<subseteq> sets M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
    5.26 +
    5.27 +
    5.28 +inductive_set
    5.29 +  smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set"
    5.30 +  for M
    5.31 +  where
    5.32 +    Basic [intro]: 
    5.33 +      "a \<in> sets M \<Longrightarrow> a \<in> smallest_ccdi_sets M"
    5.34 +  | Compl [intro]:
    5.35 +      "a \<in> smallest_ccdi_sets M \<Longrightarrow> space M - a \<in> smallest_ccdi_sets M"
    5.36 +  | Inc:
    5.37 +      "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> A 0 = {} \<Longrightarrow> (\<And>n. A n \<subseteq> A (Suc n))
    5.38 +       \<Longrightarrow> (\<Union>i. A i) \<in> smallest_ccdi_sets M"
    5.39 +  | Disj:
    5.40 +      "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> disjoint_family A
    5.41 +       \<Longrightarrow> (\<Union>i::nat. A i) \<in> smallest_ccdi_sets M"
    5.42 +  monos Pow_mono
    5.43 +
    5.44 +
    5.45 +definition
    5.46 +  smallest_closed_cdi  where
    5.47 +  "smallest_closed_cdi M = (|space = space M, sets = smallest_ccdi_sets M|)"
    5.48 +
    5.49 +definition
    5.50 +  measurable  where
    5.51 +  "measurable a b = {f . sigma_algebra a & sigma_algebra b &
    5.52 +			 f \<in> (space a -> space b) &
    5.53 +			 (\<forall>y \<in> sets b. (f -` y) \<inter> (space a) \<in> sets a)}"
    5.54 +
    5.55 +definition
    5.56 +  measure_preserving  where
    5.57 +  "measure_preserving m1 m2 =
    5.58 +     measurable m1 m2 \<inter> 
    5.59 +     {f . measure_space m1 & measure_space m2 &
    5.60 +          (\<forall>y \<in> sets m2. measure m1 ((f -` y) \<inter> (space m1)) = measure m2 y)}"
    5.61 +
    5.62 +lemma space_smallest_closed_cdi [simp]:
    5.63 +     "space (smallest_closed_cdi M) = space M"
    5.64 +  by (simp add: smallest_closed_cdi_def)
    5.65 +
    5.66 +
    5.67 +lemma (in algebra) smallest_closed_cdi1: "sets M \<subseteq> sets (smallest_closed_cdi M)"
    5.68 +  by (auto simp add: smallest_closed_cdi_def) 
    5.69 +
    5.70 +lemma (in algebra) smallest_ccdi_sets:
    5.71 +     "smallest_ccdi_sets M \<subseteq> Pow (space M)"
    5.72 +  apply (rule subsetI) 
    5.73 +  apply (erule smallest_ccdi_sets.induct) 
    5.74 +  apply (auto intro: range_subsetD dest: sets_into_space)
    5.75 +  done
    5.76 +
    5.77 +lemma (in algebra) smallest_closed_cdi2: "closed_cdi (smallest_closed_cdi M)"
    5.78 +  apply (auto simp add: closed_cdi_def smallest_closed_cdi_def smallest_ccdi_sets)
    5.79 +  apply (blast intro: smallest_ccdi_sets.Inc smallest_ccdi_sets.Disj) +
    5.80 +  done
    5.81 +
    5.82 +lemma (in algebra) smallest_closed_cdi3:
    5.83 +     "sets (smallest_closed_cdi M) \<subseteq> Pow (space M)"
    5.84 +  by (simp add: smallest_closed_cdi_def smallest_ccdi_sets) 
    5.85 +
    5.86 +lemma closed_cdi_subset: "closed_cdi M \<Longrightarrow> sets M \<subseteq> Pow (space M)"
    5.87 +  by (simp add: closed_cdi_def) 
    5.88 +
    5.89 +lemma closed_cdi_Compl: "closed_cdi M \<Longrightarrow> s \<in> sets M \<Longrightarrow> space M - s \<in> sets M"
    5.90 +  by (simp add: closed_cdi_def) 
    5.91 +
    5.92 +lemma closed_cdi_Inc:
    5.93 +     "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) \<Longrightarrow>
    5.94 +        (\<Union>i. A i) \<in> sets M"
    5.95 +  by (simp add: closed_cdi_def) 
    5.96 +
    5.97 +lemma closed_cdi_Disj:
    5.98 +     "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
    5.99 +  by (simp add: closed_cdi_def) 
   5.100 +
   5.101 +lemma closed_cdi_Un:
   5.102 +  assumes cdi: "closed_cdi M" and empty: "{} \<in> sets M"
   5.103 +      and A: "A \<in> sets M" and B: "B \<in> sets M"
   5.104 +      and disj: "A \<inter> B = {}"
   5.105 +    shows "A \<union> B \<in> sets M"
   5.106 +proof -
   5.107 +  have ra: "range (binaryset A B) \<subseteq> sets M"
   5.108 +   by (simp add: range_binaryset_eq empty A B) 
   5.109 + have di:  "disjoint_family (binaryset A B)" using disj
   5.110 +   by (simp add: disjoint_family_def binaryset_def Int_commute) 
   5.111 + from closed_cdi_Disj [OF cdi ra di]
   5.112 + show ?thesis
   5.113 +   by (simp add: UN_binaryset_eq) 
   5.114 +qed
   5.115 +
   5.116 +lemma (in algebra) smallest_ccdi_sets_Un:
   5.117 +  assumes A: "A \<in> smallest_ccdi_sets M" and B: "B \<in> smallest_ccdi_sets M"
   5.118 +      and disj: "A \<inter> B = {}"
   5.119 +    shows "A \<union> B \<in> smallest_ccdi_sets M"
   5.120 +proof -
   5.121 +  have ra: "range (binaryset A B) \<in> Pow (smallest_ccdi_sets M)"
   5.122 +    by (simp add: range_binaryset_eq  A B empty_sets smallest_ccdi_sets.Basic)
   5.123 +  have di:  "disjoint_family (binaryset A B)" using disj
   5.124 +    by (simp add: disjoint_family_def binaryset_def Int_commute) 
   5.125 +  from Disj [OF ra di]
   5.126 +  show ?thesis
   5.127 +    by (simp add: UN_binaryset_eq) 
   5.128 +qed
   5.129 +
   5.130 +
   5.131 +
   5.132 +lemma (in algebra) smallest_ccdi_sets_Int1:
   5.133 +  assumes a: "a \<in> sets M"
   5.134 +  shows "b \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
   5.135 +proof (induct rule: smallest_ccdi_sets.induct)
   5.136 +  case (Basic x)
   5.137 +  thus ?case
   5.138 +    by (metis a Int smallest_ccdi_sets.Basic)
   5.139 +next
   5.140 +  case (Compl x)
   5.141 +  have "a \<inter> (space M - x) = space M - ((space M - a) \<union> (a \<inter> x))"
   5.142 +    by blast
   5.143 +  also have "... \<in> smallest_ccdi_sets M" 
   5.144 +    by (metis smallest_ccdi_sets.Compl a Compl(2) Diff_Int2 Diff_Int_distrib2
   5.145 +           Diff_disjoint Int_Diff Int_empty_right Un_commute
   5.146 +           smallest_ccdi_sets.Basic smallest_ccdi_sets.Compl
   5.147 +           smallest_ccdi_sets_Un) 
   5.148 +  finally show ?case .
   5.149 +next
   5.150 +  case (Inc A)
   5.151 +  have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
   5.152 +    by blast
   5.153 +  have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Inc
   5.154 +    by blast
   5.155 +  moreover have "(\<lambda>i. a \<inter> A i) 0 = {}"
   5.156 +    by (simp add: Inc) 
   5.157 +  moreover have "!!n. (\<lambda>i. a \<inter> A i) n \<subseteq> (\<lambda>i. a \<inter> A i) (Suc n)" using Inc
   5.158 +    by blast
   5.159 +  ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
   5.160 +    by (rule smallest_ccdi_sets.Inc) 
   5.161 +  show ?case
   5.162 +    by (metis 1 2)
   5.163 +next
   5.164 +  case (Disj A)
   5.165 +  have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
   5.166 +    by blast
   5.167 +  have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Disj
   5.168 +    by blast
   5.169 +  moreover have "disjoint_family (\<lambda>i. a \<inter> A i)" using Disj
   5.170 +    by (auto simp add: disjoint_family_def) 
   5.171 +  ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
   5.172 +    by (rule smallest_ccdi_sets.Disj) 
   5.173 +  show ?case
   5.174 +    by (metis 1 2)
   5.175 +qed
   5.176 +
   5.177 +
   5.178 +lemma (in algebra) smallest_ccdi_sets_Int:
   5.179 +  assumes b: "b \<in> smallest_ccdi_sets M"
   5.180 +  shows "a \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
   5.181 +proof (induct rule: smallest_ccdi_sets.induct)
   5.182 +  case (Basic x)
   5.183 +  thus ?case
   5.184 +    by (metis b smallest_ccdi_sets_Int1)
   5.185 +next
   5.186 +  case (Compl x)
   5.187 +  have "(space M - x) \<inter> b = space M - (x \<inter> b \<union> (space M - b))"
   5.188 +    by blast
   5.189 +  also have "... \<in> smallest_ccdi_sets M"
   5.190 +    by (metis Compl(2) Diff_disjoint Int_Diff Int_commute Int_empty_right b 
   5.191 +           smallest_ccdi_sets.Compl smallest_ccdi_sets_Un) 
   5.192 +  finally show ?case .
   5.193 +next
   5.194 +  case (Inc A)
   5.195 +  have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
   5.196 +    by blast
   5.197 +  have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Inc
   5.198 +    by blast
   5.199 +  moreover have "(\<lambda>i. A i \<inter> b) 0 = {}"
   5.200 +    by (simp add: Inc) 
   5.201 +  moreover have "!!n. (\<lambda>i. A i \<inter> b) n \<subseteq> (\<lambda>i. A i \<inter> b) (Suc n)" using Inc
   5.202 +    by blast
   5.203 +  ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
   5.204 +    by (rule smallest_ccdi_sets.Inc) 
   5.205 +  show ?case
   5.206 +    by (metis 1 2)
   5.207 +next
   5.208 +  case (Disj A)
   5.209 +  have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
   5.210 +    by blast
   5.211 +  have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Disj
   5.212 +    by blast
   5.213 +  moreover have "disjoint_family (\<lambda>i. A i \<inter> b)" using Disj
   5.214 +    by (auto simp add: disjoint_family_def) 
   5.215 +  ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
   5.216 +    by (rule smallest_ccdi_sets.Disj) 
   5.217 +  show ?case
   5.218 +    by (metis 1 2)
   5.219 +qed
   5.220 +
   5.221 +lemma (in algebra) sets_smallest_closed_cdi_Int:
   5.222 +   "a \<in> sets (smallest_closed_cdi M) \<Longrightarrow> b \<in> sets (smallest_closed_cdi M)
   5.223 +    \<Longrightarrow> a \<inter> b \<in> sets (smallest_closed_cdi M)"
   5.224 +  by (simp add: smallest_ccdi_sets_Int smallest_closed_cdi_def) 
   5.225 +
   5.226 +lemma algebra_iff_Int:
   5.227 +     "algebra M \<longleftrightarrow> 
   5.228 +       sets M \<subseteq> Pow (space M) & {} \<in> sets M & 
   5.229 +       (\<forall>a \<in> sets M. space M - a \<in> sets M) &
   5.230 +       (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
   5.231 +proof (auto simp add: algebra.Int, auto simp add: algebra_def)
   5.232 +  fix a b
   5.233 +  assume ab: "sets M \<subseteq> Pow (space M)"
   5.234 +             "\<forall>a\<in>sets M. space M - a \<in> sets M" 
   5.235 +             "\<forall>a\<in>sets M. \<forall>b\<in>sets M. a \<inter> b \<in> sets M"
   5.236 +             "a \<in> sets M" "b \<in> sets M"
   5.237 +  hence "a \<union> b = space M - ((space M - a) \<inter> (space M - b))"
   5.238 +    by blast
   5.239 +  also have "... \<in> sets M"
   5.240 +    by (metis ab)
   5.241 +  finally show "a \<union> b \<in> sets M" .
   5.242 +qed
   5.243 +
   5.244 +lemma (in algebra) sigma_property_disjoint_lemma:
   5.245 +  assumes sbC: "sets M \<subseteq> C"
   5.246 +      and ccdi: "closed_cdi (|space = space M, sets = C|)"
   5.247 +  shows "sigma_sets (space M) (sets M) \<subseteq> C"
   5.248 +proof -
   5.249 +  have "smallest_ccdi_sets M \<in> {B . sets M \<subseteq> B \<and> sigma_algebra (|space = space M, sets = B|)}"
   5.250 +    apply (auto simp add: sigma_algebra_disjoint_iff algebra_iff_Int 
   5.251 +            smallest_ccdi_sets_Int)
   5.252 +    apply (metis Union_Pow_eq Union_upper subsetD smallest_ccdi_sets) 
   5.253 +    apply (blast intro: smallest_ccdi_sets.Disj) 
   5.254 +    done
   5.255 +  hence "sigma_sets (space M) (sets M) \<subseteq> smallest_ccdi_sets M"
   5.256 +    by auto 
   5.257 +       (metis sigma_algebra.sigma_sets_subset algebra.simps(1) 
   5.258 +          algebra.simps(2) subsetD) 
   5.259 +  also have "...  \<subseteq> C"
   5.260 +    proof
   5.261 +      fix x
   5.262 +      assume x: "x \<in> smallest_ccdi_sets M"
   5.263 +      thus "x \<in> C"
   5.264 +	proof (induct rule: smallest_ccdi_sets.induct)
   5.265 +	  case (Basic x)
   5.266 +	  thus ?case
   5.267 +	    by (metis Basic subsetD sbC)
   5.268 +	next
   5.269 +	  case (Compl x)
   5.270 +	  thus ?case
   5.271 +	    by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
   5.272 + 	next
   5.273 +	  case (Inc A)
   5.274 +	  thus ?case
   5.275 +	       by (auto intro: closed_cdi_Inc [OF ccdi, simplified]) 
   5.276 +	next
   5.277 +	  case (Disj A)
   5.278 +	  thus ?case
   5.279 +	       by (auto intro: closed_cdi_Disj [OF ccdi, simplified]) 
   5.280 +	qed
   5.281 +    qed
   5.282 +  finally show ?thesis .
   5.283 +qed
   5.284 +
   5.285 +lemma (in algebra) sigma_property_disjoint:
   5.286 +  assumes sbC: "sets M \<subseteq> C"
   5.287 +      and compl: "!!s. s \<in> C \<inter> sigma_sets (space M) (sets M) \<Longrightarrow> space M - s \<in> C"
   5.288 +      and inc: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M) 
   5.289 +                     \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) 
   5.290 +                     \<Longrightarrow> (\<Union>i. A i) \<in> C"
   5.291 +      and disj: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M) 
   5.292 +                      \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> C"
   5.293 +  shows "sigma_sets (space M) (sets M) \<subseteq> C"
   5.294 +proof -
   5.295 +  have "sigma_sets (space M) (sets M) \<subseteq> C \<inter> sigma_sets (space M) (sets M)" 
   5.296 +    proof (rule sigma_property_disjoint_lemma) 
   5.297 +      show "sets M \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
   5.298 +	by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
   5.299 +    next
   5.300 +      show "closed_cdi \<lparr>space = space M, sets = C \<inter> sigma_sets (space M) (sets M)\<rparr>"
   5.301 +	by (simp add: closed_cdi_def compl inc disj)
   5.302 +           (metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed
   5.303 +	     IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
   5.304 +    qed
   5.305 +  thus ?thesis
   5.306 +    by blast
   5.307 +qed
   5.308 +
   5.309 +
   5.310 +(* or just countably_additiveD [OF measure_space.ca] *)
   5.311 +lemma (in measure_space) measure_countably_additive:
   5.312 +    "range A \<subseteq> sets M
   5.313 +     \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i. A i) \<in> sets M
   5.314 +     \<Longrightarrow> (measure M o A)  sums  measure M (\<Union>i. A i)"
   5.315 +  by (insert ca) (simp add: countably_additive_def o_def) 
   5.316 +
   5.317 +lemma (in measure_space) additive:
   5.318 +     "additive M (measure M)"
   5.319 +proof (rule algebra.countably_additive_additive [OF _ _ ca]) 
   5.320 +  show "algebra M"
   5.321 +    by (blast intro: sigma_algebra.axioms local.sigma_algebra_axioms)
   5.322 +  show "positive M (measure M)"
   5.323 +    by (simp add: positive_def empty_measure positive) 
   5.324 +qed
   5.325 + 
   5.326 +lemma (in measure_space) measure_additive:
   5.327 +     "a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {} 
   5.328 +      \<Longrightarrow> measure M a + measure M b = measure M (a \<union> b)"
   5.329 +  by (metis additiveD additive)
   5.330 +
   5.331 +lemma (in measure_space) measure_compl:
   5.332 +  assumes s: "s \<in> sets M"
   5.333 +  shows "measure M (space M - s) = measure M (space M) - measure M s"
   5.334 +proof -
   5.335 +  have "measure M (space M) = measure M (s \<union> (space M - s))" using s
   5.336 +    by (metis Un_Diff_cancel Un_absorb1 s sets_into_space)
   5.337 +  also have "... = measure M s + measure M (space M - s)"
   5.338 +    by (rule additiveD [OF additive]) (auto simp add: s) 
   5.339 +  finally have "measure M (space M) = measure M s + measure M (space M - s)" .
   5.340 +  thus ?thesis
   5.341 +    by arith
   5.342 +qed
   5.343 +
   5.344 +lemma disjoint_family_Suc:
   5.345 +  assumes Suc: "!!n. A n \<subseteq> A (Suc n)"
   5.346 +  shows "disjoint_family (\<lambda>i. A (Suc i) - A i)"
   5.347 +proof -
   5.348 +  {
   5.349 +    fix m
   5.350 +    have "!!n. A n \<subseteq> A (m+n)" 
   5.351 +    proof (induct m)
   5.352 +      case 0 show ?case by simp
   5.353 +    next
   5.354 +      case (Suc m) thus ?case
   5.355 +	by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans)
   5.356 +    qed
   5.357 +  }
   5.358 +  hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n"
   5.359 +    by (metis add_commute le_add_diff_inverse nat_less_le)
   5.360 +  thus ?thesis
   5.361 +    by (auto simp add: disjoint_family_def)
   5.362 +      (metis insert_absorb insert_subset le_SucE le_anti_sym not_leE) 
   5.363 +qed
   5.364 +
   5.365 +
   5.366 +lemma (in measure_space) measure_countable_increasing:
   5.367 +  assumes A: "range A \<subseteq> sets M"
   5.368 +      and A0: "A 0 = {}"
   5.369 +      and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
   5.370 +  shows "(measure M o A) ----> measure M (\<Union>i. A i)"
   5.371 +proof -
   5.372 +  {
   5.373 +    fix n
   5.374 +    have "(measure M \<circ> A) n =
   5.375 +          setsum (measure M \<circ> (\<lambda>i. A (Suc i) - A i)) {0..<n}"
   5.376 +      proof (induct n)
   5.377 +	case 0 thus ?case by (auto simp add: A0 empty_measure)
   5.378 +      next
   5.379 +	case (Suc m) 
   5.380 +	have "A (Suc m) = A m \<union> (A (Suc m) - A m)"
   5.381 +	  by (metis ASuc Un_Diff_cancel Un_absorb1)
   5.382 +	hence "measure M (A (Suc m)) =
   5.383 +               measure M (A m) + measure M (A (Suc m) - A m)" 
   5.384 +	  by (subst measure_additive) 
   5.385 +             (auto simp add: measure_additive range_subsetD [OF A]) 
   5.386 +	with Suc show ?case
   5.387 +	  by simp
   5.388 +      qed
   5.389 +  }
   5.390 +  hence Meq: "measure M o A = (\<lambda>n. setsum (measure M o (\<lambda>i. A(Suc i) - A i)) {0..<n})"
   5.391 +    by (blast intro: ext) 
   5.392 +  have Aeq: "(\<Union>i. A (Suc i) - A i) = (\<Union>i. A i)"
   5.393 +    proof (rule UN_finite2_eq [where k=1], simp) 
   5.394 +      fix i
   5.395 +      show "(\<Union>i\<in>{0..<i}. A (Suc i) - A i) = (\<Union>i\<in>{0..<Suc i}. A i)"
   5.396 +	proof (induct i)
   5.397 +	  case 0 thus ?case by (simp add: A0)
   5.398 +	next
   5.399 +	  case (Suc i) 
   5.400 +	  thus ?case
   5.401 +	    by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc])
   5.402 +	qed
   5.403 +    qed
   5.404 +  have A1: "\<And>i. A (Suc i) - A i \<in> sets M"
   5.405 +    by (metis A Diff range_subsetD)
   5.406 +  have A2: "(\<Union>i. A (Suc i) - A i) \<in> sets M"
   5.407 +    by (blast intro: countable_UN range_subsetD [OF A])  
   5.408 +  have "(measure M o (\<lambda>i. A (Suc i) - A i)) sums measure M (\<Union>i. A (Suc i) - A i)"
   5.409 +    by (rule measure_countably_additive) 
   5.410 +       (auto simp add: disjoint_family_Suc ASuc A1 A2)
   5.411 +  also have "... =  measure M (\<Union>i. A i)"
   5.412 +    by (simp add: Aeq) 
   5.413 +  finally have "(measure M o (\<lambda>i. A (Suc i) - A i)) sums measure M (\<Union>i. A i)" .
   5.414 +  thus ?thesis
   5.415 +    by (auto simp add: sums_iff Meq dest: summable_sumr_LIMSEQ_suminf) 
   5.416 +qed
   5.417 +
   5.418 +lemma (in measure_space) monotone_convergence:
   5.419 +  assumes A: "range A \<subseteq> sets M"
   5.420 +      and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
   5.421 +  shows "(measure M \<circ> A) ----> measure M (\<Union>i. A i)"
   5.422 +proof -
   5.423 +  have ueq: "(\<Union>i. nat_case {} A i) = (\<Union>i. A i)" 
   5.424 +    by (auto simp add: split: nat.splits) 
   5.425 +  have meq: "measure M \<circ> A = (\<lambda>n. (measure M \<circ> nat_case {} A) (Suc n))"
   5.426 +    by (rule ext) simp
   5.427 +  have "(measure M \<circ> nat_case {} A) ----> measure M (\<Union>i. nat_case {} A i)" 
   5.428 +    by (rule measure_countable_increasing) 
   5.429 +       (auto simp add: range_subsetD [OF A] subsetD [OF ASuc] split: nat.splits) 
   5.430 +  also have "... = measure M (\<Union>i. A i)" 
   5.431 +    by (simp add: ueq) 
   5.432 +  finally have "(measure M \<circ> nat_case {} A) ---->  measure M (\<Union>i. A i)" .
   5.433 +  thus ?thesis using meq
   5.434 +    by (metis LIMSEQ_Suc)
   5.435 +qed
   5.436 +
   5.437 +lemma measurable_sigma_preimages:
   5.438 +  assumes a: "sigma_algebra a" and b: "sigma_algebra b"
   5.439 +      and f: "f \<in> space a -> space b"
   5.440 +      and ba: "!!y. y \<in> sets b ==> f -` y \<in> sets a"
   5.441 +  shows "sigma_algebra (|space = space a, sets = (vimage f) ` (sets b) |)"
   5.442 +proof (simp add: sigma_algebra_iff2, intro conjI) 
   5.443 +  show "op -` f ` sets b \<subseteq> Pow (space a)"
   5.444 +    by auto (metis IntE a algebra.Int_space_eq1 ba sigma_algebra_iff vimageI) 
   5.445 +next
   5.446 +  show "{} \<in> op -` f ` sets b"
   5.447 +    by (metis algebra.empty_sets b image_iff sigma_algebra_iff vimage_empty)
   5.448 +next
   5.449 +  { fix y
   5.450 +    assume y: "y \<in> sets b"
   5.451 +    with a b f
   5.452 +    have "space a - f -` y = f -` (space b - y)"
   5.453 +      by (auto simp add: sigma_algebra_iff2) (blast intro: ba) 
   5.454 +    hence "space a - (f -` y) \<in> (vimage f) ` sets b"
   5.455 +      by auto
   5.456 +         (metis b y subsetD equalityE imageI sigma_algebra.sigma_sets_eq
   5.457 +                sigma_sets.Compl) 
   5.458 +  } 
   5.459 +  thus "\<forall>s\<in>sets b. space a - f -` s \<in> (vimage f) ` sets b"
   5.460 +    by blast
   5.461 +next
   5.462 +  {
   5.463 +    fix A:: "nat \<Rightarrow> 'a set"
   5.464 +    assume A: "range A \<subseteq> (vimage f) ` (sets b)"
   5.465 +    have  "(\<Union>i. A i) \<in> (vimage f) ` (sets b)"
   5.466 +      proof -
   5.467 +	def B \<equiv> "\<lambda>i. @v. v \<in> sets b \<and> f -` v = A i"
   5.468 +	{ 
   5.469 +	  fix i
   5.470 +	  have "A i \<in> (vimage f) ` (sets b)" using A
   5.471 +	    by blast
   5.472 +	  hence "\<exists>v. v \<in> sets b \<and> f -` v = A i"
   5.473 +	    by blast
   5.474 +	  hence "B i \<in> sets b \<and> f -` B i = A i" 
   5.475 +	    by (simp add: B_def) (erule someI_ex)
   5.476 +	} note B = this
   5.477 +	show ?thesis
   5.478 +	  proof
   5.479 +	    show "(\<Union>i. A i) = f -` (\<Union>i. B i)"
   5.480 +	      by (simp add: vimage_UN B) 
   5.481 +	   show "(\<Union>i. B i) \<in> sets b" using B
   5.482 +	     by (auto intro: sigma_algebra.countable_UN [OF b]) 
   5.483 +	  qed
   5.484 +      qed
   5.485 +  }
   5.486 +  thus "\<forall>A::nat \<Rightarrow> 'a set.
   5.487 +           range A \<subseteq> (vimage f) ` sets b \<longrightarrow> (\<Union>i. A i) \<in> (vimage f) ` sets b"
   5.488 +    by blast
   5.489 +qed
   5.490 +
   5.491 +lemma (in sigma_algebra) measurable_sigma:
   5.492 +  assumes B: "B \<subseteq> Pow X" 
   5.493 +      and f: "f \<in> space M -> X"
   5.494 +      and ba: "!!y. y \<in> B ==> (f -` y) \<inter> space M \<in> sets M"
   5.495 +  shows "f \<in> measurable M (sigma X B)"
   5.496 +proof -
   5.497 +  have "sigma_sets X B \<subseteq> {y . (f -` y) \<inter> space M \<in> sets M & y \<subseteq> X}"
   5.498 +    proof clarify
   5.499 +      fix x
   5.500 +      assume "x \<in> sigma_sets X B"
   5.501 +      thus "f -` x \<inter> space M \<in> sets M \<and> x \<subseteq> X"
   5.502 +	proof induct
   5.503 +	  case (Basic a)
   5.504 +	  thus ?case
   5.505 +	    by (auto simp add: ba) (metis B subsetD PowD) 
   5.506 +        next
   5.507 +	  case Empty
   5.508 +	  thus ?case
   5.509 +	    by auto
   5.510 +        next
   5.511 +	  case (Compl a)
   5.512 +	  have [simp]: "f -` X \<inter> space M = space M"
   5.513 +	    by (auto simp add: funcset_mem [OF f]) 
   5.514 +	  thus ?case
   5.515 +	    by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
   5.516 +	next
   5.517 +	  case (Union a)
   5.518 +	  thus ?case
   5.519 +	    by (simp add: vimage_UN, simp only: UN_extend_simps(4))
   5.520 +	       (blast intro: countable_UN)
   5.521 +	qed
   5.522 +    qed
   5.523 +  thus ?thesis
   5.524 +    by (simp add: measurable_def sigma_algebra_axioms sigma_algebra_sigma B f) 
   5.525 +       (auto simp add: sigma_def) 
   5.526 +qed
   5.527 +
   5.528 +lemma measurable_subset:
   5.529 +     "measurable a b \<subseteq> measurable a (sigma (space b) (sets b))"
   5.530 +  apply clarify
   5.531 +  apply (rule sigma_algebra.measurable_sigma) 
   5.532 +  apply (auto simp add: measurable_def)
   5.533 +  apply (metis algebra.sets_into_space subsetD sigma_algebra_iff) 
   5.534 +  done
   5.535 +
   5.536 +lemma measurable_eqI: 
   5.537 +     "space m1 = space m1' \<Longrightarrow> space m2 = space m2'
   5.538 +      \<Longrightarrow> sets m1 = sets m1' \<Longrightarrow> sets m2 = sets m2'
   5.539 +      \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
   5.540 +  by (simp add: measurable_def sigma_algebra_iff2) 
   5.541 +
   5.542 +lemma measure_preserving_lift:
   5.543 +  fixes f :: "'a1 \<Rightarrow> 'a2" 
   5.544 +    and m1 :: "('a1, 'b1) measure_space_scheme"
   5.545 +    and m2 :: "('a2, 'b2) measure_space_scheme"
   5.546 +  assumes m1: "measure_space m1" and m2: "measure_space m2" 
   5.547 +  defines "m x \<equiv> (|space = space m2, sets = x, measure = measure m2, ... = more m2|)"
   5.548 +  assumes setsm2: "sets m2 = sigma_sets (space m2) a"
   5.549 +      and fmp: "f \<in> measure_preserving m1 (m a)"
   5.550 +  shows "f \<in> measure_preserving m1 m2"
   5.551 +proof -
   5.552 +  have [simp]: "!!x. space (m x) = space m2 & sets (m x) = x & measure (m x) = measure m2"
   5.553 +    by (simp add: m_def) 
   5.554 +  have sa1: "sigma_algebra m1" using m1 
   5.555 +    by (simp add: measure_space_def) 
   5.556 +  show ?thesis using fmp
   5.557 +    proof (clarsimp simp add: measure_preserving_def m1 m2) 
   5.558 +      assume fm: "f \<in> measurable m1 (m a)" 
   5.559 +	 and mam: "measure_space (m a)"
   5.560 +	 and meq: "\<forall>y\<in>a. measure m1 (f -` y \<inter> space m1) = measure m2 y"
   5.561 +      have "f \<in> measurable m1 (sigma (space (m a)) (sets (m a)))"
   5.562 +	by (rule subsetD [OF measurable_subset fm]) 
   5.563 +      also have "... = measurable m1 m2"
   5.564 +	by (rule measurable_eqI) (simp_all add: m_def setsm2 sigma_def) 
   5.565 +      finally have f12: "f \<in> measurable m1 m2" .
   5.566 +      hence ffn: "f \<in> space m1 \<rightarrow> space m2"
   5.567 +	by (simp add: measurable_def) 
   5.568 +      have "space m1 \<subseteq> f -` (space m2)"
   5.569 +	by auto (metis PiE ffn)
   5.570 +      hence fveq [simp]: "(f -` (space m2)) \<inter> space m1 = space m1"
   5.571 +	by blast
   5.572 +      {
   5.573 +	fix y
   5.574 +	assume y: "y \<in> sets m2" 
   5.575 +	have ama: "algebra (m a)"  using mam
   5.576 +	  by (simp add: measure_space_def sigma_algebra_iff) 
   5.577 +	have spa: "space m2 \<in> a" using algebra.top [OF ama]
   5.578 +	  by (simp add: m_def) 
   5.579 +	have "sigma_sets (space m2) a = sigma_sets (space (m a)) (sets (m a))"
   5.580 +	  by (simp add: m_def) 
   5.581 +	also have "... \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}"
   5.582 +	  proof (rule algebra.sigma_property_disjoint, auto simp add: ama) 
   5.583 +	    fix x
   5.584 +	    assume x: "x \<in> a"
   5.585 +	    thus "measure m1 (f -` x \<inter> space m1) = measure m2 x"
   5.586 +	      by (simp add: meq)
   5.587 +	  next
   5.588 +	    fix s
   5.589 +	    assume eq: "measure m1 (f -` s \<inter> space m1) = measure m2 s"
   5.590 +	       and s: "s \<in> sigma_sets (space m2) a"
   5.591 +	    hence s2: "s \<in> sets m2"
   5.592 +	      by (simp add: setsm2) 
   5.593 +	    thus "measure m1 (f -` (space m2 - s) \<inter> space m1) =
   5.594 +                  measure m2 (space m2 - s)" using f12
   5.595 +	      by (simp add: vimage_Diff Diff_Int_distrib2 eq m1 m2
   5.596 +		    measure_space.measure_compl measurable_def)  
   5.597 +	         (metis fveq meq spa) 
   5.598 +	  next
   5.599 +	    fix A
   5.600 +	      assume A0: "A 0 = {}"
   5.601 +	 	 and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
   5.602 +		 and rA1: "range A \<subseteq> 
   5.603 +		           {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
   5.604 +		 and "range A \<subseteq> sigma_sets (space m2) a"
   5.605 +	      hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
   5.606 +	      have eq1: "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
   5.607 +		using rA1 by blast
   5.608 +	      have "(measure m2 \<circ> A) = measure m1 o (\<lambda>i. (f -` A i \<inter> space m1))" 
   5.609 +		by (simp add: o_def eq1) 
   5.610 +	      also have "... ----> measure m1 (\<Union>i. f -` A i \<inter> space m1)"
   5.611 +		proof (rule measure_space.measure_countable_increasing [OF m1])
   5.612 +		  show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
   5.613 +		    using f12 rA2 by (auto simp add: measurable_def)
   5.614 +		  show "f -` A 0 \<inter> space m1 = {}" using A0
   5.615 +		    by blast
   5.616 +		  show "\<And>n. f -` A n \<inter> space m1 \<subseteq> f -` A (Suc n) \<inter> space m1"
   5.617 +		    using ASuc by auto
   5.618 +		qed
   5.619 +	      also have "... = measure m1 (f -` (\<Union>i. A i) \<inter> space m1)"
   5.620 +		by (simp add: vimage_UN)
   5.621 +	      finally have "(measure m2 \<circ> A) ----> measure m1 (f -` (\<Union>i. A i) \<inter> space m1)" .
   5.622 +	      moreover
   5.623 +	      have "(measure m2 \<circ> A) ----> measure m2 (\<Union>i. A i)"
   5.624 +		by (rule measure_space.measure_countable_increasing 
   5.625 +		          [OF m2 rA2, OF A0 ASuc])
   5.626 +	      ultimately 
   5.627 +	      show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
   5.628 +                    measure m2 (\<Union>i. A i)"
   5.629 +		by (rule LIMSEQ_unique) 
   5.630 +	  next
   5.631 +	    fix A :: "nat => 'a2 set"
   5.632 +	      assume dA: "disjoint_family A"
   5.633 +		 and rA1: "range A \<subseteq> 
   5.634 +		           {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
   5.635 +		 and "range A \<subseteq> sigma_sets (space m2) a"
   5.636 +	      hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
   5.637 +	      hence Um2: "(\<Union>i. A i) \<in> sets m2"
   5.638 +		by (metis range_subsetD setsm2 sigma_sets.Union)
   5.639 +	      have "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
   5.640 +		using rA1 by blast
   5.641 +	      hence "measure m2 o A = measure m1 o (\<lambda>i. f -` A i \<inter> space m1)"
   5.642 +		by (simp add: o_def) 
   5.643 +	      also have "... sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" 
   5.644 +		proof (rule measure_space.measure_countably_additive [OF m1] )
   5.645 +		  show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
   5.646 +		    using f12 rA2 by (auto simp add: measurable_def)
   5.647 +		  show "disjoint_family (\<lambda>i. f -` A i \<inter> space m1)" using dA
   5.648 +		    by (auto simp add: disjoint_family_def) 
   5.649 +		  show "(\<Union>i. f -` A i \<inter> space m1) \<in> sets m1"
   5.650 +		    proof (rule sigma_algebra.countable_UN [OF sa1])
   5.651 +		      show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1" using f12 rA2
   5.652 +			by (auto simp add: measurable_def) 
   5.653 +		    qed
   5.654 + 		qed
   5.655 +	      finally have "(measure m2 o A) sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" .
   5.656 +	      with measure_space.measure_countably_additive [OF m2 rA2 dA Um2] 
   5.657 +	      have "measure m1 (\<Union>i. f -` A i \<inter> space m1) = measure m2 (\<Union>i. A i)"
   5.658 +		by (metis sums_unique) 
   5.659 +
   5.660 +	      moreover have "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) = measure m1 (\<Union>i. f -` A i \<inter> space m1)"
   5.661 +		by (simp add: vimage_UN)
   5.662 +	      ultimately show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
   5.663 +                    measure m2 (\<Union>i. A i)" 
   5.664 +		by metis
   5.665 +	  qed
   5.666 +	finally have "sigma_sets (space m2) a 
   5.667 +              \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}" .
   5.668 +	hence "measure m1 (f -` y \<inter> space m1) = measure m2 y" using y
   5.669 +	  by (force simp add: setsm2) 
   5.670 +      }
   5.671 +      thus "f \<in> measurable m1 m2 \<and>
   5.672 +       (\<forall>y\<in>sets m2.
   5.673 +           measure m1 (f -` y \<inter> space m1) = measure m2 y)"
   5.674 +	by (blast intro: f12) 
   5.675 +    qed
   5.676 +qed
   5.677 +
   5.678 +lemma measurable_ident:
   5.679 +     "sigma_algebra M ==> id \<in> measurable M M"
   5.680 +  apply (simp add: measurable_def)
   5.681 +  apply (auto simp add: sigma_algebra_def algebra.Int algebra.top)
   5.682 +  done
   5.683 +
   5.684 +lemma measurable_comp:
   5.685 +  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c" 
   5.686 +  shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
   5.687 +  apply (auto simp add: measurable_def vimage_compose) 
   5.688 +  apply (subgoal_tac "f -` g -` y \<inter> space a = f -` (g -` y \<inter> space b) \<inter> space a")
   5.689 +  apply force+
   5.690 +  done
   5.691 +
   5.692 + lemma measurable_strong:
   5.693 +  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c" 
   5.694 +  assumes f: "f \<in> measurable a b" and g: "g \<in> (space b -> space c)"
   5.695 +      and c: "sigma_algebra c"
   5.696 +      and t: "f ` (space a) \<subseteq> t"
   5.697 +      and cb: "\<And>s. s \<in> sets c \<Longrightarrow> (g -` s) \<inter> t \<in> sets b"
   5.698 +  shows "(g o f) \<in> measurable a c"
   5.699 +proof -
   5.700 +  have a: "sigma_algebra a" and b: "sigma_algebra b"
   5.701 +   and fab: "f \<in> (space a -> space b)"
   5.702 +   and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f -` y) \<inter> (space a) \<in> sets a" using f
   5.703 +     by (auto simp add: measurable_def)
   5.704 +  have eq: "f -` g -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
   5.705 +    by force
   5.706 +  show ?thesis
   5.707 +    apply (auto simp add: measurable_def vimage_compose a c) 
   5.708 +    apply (metis funcset_mem fab g) 
   5.709 +    apply (subst eq, metis ba cb) 
   5.710 +    done
   5.711 +qed
   5.712 + 
   5.713 +lemma measurable_mono1:
   5.714 +     "a \<subseteq> b \<Longrightarrow> sigma_algebra \<lparr>space = X, sets = b\<rparr>
   5.715 +      \<Longrightarrow> measurable \<lparr>space = X, sets = a\<rparr> c \<subseteq> measurable \<lparr>space = X, sets = b\<rparr> c"
   5.716 +  by (auto simp add: measurable_def) 
   5.717 +
   5.718 +lemma measurable_up_sigma:
   5.719 +   "measurable a b \<subseteq> measurable (sigma (space a) (sets a)) b"
   5.720 +  apply (auto simp add: measurable_def) 
   5.721 +  apply (metis sigma_algebra_iff2 sigma_algebra_sigma)
   5.722 +  apply (metis algebra.simps(2) sigma_algebra.sigma_sets_eq sigma_def) 
   5.723 +  done
   5.724 +
   5.725 +lemma measure_preserving_up:
   5.726 +   "f \<in> measure_preserving \<lparr>space = space m1, sets = a, measure = measure m1\<rparr> m2 \<Longrightarrow>
   5.727 +    measure_space m1 \<Longrightarrow> sigma_algebra m1 \<Longrightarrow> a \<subseteq> sets m1 
   5.728 +    \<Longrightarrow> f \<in> measure_preserving m1 m2"
   5.729 +  by (auto simp add: measure_preserving_def measurable_def) 
   5.730 +
   5.731 +lemma measure_preserving_up_sigma:
   5.732 +   "measure_space m1 \<Longrightarrow> (sets m1 = sets (sigma (space m1) a))
   5.733 +    \<Longrightarrow> measure_preserving \<lparr>space = space m1, sets = a, measure = measure m1\<rparr> m2 
   5.734 +        \<subseteq> measure_preserving m1 m2"
   5.735 +  apply (rule subsetI) 
   5.736 +  apply (rule measure_preserving_up) 
   5.737 +  apply (simp_all add: measure_space_def sigma_def) 
   5.738 +  apply (metis sigma_algebra.sigma_sets_eq subsetI sigma_sets.Basic) 
   5.739 +  done
   5.740 +
   5.741 +lemma (in sigma_algebra) measurable_prod_sigma:
   5.742 +  assumes 1: "(fst o f) \<in> measurable M a1" and 2: "(snd o f) \<in> measurable M a2"
   5.743 +  shows "f \<in> measurable M (sigma ((space a1) \<times> (space a2)) 
   5.744 +                          (prod_sets (sets a1) (sets a2)))"
   5.745 +proof -
   5.746 +  from 1 have sa1: "sigma_algebra a1" and fn1: "fst \<circ> f \<in> space M \<rightarrow> space a1"
   5.747 +     and q1: "\<forall>y\<in>sets a1. (fst \<circ> f) -` y \<inter> space M \<in> sets M"
   5.748 +    by (auto simp add: measurable_def) 
   5.749 +  from 2 have sa2: "sigma_algebra a2" and fn2: "snd \<circ> f \<in> space M \<rightarrow> space a2"
   5.750 +     and q2: "\<forall>y\<in>sets a2. (snd \<circ> f) -` y \<inter> space M \<in> sets M"
   5.751 +    by (auto simp add: measurable_def) 
   5.752 +  show ?thesis
   5.753 +    proof (rule measurable_sigma) 
   5.754 +      show "prod_sets (sets a1) (sets a2) \<subseteq> Pow (space a1 \<times> space a2)" using sa1 sa2
   5.755 +        by (force simp add: prod_sets_def sigma_algebra_iff algebra_def) 
   5.756 +    next
   5.757 +      show "f \<in> space M \<rightarrow> space a1 \<times> space a2" 
   5.758 +        by (rule prod_final [OF fn1 fn2])
   5.759 +    next
   5.760 +      fix z
   5.761 +      assume z: "z \<in> prod_sets (sets a1) (sets a2)" 
   5.762 +      thus "f -` z \<inter> space M \<in> sets M"
   5.763 +        proof (auto simp add: prod_sets_def vimage_Times) 
   5.764 +          fix x y
   5.765 +          assume x: "x \<in> sets a1" and y: "y \<in> sets a2"
   5.766 +          have "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M = 
   5.767 +                ((fst \<circ> f) -` x \<inter> space M) \<inter> ((snd \<circ> f) -` y \<inter> space M)"
   5.768 +            by blast
   5.769 +          also have "...  \<in> sets M" using x y q1 q2
   5.770 +            by blast
   5.771 +          finally show "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M \<in> sets M" .
   5.772 +        qed
   5.773 +    qed
   5.774 +qed
   5.775 +
   5.776 +
   5.777 +lemma (in measure_space) measurable_range_reduce:
   5.778 +   "f \<in> measurable M \<lparr>space = s, sets = Pow s\<rparr> \<Longrightarrow>
   5.779 +    s \<noteq> {} 
   5.780 +    \<Longrightarrow> f \<in> measurable M \<lparr>space = s \<inter> (f ` space M), sets = Pow (s \<inter> (f ` space M))\<rparr>"
   5.781 +  by (simp add: measurable_def sigma_algebra_Pow del: Pow_Int_eq) blast
   5.782 +
   5.783 +lemma (in measure_space) measurable_Pow_to_Pow:
   5.784 +   "(sets M = Pow (space M)) \<Longrightarrow> f \<in> measurable M \<lparr>space = UNIV, sets = Pow UNIV\<rparr>"
   5.785 +  by (auto simp add: measurable_def sigma_algebra_def sigma_algebra_axioms_def algebra_def)
   5.786 +
   5.787 +lemma (in measure_space) measurable_Pow_to_Pow_image:
   5.788 +   "sets M = Pow (space M)
   5.789 +    \<Longrightarrow> f \<in> measurable M \<lparr>space = f ` space M, sets = Pow (f ` space M)\<rparr>"
   5.790 +  by (simp add: measurable_def sigma_algebra_Pow) intro_locales
   5.791 +
   5.792 +lemma (in measure_space) measure_real_sum_image:
   5.793 +  assumes s: "s \<in> sets M"
   5.794 +      and ssets: "\<And>x. x \<in> s ==> {x} \<in> sets M"
   5.795 +      and fin: "finite s"
   5.796 +  shows "measure M s = (\<Sum>x\<in>s. measure M {x})"
   5.797 +proof -
   5.798 +  {
   5.799 +    fix u
   5.800 +    assume u: "u \<subseteq> s & u \<in> sets M"
   5.801 +    hence "finite u"
   5.802 +      by (metis fin finite_subset) 
   5.803 +    hence "measure M u = (\<Sum>x\<in>u. measure M {x})" using u
   5.804 +      proof (induct u)
   5.805 +        case empty
   5.806 +        thus ?case by simp
   5.807 +      next
   5.808 +        case (insert x t)
   5.809 +        hence x: "x \<in> s" and t: "t \<subseteq> s" 
   5.810 +          by (simp_all add: insert_subset) 
   5.811 +        hence ts: "t \<in> sets M"  using insert
   5.812 +          by (metis Diff_insert_absorb Diff ssets)
   5.813 +        have "measure M (insert x t) = measure M ({x} \<union> t)"
   5.814 +          by simp
   5.815 +        also have "... = measure M {x} + measure M t" 
   5.816 +          by (simp add: measure_additive insert insert_disjoint ssets x ts 
   5.817 +                  del: Un_insert_left)
   5.818 +        also have "... = (\<Sum>x\<in>insert x t. measure M {x})" 
   5.819 +          by (simp add: x t ts insert) 
   5.820 +        finally show ?case .
   5.821 +      qed
   5.822 +    }
   5.823 +  thus ?thesis
   5.824 +    by (metis subset_refl s)
   5.825 +qed
   5.826 +  
   5.827 +lemma (in sigma_algebra) sigma_algebra_extend:
   5.828 +     "sigma_algebra \<lparr>space = space M, sets = sets M, measure_space.measure = f\<rparr>"
   5.829 +proof -
   5.830 +  have 1: "sigma_algebra M \<Longrightarrow> ?thesis"
   5.831 +    by (simp add: sigma_algebra_def algebra_def sigma_algebra_axioms_def) 
   5.832 +  show ?thesis
   5.833 +    by (rule 1) intro_locales
   5.834 +qed
   5.835 +
   5.836 +
   5.837 +lemma (in sigma_algebra) finite_additivity_sufficient:
   5.838 +  assumes fin: "finite (space M)"
   5.839 +      and posf: "positive M f" and addf: "additive M f" 
   5.840 +  defines "Mf \<equiv> \<lparr>space = space M, sets = sets M, measure = f\<rparr>"
   5.841 +  shows "measure_space Mf" 
   5.842 +proof -
   5.843 +  have [simp]: "f {} = 0" using posf
   5.844 +    by (simp add: positive_def) 
   5.845 +  have "countably_additive Mf f"
   5.846 +    proof (auto simp add: countably_additive_def positive_def) 
   5.847 +      fix A :: "nat \<Rightarrow> 'a set"
   5.848 +      assume A: "range A \<subseteq> sets Mf"
   5.849 +         and disj: "disjoint_family A"
   5.850 +         and UnA: "(\<Union>i. A i) \<in> sets Mf"
   5.851 +      def I \<equiv> "{i. A i \<noteq> {}}"
   5.852 +      have "Union (A ` I) \<subseteq> space M" using A
   5.853 +        by (auto simp add: Mf_def) (metis range_subsetD subsetD sets_into_space) 
   5.854 +      hence "finite (A ` I)"
   5.855 +        by (metis finite_UnionD finite_subset fin) 
   5.856 +      moreover have "inj_on A I" using disj
   5.857 +        by (auto simp add: I_def disjoint_family_def inj_on_def) 
   5.858 +      ultimately have finI: "finite I"
   5.859 +        by (metis finite_imageD)
   5.860 +      hence "\<exists>N. \<forall>m\<ge>N. A m = {}"
   5.861 +        proof (cases "I = {}")
   5.862 +          case True thus ?thesis by (simp add: I_def) 
   5.863 +        next
   5.864 +          case False
   5.865 +          hence "\<forall>i\<in>I. i < Suc(Max I)"
   5.866 +            by (simp add: Max_less_iff [symmetric] finI) 
   5.867 +          hence "\<forall>m \<ge> Suc(Max I). A m = {}"
   5.868 +            by (simp add: I_def) (metis less_le_not_le) 
   5.869 +          thus ?thesis
   5.870 +            by blast
   5.871 +        qed
   5.872 +      then obtain N where N: "\<forall>m\<ge>N. A m = {}" by blast
   5.873 +      hence "\<forall>m\<ge>N. (f o A) m = 0"
   5.874 +        by simp 
   5.875 +      hence "(\<lambda>n. f (A n)) sums setsum (f o A) {0..<N}" 
   5.876 +        by (simp add: series_zero o_def) 
   5.877 +      also have "... = f (\<Union>i<N. A i)"
   5.878 +        proof (induct N)
   5.879 +          case 0 thus ?case by simp
   5.880 +        next
   5.881 +          case (Suc n) 
   5.882 +          have "f (A n \<union> (\<Union> x<n. A x)) = f (A n) + f (\<Union> i<n. A i)"
   5.883 +            proof (rule Caratheodory.additiveD [OF addf])
   5.884 +              show "A n \<inter> (\<Union> x<n. A x) = {}" using disj
   5.885 +                by (auto simp add: disjoint_family_def nat_less_le) blast
   5.886 +              show "A n \<in> sets M" using A 
   5.887 +                by (force simp add: Mf_def) 
   5.888 +              show "(\<Union>i<n. A i) \<in> sets M"
   5.889 +                proof (induct n)
   5.890 +                  case 0 thus ?case by simp
   5.891 +                next
   5.892 +                  case (Suc n) thus ?case using A
   5.893 +                    by (simp add: lessThan_Suc Mf_def Un range_subsetD) 
   5.894 +                qed
   5.895 +            qed
   5.896 +          thus ?case using Suc
   5.897 +            by (simp add: lessThan_Suc) 
   5.898 +        qed
   5.899 +      also have "... = f (\<Union>i. A i)" 
   5.900 +        proof -
   5.901 +          have "(\<Union> i<N. A i) = (\<Union>i. A i)" using N
   5.902 +            by auto (metis Int_absorb N disjoint_iff_not_equal lessThan_iff not_leE)
   5.903 +          thus ?thesis by simp
   5.904 +        qed
   5.905 +      finally show "(\<lambda>n. f (A n)) sums f (\<Union>i. A i)" .
   5.906 +    qed
   5.907 +  thus ?thesis using posf 
   5.908 +    by (simp add: Mf_def measure_space_def measure_space_axioms_def sigma_algebra_extend positive_def) 
   5.909 +qed
   5.910 +
   5.911 +lemma finite_additivity_sufficient:
   5.912 +     "sigma_algebra M 
   5.913 +      \<Longrightarrow> finite (space M) 
   5.914 +      \<Longrightarrow> positive M (measure M) \<Longrightarrow> additive M (measure M) 
   5.915 +      \<Longrightarrow> measure_space M"
   5.916 +  by (rule measure_down [OF sigma_algebra.finite_additivity_sufficient], auto) 
   5.917 +
   5.918 +end
   5.919 +
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Probability/Probability.thy	Wed Oct 28 11:42:31 2009 +0000
     6.3 @@ -0,0 +1,5 @@
     6.4 +theory Probability imports
     6.5 +	Measure
     6.6 +begin
     6.7 +
     6.8 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Probability/ROOT.ML	Wed Oct 28 11:42:31 2009 +0000
     7.3 @@ -0,0 +1,6 @@
     7.4 +(*
     7.5 +  no_document use_thy "ThisTheory";
     7.6 +  use_thy "ThatTheory";
     7.7 +*)
     7.8 +
     7.9 +use_thy "Probability";
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Probability/SeriesPlus.thy	Wed Oct 28 11:42:31 2009 +0000
     8.3 @@ -0,0 +1,127 @@
     8.4 +theory SeriesPlus
     8.5 +  imports Complex_Main Nat_Int_Bij 
     8.6 +
     8.7 +begin
     8.8 +
     8.9 +text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
    8.10 +
    8.11 +lemma choice2: "(!!x. \<exists>y z. Q x y z) ==> \<exists>f g. \<forall>x. Q x (f x) (g x)"
    8.12 +  by metis
    8.13 +
    8.14 +lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
    8.15 +  by blast
    8.16 +
    8.17 +
    8.18 +lemma suminf_2dimen:
    8.19 +  fixes f:: "nat * nat \<Rightarrow> real"
    8.20 +  assumes f_nneg: "!!m n. 0 \<le> f(m,n)"
    8.21 +      and fsums: "!!m. (\<lambda>n. f (m,n)) sums (g m)"
    8.22 +      and sumg: "summable g"
    8.23 +  shows "(f o nat_to_nat2) sums suminf g"
    8.24 +proof (simp add: sums_def)
    8.25 +  {
    8.26 +    fix x
    8.27 +    have "0 \<le> f x"
    8.28 +      by (cases x) (simp add: f_nneg) 
    8.29 +  } note [iff]  = this
    8.30 +  have g_nneg: "!!m. 0 \<le> g m"
    8.31 +    proof -
    8.32 +      fix m
    8.33 +      have "0 \<le> suminf (\<lambda>n. f (m,n))"
    8.34 +	by (rule suminf_0_le, simp add: f_nneg, metis fsums sums_iff)
    8.35 +      thus "0 \<le> g m" using fsums [of m] 
    8.36 +	by (auto simp add: sums_iff) 
    8.37 +    qed
    8.38 +  show "(\<lambda>n. \<Sum>x = 0..<n. f (nat_to_nat2 x)) ----> suminf g"
    8.39 +  proof (rule increasing_LIMSEQ, simp add: f_nneg)
    8.40 +    fix n
    8.41 +    def i \<equiv> "Max (Domain (nat_to_nat2 ` {0..<n}))"
    8.42 +    def j \<equiv> "Max (Range (nat_to_nat2 ` {0..<n}))"
    8.43 +    have ij: "nat_to_nat2 ` {0..<n} \<subseteq> ({0..i} \<times> {0..j})" 
    8.44 +      by (force simp add: i_def j_def 
    8.45 +                intro: finite_imageI Max_ge finite_Domain finite_Range)  
    8.46 +    have "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) = setsum f (nat_to_nat2 ` {0..<n})" 
    8.47 +      using setsum_reindex [of nat_to_nat2 "{0..<n}" f] 
    8.48 +      by (simp add: o_def)
    8.49 +         (metis nat_to_nat2_inj subset_inj_on subset_UNIV nat_to_nat2_inj) 
    8.50 +    also have "... \<le> setsum f ({0..i} \<times> {0..j})"
    8.51 +      by (rule setsum_mono2) (auto simp add: ij) 
    8.52 +    also have "... = setsum (\<lambda>m. setsum (\<lambda>n. f (m,n)) {0..j}) {0..<Suc i}"
    8.53 +      by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost
    8.54 +	        setsum_cartesian_product split_eta) 
    8.55 +    also have "... \<le> setsum g {0..<Suc i}" 
    8.56 +      proof (rule setsum_mono, simp add: less_Suc_eq_le) 
    8.57 +	fix m
    8.58 +	assume m: "m \<le> i"
    8.59 +	thus " (\<Sum>n = 0..j. f (m, n)) \<le> g m" using fsums [of m]
    8.60 +	  by (auto simp add: sums_iff) 
    8.61 +	   (metis atLeastLessThanSuc_atLeastAtMost f_nneg series_pos_le f_nneg) 
    8.62 +      qed
    8.63 +    finally have  "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> setsum g {0..<Suc i}" .
    8.64 +    also have "... \<le> suminf g" 
    8.65 +      by (rule series_pos_le [OF sumg]) (simp add: g_nneg) 
    8.66 +    finally show "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> suminf g" .
    8.67 +  next
    8.68 +    fix e :: real
    8.69 +    assume e: "0 < e"
    8.70 +    with summable_sums [OF sumg]
    8.71 +    obtain N where "\<bar>setsum g {0..<N} - suminf g\<bar> < e/2" and nz: "N>0"
    8.72 +      by (simp add: sums_def LIMSEQ_iff_nz dist_real_def)
    8.73 +         (metis e half_gt_zero le_refl that)
    8.74 +    hence gless: "suminf g < setsum g {0..<N} + e/2" using series_pos_le [OF sumg]
    8.75 +      by (simp add: g_nneg)
    8.76 +    { fix m
    8.77 +      assume m: "m<N"
    8.78 +      hence enneg: "0 < e / (2 * real N)" using e
    8.79 +	by (simp add: zero_less_divide_iff) 
    8.80 +      hence  "\<exists>j. \<bar>(\<Sum>n = 0..<j. f (m, n)) - g m\<bar> < e/(2 * real N)"
    8.81 +	using fsums [of m] m
    8.82 +        by (force simp add: sums_def LIMSEQ_def dist_real_def)
    8.83 +      hence "\<exists>j. g m < setsum (\<lambda>n. f (m,n)) {0..<j} + e/(2 * real N)" 
    8.84 +	using fsums [of m]
    8.85 +	by (auto simp add: sums_iff) 
    8.86 +           (metis abs_diff_less_iff add_less_cancel_right eq_diff_eq') 
    8.87 +    }
    8.88 +    hence "\<exists>jj. \<forall>m. m<N \<longrightarrow> g m < (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N)"
    8.89 +      by (force intro: choice) 
    8.90 +    then obtain jj where jj:
    8.91 +          "!!m. m<N \<Longrightarrow> g m < (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N)"
    8.92 +      by auto
    8.93 +    def IJ \<equiv> "SIGMA i : {0..<N}. {0..<jj i}"
    8.94 +    have "setsum g {0..<N} <
    8.95 +             (\<Sum>m = 0..<N. (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N))"
    8.96 +      by (auto simp add: nz jj intro: setsum_strict_mono) 
    8.97 +    also have "... = (\<Sum>m = 0..<N. \<Sum>n = 0..<jj m. f (m, n)) + e/2" using nz
    8.98 +      by (auto simp add: setsum_addf real_of_nat_def) 
    8.99 +    also have "... = setsum f IJ + e/2" 
   8.100 +      by (simp add: IJ_def setsum_Sigma) 
   8.101 +    finally have "setsum g {0..<N} < setsum f IJ + e/2" .
   8.102 +    hence glessf: "suminf g < setsum f IJ + e" using gless 
   8.103 +      by auto
   8.104 +    have finite_IJ: "finite IJ"
   8.105 +      by (simp add: IJ_def) 
   8.106 +    def NIJ \<equiv> "Max (nat_to_nat2 -` IJ)"
   8.107 +    have IJsb: "IJ \<subseteq> nat_to_nat2 ` {0..NIJ}"
   8.108 +      proof (auto simp add: NIJ_def)
   8.109 +	fix i j
   8.110 +	assume ij:"(i,j) \<in> IJ"
   8.111 +	hence "(i,j) = nat_to_nat2 (inv nat_to_nat2 (i,j))"
   8.112 +	  by (metis nat_to_nat2_surj surj_f_inv_f) 
   8.113 +	thus "(i,j) \<in> nat_to_nat2 ` {0..Max (nat_to_nat2 -` IJ)}"
   8.114 +	  by (rule image_eqI) 
   8.115 +	     (simp add: ij finite_vimageI [OF finite_IJ nat_to_nat2_inj]
   8.116 +                    nat_to_nat2_surj surj_f_inv_f) 
   8.117 +      qed
   8.118 +    have "setsum f IJ \<le> setsum f (nat_to_nat2 `{0..NIJ})"
   8.119 +      by (rule setsum_mono2) (auto simp add: IJsb) 
   8.120 +    also have "... = (\<Sum>k = 0..NIJ. f (nat_to_nat2 k))"
   8.121 +      by (simp add: setsum_reindex subset_inj_on [OF nat_to_nat2_inj subset_UNIV]) 
   8.122 +    also have "... = (\<Sum>k = 0..<Suc NIJ. f (nat_to_nat2 k))"
   8.123 +      by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost)
   8.124 +    finally have "setsum f IJ \<le> (\<Sum>k = 0..<Suc NIJ. f (nat_to_nat2 k))" .
   8.125 +    thus "\<exists>n. suminf g \<le> (\<Sum>x = 0..<n. f (nat_to_nat2 x)) + e" using glessf
   8.126 +      by (metis add_right_mono local.glessf not_leE order_le_less_trans less_asym)
   8.127 +  qed
   8.128 +qed
   8.129 +
   8.130 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Oct 28 11:42:31 2009 +0000
     9.3 @@ -0,0 +1,229 @@
     9.4 +(*  Title:      Sigma_Algebra.thy
     9.5 +    Author:     Stefan Richter, Markus Wenzel, TU Muenchen
     9.6 +    Plus material from the Hurd/Coble measure theory development, 
     9.7 +    translated by Lawrence Paulson.
     9.8 +*)
     9.9 +
    9.10 +header {* Sigma Algebras *}
    9.11 +
    9.12 +theory Sigma_Algebra imports Complex_Main begin
    9.13 +
    9.14 +text {* Sigma algebras are an elementary concept in measure
    9.15 +  theory. To measure --- that is to integrate --- functions, we first have
    9.16 +  to measure sets. Unfortunately, when dealing with a large universe,
    9.17 +  it is often not possible to consistently assign a measure to every
    9.18 +  subset. Therefore it is necessary to define the set of measurable
    9.19 +  subsets of the universe. A sigma algebra is such a set that has
    9.20 +  three very natural and desirable properties. *}
    9.21 +
    9.22 +subsection {* Algebras *}
    9.23 +
    9.24 +record 'a algebra = 
    9.25 +  space :: "'a set" 
    9.26 +  sets :: "'a set set"
    9.27 +
    9.28 +locale algebra =
    9.29 +  fixes M
    9.30 +  assumes space_closed: "sets M \<subseteq> Pow (space M)"
    9.31 +     and  empty_sets [iff]: "{} \<in> sets M"
    9.32 +     and  compl_sets [intro]: "!!a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M"
    9.33 +     and  Un [intro]: "!!a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<union> b \<in> sets M"
    9.34 +
    9.35 +lemma (in algebra) top [iff]: "space M \<in> sets M"
    9.36 +  by (metis Diff_empty compl_sets empty_sets)
    9.37 +
    9.38 +lemma (in algebra) sets_into_space: "x \<in> sets M \<Longrightarrow> x \<subseteq> space M"
    9.39 +  by (metis PowD contra_subsetD space_closed)
    9.40 +
    9.41 +lemma (in algebra) Int [intro]: 
    9.42 +  assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a \<inter> b \<in> sets M"
    9.43 +proof -
    9.44 +  have "((space M - a) \<union> (space M - b)) \<in> sets M" 
    9.45 +    by (metis a b compl_sets Un)
    9.46 +  moreover
    9.47 +  have "a \<inter> b = space M - ((space M - a) \<union> (space M - b))" 
    9.48 +    using space_closed a b
    9.49 +    by blast
    9.50 +  ultimately show ?thesis
    9.51 +    by (metis compl_sets)
    9.52 +qed
    9.53 +
    9.54 +lemma (in algebra) Diff [intro]: 
    9.55 +  assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a - b \<in> sets M"
    9.56 +proof -
    9.57 +  have "(a \<inter> (space M - b)) \<in> sets M"
    9.58 +    by (metis a b compl_sets Int)
    9.59 +  moreover
    9.60 +  have "a - b = (a \<inter> (space M - b))"
    9.61 +    by (metis Int_Diff Int_absorb1 Int_commute a sets_into_space)
    9.62 +  ultimately show ?thesis
    9.63 +    by metis
    9.64 +qed
    9.65 +
    9.66 +lemma (in algebra) finite_union [intro]: 
    9.67 +  "finite X \<Longrightarrow> X \<subseteq> sets M \<Longrightarrow> Union X \<in> sets M"
    9.68 +  by (induct set: finite) (auto simp add: Un) 
    9.69 +
    9.70 +
    9.71 +subsection {* Sigma Algebras *}
    9.72 +
    9.73 +locale sigma_algebra = algebra +
    9.74 +  assumes countable_UN [intro]:
    9.75 +         "!!A. range A \<subseteq> sets M \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
    9.76 +
    9.77 +lemma (in sigma_algebra) countable_INT:
    9.78 +  assumes a: "range a \<subseteq> sets M"
    9.79 +  shows "(\<Inter>i::nat. a i) \<in> sets M"
    9.80 +proof -
    9.81 +  have "space M - (\<Union>i. space M - a i) \<in> sets M" using a
    9.82 +    by (blast intro: countable_UN compl_sets a) 
    9.83 +  moreover
    9.84 +  have "(\<Inter>i. a i) = space M - (\<Union>i. space M - a i)" using space_closed a 
    9.85 +    by blast
    9.86 +  ultimately show ?thesis by metis
    9.87 +qed
    9.88 +
    9.89 +
    9.90 +lemma algebra_Pow:
    9.91 +     "algebra (| space = sp, sets = Pow sp |)"
    9.92 +  by (auto simp add: algebra_def) 
    9.93 +
    9.94 +lemma sigma_algebra_Pow:
    9.95 +     "sigma_algebra (| space = sp, sets = Pow sp |)"
    9.96 +  by (auto simp add: sigma_algebra_def sigma_algebra_axioms_def algebra_Pow) 
    9.97 +
    9.98 +subsection {* Binary Unions *}
    9.99 +
   9.100 +definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
   9.101 +  where "binary a b =  (\<lambda>\<^isup>x. b)(0 := a)"
   9.102 +
   9.103 +lemma range_binary_eq: "range(binary a b) = {a,b}" 
   9.104 +  by (auto simp add: binary_def)  
   9.105 +
   9.106 +lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)" 
   9.107 +  by (simp add: UNION_eq_Union_image range_binary_eq) 
   9.108 +
   9.109 +lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)" 
   9.110 +  by (simp add: INTER_eq_Inter_image range_binary_eq) 
   9.111 +
   9.112 +lemma sigma_algebra_iff: 
   9.113 +     "sigma_algebra M \<longleftrightarrow> 
   9.114 +      algebra M & (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
   9.115 +  by (simp add: sigma_algebra_def sigma_algebra_axioms_def) 
   9.116 +
   9.117 +lemma sigma_algebra_iff2:
   9.118 +     "sigma_algebra M \<longleftrightarrow>
   9.119 +       sets M \<subseteq> Pow (space M) &
   9.120 +       {} \<in> sets M & (\<forall>s \<in> sets M. space M - s \<in> sets M) &
   9.121 +       (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
   9.122 +  by (force simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def
   9.123 +         algebra_def Un_range_binary) 
   9.124 +
   9.125 +
   9.126 +subsection {* Initial Sigma Algebra *}
   9.127 +
   9.128 +text {*Sigma algebras can naturally be created as the closure of any set of
   9.129 +  sets with regard to the properties just postulated.  *}
   9.130 +
   9.131 +inductive_set
   9.132 +  sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
   9.133 +  for sp :: "'a set" and A :: "'a set set"
   9.134 +  where
   9.135 +    Basic: "a \<in> A \<Longrightarrow> a \<in> sigma_sets sp A"
   9.136 +  | Empty: "{} \<in> sigma_sets sp A"
   9.137 +  | Compl: "a \<in> sigma_sets sp A \<Longrightarrow> sp - a \<in> sigma_sets sp A"
   9.138 +  | Union: "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Union>i. a i) \<in> sigma_sets sp A"
   9.139 +
   9.140 +
   9.141 +definition
   9.142 +  sigma  where
   9.143 +  "sigma sp A = (| space = sp, sets = sigma_sets sp A |)"
   9.144 +
   9.145 +
   9.146 +lemma space_sigma [simp]: "space (sigma X B) = X"
   9.147 +  by (simp add: sigma_def) 
   9.148 +
   9.149 +lemma sigma_sets_top: "sp \<in> sigma_sets sp A"
   9.150 +  by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty)
   9.151 +
   9.152 +lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp"
   9.153 +  by (erule sigma_sets.induct, auto) 
   9.154 +
   9.155 +lemma sigma_sets_Un: 
   9.156 +  "a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A"
   9.157 +apply (simp add: Un_range_binary range_binary_eq) 
   9.158 +apply (metis Union COMBK_def binary_def fun_upd_apply) 
   9.159 +done
   9.160 +
   9.161 +lemma sigma_sets_Inter:
   9.162 +  assumes Asb: "A \<subseteq> Pow sp"
   9.163 +  shows "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Inter>i. a i) \<in> sigma_sets sp A"
   9.164 +proof -
   9.165 +  assume ai: "\<And>i::nat. a i \<in> sigma_sets sp A"
   9.166 +  hence "\<And>i::nat. sp-(a i) \<in> sigma_sets sp A" 
   9.167 +    by (rule sigma_sets.Compl)
   9.168 +  hence "(\<Union>i. sp-(a i)) \<in> sigma_sets sp A" 
   9.169 +    by (rule sigma_sets.Union)
   9.170 +  hence "sp-(\<Union>i. sp-(a i)) \<in> sigma_sets sp A" 
   9.171 +    by (rule sigma_sets.Compl)
   9.172 +  also have "sp-(\<Union>i. sp-(a i)) = sp Int (\<Inter>i. a i)" 
   9.173 +    by auto
   9.174 +  also have "... = (\<Inter>i. a i)" using ai
   9.175 +    by (blast dest: sigma_sets_into_sp [OF Asb]) 
   9.176 +  finally show ?thesis . 
   9.177 +qed
   9.178 +
   9.179 +lemma sigma_sets_INTER:
   9.180 +  assumes Asb: "A \<subseteq> Pow sp" 
   9.181 +      and ai: "\<And>i::nat. i \<in> S \<Longrightarrow> a i \<in> sigma_sets sp A" and non: "S \<noteq> {}"
   9.182 +  shows "(\<Inter>i\<in>S. a i) \<in> sigma_sets sp A"
   9.183 +proof -
   9.184 +  from ai have "\<And>i. (if i\<in>S then a i else sp) \<in> sigma_sets sp A"
   9.185 +    by (simp add: sigma_sets.intros sigma_sets_top)
   9.186 +  hence "(\<Inter>i. (if i\<in>S then a i else sp)) \<in> sigma_sets sp A"
   9.187 +    by (rule sigma_sets_Inter [OF Asb])
   9.188 +  also have "(\<Inter>i. (if i\<in>S then a i else sp)) = (\<Inter>i\<in>S. a i)"
   9.189 +    by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+
   9.190 +  finally show ?thesis .
   9.191 +qed
   9.192 +
   9.193 +lemma (in sigma_algebra) sigma_sets_subset:
   9.194 +  assumes a: "a \<subseteq> sets M" 
   9.195 +  shows "sigma_sets (space M) a \<subseteq> sets M"
   9.196 +proof
   9.197 +  fix x
   9.198 +  assume "x \<in> sigma_sets (space M) a"
   9.199 +  from this show "x \<in> sets M"
   9.200 +    by (induct rule: sigma_sets.induct, auto) (metis a subsetD) 
   9.201 +qed
   9.202 +
   9.203 +lemma (in sigma_algebra) sigma_sets_eq:
   9.204 +     "sigma_sets (space M) (sets M) = sets M"
   9.205 +proof
   9.206 +  show "sets M \<subseteq> sigma_sets (space M) (sets M)"
   9.207 +    by (metis Set.subsetI sigma_sets.Basic space_closed)
   9.208 +  next
   9.209 +  show "sigma_sets (space M) (sets M) \<subseteq> sets M"
   9.210 +    by (metis sigma_sets_subset subset_refl)
   9.211 +qed
   9.212 +
   9.213 +lemma sigma_algebra_sigma_sets:
   9.214 +     "a \<subseteq> Pow (space M) \<Longrightarrow> sets M = sigma_sets (space M) a \<Longrightarrow> sigma_algebra M"
   9.215 +  apply (auto simp add: sigma_algebra_def sigma_algebra_axioms_def
   9.216 +      algebra_def sigma_sets.Empty sigma_sets.Compl sigma_sets_Un) 
   9.217 +  apply (blast dest: sigma_sets_into_sp)
   9.218 +  apply (blast intro: sigma_sets.intros) 
   9.219 +  done
   9.220 +
   9.221 +lemma sigma_algebra_sigma:
   9.222 +     "a \<subseteq> Pow X \<Longrightarrow> sigma_algebra (sigma X a)"
   9.223 +  apply (rule sigma_algebra_sigma_sets) 
   9.224 +  apply (auto simp add: sigma_def) 
   9.225 +  done
   9.226 +
   9.227 +lemma (in sigma_algebra) sigma_subset:
   9.228 +     "a \<subseteq> sets M ==> sets (sigma (space M) a) \<subseteq> (sets M)"
   9.229 +  by (simp add: sigma_def sigma_sets_subset)
   9.230 +
   9.231 +end
   9.232 +
    10.1 --- a/src/HOL/Product_Type.thy	Tue Oct 27 14:46:03 2009 +0000
    10.2 +++ b/src/HOL/Product_Type.thy	Wed Oct 28 11:42:31 2009 +0000
    10.3 @@ -927,6 +927,9 @@
    10.4     insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
    10.5  by blast
    10.6  
    10.7 +lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
    10.8 +  by (auto, rule_tac p = "f x" in PairE, auto)
    10.9 +
   10.10  subsubsection {* Code generator setup *}
   10.11  
   10.12  instance * :: (eq, eq) eq ..
    11.1 --- a/src/HOL/SEQ.thy	Tue Oct 27 14:46:03 2009 +0000
    11.2 +++ b/src/HOL/SEQ.thy	Wed Oct 28 11:42:31 2009 +0000
    11.3 @@ -205,6 +205,9 @@
    11.4    shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
    11.5  unfolding LIMSEQ_def dist_norm ..
    11.6  
    11.7 +lemma LIMSEQ_iff_nz: "X ----> L = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
    11.8 +  by (auto simp add: LIMSEQ_def) (metis Suc_leD zero_less_Suc)  
    11.9 +
   11.10  lemma LIMSEQ_Zseq_iff: "((\<lambda>n. X n) ----> L) = Zseq (\<lambda>n. X n - L)"
   11.11  by (simp only: LIMSEQ_iff Zseq_def)
   11.12  
    12.1 --- a/src/HOL/Series.thy	Tue Oct 27 14:46:03 2009 +0000
    12.2 +++ b/src/HOL/Series.thy	Wed Oct 28 11:42:31 2009 +0000
    12.3 @@ -10,7 +10,7 @@
    12.4  header{*Finite Summation and Infinite Series*}
    12.5  
    12.6  theory Series
    12.7 -imports SEQ
    12.8 +imports SEQ Deriv
    12.9  begin
   12.10  
   12.11  definition
   12.12 @@ -285,6 +285,26 @@
   12.13  text{*A summable series of positive terms has limit that is at least as
   12.14  great as any partial sum.*}
   12.15  
   12.16 +lemma pos_summable:
   12.17 +  fixes f:: "nat \<Rightarrow> real"
   12.18 +  assumes pos: "!!n. 0 \<le> f n" and le: "!!n. setsum f {0..<n} \<le> x"
   12.19 +  shows "summable f"
   12.20 +proof -
   12.21 +  have "convergent (\<lambda>n. setsum f {0..<n})" 
   12.22 +    proof (rule Bseq_mono_convergent)
   12.23 +      show "Bseq (\<lambda>n. setsum f {0..<n})"
   12.24 +	by (rule f_inc_g_dec_Beq_f [of "(\<lambda>n. setsum f {0..<n})" "\<lambda>n. x"])
   12.25 +           (auto simp add: le pos)  
   12.26 +    next 
   12.27 +      show "\<forall>m n. m \<le> n \<longrightarrow> setsum f {0..<m} \<le> setsum f {0..<n}"
   12.28 +	by (auto intro: setsum_mono2 pos) 
   12.29 +    qed
   12.30 +  then obtain L where "(%n. setsum f {0..<n}) ----> L"
   12.31 +    by (blast dest: convergentD)
   12.32 +  thus ?thesis
   12.33 +    by (force simp add: summable_def sums_def) 
   12.34 +qed
   12.35 +
   12.36  lemma series_pos_le:
   12.37    fixes f :: "nat \<Rightarrow> real"
   12.38    shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 \<le> f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} \<le> suminf f"
   12.39 @@ -361,6 +381,19 @@
   12.40    shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
   12.41  by (rule geometric_sums [THEN sums_summable])
   12.42  
   12.43 +lemma half: "0 < 1 / (2::'a::{number_ring,division_by_zero,ordered_field})"
   12.44 +  by arith 
   12.45 +
   12.46 +lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1"
   12.47 +proof -
   12.48 +  have 2: "(\<lambda>n. (1/2::real)^n) sums 2" using geometric_sums [of "1/2::real"]
   12.49 +    by auto
   12.50 +  have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)"
   12.51 +    by simp
   12.52 +  thus ?thesis using divide.sums [OF 2, of 2]
   12.53 +    by simp
   12.54 +qed
   12.55 +
   12.56  text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
   12.57  
   12.58  lemma summable_convergent_sumr_iff:
    13.1 --- a/src/HOL/SupInf.thy	Tue Oct 27 14:46:03 2009 +0000
    13.2 +++ b/src/HOL/SupInf.thy	Wed Oct 28 11:42:31 2009 +0000
    13.3 @@ -361,11 +361,6 @@
    13.4    shows "Inf (insert a X) = (if X={} then a else min a (Inf X))"
    13.5  by auto (metis Inf_insert_nonempty z) 
    13.6  
    13.7 -text{*We could prove the analogous result for the supremum, and also generalise it to the union operator.*}
    13.8 -lemma Inf_binary:
    13.9 -  "Inf{a, b::real} = min a b"
   13.10 -  by (subst Inf_insert_nonempty, auto)
   13.11 -
   13.12  lemma Inf_greater:
   13.13    fixes z :: real
   13.14    shows "X \<noteq> {} \<Longrightarrow>  Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
   13.15 @@ -437,7 +432,7 @@
   13.16      by (simp add: Inf_real_def)
   13.17  qed
   13.18  
   13.19 -subsection{*Relate max and min to sup and inf.*}
   13.20 +subsection{*Relate max and min to Sup and Inf.*}
   13.21  
   13.22  lemma real_max_Sup:
   13.23    fixes x :: real