# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1533337419 -7200
# Node ID 53ad5c01be3f5526420e1c560e539dedf6615873
# Parent  1e1818612124035fe9fcbf1ecd87ae5aec929293
Small lemmas about analysis

diff -r 1e1818612124 -r 53ad5c01be3f src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat Aug 04 01:03:39 2018 +0200
@@ -1341,6 +1341,29 @@
 lemma contour_integral_trivial [simp]: "contour_integral (linepath a a) f = 0"
   using has_contour_integral_trivial contour_integral_unique by blast
 
+lemma differentiable_linepath [intro]: "linepath a b differentiable at x within A"
+  by (auto simp: linepath_def)
+
+lemma bounded_linear_linepath:
+  assumes "bounded_linear f"
+  shows   "f (linepath a b x) = linepath (f a) (f b) x"
+proof -
+  interpret f: bounded_linear f by fact
+  show ?thesis by (simp add: linepath_def f.add f.scale)
+qed
+
+lemma bounded_linear_linepath':
+  assumes "bounded_linear f"
+  shows   "f \<circ> linepath a b = linepath (f a) (f b)"
+  using bounded_linear_linepath[OF assms] by (simp add: fun_eq_iff)
+
+lemma cnj_linepath: "cnj (linepath a b x) = linepath (cnj a) (cnj b) x"
+  by (simp add: linepath_def)
+
+lemma cnj_linepath': "cnj \<circ> linepath a b = linepath (cnj a) (cnj b)"
+  by (simp add: linepath_def fun_eq_iff)
+
+
 
 subsection\<open>Relation to subpath construction\<close>
 
@@ -1501,6 +1524,62 @@
      "contour_integral g f = integral {0..1} (\<lambda>x. f (g x) * vector_derivative g (at x))"
   by (simp add: contour_integral_def integral_def has_contour_integral contour_integrable_on)
 
+lemma contour_integral_cong:
+  assumes "g = g'" "\<And>x. x \<in> path_image g \<Longrightarrow> f x = f' x"
+  shows   "contour_integral g f = contour_integral g' f'"
+  unfolding contour_integral_integral using assms
+  by (intro integral_cong) (auto simp: path_image_def)
+
+
+text \<open>Contour integral along a segment on the real axis\<close>
+
+lemma has_contour_integral_linepath_Reals_iff:
+  fixes a b :: complex and f :: "complex \<Rightarrow> complex"
+  assumes "a \<in> Reals" "b \<in> Reals" "Re a < Re b"
+  shows   "(f has_contour_integral I) (linepath a b) \<longleftrightarrow>
+             ((\<lambda>x. f (of_real x)) has_integral I) {Re a..Re b}"
+proof -
+  from assms have [simp]: "of_real (Re a) = a" "of_real (Re b) = b"
+    by (simp_all add: complex_eq_iff)
+  from assms have "a \<noteq> b" by auto
+  have "((\<lambda>x. f (of_real x)) has_integral I) (cbox (Re a) (Re b)) \<longleftrightarrow>
+          ((\<lambda>x. f (a + b * of_real x - a * of_real x)) has_integral I /\<^sub>R (Re b - Re a)) {0..1}"
+    by (subst has_integral_affinity_iff [of "Re b - Re a" _ "Re a", symmetric])
+       (insert assms, simp_all add: field_simps scaleR_conv_of_real)
+  also have "(\<lambda>x. f (a + b * of_real x - a * of_real x)) =
+               (\<lambda>x. (f (a + b * of_real x - a * of_real x) * (b - a)) /\<^sub>R (Re b - Re a))"
+    using \<open>a \<noteq> b\<close> by (auto simp: field_simps fun_eq_iff scaleR_conv_of_real)
+  also have "(\<dots> has_integral I /\<^sub>R (Re b - Re a)) {0..1} \<longleftrightarrow> 
+               ((\<lambda>x. f (linepath a b x) * (b - a)) has_integral I) {0..1}" using assms
+    by (subst has_integral_cmul_iff) (auto simp: linepath_def scaleR_conv_of_real algebra_simps)
+  also have "\<dots> \<longleftrightarrow> (f has_contour_integral I) (linepath a b)" unfolding has_contour_integral_def
+    by (intro has_integral_cong) (simp add: vector_derivative_linepath_within)
+  finally show ?thesis by simp
+qed
+
+lemma contour_integrable_linepath_Reals_iff:
+  fixes a b :: complex and f :: "complex \<Rightarrow> complex"
+  assumes "a \<in> Reals" "b \<in> Reals" "Re a < Re b"
+  shows   "(f contour_integrable_on linepath a b) \<longleftrightarrow>
+             (\<lambda>x. f (of_real x)) integrable_on {Re a..Re b}"
+  using has_contour_integral_linepath_Reals_iff[OF assms, of f]
+  by (auto simp: contour_integrable_on_def integrable_on_def)
+
+lemma contour_integral_linepath_Reals_eq:
+  fixes a b :: complex and f :: "complex \<Rightarrow> complex"
+  assumes "a \<in> Reals" "b \<in> Reals" "Re a < Re b"
+  shows   "contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (of_real x))"
+proof (cases "f contour_integrable_on linepath a b")
+  case True
+  thus ?thesis using has_contour_integral_linepath_Reals_iff[OF assms, of f]
+    using has_contour_integral_integral has_contour_integral_unique by blast
+next
+  case False
+  thus ?thesis using contour_integrable_linepath_Reals_iff[OF assms, of f]
+    by (simp add: not_integrable_contour_integral not_integrable_integral)
+qed
+
+
 
 text\<open>Cauchy's theorem where there's a primitive\<close>
 
@@ -4875,6 +4954,10 @@
   apply (rule derivative_eq_intros | simp)+
   done
 
+corollary differentiable_part_circlepath:
+  "part_circlepath c r a b differentiable at x within A"
+  using has_vector_derivative_part_circlepath[of c r a b x A] differentiableI_vector by blast
+
 corollary vector_derivative_part_circlepath:
     "vector_derivative (part_circlepath z r s t) (at x) =
        \<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)"
@@ -4923,6 +5006,17 @@
     by (fastforce simp add: path_image_def part_circlepath_def)
 qed
 
