src/HOL/Probability/Regularity.thy
 changeset 56193 c726ecfb22b6 parent 56166 9a241bc276cd child 56212 3253aaf73a01
```     1.1 --- a/src/HOL/Probability/Regularity.thy	Tue Mar 18 14:32:23 2014 +0100
1.2 +++ b/src/HOL/Probability/Regularity.thy	Tue Mar 18 15:53:48 2014 +0100
1.3 @@ -351,9 +351,9 @@
1.4      case (union D)
1.5      then have "range D \<subseteq> sets M" by (auto simp: sb borel_eq_closed)
1.6      with union have M[symmetric]: "(\<Sum>i. M (D i)) = M (\<Union>i. D i)" by (intro suminf_emeasure)
1.7 -    also have "(\<lambda>n. \<Sum>i\<in>{0..<n}. M (D i)) ----> (\<Sum>i. M (D i))"
1.8 -      by (intro summable_sumr_LIMSEQ_suminf summable_ereal_pos emeasure_nonneg)
1.9 -    finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i = 0..<n. measure M (D i)) ----> measure M (\<Union>i. D i)"
1.10 +    also have "(\<lambda>n. \<Sum>i<n. M (D i)) ----> (\<Sum>i. M (D i))"
1.11 +      by (intro summable_LIMSEQ summable_ereal_pos emeasure_nonneg)
1.12 +    finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i<n. measure M (D i)) ----> measure M (\<Union>i. D i)"
1.14      have "(\<Union>i. D i) \<in> sets M" using `range D \<subseteq> sets M` by auto
1.15
1.16 @@ -362,18 +362,17 @@
1.17      proof (rule approx_inner)
1.18        fix e::real assume "e > 0"
1.19        with measure_LIMSEQ
1.20 -      have "\<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>i = 0..<n. measure M (D i)) -measure M (\<Union>x. D x)\<bar> < e/2"
1.21 +      have "\<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>i<n. measure M (D i)) -measure M (\<Union>x. D x)\<bar> < e/2"
1.22          by (auto simp: LIMSEQ_def dist_real_def simp del: less_divide_eq_numeral1)
1.23 -      hence "\<exists>n0. \<bar>(\<Sum>i = 0..<n0. measure M (D i)) - measure M (\<Union>x. D x)\<bar> < e/2" by auto
1.24 -      then obtain n0 where n0: "\<bar>(\<Sum>i = 0..<n0. measure M (D i)) - measure M (\<Union>i. D i)\<bar> < e/2"
1.25 +      hence "\<exists>n0. \<bar>(\<Sum>i<n0. measure M (D i)) - measure M (\<Union>x. D x)\<bar> < e/2" by auto
1.26 +      then obtain n0 where n0: "\<bar>(\<Sum>i<n0. measure M (D i)) - measure M (\<Union>i. D i)\<bar> < e/2"
1.27          unfolding choice_iff by blast
1.28 -      have "ereal (\<Sum>i = 0..<n0. measure M (D i)) = (\<Sum>i = 0..<n0. M (D i))"
1.29 +      have "ereal (\<Sum>i<n0. measure M (D i)) = (\<Sum>i<n0. M (D i))"
1.30          by (auto simp add: emeasure_eq_measure)
1.31 -      also have "\<dots> = (\<Sum>i<n0. M (D i))" by (rule setsum_cong) auto
1.32        also have "\<dots> \<le> (\<Sum>i. M (D i))" by (rule suminf_upper) (auto simp: emeasure_nonneg)
1.33        also have "\<dots> = M (\<Union>i. D i)" by (simp add: M)
1.34        also have "\<dots> = measure M (\<Union>i. D i)" by (simp add: emeasure_eq_measure)
1.35 -      finally have n0: "measure M (\<Union>i. D i) - (\<Sum>i = 0..<n0. measure M (D i)) < e/2"
1.36 +      finally have n0: "measure M (\<Union>i. D i) - (\<Sum>i<n0. measure M (D i)) < e/2"
1.37          using n0 by auto
1.38        have "\<forall>i. \<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)"
1.39        proof
1.40 @@ -388,20 +387,20 @@
1.41        then obtain K where K: "\<And>i. K i \<subseteq> D i" "\<And>i. compact (K i)"
1.42          "\<And>i. emeasure M (D i) \<le> emeasure M (K i) + e/(2*Suc n0)"
1.43          unfolding choice_iff by blast
1.44 -      let ?K = "\<Union>i\<in>{0..<n0}. K i"
1.45 -      have "disjoint_family_on K {0..<n0}" using K `disjoint_family D`
1.46 +      let ?K = "\<Union>i\<in>{..<n0}. K i"
1.47 +      have "disjoint_family_on K {..<n0}" using K `disjoint_family D`
1.48          unfolding disjoint_family_on_def by blast
1.49 -      hence mK: "measure M ?K = (\<Sum>i = 0..<n0. measure M (K i))" using K
1.50 +      hence mK: "measure M ?K = (\<Sum>i<n0. measure M (K i))" using K
1.51          by (intro finite_measure_finite_Union) (auto simp: sb compact_imp_closed)
1.52 -      have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (D i)) + e/2" using n0 by simp
1.53 -      also have "(\<Sum>i = 0..<n0. measure M (D i)) \<le> (\<Sum>i = 0..<n0. measure M (K i) + e/(2*Suc n0))"
1.54 +      have "measure M (\<Union>i. D i) < (\<Sum>i<n0. measure M (D i)) + e/2" using n0 by simp
1.55 +      also have "(\<Sum>i<n0. measure M (D i)) \<le> (\<Sum>i<n0. measure M (K i) + e/(2*Suc n0))"
1.56          using K by (auto intro: setsum_mono simp: emeasure_eq_measure)
1.57 -      also have "\<dots> = (\<Sum>i = 0..<n0. measure M (K i)) + (\<Sum>i = 0..<n0. e/(2*Suc n0))"
1.58 +      also have "\<dots> = (\<Sum>i<n0. measure M (K i)) + (\<Sum>i<n0. e/(2*Suc n0))"