# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1574778728 0
# Node ID b4d409c65a769c6210dba0e057edad108ed22883
# Parent  c9433e8e314efaafa7d48b1d741b7a522c37a102
Rearrangement of material in Complex_Analysis_Basics, which contained much that had nothing to do with complex analysis.

diff -r c9433e8e314e -r b4d409c65a76 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Nov 26 08:09:44 2019 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Nov 26 14:32:08 2019 +0000
@@ -3,13 +3,12 @@
 *)
 
 section \<open>Complex Analysis Basics\<close>
+text \<open>Definitions of analytic and holomorphic functions, limit theorems, complex differentiation\<close>
 
 theory Complex_Analysis_Basics
   imports Derivative "HOL-Library.Nonpos_Ints"
 begin
 
-(* TODO FIXME: A lot of the things in here have nothing to do with complex analysis *)
-
 subsection\<^marker>\<open>tag unimportant\<close>\<open>General lemmas\<close>
 
 lemma nonneg_Reals_cmod_eq_Re: "z \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> norm z = Re z"
@@ -38,26 +37,6 @@
   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
-
-lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = (*) 1"
-  by auto
-
-lemma uniformly_continuous_on_cmul_right [continuous_intros]:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
-  shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)"
-  using bounded_linear.uniformly_continuous_on[OF bounded_linear_mult_left] .
-
-lemma uniformly_continuous_on_cmul_left[continuous_intros]:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
-  assumes "uniformly_continuous_on s f"
-    shows "uniformly_continuous_on s (\<lambda>x. c * f x)"
-by (metis assms bounded_linear.uniformly_continuous_on bounded_linear_mult_right)
-
-lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm"
-  by (intro continuous_on_id continuous_on_norm)
-
 lemma
   shows open_halfspace_Re_lt: "open {z. Re(z) < b}"
     and open_halfspace_Re_gt: "open {z. Re(z) > b}"
@@ -135,7 +114,6 @@
   assumes "eventually (\<lambda>x. norm(f x) \<le> Re(g x)) F" "(g \<longlongrightarrow> 0) F" shows "(f \<longlongrightarrow> 0) F"
   by (rule Lim_null_comparison[OF assms(1)] tendsto_eq_intros assms(2))+ simp
 
-
 lemma closed_segment_same_Re:
   assumes "Re a = Re b"
   shows   "closed_segment a b = {z. Re z = Re a \<and> Im z \<in> closed_segment (Im a) (Im b)}"
@@ -426,20 +404,6 @@
   by (rule nonzero_deriv_nonconstant [of f "deriv f \<xi>" \<xi> S])
     (use assms in \<open>auto simp: holomorphic_derivI\<close>)
 
-subsection\<^marker>\<open>tag unimportant\<close>\<open>Caratheodory characterization\<close>
-
-lemma field_differentiable_caratheodory_at:
-  "f field_differentiable (at z) \<longleftrightarrow>
-         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
-  using CARAT_DERIV [of f]
-  by (simp add: field_differentiable_def has_field_derivative_def)
-
-lemma field_differentiable_caratheodory_within:
-  "f field_differentiable (at z within s) \<longleftrightarrow>
-         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z within s) g)"
-  using DERIV_caratheodory_within [of f]
-  by (simp add: field_differentiable_def has_field_derivative_def)
-
 subsection\<open>Analyticity on a set\<close>
 
 definition\<^marker>\<open>tag important\<close> analytic_on (infixl "(analytic'_on)" 50)
@@ -813,60 +777,6 @@
   qed
 qed
 