+proposition path_image_part_circlepath':
+  "path_image (part_circlepath z r s t) = (\<lambda>x. z + r * cis x) ` closed_segment s t"
+proof -
+  have "path_image (part_circlepath z r s t) = 
+          (\<lambda>x. z + r * exp(\<i> * of_real x)) ` linepath s t ` {0..1}"
+    by (simp add: image_image path_image_def part_circlepath_def)
+  also have "linepath s t ` {0..1} = closed_segment s t"
+    by (rule linepath_image_01)
+  finally show ?thesis by (simp add: cis_conv_exp)
+qed
+
 corollary path_image_part_circlepath_subset:
     "\<lbrakk>s \<le> t; 0 \<le> r\<rbrakk> \<Longrightarrow> path_image(part_circlepath z r s t) \<subseteq> sphere z r"
 by (auto simp: path_image_part_circlepath sphere_def dist_norm algebra_simps norm_mult)
@@ -4937,6 +5031,106 @@
     by (simp add: dist_norm norm_minus_commute)
 qed
 
+corollary path_image_part_circlepath_subset':
+  assumes "r \<ge> 0"
+  shows   "path_image (part_circlepath z r s t) \<subseteq> sphere z r"
+proof (cases "s \<le> t")
+  case True
+  thus ?thesis using path_image_part_circlepath_subset[of s t r z] assms by simp
+next
+  case False
+  thus ?thesis using path_image_part_circlepath_subset[of t s r z] assms
+    by (subst reversepath_part_circlepath [symmetric], subst path_image_reversepath) simp_all
+qed
+
+lemma part_circlepath_cnj: "cnj (part_circlepath c r a b x) = part_circlepath (cnj c) r (-a) (-b) x"
+  by (simp add: part_circlepath_def exp_cnj linepath_def algebra_simps)
+
+lemma contour_integral_bound_part_circlepath:
+  assumes "f contour_integrable_on part_circlepath c r a b"
+  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"
+  shows   "norm (contour_integral (part_circlepath c r a b) f) \<le> B * r * \<bar>b - a\<bar>"
+proof -
+  let ?I = "integral {0..1} (\<lambda>x. f (part_circlepath c r a b x) * \<i> * of_real (r * (b - a)) *
+              exp (\<i> * linepath a b x))"
+  have "norm ?I \<le> integral {0..1} (\<lambda>x::real. B * 1 * (r * \<bar>b - a\<bar>) * 1)"
+  proof (rule integral_norm_bound_integral, goal_cases)
+    case 1
+    with assms(1) show ?case
+      by (simp add: contour_integrable_on vector_derivative_part_circlepath mult_ac)
+  next
+    case (3 x)
+    with assms(2-) show ?case unfolding norm_mult norm_of_real abs_mult
+      by (intro mult_mono) (auto simp: path_image_def)
+  qed auto
+  also have "?I = contour_integral (part_circlepath c r a b) f"
+    by (simp add: contour_integral_integral vector_derivative_part_circlepath mult_ac)
+  finally show ?thesis by simp
+qed
+
+lemma has_contour_integral_part_circlepath_iff:
+  assumes "a < b"
+  shows "(f has_contour_integral I) (part_circlepath c r a b) \<longleftrightarrow>
+           ((\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) has_integral I) {a..b}"
+proof -
+  have "(f has_contour_integral I) (part_circlepath c r a b) \<longleftrightarrow>
+          ((\<lambda>x. f (part_circlepath c r a b x) * vector_derivative (part_circlepath c r a b)
+           (at x within {0..1})) has_integral I) {0..1}"
+    unfolding has_contour_integral_def ..
+  also have "\<dots> \<longleftrightarrow> ((\<lambda>x. f (part_circlepath c r a b x) * r * (b - a) * \<i> *
+                            cis (linepath a b x)) has_integral I) {0..1}"
+    by (intro has_integral_cong, subst vector_derivative_part_circlepath01)
+       (simp_all add: cis_conv_exp)
+  also have "\<dots> \<longleftrightarrow> ((\<lambda>x. f (c + r * exp (\<i> * linepath (of_real a) (of_real b) x)) *
+                       r * \<i> * exp (\<i> * linepath (of_real a) (of_real b) x) *
+                       vector_derivative (linepath (of_real a) (of_real b)) 
+                         (at x within {0..1})) has_integral I) {0..1}"
+    by (intro has_integral_cong, subst vector_derivative_linepath_within)
+       (auto simp: part_circlepath_def cis_conv_exp of_real_linepath [symmetric])
+  also have "\<dots> \<longleftrightarrow> ((\<lambda>z. f (c + r * exp (\<i> * z)) * r * \<i> * exp (\<i> * z)) has_contour_integral I)
+                      (linepath (of_real a) (of_real b))"
+    by (simp add: has_contour_integral_def)
+  also have "\<dots> \<longleftrightarrow> ((\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) has_integral I) {a..b}" using assms
+    by (subst has_contour_integral_linepath_Reals_iff) (simp_all add: cis_conv_exp)
+  finally show ?thesis .
+qed
+
+lemma contour_integrable_part_circlepath_iff:
+  assumes "a < b"
+  shows "f contour_integrable_on (part_circlepath c r a b) \<longleftrightarrow>
+           (\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}"
+  using assms by (auto simp: contour_integrable_on_def integrable_on_def 
+                             has_contour_integral_part_circlepath_iff)
+
+lemma contour_integral_part_circlepath_eq:
+  assumes "a < b"
+  shows "contour_integral (part_circlepath c r a b) f =
+           integral {a..b} (\<lambda>t. f (c + r * cis t) * r * \<i> * cis t)"
+proof (cases "f contour_integrable_on part_circlepath c r a b")
+  case True
+  hence "(\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}" 
+    using assms by (simp add: contour_integrable_part_circlepath_iff)
+  with True show ?thesis
+    using has_contour_integral_part_circlepath_iff[OF assms]
+          contour_integral_unique has_integral_integrable_integral by blast
+next
+  case False
+  hence "\<not>(\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}" 
+    using assms by (simp add: contour_integrable_part_circlepath_iff)
+  with False show ?thesis
+    by (simp add: not_integrable_contour_integral not_integrable_integral)
+qed
+
+lemma contour_integral_part_circlepath_reverse:
+  "contour_integral (part_circlepath c r a b) f = -contour_integral (part_circlepath c r b a) f"
+  by (subst reversepath_part_circlepath [symmetric], subst contour_integral_reversepath) simp_all
+
+lemma contour_integral_part_circlepath_reverse':
+  "b < a \<Longrightarrow> contour_integral (part_circlepath c r a b) f = 
+               -contour_integral (part_circlepath c r b a) f"
+  by (rule contour_integral_part_circlepath_reverse)
+
+
 proposition finite_bounded_log: "finite {z::complex. norm z \<le> b \<and> exp z = w}"
 proof (cases "w = 0")
   case True then show ?thesis by auto
