# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1430234618 -3600
# Node ID bd773c47ad0b429c104e0381134a4dd71d1ff2ff
# Parent  9b0825a00b1aa7d8e79d44253c1e283e14f28715
New material about complex transcendental functions (especially Ln, Arg) and polynomials

diff -r 9b0825a00b1a -r bd773c47ad0b src/HOL/Inequalities.thy
--- a/src/HOL/Inequalities.thy	Tue Apr 28 16:23:05 2015 +0100
+++ b/src/HOL/Inequalities.thy	Tue Apr 28 16:23:38 2015 +0100
@@ -7,14 +7,6 @@
   imports Real_Vector_Spaces
 begin
 
-lemma setsum_triangle_reindex:
-  fixes n :: nat
-  shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
-  apply (simp add: setsum.Sigma)
-  apply (rule setsum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
-  apply auto
-  done
-
 lemma gauss_sum_div2: "(2::'a::semiring_div) \<noteq> 0 \<Longrightarrow>
   setsum of_nat {1..n} = of_nat n * (of_nat n + 1) div (2::'a)"
 using gauss_sum[where n=n and 'a = 'a,symmetric] by auto
diff -r 9b0825a00b1a -r bd773c47ad0b src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Tue Apr 28 16:23:05 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Tue Apr 28 16:23:38 2015 +0100
@@ -240,7 +240,7 @@
     and closed_halfspace_Im_le: "closed {z. Im(z) \<le> b}"
     and closed_halfspace_Im_eq: "closed {z. Im(z) = b}"
   by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re
-            isCont_Im isCont_ident isCont_const)+
+            isCont_Im continuous_ident continuous_const)+
 
 lemma closed_complex_Reals: "closed (Reals :: complex set)"
 proof -
diff -r 9b0825a00b1a -r bd773c47ad0b src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Apr 28 16:23:05 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Apr 28 16:23:38 2015 +0100
@@ -42,11 +42,8 @@
 
 subsection{*The Exponential Function is Differentiable and Continuous*}
 
-lemma complex_differentiable_at_exp: "exp complex_differentiable at z"
-  using DERIV_exp complex_differentiable_def by blast
-
 lemma complex_differentiable_within_exp: "exp complex_differentiable (at z within s)"
-  by (simp add: complex_differentiable_at_exp complex_differentiable_at_within)
+  using DERIV_exp complex_differentiable_at_within complex_differentiable_def by blast
 
 lemma continuous_within_exp:
   fixes z::"'a::{real_normed_field,banach}"
@@ -777,6 +774,11 @@
     by blast
 qed
 
+corollary Arg_gt_0: 
+  assumes "z \<in> \<real> \<Longrightarrow> Re z < 0"
+    shows "Arg z > 0"
+  using Arg_eq_0 Arg_ge_0 assms dual_order.strict_iff_order by fastforce
+
 lemma Arg_of_real: "Arg(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
   by (simp add: Arg_eq_0)
 
@@ -952,6 +954,12 @@
 corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> ln z \<in> \<real>"
   by (auto simp: Ln_of_real elim: Reals_cases)
 
+corollary Im_Ln_of_real [simp]: "r > 0 \<Longrightarrow> Im (ln (of_real r)) = 0"
+  by (simp add: Ln_of_real)
+
+lemma cmod_Ln_Reals [simp]: "z \<in> Reals \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
+  using Ln_of_real by force
+
 lemma Ln_1: "ln 1 = (0::complex)"
 proof -
   have "ln (exp 0) = (0::complex)"
@@ -975,7 +983,13 @@
   using Ln_exp by blast
 
 lemma Re_Ln [simp]: "z \<noteq> 0 \<Longrightarrow> Re(Ln z) = ln(norm z)"
-by (metis exp_Ln assms ln_exp norm_exp_eq_Re)
+  by (metis exp_Ln assms ln_exp norm_exp_eq_Re)
+
+corollary ln_cmod_le: 
+  assumes z: "z \<noteq> 0"
+    shows "ln (cmod z) \<le> cmod (Ln z)"
+  using norm_exp [of "Ln z", simplified exp_Ln [OF z]]
+  by (metis Re_Ln complex_Re_le_cmod z)
 
 lemma exists_complex_root:
   fixes a :: complex