-
-lemma field_differentiable_series:
-  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach} \<Rightarrow> 'a"
-  assumes "convex S" "open S"
-  assumes "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
-  assumes "uniformly_convergent_on S (\<lambda>n x. \<Sum>i<n. f' i x)"
-  assumes "x0 \<in> S" "summable (\<lambda>n. f n x0)" and x: "x \<in> S"
-  shows  "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)"
-proof -
-  from assms(4) obtain g' where A: "uniform_limit S (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
-    unfolding uniformly_convergent_on_def by blast
-  from x and \<open>open S\<close> have S: "at x within S = at x" by (rule at_within_open)
-  have "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within S)"
-    by (intro has_field_derivative_series[of S f f' g' x0] assms A has_field_derivative_at_within)
-  then obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x"
-    "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast
-  from g(2)[OF x] have g': "(g has_derivative (*) (g' x)) (at x)"
-    by (simp add: has_field_derivative_def S)
-  have "((\<lambda>x. \<Sum>n. f n x) has_derivative (*) (g' x)) (at x)"
-    by (rule has_derivative_transform_within_open[OF g' \<open>open S\<close> x])
-       (insert g, auto simp: sums_iff)
-  thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def
-    by (auto simp: summable_def field_differentiable_def has_field_derivative_def)
-qed
-
-subsection\<^marker>\<open>tag unimportant\<close>\<open>Bound theorem\<close>
-
-lemma field_differentiable_bound:
-  fixes S :: "'a::real_normed_field set"
-  assumes cvs: "convex S"
-      and df:  "\<And>z. z \<in> S \<Longrightarrow> (f has_field_derivative f' z) (at z within S)"
-      and dn:  "\<And>z. z \<in> S \<Longrightarrow> norm (f' z) \<le> B"
-      and "x \<in> S"  "y \<in> S"
-    shows "norm(f x - f y) \<le> B * norm(x - y)"
-  apply (rule differentiable_bound [OF cvs])
-  apply (erule df [unfolded has_field_derivative_def])
-  apply (rule onorm_le, simp_all add: norm_mult mult_right_mono assms)
-  done
-
-subsection\<^marker>\<open>tag unimportant\<close>\<open>Inverse function theorem for complex derivatives\<close>
-
-lemma has_field_derivative_inverse_basic:
-  shows "DERIV f (g y) :> f' \<Longrightarrow>
-        f' \<noteq> 0 \<Longrightarrow>
-        continuous (at y) g \<Longrightarrow>
-        open t \<Longrightarrow>
-        y \<in> t \<Longrightarrow>
-        (\<And>z. z \<in> t \<Longrightarrow> f (g z) = z)
-        \<Longrightarrow> DERIV g y :> inverse (f')"
-  unfolding has_field_derivative_def
-  apply (rule has_derivative_inverse_basic)
-  apply (auto simp:  bounded_linear_mult_right)
-  done
-
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Taylor on Complex Numbers\<close>
 
 lemma sum_Suc_reindex:
@@ -1053,92 +963,4 @@
 qed
 
 
-subsection\<^marker>\<open>tag unimportant\<close> \<open>Polynomal function extremal theorem, from HOL Light\<close>
-
-lemma polyfun_extremal_lemma: (*COMPLEX_POLYFUN_EXTREMAL_LEMMA in HOL Light*)
-    fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
-  assumes "0 < e"
-    shows "\<exists>M. \<forall>z. M \<le> norm(z) \<longrightarrow> norm (\<Sum>i\<le>n. c(i) * z^i) \<le> e * norm(z) ^ (Suc n)"
-proof (induct n)
-  case 0 with assms
-  show ?case
-    apply (rule_tac x="norm (c 0) / e" in exI)
-    apply (auto simp: field_simps)
-    done
-next
-  case (Suc n)
-  obtain M where M: "\<And>z. M \<le> norm z \<Longrightarrow> norm (\<Sum>i\<le>n. c i * z^i) \<le> e * norm z ^ Suc n"
-    using Suc assms by blast
-  show ?case
-  proof (rule exI [where x= "max M (1 + norm(c(Suc n)) / e)"], clarsimp simp del: power_Suc)
-    fix z::'a
-    assume z1: "M \<le> norm z" and "1 + norm (c (Suc n)) / e \<le> norm z"
-    then have z2: "e + norm (c (Suc n)) \<le> e * norm z"
-      using assms by (simp add: field_simps)
-    have "norm (\<Sum>i\<le>n. c i * z^i) \<le> e * norm z ^ Suc n"
-      using M [OF z1] by simp
-    then have "norm (\<Sum>i\<le>n. c i * z^i) + norm (c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
-      by simp
-    then have "norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
-      by (blast intro: norm_triangle_le elim: )
-    also have "... \<le> (e + norm (c (Suc n))) * norm z ^ Suc n"
-      by (simp add: norm_power norm_mult algebra_simps)
-    also have "... \<le> (e * norm z) * norm z ^ Suc n"
-      by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power)
-    finally show "norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc (Suc n)"
-      by simp
-  qed
-qed
-
-lemma polyfun_extremal: (*COMPLEX_POLYFUN_EXTREMAL in HOL Light*)
-    fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
-  assumes k: "c k \<noteq> 0" "1\<le>k" and kn: "k\<le>n"
-    shows "eventually (\<lambda>z. norm (\<Sum>i\<le>n. c(i) * z^i) \<ge> B) at_infinity"
-using kn
-proof (induction n)
-  case 0
-  then show ?case
-    using k  by simp
-next
-  case (Suc m)
-  let ?even = ?case
-  show ?even
-  proof (cases "c (Suc m) = 0")
-    case True
-    then show ?even using Suc k
-      by auto (metis antisym_conv less_eq_Suc_le not_le)
-  next
-    case False
-    then obtain M where M:
-          "\<And>z. M \<le> norm z \<Longrightarrow> norm (\<Sum>i\<le>m. c i * z^i) \<le> norm (c (Suc m)) / 2 * norm z ^ Suc m"
-      using polyfun_extremal_lemma [of "norm(c (Suc m)) / 2" c m] Suc
-      by auto
-    have "\<exists>b. \<forall>z. b \<le> norm z \<longrightarrow> B \<le> norm (\<Sum>i\<le>Suc m. c i * z^i)"
-    proof (rule exI [where x="max M (max 1 (\<bar>B\<bar> / (norm(c (Suc m)) / 2)))"], clarsimp simp del: power_Suc)
-      fix z::'a
-      assume z1: "M \<le> norm z" "1 \<le> norm z"
-         and "\<bar>B\<bar> * 2 / norm (c (Suc m)) \<le> norm z"
-      then have z2: "\<bar>B\<bar> \<le> norm (c (Suc m)) * norm z / 2"
-        using False by (simp add: field_simps)
-      have nz: "norm z \<le> norm z ^ Suc m"
-        by (metis \<open>1 \<le> norm z\<close> One_nat_def less_eq_Suc_le power_increasing power_one_right zero_less_Suc)
-      have *: "\<And>y x. norm (c (Suc m)) * norm z / 2 \<le> norm y - norm x \<Longrightarrow> B \<le> norm (x + y)"
-        by (metis abs_le_iff add.commute norm_diff_ineq order_trans z2)
-      have "norm z * norm (c (Suc m)) + 2 * norm (\<Sum>i\<le>m. c i * z^i)
-            \<le> norm (c (Suc m)) * norm z + norm (c (Suc m)) * norm z ^ Suc m"
-        using M [of z] Suc z1  by auto
-      also have "... \<le> 2 * (norm (c (Suc m)) * norm z ^ Suc m)"
-        using nz by (simp add: mult_mono del: power_Suc)
-      finally show "B \<le> norm ((\<Sum>i\<le>m. c i * z^i) + c (Suc m) * z ^ Suc m)"
-        using Suc.IH
-        apply (auto simp: eventually_at_infinity)
-        apply (rule *)
-        apply (simp add: field_simps norm_mult norm_power)
-        done
-    qed
-    then show ?even
-      by (simp add: eventually_at_infinity)
-  qed
-qed
-
 end
diff -r c9433e8e314e -r b4d409c65a76 src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Tue Nov 26 08:09:44 2019 +0100
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue Nov 26 14:32:08 2019 +0000
@@ -386,8 +386,7 @@
       have frne: "frontier (cball \<xi> r) \<noteq> {}"
         using \<open>0 < r\<close> by auto
       have contfr: "continuous_on (frontier (cball \<xi> r)) (\<lambda>z. norm (f z - f \<xi>))"
-        apply (rule continuous_on_compose2 [OF Complex_Analysis_Basics.continuous_on_norm_id])
-        using hol frsbU holomorphic_on_imp_continuous_on holomorphic_on_subset by blast+
+        by (metis continuous_on_norm continuous_on_subset frsbU hol holomorphic_on_imp_continuous_on)
       obtain w where "norm (\<xi> - w) = r"
                  and w: "(\<And>z. norm (\<xi> - z) = r \<Longrightarrow> norm (f w - f \<xi>) \<le> norm(f z - f \<xi>))"
         apply (rule bexE [OF continuous_attains_inf [OF cof frne contfr]])
diff -r c9433e8e314e -r b4d409c65a76 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Tue Nov 26 08:09:44 2019 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Tue Nov 26 14:32:08 2019 +0000
@@ -937,6 +937,18 @@
   finally show ?thesis .
 qed
 
+lemma field_differentiable_bound:
+  fixes S :: "'a::real_normed_field set"
+  assumes cvs: "convex S"
+      and df:  "\<And>z. z \<in> S \<Longrightarrow> (f has_field_derivative f' z) (at z within S)"
+      and dn:  "\<And>z. z \<in> S \<Longrightarrow> norm (f' z) \<le> B"
+      and "x \<in> S"  "y \<in> S"
+    shows "norm(f x - f y) \<le> B * norm(x - y)"
+  apply (rule differentiable_bound [OF cvs])
+  apply (erule df [unfolded has_field_derivative_def])
+  apply (rule onorm_le, simp_all add: norm_mult mult_right_mono assms)
+  done
+
 lemma
   differentiable_bound_segment:
   fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
@@ -1162,6 +1174,20 @@
   qed
 qed
 
+text\<^marker>\<open>tag unimportant\<close>\<open>Inverse function theorem for complex derivatives\<close>
+lemma has_field_derivative_inverse_basic:
+  shows "DERIV f (g y) :> f' \<Longrightarrow>
+        f' \<noteq> 0 \<Longrightarrow>
+        continuous (at y) g \<Longrightarrow>
+        open t \<Longrightarrow>
+        y \<in> t \<Longrightarrow>
+        (\<And>z. z \<in> t \<Longrightarrow> f (g z) = z)
+        \<Longrightarrow> DERIV g y :> inverse (f')"
+  unfolding has_field_derivative_def
+  apply (rule has_derivative_inverse_basic)
+  apply (auto simp:  bounded_linear_mult_right)
+  done
+
 text \<open>Simply rewrite that based on the domain point x.\<close>
 
 lemma has_derivative_inverse_basic_x:
@@ -2175,6 +2201,45 @@
   using exp_scaleR_has_vector_derivative_right[of A t]
   by (simp add: exp_times_scaleR_commute)
 
+lemma field_differentiable_series:
+  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach} \<Rightarrow> 'a"
+  assumes "convex S" "open S"
+  assumes "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
+  assumes "uniformly_convergent_on S (\<lambda>n x. \<Sum>i<n. f' i x)"
+  assumes "x0 \<in> S" "summable (\<lambda>n. f n x0)" and x: "x \<in> S"
+  shows  "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)"
+proof -
+  from assms(4) obtain g' where A: "uniform_limit S (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
+    unfolding uniformly_convergent_on_def by blast
+  from x and \<open>open S\<close> have S: "at x within S = at x" by (rule at_within_open)
+  have "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within S)"
+    by (intro has_field_derivative_series[of S f f' g' x0] assms A has_field_derivative_at_within)
+  then obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x"
+    "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast
+  from g(2)[OF x] have g': "(g has_derivative (*) (g' x)) (at x)"
+    by (simp add: has_field_derivative_def S)
+  have "((\<lambda>x. \<Sum>n. f n x) has_derivative (*) (g' x)) (at x)"
+    by (rule has_derivative_transform_within_open[OF g' \<open>open S\<close> x])
+       (insert g, auto simp: sums_iff)
+  thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def
+    by (auto simp: summable_def field_differentiable_def has_field_derivative_def)
+qed
+
+subsubsection\<^marker>\<open>tag unimportant\<close>\<open>Caratheodory characterization\<close>
+
+lemma field_differentiable_caratheodory_at:
+  "f field_differentiable (at z) \<longleftrightarrow>
+         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
+  using CARAT_DERIV [of f]
+  by (simp add: field_differentiable_def has_field_derivative_def)
+
+lemma field_differentiable_caratheodory_within:
+  "f field_differentiable (at z within s) \<longleftrightarrow>
+         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z within s) g)"
+  using DERIV_caratheodory_within [of f]
+  by (simp add: field_differentiable_def has_field_derivative_def)
+
+
 subsection \<open>Field derivative\<close>
 
 definition\<^marker>\<open>tag important\<close> deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
