diff -r d666cb0e4cf9 -r c726ecfb22b6 src/HOL/Probability/Regularity.thy --- a/src/HOL/Probability/Regularity.thy Tue Mar 18 14:32:23 2014 +0100 +++ b/src/HOL/Probability/Regularity.thy Tue Mar 18 15:53:48 2014 +0100 @@ -351,9 +351,9 @@ case (union D) then have "range D \ sets M" by (auto simp: sb borel_eq_closed) with union have M[symmetric]: "(\i. M (D i)) = M (\i. D i)" by (intro suminf_emeasure) - also have "(\n. \i\{0.. (\i. M (D i))" - by (intro summable_sumr_LIMSEQ_suminf summable_ereal_pos emeasure_nonneg) - finally have measure_LIMSEQ: "(\n. \i = 0.. measure M (\i. D i)" + also have "(\n. \i (\i. M (D i))" + by (intro summable_LIMSEQ summable_ereal_pos emeasure_nonneg) + finally have measure_LIMSEQ: "(\n. \i measure M (\i. D i)" by (simp add: emeasure_eq_measure) have "(\i. D i) \ sets M" using `range D \ sets M` by auto @@ -362,18 +362,17 @@ proof (rule approx_inner) fix e::real assume "e > 0" with measure_LIMSEQ - have "\no. \n\no. \(\i = 0..x. D x)\ < e/2" + have "\no. \n\no. \(\ix. D x)\ < e/2" by (auto simp: LIMSEQ_def dist_real_def simp del: less_divide_eq_numeral1) - hence "\n0. \(\i = 0..x. D x)\ < e/2" by auto - then obtain n0 where n0: "\(\i = 0..i. D i)\ < e/2" + hence "\n0. \(\ix. D x)\ < e/2" by auto + then obtain n0 where n0: "\(\ii. D i)\ < e/2" unfolding choice_iff by blast - have "ereal (\i = 0..i = 0..ii = (\i \ (\i. M (D i))" by (rule suminf_upper) (auto simp: emeasure_nonneg) also have "\ = M (\i. D i)" by (simp add: M) also have "\ = measure M (\i. D i)" by (simp add: emeasure_eq_measure) - finally have n0: "measure M (\i. D i) - (\i = 0..i. D i) - (\ii. \K. K \ D i \ compact K \ emeasure M (D i) \ emeasure M K + e/(2*Suc n0)" proof @@ -388,20 +387,20 @@ then obtain K where K: "\i. K i \ D i" "\i. compact (K i)" "\i. emeasure M (D i) \ emeasure M (K i) + e/(2*Suc n0)" unfolding choice_iff by blast - let ?K = "\i\{0..i = 0..ii. D i) < (\i = 0..i = 0.. (\i = 0..i. D i) < (\ii (\i = (\i = 0..i = 0.. = (\ii \ (\i = 0.. \ (\ii. D i) < (\i = 0..i. D i) < (\ii. D i) < M ?K + e" by (auto simp: mK emeasure_eq_measure) moreover