@@ -1185,7 +1199,7 @@
   also have "... = - (Ln ii)"
     by (metis Ln_inverse ii.sel(2) inverse_eq_divide zero_neq_one)
   also have "... = - (ii * pi/2)"
-    by (simp add: Ln_ii)
+    by simp
   finally show ?thesis .
 qed
 
@@ -1201,11 +1215,22 @@
   using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z]
   by (auto simp: of_real_numeral exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique)
 
-lemma Ln_times_simple:
+corollary Ln_times_simple:
     "\<lbrakk>w \<noteq> 0; z \<noteq> 0; -pi < Im(Ln w) + Im(Ln z); Im(Ln w) + Im(Ln z) \<le> pi\<rbrakk>
          \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z)"
   by (simp add: Ln_times)
 
+corollary Ln_times_of_real:
+    "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(of_real r * z) = ln r + Ln(z)"
+  using mpi_less_Im_Ln Im_Ln_le_pi
+  by (force simp: Ln_times)
+
+corollary Ln_divide_of_real:
+    "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(z / of_real r) = Ln(z) - ln r"
+using Ln_times_of_real [of "inverse r" z]
+by (simp add: ln_inverse Ln_of_real mult.commute divide_inverse of_real_inverse [symmetric] 
+         del: of_real_inverse)
+
 lemma Ln_minus:
   assumes "z \<noteq> 0"
     shows "Ln(-z) = (if Im(z) \<le> 0 \<and> ~(Re(z) < 0 \<and> Im(z) = 0)
@@ -1260,6 +1285,161 @@
   by (auto simp: of_real_numeral Ln_times)
 
 