diff -r 1e1818612124 -r 53ad5c01be3f src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat Aug 04 01:03:39 2018 +0200
@@ -41,6 +41,24 @@
 lemma linear_cnj: "linear cnj"
   using bounded_linear.linear[OF bounded_linear_cnj] .
 
+lemma vector_derivative_cnj_within:
+  assumes "at x within A \<noteq> bot" and "f differentiable at x within A"
+  shows   "vector_derivative (\<lambda>z. cnj (f z)) (at x within A) = 
+             cnj (vector_derivative f (at x within A))" (is "_ = cnj ?D")
+proof -
+  let ?D = "vector_derivative f (at x within A)"
+  from assms have "(f has_vector_derivative ?D) (at x within A)"
+    by (subst (asm) vector_derivative_works)
+  hence "((\<lambda>x. cnj (f x)) has_vector_derivative cnj ?D) (at x within A)"
+    by (rule has_vector_derivative_cnj)
+  thus ?thesis using assms by (auto dest: vector_derivative_within)
+qed
+
+lemma vector_derivative_cnj:
+  assumes "f differentiable at x"
+  shows   "vector_derivative (\<lambda>z. cnj (f z)) (at x) = cnj (vector_derivative f (at x))"
+  using assms by (intro vector_derivative_cnj_within) auto
+
 lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = ( * ) 0"
   by auto
 
@@ -286,6 +304,35 @@
   "f holomorphic_on s \<Longrightarrow> g holomorphic_on t \<Longrightarrow> f ` s \<subseteq> t \<Longrightarrow> (g o f) holomorphic_on s"
   by (metis holomorphic_on_compose holomorphic_on_subset)
 
+lemma holomorphic_on_balls_imp_entire:
+  assumes "\<not>bdd_above A" "\<And>r. r \<in> A \<Longrightarrow> f holomorphic_on ball c r"
+  shows   "f holomorphic_on B"
+proof (rule holomorphic_on_subset)
+  show "f holomorphic_on UNIV" unfolding holomorphic_on_def
+  proof
+    fix z :: complex
+    from \<open>\<not>bdd_above A\<close> obtain r where r: "r \<in> A" "r > norm (z - c)"
+      by (meson bdd_aboveI not_le)
+    with assms(2) have "f holomorphic_on ball c r" by blast
+    moreover from r have "z \<in> ball c r" by (auto simp: dist_norm norm_minus_commute)
+    ultimately show "f field_differentiable at z"
+      by (auto simp: holomorphic_on_def at_within_open[of _ "ball c r"])
+  qed
+qed auto
+
+lemma holomorphic_on_balls_imp_entire':
+  assumes "\<And>r. r > 0 \<Longrightarrow> f holomorphic_on ball c r"
+  shows   "f holomorphic_on B"
+proof (rule holomorphic_on_balls_imp_entire)
+  {
+    fix M :: real
+    have "\<exists>x. x > max M 0" by (intro gt_ex)
+    hence "\<exists>x>0. x > M" by auto
+  }
+  thus "\<not>bdd_above {(0::real)<..}" unfolding bdd_above_def
+    by (auto simp: not_le)
+qed (insert assms, auto)
+
 lemma holomorphic_on_minus [holomorphic_intros]: "f holomorphic_on s \<Longrightarrow> (\<lambda>z. -(f z)) holomorphic_on s"
   by (metis field_differentiable_minus holomorphic_on_def)
 
diff -r 1e1818612124 -r 53ad5c01be3f src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sat Aug 04 01:03:39 2018 +0200
@@ -176,6 +176,16 @@
 lemma holomorphic_on_cos: "cos holomorphic_on S"
   by (simp add: field_differentiable_within_cos holomorphic_on_def)
 
+lemma holomorphic_on_sin' [holomorphic_intros]:
+  assumes "f holomorphic_on A"
+  shows   "(\<lambda>x. sin (f x)) holomorphic_on A"
+  using holomorphic_on_compose[OF assms holomorphic_on_sin] by (simp add: o_def)
+
+lemma holomorphic_on_cos' [holomorphic_intros]:
+  assumes "f holomorphic_on A"
+  shows   "(\<lambda>x. cos (f x)) holomorphic_on A"
+  using holomorphic_on_compose[OF assms holomorphic_on_cos] by (simp add: o_def)
+
 subsection\<open>Get a nice real/imaginary separation in Euler's formula\<close>
 
 lemma Euler: "exp(z) = of_real(exp(Re z)) *
@@ -1308,6 +1318,11 @@
 lemma holomorphic_on_Ln [holomorphic_intros]: "(\<And>z. z \<in> S \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on S"
   by (simp add: field_differentiable_within_Ln holomorphic_on_def)
 
+lemma holomorphic_on_Ln' [holomorphic_intros]:
+  "(\<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"
+  using holomorphic_on_compose_gen[OF _ holomorphic_on_Ln, of f A "- \<real>\<^sub>\<le>\<^sub>0"]
+  by (auto simp: o_def)
+
 lemma tendsto_Ln [tendsto_intros]:
   fixes L F
   assumes "(f \<longlongrightarrow> L) F" "L \<notin> \<real>\<^sub>\<le>\<^sub>0"
diff -r 1e1818612124 -r 53ad5c01be3f src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Aug 04 01:03:39 2018 +0200
@@ -4612,6 +4612,93 @@
     unfolding absolutely_integrable_restrict_UNIV .
 qed
 