@@ -2236,7 +2301,6 @@
   apply (rule vector_derivative_at [OF field_vector_diff_chain_at])
   using assms vector_derivative_works by (auto simp: field_differentiable_derivI)
 
-
 subsection \<open>Relation between convexity and derivative\<close>
 
 (* TODO: Generalise to real vector spaces? *)
diff -r c9433e8e314e -r b4d409c65a76 src/HOL/Analysis/Elementary_Normed_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Tue Nov 26 08:09:44 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Tue Nov 26 14:32:08 2019 +0000
@@ -1085,6 +1085,17 @@
     unfolding dist_real_def by simp
 qed
 
+lemma uniformly_continuous_on_cmul_right [continuous_intros]:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
+  shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)"
+  using bounded_linear.uniformly_continuous_on[OF bounded_linear_mult_left] .
+
+lemma uniformly_continuous_on_cmul_left[continuous_intros]:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
+  assumes "uniformly_continuous_on s f"
+    shows "uniformly_continuous_on s (\<lambda>x. c * f x)"
+by (metis assms bounded_linear.uniformly_continuous_on bounded_linear_mult_right)
+
 lemma uniformly_continuous_on_norm[continuous_intros]:
   fixes f :: "'a :: metric_space \<Rightarrow> 'b :: real_normed_vector"
   assumes "uniformly_continuous_on s f"
