src/HOL/Probability/Caratheodory.thy
 changeset 33536 fd28b7399f2b parent 33271 7be66dee1a5a child 35582 b16d99a72dc9
```     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Mon Nov 09 16:06:08 2009 +0000
1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Mon Nov 09 19:42:33 2009 +0100
1.3 @@ -2,7 +2,6 @@
1.4
1.5  theory Caratheodory
1.6    imports Sigma_Algebra SupInf SeriesPlus
1.7 -
1.8  begin
1.9
1.10  text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
1.11 @@ -136,7 +135,7 @@
1.12      proof
1.13        fix n
1.14        show "(\<Sum>i\<Colon>nat = 0\<Colon>nat..<Suc (Suc n). f (binaryset A B i)) = f A + f B"
1.15 -	by (induct n)  (auto simp add: binaryset_def f)
1.16 +        by (induct n)  (auto simp add: binaryset_def f)
1.17      qed
1.18    moreover
1.19    have "... ----> f A + f B" by (rule LIMSEQ_const)
1.20 @@ -198,30 +197,30 @@
1.21    proof -
1.22      from xl yl show ?thesis
1.23        proof (auto simp add: positive_def lambda_system_eq Int)
1.24 -	fix u
1.25 -	assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M"
1.26 +        fix u
1.27 +        assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M"
1.28             and fx: "\<forall>z\<in>sets M. f (z \<inter> x) + f (z - x) = f z"
1.29             and fy: "\<forall>z\<in>sets M. f (z \<inter> y) + f (z - y) = f z"
1.30 -	have "u - x \<inter> y \<in> sets M"
1.31 -	  by (metis Diff Diff_Int Un u x y)
1.32 -	moreover
1.33 -	have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
1.34 -	moreover
1.35 -	have "u - x \<inter> y - y = u - y" by blast
1.36 -	ultimately
1.37 -	have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
1.38 -	  by force
1.39 -	have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y)
1.40 +        have "u - x \<inter> y \<in> sets M"
1.41 +          by (metis Diff Diff_Int Un u x y)
1.42 +        moreover
1.43 +        have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
1.44 +        moreover
1.45 +        have "u - x \<inter> y - y = u - y" by blast
1.46 +        ultimately
1.47 +        have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
1.48 +          by force
1.49 +        have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y)
1.50                = (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)"
1.51 -	  by (simp add: ey)
1.52 -	also have "... =  (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
1.53 -	  by (simp add: Int_ac)
1.54 -	also have "... = f (u \<inter> y) + f (u - y)"
1.55 -	  using fx [THEN bspec, of "u \<inter> y"] Int y u
1.56 -	  by force
1.57 -	also have "... = f u"
1.58 -	  by (metis fy u)
1.59 -	finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
1.60 +          by (simp add: ey)
1.61 +        also have "... =  (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
1.62 +          by (simp add: Int_ac)
1.63 +        also have "... = f (u \<inter> y) + f (u - y)"
1.64 +          using fx [THEN bspec, of "u \<inter> y"] Int y u
1.65 +          by force
1.66 +        also have "... = f u"
1.67 +          by (metis fy u)
1.68 +        finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
1.69        qed
1.70    qed
1.71
1.72 @@ -478,11 +477,11 @@
1.73    have U_eq: "f (\<Union>i. A i) = suminf (f o A)"
1.74      proof (rule antisym)
1.75        show "f (\<Union>i. A i) \<le> suminf (f \<circ> A)"
1.76 -	by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA])
1.77 +        by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA])
1.78        show "suminf (f \<circ> A) \<le> f (\<Union>i. A i)"
1.79 -	by (rule suminf_le [OF sumfA])
1.80 +        by (rule suminf_le [OF sumfA])
1.81             (metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right
1.82 -	          lambda_system_positive lambda_system_additive
1.83 +                  lambda_system_positive lambda_system_additive
1.84                    subset_Un_eq increasingD [OF inc] A' A'' UNION_in_sets U_in)
1.85      qed
1.86    {
1.87 @@ -491,58 +490,58 @@
1.88      have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
1.89      proof -
1.90        have summ: "summable (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)" using pos A''
1.91 -	apply -
1.92 -	apply (rule summable_comparison_test [OF _ sumfA])
1.93 -	apply (rule_tac x="0" in exI)
1.94 -	apply (simp add: positive_def)
1.95 -	apply (auto simp add: )
1.96 -	apply (subst abs_of_nonneg)
1.97 -	apply (metis A'' Int UNIV_I a image_subset_iff)
1.98 -	apply (blast intro:  increasingD [OF inc] a)
1.99 -	done
1.100 +        apply -
1.101 +        apply (rule summable_comparison_test [OF _ sumfA])
1.102 +        apply (rule_tac x="0" in exI)
1.103 +        apply (simp add: positive_def)
1.104 +        apply (auto simp add: )
1.105 +        apply (subst abs_of_nonneg)
1.106 +        apply (metis A'' Int UNIV_I a image_subset_iff)
1.107 +        apply (blast intro:  increasingD [OF inc] a)
1.108 +        done
1.109        show ?thesis
1.110        proof (rule antisym)
1.111 -	have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
1.112 -	  by blast
1.113 -	moreover
1.114 -	have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
1.115 -	  by (auto simp add: disjoint_family_def)
1.116 -	moreover
1.117 -	have "a \<inter> (\<Union>i. A i) \<in> sets M"
1.118 -	  by (metis Int U_in a)
1.119 -	ultimately
1.120 -	have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
1.121 -	  using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ
1.122 -	  by (simp add: o_def)
1.123 -	moreover
1.124 -	have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)  \<le> f a - f (a - (\<Union>i. A i))"
1.125 -	  proof (rule suminf_le [OF summ])
1.126 -	    fix n
1.127 -	    have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
1.128 -	      by (metis A'' UNION_in_sets)
1.129 -	    have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
1.130 -	      by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a)
1.131 -	    have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
1.132 -	      using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]]
1.133 -	      by (simp add: A)
1.134 -	    hence eq_fa: "f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i)) = f a"
1.135 -	      by (simp add: lambda_system_eq UNION_in Diff_Compl a)
1.136 -	    have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
1.137 -	      by (blast intro: increasingD [OF inc] Diff UNION_eq_Union_image
1.138 +        have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
1.139 +          by blast
1.140 +        moreover
1.141 +        have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
1.142 +          by (auto simp add: disjoint_family_def)
1.143 +        moreover
1.144 +        have "a \<inter> (\<Union>i. A i) \<in> sets M"
1.145 +          by (metis Int U_in a)
1.146 +        ultimately
1.147 +        have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
1.148 +          using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ
1.149 +          by (simp add: o_def)
1.150 +        moreover
1.151 +        have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)  \<le> f a - f (a - (\<Union>i. A i))"
1.152 +          proof (rule suminf_le [OF summ])
1.153 +            fix n
1.154 +            have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
1.155 +              by (metis A'' UNION_in_sets)
1.156 +            have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
1.157 +              by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a)
1.158 +            have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
1.159 +              using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]]
1.160 +              by (simp add: A)
1.161 +            hence eq_fa: "f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i)) = f a"
1.162 +              by (simp add: lambda_system_eq UNION_in Diff_Compl a)
1.163 +            have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
1.164 +              by (blast intro: increasingD [OF inc] Diff UNION_eq_Union_image
1.165                                 UNION_in U_in a)
1.166 -	    thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>i. A i))"
1.167 -	      using eq_fa
1.168 -	      by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos
1.169 +            thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>i. A i))"
1.170 +              using eq_fa
1.171 +              by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos
1.172                              a A disj)
1.173 -	  qed
1.174 -	ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a"
1.175 -	  by arith
1.176 +          qed
1.177 +        ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a"
1.178 +          by arith
1.179        next
1.180 -	have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))"
1.181 -	  by (blast intro:  increasingD [OF inc] a U_in)
1.182 -	also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
1.183 -	  by (blast intro: subadditiveD [OF sa] Int Diff U_in)
1.184 -	finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
1.185 +        have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))"
1.186 +          by (blast intro:  increasingD [OF inc] a U_in)
1.187 +        also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
1.188 +          by (blast intro: subadditiveD [OF sa] Int Diff U_in)
1.189 +        finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
1.190          qed
1.191       qed
1.192    }
1.193 @@ -654,20 +653,20 @@
1.194    have sums: "(\<lambda>i. f (A i \<inter> s)) sums f (\<Union>i. A i \<inter> s)"
1.195      proof (rule countably_additiveD [OF ca])
1.196        show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s
1.197 -	by blast
1.198 +        by blast
1.199        show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
1.200 -	by (auto simp add: disjoint_family_def)
1.201 +        by (auto simp add: disjoint_family_def)
1.202        show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s
1.203 -	by (metis UN_extend_simps(4) s seq)
1.204 +        by (metis UN_extend_simps(4) s seq)
1.205      qed
1.206    hence "f s = suminf (\<lambda>i. f (A i \<inter> s))"
1.207      by (metis Int_commute UN_simps(4) seq sums_iff)
1.208    also have "... \<le> suminf (f \<circ> A)"
1.209      proof (rule summable_le [OF _ _ sm])
1.210        show "\<forall>n. f (A n \<inter> s) \<le> (f \<circ> A) n" using A s
1.211 -	by (force intro: increasingD [OF inc])
1.212 +        by (force intro: increasingD [OF inc])
1.213        show "summable (\<lambda>i. f (A i \<inter> s))" using sums
1.214 -	by (simp add: sums_iff)
1.215 +        by (simp add: sums_iff)
1.216      qed
1.217    also have "... = z" by (rule si)
1.218    finally show "f s \<le> z" .
1.219 @@ -722,9 +721,9 @@
1.220      proof (auto)
1.221        fix n
1.222        have "\<bar>f (disjointed A n)\<bar> = f (disjointed A n)" using posf dA
1.223 -	by (auto simp add: positive_def image_subset_iff)
1.224 +        by (auto simp add: positive_def image_subset_iff)
1.225        also have "... \<le> f (A n)"
1.226 -	by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
1.227 +        by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
1.228        finally show "\<bar>f (disjointed A n)\<bar> \<le> f (A n)" .
1.229      qed
1.230    from Series.summable_le2 [OF this sm]
1.231 @@ -787,32 +786,32 @@
1.232          and ll: "!!n. ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
1.233        by auto blast
1.234      have llpos: "!!n. 0 \<le> ll n"
1.235 -	by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero
1.236 +        by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero
1.237                range_subsetD BB)
1.238      have sll: "summable ll &
1.239                 suminf ll \<le> suminf (\<lambda>n. Inf (measure_set M f (A n))) + e"
1.240        proof -
1.241 -	have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)"
1.242 -	  by (rule sums_mult [OF power_half_series])
1.243 -	hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)"
1.244 -	  and eqe:  "(\<Sum>n. e * (1 / 2) ^ n / 2) = e"
1.245 -	  by (auto simp add: sums_iff)
1.246 -	have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) +
1.247 +        have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)"
1.248 +          by (rule sums_mult [OF power_half_series])
1.249 +        hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)"
1.250 +          and eqe:  "(\<Sum>n. e * (1 / 2) ^ n / 2) = e"
1.251 +          by (auto simp add: sums_iff)
1.252 +        have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) +
1.253                   suminf (\<lambda>n. e * (1/2)^(Suc n)) =
1.254                   suminf (\<lambda>n. Inf (measure_set M f (A n)) + e * (1/2)^(Suc n))"
1.255 -	  by (rule suminf_add [OF sum1 sum0])
1.256 -	have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n"
1.257 -	  by (metis ll llpos abs_of_nonneg)
1.258 -	have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))"
1.259 -	  by (rule summable_add [OF sum1 sum0])
1.260 -	have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)"
1.261 -	  using Series.summable_le2 [OF 1 2] by auto
1.262 -	also have "... = (\<Sum>n. Inf (measure_set M f (A n))) +
1.263 +          by (rule suminf_add [OF sum1 sum0])
1.264 +        have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n"
1.265 +          by (metis ll llpos abs_of_nonneg)
1.266 +        have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))"
1.267 +          by (rule summable_add [OF sum1 sum0])
1.268 +        have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)"
1.269 +          using Series.summable_le2 [OF 1 2] by auto
1.270 +        also have "... = (\<Sum>n. Inf (measure_set M f (A n))) +
1.271                           (\<Sum>n. e * (1 / 2) ^ Suc n)"
1.272 -	  by (metis 0)
1.273 -	also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + e"
1.274 -	  by (simp add: eqe)
1.275 -	finally show ?thesis using  Series.summable_le2 [OF 1 2] by auto
1.276 +          by (metis 0)
1.277 +        also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + e"
1.278 +          by (simp add: eqe)
1.279 +        finally show ?thesis using  Series.summable_le2 [OF 1 2] by auto
1.280        qed
1.281      def C \<equiv> "(split BB) o nat_to_nat2"
1.282      have C: "!!n. C n \<in> sets M"
1.283 @@ -822,24 +821,24 @@
1.284        done
1.285      have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
1.286        proof (auto simp add: C_def)
1.287 -	fix x i
1.288 -	assume x: "x \<in> A i"
1.289 -	with sbBB [of i] obtain j where "x \<in> BB i j"
1.290 -	  by blast
1.291 -	thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
1.292 -	  by (metis nat_to_nat2_surj internal_split_def prod.cases
1.293 +        fix x i
1.294 +        assume x: "x \<in> A i"
1.295 +        with sbBB [of i] obtain j where "x \<in> BB i j"
1.296 +          by blast
1.297 +        thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
1.298 +          by (metis nat_to_nat2_surj internal_split_def prod.cases
1.299                  prod_case_split surj_f_inv_f)
1.300        qed
1.301      have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> nat_to_nat2"
1.302        by (rule ext)  (auto simp add: C_def)
1.303      also have "... sums suminf ll"
1.304        proof (rule suminf_2dimen)
1.305 -	show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB
1.306 -	  by (force simp add: positive_def)
1.307 -	show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB
1.308 -	  by (force simp add: o_def)
1.309 -	show "summable ll" using sll
1.310 -	  by auto
1.311 +        show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB
1.312 +          by (force simp add: positive_def)
1.313 +        show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB
1.314 +          by (force simp add: o_def)
1.315 +        show "summable ll" using sll
1.316 +          by auto
1.317        qed
1.318      finally have Csums: "(f \<circ> C) sums suminf ll" .
1.319      have "Inf (measure_set M f (\<Union>i. A i)) \<le> suminf ll"
1.320 @@ -882,24 +881,24 @@
1.321        from inf_measure_close [OF posf e s]
1.322        obtain A l where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
1.323                     and sUN: "s \<subseteq> (\<Union>i. A i)" and fsums: "(f \<circ> A) sums l"
1.324 -	           and l: "l \<le> Inf (measure_set M f s) + e"
1.325 -	by auto
1.326 +                   and l: "l \<le> Inf (measure_set M f s) + e"
1.327 +        by auto
1.328        have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
1.329                        (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
1.330 -	by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
1.331 +        by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
1.332        have  [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)"
1.333 -	by (subst additiveD [OF add, symmetric])
1.334 - 	   (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
1.335 +        by (subst additiveD [OF add, symmetric])
1.336 +           (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
1.337        have fsumb: "summable (f \<circ> A)"
1.338 -	by (metis fsums sums_iff)
1.339 +        by (metis fsums sums_iff)
1.340        { fix u
1.341 -	assume u: "u \<in> sets M"
1.342 -	have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> f (A n)"
1.343 -	  by (simp add: positive_imp_pos [OF posf]  increasingD [OF inc]
1.344 +        assume u: "u \<in> sets M"
1.345 +        have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> f (A n)"
1.346 +          by (simp add: positive_imp_pos [OF posf]  increasingD [OF inc]
1.347                          u Int  range_subsetD [OF A])
1.348 -	have 1: "summable (f o (\<lambda>z. z\<inter>u) o A)"
1.349 +        have 1: "summable (f o (\<lambda>z. z\<inter>u) o A)"
1.350            by (rule summable_comparison_test [OF _ fsumb]) simp
1.351 -	have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)"
1.352 +        have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)"
1.353            proof (rule Inf_lower)
1.354              show "suminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)"
1.355                apply (simp add: measure_set_def)
1.356 @@ -920,14 +919,14 @@
1.357          and sum2: "summable (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
1.358          and inf2: "Inf (measure_set M f (s \<inter> (space M - x)))
1.359                     \<le> suminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
1.360 -	by (metis Diff lesum top x)+
1.361 +        by (metis Diff lesum top x)+
1.362        hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
1.363             \<le> suminf (f o (\<lambda>s. s\<inter>x) o A) + suminf (f o (\<lambda>s. s-x) o A)"
1.364 -	by (simp add: x)
1.365 +        by (simp add: x)
1.366        also have "... \<le> suminf (f o A)" using suminf_add [OF sum1 sum2]
1.367 -	by (simp add: x) (simp add: o_def)
1.368 +        by (simp add: x) (simp add: o_def)
1.369        also have "... \<le> Inf (measure_set M f s) + e"
1.370 -	by (metis fsums l sums_unique)
1.371 +        by (metis fsums l sums_unique)
1.372        finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
1.373          \<le> Inf (measure_set M f s) + e" .
1.374      qed
1.375 @@ -940,7 +939,7 @@
1.376      also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
1.377        apply (rule subadditiveD)