+lemma uniform_limit_set_lebesgue_integral_at_top:
+  fixes f :: "'a \<Rightarrow> real \<Rightarrow> 'b::{banach, second_countable_topology}"
+    and g :: "real \<Rightarrow> real"
+  assumes bound: "\<And>x y. x \<in> A \<Longrightarrow> y \<ge> a \<Longrightarrow> norm (f x y) \<le> g y"
+  assumes integrable: "set_integrable M {a..} g"
+  assumes measurable: "\<And>x. x \<in> A \<Longrightarrow> set_borel_measurable M {a..} (f x)"
+  assumes "sets borel \<subseteq> sets M"
+  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"
+proof (cases "A = {}")
+  case False
+  then obtain x where x: "x \<in> A" by auto
+  have g_nonneg: "g y \<ge> 0" if "y \<ge> a" for y
+  proof -
+    have "0 \<le> norm (f x y)" by simp
+    also have "\<dots> \<le> g y" using bound[OF x that] by simp
+    finally show ?thesis .
+  qed
+
+  have integrable': "set_integrable M {a..} (\<lambda>y. f x y)" if "x \<in> A" for x
+    unfolding set_integrable_def
+  proof (rule Bochner_Integration.integrable_bound)
+    show "integrable M (\<lambda>x. indicator {a..} x * g x)"
+      using integrable by (simp add: set_integrable_def)
+    show "(\<lambda>y. indicat_real {a..} y *\<^sub>R f x y) \<in> borel_measurable M" using measurable[OF that]
+      by (simp add: set_borel_measurable_def)
+    show "AE y in M. norm (indicat_real {a..} y *\<^sub>R f x y) \<le> norm (indicat_real {a..} y * g y)"
+      using bound[OF that] by (intro AE_I2) (auto simp: indicator_def g_nonneg)
+  qed
+
+  show ?thesis
+  proof (rule uniform_limitI)
+    fix e :: real assume e: "e > 0"
+    have sets [intro]: "A \<in> sets M" if "A \<in> sets borel" for A
+      using that assms by blast
+  
+    have "((\<lambda>b. LINT y:{a..b}|M. g y) \<longlongrightarrow> (LINT y:{a..}|M. g y)) at_top"
+      by (intro tendsto_set_lebesgue_integral_at_top assms sets) auto
+    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"
+      by (auto simp: tendsto_iff eventually_at_top_linorder dist_real_def abs_minus_commute)
+    define b where "b = max a b0"
+    have "a \<le> b" by (simp add: b_def)
+    from b0 have "\<bar>(LINT y:{a..}|M. g y) - (LINT y:{a..b}|M. g y)\<bar> < e"
+      by (auto simp: b_def)
+    also have "{a..} = {a..b} \<union> {b<..}" by (auto simp: b_def)
+    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>"
+      using \<open>a \<le> b\<close> by (subst set_integral_Un) (auto intro!: set_integrable_subset[OF integrable])
+    also have "(LINT y:{b<..}|M. g y) \<ge> 0"
+      using g_nonneg \<open>a \<le> b\<close> unfolding set_lebesgue_integral_def
+      by (intro Bochner_Integration.integral_nonneg) (auto simp: indicator_def)
+    hence "\<bar>(LINT y:{b<..}|M. g y)\<bar> = (LINT y:{b<..}|M. g y)" by simp
+    finally have less: "(LINT y:{b<..}|M. g y) < e" .
+
+    have "eventually (\<lambda>b. b \<ge> b0) at_top" by (rule eventually_ge_at_top)
+    moreover have "eventually (\<lambda>b. b \<ge> a) at_top" by (rule eventually_ge_at_top)
+    ultimately show "eventually (\<lambda>b. \<forall>x\<in>A. 
+                       dist (LINT y:{a..b}|M. f x y) (LINT y:{a..}|M. f x y) < e) at_top"
+    proof eventually_elim
+      case (elim b)
+      show ?case
+      proof
+        fix x assume x: "x \<in> A"
+        have "dist (LINT y:{a..b}|M. f x y) (LINT y:{a..}|M. f x y) =
+                norm ((LINT y:{a..}|M. f x y) - (LINT y:{a..b}|M. f x y))"
+          by (simp add: dist_norm norm_minus_commute)
+        also have "{a..} = {a..b} \<union> {b<..}" using elim by auto
+        also have "(LINT y:\<dots>|M. f x y) - (LINT y:{a..b}|M. f x y) = (LINT y:{b<..}|M. f x y)"
+          using elim x
+          by (subst set_integral_Un) (auto intro!: set_integrable_subset[OF integrable'])
+        also have "norm \<dots> \<le> (LINT y:{b<..}|M. norm (f x y))" using elim x
+          by (intro set_integral_norm_bound set_integrable_subset[OF integrable']) auto
+        also have "\<dots> \<le> (LINT y:{b<..}|M. g y)" using elim x bound g_nonneg
+          by (intro set_integral_mono set_integrable_norm set_integrable_subset[OF integrable']
+                    set_integrable_subset[OF integrable]) auto
+        also have "(LINT y:{b<..}|M. g y) \<ge> 0"
+          using g_nonneg \<open>a \<le> b\<close> unfolding set_lebesgue_integral_def
+          by (intro Bochner_Integration.integral_nonneg) (auto simp: indicator_def)
+        hence "(LINT y:{b<..}|M. g y) = \<bar>(LINT y:{b<..}|M. g y)\<bar>" by simp
+        also have "\<dots> = \<bar>(LINT y:{a..b} \<union> {b<..}|M. g y) - (LINT y:{a..b}|M. g y)\<bar>"
+          using elim by (subst set_integral_Un) (auto intro!: set_integrable_subset[OF integrable])
+        also have "{a..b} \<union> {b<..} = {a..}" using elim by auto
+        also have "\<bar>(LINT y:{a..}|M. g y) - (LINT y:{a..b}|M. g y)\<bar> < e"
+          using b0 elim by blast
+        finally show "dist (LINT y:{a..b}|M. f x y) (LINT y:{a..}|M. f x y) < e" .
+      qed
+    qed
+  qed
+qed auto
 
 
 
diff -r 1e1818612124 -r 53ad5c01be3f src/HOL/Analysis/FPS_Convergence.thy
--- a/src/HOL/Analysis/FPS_Convergence.thy	Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/FPS_Convergence.thy	Sat Aug 04 01:03:39 2018 +0200
@@ -193,6 +193,24 @@
     by (subst analytic_on_open) auto
 qed
 
+lemma continuous_eval_fps [continuous_intros]:
+  fixes z :: "'a::{real_normed_field,banach}"
+  assumes "norm z < fps_conv_radius F"
+  shows   "continuous (at z within A) (eval_fps F)"
+proof -
+  from ereal_dense2[OF assms] obtain K :: real where K: "norm z < K" "K < fps_conv_radius F"
+    by auto
+  have "0 \<le> norm z" by simp
+  also have "norm z < K" by fact
+  finally have "K > 0" .
+  from K and \<open>K > 0\<close> have "summable (\<lambda>n. fps_nth F n * of_real K ^ n)"
+    by (intro summable_fps) auto
+  from this have "isCont (eval_fps F) z" unfolding eval_fps_def
+    by (rule isCont_powser) (use K in auto)
+  thus "continuous (at z within A)  (eval_fps F)"
+    by (simp add: continuous_at_imp_continuous_within)
+qed
+
 
 subsection%unimportant \<open>Lower bounds on radius of convergence\<close>
 
@@ -831,6 +849,20 @@
   ultimately show ?thesis using r(1) by (auto simp: has_fps_expansion_def)
 qed
 
+lemma has_fps_expansion_imp_continuous:
+  fixes F :: "'a::{real_normed_field,banach} fps"
+  assumes "f has_fps_expansion F"
+  shows   "continuous (at 0 within A) f"
+proof -
+  from assms have "isCont (eval_fps F) 0"
+    by (intro continuous_eval_fps) (auto simp: has_fps_expansion_def zero_ereal_def)
+  also have "?this \<longleftrightarrow> isCont f 0" using assms
+    by (intro isCont_cong) (auto simp: has_fps_expansion_def)
+  finally have "isCont f 0" .
+  thus "continuous (at 0 within A) f"
+    by (simp add: continuous_at_imp_continuous_within)
+qed
+
 lemma has_fps_expansion_const [simp, intro, fps_expansion_intros]:
   "(\<lambda>_. c) has_fps_expansion fps_const c"
   by (auto simp: has_fps_expansion_def)
diff -r 1e1818612124 -r 53ad5c01be3f src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy	Sat Aug 04 01:03:39 2018 +0200
@@ -1457,6 +1457,15 @@
 lemma holomorphic_rGamma [holomorphic_intros]: "rGamma holomorphic_on A"
   unfolding holomorphic_on_def by (auto intro!: field_differentiable_rGamma)
 
+lemma holomorphic_rGamma' [holomorphic_intros]: 
+  assumes "f holomorphic_on A"
+  shows   "(\<lambda>x. rGamma (f x)) holomorphic_on A"
+proof -
+  have "rGamma \<circ> f holomorphic_on A" using assms
+    by (intro holomorphic_on_compose assms holomorphic_rGamma)
+  thus ?thesis by (simp only: o_def)
+qed
+
 lemma analytic_rGamma: "rGamma analytic_on A"
   unfolding analytic_on_def by (auto intro!: exI[of _ 1] holomorphic_rGamma)
 
@@ -1467,6 +1476,15 @@
 lemma holomorphic_Gamma [holomorphic_intros]: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma holomorphic_on A"
   unfolding holomorphic_on_def by (auto intro!: field_differentiable_Gamma)
 
+lemma holomorphic_Gamma' [holomorphic_intros]: 
+  assumes "f holomorphic_on A" and "\<And>x. x \<in> A \<Longrightarrow> f x \<notin> \<int>\<^sub>\<le>\<^sub>0"
+  shows   "(\<lambda>x. Gamma (f x)) holomorphic_on A"
+proof -
+  have "Gamma \<circ> f holomorphic_on A" using assms
+    by (intro holomorphic_on_compose assms holomorphic_Gamma) auto
+  thus ?thesis by (simp only: o_def)
+qed
+
 lemma analytic_Gamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma analytic_on A"
   by (rule analytic_on_subset[of _ "UNIV - \<int>\<^sub>\<le>\<^sub>0"], subst analytic_on_open)
      (auto intro!: holomorphic_Gamma)
diff -r 1e1818612124 -r 53ad5c01be3f src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Aug 04 01:03:39 2018 +0200
@@ -687,6 +687,17 @@
   apply (simp_all add: integrable_integral integrable_linear has_integral_linear )
   done
 
+lemma integrable_on_cnj_iff:
+  "(\<lambda>x. cnj (f x)) integrable_on A \<longleftrightarrow> f integrable_on A"
+  using integrable_linear[OF _ bounded_linear_cnj, of f A]
+        integrable_linear[OF _ bounded_linear_cnj, of "cnj \<circ> f" A]
+  by (auto simp: o_def)
+
+lemma integral_cnj: "cnj (integral A f) = integral A (\<lambda>x. cnj (f x))"
+  by (cases "f integrable_on A")
+     (simp_all add: integral_linear[OF _ bounded_linear_cnj, symmetric]
+                    o_def integrable_on_cnj_iff not_integrable_integral)
+
 lemma integral_component_eq[simp]:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   assumes "f integrable_on S"
@@ -3440,6 +3451,64 @@
 
 lemmas has_integral_affinity01 = has_integral_affinity [of _ _ 0 "1::real", simplified]
 
+lemma integrable_on_affinity:
+  assumes "m \<noteq> 0" "f integrable_on (cbox a b)"
+  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)"
+proof -
+  from assms obtain I where "(f has_integral I) (cbox a b)"
+    by (auto simp: integrable_on_def)
+  from has_integral_affinity[OF this assms(1), of c] show ?thesis
+    by (auto simp: integrable_on_def)
+qed
+
+lemma has_integral_cmul_iff:
+  assumes "c \<noteq> 0"
+  shows   "((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R I)) A \<longleftrightarrow> (f has_integral I) A"
+  using assms has_integral_cmul[of f I A c]
+        has_integral_cmul[of "\<lambda>x. c *\<^sub>R f x" "c *\<^sub>R I" A "inverse c"] by (auto simp: field_simps)
+
+lemma has_integral_affinity':
+  fixes a :: "'a::euclidean_space"
+  assumes "(f has_integral i) (cbox a b)" and "m > 0"
+  shows "((\<lambda>x. f(m *\<^sub>R x + c)) has_integral (i /\<^sub>R m ^ DIM('a)))
+           (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))"
+proof (cases "cbox a b = {}")
+  case True
+  hence "(cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)) = {}"
+    using \<open>m > 0\<close> unfolding box_eq_empty by (auto simp: algebra_simps)
+  with True and assms show ?thesis by simp
+next
+  case False
+  have "((\<lambda>x. f (m *\<^sub>R x + c)) has_integral (1 / \<bar>m\<bar> ^ DIM('a)) *\<^sub>R i)
+          ((\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b)"
+    using assms by (intro has_integral_affinity) auto
+  also have "((\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b) =
+               ((\<lambda>x.  - ((1 / m) *\<^sub>R c) + x) ` (\<lambda>x. (1 / m) *\<^sub>R x) ` cbox a b)"
+    by (simp add: image_image algebra_simps)
+  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
+    by (subst image_smult_cbox) simp_all
+  also have "(\<lambda>x. - ((1 / m) *\<^sub>R c) + x) ` \<dots> = cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)"
+    by (subst cbox_translation [symmetric]) (simp add: field_simps vector_add_divide_simps)
+  finally show ?thesis using \<open>m > 0\<close> by (simp add: field_simps)
+qed
+
+lemma has_integral_affinity_iff:
+  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: real_normed_vector"
+  assumes "m > 0"
+  shows   "((\<lambda>x. f (m *\<^sub>R x + c)) has_integral (I /\<^sub>R m ^ DIM('a)))
+               (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)) \<longleftrightarrow>
+           (f has_integral I) (cbox a b)" (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  from has_integral_affinity'[OF this, of "1 / m" "-c /\<^sub>R m"] and \<open>m > 0\<close>
+    show ?rhs by (simp add: field_simps vector_add_divide_simps)
+next
+  assume ?rhs
+  from has_integral_affinity'[OF this, of m c] and \<open>m > 0\<close>
+  show ?lhs by simp
+qed
+
+
 subsection \<open>Special case of stretching coordinate axes separately\<close>
 
 lemma has_integral_stretch:
diff -r 1e1818612124 -r 53ad5c01be3f src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Sat Aug 04 01:03:39 2018 +0200
@@ -1177,6 +1177,21 @@
   unfolding pathfinish_def linepath_def
   by auto
 
+lemma linepath_inner: "linepath a b x \<bullet> v = linepath (a \<bullet> v) (b \<bullet> v) x"
+  by (simp add: linepath_def algebra_simps)
+
+lemma Re_linepath': "Re (linepath a b x) = linepath (Re a) (Re b) x"
+  by (simp add: linepath_def)
+
+lemma Im_linepath': "Im (linepath a b x) = linepath (Im a) (Im b) x"
+  by (simp add: linepath_def)
+
+lemma linepath_0': "linepath a b 0 = a"
+  by (simp add: linepath_def)
+
+lemma linepath_1': "linepath a b 1 = b"
+  by (simp add: linepath_def)
+
 lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)"
   unfolding linepath_def
   by (intro continuous_intros)
@@ -1200,6 +1215,9 @@
 lemma linepath_0 [simp]: "linepath 0 b x = x *\<^sub>R b"
   by (simp add: linepath_def)
 
+lemma linepath_cnj: "cnj (linepath a b x) = linepath (cnj a) (cnj b) x"
+  by (simp add: linepath_def)
+
 lemma arc_linepath:
   assumes "a \<noteq> b" shows [simp]: "arc (linepath a b)"
 proof -
diff -r 1e1818612124 -r 53ad5c01be3f src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy	Sat Aug 04 01:03:39 2018 +0200
@@ -54,6 +54,15 @@
   by (auto simp add: indicator_def)
 *)
 
+lemma set_integrable_cong:
+  assumes "M = M'" "A = A'" "\<And>x. x \<in> A \<Longrightarrow> f x = f' x"
+  shows   "set_integrable M A f = set_integrable M' A' f'"
+proof -
+  have "(\<lambda>x. indicator A x *\<^sub>R f x) = (\<lambda>x. indicator A' x *\<^sub>R f' x)"
+    using assms by (auto simp: indicator_def)
+  thus ?thesis by (simp add: set_integrable_def assms)
+qed
+
 lemma set_borel_measurable_sets:
   fixes f :: "_ \<Rightarrow> _::real_normed_vector"
   assumes "set_borel_measurable M X f" "B \<in> sets borel" "X \<in> sets M"
@@ -925,4 +934,127 @@
   then show "integrable M (F n)" by (subst integrable_iff_bounded, simp add: assms(1)[of n])
 qed (auto simp add: assms Limsup_bounded)
 
+lemma tendsto_set_lebesgue_integral_at_right:
+  fixes a b :: real and f :: "real \<Rightarrow> 'a :: {banach,second_countable_topology}"
+  assumes "a < b" and sets: "\<And>a'. a' \<in> {a<..b} \<Longrightarrow> {a'..b} \<in> sets M"
+      and "set_integrable M {a<..b} f"
+  shows   "((\<lambda>a'. set_lebesgue_integral M {a'..b} f) \<longlongrightarrow>
+             set_lebesgue_integral M {a<..b} f) (at_right a)"
+proof (rule tendsto_at_right_sequentially[OF assms(1)], goal_cases)
+  case (1 S)
+  have eq: "(\<Union>n. {S n..b}) = {a<..b}"
+  proof safe
+    fix x n assume "x \<in> {S n..b}"
+    with 1(1,2)[of n] show "x \<in> {a<..b}" by auto
+  next
+    fix x assume "x \<in> {a<..b}"
+    with order_tendstoD[OF \<open>S \<longlonglongrightarrow> a\<close>, of x] show "x \<in> (\<Union>n. {S n..b})"
+      by (force simp: eventually_at_top_linorder dest: less_imp_le)
+  qed
+  have "(\<lambda>n. set_lebesgue_integral M {S n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M (\<Union>n. {S n..b}) f"
+    by (rule set_integral_cont_up) (insert assms 1, auto simp: eq incseq_def decseq_def less_imp_le)
+  with eq show ?case by simp
+qed
+
+
+text \<open>
+  The next lemmas relate convergence of integrals over an interval to
+  improper integrals.
+\<close>
+lemma tendsto_set_lebesgue_integral_at_left:
+  fixes a b :: real and f :: "real \<Rightarrow> 'a :: {banach,second_countable_topology}"
+  assumes "a < b" and sets: "\<And>b'. b' \<in> {a..<b} \<Longrightarrow> {a..b'} \<in> sets M"
+      and "set_integrable M {a..<b} f"
+  shows   "((\<lambda>b'. set_lebesgue_integral M {a..b'} f) \<longlongrightarrow>
+             set_lebesgue_integral M {a..<b} f) (at_left b)"
+proof (rule tendsto_at_left_sequentially[OF assms(1)], goal_cases)
+  case (1 S)
+  have eq: "(\<Union>n. {a..S n}) = {a..<b}"
+  proof safe
+    fix x n assume "x \<in> {a..S n}"
+    with 1(1,2)[of n] show "x \<in> {a..<b}" by auto
+  next
+    fix x assume "x \<in> {a..<b}"
+    with order_tendstoD[OF \<open>S \<longlonglongrightarrow> b\<close>, of x] show "x \<in> (\<Union>n. {a..S n})"
+      by (force simp: eventually_at_top_linorder dest: less_imp_le)
+  qed
+  have "(\<lambda>n. set_lebesgue_integral M {a..S n} f) \<longlonglongrightarrow> set_lebesgue_integral M (\<Union>n. {a..S n}) f"
+    by (rule set_integral_cont_up) (insert assms 1, auto simp: eq incseq_def decseq_def less_imp_le)
+  with eq show ?case by simp
+qed
+
+lemma tendsto_set_lebesgue_integral_at_top:
+  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
+  assumes sets: "\<And>b. b \<ge> a \<Longrightarrow> {a..b} \<in> sets M"
+      and int: "set_integrable M {a..} f"
+  shows "((\<lambda>b. set_lebesgue_integral M {a..b} f) \<longlongrightarrow> set_lebesgue_integral M {a..} f) at_top"
+proof (rule tendsto_at_topI_sequentially)
+  fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
+  show "(\<lambda>n. set_lebesgue_integral M {a..X n} f) \<longlonglongrightarrow> set_lebesgue_integral M {a..} f"
+    unfolding set_lebesgue_integral_def
+  proof (rule integral_dominated_convergence)
+    show "integrable M (\<lambda>x. indicat_real {a..} x *\<^sub>R norm (f x))"
+      using integrable_norm[OF int[unfolded set_integrable_def]] by simp
+    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"
+    proof
+      fix x
+      from \<open>filterlim X at_top sequentially\<close>
+      have "eventually (\<lambda>n. x \<le> X n) sequentially"
+        unfolding filterlim_at_top_ge[where c=x] by auto
+      then show "(\<lambda>n. indicator {a..X n} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {a..} x *\<^sub>R f x"
+        by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
+    qed
+    fix n show "AE x in M. norm (indicator {a..X n} x *\<^sub>R f x) \<le> 
+                             indicator {a..} x *\<^sub>R norm (f x)"
+      by (auto split: split_indicator)
+  next
+    from int show "(\<lambda>x. indicat_real {a..} x *\<^sub>R f x) \<in> borel_measurable M"
+      by (simp add: set_integrable_def)
+  next
+    fix n :: nat
+    from sets have "{a..X n} \<in> sets M" by (cases "X n \<ge> a") auto
+    with int have "set_integrable M {a..X n} f"
+      by (rule set_integrable_subset) auto
+    thus "(\<lambda>x. indicat_real {a..X n} x *\<^sub>R f x) \<in> borel_measurable M"
+      by (simp add: set_integrable_def)
+  qed
+qed
+
+lemma tendsto_set_lebesgue_integral_at_bot:
+  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
+  assumes sets: "\<And>a. a \<le> b \<Longrightarrow> {a..b} \<in> sets M"
+      and int: "set_integrable M {..b} f"
+    shows "((\<lambda>a. set_lebesgue_integral M {a..b} f) \<longlongrightarrow> set_lebesgue_integral M {..b} f) at_bot"
+proof (rule tendsto_at_botI_sequentially)
+  fix X :: "nat \<Rightarrow> real" assume "filterlim X at_bot sequentially"
+  show "(\<lambda>n. set_lebesgue_integral M {X n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M {..b} f"
+    unfolding set_lebesgue_integral_def
+  proof (rule integral_dominated_convergence)
+    show "integrable M (\<lambda>x. indicat_real {..b} x *\<^sub>R norm (f x))"
+      using integrable_norm[OF int[unfolded set_integrable_def]] by simp
+    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"
+    proof
+      fix x
+      from \<open>filterlim X at_bot sequentially\<close>
+      have "eventually (\<lambda>n. x \<ge> X n) sequentially"
+        unfolding filterlim_at_bot_le[where c=x] by auto
+      then show "(\<lambda>n. indicator {X n..b} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {..b} x *\<^sub>R f x"
+        by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
+    qed
+    fix n show "AE x in M. norm (indicator {X n..b} x *\<^sub>R f x) \<le> 
+                             indicator {..b} x *\<^sub>R norm (f x)"
+      by (auto split: split_indicator)
+  next
+    from int show "(\<lambda>x. indicat_real {..b} x *\<^sub>R f x) \<in> borel_measurable M"
+      by (simp add: set_integrable_def)
+  next
+    fix n :: nat
+    from sets have "{X n..b} \<in> sets M" by (cases "X n \<le> b") auto
+    with int have "set_integrable M {X n..b} f"
+      by (rule set_integrable_subset) auto
+    thus "(\<lambda>x. indicat_real {X n..b} x *\<^sub>R f x) \<in> borel_measurable M"
+      by (simp add: set_integrable_def)
+  qed
+qed
+
 end