+subsection{*Relation between Ln and Arg, and hence continuity of Arg*}
+
+lemma Arg_Ln: 
+  assumes "0 < Arg z" shows "Arg z = Im(Ln(-z)) + pi"
+proof (cases "z = 0")
+  case True
+  with assms show ?thesis
+    by simp
+next
+  case False
+  then have "z / of_real(norm z) = exp(ii * of_real(Arg z))"
+    using Arg [of z]
+    by (metis abs_norm_cancel nonzero_mult_divide_cancel_left norm_of_real zero_less_norm_iff)
+  then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg z) - pi))"
+    using cis_conv_exp cis_pi
+    by (auto simp: exp_diff algebra_simps)
+  then have "ln (- z / of_real(norm z)) = ln (exp (\<i> * (of_real (Arg z) - pi)))"
+    by simp
+  also have "... = \<i> * (of_real(Arg z) - pi)"
+    using Arg [of z] assms pi_not_less_zero
+    by auto
+  finally have "Arg z =  Im (Ln (- z / of_real (cmod z))) + pi"
+    by simp
+  also have "... = Im (Ln (-z) - ln (cmod z)) + pi"
+    by (metis diff_0_right minus_diff_eq zero_less_norm_iff Ln_divide_of_real False)
+  also have "... = Im (Ln (-z)) + pi"
+    by simp
+  finally show ?thesis .
+qed
+
+lemma continuous_at_Arg: 
+  assumes "z \<in> \<real> \<Longrightarrow> Re z < 0"
+    shows "continuous (at z) Arg"
+proof -
+  have *: "isCont (\<lambda>z. Im (Ln (- z)) + pi) z"
+    by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+
+  then show ?thesis
+    apply (simp add: continuous_at)
+    apply (rule Lim_transform_within_open [of "-{z. z \<in> \<real> & 0 \<le> Re z}" _ "\<lambda>z. Im(Ln(-z)) + pi"])
+    apply (simp add: closed_def [symmetric] closed_Collect_conj closed_complex_Reals closed_halfspace_Re_ge)
+    apply (simp_all add: assms not_le Arg_Ln [OF Arg_gt_0])
+    done
+qed
+
+text{*Relation between Arg and arctangent in upper halfplane*}
+lemma Arg_arctan_upperhalf: 
+  assumes "0 < Im z"
+    shows "Arg z = pi/2 - arctan(Re z / Im z)"
+proof (cases "z = 0")
+  case True with assms show ?thesis
+    by simp
+next
+  case False
+  show ?thesis
+    apply (rule Arg_unique [of "norm z"])
+    using False assms arctan [of "Re z / Im z"] pi_ge_two pi_half_less_two
+    apply (auto simp: exp_Euler cos_diff sin_diff)
+    using norm_complex_def [of z, symmetric]
+    apply (simp add: of_real_numeral sin_of_real cos_of_real sin_arctan cos_arctan field_simps real_sqrt_divide)
+    apply (metis complex_eq mult.assoc ring_class.ring_distribs(2))
+    done
+qed
+
+lemma Arg_eq_Im_Ln: 
+  assumes "0 \<le> Im z" "0 < Re z" 
+    shows "Arg z = Im (Ln z)"
+proof (cases "z = 0 \<or> Im z = 0")
+  case True then show ?thesis
+    using assms Arg_eq_0 complex_is_Real_iff  
+    apply auto
+    by (metis Arg_eq_0_pi Arg_eq_pi Im_Ln_eq_0 Im_Ln_eq_pi less_numeral_extra(3) zero_complex.simps(1))
+next
+  case False 
+  then have "Arg z > 0"
+    using Arg_gt_0 complex_is_Real_iff by blast
+  then show ?thesis
+    using assms False 
+    by (subst Arg_Ln) (auto simp: Ln_minus)
+qed
+
+lemma continuous_within_upperhalf_Arg: 
+  assumes "z \<noteq> 0"
+    shows "continuous (at z within {z. 0 \<le> Im z}) Arg"
+proof (cases "z \<in> \<real> & 0 \<le> Re z")
+  case False then show ?thesis
+    using continuous_at_Arg continuous_at_imp_continuous_within by auto
+next
+  case True
+  then have z: "z \<in> \<real>" "0 < Re z"
+    using assms  by (auto simp: complex_is_Real_iff complex_neq_0)
+  then have [simp]: "Arg z = 0" "Im (Ln z) = 0"
+    by (auto simp: Arg_eq_0 Im_Ln_eq_0 assms complex_is_Real_iff)
+  show ?thesis  
+  proof (clarsimp simp add: continuous_within Lim_within dist_norm)
+    fix e::real
+    assume "0 < e"
+    moreover have "continuous (at z) (\<lambda>x. Im (Ln x))"
+      using z  by (rule continuous_intros | simp)
+    ultimately
+    obtain d where d: "d>0" "\<And>x. x \<noteq> z \<Longrightarrow> cmod (x - z) < d \<Longrightarrow> \<bar>Im (Ln x)\<bar> < e"
+      by (auto simp: continuous_within Lim_within dist_norm)
+    { fix x
+      assume "cmod (x - z) < Re z / 2"
+      then have "\<bar>Re x - Re z\<bar> < Re z / 2"
+        by (metis le_less_trans abs_Re_le_cmod minus_complex.simps(1))
+      then have "0 < Re x"
+        using z by linarith
+    }
+    then show "\<exists>d>0. \<forall>x. 0 \<le> Im x \<longrightarrow> x \<noteq> z \<and> cmod (x - z) < d \<longrightarrow> \<bar>Arg x\<bar> < e"
+      apply (rule_tac x="min d (Re z / 2)" in exI)
+      using z d
+      apply (auto simp: Arg_eq_Im_Ln)
+      done
+  qed
+qed
+
+lemma continuous_on_upperhalf_Arg: "continuous_on ({z. 0 \<le> Im z} - {0}) Arg"
+  apply (auto simp: continuous_on_eq_continuous_within)
+  by (metis Diff_subset continuous_within_subset continuous_within_upperhalf_Arg)
+
+lemma open_Arg_less_Int: 
+  assumes "0 \<le> s" "t \<le> 2*pi"
+    shows "open ({y. s < Arg y} \<inter> {y. Arg y < t})"
+proof -
+  have 1: "continuous_on (UNIV - {z \<in> \<real>. 0 \<le> Re z}) Arg"
+    using continuous_at_Arg continuous_at_imp_continuous_within 
+    by (auto simp: continuous_on_eq_continuous_within set_diff_eq)
+  have 2: "open (UNIV - {z \<in> \<real>. 0 \<le> Re z})"
+    by (simp add: closed_Collect_conj closed_complex_Reals closed_halfspace_Re_ge open_Diff)
+  have "open ({z. s < z} \<inter> {z. z < t})"
+    using open_lessThan [of t] open_greaterThan [of s]
+    by (metis greaterThan_def lessThan_def open_Int)
+  moreover have "{y. s < Arg y} \<inter> {y. Arg y < t} \<subseteq> - {z \<in> \<real>. 0 \<le> Re z}"
+    using assms
+    by (auto simp: Arg_real)
+  ultimately show ?thesis
+    using continuous_imp_open_vimage [OF 1 2, of  "{z. Re z > s} \<inter> {z. Re z < t}"] 
+    by auto
+qed
+
+lemma open_Arg_gt: "open {z. t < Arg z}"
+proof (cases "t < 0")
+  case True then have "{z. t < Arg z} = UNIV"
+    using Arg_ge_0 less_le_trans by auto
+  then show ?thesis
+    by simp
+next
+  case False then show ?thesis
+    using open_Arg_less_Int [of t "2*pi"] Arg_lt_2pi
+    by auto
+qed
+
+lemma closed_Arg_le: "closed {z. Arg z \<le> t}"
+  using open_Arg_gt [of t]
+  by (simp add: closed_def Set.Collect_neg_eq [symmetric] not_le)
 
 subsection{*Complex Powers*}
 
