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\{..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