author paulson Sun, 13 Aug 2017 19:24:33 +0100 changeset 66408 46cfd348c373 parent 66407 7d3e4cedf824 child 66409 f749d39c016b
general rationalisation of Analysis
```--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Aug 12 23:11:26 2017 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Aug 13 19:24:33 2017 +0100
@@ -513,11 +513,11 @@

have *: "f integrable_on UNIV \<and> (\<lambda>k. integral UNIV (U k)) \<longlonglongrightarrow> integral UNIV f"
proof (rule monotone_convergence_increasing)
-    show "\<forall>k. U k integrable_on UNIV" using U_int by auto
-    show "\<forall>k. \<forall>x\<in>UNIV. U k x \<le> U (Suc k) x" using \<open>incseq U\<close> by (auto simp: incseq_def le_fun_def)
-    then show "bounded {integral UNIV (U k) |k. True}"
+    show "\<And>k. U k integrable_on UNIV" using U_int by auto
+    show "\<And>k x. x\<in>UNIV \<Longrightarrow> U k x \<le> U (Suc k) x" using \<open>incseq U\<close> by (auto simp: incseq_def le_fun_def)
+    then show "bounded (range (\<lambda>k. integral UNIV (U k)))"
using bnd int_eq by (auto simp: bounded_real intro!: exI[of _ r])
-    show "\<forall>x\<in>UNIV. (\<lambda>k. U k x) \<longlonglongrightarrow> f x"
+    show "\<And>x. x\<in>UNIV \<Longrightarrow> (\<lambda>k. U k x) \<longlonglongrightarrow> f x"
using seq by auto
qed
moreover have "(\<lambda>i. (\<integral>\<^sup>+x. U i x \<partial>lborel)) \<longlonglongrightarrow> (\<integral>\<^sup>+x. f x \<partial>lborel)"```
```--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Aug 12 23:11:26 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Aug 13 19:24:33 2017 +0100
@@ -6018,12 +6018,19 @@

subsection \<open>Monotone convergence (bounded interval first)\<close>

+(* TODO: is this lemma necessary? *)
+lemma bounded_increasing_convergent:
+  fixes f :: "nat \<Rightarrow> real"
+  shows "\<lbrakk>bounded (range f); \<And>n. f n \<le> f (Suc n)\<rbrakk> \<Longrightarrow> \<exists>l. f \<longlonglongrightarrow> l"
+  using Bseq_mono_convergent[of f] incseq_Suc_iff[of f]
+  by (auto simp: image_def Bseq_eq_bounded convergent_def incseq_def)
+
lemma monotone_convergence_interval:
fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
assumes "\<forall>k. (f k) integrable_on cbox a b"
and "\<forall>k. \<forall>x\<in>cbox a b.(f k x) \<le> f (Suc k) x"
and "\<forall>x\<in>cbox a b. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
-    and "bounded {integral (cbox a b) (f k) | k . k \<in> UNIV}"
+    and bounded: "bounded (range (\<lambda>k. integral (cbox a b) (f k)))"
shows "g integrable_on cbox a b \<and> ((\<lambda>k. integral (cbox a b) (f k)) \<longlongrightarrow> integral (cbox a b) g) sequentially"
proof (cases "content (cbox a b) = 0")
case True
@@ -6049,45 +6056,31 @@
apply auto
done
qed
-  have "\<exists>i. ((\<lambda>k. integral (cbox a b) (f k)) \<longlongrightarrow> i) sequentially"
-    apply (rule bounded_increasing_convergent)
-    defer
-    apply rule
-    apply (rule integral_le)
-    apply safe
-    apply (rule assms(1-2)[rule_format])+
-    using assms(4)
-    apply auto
-    done
-  then guess i..note i=this
-  have i': "\<And>k. (integral(cbox a b) (f k)) \<le> i\<bullet>1"
-    apply (rule Lim_component_ge)
-    apply (rule i)
-    apply (rule trivial_limit_sequentially)
+  have int_inc: "\<And>n. integral (cbox a b) (f n) \<le> integral (cbox a b) (f (Suc n))"
+    by (metis integral_le assms(1-2))
+  then obtain i where i: "(\<lambda>k. integral (cbox a b) (f k)) \<longlonglongrightarrow> i"
+    using bounded_increasing_convergent bounded by blast
+  have "\<And>k. \<forall>\<^sub>F x in sequentially. integral (cbox a b) (f k) \<le> integral (cbox a b) (f x) \<bullet> 1"
unfolding eventually_sequentially
-    apply (rule_tac x=k in exI)
-    apply clarify
-    apply (erule transitive_stepwise_le)
-    prefer 3
-    unfolding inner_simps real_inner_1_right
-    apply (rule integral_le)
-    apply (rule assms(1-2)[rule_format])+
-    using assms(2)
-    apply auto
-    done
-
+    by (force intro: transitive_stepwise_le int_inc)
+  then have i': "\<And>k. (integral(cbox a b) (f k)) \<le> i\<bullet>1"
+    using Lim_component_ge [OF i] trivial_limit_sequentially by blast
have "(g has_integral i) (cbox a b)"
unfolding has_integral
proof (safe, goal_cases)
-    case e: (1 e)
-    then have "\<forall>k. (\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
+    fix e::real
+    assume e: "e > 0"
+    have "\<And>k. (\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f k x) - integral (cbox a b) (f k)) < e/2 ^ (k + 2)))"
-      apply -
-      apply rule
apply (rule assms(1)[unfolded has_integral_integral has_integral,rule_format])
-      apply auto
+      using e apply auto
done
-    from choice[OF this] guess c..note c=conjunctD2[OF this[rule_format],rule_format]
+    then obtain c where c:
+          "\<And>x. gauge (c x)"
+          "\<And>x p. \<lbrakk>p tagged_division_of cbox a b; c x fine p\<rbrakk> \<Longrightarrow>
+              norm ((\<Sum>(u, ka)\<in>p. content ka *\<^sub>R f x u) - integral (cbox a b) (f x))
+              < e / 2 ^ (x + 2)"
+      by metis

have "\<exists>r. \<forall>k\<ge>r. 0 \<le> i\<bullet>1 - (integral (cbox a b) (f k)) \<and> i\<bullet>1 - (integral (cbox a b) (f k)) < e / 4"
proof -
@@ -6095,11 +6088,7 @@
using e by auto
from LIMSEQ_D [OF i this] guess r ..
then show ?thesis
-        apply (rule_tac x=r in exI)
-        apply rule
-        apply (erule_tac x=k in allE)
-        subgoal for k using i'[of k] by auto
-        done
+        using i' by auto
qed
then guess r..note r=conjunctD2[OF this[rule_format]]

@@ -6122,7 +6111,14 @@
qed
from bchoice[OF this] guess m..note m=conjunctD2[OF this[rule_format],rule_format]
define d where "d x = c (m x) x" for x
-    show ?case
+    show "\<exists>d. gauge d \<and>
+             (\<forall>p. p tagged_division_of cbox a b \<and>
+                  d fine p \<longrightarrow>
+                  norm
+                   ((\<Sum>(x, k)\<in>p.
+                       content k *\<^sub>R g x) -
+                    i)
+                  < e)"
apply (rule_tac x=d in exI)
proof safe
show "gauge d"
@@ -6215,7 +6211,6 @@
apply (simp add: e)
apply safe
apply (rule c)+
-              apply rule
apply assumption+
apply (rule tagged_partial_division_subset[of p])
apply (rule p(1)[unfolded tagged_division_of_def,THEN conjunct1])
@@ -6286,22 +6281,22 @@

lemma monotone_convergence_increasing:
fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
-  assumes "\<forall>k. (f k) integrable_on s"
-    and "\<forall>k. \<forall>x\<in>s. (f k x) \<le> (f (Suc k) x)"
-    and "\<forall>x\<in>s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
-    and "bounded {integral s (f k)| k. True}"
-  shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
+  assumes "\<And>k. (f k) integrable_on S"
+    and "\<And>k x. x \<in> S \<Longrightarrow> (f k x) \<le> (f (Suc k) x)"
+    and "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
+    and "bounded (range (\<lambda>k. integral S (f k)))"
+  shows "g integrable_on S \<and> ((\<lambda>k. integral S (f k)) \<longlongrightarrow> integral S g) sequentially"
proof -
-  have lem: "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
-    if "\<forall>k. \<forall>x\<in>s. 0 \<le> f k x"
-    and "\<forall>k. (f k) integrable_on s"
-    and "\<forall>k. \<forall>x\<in>s. f k x \<le> f (Suc k) x"
-    and "\<forall>x\<in>s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
-    and "bounded {integral s (f k)| k. True}"
-    for f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" and g s
+  have lem: "g integrable_on S \<and> ((\<lambda>k. integral S (f k)) \<longlongrightarrow> integral S g) sequentially"
+    if "\<forall>k. \<forall>x\<in>S. 0 \<le> f k x"
+    and "\<forall>k. (f k) integrable_on S"
+    and "\<forall>k. \<forall>x\<in>S. f k x \<le> f (Suc k) x"
+    and "\<forall>x\<in>S. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
+    and bou: "bounded (range(\<lambda>k. integral S (f k)))"
+    for f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" and g S
proof -
note assms=that[rule_format]
-    have "\<forall>x\<in>s. \<forall>k. (f k x)\<bullet>1 \<le> (g x)\<bullet>1"
+    have "\<forall>x\<in>S. \<forall>k. (f k x)\<bullet>1 \<le> (g x)\<bullet>1"
apply safe
apply (rule Lim_component_ge)
apply (rule that(4)[rule_format])
@@ -6312,19 +6307,12 @@
using assms(3) by (force intro: transitive_stepwise_le)
note fg=this[rule_format]

-    have "\<exists>i. ((\<lambda>k. integral s (f k)) \<longlongrightarrow> i) sequentially"
-      apply (rule bounded_increasing_convergent)
-      apply (rule that(5))
-      apply rule
-      apply (rule integral_le)
-      apply (rule that(2)[rule_format])+
-      using that(3)
-      apply auto
-      done
-    then guess i..note i=this
-    have "\<And>k. \<forall>x\<in>s. \<forall>n\<ge>k. f k x \<le> f n x"
+    obtain i where i: "(\<lambda>k. integral S (f k)) \<longlonglongrightarrow> i"
+      using bounded_increasing_convergent [OF bou]
+      using \<open>\<forall>k. \<forall>x\<in>S. f k x \<le> f (Suc k) x\<close> assms(2) integral_le by blast
+    have "\<And>k. \<forall>x\<in>S. \<forall>n\<ge>k. f k x \<le> f n x"
using assms(3) by (force intro: transitive_stepwise_le)
-    then have i': "\<forall>k. (integral s (f k))\<bullet>1 \<le> i\<bullet>1"
+    then have i': "\<forall>k. (integral S (f k))\<bullet>1 \<le> i\<bullet>1"
apply -
apply rule
apply (rule Lim_component_ge)
@@ -6339,45 +6327,45 @@
apply auto
done

-    note int = assms(2)[unfolded integrable_alt[of _ s],THEN conjunct1,rule_format]
-    have ifif: "\<And>k t. (\<lambda>x. if x \<in> t then if x \<in> s then f k x else 0 else 0) =
-      (\<lambda>x. if x \<in> t \<inter> s then f k x else 0)"
+    note int = assms(2)[unfolded integrable_alt[of _ S],THEN conjunct1,rule_format]
+    have ifif: "\<And>k t. (\<lambda>x. if x \<in> t then if x \<in> S then f k x else 0 else 0) =
+      (\<lambda>x. if x \<in> t \<inter> S then f k x else 0)"
by (rule ext) auto
-    have int': "\<And>k a b. f k integrable_on cbox a b \<inter> s"
+    have int': "\<And>k a b. f k integrable_on cbox a b \<inter> S"
apply (subst integrable_restrict_UNIV[symmetric])
apply (subst ifif[symmetric])
apply (subst integrable_restrict_UNIV)
apply (rule int)
done
-    have "\<And>a b. (\<lambda>x. if x \<in> s then g x else 0) integrable_on cbox a b \<and>
-      ((\<lambda>k. integral (cbox a b) (\<lambda>x. if x \<in> s then f k x else 0)) \<longlongrightarrow>
-      integral (cbox a b) (\<lambda>x. if x \<in> s then g x else 0)) sequentially"
+    have "\<And>a b. (\<lambda>x. if x \<in> S then g x else 0) integrable_on cbox a b \<and>
+      ((\<lambda>k. integral (cbox a b) (\<lambda>x. if x \<in> S then f k x else 0)) \<longlongrightarrow>
+      integral (cbox a b) (\<lambda>x. if x \<in> S then g x else 0)) sequentially"
proof (rule monotone_convergence_interval, safe, goal_cases)
case 1
show ?case by (rule int)
next
case (2 _ _ _ x)
then show ?case
-        apply (cases "x \<in> s")
+        apply (cases "x \<in> S")
using assms(3)
apply auto
done
next
case (3 _ _ x)
then show ?case
-        apply (cases "x \<in> s")
+        apply (cases "x \<in> S")
using assms(4)
apply auto
done
next
case (4 a b)
note * = integral_nonneg
-      have "\<And>k. norm (integral (cbox a b) (\<lambda>x. if x \<in> s then f k x else 0)) \<le> norm (integral s (f k))"
+      have "\<And>k. norm (integral (cbox a b) (\<lambda>x. if x \<in> S then f k x else 0)) \<le> norm (integral S (f k))"
unfolding real_norm_def
apply (subst abs_of_nonneg)
apply (rule *[OF int])
apply safe
-        apply (case_tac "x \<in> s")
+        apply (case_tac "x \<in> S")
apply (drule assms(1))
prefer 3
apply (subst abs_of_nonneg)
@@ -6395,7 +6383,7 @@
apply safe
apply (rule_tac x=aa in exI)
apply safe
-        apply (erule_tac x="integral s (f k)" in ballE)
+        apply (erule_tac x="integral S (f k)" in ballE)
apply (rule order_trans)
apply assumption
apply auto
@@ -6403,7 +6391,7 @@
qed
note g = conjunctD2[OF this]

-    have "(g has_integral i) s"
+    have "(g has_integral i) S"
unfolding has_integral_alt'
apply safe
apply (rule g(1))
@@ -6425,7 +6413,7 @@
from \<open>e > 0\<close> have "e/2 > 0"
by auto
from LIMSEQ_D [OF g(2)[of a b] this] guess M..note M=this
-        have **: "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then f N x else 0) - i) < e/2"
+        have **: "norm (integral (cbox a b) (\<lambda>x. if x \<in> S then f N x else 0) - i) < e/2"
apply (rule norm_triangle_half_l)
using B(2)[rule_format,OF ab] N[rule_format,of N]
apply -
@@ -6436,7 +6424,7 @@
have *: "\<And>f1 f2 g. \<bar>f1 - i\<bar> < e/2 \<longrightarrow> \<bar>f2 - g\<bar> < e/2 \<longrightarrow>
f1 \<le> f2 \<longrightarrow> f2 \<le> i \<longrightarrow> \<bar>g - i\<bar> < e"
unfolding real_inner_1_right by arith
-        show "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then g x else 0) - i) < e"
+        show "norm (integral (cbox a b) (\<lambda>x. if x \<in> S then g x else 0) - i) < e"
unfolding real_norm_def
apply (rule *[rule_format])
apply (rule **[unfolded real_norm_def])
@@ -6447,7 +6435,7 @@
apply (rule order_trans[OF _ i'[rule_format,of "M + N",unfolded real_inner_1_right]])
proof (safe, goal_cases)
case (2 x)
-          have "\<And>m. x \<in> s \<Longrightarrow> \<forall>n\<ge>m. (f m x)\<bullet>1 \<le> (f n x)\<bullet>1"
+          have "\<And>m. x \<in> S \<Longrightarrow> \<forall>n\<ge>m. (f m x)\<bullet>1 \<le> (f n x)\<bullet>1"
using assms(3) by (force intro: transitive_stepwise_le)
then show ?case
by auto
@@ -6472,16 +6460,16 @@
done
qed

-  have sub: "\<And>k. integral s (\<lambda>x. f k x - f 0 x) = integral s (f k) - integral s (f 0)"
+  have sub: "\<And>k. integral S (\<lambda>x. f k x - f 0 x) = integral S (f k) - integral S (f 0)"
apply (subst integral_diff)
apply (rule assms(1)[rule_format])+
apply rule
done
-  have "\<And>x m. x \<in> s \<Longrightarrow> \<forall>n\<ge>m. f m x \<le> f n x"
+  have "\<And>x m. x \<in> S \<Longrightarrow> \<forall>n\<ge>m. f m x \<le> f n x"
using assms(2) by (force intro: transitive_stepwise_le)
note * = this[rule_format]
-  have "(\<lambda>x. g x - f 0 x) integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. f (Suc k) x - f 0 x)) \<longlongrightarrow>
-    integral s (\<lambda>x. g x - f 0 x)) sequentially"
+  have "(\<lambda>x. g x - f 0 x) integrable_on S \<and> ((\<lambda>k. integral S (\<lambda>x. f (Suc k) x - f 0 x)) \<longlongrightarrow>
+    integral S (\<lambda>x. g x - f 0 x)) sequentially"
apply (rule lem)
apply safe
proof goal_cases
@@ -6513,16 +6501,16 @@
using assms(4)
unfolding bounded_iff
apply safe
-      apply (rule_tac x="a + norm (integral s (\<lambda>x. f 0 x))" in exI)
+      apply (rule_tac x="a + norm (integral S (\<lambda>x. f 0 x))" in exI)
apply safe
-      apply (erule_tac x="integral s (\<lambda>x. f (Suc k) x)" in ballE)
+      apply (erule_tac x="integral S (\<lambda>x. f (Suc k) x)" in ballE)
unfolding sub
apply (rule order_trans[OF norm_triangle_ineq4])
apply auto
done
qed
note conjunctD2[OF this]
-  note tendsto_add[OF this(2) tendsto_const[of "integral s (f 0)"]]
+  note tendsto_add[OF this(2) tendsto_const[of "integral S (f 0)"]]
integrable_add[OF this(1) assms(1)[rule_format,of 0]]
then show ?thesis
unfolding sub
@@ -6547,13 +6535,12 @@
proof -
have x_eq: "x = (\<lambda>i. integral s (f i))"
by (simp add: integral_unique[OF f])
-  then have x: "{integral s (f k) |k. True} = range x"
+  then have x: "range(\<lambda>k. integral s (f k)) = range x"
by auto
-
have *: "g integrable_on s \<and> (\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
proof (intro monotone_convergence_increasing allI ballI assms)
-    show "bounded {integral s (f k) |k. True}"
-      unfolding x by (rule convergent_imp_bounded) fact
+    show "bounded (range(\<lambda>k. integral s (f k)))"
+      using x convergent_imp_bounded assms by metis
qed (use f in auto)
then have "integral s g = x'"
by (intro LIMSEQ_unique[OF _ \<open>x \<longlonglongrightarrow> x'\<close>]) (simp add: x_eq)
@@ -6563,40 +6550,34 @@

lemma monotone_convergence_decreasing:
fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
-  assumes "\<forall>k. (f k) integrable_on s"
-    and "\<forall>k. \<forall>x\<in>s. f (Suc k) x \<le> f k x"
-    and "\<forall>x\<in>s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
-    and "bounded {integral s (f k)| k. True}"
-  shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
+  assumes "\<And>k. (f k) integrable_on S"
+    and "\<And>k x. x \<in> S \<Longrightarrow> f (Suc k) x \<le> f k x"
+    and "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
+    and "bounded (range(\<lambda>k. integral S (f k)))"
+  shows "g integrable_on S \<and> ((\<lambda>k. integral S (f k)) \<longlongrightarrow> integral S g) sequentially"
proof -
-  note assm = assms[rule_format]
-  have *: "{integral s (\<lambda>x. - f k x) |k. True} = op *\<^sub>R (- 1) ` {integral s (f k)| k. True}"
+  have *: "{integral S (\<lambda>x. - f k x) |k. True} = op *\<^sub>R (- 1) ` (range(\<lambda>k. integral S (f k)))"
apply safe
unfolding image_iff
-    apply (rule_tac x="integral s (f k)" in bexI)
+    apply (rule_tac x="integral S (f k)" in bexI)
prefer 3
apply (rule_tac x=k in exI)
apply auto
done
-  have "(\<lambda>x. - g x) integrable_on s \<and>
-    ((\<lambda>k. integral s (\<lambda>x. - f k x)) \<longlongrightarrow> integral s (\<lambda>x. - g x)) sequentially"
-    apply (rule monotone_convergence_increasing)
-    apply safe
-    apply (rule integrable_neg)
-    apply (rule assm)
-    defer
-    apply (rule tendsto_minus)
-    apply (rule assm)
-    apply assumption
-    unfolding *
-    apply (rule bounded_scaling)
-    using assm
-    apply auto
-    done
-  note * = conjunctD2[OF this]
-  show ?thesis
-    using integrable_neg[OF *(1)] tendsto_minus[OF *(2)]
-    by auto
+  have "(\<lambda>x. - g x) integrable_on S \<and>
+    ((\<lambda>k. integral S (\<lambda>x. - f k x)) \<longlongrightarrow> integral S (\<lambda>x. - g x)) sequentially"
+  proof (rule monotone_convergence_increasing)
+    show "\<And>k. (\<lambda>x. - f k x) integrable_on S"
+      by (blast intro: integrable_neg assms)
+    show "\<And>k x. x \<in> S \<Longrightarrow> - f k x \<le> - f (Suc k) x"
+      by (simp add: assms)
+    show "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>k. - f k x) \<longlonglongrightarrow> - g x"
+      by (simp add: assms tendsto_minus)
+    show "bounded (range(\<lambda>k. integral S (\<lambda>x. - f k x)))"
+      using "*" assms(4) bounded_scaling by auto
+  qed
+  then show ?thesis
+    by (force dest: integrable_neg tendsto_minus)
qed