@@ -1338,9 +1518,135 @@
   "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = Re w powr Re z"
   by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm)
 
-lemma cmod_Ln_Reals [simp]:"z \<in> Reals \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (Ln z) = norm (ln (Re z))"
+
+subsection{*Some Limits involving Logarithms*}
+        
+lemma lim_Ln_over_power:
+  fixes s::complex
+  assumes "0 < Re s"
+    shows "((\<lambda>n. Ln n / (n powr s)) ---> 0) sequentially"
+proof (simp add: lim_sequentially dist_norm, clarify)
+  fix e::real 
+  assume e: "0 < e"
+  have "\<exists>xo>0. \<forall>x\<ge>xo. 0 < e * 2 + (e * Re s * 2 - 2) * x + e * (Re s)\<^sup>2 * x\<^sup>2"
+  proof (rule_tac x="2/(e * (Re s)\<^sup>2)" in exI, safe)
+    show "0 < 2 / (e * (Re s)\<^sup>2)"
+      using e assms by (simp add: field_simps)
+  next
+    fix x::real
+    assume x: "2 / (e * (Re s)\<^sup>2) \<le> x"
+    then have "x>0"
+    using e assms
+      by (metis less_le_trans mult_eq_0_iff mult_pos_pos pos_less_divide_eq power2_eq_square
+                zero_less_numeral)
+    then show "0 < e * 2 + (e * Re s * 2 - 2) * x + e * (Re s)\<^sup>2 * x\<^sup>2"
+      using e assms x
+      apply (auto simp: field_simps)
+      apply (rule_tac y = "e * (x\<^sup>2 * (Re s)\<^sup>2)" in le_less_trans)
+      apply (auto simp: power2_eq_square field_simps add_pos_pos)
+      done
+  qed
+  then have "\<exists>xo>0. \<forall>x\<ge>xo. x / e < 1 + (Re s * x) + (1/2) * (Re s * x)^2"
+    using e  by (simp add: field_simps)
+  then have "\<exists>xo>0. \<forall>x\<ge>xo. x / e < exp (Re s * x)"
+    using assms
+    by (force intro: less_le_trans [OF _ exp_lower_taylor_quadratic])
+  then have "\<exists>xo>0. \<forall>x\<ge>xo. x < e * exp (Re s * x)"
+    using e   by (auto simp: field_simps)
+  with e show "\<exists>no. \<forall>n\<ge>no. norm (Ln (of_nat n) / of_nat n powr s) < e"
+    apply (auto simp: norm_divide norm_powr_real divide_simps)
+    apply (rule_tac x="nat (ceiling (exp xo))" in exI)
+    apply clarify
+    apply (drule_tac x="ln n" in spec)
+    apply (auto simp: real_of_nat_def exp_less_mono nat_ceiling_le_eq not_le)
+    apply (metis exp_less_mono exp_ln not_le of_nat_0_less_iff)
+    done
+qed
+
+lemma lim_Ln_over_n: "((\<lambda>n. Ln(of_nat n) / of_nat n) ---> 0) sequentially"
+  using lim_Ln_over_power [of 1]
+  by simp
+
+lemma Ln_Reals_eq: "x \<in> Reals \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
   using Ln_of_real by force
 
