1030 apply (rule p open_interior ballI)+ |
1030 apply (rule p open_interior ballI)+ |
1031 proof (assumption, rule) |
1031 proof (assumption, rule) |
1032 fix k |
1032 fix k |
1033 assume k: "k\<in>p" |
1033 assume k: "k\<in>p" |
1034 have *: "\<And>u t s. u \<subseteq> s \<Longrightarrow> s \<inter> t = {} \<Longrightarrow> u \<inter> t = {}" by auto |
1034 have *: "\<And>u t s. u \<subseteq> s \<Longrightarrow> s \<inter> t = {} \<Longrightarrow> u \<inter> t = {}" by auto |
1035 show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<inter> interior k = {}" |
1035 show "interior (\<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)) \<inter> interior k = {}" |
1036 apply (rule *[of _ "interior (\<Union>(q k - {k}))"]) |
1036 apply (rule *[of _ "interior (\<Union>(q k - {k}))"]) |
1037 defer |
1037 defer |
1038 apply (subst Int_commute) |
1038 apply (subst Int_commute) |
1039 apply (rule inter_interior_unions_intervals) |
1039 apply (rule inter_interior_unions_intervals) |
1040 proof - |
1040 proof - |
1042 show "finite (q k - {k})" "open (interior k)" |
1042 show "finite (q k - {k})" "open (interior k)" |
1043 "\<forall>t\<in>q k - {k}. \<exists>a b. t = {a..b}" using qk by auto |
1043 "\<forall>t\<in>q k - {k}. \<exists>a b. t = {a..b}" using qk by auto |
1044 show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}" |
1044 show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}" |
1045 using qk(5) using q(2)[OF k] by auto |
1045 using qk(5) using q(2)[OF k] by auto |
1046 have *: "\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto |
1046 have *: "\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto |
1047 show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<subseteq> interior (\<Union>(q k - {k}))" |
1047 show "interior (\<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)) \<subseteq> interior (\<Union>(q k - {k}))" |
1048 apply (rule interior_mono *)+ |
1048 apply (rule interior_mono *)+ |
1049 using k by auto |
1049 using k by auto |
1050 qed |
1050 qed |
1051 qed |
1051 qed |
1052 qed auto |
1052 qed auto |
1129 using division_ofD[OF assms(2)] by auto |
1129 using division_ofD[OF assms(2)] by auto |
1130 |
1130 |
1131 lemma elementary_union_interval: assumes "p division_of \<Union>p" |
1131 lemma elementary_union_interval: assumes "p division_of \<Union>p" |
1132 obtains q where "q division_of ({a..b::'a::ordered_euclidean_space} \<union> \<Union>p)" proof- |
1132 obtains q where "q division_of ({a..b::'a::ordered_euclidean_space} \<union> \<Union>p)" proof- |
1133 note assm=division_ofD[OF assms] |
1133 note assm=division_ofD[OF assms] |
1134 have lem1:"\<And>f s. \<Union>\<Union> (f ` s) = \<Union>(\<lambda>x.\<Union>(f x)) ` s" by auto |
1134 have lem1:"\<And>f s. \<Union>\<Union> (f ` s) = \<Union>((\<lambda>x.\<Union>(f x)) ` s)" by auto |
1135 have lem2:"\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t |t. t \<in> f} = s \<union> \<Union>f" by auto |
1135 have lem2:"\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t |t. t \<in> f} = s \<union> \<Union>f" by auto |
1136 { presume "p={} \<Longrightarrow> thesis" "{a..b} = {} \<Longrightarrow> thesis" "{a..b} \<noteq> {} \<Longrightarrow> interior {a..b} = {} \<Longrightarrow> thesis" |
1136 { presume "p={} \<Longrightarrow> thesis" "{a..b} = {} \<Longrightarrow> thesis" "{a..b} \<noteq> {} \<Longrightarrow> interior {a..b} = {} \<Longrightarrow> thesis" |
1137 "p\<noteq>{} \<Longrightarrow> interior {a..b}\<noteq>{} \<Longrightarrow> {a..b} \<noteq> {} \<Longrightarrow> thesis" |
1137 "p\<noteq>{} \<Longrightarrow> interior {a..b}\<noteq>{} \<Longrightarrow> {a..b} \<noteq> {} \<Longrightarrow> thesis" |
1138 thus thesis by auto |
1138 thus thesis by auto |
1139 next assume as:"p={}" guess p apply(rule elementary_interval[of a b]) . |
1139 next assume as:"p={}" guess p apply(rule elementary_interval[of a b]) . |
1280 "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow> (x2,k2) \<in> s \<Longrightarrow> ~((x1,k1) = (x2,k2)) \<Longrightarrow> (interior(k1) \<inter> interior(k2) = {})" |
1280 "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow> (x2,k2) \<in> s \<Longrightarrow> ~((x1,k1) = (x2,k2)) \<Longrightarrow> (interior(k1) \<inter> interior(k2) = {})" |
1281 "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)" using assms unfolding tagged_division_of apply- by blast+ |
1281 "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)" using assms unfolding tagged_division_of apply- by blast+ |
1282 |
1282 |
1283 lemma division_of_tagged_division: assumes"s tagged_division_of i" shows "(snd ` s) division_of i" |
1283 lemma division_of_tagged_division: assumes"s tagged_division_of i" shows "(snd ` s) division_of i" |
1284 proof(rule division_ofI) note assm=tagged_division_ofD[OF assms] |
1284 proof(rule division_ofI) note assm=tagged_division_ofD[OF assms] |
1285 show "\<Union>snd ` s = i" "finite (snd ` s)" using assm by auto |
1285 show "\<Union>(snd ` s) = i" "finite (snd ` s)" using assm by auto |
1286 fix k assume k:"k \<in> snd ` s" then obtain xk where xk:"(xk, k) \<in> s" by auto |
1286 fix k assume k:"k \<in> snd ` s" then obtain xk where xk:"(xk, k) \<in> s" by auto |
1287 thus "k \<subseteq> i" "k \<noteq> {}" "\<exists>a b. k = {a..b}" using assm apply- by fastforce+ |
1287 thus "k \<subseteq> i" "k \<noteq> {}" "\<exists>a b. k = {a..b}" using assm apply- by fastforce+ |
1288 fix k' assume k':"k' \<in> snd ` s" "k \<noteq> k'" from this(1) obtain xk' where xk':"(xk', k') \<in> s" by auto |
1288 fix k' assume k':"k' \<in> snd ` s" "k \<noteq> k'" from this(1) obtain xk' where xk':"(xk', k') \<in> s" by auto |
1289 thus "interior k \<inter> interior k' = {}" apply-apply(rule assm(5)) apply(rule xk xk')+ using k' by auto |
1289 thus "interior k \<inter> interior k' = {}" apply-apply(rule assm(5)) apply(rule xk xk')+ using k' by auto |
1290 qed |
1290 qed |
1291 |
1291 |
1292 lemma partial_division_of_tagged_division: assumes "s tagged_partial_division_of i" |
1292 lemma partial_division_of_tagged_division: assumes "s tagged_partial_division_of i" |
1293 shows "(snd ` s) division_of \<Union>(snd ` s)" |
1293 shows "(snd ` s) division_of \<Union>(snd ` s)" |
1294 proof(rule division_ofI) note assm=tagged_partial_division_ofD[OF assms] |
1294 proof(rule division_ofI) note assm=tagged_partial_division_ofD[OF assms] |
1295 show "finite (snd ` s)" "\<Union>snd ` s = \<Union>snd ` s" using assm by auto |
1295 show "finite (snd ` s)" "\<Union>(snd ` s) = \<Union>(snd ` s)" using assm by auto |
1296 fix k assume k:"k \<in> snd ` s" then obtain xk where xk:"(xk, k) \<in> s" by auto |
1296 fix k assume k:"k \<in> snd ` s" then obtain xk where xk:"(xk, k) \<in> s" by auto |
1297 thus "k\<noteq>{}" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>snd ` s" using assm by auto |
1297 thus "k\<noteq>{}" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>(snd ` s)" using assm by auto |
1298 fix k' assume k':"k' \<in> snd ` s" "k \<noteq> k'" from this(1) obtain xk' where xk':"(xk', k') \<in> s" by auto |
1298 fix k' assume k':"k' \<in> snd ` s" "k \<noteq> k'" from this(1) obtain xk' where xk':"(xk', k') \<in> s" by auto |
1299 thus "interior k \<inter> interior k' = {}" apply-apply(rule assm(5)) apply(rule xk xk')+ using k' by auto |
1299 thus "interior k \<inter> interior k' = {}" apply-apply(rule assm(5)) apply(rule xk xk')+ using k' by auto |
1300 qed |
1300 qed |
1301 |
1301 |
1302 lemma tagged_partial_division_subset: assumes "s tagged_partial_division_of i" "t \<subseteq> s" |
1302 lemma tagged_partial_division_subset: assumes "s tagged_partial_division_of i" "t \<subseteq> s" |
1353 assumes "finite iset" "\<forall>i\<in>iset. (pfn(i) tagged_division_of i)" |
1353 assumes "finite iset" "\<forall>i\<in>iset. (pfn(i) tagged_division_of i)" |
1354 "\<forall>i1 \<in> iset. \<forall>i2 \<in> iset. ~(i1 = i2) \<longrightarrow> (interior(i1) \<inter> interior(i2) = {})" |
1354 "\<forall>i1 \<in> iset. \<forall>i2 \<in> iset. ~(i1 = i2) \<longrightarrow> (interior(i1) \<inter> interior(i2) = {})" |
1355 shows "\<Union>(pfn ` iset) tagged_division_of (\<Union>iset)" |
1355 shows "\<Union>(pfn ` iset) tagged_division_of (\<Union>iset)" |
1356 proof(rule tagged_division_ofI) |
1356 proof(rule tagged_division_ofI) |
1357 note assm = tagged_division_ofD[OF assms(2)[rule_format]] |
1357 note assm = tagged_division_ofD[OF assms(2)[rule_format]] |
1358 show "finite (\<Union>pfn ` iset)" apply(rule finite_Union) using assms by auto |
1358 show "finite (\<Union>(pfn ` iset))" apply(rule finite_Union) using assms by auto |
1359 have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>pfn ` iset} = \<Union>(\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` iset" by blast |
1359 have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>((\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` iset)" by blast |
1360 also have "\<dots> = \<Union>iset" using assm(6) by auto |
1360 also have "\<dots> = \<Union>iset" using assm(6) by auto |
1361 finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>pfn ` iset} = \<Union>iset" . |
1361 finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>iset" . |
1362 fix x k assume xk:"(x,k)\<in>\<Union>pfn ` iset" then obtain i where i:"i \<in> iset" "(x, k) \<in> pfn i" by auto |
1362 fix x k assume xk:"(x,k)\<in>\<Union>(pfn ` iset)" then obtain i where i:"i \<in> iset" "(x, k) \<in> pfn i" by auto |
1363 show "x\<in>k" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>iset" using assm(2-4)[OF i] using i(1) by auto |
1363 show "x\<in>k" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>iset" using assm(2-4)[OF i] using i(1) by auto |
1364 fix x' k' assume xk':"(x',k')\<in>\<Union>pfn ` iset" "(x, k) \<noteq> (x', k')" then obtain i' where i':"i' \<in> iset" "(x', k') \<in> pfn i'" by auto |
1364 fix x' k' assume xk':"(x',k')\<in>\<Union>(pfn ` iset)" "(x, k) \<noteq> (x', k')" then obtain i' where i':"i' \<in> iset" "(x', k') \<in> pfn i'" by auto |
1365 have *:"\<And>a b. i\<noteq>i' \<Longrightarrow> a\<subseteq> i \<Longrightarrow> b\<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}" using i(1) i'(1) |
1365 have *:"\<And>a b. i\<noteq>i' \<Longrightarrow> a\<subseteq> i \<Longrightarrow> b\<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}" using i(1) i'(1) |
1366 using assms(3)[rule_format] interior_mono by blast |
1366 using assms(3)[rule_format] interior_mono by blast |
1367 show "interior k \<inter> interior k' = {}" apply(cases "i=i'") |
1367 show "interior k \<inter> interior k' = {}" apply(cases "i=i'") |
1368 using assm(5)[OF i _ xk'(2)] i'(2) using assm(3)[OF i] assm(3)[OF i'] defer apply-apply(rule *) by auto |
1368 using assm(5)[OF i _ xk'(2)] i'(2) using assm(3)[OF i] assm(3)[OF i'] defer apply-apply(rule *) by auto |
1369 qed |
1369 qed |
4973 "(\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral({a..b}) f) < e)" |
4973 "(\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral({a..b}) f) < e)" |
4974 and p:"p tagged_partial_division_of {a..b}" "d fine p" |
4974 and p:"p tagged_partial_division_of {a..b}" "d fine p" |
4975 shows "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x - integral k f) p) \<le> e" (is "?x \<le> e") |
4975 shows "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x - integral k f) p) \<le> e" (is "?x \<le> e") |
4976 proof- { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" thus ?thesis by (blast intro: field_le_epsilon) } |
4976 proof- { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" thus ?thesis by (blast intro: field_le_epsilon) } |
4977 fix k::real assume k:"k>0" note p' = tagged_partial_division_ofD[OF p(1)] |
4977 fix k::real assume k:"k>0" note p' = tagged_partial_division_ofD[OF p(1)] |
4978 have "\<Union>snd ` p \<subseteq> {a..b}" using p'(3) by fastforce |
4978 have "\<Union>(snd ` p) \<subseteq> {a..b}" using p'(3) by fastforce |
4979 note partial_division_of_tagged_division[OF p(1)] this |
4979 note partial_division_of_tagged_division[OF p(1)] this |
4980 from partial_division_extend_interval[OF this] guess q . note q=this and q' = division_ofD[OF this(2)] |
4980 from partial_division_extend_interval[OF this] guess q . note q=this and q' = division_ofD[OF this(2)] |
4981 def r \<equiv> "q - snd ` p" have "snd ` p \<inter> r = {}" unfolding r_def by auto |
4981 def r \<equiv> "q - snd ` p" have "snd ` p \<inter> r = {}" unfolding r_def by auto |
4982 have r:"finite r" using q' unfolding r_def by auto |
4982 have r:"finite r" using q' unfolding r_def by auto |
4983 |
4983 |
4992 from this[rule_format,OF *] guess dd .. note dd=conjunctD2[OF this,rule_format] |
4992 from this[rule_format,OF *] guess dd .. note dd=conjunctD2[OF this,rule_format] |
4993 note gauge_inter[OF `gauge d` dd(1)] from fine_division_exists[OF this,of u v] guess qq . |
4993 note gauge_inter[OF `gauge d` dd(1)] from fine_division_exists[OF this,of u v] guess qq . |
4994 thus ?case apply(rule_tac x=qq in exI) using dd(2)[of qq] unfolding fine_inter uv by auto qed |
4994 thus ?case apply(rule_tac x=qq in exI) using dd(2)[of qq] unfolding fine_inter uv by auto qed |
4995 from bchoice[OF this] guess qq .. note qq=this[rule_format] |
4995 from bchoice[OF this] guess qq .. note qq=this[rule_format] |
4996 |
4996 |
4997 let ?p = "p \<union> \<Union>qq ` r" have "norm ((\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) - integral {a..b} f) < e" |
4997 let ?p = "p \<union> \<Union>(qq ` r)" have "norm ((\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) - integral {a..b} f) < e" |
4998 apply(rule assms(4)[rule_format]) |
4998 apply(rule assms(4)[rule_format]) |
4999 proof show "d fine ?p" apply(rule fine_union,rule p) apply(rule fine_unions) using qq by auto |
4999 proof show "d fine ?p" apply(rule fine_union,rule p) apply(rule fine_unions) using qq by auto |
5000 note * = tagged_partial_division_of_union_self[OF p(1)] |
5000 note * = tagged_partial_division_of_union_self[OF p(1)] |
5001 have "p \<union> \<Union>qq ` r tagged_division_of \<Union>snd ` p \<union> \<Union>r" |
5001 have "p \<union> \<Union>(qq ` r) tagged_division_of \<Union>(snd ` p) \<union> \<Union>r" |
5002 proof(rule tagged_division_union[OF * tagged_division_unions]) |
5002 proof(rule tagged_division_union[OF * tagged_division_unions]) |
5003 show "finite r" by fact case goal2 thus ?case using qq by auto |
5003 show "finite r" by fact case goal2 thus ?case using qq by auto |
5004 next case goal3 thus ?case apply(rule,rule,rule) apply(rule q'(5)) unfolding r_def by auto |
5004 next case goal3 thus ?case apply(rule,rule,rule) apply(rule q'(5)) unfolding r_def by auto |
5005 next case goal4 thus ?case apply(rule inter_interior_unions_intervals) apply(fact,rule) |
5005 next case goal4 thus ?case apply(rule inter_interior_unions_intervals) apply(fact,rule) |
5006 apply(rule,rule q') defer apply(rule,subst Int_commute) |
5006 apply(rule,rule q') defer apply(rule,subst Int_commute) |
5007 apply(rule inter_interior_unions_intervals) apply(rule finite_imageI,rule p',rule) defer |
5007 apply(rule inter_interior_unions_intervals) apply(rule finite_imageI,rule p',rule) defer |
5008 apply(rule,rule q') using q(1) p' unfolding r_def by auto qed |
5008 apply(rule,rule q') using q(1) p' unfolding r_def by auto qed |
5009 moreover have "\<Union>snd ` p \<union> \<Union>r = {a..b}" "{qq i |i. i \<in> r} = qq ` r" |
5009 moreover have "\<Union>(snd ` p) \<union> \<Union>r = {a..b}" "{qq i |i. i \<in> r} = qq ` r" |
5010 unfolding Union_Un_distrib[THEN sym] r_def using q by auto |
5010 unfolding Union_Un_distrib[THEN sym] r_def using q by auto |
5011 ultimately show "?p tagged_division_of {a..b}" by fastforce qed |
5011 ultimately show "?p tagged_division_of {a..b}" by fastforce qed |
5012 |
5012 |
5013 hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>\<Union>qq ` r. content k *\<^sub>R f x) - |
5013 hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>\<Union>(qq ` r). content k *\<^sub>R f x) - |
5014 integral {a..b} f) < e" apply(subst setsum_Un_zero[THEN sym]) apply(rule p') prefer 3 |
5014 integral {a..b} f) < e" apply(subst setsum_Un_zero[THEN sym]) apply(rule p') prefer 3 |
5015 apply assumption apply rule apply(rule finite_imageI,rule r) apply safe apply(drule qq) |
5015 apply assumption apply rule apply(rule finite_imageI,rule r) apply safe apply(drule qq) |
5016 proof- fix x l k assume as:"(x,l)\<in>p" "(x,l)\<in>qq k" "k\<in>r" |
5016 proof- fix x l k assume as:"(x,l)\<in>p" "(x,l)\<in>qq k" "k\<in>r" |
5017 note qq[OF this(3)] note tagged_division_ofD(3,4)[OF conjunct1[OF this] as(2)] |
5017 note qq[OF this(3)] note tagged_division_ofD(3,4)[OF conjunct1[OF this] as(2)] |
5018 from this(2) guess u v apply-by(erule exE)+ note uv=this |
5018 from this(2) guess u v apply-by(erule exE)+ note uv=this |