lemma integral_norm_bound_integral:
@@ -7553,7 +7534,7 @@
also have "\<dots> \<le> exp (- a * c) / a" using a by simp
finally show ?thesis .
qed (insert a, simp_all add: integral_f)
-    thus "bounded {integral {c..} (f k) |k. True}"
+    thus "bounded (range(\<lambda>k. integral {c..} (f k)))"
by (intro boundedI[of _ "exp (-a*c)/a"]) auto
qed (auto simp: f_def)

@@ -7646,7 +7627,7 @@
hence "F k = abs (F k)" by simp
finally have "abs (F k) \<le>  c powr (a + 1) / (a + 1)" .
}
-    thus "bounded {integral {0..c} (f k) |k. True}"
+    thus "bounded (range(\<lambda>k. integral {0..c} (f k)))"
by (intro boundedI[of _ "c powr (a+1) / (a+1)"]) (auto simp: integral_f)
qed

@@ -7732,7 +7713,7 @@
by (intro powr_mono2') simp_all
with assms show ?thesis by (auto simp: divide_simps F_def integral_f)
qed (insert assms, simp add: integral_f F_def divide_simps)
-    thus "bounded {integral {a..} (f n) |n. True}"
+    thus "bounded (range(\<lambda>k. integral {a..} (f k)))"
unfolding bounded_iff by (intro exI[of _ "-F a"]) auto
qed
```
```--- a/src/HOL/Analysis/Improper_Integral.thy	Sat Aug 12 23:11:26 2017 +0100
+++ b/src/HOL/Analysis/Improper_Integral.thy	Sun Aug 13 19:24:33 2017 +0100
@@ -1507,7 +1507,7 @@
let ?\<phi> = "\<lambda>k x. if x \<in> cbox (a + (b - a) /\<^sub>R (Suc k)) (b - (b - a) /\<^sub>R (Suc k))
then g x - f x \<bullet> j else 0"
have "(\<lambda>x. g x - f x \<bullet> j) integrable_on box a b"
-        proof (rule monotone_convergence_increasing [of ?\<phi>, THEN conjunct1], safe)
+        proof (rule monotone_convergence_increasing [of ?\<phi>, THEN conjunct1])
have *: "cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k)) \<inter> box a b
= cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k))" for k
using box_subset_cbox "1" by fastforce
@@ -1562,7 +1562,7 @@
apply (simp add: integral_restrict_Int integral_diff)
using "*" box_subset_cbox by (blast intro: Bg add_mono order_trans [OF abs_triangle_ineq4])
qed
-          then show "bounded {integral (box a b) (?\<phi> k)| k. True}"
+          then show "bounded (range (\<lambda>k. integral (box a b) (?\<phi> k)))"
apply (simp add: bounded_pos)
apply (rule_tac x="Bg+Bf" in exI)
using \<open>0 < Bf\<close> \<open>0 < Bg\<close>  apply auto
@@ -1585,7 +1585,7 @@
let ?\<phi> = "\<lambda>k x. if x \<in> cbox (a + (b - a) /\<^sub>R (Suc k)) (b - (b - a) /\<^sub>R (Suc k))
then f x \<bullet> j - g x else 0"
have "(\<lambda>x. f x \<bullet> j - g x) integrable_on box a b"
-        proof (rule monotone_convergence_increasing [of ?\<phi>, THEN conjunct1], safe)
+        proof (rule monotone_convergence_increasing [of ?\<phi>, THEN conjunct1])
have *: "cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k)) \<inter> box a b
= cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k))" for k
using box_subset_cbox "1" by fastforce
@@ -1642,7 +1642,7 @@
apply (simp add: integral_restrict_Int integral_diff)
using "*" box_subset_cbox by (blast intro: Bg add_mono order_trans [OF abs_triangle_ineq4])
qed
-          then show "bounded {integral (box a b) (?\<phi> k)| k. True}"
+          then show "bounded (range (\<lambda>k. integral (box a b) (?\<phi> k)))"
apply (simp add: bounded_pos)
apply (rule_tac x="Bf+Bg" in exI)
using \<open>0 < Bf\<close> \<open>0 < Bg\<close>  by auto```
```--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sat Aug 12 23:11:26 2017 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Aug 13 19:24:33 2017 +0100
@@ -5389,13 +5389,6 @@
shows "~ compact (UNIV::'a set)"
by (simp add: compact_eq_bounded_closed)

-(* TODO: is this lemma necessary? *)
-lemma bounded_increasing_convergent:
-  fixes s :: "nat \<Rightarrow> real"
-  shows "bounded {s n| n. True} \<Longrightarrow> \<forall>n. s n \<le> s (Suc n) \<Longrightarrow> \<exists>l. s \<longlonglongrightarrow> l"
-  using Bseq_mono_convergent[of s] incseq_Suc_iff[of s]
-  by (auto simp: image_def Bseq_eq_bounded convergent_def incseq_def)
-
instance real :: heine_borel
proof
fix f :: "nat \<Rightarrow> real"```