+lemma powr_Reals_eq: "x \<in> Reals \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"
+  by (simp add: powr_of_real)
+
+lemma lim_ln_over_power:
+  fixes s :: real
+  assumes "0 < s"
+    shows "((\<lambda>n. ln n / (n powr s)) ---> 0) sequentially"
+  using lim_Ln_over_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms
+  apply (subst filterlim_sequentially_Suc [symmetric])
+  apply (simp add: lim_sequentially dist_norm
+          Ln_Reals_eq norm_powr_real_powr norm_divide real_of_nat_def)
+  done
+
+lemma lim_ln_over_n: "((\<lambda>n. ln(real_of_nat n) / of_nat n) ---> 0) sequentially"
+  using lim_ln_over_power [of 1, THEN filterlim_sequentially_Suc [THEN iffD2]]
+  apply (subst filterlim_sequentially_Suc [symmetric])
+  apply (simp add: lim_sequentially dist_norm real_of_nat_def)
+  done
+
+lemma lim_1_over_complex_power:
+  assumes "0 < Re s"
+    shows "((\<lambda>n. 1 / (of_nat n powr s)) ---> 0) sequentially"
+proof -
+  have "\<forall>n>0. 3 \<le> n \<longrightarrow> 1 \<le> ln (real_of_nat n)"
+    using ln3_gt_1
+    by (force intro: order_trans [of _ "ln 3"] ln3_gt_1)
+  moreover have "(\<lambda>n. cmod (Ln (of_nat n) / of_nat n powr s)) ----> 0"
+    using lim_Ln_over_power [OF assms]
+    by (metis tendsto_norm_zero_iff)
+  ultimately show ?thesis
+    apply (auto intro!: Lim_null_comparison [where g = "\<lambda>n. norm (Ln(of_nat n) / of_nat n powr s)"])
+    apply (auto simp: norm_divide divide_simps eventually_sequentially)
+    done
+qed
+
+lemma lim_1_over_real_power:
+  fixes s :: real
+  assumes "0 < s"
+    shows "((\<lambda>n. 1 / (of_nat n powr s)) ---> 0) sequentially"
+  using lim_1_over_complex_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms
+  apply (subst filterlim_sequentially_Suc [symmetric])
+  apply (simp add: lim_sequentially dist_norm)
+  apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide real_of_nat_def)
+  done
+
+lemma lim_1_over_Ln: "((\<lambda>n. 1 / Ln(of_nat n)) ---> 0) sequentially"
+proof (clarsimp simp add: lim_sequentially dist_norm norm_divide divide_simps)
+  fix r::real
+  assume "0 < r"
+  have ir: "inverse (exp (inverse r)) > 0"
+    by simp
+  obtain n where n: "1 < of_nat n * inverse (exp (inverse r))"
+    using ex_less_of_nat_mult [of _ 1, OF ir]
+    by auto
+  then have "exp (inverse r) < of_nat n"
+    by (simp add: divide_simps)
+  then have "ln (exp (inverse r)) < ln (of_nat n)"
+    by (metis exp_gt_zero less_trans ln_exp ln_less_cancel_iff)
+  with `0 < r` have "1 < r * ln (real_of_nat n)"
+    by (simp add: field_simps)
+  moreover have "n > 0" using n
+    using neq0_conv by fastforce
+  ultimately show "\<exists>no. \<forall>n. Ln (of_nat n) \<noteq> 0 \<longrightarrow> no \<le> n \<longrightarrow> 1 < r * cmod (Ln (of_nat n))"
+    using n `0 < r`
+    apply (rule_tac x=n in exI)
+    apply (auto simp: divide_simps)
+    apply (erule less_le_trans, auto)
+    done
+qed
+
+lemma lim_1_over_ln: "((\<lambda>n. 1 / ln(real_of_nat n)) ---> 0) sequentially"
+  using lim_1_over_Ln [THEN filterlim_sequentially_Suc [THEN iffD2]] assms
+  apply (subst filterlim_sequentially_Suc [symmetric])
+  apply (simp add: lim_sequentially dist_norm)
+  apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide real_of_nat_def)
+  done
+
 
 subsection{*Relation between Square Root and exp/ln, hence its derivative*}
 
