Small lemmas about analysis
authoreberlm <eberlm@in.tum.de>
Sat Aug 04 01:03:39 2018 +0200 (9 months ago)
changeset 6872153ad5c01be3f
parent 68720 1e1818612124
child 68722 6aea897bff2a
Small lemmas about analysis
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/FPS_Convergence.thy
src/HOL/Analysis/Gamma_Function.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Set_Integral.thy
src/HOL/Archimedean_Field.thy
src/HOL/Complex.thy
src/HOL/Int.thy
src/HOL/Limits.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Series.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat Aug 04 00:19:23 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat Aug 04 01:03:39 2018 +0200
     1.3 @@ -1341,6 +1341,29 @@
     1.4  lemma contour_integral_trivial [simp]: "contour_integral (linepath a a) f = 0"
     1.5    using has_contour_integral_trivial contour_integral_unique by blast
     1.6  
     1.7 +lemma differentiable_linepath [intro]: "linepath a b differentiable at x within A"
     1.8 +  by (auto simp: linepath_def)
     1.9 +
    1.10 +lemma bounded_linear_linepath:
    1.11 +  assumes "bounded_linear f"
    1.12 +  shows   "f (linepath a b x) = linepath (f a) (f b) x"
    1.13 +proof -
    1.14 +  interpret f: bounded_linear f by fact
    1.15 +  show ?thesis by (simp add: linepath_def f.add f.scale)
    1.16 +qed
    1.17 +
    1.18 +lemma bounded_linear_linepath':
    1.19 +  assumes "bounded_linear f"
    1.20 +  shows   "f \<circ> linepath a b = linepath (f a) (f b)"
    1.21 +  using bounded_linear_linepath[OF assms] by (simp add: fun_eq_iff)
    1.22 +
    1.23 +lemma cnj_linepath: "cnj (linepath a b x) = linepath (cnj a) (cnj b) x"
    1.24 +  by (simp add: linepath_def)
    1.25 +
    1.26 +lemma cnj_linepath': "cnj \<circ> linepath a b = linepath (cnj a) (cnj b)"
    1.27 +  by (simp add: linepath_def fun_eq_iff)
    1.28 +
    1.29 +
    1.30  
    1.31  subsection\<open>Relation to subpath construction\<close>
    1.32  
    1.33 @@ -1501,6 +1524,62 @@
    1.34       "contour_integral g f = integral {0..1} (\<lambda>x. f (g x) * vector_derivative g (at x))"
    1.35    by (simp add: contour_integral_def integral_def has_contour_integral contour_integrable_on)
    1.36  
    1.37 +lemma contour_integral_cong:
    1.38 +  assumes "g = g'" "\<And>x. x \<in> path_image g \<Longrightarrow> f x = f' x"
    1.39 +  shows   "contour_integral g f = contour_integral g' f'"
    1.40 +  unfolding contour_integral_integral using assms
    1.41 +  by (intro integral_cong) (auto simp: path_image_def)
    1.42 +
    1.43 +
    1.44 +text \<open>Contour integral along a segment on the real axis\<close>
    1.45 +
    1.46 +lemma has_contour_integral_linepath_Reals_iff:
    1.47 +  fixes a b :: complex and f :: "complex \<Rightarrow> complex"
    1.48 +  assumes "a \<in> Reals" "b \<in> Reals" "Re a < Re b"
    1.49 +  shows   "(f has_contour_integral I) (linepath a b) \<longleftrightarrow>
    1.50 +             ((\<lambda>x. f (of_real x)) has_integral I) {Re a..Re b}"
    1.51 +proof -
    1.52 +  from assms have [simp]: "of_real (Re a) = a" "of_real (Re b) = b"
    1.53 +    by (simp_all add: complex_eq_iff)
    1.54 +  from assms have "a \<noteq> b" by auto
    1.55 +  have "((\<lambda>x. f (of_real x)) has_integral I) (cbox (Re a) (Re b)) \<longleftrightarrow>
    1.56 +          ((\<lambda>x. f (a + b * of_real x - a * of_real x)) has_integral I /\<^sub>R (Re b - Re a)) {0..1}"
    1.57 +    by (subst has_integral_affinity_iff [of "Re b - Re a" _ "Re a", symmetric])
    1.58 +       (insert assms, simp_all add: field_simps scaleR_conv_of_real)
    1.59 +  also have "(\<lambda>x. f (a + b * of_real x - a * of_real x)) =
    1.60 +               (\<lambda>x. (f (a + b * of_real x - a * of_real x) * (b - a)) /\<^sub>R (Re b - Re a))"
    1.61 +    using \<open>a \<noteq> b\<close> by (auto simp: field_simps fun_eq_iff scaleR_conv_of_real)
    1.62 +  also have "(\<dots> has_integral I /\<^sub>R (Re b - Re a)) {0..1} \<longleftrightarrow> 
    1.63 +               ((\<lambda>x. f (linepath a b x) * (b - a)) has_integral I) {0..1}" using assms
    1.64 +    by (subst has_integral_cmul_iff) (auto simp: linepath_def scaleR_conv_of_real algebra_simps)
    1.65 +  also have "\<dots> \<longleftrightarrow> (f has_contour_integral I) (linepath a b)" unfolding has_contour_integral_def
    1.66 +    by (intro has_integral_cong) (simp add: vector_derivative_linepath_within)
    1.67 +  finally show ?thesis by simp
    1.68 +qed
    1.69 +
    1.70 +lemma contour_integrable_linepath_Reals_iff:
    1.71 +  fixes a b :: complex and f :: "complex \<Rightarrow> complex"
    1.72 +  assumes "a \<in> Reals" "b \<in> Reals" "Re a < Re b"
    1.73 +  shows   "(f contour_integrable_on linepath a b) \<longleftrightarrow>
    1.74 +             (\<lambda>x. f (of_real x)) integrable_on {Re a..Re b}"
    1.75 +  using has_contour_integral_linepath_Reals_iff[OF assms, of f]
    1.76 +  by (auto simp: contour_integrable_on_def integrable_on_def)
    1.77 +
    1.78 +lemma contour_integral_linepath_Reals_eq:
    1.79 +  fixes a b :: complex and f :: "complex \<Rightarrow> complex"
    1.80 +  assumes "a \<in> Reals" "b \<in> Reals" "Re a < Re b"
    1.81 +  shows   "contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (of_real x))"
    1.82 +proof (cases "f contour_integrable_on linepath a b")
    1.83 +  case True
    1.84 +  thus ?thesis using has_contour_integral_linepath_Reals_iff[OF assms, of f]
    1.85 +    using has_contour_integral_integral has_contour_integral_unique by blast
    1.86 +next
    1.87 +  case False
    1.88 +  thus ?thesis using contour_integrable_linepath_Reals_iff[OF assms, of f]
    1.89 +    by (simp add: not_integrable_contour_integral not_integrable_integral)
    1.90 +qed
    1.91 +
    1.92 +
    1.93  
    1.94  text\<open>Cauchy's theorem where there's a primitive\<close>
    1.95  
    1.96 @@ -4875,6 +4954,10 @@
    1.97    apply (rule derivative_eq_intros | simp)+
    1.98    done
    1.99  
   1.100 +corollary differentiable_part_circlepath:
   1.101 +  "part_circlepath c r a b differentiable at x within A"
   1.102 +  using has_vector_derivative_part_circlepath[of c r a b x A] differentiableI_vector by blast
   1.103 +
   1.104  corollary vector_derivative_part_circlepath:
   1.105      "vector_derivative (part_circlepath z r s t) (at x) =
   1.106         \<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)"
   1.107 @@ -4923,6 +5006,17 @@
   1.108      by (fastforce simp add: path_image_def part_circlepath_def)
   1.109  qed
   1.110  
   1.111 +proposition path_image_part_circlepath':
   1.112 +  "path_image (part_circlepath z r s t) = (\<lambda>x. z + r * cis x) ` closed_segment s t"
   1.113 +proof -
   1.114 +  have "path_image (part_circlepath z r s t) = 
   1.115 +          (\<lambda>x. z + r * exp(\<i> * of_real x)) ` linepath s t ` {0..1}"
   1.116 +    by (simp add: image_image path_image_def part_circlepath_def)
   1.117 +  also have "linepath s t ` {0..1} = closed_segment s t"
   1.118 +    by (rule linepath_image_01)
   1.119 +  finally show ?thesis by (simp add: cis_conv_exp)
   1.120 +qed
   1.121 +
   1.122  corollary path_image_part_circlepath_subset:
   1.123      "\<lbrakk>s \<le> t; 0 \<le> r\<rbrakk> \<Longrightarrow> path_image(part_circlepath z r s t) \<subseteq> sphere z r"
   1.124  by (auto simp: path_image_part_circlepath sphere_def dist_norm algebra_simps norm_mult)
   1.125 @@ -4937,6 +5031,106 @@
   1.126      by (simp add: dist_norm norm_minus_commute)
   1.127  qed
   1.128  
   1.129 +corollary path_image_part_circlepath_subset':
   1.130 +  assumes "r \<ge> 0"
   1.131 +  shows   "path_image (part_circlepath z r s t) \<subseteq> sphere z r"
   1.132 +proof (cases "s \<le> t")
   1.133 +  case True
   1.134 +  thus ?thesis using path_image_part_circlepath_subset[of s t r z] assms by simp
   1.135 +next
   1.136 +  case False
   1.137 +  thus ?thesis using path_image_part_circlepath_subset[of t s r z] assms
   1.138 +    by (subst reversepath_part_circlepath [symmetric], subst path_image_reversepath) simp_all
   1.139 +qed
   1.140 +
   1.141 +lemma part_circlepath_cnj: "cnj (part_circlepath c r a b x) = part_circlepath (cnj c) r (-a) (-b) x"
   1.142 +  by (simp add: part_circlepath_def exp_cnj linepath_def algebra_simps)
   1.143 +
   1.144 +lemma contour_integral_bound_part_circlepath:
   1.145 +  assumes "f contour_integrable_on part_circlepath c r a b"
   1.146 +  assumes "B \<ge> 0" "r \<ge> 0" "\<And>x. x \<in> path_image (part_circlepath c r a b) \<Longrightarrow> norm (f x) \<le> B"
   1.147 +  shows   "norm (contour_integral (part_circlepath c r a b) f) \<le> B * r * \<bar>b - a\<bar>"
   1.148 +proof -
   1.149 +  let ?I = "integral {0..1} (\<lambda>x. f (part_circlepath c r a b x) * \<i> * of_real (r * (b - a)) *
   1.150 +              exp (\<i> * linepath a b x))"
   1.151 +  have "norm ?I \<le> integral {0..1} (\<lambda>x::real. B * 1 * (r * \<bar>b - a\<bar>) * 1)"
   1.152 +  proof (rule integral_norm_bound_integral, goal_cases)
   1.153 +    case 1
   1.154 +    with assms(1) show ?case
   1.155 +      by (simp add: contour_integrable_on vector_derivative_part_circlepath mult_ac)
   1.156 +  next
   1.157 +    case (3 x)
   1.158 +    with assms(2-) show ?case unfolding norm_mult norm_of_real abs_mult
   1.159 +      by (intro mult_mono) (auto simp: path_image_def)
   1.160 +  qed auto
   1.161 +  also have "?I = contour_integral (part_circlepath c r a b) f"
   1.162 +    by (simp add: contour_integral_integral vector_derivative_part_circlepath mult_ac)
   1.163 +  finally show ?thesis by simp
   1.164 +qed
   1.165 +
   1.166 +lemma has_contour_integral_part_circlepath_iff:
   1.167 +  assumes "a < b"
   1.168 +  shows "(f has_contour_integral I) (part_circlepath c r a b) \<longleftrightarrow>
   1.169 +           ((\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) has_integral I) {a..b}"
   1.170 +proof -
   1.171 +  have "(f has_contour_integral I) (part_circlepath c r a b) \<longleftrightarrow>
   1.172 +          ((\<lambda>x. f (part_circlepath c r a b x) * vector_derivative (part_circlepath c r a b)
   1.173 +           (at x within {0..1})) has_integral I) {0..1}"
   1.174 +    unfolding has_contour_integral_def ..
   1.175 +  also have "\<dots> \<longleftrightarrow> ((\<lambda>x. f (part_circlepath c r a b x) * r * (b - a) * \<i> *
   1.176 +                            cis (linepath a b x)) has_integral I) {0..1}"
   1.177 +    by (intro has_integral_cong, subst vector_derivative_part_circlepath01)
   1.178 +       (simp_all add: cis_conv_exp)
   1.179 +  also have "\<dots> \<longleftrightarrow> ((\<lambda>x. f (c + r * exp (\<i> * linepath (of_real a) (of_real b) x)) *
   1.180 +                       r * \<i> * exp (\<i> * linepath (of_real a) (of_real b) x) *
   1.181 +                       vector_derivative (linepath (of_real a) (of_real b)) 
   1.182 +                         (at x within {0..1})) has_integral I) {0..1}"
   1.183 +    by (intro has_integral_cong, subst vector_derivative_linepath_within)
   1.184 +       (auto simp: part_circlepath_def cis_conv_exp of_real_linepath [symmetric])
   1.185 +  also have "\<dots> \<longleftrightarrow> ((\<lambda>z. f (c + r * exp (\<i> * z)) * r * \<i> * exp (\<i> * z)) has_contour_integral I)
   1.186 +                      (linepath (of_real a) (of_real b))"
   1.187 +    by (simp add: has_contour_integral_def)
   1.188 +  also have "\<dots> \<longleftrightarrow> ((\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) has_integral I) {a..b}" using assms
   1.189 +    by (subst has_contour_integral_linepath_Reals_iff) (simp_all add: cis_conv_exp)
   1.190 +  finally show ?thesis .
   1.191 +qed
   1.192 +
   1.193 +lemma contour_integrable_part_circlepath_iff:
   1.194 +  assumes "a < b"
   1.195 +  shows "f contour_integrable_on (part_circlepath c r a b) \<longleftrightarrow>
   1.196 +           (\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}"
   1.197 +  using assms by (auto simp: contour_integrable_on_def integrable_on_def 
   1.198 +                             has_contour_integral_part_circlepath_iff)
   1.199 +
   1.200 +lemma contour_integral_part_circlepath_eq:
   1.201 +  assumes "a < b"
   1.202 +  shows "contour_integral (part_circlepath c r a b) f =
   1.203 +           integral {a..b} (\<lambda>t. f (c + r * cis t) * r * \<i> * cis t)"
   1.204 +proof (cases "f contour_integrable_on part_circlepath c r a b")
   1.205 +  case True
   1.206 +  hence "(\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}" 
   1.207 +    using assms by (simp add: contour_integrable_part_circlepath_iff)
   1.208 +  with True show ?thesis
   1.209 +    using has_contour_integral_part_circlepath_iff[OF assms]
   1.210 +          contour_integral_unique has_integral_integrable_integral by blast
   1.211 +next
   1.212 +  case False
   1.213 +  hence "\<not>(\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}" 
   1.214 +    using assms by (simp add: contour_integrable_part_circlepath_iff)
   1.215 +  with False show ?thesis
   1.216 +    by (simp add: not_integrable_contour_integral not_integrable_integral)
   1.217 +qed
   1.218 +
   1.219 +lemma contour_integral_part_circlepath_reverse:
   1.220 +  "contour_integral (part_circlepath c r a b) f = -contour_integral (part_circlepath c r b a) f"
   1.221 +  by (subst reversepath_part_circlepath [symmetric], subst contour_integral_reversepath) simp_all
   1.222 +
   1.223 +lemma contour_integral_part_circlepath_reverse':
   1.224 +  "b < a \<Longrightarrow> contour_integral (part_circlepath c r a b) f = 
   1.225 +               -contour_integral (part_circlepath c r b a) f"
   1.226 +  by (rule contour_integral_part_circlepath_reverse)
   1.227 +
   1.228 +
   1.229  proposition finite_bounded_log: "finite {z::complex. norm z \<le> b \<and> exp z = w}"
   1.230  proof (cases "w = 0")
   1.231    case True then show ?thesis by auto
     2.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat Aug 04 00:19:23 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat Aug 04 01:03:39 2018 +0200
     2.3 @@ -41,6 +41,24 @@
     2.4  lemma linear_cnj: "linear cnj"
     2.5    using bounded_linear.linear[OF bounded_linear_cnj] .
     2.6  
     2.7 +lemma vector_derivative_cnj_within:
     2.8 +  assumes "at x within A \<noteq> bot" and "f differentiable at x within A"
     2.9 +  shows   "vector_derivative (\<lambda>z. cnj (f z)) (at x within A) = 
    2.10 +             cnj (vector_derivative f (at x within A))" (is "_ = cnj ?D")
    2.11 +proof -
    2.12 +  let ?D = "vector_derivative f (at x within A)"
    2.13 +  from assms have "(f has_vector_derivative ?D) (at x within A)"
    2.14 +    by (subst (asm) vector_derivative_works)
    2.15 +  hence "((\<lambda>x. cnj (f x)) has_vector_derivative cnj ?D) (at x within A)"
    2.16 +    by (rule has_vector_derivative_cnj)
    2.17 +  thus ?thesis using assms by (auto dest: vector_derivative_within)
    2.18 +qed
    2.19 +
    2.20 +lemma vector_derivative_cnj:
    2.21 +  assumes "f differentiable at x"
    2.22 +  shows   "vector_derivative (\<lambda>z. cnj (f z)) (at x) = cnj (vector_derivative f (at x))"
    2.23 +  using assms by (intro vector_derivative_cnj_within) auto
    2.24 +
    2.25  lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = ( * ) 0"
    2.26    by auto
    2.27  
    2.28 @@ -286,6 +304,35 @@
    2.29    "f holomorphic_on s \<Longrightarrow> g holomorphic_on t \<Longrightarrow> f ` s \<subseteq> t \<Longrightarrow> (g o f) holomorphic_on s"
    2.30    by (metis holomorphic_on_compose holomorphic_on_subset)
    2.31  
    2.32 +lemma holomorphic_on_balls_imp_entire:
    2.33 +  assumes "\<not>bdd_above A" "\<And>r. r \<in> A \<Longrightarrow> f holomorphic_on ball c r"
    2.34 +  shows   "f holomorphic_on B"
    2.35 +proof (rule holomorphic_on_subset)
    2.36 +  show "f holomorphic_on UNIV" unfolding holomorphic_on_def
    2.37 +  proof
    2.38 +    fix z :: complex
    2.39 +    from \<open>\<not>bdd_above A\<close> obtain r where r: "r \<in> A" "r > norm (z - c)"
    2.40 +      by (meson bdd_aboveI not_le)
    2.41 +    with assms(2) have "f holomorphic_on ball c r" by blast
    2.42 +    moreover from r have "z \<in> ball c r" by (auto simp: dist_norm norm_minus_commute)
    2.43 +    ultimately show "f field_differentiable at z"
    2.44 +      by (auto simp: holomorphic_on_def at_within_open[of _ "ball c r"])
    2.45 +  qed
    2.46 +qed auto
    2.47 +
    2.48 +lemma holomorphic_on_balls_imp_entire':
    2.49 +  assumes "\<And>r. r > 0 \<Longrightarrow> f holomorphic_on ball c r"
    2.50 +  shows   "f holomorphic_on B"
    2.51 +proof (rule holomorphic_on_balls_imp_entire)
    2.52 +  {
    2.53 +    fix M :: real
    2.54 +    have "\<exists>x. x > max M 0" by (intro gt_ex)
    2.55 +    hence "\<exists>x>0. x > M" by auto
    2.56 +  }
    2.57 +  thus "\<not>bdd_above {(0::real)<..}" unfolding bdd_above_def
    2.58 +    by (auto simp: not_le)
    2.59 +qed (insert assms, auto)
    2.60 +
    2.61  lemma holomorphic_on_minus [holomorphic_intros]: "f holomorphic_on s \<Longrightarrow> (\<lambda>z. -(f z)) holomorphic_on s"
    2.62    by (metis field_differentiable_minus holomorphic_on_def)
    2.63  
     3.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Sat Aug 04 00:19:23 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sat Aug 04 01:03:39 2018 +0200
     3.3 @@ -176,6 +176,16 @@
     3.4  lemma holomorphic_on_cos: "cos holomorphic_on S"
     3.5    by (simp add: field_differentiable_within_cos holomorphic_on_def)
     3.6  
     3.7 +lemma holomorphic_on_sin' [holomorphic_intros]:
     3.8 +  assumes "f holomorphic_on A"
     3.9 +  shows   "(\<lambda>x. sin (f x)) holomorphic_on A"
    3.10 +  using holomorphic_on_compose[OF assms holomorphic_on_sin] by (simp add: o_def)
    3.11 +
    3.12 +lemma holomorphic_on_cos' [holomorphic_intros]:
    3.13 +  assumes "f holomorphic_on A"
    3.14 +  shows   "(\<lambda>x. cos (f x)) holomorphic_on A"
    3.15 +  using holomorphic_on_compose[OF assms holomorphic_on_cos] by (simp add: o_def)
    3.16 +
    3.17  subsection\<open>Get a nice real/imaginary separation in Euler's formula\<close>
    3.18  
    3.19  lemma Euler: "exp(z) = of_real(exp(Re z)) *
    3.20 @@ -1308,6 +1318,11 @@
    3.21  lemma holomorphic_on_Ln [holomorphic_intros]: "(\<And>z. z \<in> S \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on S"
    3.22    by (simp add: field_differentiable_within_Ln holomorphic_on_def)
    3.23  
    3.24 +lemma holomorphic_on_Ln' [holomorphic_intros]:
    3.25 +  "(\<And>z. z \<in> A \<Longrightarrow> f z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> f holomorphic_on A \<Longrightarrow> (\<lambda>z. Ln (f z)) holomorphic_on A"
    3.26 +  using holomorphic_on_compose_gen[OF _ holomorphic_on_Ln, of f A "- \<real>\<^sub>\<le>\<^sub>0"]
    3.27 +  by (auto simp: o_def)
    3.28 +
    3.29  lemma tendsto_Ln [tendsto_intros]:
    3.30    fixes L F
    3.31    assumes "(f \<longlongrightarrow> L) F" "L \<notin> \<real>\<^sub>\<le>\<^sub>0"
     4.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Aug 04 00:19:23 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Aug 04 01:03:39 2018 +0200
     4.3 @@ -4612,6 +4612,93 @@
     4.4      unfolding absolutely_integrable_restrict_UNIV .
     4.5  qed
     4.6  
     4.7 +lemma uniform_limit_set_lebesgue_integral_at_top:
     4.8 +  fixes f :: "'a \<Rightarrow> real \<Rightarrow> 'b::{banach, second_countable_topology}"
     4.9 +    and g :: "real \<Rightarrow> real"
    4.10 +  assumes bound: "\<And>x y. x \<in> A \<Longrightarrow> y \<ge> a \<Longrightarrow> norm (f x y) \<le> g y"
    4.11 +  assumes integrable: "set_integrable M {a..} g"
    4.12 +  assumes measurable: "\<And>x. x \<in> A \<Longrightarrow> set_borel_measurable M {a..} (f x)"
    4.13 +  assumes "sets borel \<subseteq> sets M"
    4.14 +  shows   "uniform_limit A (\<lambda>b x. LINT y:{a..b}|M. f x y) (\<lambda>x. LINT y:{a..}|M. f x y) at_top"
    4.15 +proof (cases "A = {}")
    4.16 +  case False
    4.17 +  then obtain x where x: "x \<in> A" by auto
    4.18 +  have g_nonneg: "g y \<ge> 0" if "y \<ge> a" for y
    4.19 +  proof -
    4.20 +    have "0 \<le> norm (f x y)" by simp
    4.21 +    also have "\<dots> \<le> g y" using bound[OF x that] by simp
    4.22 +    finally show ?thesis .
    4.23 +  qed
    4.24 +
    4.25 +  have integrable': "set_integrable M {a..} (\<lambda>y. f x y)" if "x \<in> A" for x
    4.26 +    unfolding set_integrable_def
    4.27 +  proof (rule Bochner_Integration.integrable_bound)
    4.28 +    show "integrable M (\<lambda>x. indicator {a..} x * g x)"
    4.29 +      using integrable by (simp add: set_integrable_def)
    4.30 +    show "(\<lambda>y. indicat_real {a..} y *\<^sub>R f x y) \<in> borel_measurable M" using measurable[OF that]
    4.31 +      by (simp add: set_borel_measurable_def)
    4.32 +    show "AE y in M. norm (indicat_real {a..} y *\<^sub>R f x y) \<le> norm (indicat_real {a..} y * g y)"
    4.33 +      using bound[OF that] by (intro AE_I2) (auto simp: indicator_def g_nonneg)
    4.34 +  qed
    4.35 +
    4.36 +  show ?thesis
    4.37 +  proof (rule uniform_limitI)
    4.38 +    fix e :: real assume e: "e > 0"
    4.39 +    have sets [intro]: "A \<in> sets M" if "A \<in> sets borel" for A
    4.40 +      using that assms by blast
    4.41 +  
    4.42 +    have "((\<lambda>b. LINT y:{a..b}|M. g y) \<longlongrightarrow> (LINT y:{a..}|M. g y)) at_top"
    4.43 +      by (intro tendsto_set_lebesgue_integral_at_top assms sets) auto
    4.44 +    with e obtain b0 :: real where b0: "\<forall>b\<ge>b0. \<bar>(LINT y:{a..}|M. g y) - (LINT y:{a..b}|M. g y)\<bar> < e"
    4.45 +      by (auto simp: tendsto_iff eventually_at_top_linorder dist_real_def abs_minus_commute)
    4.46 +    define b where "b = max a b0"
    4.47 +    have "a \<le> b" by (simp add: b_def)
    4.48 +    from b0 have "\<bar>(LINT y:{a..}|M. g y) - (LINT y:{a..b}|M. g y)\<bar> < e"
    4.49 +      by (auto simp: b_def)
    4.50 +    also have "{a..} = {a..b} \<union> {b<..}" by (auto simp: b_def)
    4.51 +    also have "\<bar>(LINT y:\<dots>|M. g y) - (LINT y:{a..b}|M. g y)\<bar> = \<bar>(LINT y:{b<..}|M. g y)\<bar>"
    4.52 +      using \<open>a \<le> b\<close> by (subst set_integral_Un) (auto intro!: set_integrable_subset[OF integrable])
    4.53 +    also have "(LINT y:{b<..}|M. g y) \<ge> 0"
    4.54 +      using g_nonneg \<open>a \<le> b\<close> unfolding set_lebesgue_integral_def
    4.55 +      by (intro Bochner_Integration.integral_nonneg) (auto simp: indicator_def)
    4.56 +    hence "\<bar>(LINT y:{b<..}|M. g y)\<bar> = (LINT y:{b<..}|M. g y)" by simp
    4.57 +    finally have less: "(LINT y:{b<..}|M. g y) < e" .
    4.58 +
    4.59 +    have "eventually (\<lambda>b. b \<ge> b0) at_top" by (rule eventually_ge_at_top)
    4.60 +    moreover have "eventually (\<lambda>b. b \<ge> a) at_top" by (rule eventually_ge_at_top)
    4.61 +    ultimately show "eventually (\<lambda>b. \<forall>x\<in>A. 
    4.62 +                       dist (LINT y:{a..b}|M. f x y) (LINT y:{a..}|M. f x y) < e) at_top"
    4.63 +    proof eventually_elim
    4.64 +      case (elim b)
    4.65 +      show ?case
    4.66 +      proof
    4.67 +        fix x assume x: "x \<in> A"
    4.68 +        have "dist (LINT y:{a..b}|M. f x y) (LINT y:{a..}|M. f x y) =
    4.69 +                norm ((LINT y:{a..}|M. f x y) - (LINT y:{a..b}|M. f x y))"
    4.70 +          by (simp add: dist_norm norm_minus_commute)
    4.71 +        also have "{a..} = {a..b} \<union> {b<..}" using elim by auto
    4.72 +        also have "(LINT y:\<dots>|M. f x y) - (LINT y:{a..b}|M. f x y) = (LINT y:{b<..}|M. f x y)"
    4.73 +          using elim x
    4.74 +          by (subst set_integral_Un) (auto intro!: set_integrable_subset[OF integrable'])
    4.75 +        also have "norm \<dots> \<le> (LINT y:{b<..}|M. norm (f x y))" using elim x
    4.76 +          by (intro set_integral_norm_bound set_integrable_subset[OF integrable']) auto
    4.77 +        also have "\<dots> \<le> (LINT y:{b<..}|M. g y)" using elim x bound g_nonneg
    4.78 +          by (intro set_integral_mono set_integrable_norm set_integrable_subset[OF integrable']
    4.79 +                    set_integrable_subset[OF integrable]) auto
    4.80 +        also have "(LINT y:{b<..}|M. g y) \<ge> 0"
    4.81 +          using g_nonneg \<open>a \<le> b\<close> unfolding set_lebesgue_integral_def
    4.82 +          by (intro Bochner_Integration.integral_nonneg) (auto simp: indicator_def)
    4.83 +        hence "(LINT y:{b<..}|M. g y) = \<bar>(LINT y:{b<..}|M. g y)\<bar>" by simp
    4.84 +        also have "\<dots> = \<bar>(LINT y:{a..b} \<union> {b<..}|M. g y) - (LINT y:{a..b}|M. g y)\<bar>"
    4.85 +          using elim by (subst set_integral_Un) (auto intro!: set_integrable_subset[OF integrable])
    4.86 +        also have "{a..b} \<union> {b<..} = {a..}" using elim by auto
    4.87 +        also have "\<bar>(LINT y:{a..}|M. g y) - (LINT y:{a..b}|M. g y)\<bar> < e"
    4.88 +          using b0 elim by blast
    4.89 +        finally show "dist (LINT y:{a..b}|M. f x y) (LINT y:{a..}|M. f x y) < e" .
    4.90 +      qed
    4.91 +    qed
    4.92 +  qed
    4.93 +qed auto
    4.94  
    4.95  
    4.96  
     5.1 --- a/src/HOL/Analysis/FPS_Convergence.thy	Sat Aug 04 00:19:23 2018 +0100
     5.2 +++ b/src/HOL/Analysis/FPS_Convergence.thy	Sat Aug 04 01:03:39 2018 +0200
     5.3 @@ -193,6 +193,24 @@
     5.4      by (subst analytic_on_open) auto
     5.5  qed
     5.6  
     5.7 +lemma continuous_eval_fps [continuous_intros]:
     5.8 +  fixes z :: "'a::{real_normed_field,banach}"
     5.9 +  assumes "norm z < fps_conv_radius F"
    5.10 +  shows   "continuous (at z within A) (eval_fps F)"
    5.11 +proof -
    5.12 +  from ereal_dense2[OF assms] obtain K :: real where K: "norm z < K" "K < fps_conv_radius F"
    5.13 +    by auto
    5.14 +  have "0 \<le> norm z" by simp
    5.15 +  also have "norm z < K" by fact
    5.16 +  finally have "K > 0" .
    5.17 +  from K and \<open>K > 0\<close> have "summable (\<lambda>n. fps_nth F n * of_real K ^ n)"
    5.18 +    by (intro summable_fps) auto
    5.19 +  from this have "isCont (eval_fps F) z" unfolding eval_fps_def
    5.20 +    by (rule isCont_powser) (use K in auto)
    5.21 +  thus "continuous (at z within A)  (eval_fps F)"
    5.22 +    by (simp add: continuous_at_imp_continuous_within)
    5.23 +qed
    5.24 +
    5.25  
    5.26  subsection%unimportant \<open>Lower bounds on radius of convergence\<close>
    5.27  
    5.28 @@ -831,6 +849,20 @@
    5.29    ultimately show ?thesis using r(1) by (auto simp: has_fps_expansion_def)
    5.30  qed
    5.31  
    5.32 +lemma has_fps_expansion_imp_continuous:
    5.33 +  fixes F :: "'a::{real_normed_field,banach} fps"
    5.34 +  assumes "f has_fps_expansion F"
    5.35 +  shows   "continuous (at 0 within A) f"
    5.36 +proof -
    5.37 +  from assms have "isCont (eval_fps F) 0"
    5.38 +    by (intro continuous_eval_fps) (auto simp: has_fps_expansion_def zero_ereal_def)
    5.39 +  also have "?this \<longleftrightarrow> isCont f 0" using assms
    5.40 +    by (intro isCont_cong) (auto simp: has_fps_expansion_def)
    5.41 +  finally have "isCont f 0" .
    5.42 +  thus "continuous (at 0 within A) f"
    5.43 +    by (simp add: continuous_at_imp_continuous_within)
    5.44 +qed
    5.45 +
    5.46  lemma has_fps_expansion_const [simp, intro, fps_expansion_intros]:
    5.47    "(\<lambda>_. c) has_fps_expansion fps_const c"
    5.48    by (auto simp: has_fps_expansion_def)
     6.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Sat Aug 04 00:19:23 2018 +0100
     6.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Sat Aug 04 01:03:39 2018 +0200
     6.3 @@ -1457,6 +1457,15 @@
     6.4  lemma holomorphic_rGamma [holomorphic_intros]: "rGamma holomorphic_on A"
     6.5    unfolding holomorphic_on_def by (auto intro!: field_differentiable_rGamma)
     6.6  
     6.7 +lemma holomorphic_rGamma' [holomorphic_intros]: 
     6.8 +  assumes "f holomorphic_on A"
     6.9 +  shows   "(\<lambda>x. rGamma (f x)) holomorphic_on A"
    6.10 +proof -
    6.11 +  have "rGamma \<circ> f holomorphic_on A" using assms
    6.12 +    by (intro holomorphic_on_compose assms holomorphic_rGamma)
    6.13 +  thus ?thesis by (simp only: o_def)
    6.14 +qed
    6.15 +
    6.16  lemma analytic_rGamma: "rGamma analytic_on A"
    6.17    unfolding analytic_on_def by (auto intro!: exI[of _ 1] holomorphic_rGamma)
    6.18  
    6.19 @@ -1467,6 +1476,15 @@
    6.20  lemma holomorphic_Gamma [holomorphic_intros]: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma holomorphic_on A"
    6.21    unfolding holomorphic_on_def by (auto intro!: field_differentiable_Gamma)
    6.22  
    6.23 +lemma holomorphic_Gamma' [holomorphic_intros]: 
    6.24 +  assumes "f holomorphic_on A" and "\<And>x. x \<in> A \<Longrightarrow> f x \<notin> \<int>\<^sub>\<le>\<^sub>0"
    6.25 +  shows   "(\<lambda>x. Gamma (f x)) holomorphic_on A"
    6.26 +proof -
    6.27 +  have "Gamma \<circ> f holomorphic_on A" using assms
    6.28 +    by (intro holomorphic_on_compose assms holomorphic_Gamma) auto
    6.29 +  thus ?thesis by (simp only: o_def)
    6.30 +qed
    6.31 +
    6.32  lemma analytic_Gamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma analytic_on A"
    6.33    by (rule analytic_on_subset[of _ "UNIV - \<int>\<^sub>\<le>\<^sub>0"], subst analytic_on_open)
    6.34       (auto intro!: holomorphic_Gamma)
     7.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Aug 04 00:19:23 2018 +0100
     7.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Aug 04 01:03:39 2018 +0200
     7.3 @@ -687,6 +687,17 @@
     7.4    apply (simp_all add: integrable_integral integrable_linear has_integral_linear )
     7.5    done
     7.6  
     7.7 +lemma integrable_on_cnj_iff:
     7.8 +  "(\<lambda>x. cnj (f x)) integrable_on A \<longleftrightarrow> f integrable_on A"
     7.9 +  using integrable_linear[OF _ bounded_linear_cnj, of f A]
    7.10 +        integrable_linear[OF _ bounded_linear_cnj, of "cnj \<circ> f" A]
    7.11 +  by (auto simp: o_def)
    7.12 +
    7.13 +lemma integral_cnj: "cnj (integral A f) = integral A (\<lambda>x. cnj (f x))"
    7.14 +  by (cases "f integrable_on A")
    7.15 +     (simp_all add: integral_linear[OF _ bounded_linear_cnj, symmetric]
    7.16 +                    o_def integrable_on_cnj_iff not_integrable_integral)
    7.17 +
    7.18  lemma integral_component_eq[simp]:
    7.19    fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
    7.20    assumes "f integrable_on S"
    7.21 @@ -3440,6 +3451,64 @@
    7.22  
    7.23  lemmas has_integral_affinity01 = has_integral_affinity [of _ _ 0 "1::real", simplified]
    7.24  
    7.25 +lemma integrable_on_affinity:
    7.26 +  assumes "m \<noteq> 0" "f integrable_on (cbox a b)"
    7.27 +  shows   "(\<lambda>x. f (m *\<^sub>R x + c)) integrable_on ((\<lambda>x. (1 / m) *\<^sub>R x - ((1 / m) *\<^sub>R c)) ` cbox a b)"
    7.28 +proof -
    7.29 +  from assms obtain I where "(f has_integral I) (cbox a b)"
    7.30 +    by (auto simp: integrable_on_def)
    7.31 +  from has_integral_affinity[OF this assms(1), of c] show ?thesis
    7.32 +    by (auto simp: integrable_on_def)
    7.33 +qed
    7.34 +
    7.35 +lemma has_integral_cmul_iff:
    7.36 +  assumes "c \<noteq> 0"
    7.37 +  shows   "((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R I)) A \<longleftrightarrow> (f has_integral I) A"
    7.38 +  using assms has_integral_cmul[of f I A c]
    7.39 +        has_integral_cmul[of "\<lambda>x. c *\<^sub>R f x" "c *\<^sub>R I" A "inverse c"] by (auto simp: field_simps)
    7.40 +
    7.41 +lemma has_integral_affinity':
    7.42 +  fixes a :: "'a::euclidean_space"
    7.43 +  assumes "(f has_integral i) (cbox a b)" and "m > 0"
    7.44 +  shows "((\<lambda>x. f(m *\<^sub>R x + c)) has_integral (i /\<^sub>R m ^ DIM('a)))
    7.45 +           (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))"
    7.46 +proof (cases "cbox a b = {}")
    7.47 +  case True
    7.48 +  hence "(cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)) = {}"
    7.49 +    using \<open>m > 0\<close> unfolding box_eq_empty by (auto simp: algebra_simps)
    7.50 +  with True and assms show ?thesis by simp
    7.51 +next
    7.52 +  case False
    7.53 +  have "((\<lambda>x. f (m *\<^sub>R x + c)) has_integral (1 / \<bar>m\<bar> ^ DIM('a)) *\<^sub>R i)
    7.54 +          ((\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b)"
    7.55 +    using assms by (intro has_integral_affinity) auto
    7.56 +  also have "((\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b) =
    7.57 +               ((\<lambda>x.  - ((1 / m) *\<^sub>R c) + x) ` (\<lambda>x. (1 / m) *\<^sub>R x) ` cbox a b)"
    7.58 +    by (simp add: image_image algebra_simps)
    7.59 +  also have "(\<lambda>x. (1 / m) *\<^sub>R x) ` cbox a b = cbox ((1 / m) *\<^sub>R a) ((1 / m) *\<^sub>R b)" using \<open>m > 0\<close> False
    7.60 +    by (subst image_smult_cbox) simp_all
    7.61 +  also have "(\<lambda>x. - ((1 / m) *\<^sub>R c) + x) ` \<dots> = cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)"
    7.62 +    by (subst cbox_translation [symmetric]) (simp add: field_simps vector_add_divide_simps)
    7.63 +  finally show ?thesis using \<open>m > 0\<close> by (simp add: field_simps)
    7.64 +qed
    7.65 +
    7.66 +lemma has_integral_affinity_iff:
    7.67 +  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: real_normed_vector"
    7.68 +  assumes "m > 0"
    7.69 +  shows   "((\<lambda>x. f (m *\<^sub>R x + c)) has_integral (I /\<^sub>R m ^ DIM('a)))
    7.70 +               (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)) \<longleftrightarrow>
    7.71 +           (f has_integral I) (cbox a b)" (is "?lhs = ?rhs")
    7.72 +proof
    7.73 +  assume ?lhs
    7.74 +  from has_integral_affinity'[OF this, of "1 / m" "-c /\<^sub>R m"] and \<open>m > 0\<close>
    7.75 +    show ?rhs by (simp add: field_simps vector_add_divide_simps)
    7.76 +next
    7.77 +  assume ?rhs
    7.78 +  from has_integral_affinity'[OF this, of m c] and \<open>m > 0\<close>
    7.79 +  show ?lhs by simp
    7.80 +qed
    7.81 +
    7.82 +
    7.83  subsection \<open>Special case of stretching coordinate axes separately\<close>
    7.84  
    7.85  lemma has_integral_stretch:
     8.1 --- a/src/HOL/Analysis/Path_Connected.thy	Sat Aug 04 00:19:23 2018 +0100
     8.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Sat Aug 04 01:03:39 2018 +0200
     8.3 @@ -1177,6 +1177,21 @@
     8.4    unfolding pathfinish_def linepath_def
     8.5    by auto
     8.6  
     8.7 +lemma linepath_inner: "linepath a b x \<bullet> v = linepath (a \<bullet> v) (b \<bullet> v) x"
     8.8 +  by (simp add: linepath_def algebra_simps)
     8.9 +
    8.10 +lemma Re_linepath': "Re (linepath a b x) = linepath (Re a) (Re b) x"
    8.11 +  by (simp add: linepath_def)
    8.12 +
    8.13 +lemma Im_linepath': "Im (linepath a b x) = linepath (Im a) (Im b) x"
    8.14 +  by (simp add: linepath_def)
    8.15 +
    8.16 +lemma linepath_0': "linepath a b 0 = a"
    8.17 +  by (simp add: linepath_def)
    8.18 +
    8.19 +lemma linepath_1': "linepath a b 1 = b"
    8.20 +  by (simp add: linepath_def)
    8.21 +
    8.22  lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)"
    8.23    unfolding linepath_def
    8.24    by (intro continuous_intros)
    8.25 @@ -1200,6 +1215,9 @@
    8.26  lemma linepath_0 [simp]: "linepath 0 b x = x *\<^sub>R b"
    8.27    by (simp add: linepath_def)
    8.28  
    8.29 +lemma linepath_cnj: "cnj (linepath a b x) = linepath (cnj a) (cnj b) x"
    8.30 +  by (simp add: linepath_def)
    8.31 +
    8.32  lemma arc_linepath:
    8.33    assumes "a \<noteq> b" shows [simp]: "arc (linepath a b)"
    8.34  proof -
     9.1 --- a/src/HOL/Analysis/Set_Integral.thy	Sat Aug 04 00:19:23 2018 +0100
     9.2 +++ b/src/HOL/Analysis/Set_Integral.thy	Sat Aug 04 01:03:39 2018 +0200
     9.3 @@ -54,6 +54,15 @@
     9.4    by (auto simp add: indicator_def)
     9.5  *)
     9.6  
     9.7 +lemma set_integrable_cong:
     9.8 +  assumes "M = M'" "A = A'" "\<And>x. x \<in> A \<Longrightarrow> f x = f' x"
     9.9 +  shows   "set_integrable M A f = set_integrable M' A' f'"
    9.10 +proof -
    9.11 +  have "(\<lambda>x. indicator A x *\<^sub>R f x) = (\<lambda>x. indicator A' x *\<^sub>R f' x)"
    9.12 +    using assms by (auto simp: indicator_def)
    9.13 +  thus ?thesis by (simp add: set_integrable_def assms)
    9.14 +qed
    9.15 +
    9.16  lemma set_borel_measurable_sets:
    9.17    fixes f :: "_ \<Rightarrow> _::real_normed_vector"
    9.18    assumes "set_borel_measurable M X f" "B \<in> sets borel" "X \<in> sets M"
    9.19 @@ -925,4 +934,127 @@
    9.20    then show "integrable M (F n)" by (subst integrable_iff_bounded, simp add: assms(1)[of n])
    9.21  qed (auto simp add: assms Limsup_bounded)
    9.22  
    9.23 +lemma tendsto_set_lebesgue_integral_at_right:
    9.24 +  fixes a b :: real and f :: "real \<Rightarrow> 'a :: {banach,second_countable_topology}"
    9.25 +  assumes "a < b" and sets: "\<And>a'. a' \<in> {a<..b} \<Longrightarrow> {a'..b} \<in> sets M"
    9.26 +      and "set_integrable M {a<..b} f"
    9.27 +  shows   "((\<lambda>a'. set_lebesgue_integral M {a'..b} f) \<longlongrightarrow>
    9.28 +             set_lebesgue_integral M {a<..b} f) (at_right a)"
    9.29 +proof (rule tendsto_at_right_sequentially[OF assms(1)], goal_cases)
    9.30 +  case (1 S)
    9.31 +  have eq: "(\<Union>n. {S n..b}) = {a<..b}"
    9.32 +  proof safe
    9.33 +    fix x n assume "x \<in> {S n..b}"
    9.34 +    with 1(1,2)[of n] show "x \<in> {a<..b}" by auto
    9.35 +  next
    9.36 +    fix x assume "x \<in> {a<..b}"
    9.37 +    with order_tendstoD[OF \<open>S \<longlonglongrightarrow> a\<close>, of x] show "x \<in> (\<Union>n. {S n..b})"
    9.38 +      by (force simp: eventually_at_top_linorder dest: less_imp_le)
    9.39 +  qed
    9.40 +  have "(\<lambda>n. set_lebesgue_integral M {S n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M (\<Union>n. {S n..b}) f"
    9.41 +    by (rule set_integral_cont_up) (insert assms 1, auto simp: eq incseq_def decseq_def less_imp_le)
    9.42 +  with eq show ?case by simp
    9.43 +qed
    9.44 +
    9.45 +
    9.46 +text \<open>
    9.47 +  The next lemmas relate convergence of integrals over an interval to
    9.48 +  improper integrals.
    9.49 +\<close>
    9.50 +lemma tendsto_set_lebesgue_integral_at_left:
    9.51 +  fixes a b :: real and f :: "real \<Rightarrow> 'a :: {banach,second_countable_topology}"
    9.52 +  assumes "a < b" and sets: "\<And>b'. b' \<in> {a..<b} \<Longrightarrow> {a..b'} \<in> sets M"
    9.53 +      and "set_integrable M {a..<b} f"
    9.54 +  shows   "((\<lambda>b'. set_lebesgue_integral M {a..b'} f) \<longlongrightarrow>
    9.55 +             set_lebesgue_integral M {a..<b} f) (at_left b)"
    9.56 +proof (rule tendsto_at_left_sequentially[OF assms(1)], goal_cases)
    9.57 +  case (1 S)
    9.58 +  have eq: "(\<Union>n. {a..S n}) = {a..<b}"
    9.59 +  proof safe
    9.60 +    fix x n assume "x \<in> {a..S n}"
    9.61 +    with 1(1,2)[of n] show "x \<in> {a..<b}" by auto
    9.62 +  next
    9.63 +    fix x assume "x \<in> {a..<b}"
    9.64 +    with order_tendstoD[OF \<open>S \<longlonglongrightarrow> b\<close>, of x] show "x \<in> (\<Union>n. {a..S n})"
    9.65 +      by (force simp: eventually_at_top_linorder dest: less_imp_le)
    9.66 +  qed
    9.67 +  have "(\<lambda>n. set_lebesgue_integral M {a..S n} f) \<longlonglongrightarrow> set_lebesgue_integral M (\<Union>n. {a..S n}) f"
    9.68 +    by (rule set_integral_cont_up) (insert assms 1, auto simp: eq incseq_def decseq_def less_imp_le)
    9.69 +  with eq show ?case by simp
    9.70 +qed
    9.71 +
    9.72 +lemma tendsto_set_lebesgue_integral_at_top:
    9.73 +  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
    9.74 +  assumes sets: "\<And>b. b \<ge> a \<Longrightarrow> {a..b} \<in> sets M"
    9.75 +      and int: "set_integrable M {a..} f"
    9.76 +  shows "((\<lambda>b. set_lebesgue_integral M {a..b} f) \<longlongrightarrow> set_lebesgue_integral M {a..} f) at_top"
    9.77 +proof (rule tendsto_at_topI_sequentially)
    9.78 +  fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
    9.79 +  show "(\<lambda>n. set_lebesgue_integral M {a..X n} f) \<longlonglongrightarrow> set_lebesgue_integral M {a..} f"
    9.80 +    unfolding set_lebesgue_integral_def
    9.81 +  proof (rule integral_dominated_convergence)
    9.82 +    show "integrable M (\<lambda>x. indicat_real {a..} x *\<^sub>R norm (f x))"
    9.83 +      using integrable_norm[OF int[unfolded set_integrable_def]] by simp
    9.84 +    show "AE x in M. (\<lambda>n. indicator {a..X n} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {a..} x *\<^sub>R f x"
    9.85 +    proof
    9.86 +      fix x
    9.87 +      from \<open>filterlim X at_top sequentially\<close>
    9.88 +      have "eventually (\<lambda>n. x \<le> X n) sequentially"
    9.89 +        unfolding filterlim_at_top_ge[where c=x] by auto
    9.90 +      then show "(\<lambda>n. indicator {a..X n} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {a..} x *\<^sub>R f x"
    9.91 +        by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
    9.92 +    qed
    9.93 +    fix n show "AE x in M. norm (indicator {a..X n} x *\<^sub>R f x) \<le> 
    9.94 +                             indicator {a..} x *\<^sub>R norm (f x)"
    9.95 +      by (auto split: split_indicator)
    9.96 +  next
    9.97 +    from int show "(\<lambda>x. indicat_real {a..} x *\<^sub>R f x) \<in> borel_measurable M"
    9.98 +      by (simp add: set_integrable_def)
    9.99 +  next
   9.100 +    fix n :: nat
   9.101 +    from sets have "{a..X n} \<in> sets M" by (cases "X n \<ge> a") auto
   9.102 +    with int have "set_integrable M {a..X n} f"
   9.103 +      by (rule set_integrable_subset) auto
   9.104 +    thus "(\<lambda>x. indicat_real {a..X n} x *\<^sub>R f x) \<in> borel_measurable M"
   9.105 +      by (simp add: set_integrable_def)
   9.106 +  qed
   9.107 +qed
   9.108 +
   9.109 +lemma tendsto_set_lebesgue_integral_at_bot:
   9.110 +  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
   9.111 +  assumes sets: "\<And>a. a \<le> b \<Longrightarrow> {a..b} \<in> sets M"
   9.112 +      and int: "set_integrable M {..b} f"
   9.113 +    shows "((\<lambda>a. set_lebesgue_integral M {a..b} f) \<longlongrightarrow> set_lebesgue_integral M {..b} f) at_bot"
   9.114 +proof (rule tendsto_at_botI_sequentially)
   9.115 +  fix X :: "nat \<Rightarrow> real" assume "filterlim X at_bot sequentially"
   9.116 +  show "(\<lambda>n. set_lebesgue_integral M {X n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M {..b} f"
   9.117 +    unfolding set_lebesgue_integral_def
   9.118 +  proof (rule integral_dominated_convergence)
   9.119 +    show "integrable M (\<lambda>x. indicat_real {..b} x *\<^sub>R norm (f x))"
   9.120 +      using integrable_norm[OF int[unfolded set_integrable_def]] by simp
   9.121 +    show "AE x in M. (\<lambda>n. indicator {X n..b} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {..b} x *\<^sub>R f x"
   9.122 +    proof
   9.123 +      fix x
   9.124 +      from \<open>filterlim X at_bot sequentially\<close>
   9.125 +      have "eventually (\<lambda>n. x \<ge> X n) sequentially"
   9.126 +        unfolding filterlim_at_bot_le[where c=x] by auto
   9.127 +      then show "(\<lambda>n. indicator {X n..b} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {..b} x *\<^sub>R f x"
   9.128 +        by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
   9.129 +    qed
   9.130 +    fix n show "AE x in M. norm (indicator {X n..b} x *\<^sub>R f x) \<le> 
   9.131 +                             indicator {..b} x *\<^sub>R norm (f x)"
   9.132 +      by (auto split: split_indicator)
   9.133 +  next
   9.134 +    from int show "(\<lambda>x. indicat_real {..b} x *\<^sub>R f x) \<in> borel_measurable M"
   9.135 +      by (simp add: set_integrable_def)
   9.136 +  next
   9.137 +    fix n :: nat
   9.138 +    from sets have "{X n..b} \<in> sets M" by (cases "X n \<le> b") auto
   9.139 +    with int have "set_integrable M {X n..b} f"
   9.140 +      by (rule set_integrable_subset) auto
   9.141 +    thus "(\<lambda>x. indicat_real {X n..b} x *\<^sub>R f x) \<in> borel_measurable M"
   9.142 +      by (simp add: set_integrable_def)
   9.143 +  qed
   9.144 +qed
   9.145 +
   9.146  end
    10.1 --- a/src/HOL/Archimedean_Field.thy	Sat Aug 04 00:19:23 2018 +0100
    10.2 +++ b/src/HOL/Archimedean_Field.thy	Sat Aug 04 01:03:39 2018 +0200
    10.3 @@ -707,6 +707,9 @@
    10.4  lemma frac_of_int [simp]: "frac (of_int z) = 0"
    10.5    by (simp add: frac_def)
    10.6  
    10.7 +lemma frac_frac [simp]: "frac (frac x) = frac x"
    10.8 +  by (simp add: frac_def)
    10.9 +
   10.10  lemma floor_add: "\<lfloor>x + y\<rfloor> = (if frac x + frac y < 1 then \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> else (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>) + 1)"
   10.11  proof -
   10.12    have "x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>) \<Longrightarrow> \<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
   10.13 @@ -743,6 +746,14 @@
   10.14    apply (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq)
   10.15    done
   10.16  
   10.17 +lemma frac_in_Ints_iff [simp]: "frac x \<in> \<int> \<longleftrightarrow> x \<in> \<int>"
   10.18 +proof safe
   10.19 +  assume "frac x \<in> \<int>"
   10.20 +  hence "of_int \<lfloor>x\<rfloor> + frac x \<in> \<int>" by auto
   10.21 +  also have "of_int \<lfloor>x\<rfloor> + frac x = x" by (simp add: frac_def)
   10.22 +  finally show "x \<in> \<int>" .
   10.23 +qed (auto simp: frac_def)
   10.24 +
   10.25  
   10.26  subsection \<open>Rounding to the nearest integer\<close>
   10.27  
    11.1 --- a/src/HOL/Complex.thy	Sat Aug 04 00:19:23 2018 +0100
    11.2 +++ b/src/HOL/Complex.thy	Sat Aug 04 01:03:39 2018 +0200
    11.3 @@ -623,6 +623,27 @@
    11.4  lemma sums_cnj: "((\<lambda>x. cnj(f x)) sums cnj l) \<longleftrightarrow> (f sums l)"
    11.5    by (simp add: sums_def lim_cnj cnj_sum [symmetric] del: cnj_sum)
    11.6  
    11.7 +lemma differentiable_cnj_iff:
    11.8 +  "(\<lambda>z. cnj (f z)) differentiable at x within A \<longleftrightarrow> f differentiable at x within A"
    11.9 +proof
   11.10 +  assume "(\<lambda>z. cnj (f z)) differentiable at x within A"
   11.11 +  then obtain D where "((\<lambda>z. cnj (f z)) has_derivative D) (at x within A)"
   11.12 +    by (auto simp: differentiable_def)
   11.13 +  from has_derivative_cnj[OF this] show "f differentiable at x within A"
   11.14 +    by (auto simp: differentiable_def)
   11.15 +next
   11.16 +  assume "f differentiable at x within A"
   11.17 +  then obtain D where "(f has_derivative D) (at x within A)"
   11.18 +    by (auto simp: differentiable_def)
   11.19 +  from has_derivative_cnj[OF this] show "(\<lambda>z. cnj (f z)) differentiable at x within A"
   11.20 +    by (auto simp: differentiable_def)
   11.21 +qed
   11.22 +
   11.23 +lemma has_vector_derivative_cnj [derivative_intros]:
   11.24 +  assumes "(f has_vector_derivative f') (at z within A)"
   11.25 +  shows   "((\<lambda>z. cnj (f z)) has_vector_derivative cnj f') (at z within A)"
   11.26 +  using assms by (auto simp: has_vector_derivative_complex_iff intro: derivative_intros)
   11.27 +
   11.28  
   11.29  subsection \<open>Basic Lemmas\<close>
   11.30  
   11.31 @@ -778,9 +799,15 @@
   11.32  lemma sgn_cis [simp]: "sgn (cis a) = cis a"
   11.33    by (simp add: sgn_div_norm)
   11.34  
   11.35 +lemma cis_2pi [simp]: "cis (2 * pi) = 1"
   11.36 +  by (simp add: cis.ctr complex_eq_iff)
   11.37 +
   11.38  lemma cis_neq_zero [simp]: "cis a \<noteq> 0"
   11.39    by (metis norm_cis norm_zero zero_neq_one)
   11.40  
   11.41 +lemma cis_cnj: "cnj (cis t) = cis (-t)"
   11.42 +  by (simp add: complex_eq_iff)
   11.43 +
   11.44  lemma cis_mult: "cis a * cis b = cis (a + b)"
   11.45    by (simp add: complex_eq_iff cos_add sin_add)
   11.46  
   11.47 @@ -802,6 +829,15 @@
   11.48  lemma cis_pi [simp]: "cis pi = -1"
   11.49    by (simp add: complex_eq_iff)
   11.50  
   11.51 +lemma cis_pi_half[simp]: "cis (pi / 2) = \<i>"
   11.52 +  by (simp add: cis.ctr complex_eq_iff)
   11.53 +
   11.54 +lemma cis_minus_pi_half[simp]: "cis (-(pi / 2)) = -\<i>"
   11.55 +  by (simp add: cis.ctr complex_eq_iff)
   11.56 +
   11.57 +lemma cis_multiple_2pi[simp]: "n \<in> \<int> \<Longrightarrow> cis (2 * pi * n) = 1"
   11.58 +  by (auto elim!: Ints_cases simp: cis.ctr one_complex.ctr)
   11.59 +
   11.60  
   11.61  subsubsection \<open>$r(\cos \theta + i \sin \theta)$\<close>
   11.62  
   11.63 @@ -847,6 +883,11 @@
   11.64  
   11.65  subsubsection \<open>Complex exponential\<close>
   11.66  
   11.67 +lemma exp_Reals_eq:
   11.68 +  assumes "z \<in> \<real>"
   11.69 +  shows   "exp z = of_real (exp (Re z))"
   11.70 +  using assms by (auto elim!: Reals_cases simp: exp_of_real)
   11.71 +
   11.72  lemma cis_conv_exp: "cis b = exp (\<i> * b)"
   11.73  proof -
   11.74    have "(\<i> * complex_of_real b) ^ n /\<^sub>R fact n =
   11.75 @@ -901,6 +942,10 @@
   11.76  lemma exp_two_pi_i' [simp]: "exp (\<i> * (of_real pi * 2)) = 1"
   11.77    by (metis exp_two_pi_i mult.commute)
   11.78  
   11.79 +lemma continuous_on_cis [continuous_intros]:
   11.80 +  "continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. cis (f x))"
   11.81 +  by (auto simp: cis_conv_exp intro!: continuous_intros)
   11.82 +
   11.83  
   11.84  subsubsection \<open>Complex argument\<close>
   11.85  
    12.1 --- a/src/HOL/Int.thy	Sat Aug 04 00:19:23 2018 +0100
    12.2 +++ b/src/HOL/Int.thy	Sat Aug 04 01:03:39 2018 +0200
    12.3 @@ -892,6 +892,9 @@
    12.4    apply (rule of_int_minus [symmetric])
    12.5    done
    12.6  
    12.7 +lemma minus_in_Ints_iff: "-x \<in> \<int> \<longleftrightarrow> x \<in> \<int>"
    12.8 +  using Ints_minus[of x] Ints_minus[of "-x"] by auto
    12.9 +
   12.10  lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
   12.11    apply (auto simp add: Ints_def)
   12.12    apply (rule range_eqI)
    13.1 --- a/src/HOL/Limits.thy	Sat Aug 04 00:19:23 2018 +0100
    13.2 +++ b/src/HOL/Limits.thy	Sat Aug 04 01:03:39 2018 +0200
    13.3 @@ -1316,6 +1316,16 @@
    13.4      and filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "\<lambda>x. - f x" F]
    13.5    by auto
    13.6  
    13.7 +lemma tendsto_at_botI_sequentially:
    13.8 +  fixes f :: "real \<Rightarrow> 'b::first_countable_topology"
    13.9 +  assumes *: "\<And>X. filterlim X at_bot sequentially \<Longrightarrow> (\<lambda>n. f (X n)) \<longlonglongrightarrow> y"
   13.10 +  shows "(f \<longlongrightarrow> y) at_bot"
   13.11 +  unfolding filterlim_at_bot_mirror
   13.12 +proof (rule tendsto_at_topI_sequentially)
   13.13 +  fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
   13.14 +  thus "(\<lambda>n. f (-X n)) \<longlonglongrightarrow> y" by (intro *) (auto simp: filterlim_uminus_at_top)
   13.15 +qed
   13.16 +
   13.17  lemma filterlim_at_infinity_imp_filterlim_at_top:
   13.18    assumes "filterlim (f :: 'a \<Rightarrow> real) at_infinity F"
   13.19    assumes "eventually (\<lambda>x. f x > 0) F"
    14.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sat Aug 04 00:19:23 2018 +0100
    14.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Sat Aug 04 01:03:39 2018 +0200
    14.3 @@ -1012,6 +1012,9 @@
    14.4  lemma dist_triangle3: "dist x y \<le> dist a x + dist a y"
    14.5    using dist_triangle2 [of x y a] by (simp add: dist_commute)
    14.6  
    14.7 +lemma abs_dist_diff_le: "\<bar>dist a b - dist b c\<bar> \<le> dist a c"
    14.8 +  using dist_triangle3[of b c a] dist_triangle2[of a b c] by simp
    14.9 +
   14.10  lemma dist_pos_lt: "x \<noteq> y \<Longrightarrow> 0 < dist x y"
   14.11    by (simp add: zero_less_dist_iff)
   14.12  
    15.1 --- a/src/HOL/Series.thy	Sat Aug 04 00:19:23 2018 +0100
    15.2 +++ b/src/HOL/Series.thy	Sat Aug 04 01:03:39 2018 +0200
    15.3 @@ -703,6 +703,27 @@
    15.4    qed
    15.5  qed
    15.6  
    15.7 +lemma summable_Cauchy':
    15.8 +  fixes f :: "nat \<Rightarrow> 'a :: banach"
    15.9 +  assumes "eventually (\<lambda>m. \<forall>n\<ge>m. norm (sum f {m..<n}) \<le> g m) sequentially"
   15.10 +  assumes "filterlim g (nhds 0) sequentially"
   15.11 +  shows "summable f"
   15.12 +proof (subst summable_Cauchy, intro allI impI, goal_cases)
   15.13 +  case (1 e)
   15.14 +  from order_tendstoD(2)[OF assms(2) this] and assms(1)
   15.15 +  have "eventually (\<lambda>m. \<forall>n. norm (sum f {m..<n}) < e) at_top"
   15.16 +  proof eventually_elim
   15.17 +    case (elim m)
   15.18 +    show ?case
   15.19 +    proof
   15.20 +      fix n
   15.21 +      from elim show "norm (sum f {m..<n}) < e"
   15.22 +        by (cases "n \<ge> m") auto
   15.23 +    qed
   15.24 +  qed
   15.25 +  thus ?case by (auto simp: eventually_at_top_linorder)
   15.26 +qed
   15.27 +
   15.28  context
   15.29    fixes f :: "nat \<Rightarrow> 'a::banach"
   15.30  begin
    16.1 --- a/src/HOL/Topological_Spaces.thy	Sat Aug 04 00:19:23 2018 +0100
    16.2 +++ b/src/HOL/Topological_Spaces.thy	Sat Aug 04 01:03:39 2018 +0200
    16.3 @@ -2131,6 +2131,9 @@
    16.4  lemma isCont_def: "isCont f a \<longleftrightarrow> f \<midarrow>a\<rightarrow> f a"
    16.5    by (rule continuous_at)
    16.6  
    16.7 +lemma isContD: "isCont f x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x"
    16.8 +  by (simp add: isCont_def)
    16.9 +
   16.10  lemma isCont_cong:
   16.11    assumes "eventually (\<lambda>x. f x = g x) (nhds x)"
   16.12    shows "isCont f x \<longleftrightarrow> isCont g x"