1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Nov 05 09:45:00 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Nov 05 09:45:02 2013 +0100
1.3 @@ -28,10 +28,10 @@
1.4 proof -
1.5 have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
1.6 by arith
1.7 - then show ?thesis
1.8 - using S b cSup_bounds[of S "l - e" "l+e"]
1.9 - unfolding th
1.10 - by (auto simp add: setge_def setle_def)
1.11 + have "bdd_above S"
1.12 + using b by (auto intro!: bdd_aboveI[of _ "l + e"])
1.13 + with S b show ?thesis
1.14 + unfolding th by (auto intro!: cSup_upper2 cSup_least)
1.15 qed
1.16
1.17 lemma cInf_asclose: (* TODO: is this really needed? *)
1.18 @@ -70,39 +70,6 @@
1.19 shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists>x\<in>S. a \<ge> x)"
1.20 by (metis cInf_eq_Min Min_le_iff)
1.21
1.22 -lemma Inf: (* rename *)
1.23 - fixes S :: "real set"
1.24 - shows "S \<noteq> {} \<Longrightarrow> (\<exists>b. b <=* S) \<Longrightarrow> isGlb UNIV S (Inf S)"
1.25 - by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def
1.26 - intro: cInf_lower cInf_greatest)
1.27 -
1.28 -lemma real_le_inf_subset:
1.29 - assumes "t \<noteq> {}"
1.30 - and "t \<subseteq> s"
1.31 - and "\<exists>b. b <=* s"
1.32 - shows "Inf s \<le> Inf (t::real set)"
1.33 - apply (rule isGlb_le_isLb)
1.34 - apply (rule Inf[OF assms(1)])
1.35 - apply (insert assms)
1.36 - apply (erule exE)
1.37 - apply (rule_tac x = b in exI)
1.38 - apply (auto simp: isLb_def setge_def intro!: cInf_lower cInf_greatest)
1.39 - done
1.40 -
1.41 -lemma real_ge_sup_subset:
1.42 - fixes t :: "real set"
1.43 - assumes "t \<noteq> {}"
1.44 - and "t \<subseteq> s"
1.45 - and "\<exists>b. s *<= b"
1.46 - shows "Sup s \<ge> Sup t"
1.47 - apply (rule isLub_le_isUb)
1.48 - apply (rule isLub_cSup[OF assms(1)])
1.49 - apply (insert assms)
1.50 - apply (erule exE)
1.51 - apply (rule_tac x = b in exI)
1.52 - apply (auto simp: isUb_def setle_def intro!: cSup_upper cSup_least)
1.53 - done
1.54 -
1.55 (*declare not_less[simp] not_le[simp]*)
1.56
1.57 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
1.58 @@ -486,24 +453,24 @@
1.59 subsection {* Bounds on intervals where they exist. *}
1.60
1.61 definition interval_upperbound :: "('a::ordered_euclidean_space) set \<Rightarrow> 'a"
1.62 - where "interval_upperbound s = (\<Sum>i\<in>Basis. Sup {a. \<exists>x\<in>s. x\<bullet>i = a} *\<^sub>R i)"
1.63 + where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
1.64
1.65 definition interval_lowerbound :: "('a::ordered_euclidean_space) set \<Rightarrow> 'a"
1.66 - where "interval_lowerbound s = (\<Sum>i\<in>Basis. Inf {a. \<exists>x\<in>s. x\<bullet>i = a} *\<^sub>R i)"
1.67 + where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
1.68
1.69 lemma interval_upperbound[simp]:
1.70 "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
1.71 interval_upperbound {a..b} = (b::'a::ordered_euclidean_space)"
1.72 unfolding interval_upperbound_def euclidean_representation_setsum
1.73 - by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setle_def
1.74 - intro!: cSup_unique)
1.75 + by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] SUP_def
1.76 + intro!: cSup_eq)
1.77
1.78 lemma interval_lowerbound[simp]:
1.79 "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
1.80 interval_lowerbound {a..b} = (a::'a::ordered_euclidean_space)"
1.81 unfolding interval_lowerbound_def euclidean_representation_setsum
1.82 - by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setge_def
1.83 - intro!: cInf_unique)
1.84 + by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] INF_def
1.85 + intro!: cInf_eq)
1.86
1.87 lemmas interval_bounds = interval_upperbound interval_lowerbound
1.88
1.89 @@ -6627,7 +6594,7 @@
1.90 lemma interval_bound_sing[simp]:
1.91 "interval_upperbound {a} = a"
1.92 "interval_lowerbound {a} = a"
1.93 - unfolding interval_upperbound_def interval_lowerbound_def
1.94 + unfolding interval_upperbound_def interval_lowerbound_def SUP_def INF_def
1.95 by (auto simp: euclidean_representation)
1.96
1.97 lemma additive_tagged_division_1:
1.98 @@ -11236,37 +11203,26 @@
1.99 lemma bounded_variation_absolutely_integrable_interval:
1.100 fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'm::ordered_euclidean_space"
1.101 assumes "f integrable_on {a..b}"
1.102 - and "\<forall>d. d division_of {a..b} \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
1.103 + and *: "\<forall>d. d division_of {a..b} \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
1.104 shows "f absolutely_integrable_on {a..b}"
1.105 proof -
1.106 - let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of {a..b} }"
1.107 - def i \<equiv> "Sup ?S"
1.108 - have i: "isLub UNIV ?S i"
1.109 - unfolding i_def
1.110 - apply (rule isLub_cSup)
1.111 - apply (rule elementary_interval)
1.112 - defer
1.113 - apply (rule_tac x=B in exI)
1.114 - apply (rule setleI)
1.115 - using assms(2)
1.116 - apply auto
1.117 - done
1.118 + let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of {a..b}}"
1.119 + have D_1: "?D \<noteq> {}"
1.120 + by (rule elementary_interval[of a b]) auto
1.121 + have D_2: "bdd_above (?f`?D)"
1.122 + by (metis * mem_Collect_eq bdd_aboveI2)
1.123 + note D = D_1 D_2
1.124 + let ?S = "SUP x:?D. ?f x"
1.125 show ?thesis
1.126 apply rule
1.127 apply (rule assms)
1.128 apply rule
1.129 - apply (subst has_integral[of _ i])
1.130 + apply (subst has_integral[of _ ?S])
1.131 proof safe
1.132 case goal1
1.133 - then have "i - e / 2 \<notin> Collect (isUb UNIV (setsum (\<lambda>k. norm (integral k f)) `
1.134 - {d. d division_of {a..b}}))"
1.135 - using isLub_ubs[OF i,rule_format]
1.136 - unfolding setge_def ubs_def
1.137 - by auto
1.138 - then have "\<exists>y. y division_of {a..b} \<and> i - e / 2 < (\<Sum>k\<in>y. norm (integral k f))"
1.139 - unfolding mem_Collect_eq isUb_def setle_def
1.140 - by (simp add: not_le)
1.141 - then guess d .. note d=conjunctD2[OF this]
1.142 + then have "?S - e / 2 < ?S" by simp
1.143 + then obtain d where d: "d division_of {a..b}" "?S - e / 2 < (\<Sum>k\<in>d. norm (integral k f))"
1.144 + unfolding less_cSUP_iff[OF D] by auto
1.145 note d' = division_ofD[OF this(1)]
1.146
1.147 have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
1.148 @@ -11451,21 +11407,17 @@
1.149 done
1.150 note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
1.151
1.152 - have *: "\<And>sni sni' sf sf'. abs (sf' - sni') < e / 2 \<longrightarrow> i - e / 2 < sni \<and> sni' \<le> i \<and>
1.153 - sni \<le> sni' \<and> sf' = sf \<longrightarrow> abs (sf - i) < e"
1.154 + have *: "\<And>sni sni' sf sf'. abs (sf' - sni') < e / 2 \<longrightarrow> ?S - e / 2 < sni \<and> sni' \<le> ?S \<and>
1.155 + sni \<le> sni' \<and> sf' = sf \<longrightarrow> abs (sf - ?S) < e"
1.156 by arith
1.157 - show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - i) < e"
1.158 + show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - ?S) < e"
1.159 unfolding real_norm_def
1.160 apply (rule *[rule_format,OF **])
1.161 apply safe
1.162 apply(rule d(2))
1.163 proof -
1.164 - case goal1
1.165 - show ?case unfolding sum_p'
1.166 - apply (rule isLubD2[OF i])
1.167 - using division_of_tagged_division[OF p'']
1.168 - apply auto
1.169 - done
1.170 + case goal1 show ?case
1.171 + by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
1.172 next
1.173 case goal2
1.174 have *: "{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} =
1.175 @@ -11756,18 +11708,13 @@
1.176 and "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm (integral k f)) d \<le> B"
1.177 shows "f absolutely_integrable_on UNIV"
1.178 proof (rule absolutely_integrable_onI, fact, rule)
1.179 - let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of (\<Union>d)}"
1.180 - def i \<equiv> "Sup ?S"
1.181 - have i: "isLub UNIV ?S i"
1.182 - unfolding i_def
1.183 - apply (rule isLub_cSup)
1.184 - apply (rule elementary_interval)
1.185 - defer
1.186 - apply (rule_tac x=B in exI)
1.187 - apply (rule setleI)
1.188 - using assms(2)
1.189 - apply auto
1.190 - done
1.191 + let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of (\<Union>d)}"
1.192 + have D_1: "?D \<noteq> {}"
1.193 + by (rule elementary_interval) auto
1.194 + have D_2: "bdd_above (?f`?D)"
1.195 + by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
1.196 + note D = D_1 D_2
1.197 + let ?S = "SUP d:?D. ?f d"
1.198 have f_int: "\<And>a b. f absolutely_integrable_on {a..b}"
1.199 apply (rule bounded_variation_absolutely_integrable_interval[where B=B])
1.200 apply (rule integrable_on_subinterval[OF assms(1)])
1.201 @@ -11776,7 +11723,7 @@
1.202 apply (rule assms(2)[rule_format])
1.203 apply auto
1.204 done
1.205 - show "((\<lambda>x. norm (f x)) has_integral i) UNIV"
1.206 + show "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
1.207 apply (subst has_integral_alt')
1.208 apply safe
1.209 proof -
1.210 @@ -11785,16 +11732,11 @@
1.211 using f_int[of a b] by auto
1.212 next
1.213 case goal2
1.214 - have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> i - e"
1.215 + have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> ?S - e"
1.216 proof (rule ccontr)
1.217 assume "\<not> ?thesis"
1.218 - then have "i \<le> i - e"
1.219 - apply -
1.220 - apply (rule isLub_le_isUb[OF i])
1.221 - apply (rule isUbI)
1.222 - unfolding setle_def
1.223 - apply auto
1.224 - done
1.225 + then have "?S \<le> ?S - e"
1.226 + by (intro cSUP_least[OF D(1)]) auto
1.227 then show False
1.228 using goal2 by auto
1.229 qed
1.230 @@ -11811,9 +11753,9 @@
1.231 proof -
1.232 fix a b :: 'n
1.233 assume ab: "ball 0 (K + 1) \<subseteq> {a..b}"
1.234 - have *: "\<forall>s s1. i - e < s1 \<and> s1 \<le> s \<and> s < i + e \<longrightarrow> abs (s - i) < e"
1.235 + have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> abs (s - ?S) < e"
1.236 by arith
1.237 - show "norm (integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - i) < e"
1.238 + show "norm (integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
1.239 unfolding real_norm_def
1.240 apply (rule *[rule_format])
1.241 apply safe
1.242 @@ -11865,10 +11807,10 @@
1.243 from henstock_lemma[OF f(1) `e/2>0`] guess d2 . note d2=this
1.244 from fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] guess p .
1.245 note p=this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
1.246 - have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> i \<longrightarrow> abs (sf - si) < e / 2 \<longrightarrow>
1.247 - abs (sf' - di) < e / 2 \<longrightarrow> di < i + e"
1.248 + have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> abs (sf - si) < e / 2 \<longrightarrow>
1.249 + abs (sf' - di) < e / 2 \<longrightarrow> di < ?S + e"
1.250 by arith
1.251 - show "integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < i + e"
1.252 + show "integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
1.253 apply (subst if_P)
1.254 apply rule
1.255 proof (rule *[rule_format])
1.256 @@ -11891,18 +11833,12 @@
1.257 apply (subst abs_of_nonneg)
1.258 apply auto
1.259 done
1.260 - show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> i"
1.261 + show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> ?S"
1.262 + using partial_division_of_tagged_division[of p "{a..b}"] p(1)
1.263 apply (subst setsum_over_tagged_division_lemma[OF p(1)])
1.264 - defer
1.265 - apply (rule isLubD2[OF i])
1.266 - unfolding image_iff
1.267 - apply (rule_tac x="snd ` p" in bexI)
1.268 - unfolding mem_Collect_eq
1.269 - defer
1.270 - apply (rule partial_division_of_tagged_division[of _ "{a..b}"])
1.271 - using p(1)
1.272 - unfolding tagged_division_of_def
1.273 - apply auto
1.274 + apply (simp add: integral_null)
1.275 + apply (intro cSUP_upper2[OF D(2), of "snd ` p"])
1.276 + apply (auto simp: tagged_partial_division_of_def)
1.277 done
1.278 qed
1.279 qed
1.280 @@ -12378,11 +12314,22 @@
1.281 lemma dominated_convergence:
1.282 fixes f :: "nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
1.283 assumes "\<And>k. (f k) integrable_on s" "h integrable_on s"
1.284 - and "\<And>k. \<forall>x \<in> s. norm(f k x) \<le> (h x)"
1.285 + and "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
1.286 and "\<forall>x \<in> s. ((\<lambda>k. f k x) ---> g x) sequentially"
1.287 shows "g integrable_on s"
1.288 and "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
1.289 proof -
1.290 + have bdd_below[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_below {f n x |n. P n}"
1.291 + proof (safe intro!: bdd_belowI)
1.292 + fix n x show "x \<in> s \<Longrightarrow> - h x \<le> f n x"
1.293 + using assms(3)[rule_format, of x n] by simp
1.294 + qed
1.295 + have bdd_above[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_above {f n x |n. P n}"
1.296 + proof (safe intro!: bdd_aboveI)
1.297 + fix n x show "x \<in> s \<Longrightarrow> f n x \<le> h x"
1.298 + using assms(3)[rule_format, of x n] by simp
1.299 + qed
1.300 +
1.301 have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and>
1.302 ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) --->
1.303 integral s (\<lambda>x. Inf {f j x |j. m \<le> j}))sequentially"
1.304 @@ -12422,66 +12369,32 @@
1.305 fix x
1.306 assume x: "x \<in> s"
1.307 show "Inf {f j x |j. j \<in> {m..m + Suc k}} \<le> Inf {f j x |j. j \<in> {m..m + k}}"
1.308 - apply (rule cInf_ge)
1.309 - unfolding setge_def
1.310 - defer
1.311 - apply rule
1.312 - apply (subst cInf_finite_le_iff)
1.313 - prefer 3
1.314 - apply (rule_tac x=xa in bexI)
1.315 - apply auto
1.316 - done
1.317 - let ?S = "{f j x| j. m \<le> j}"
1.318 - def i \<equiv> "Inf ?S"
1.319 - show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
1.320 + by (rule cInf_superset_mono) auto
1.321 + let ?S = "{f j x| j. m \<le> j}"
1.322 + show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> Inf ?S) sequentially"
1.323 proof (rule LIMSEQ_I)
1.324 case goal1
1.325 note r = this
1.326 - have i: "isGlb UNIV ?S i"
1.327 - unfolding i_def
1.328 - apply (rule Inf)
1.329 - defer
1.330 - apply (rule_tac x="- h x - 1" in exI)
1.331 - unfolding setge_def
1.332 - proof safe
1.333 - case goal1
1.334 - then show ?case using assms(3)[rule_format,OF x, of j] by auto
1.335 - qed auto
1.336 -
1.337 - have "\<exists>y\<in>?S. \<not> y \<ge> i + r"
1.338 - proof(rule ccontr)
1.339 - assume "\<not> ?thesis"
1.340 - then have "i \<ge> i + r"
1.341 - apply -
1.342 - apply (rule isGlb_le_isLb[OF i])
1.343 - apply (rule isLbI)
1.344 - unfolding setge_def
1.345 - apply fastforce+
1.346 - done
1.347 - then show False using r by auto
1.348 - qed
1.349 - then guess y .. note y=this[unfolded not_le]
1.350 - from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
1.351 +
1.352 + have "\<exists>y\<in>?S. y < Inf ?S + r"
1.353 + by (subst cInf_less_iff[symmetric]) (auto simp: `x\<in>s` r)
1.354 + then obtain N where N: "f N x < Inf ?S + r" "m \<le> N"
1.355 + by blast
1.356
1.357 show ?case
1.358 apply (rule_tac x=N in exI)
1.359 proof safe
1.360 case goal1
1.361 - have *: "\<And>y ix. y < i + r \<longrightarrow> i \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - i) < r"
1.362 + have *: "\<And>y ix. y < Inf ?S + r \<longrightarrow> Inf ?S \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - Inf ?S) < r"
1.363 by arith
1.364 show ?case
1.365 unfolding real_norm_def
1.366 - apply (rule *[rule_format,OF y(2)])
1.367 - unfolding i_def
1.368 - apply (rule real_le_inf_subset)
1.369 - prefer 3
1.370 - apply (rule,rule isGlbD1[OF i])
1.371 - prefer 3
1.372 - apply (subst cInf_finite_le_iff)
1.373 - prefer 3
1.374 - apply (rule_tac x=y in bexI)
1.375 + apply (rule *[rule_format, OF N(1)])
1.376 + apply (rule cInf_superset_mono, auto simp: `x\<in>s`) []
1.377 + apply (rule cInf_lower)
1.378 using N goal1
1.379 - apply auto
1.380 + apply auto []
1.381 + apply simp
1.382 done
1.383 qed
1.384 qed
1.385 @@ -12525,65 +12438,27 @@
1.386 fix x
1.387 assume x: "x\<in>s"
1.388 show "Sup {f j x |j. j \<in> {m..m + Suc k}} \<ge> Sup {f j x |j. j \<in> {m..m + k}}"
1.389 - apply (rule cSup_le)
1.390 - unfolding setle_def
1.391 - defer
1.392 - apply rule
1.393 - apply (subst cSup_finite_ge_iff)
1.394 - prefer 3
1.395 - apply (rule_tac x=y in bexI)
1.396 - apply auto
1.397 - done
1.398 - let ?S = "{f j x| j. m \<le> j}"
1.399 - def i \<equiv> "Sup ?S"
1.400 - show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
1.401 + by (rule cSup_subset_mono) auto
1.402 + let ?S = "{f j x| j. m \<le> j}"
1.403 + show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> Sup ?S) sequentially"
1.404 proof (rule LIMSEQ_I)
1.405 case goal1 note r=this
1.406 - have i: "isLub UNIV ?S i"
1.407 - unfolding i_def
1.408 - apply (rule isLub_cSup)
1.409 - defer
1.410 - apply (rule_tac x="h x" in exI)
1.411 - unfolding setle_def
1.412 - proof safe
1.413 - case goal1
1.414 - then show ?case
1.415 - using assms(3)[rule_format,OF x, of j] by auto
1.416 - qed auto
1.417 -
1.418 - have "\<exists>y\<in>?S. \<not> y \<le> i - r"
1.419 - proof (rule ccontr)
1.420 - assume "\<not> ?thesis"
1.421 - then have "i \<le> i - r"
1.422 - apply -
1.423 - apply (rule isLub_le_isUb[OF i])
1.424 - apply (rule isUbI)
1.425 - unfolding setle_def
1.426 - apply fastforce+
1.427 - done
1.428 - then show False
1.429 - using r by auto
1.430 - qed
1.431 - then guess y .. note y=this[unfolded not_le]
1.432 - from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
1.433 + have "\<exists>y\<in>?S. Sup ?S - r < y"
1.434 + by (subst less_cSup_iff[symmetric]) (auto simp: r `x\<in>s`)
1.435 + then obtain N where N: "Sup ?S - r < f N x" "m \<le> N"
1.436 + by blast
1.437
1.438 show ?case
1.439 apply (rule_tac x=N in exI)
1.440 proof safe
1.441 case goal1
1.442 - have *: "\<And>y ix. i - r < y \<longrightarrow> ix \<le> i \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - i) < r"
1.443 + have *: "\<And>y ix. Sup ?S - r < y \<longrightarrow> ix \<le> Sup ?S \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - Sup ?S) < r"
1.444 by arith
1.445 show ?case
1.446 - unfolding real_norm_def
1.447 - apply (rule *[rule_format,OF y(2)])
1.448 - unfolding i_def
1.449 - apply (rule real_ge_sup_subset)
1.450 - prefer 3
1.451 - apply (rule, rule isLubD1[OF i])
1.452 - prefer 3
1.453 - apply (subst cSup_finite_ge_iff)
1.454 - prefer 3
1.455 - apply (rule_tac x = y in bexI)
1.456 + apply simp
1.457 + apply (rule *[rule_format, OF N(1)])
1.458 + apply (rule cSup_subset_mono, auto simp: `x\<in>s`) []
1.459 + apply (subst cSup_upper)
1.460 using N goal1
1.461 apply auto
1.462 done
1.463 @@ -12616,17 +12491,7 @@
1.464
1.465 have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
1.466 show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}"
1.467 - apply -
1.468 - apply (rule real_le_inf_subset)
1.469 - prefer 3
1.470 - unfolding setge_def
1.471 - apply (rule_tac x="- h x" in exI)
1.472 - apply safe
1.473 - apply (rule *)
1.474 - using assms(3)[rule_format,OF x]
1.475 - unfolding real_norm_def abs_le_iff
1.476 - apply auto
1.477 - done
1.478 + by (intro cInf_superset_mono) (auto simp: `x\<in>s`)
1.479
1.480 show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) ----> g x"
1.481 proof (rule LIMSEQ_I)
1.482 @@ -12674,16 +12539,7 @@
1.483 assume x: "x \<in> s"
1.484
1.485 show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}"
1.486 - apply -
1.487 - apply (rule real_ge_sup_subset)
1.488 - prefer 3
1.489 - unfolding setle_def
1.490 - apply (rule_tac x="h x" in exI)
1.491 - apply safe
1.492 - using assms(3)[rule_format,OF x]
1.493 - unfolding real_norm_def abs_le_iff
1.494 - apply auto
1.495 - done
1.496 + by (rule cSup_subset_mono) (auto simp: `x\<in>s`)
1.497 show "((\<lambda>k. Sup {f j x |j. k \<le> j}) ---> g x) sequentially"
1.498 proof (rule LIMSEQ_I)
1.499 case goal1
1.500 @@ -12712,41 +12568,18 @@
1.501 from LIMSEQ_D [OF inc2(2) goal1] guess N1 .. note N1=this[unfolded real_norm_def]
1.502 from LIMSEQ_D [OF dec2(2) goal1] guess N2 .. note N2=this[unfolded real_norm_def]
1.503 show ?case
1.504 - apply (rule_tac x="N1+N2" in exI, safe)
1.505 - proof -
1.506 + proof (rule_tac x="N1+N2" in exI, safe)
1.507 fix n
1.508 assume n: "n \<ge> N1 + N2"
1.509 have *: "\<And>i0 i i1 g. \<bar>i0 - g\<bar> < r \<longrightarrow> \<bar>i1 - g\<bar> < r \<longrightarrow> i0 \<le> i \<longrightarrow> i \<le> i1 \<longrightarrow> \<bar>i - g\<bar> < r"
1.510 by arith
1.511 show "norm (integral s (f n) - integral s g) < r"
1.512 unfolding real_norm_def
1.513 - apply (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
1.514 - proof -
1.515 + proof (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
1.516 show "integral s (\<lambda>x. Inf {f j x |j. n \<le> j}) \<le> integral s (f n)"
1.517 - proof (rule integral_le[OF dec1(1) assms(1)], safe)
1.518 - fix x
1.519 - assume x: "x \<in> s"
1.520 - have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
1.521 - show "Inf {f j x |j. n \<le> j} \<le> f n x"
1.522 - apply (intro cInf_lower bdd_belowI)
1.523 - apply auto []
1.524 - apply (rule *)
1.525 - using assms(3)[rule_format,OF x]
1.526 - unfolding real_norm_def abs_le_iff
1.527 - apply auto
1.528 - done
1.529 - qed
1.530 + by (rule integral_le[OF dec1(1) assms(1)]) (auto intro!: cInf_lower)
1.531 show "integral s (f n) \<le> integral s (\<lambda>x. Sup {f j x |j. n \<le> j})"
1.532 - proof (rule integral_le[OF assms(1) inc1(1)], safe)
1.533 - fix x
1.534 - assume x: "x \<in> s"
1.535 - show "f n x \<le> Sup {f j x |j. n \<le> j}"
1.536 - apply (rule cSup_upper)
1.537 - using assms(3)[rule_format,OF x]
1.538 - unfolding real_norm_def abs_le_iff
1.539 - apply auto
1.540 - done
1.541 - qed
1.542 + by (rule integral_le[OF assms(1) inc1(1)]) (auto intro!: cSup_upper)
1.543 qed (insert n, auto)
1.544 qed
1.545 qed