diff -r 1e1818612124 -r 53ad5c01be3f src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Archimedean_Field.thy	Sat Aug 04 01:03:39 2018 +0200
@@ -707,6 +707,9 @@
 lemma frac_of_int [simp]: "frac (of_int z) = 0"
   by (simp add: frac_def)
 
+lemma frac_frac [simp]: "frac (frac x) = frac x"
+  by (simp add: frac_def)
+
 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)"
 proof -
   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>"
@@ -743,6 +746,14 @@
   apply (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq)
   done
 
+lemma frac_in_Ints_iff [simp]: "frac x \<in> \<int> \<longleftrightarrow> x \<in> \<int>"
+proof safe
+  assume "frac x \<in> \<int>"
+  hence "of_int \<lfloor>x\<rfloor> + frac x \<in> \<int>" by auto
+  also have "of_int \<lfloor>x\<rfloor> + frac x = x" by (simp add: frac_def)
+  finally show "x \<in> \<int>" .
+qed (auto simp: frac_def)
+
 
 subsection \<open>Rounding to the nearest integer\<close>
 
diff -r 1e1818612124 -r 53ad5c01be3f src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Complex.thy	Sat Aug 04 01:03:39 2018 +0200
@@ -623,6 +623,27 @@
 lemma sums_cnj: "((\<lambda>x. cnj(f x)) sums cnj l) \<longleftrightarrow> (f sums l)"
   by (simp add: sums_def lim_cnj cnj_sum [symmetric] del: cnj_sum)
 