diff -r 9b0825a00b1a -r bd773c47ad0b src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Apr 28 16:23:05 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Apr 28 16:23:38 2015 +0100
@@ -28,7 +28,7 @@
 lemma square_continuous:
   fixes e :: real
   shows "e > 0 \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> \<bar>y * y - x * x\<bar> < e)"
-  using isCont_power[OF isCont_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
+  using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
   apply (auto simp add: power2_eq_square)
   apply (rule_tac x="s" in exI)
   apply auto
diff -r 9b0825a00b1a -r bd773c47ad0b src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Apr 28 16:23:05 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Apr 28 16:23:38 2015 +0100
@@ -4804,7 +4804,7 @@
 
 lemmas continuous_within_id = continuous_ident
 
-lemmas continuous_at_id = isCont_ident
+lemmas continuous_at_id = continuous_ident
 
 lemma continuous_infdist[continuous_intros]:
   assumes "continuous F f"
diff -r 9b0825a00b1a -r bd773c47ad0b src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Tue Apr 28 16:23:05 2015 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Tue Apr 28 16:23:38 2015 +0100
@@ -1345,7 +1345,7 @@
       by (intro tendsto_infdist lim)
     show "\<And>i. (\<lambda>x. infdist (f i x) A) \<in> borel_measurable M"
       by (intro borel_measurable_continuous_on[where f="\<lambda>x. infdist x A"]
-        continuous_at_imp_continuous_on ballI continuous_infdist isCont_ident) auto
+        continuous_at_imp_continuous_on ballI continuous_infdist continuous_ident) auto
   qed
 
   show "g -` A \<inter> space M \<in> sets M"
diff -r 9b0825a00b1a -r bd773c47ad0b src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue Apr 28 16:23:05 2015 +0100
+++ b/src/HOL/Set_Interval.thy	Tue Apr 28 16:23:38 2015 +0100
@@ -1298,7 +1298,14 @@
   "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m<..u} = {l..u}"
 by auto
 
-lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
+lemma ivl_disj_un_two_touch:
+  "[| (l::'a::linorder) < m; m < u |] ==> {l<..m} Un {m..<u} = {l<..<u}"
+  "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {m..<u} = {l..<u}"
+  "[| (l::'a::linorder) < m; m <= u |] ==> {l<..m} Un {m..u} = {l<..u}"
+  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m..u} = {l..u}"
+by auto
+
+lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two ivl_disj_un_two_touch
 
 subsubsection {* Disjoint Intersections *}
 
@@ -1498,6 +1505,20 @@
   apply (simp_all add: setsum_add_nat_ivl add.commute atLeast0LessThan[symmetric])
   done
 
+lemma setsum_triangle_reindex:
+  fixes n :: nat
+  shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
+  apply (simp add: setsum.Sigma)
+  apply (rule setsum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
+  apply auto
+  done
+
+lemma setsum_triangle_reindex_eq:
+  fixes n :: nat
+  shows "(\<Sum>(i,j)\<in>{(i,j). i+j \<le> n}. f i j) = (\<Sum>k\<le>n. \<Sum>i\<le>k. f i (k - i))"
+using setsum_triangle_reindex [of f "Suc n"]
+by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost)
+
 subsection{* Shifting bounds *}
 
 lemma setsum_shift_bounds_nat_ivl:
