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.13        by (simp add: emeasure_eq_measure)
    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))"
    1.59          by (simp add: setsum.distrib)
    1.60 -      also have "\<dots> \<le> (\<Sum>i = 0..<n0. measure M (K i)) +  e / 2" using `0 < e`
    1.61 +      also have "\<dots> \<le> (\<Sum>i<n0. measure M (K i)) +  e / 2" using `0 < e`
    1.62          by (auto simp: real_of_nat_def[symmetric] field_simps intro!: mult_left_mono)
    1.63        finally
    1.64 -      have "measure M (\<Union>i. D i) < (\<Sum>i = 0..<n0. measure M (K i)) + e / 2 + e / 2"
    1.65 +      have "measure M (\<Union>i. D i) < (\<Sum>i<n0. measure M (K i)) + e / 2 + e / 2"
    1.66          by auto
    1.67        hence "M (\<Union>i. D i) < M ?K + e" by (auto simp: mK emeasure_eq_measure)
    1.68        moreover