+lemma differentiable_cnj_iff:
+  "(\<lambda>z. cnj (f z)) differentiable at x within A \<longleftrightarrow> f differentiable at x within A"
+proof
+  assume "(\<lambda>z. cnj (f z)) differentiable at x within A"
+  then obtain D where "((\<lambda>z. cnj (f z)) has_derivative D) (at x within A)"
+    by (auto simp: differentiable_def)
+  from has_derivative_cnj[OF this] show "f differentiable at x within A"
+    by (auto simp: differentiable_def)
+next
+  assume "f differentiable at x within A"
+  then obtain D where "(f has_derivative D) (at x within A)"
+    by (auto simp: differentiable_def)
+  from has_derivative_cnj[OF this] show "(\<lambda>z. cnj (f z)) differentiable at x within A"
+    by (auto simp: differentiable_def)
+qed
+
+lemma has_vector_derivative_cnj [derivative_intros]:
+  assumes "(f has_vector_derivative f') (at z within A)"
+  shows   "((\<lambda>z. cnj (f z)) has_vector_derivative cnj f') (at z within A)"
+  using assms by (auto simp: has_vector_derivative_complex_iff intro: derivative_intros)
+
 
 subsection \<open>Basic Lemmas\<close>
 
@@ -778,9 +799,15 @@
 lemma sgn_cis [simp]: "sgn (cis a) = cis a"
   by (simp add: sgn_div_norm)
 