diff -r 9b0825a00b1a -r bd773c47ad0b src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Apr 28 16:23:05 2015 +0100
+++ b/src/HOL/Topological_Spaces.thy	Tue Apr 28 16:23:38 2015 +0100
@@ -1479,14 +1479,6 @@
 lemma continuous_at_imp_continuous_on: "\<forall>x\<in>s. isCont f x \<Longrightarrow> continuous_on s f"
   by (auto intro: continuous_at_within simp: continuous_on_eq_continuous_within)
 
-lemma isContI_continuous: "continuous (at x within UNIV) f \<Longrightarrow> isCont f x"
-  by simp
-
-lemma isCont_ident[continuous_intros, simp]: "isCont (\<lambda>x. x) a"
-  using continuous_ident by (rule isContI_continuous)
-
-lemmas isCont_const = continuous_const
-
 lemma isCont_o2: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
   unfolding isCont_def by (rule tendsto_compose)
 
diff -r 9b0825a00b1a -r bd773c47ad0b src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Apr 28 16:23:05 2015 +0100
+++ b/src/HOL/Transcendental.thy	Tue Apr 28 16:23:38 2015 +0100
@@ -4781,6 +4781,11 @@
     using cos_gt_zero_pi [OF 1 2] by (simp add: arctan tan_add)
 qed
 
+lemma arctan_double:
+  assumes "\<bar>x\<bar> < 1"
+  shows "2 * arctan x = arctan ((2*x) / (1 - x\<^sup>2))"
+  by (metis assms arctan_add linear mult_2 not_less power2_eq_square)
+
 theorem machin: "pi / 4 = 4 * arctan (1/5) - arctan (1 / 239)"
 proof -
   have "\<bar>1 / 5\<bar> < (1 :: real)" by auto
@@ -4798,6 +4803,35 @@
   thus ?thesis unfolding arctan_one by algebra
 qed
 
+lemma machin_Euler: "5 * arctan(1/7) + 2 * arctan(3/79) = pi/4"
+proof -
+  have 17: "\<bar>1/7\<bar> < (1 :: real)" by auto
+  with arctan_double
+  have "2 * arctan (1/7) = arctan (7/24)"  by auto
+  moreover
+  have "\<bar>7/24\<bar> < (1 :: real)" by auto
+  with arctan_double
+  have "2 * arctan (7/24) = arctan (336/527)"  by auto
+  moreover
+  have "\<bar>336/527\<bar> < (1 :: real)" by auto
+  from arctan_add[OF less_imp_le[OF 17] this]
+  have "arctan(1/7) + arctan (336/527) = arctan (2879/3353)"  by auto 
+  ultimately have I: "5 * arctan(1/7) = arctan (2879/3353)"  by auto
+  have 379: "\<bar>3/79\<bar> < (1 :: real)" by auto
+  with arctan_double
+  have II: "2 * arctan (3/79) = arctan (237/3116)"  by auto
+  have *: "\<bar>2879/3353\<bar> < (1 :: real)" by auto
+  have "\<bar>237/3116\<bar> < (1 :: real)" by auto
+  from arctan_add[OF less_imp_le[OF *] this]
+  have "arctan (2879/3353) + arctan (237/3116) = pi/4"
+    by (simp add: arctan_one)
+  then show ?thesis using I II
+    by auto
+qed
+
+(*But could also prove MACHIN_GAUSS:
+  12 * arctan(1/18) + 8 * arctan(1/57) - 5 * arctan(1/239) = pi/4*)
+
 
 subsection {* Introducing the inverse tangent power series *}
 
@@ -5110,8 +5144,8 @@
       hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
       moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
         unfolding diff_conv_add_uminus divide_inverse
-        by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan
-          isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum
+        by (auto intro!: isCont_add isCont_rabs continuous_ident isCont_minus isCont_arctan
+          isCont_inverse isCont_mult isCont_power continuous_const isCont_setsum
           simp del: add_uminus_conv_diff)
       ultimately have "0 \<le> ?a 1 n - ?diff 1 n"
         by (rule LIM_less_bound)
