summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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