+lemma cis_2pi [simp]: "cis (2 * pi) = 1"
+  by (simp add: cis.ctr complex_eq_iff)
+
 lemma cis_neq_zero [simp]: "cis a \<noteq> 0"
   by (metis norm_cis norm_zero zero_neq_one)
 
+lemma cis_cnj: "cnj (cis t) = cis (-t)"
+  by (simp add: complex_eq_iff)
+
 lemma cis_mult: "cis a * cis b = cis (a + b)"
   by (simp add: complex_eq_iff cos_add sin_add)
 
@@ -802,6 +829,15 @@
 lemma cis_pi [simp]: "cis pi = -1"
   by (simp add: complex_eq_iff)
 
+lemma cis_pi_half[simp]: "cis (pi / 2) = \<i>"
+  by (simp add: cis.ctr complex_eq_iff)
+
+lemma cis_minus_pi_half[simp]: "cis (-(pi / 2)) = -\<i>"
+  by (simp add: cis.ctr complex_eq_iff)
+
+lemma cis_multiple_2pi[simp]: "n \<in> \<int> \<Longrightarrow> cis (2 * pi * n) = 1"
+  by (auto elim!: Ints_cases simp: cis.ctr one_complex.ctr)
+
 
 subsubsection \<open>$r(\cos \theta + i \sin \theta)$\<close>
 