@@ -5282,8 +5316,57 @@
 qed
 
 
-subsection{*Basics about polynomial functions: extremal behaviour and root counts*}
-(*ALL COULD GO TO COMPLEX_MAIN OR EARLIER*)
+subsection{*Basics about polynomial functions: products, extremal behaviour and root counts*}
+
+lemma pairs_le_eq_Sigma:
+  fixes m::nat
+  shows "{(i,j). i+j \<le> m} = Sigma (atMost m) (\<lambda>r. atMost (m-r))"
+by auto
+
+lemma setsum_up_index_split:
+    "(\<Sum>k\<le>m + n. f k) = (\<Sum>k\<le>m. f k) + (\<Sum>k = Suc m..m + n. f k)"
+  by (metis atLeast0AtMost Suc_eq_plus1 le0 setsum_ub_add_nat)
+
+lemma Sigma_interval_disjoint:
+  fixes w :: "'a::order"
+  shows "(SIGMA i:A. {..v i}) \<inter> (SIGMA i:A.{v i<..w}) = {}"
+    by auto
+
+lemma product_atMost_eq_Un:
+  fixes m :: nat
+  shows "A \<times> {..m} = (SIGMA i:A.{..m - i}) \<union> (SIGMA i:A.{m - i<..m})"
+    by auto
+
+lemma polynomial_product: (*with thanks to Chaitanya Mangla*)
+  fixes x:: "'a :: idom"
+  assumes m: "\<And>i. i>m \<Longrightarrow> (a i) = 0" and n: "\<And>j. j>n \<Longrightarrow> (b j) = 0"
+  shows "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) = 
+         (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
+proof -
+  have "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) = (\<Sum>i\<le>m. \<Sum>j\<le>n. (a i * x ^ i) * (b j * x ^ j))"
+    by (rule setsum_product)
+  also have "... = (\<Sum>i\<le>m + n. \<Sum>j\<le>n + m. a i * x ^ i * (b j * x ^ j))"
+    using assms by (auto simp: setsum_up_index_split)
+  also have "... = (\<Sum>r\<le>m + n. \<Sum>j\<le>m + n - r. a r * x ^ r * (b j * x ^ j))"
+    apply (simp add: add_ac setsum.Sigma product_atMost_eq_Un)
+    apply (clarsimp simp add: setsum_Un Sigma_interval_disjoint intro!: setsum.neutral)
+    by (metis add_diff_assoc2 add.commute add_lessD1 leD m n nat_le_linear neqE)
+  also have "... = (\<Sum>(i,j)\<in>{(i,j). i+j \<le> m+n}. (a i * x ^ i) * (b j * x ^ j))"
+    by (auto simp: pairs_le_eq_Sigma setsum.Sigma)
+  also have "... = (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
+    apply (subst setsum_triangle_reindex_eq)  
+    apply (auto simp: algebra_simps setsum_right_distrib intro!: setsum.cong)
+    by (metis le_add_diff_inverse power_add)
+  finally show ?thesis .
+qed
+
+lemma polynomial_product_nat: 
+  fixes x:: nat
+  assumes m: "\<And>i. i>m \<Longrightarrow> (a i) = 0" and n: "\<And>j. j>n \<Longrightarrow> (b j) = 0"
+  shows "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) = 
+         (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
+  using polynomial_product [of m a n b x] assms
+  by (simp add: Int.zpower_int Int.zmult_int Int.int_setsum [symmetric])
 
 lemma polyfun_diff: (*COMPLEX_SUB_POLYFUN in HOL Light*)
     fixes x :: "'a::idom"
@@ -5357,6 +5440,9 @@
   using polyfun_linear_factor [of c n a] assms
   by auto
 
+(*The material of this section, up until this point, could go into a new theory of polynomials
+  based on Main alone. The remaining material involves limits, continuity, series, etc.*)
+
 lemma isCont_polynom:
   fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
   shows "isCont (\<lambda>w. \<Sum>i\<le>n. c i * w^i) a"