diff -r c9433e8e314e -r b4d409c65a76 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Nov 26 08:09:44 2019 +0100
+++ b/src/HOL/Limits.thy	Tue Nov 26 14:32:08 2019 +0000
@@ -341,6 +341,94 @@
   by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def)
 
 
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Polynomal function extremal theorem, from HOL Light\<close>
+
+lemma polyfun_extremal_lemma: (*COMPLEX_POLYFUN_EXTREMAL_LEMMA in HOL Light*)
+    fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
+  assumes "0 < e"
+    shows "\<exists>M. \<forall>z. M \<le> norm(z) \<longrightarrow> norm (\<Sum>i\<le>n. c(i) * z^i) \<le> e * norm(z) ^ (Suc n)"
+proof (induct n)
+  case 0 with assms
+  show ?case
+    apply (rule_tac x="norm (c 0) / e" in exI)
+    apply (auto simp: field_simps)
+    done
+next
+  case (Suc n)
+  obtain M where M: "\<And>z. M \<le> norm z \<Longrightarrow> norm (\<Sum>i\<le>n. c i * z^i) \<le> e * norm z ^ Suc n"
+    using Suc assms by blast
+  show ?case
+  proof (rule exI [where x= "max M (1 + norm(c(Suc n)) / e)"], clarsimp simp del: power_Suc)
+    fix z::'a
+    assume z1: "M \<le> norm z" and "1 + norm (c (Suc n)) / e \<le> norm z"
+    then have z2: "e + norm (c (Suc n)) \<le> e * norm z"
+      using assms by (simp add: field_simps)
+    have "norm (\<Sum>i\<le>n. c i * z^i) \<le> e * norm z ^ Suc n"
+      using M [OF z1] by simp
+    then have "norm (\<Sum>i\<le>n. c i * z^i) + norm (c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
+      by simp
+    then have "norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
+      by (blast intro: norm_triangle_le elim: )
+    also have "... \<le> (e + norm (c (Suc n))) * norm z ^ Suc n"
+      by (simp add: norm_power norm_mult algebra_simps)
+    also have "... \<le> (e * norm z) * norm z ^ Suc n"
+      by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power)
+    finally show "norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc (Suc n)"
+      by simp
+  qed
+qed
+
+lemma polyfun_extremal: (*COMPLEX_POLYFUN_EXTREMAL in HOL Light*)
+    fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
+  assumes k: "c k \<noteq> 0" "1\<le>k" and kn: "k\<le>n"
+    shows "eventually (\<lambda>z. norm (\<Sum>i\<le>n. c(i) * z^i) \<ge> B) at_infinity"
+using kn
+proof (induction n)
+  case 0
+  then show ?case
+    using k  by simp
+next
+  case (Suc m)
+  let ?even = ?case
+  show ?even
+  proof (cases "c (Suc m) = 0")
+    case True
+    then show ?even using Suc k
+      by auto (metis antisym_conv less_eq_Suc_le not_le)
+  next
+    case False
+    then obtain M where M:
+          "\<And>z. M \<le> norm z \<Longrightarrow> norm (\<Sum>i\<le>m. c i * z^i) \<le> norm (c (Suc m)) / 2 * norm z ^ Suc m"
+      using polyfun_extremal_lemma [of "norm(c (Suc m)) / 2" c m] Suc
+      by auto
+    have "\<exists>b. \<forall>z. b \<le> norm z \<longrightarrow> B \<le> norm (\<Sum>i\<le>Suc m. c i * z^i)"
+    proof (rule exI [where x="max M (max 1 (\<bar>B\<bar> / (norm(c (Suc m)) / 2)))"], clarsimp simp del: power_Suc)
+      fix z::'a
+      assume z1: "M \<le> norm z" "1 \<le> norm z"
+         and "\<bar>B\<bar> * 2 / norm (c (Suc m)) \<le> norm z"
+      then have z2: "\<bar>B\<bar> \<le> norm (c (Suc m)) * norm z / 2"
+        using False by (simp add: field_simps)
+      have nz: "norm z \<le> norm z ^ Suc m"
+        by (metis \<open>1 \<le> norm z\<close> One_nat_def less_eq_Suc_le power_increasing power_one_right zero_less_Suc)
+      have *: "\<And>y x. norm (c (Suc m)) * norm z / 2 \<le> norm y - norm x \<Longrightarrow> B \<le> norm (x + y)"
+        by (metis abs_le_iff add.commute norm_diff_ineq order_trans z2)
+      have "norm z * norm (c (Suc m)) + 2 * norm (\<Sum>i\<le>m. c i * z^i)
+            \<le> norm (c (Suc m)) * norm z + norm (c (Suc m)) * norm z ^ Suc m"
+        using M [of z] Suc z1  by auto
+      also have "... \<le> 2 * (norm (c (Suc m)) * norm z ^ Suc m)"
+        using nz by (simp add: mult_mono del: power_Suc)
+      finally show "B \<le> norm ((\<Sum>i\<le>m. c i * z^i) + c (Suc m) * z ^ Suc m)"
+        using Suc.IH
+        apply (auto simp: eventually_at_infinity)
+        apply (rule *)
+        apply (simp add: field_simps norm_mult norm_power)
+        done
+    qed
+    then show ?even
+      by (simp add: eventually_at_infinity)
+  qed
+qed
+
 subsection \<open>Convergence to Zero\<close>
 
 definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