@@ -847,6 +883,11 @@
 
 subsubsection \<open>Complex exponential\<close>
 
+lemma exp_Reals_eq:
+  assumes "z \<in> \<real>"
+  shows   "exp z = of_real (exp (Re z))"
+  using assms by (auto elim!: Reals_cases simp: exp_of_real)
+
 lemma cis_conv_exp: "cis b = exp (\<i> * b)"
 proof -
   have "(\<i> * complex_of_real b) ^ n /\<^sub>R fact n =
@@ -901,6 +942,10 @@
 lemma exp_two_pi_i' [simp]: "exp (\<i> * (of_real pi * 2)) = 1"
   by (metis exp_two_pi_i mult.commute)
 
+lemma continuous_on_cis [continuous_intros]:
+  "continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. cis (f x))"
+  by (auto simp: cis_conv_exp intro!: continuous_intros)
+
 
 subsubsection \<open>Complex argument\<close>
 
diff -r 1e1818612124 -r 53ad5c01be3f src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Int.thy	Sat Aug 04 01:03:39 2018 +0200
@@ -892,6 +892,9 @@
   apply (rule of_int_minus [symmetric])
   done
 
+lemma minus_in_Ints_iff: "-x \<in> \<int> \<longleftrightarrow> x \<in> \<int>"
+  using Ints_minus[of x] Ints_minus[of "-x"] by auto
+
 lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
   apply (auto simp add: Ints_def)
   apply (rule range_eqI)
diff -r 1e1818612124 -r 53ad5c01be3f src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Limits.thy	Sat Aug 04 01:03:39 2018 +0200
@@ -1316,6 +1316,16 @@
     and filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "\<lambda>x. - f x" F]
   by auto
 
+lemma tendsto_at_botI_sequentially:
+  fixes f :: "real \<Rightarrow> 'b::first_countable_topology"
+  assumes *: "\<And>X. filterlim X at_bot sequentially \<Longrightarrow> (\<lambda>n. f (X n)) \<longlonglongrightarrow> y"
+  shows "(f \<longlongrightarrow> y) at_bot"
+  unfolding filterlim_at_bot_mirror
+proof (rule tendsto_at_topI_sequentially)
+  fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
+  thus "(\<lambda>n. f (-X n)) \<longlonglongrightarrow> y" by (intro *) (auto simp: filterlim_uminus_at_top)
+qed
+
 lemma filterlim_at_infinity_imp_filterlim_at_top:
   assumes "filterlim (f :: 'a \<Rightarrow> real) at_infinity F"
   assumes "eventually (\<lambda>x. f x > 0) F"
diff -r 1e1818612124 -r 53ad5c01be3f src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Sat Aug 04 01:03:39 2018 +0200
@@ -1012,6 +1012,9 @@
 lemma dist_triangle3: "dist x y \<le> dist a x + dist a y"
   using dist_triangle2 [of x y a] by (simp add: dist_commute)
 
+lemma abs_dist_diff_le: "\<bar>dist a b - dist b c\<bar> \<le> dist a c"
+  using dist_triangle3[of b c a] dist_triangle2[of a b c] by simp
+
 lemma dist_pos_lt: "x \<noteq> y \<Longrightarrow> 0 < dist x y"
   by (simp add: zero_less_dist_iff)
 
diff -r 1e1818612124 -r 53ad5c01be3f src/HOL/Series.thy
--- a/src/HOL/Series.thy	Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Series.thy	Sat Aug 04 01:03:39 2018 +0200
@@ -703,6 +703,27 @@
   qed
 qed
 
+lemma summable_Cauchy':
+  fixes f :: "nat \<Rightarrow> 'a :: banach"
+  assumes "eventually (\<lambda>m. \<forall>n\<ge>m. norm (sum f {m..<n}) \<le> g m) sequentially"
+  assumes "filterlim g (nhds 0) sequentially"
+  shows "summable f"
+proof (subst summable_Cauchy, intro allI impI, goal_cases)
+  case (1 e)
+  from order_tendstoD(2)[OF assms(2) this] and assms(1)
+  have "eventually (\<lambda>m. \<forall>n. norm (sum f {m..<n}) < e) at_top"
+  proof eventually_elim
+    case (elim m)
+    show ?case
+    proof
+      fix n
+      from elim show "norm (sum f {m..<n}) < e"
+        by (cases "n \<ge> m") auto
+    qed
+  qed
+  thus ?case by (auto simp: eventually_at_top_linorder)
+qed
+
 context
   fixes f :: "nat \<Rightarrow> 'a::banach"
 begin
diff -r 1e1818612124 -r 53ad5c01be3f src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy	Sat Aug 04 01:03:39 2018 +0200
@@ -2131,6 +2131,9 @@
 lemma isCont_def: "isCont f a \<longleftrightarrow> f \<midarrow>a\<rightarrow> f a"
   by (rule continuous_at)
 
+lemma isContD: "isCont f x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x"
+  by (simp add: isCont_def)
+
 lemma isCont_cong:
   assumes "eventually (\<lambda>x. f x = g x) (nhds x)"
   shows "isCont f x \<longleftrightarrow> isCont g x"