@@ -545,6 +633,9 @@
   "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. norm (f x))"
   unfolding continuous_on_def by (auto intro: tendsto_norm)
 
+lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm"
+  by (intro continuous_on_id continuous_on_norm)
+
 lemma tendsto_norm_zero: "(f \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. norm (f x)) \<longlongrightarrow> 0) F"
   by (drule tendsto_norm) simp
 
diff -r c9433e8e314e -r b4d409c65a76 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Tue Nov 26 08:09:44 2019 +0100
+++ b/src/HOL/Rings.thy	Tue Nov 26 14:32:08 2019 +0000
@@ -128,6 +128,11 @@
 
 end
 
+lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = (*) 0"
+  by auto
+
+lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = (*) 1"
+  by auto
 
 subsection \<open>Abstract divisibility\<close>
 
diff -r c9433e8e314e -r b4d409c65a76 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue Nov 26 08:09:44 2019 +0100
+++ b/src/HOL/Set_Interval.thy	Tue Nov 26 14:32:08 2019 +0000
@@ -1944,6 +1944,9 @@
   "F g {Suc m..Suc n} = F (\<lambda>i. g(Suc i)){m..n}"
 by (simp add: shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
 
+corollary Suc_reindex_ivl: "m \<le> n \<Longrightarrow> F g {m..n} \<^bold>* g (Suc n) = g m \<^bold>* F (\<lambda>i. g (Suc i)) {m..n}"
+  by (simp add: assoc atLeast_Suc_atMost flip: shift_bounds_cl_Suc_ivl)
+
 corollary shift_bounds_Suc_ivl:
   "F g {Suc m..<Suc n} = F (\<lambda>i. g(Suc i)){m..<n}"
 by (simp add: shift_bounds_nat_ivl[where k="Suc 0", simplified])