New material about complex transcendental functions (especially Ln, Arg) and polynomials
authorpaulson <lp15@cam.ac.uk>
Tue Apr 28 16:23:38 2015 +0100 (2015-04-28)
changeset 60150bd773c47ad0b
parent 60149 9b0825a00b1a
child 60151 9023d59acce6
New material about complex transcendental functions (especially Ln, Arg) and polynomials
src/HOL/Inequalities.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Set_Interval.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Inequalities.thy	Tue Apr 28 16:23:05 2015 +0100
     1.2 +++ b/src/HOL/Inequalities.thy	Tue Apr 28 16:23:38 2015 +0100
     1.3 @@ -7,14 +7,6 @@
     1.4    imports Real_Vector_Spaces
     1.5  begin
     1.6  
     1.7 -lemma setsum_triangle_reindex:
     1.8 -  fixes n :: nat
     1.9 -  shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
    1.10 -  apply (simp add: setsum.Sigma)
    1.11 -  apply (rule setsum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
    1.12 -  apply auto
    1.13 -  done
    1.14 -
    1.15  lemma gauss_sum_div2: "(2::'a::semiring_div) \<noteq> 0 \<Longrightarrow>
    1.16    setsum of_nat {1..n} = of_nat n * (of_nat n + 1) div (2::'a)"
    1.17  using gauss_sum[where n=n and 'a = 'a,symmetric] by auto
     2.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Tue Apr 28 16:23:05 2015 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Tue Apr 28 16:23:38 2015 +0100
     2.3 @@ -240,7 +240,7 @@
     2.4      and closed_halfspace_Im_le: "closed {z. Im(z) \<le> b}"
     2.5      and closed_halfspace_Im_eq: "closed {z. Im(z) = b}"
     2.6    by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re
     2.7 -            isCont_Im isCont_ident isCont_const)+
     2.8 +            isCont_Im continuous_ident continuous_const)+
     2.9  
    2.10  lemma closed_complex_Reals: "closed (Reals :: complex set)"
    2.11  proof -
     3.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Apr 28 16:23:05 2015 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Apr 28 16:23:38 2015 +0100
     3.3 @@ -42,11 +42,8 @@
     3.4  
     3.5  subsection{*The Exponential Function is Differentiable and Continuous*}
     3.6  
     3.7 -lemma complex_differentiable_at_exp: "exp complex_differentiable at z"
     3.8 -  using DERIV_exp complex_differentiable_def by blast
     3.9 -
    3.10  lemma complex_differentiable_within_exp: "exp complex_differentiable (at z within s)"
    3.11 -  by (simp add: complex_differentiable_at_exp complex_differentiable_at_within)
    3.12 +  using DERIV_exp complex_differentiable_at_within complex_differentiable_def by blast
    3.13  
    3.14  lemma continuous_within_exp:
    3.15    fixes z::"'a::{real_normed_field,banach}"
    3.16 @@ -777,6 +774,11 @@
    3.17      by blast
    3.18  qed
    3.19  
    3.20 +corollary Arg_gt_0: 
    3.21 +  assumes "z \<in> \<real> \<Longrightarrow> Re z < 0"
    3.22 +    shows "Arg z > 0"
    3.23 +  using Arg_eq_0 Arg_ge_0 assms dual_order.strict_iff_order by fastforce
    3.24 +
    3.25  lemma Arg_of_real: "Arg(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
    3.26    by (simp add: Arg_eq_0)
    3.27  
    3.28 @@ -952,6 +954,12 @@
    3.29  corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> ln z \<in> \<real>"
    3.30    by (auto simp: Ln_of_real elim: Reals_cases)
    3.31  
    3.32 +corollary Im_Ln_of_real [simp]: "r > 0 \<Longrightarrow> Im (ln (of_real r)) = 0"
    3.33 +  by (simp add: Ln_of_real)
    3.34 +
    3.35 +lemma cmod_Ln_Reals [simp]: "z \<in> Reals \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
    3.36 +  using Ln_of_real by force
    3.37 +
    3.38  lemma Ln_1: "ln 1 = (0::complex)"
    3.39  proof -
    3.40    have "ln (exp 0) = (0::complex)"
    3.41 @@ -975,7 +983,13 @@
    3.42    using Ln_exp by blast
    3.43  
    3.44  lemma Re_Ln [simp]: "z \<noteq> 0 \<Longrightarrow> Re(Ln z) = ln(norm z)"
    3.45 -by (metis exp_Ln assms ln_exp norm_exp_eq_Re)
    3.46 +  by (metis exp_Ln assms ln_exp norm_exp_eq_Re)
    3.47 +
    3.48 +corollary ln_cmod_le: 
    3.49 +  assumes z: "z \<noteq> 0"
    3.50 +    shows "ln (cmod z) \<le> cmod (Ln z)"
    3.51 +  using norm_exp [of "Ln z", simplified exp_Ln [OF z]]
    3.52 +  by (metis Re_Ln complex_Re_le_cmod z)
    3.53  
    3.54  lemma exists_complex_root:
    3.55    fixes a :: complex
    3.56 @@ -1185,7 +1199,7 @@
    3.57    also have "... = - (Ln ii)"
    3.58      by (metis Ln_inverse ii.sel(2) inverse_eq_divide zero_neq_one)
    3.59    also have "... = - (ii * pi/2)"
    3.60 -    by (simp add: Ln_ii)
    3.61 +    by simp
    3.62    finally show ?thesis .
    3.63  qed
    3.64  
    3.65 @@ -1201,11 +1215,22 @@
    3.66    using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z]
    3.67    by (auto simp: of_real_numeral exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique)
    3.68  
    3.69 -lemma Ln_times_simple:
    3.70 +corollary Ln_times_simple:
    3.71      "\<lbrakk>w \<noteq> 0; z \<noteq> 0; -pi < Im(Ln w) + Im(Ln z); Im(Ln w) + Im(Ln z) \<le> pi\<rbrakk>
    3.72           \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z)"
    3.73    by (simp add: Ln_times)
    3.74  
    3.75 +corollary Ln_times_of_real:
    3.76 +    "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(of_real r * z) = ln r + Ln(z)"
    3.77 +  using mpi_less_Im_Ln Im_Ln_le_pi
    3.78 +  by (force simp: Ln_times)
    3.79 +
    3.80 +corollary Ln_divide_of_real:
    3.81 +    "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(z / of_real r) = Ln(z) - ln r"
    3.82 +using Ln_times_of_real [of "inverse r" z]
    3.83 +by (simp add: ln_inverse Ln_of_real mult.commute divide_inverse of_real_inverse [symmetric] 
    3.84 +         del: of_real_inverse)
    3.85 +
    3.86  lemma Ln_minus:
    3.87    assumes "z \<noteq> 0"
    3.88      shows "Ln(-z) = (if Im(z) \<le> 0 \<and> ~(Re(z) < 0 \<and> Im(z) = 0)
    3.89 @@ -1260,6 +1285,161 @@
    3.90    by (auto simp: of_real_numeral Ln_times)
    3.91  
    3.92  
    3.93 +subsection{*Relation between Ln and Arg, and hence continuity of Arg*}
    3.94 +
    3.95 +lemma Arg_Ln: 
    3.96 +  assumes "0 < Arg z" shows "Arg z = Im(Ln(-z)) + pi"
    3.97 +proof (cases "z = 0")
    3.98 +  case True
    3.99 +  with assms show ?thesis
   3.100 +    by simp
   3.101 +next
   3.102 +  case False
   3.103 +  then have "z / of_real(norm z) = exp(ii * of_real(Arg z))"
   3.104 +    using Arg [of z]
   3.105 +    by (metis abs_norm_cancel nonzero_mult_divide_cancel_left norm_of_real zero_less_norm_iff)
   3.106 +  then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg z) - pi))"
   3.107 +    using cis_conv_exp cis_pi
   3.108 +    by (auto simp: exp_diff algebra_simps)
   3.109 +  then have "ln (- z / of_real(norm z)) = ln (exp (\<i> * (of_real (Arg z) - pi)))"
   3.110 +    by simp
   3.111 +  also have "... = \<i> * (of_real(Arg z) - pi)"
   3.112 +    using Arg [of z] assms pi_not_less_zero
   3.113 +    by auto
   3.114 +  finally have "Arg z =  Im (Ln (- z / of_real (cmod z))) + pi"
   3.115 +    by simp
   3.116 +  also have "... = Im (Ln (-z) - ln (cmod z)) + pi"
   3.117 +    by (metis diff_0_right minus_diff_eq zero_less_norm_iff Ln_divide_of_real False)
   3.118 +  also have "... = Im (Ln (-z)) + pi"
   3.119 +    by simp
   3.120 +  finally show ?thesis .
   3.121 +qed
   3.122 +
   3.123 +lemma continuous_at_Arg: 
   3.124 +  assumes "z \<in> \<real> \<Longrightarrow> Re z < 0"
   3.125 +    shows "continuous (at z) Arg"
   3.126 +proof -
   3.127 +  have *: "isCont (\<lambda>z. Im (Ln (- z)) + pi) z"
   3.128 +    by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+
   3.129 +  then show ?thesis
   3.130 +    apply (simp add: continuous_at)
   3.131 +    apply (rule Lim_transform_within_open [of "-{z. z \<in> \<real> & 0 \<le> Re z}" _ "\<lambda>z. Im(Ln(-z)) + pi"])
   3.132 +    apply (simp add: closed_def [symmetric] closed_Collect_conj closed_complex_Reals closed_halfspace_Re_ge)
   3.133 +    apply (simp_all add: assms not_le Arg_Ln [OF Arg_gt_0])
   3.134 +    done
   3.135 +qed
   3.136 +
   3.137 +text{*Relation between Arg and arctangent in upper halfplane*}
   3.138 +lemma Arg_arctan_upperhalf: 
   3.139 +  assumes "0 < Im z"
   3.140 +    shows "Arg z = pi/2 - arctan(Re z / Im z)"
   3.141 +proof (cases "z = 0")
   3.142 +  case True with assms show ?thesis
   3.143 +    by simp
   3.144 +next
   3.145 +  case False
   3.146 +  show ?thesis
   3.147 +    apply (rule Arg_unique [of "norm z"])
   3.148 +    using False assms arctan [of "Re z / Im z"] pi_ge_two pi_half_less_two
   3.149 +    apply (auto simp: exp_Euler cos_diff sin_diff)
   3.150 +    using norm_complex_def [of z, symmetric]
   3.151 +    apply (simp add: of_real_numeral sin_of_real cos_of_real sin_arctan cos_arctan field_simps real_sqrt_divide)
   3.152 +    apply (metis complex_eq mult.assoc ring_class.ring_distribs(2))
   3.153 +    done
   3.154 +qed
   3.155 +
   3.156 +lemma Arg_eq_Im_Ln: 
   3.157 +  assumes "0 \<le> Im z" "0 < Re z" 
   3.158 +    shows "Arg z = Im (Ln z)"
   3.159 +proof (cases "z = 0 \<or> Im z = 0")
   3.160 +  case True then show ?thesis
   3.161 +    using assms Arg_eq_0 complex_is_Real_iff  
   3.162 +    apply auto
   3.163 +    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))
   3.164 +next
   3.165 +  case False 
   3.166 +  then have "Arg z > 0"
   3.167 +    using Arg_gt_0 complex_is_Real_iff by blast
   3.168 +  then show ?thesis
   3.169 +    using assms False 
   3.170 +    by (subst Arg_Ln) (auto simp: Ln_minus)
   3.171 +qed
   3.172 +
   3.173 +lemma continuous_within_upperhalf_Arg: 
   3.174 +  assumes "z \<noteq> 0"
   3.175 +    shows "continuous (at z within {z. 0 \<le> Im z}) Arg"
   3.176 +proof (cases "z \<in> \<real> & 0 \<le> Re z")
   3.177 +  case False then show ?thesis
   3.178 +    using continuous_at_Arg continuous_at_imp_continuous_within by auto
   3.179 +next
   3.180 +  case True
   3.181 +  then have z: "z \<in> \<real>" "0 < Re z"
   3.182 +    using assms  by (auto simp: complex_is_Real_iff complex_neq_0)
   3.183 +  then have [simp]: "Arg z = 0" "Im (Ln z) = 0"
   3.184 +    by (auto simp: Arg_eq_0 Im_Ln_eq_0 assms complex_is_Real_iff)
   3.185 +  show ?thesis  
   3.186 +  proof (clarsimp simp add: continuous_within Lim_within dist_norm)
   3.187 +    fix e::real
   3.188 +    assume "0 < e"
   3.189 +    moreover have "continuous (at z) (\<lambda>x. Im (Ln x))"
   3.190 +      using z  by (rule continuous_intros | simp)
   3.191 +    ultimately
   3.192 +    obtain d where d: "d>0" "\<And>x. x \<noteq> z \<Longrightarrow> cmod (x - z) < d \<Longrightarrow> \<bar>Im (Ln x)\<bar> < e"
   3.193 +      by (auto simp: continuous_within Lim_within dist_norm)
   3.194 +    { fix x
   3.195 +      assume "cmod (x - z) < Re z / 2"
   3.196 +      then have "\<bar>Re x - Re z\<bar> < Re z / 2"
   3.197 +        by (metis le_less_trans abs_Re_le_cmod minus_complex.simps(1))
   3.198 +      then have "0 < Re x"
   3.199 +        using z by linarith
   3.200 +    }
   3.201 +    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"
   3.202 +      apply (rule_tac x="min d (Re z / 2)" in exI)
   3.203 +      using z d
   3.204 +      apply (auto simp: Arg_eq_Im_Ln)
   3.205 +      done
   3.206 +  qed
   3.207 +qed
   3.208 +
   3.209 +lemma continuous_on_upperhalf_Arg: "continuous_on ({z. 0 \<le> Im z} - {0}) Arg"
   3.210 +  apply (auto simp: continuous_on_eq_continuous_within)
   3.211 +  by (metis Diff_subset continuous_within_subset continuous_within_upperhalf_Arg)
   3.212 +
   3.213 +lemma open_Arg_less_Int: 
   3.214 +  assumes "0 \<le> s" "t \<le> 2*pi"
   3.215 +    shows "open ({y. s < Arg y} \<inter> {y. Arg y < t})"
   3.216 +proof -
   3.217 +  have 1: "continuous_on (UNIV - {z \<in> \<real>. 0 \<le> Re z}) Arg"
   3.218 +    using continuous_at_Arg continuous_at_imp_continuous_within 
   3.219 +    by (auto simp: continuous_on_eq_continuous_within set_diff_eq)
   3.220 +  have 2: "open (UNIV - {z \<in> \<real>. 0 \<le> Re z})"
   3.221 +    by (simp add: closed_Collect_conj closed_complex_Reals closed_halfspace_Re_ge open_Diff)
   3.222 +  have "open ({z. s < z} \<inter> {z. z < t})"
   3.223 +    using open_lessThan [of t] open_greaterThan [of s]
   3.224 +    by (metis greaterThan_def lessThan_def open_Int)
   3.225 +  moreover have "{y. s < Arg y} \<inter> {y. Arg y < t} \<subseteq> - {z \<in> \<real>. 0 \<le> Re z}"
   3.226 +    using assms
   3.227 +    by (auto simp: Arg_real)
   3.228 +  ultimately show ?thesis
   3.229 +    using continuous_imp_open_vimage [OF 1 2, of  "{z. Re z > s} \<inter> {z. Re z < t}"] 
   3.230 +    by auto
   3.231 +qed
   3.232 +
   3.233 +lemma open_Arg_gt: "open {z. t < Arg z}"
   3.234 +proof (cases "t < 0")
   3.235 +  case True then have "{z. t < Arg z} = UNIV"
   3.236 +    using Arg_ge_0 less_le_trans by auto
   3.237 +  then show ?thesis
   3.238 +    by simp
   3.239 +next
   3.240 +  case False then show ?thesis
   3.241 +    using open_Arg_less_Int [of t "2*pi"] Arg_lt_2pi
   3.242 +    by auto
   3.243 +qed
   3.244 +
   3.245 +lemma closed_Arg_le: "closed {z. Arg z \<le> t}"
   3.246 +  using open_Arg_gt [of t]
   3.247 +  by (simp add: closed_def Set.Collect_neg_eq [symmetric] not_le)
   3.248  
   3.249  subsection{*Complex Powers*}
   3.250  
   3.251 @@ -1338,9 +1518,135 @@
   3.252    "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = Re w powr Re z"
   3.253    by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm)
   3.254  
   3.255 -lemma cmod_Ln_Reals [simp]:"z \<in> Reals \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (Ln z) = norm (ln (Re z))"
   3.256 +
   3.257 +subsection{*Some Limits involving Logarithms*}
   3.258 +        
   3.259 +lemma lim_Ln_over_power:
   3.260 +  fixes s::complex
   3.261 +  assumes "0 < Re s"
   3.262 +    shows "((\<lambda>n. Ln n / (n powr s)) ---> 0) sequentially"
   3.263 +proof (simp add: lim_sequentially dist_norm, clarify)
   3.264 +  fix e::real 
   3.265 +  assume e: "0 < e"
   3.266 +  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"
   3.267 +  proof (rule_tac x="2/(e * (Re s)\<^sup>2)" in exI, safe)
   3.268 +    show "0 < 2 / (e * (Re s)\<^sup>2)"
   3.269 +      using e assms by (simp add: field_simps)
   3.270 +  next
   3.271 +    fix x::real
   3.272 +    assume x: "2 / (e * (Re s)\<^sup>2) \<le> x"
   3.273 +    then have "x>0"
   3.274 +    using e assms
   3.275 +      by (metis less_le_trans mult_eq_0_iff mult_pos_pos pos_less_divide_eq power2_eq_square
   3.276 +                zero_less_numeral)
   3.277 +    then show "0 < e * 2 + (e * Re s * 2 - 2) * x + e * (Re s)\<^sup>2 * x\<^sup>2"
   3.278 +      using e assms x
   3.279 +      apply (auto simp: field_simps)
   3.280 +      apply (rule_tac y = "e * (x\<^sup>2 * (Re s)\<^sup>2)" in le_less_trans)
   3.281 +      apply (auto simp: power2_eq_square field_simps add_pos_pos)
   3.282 +      done
   3.283 +  qed
   3.284 +  then have "\<exists>xo>0. \<forall>x\<ge>xo. x / e < 1 + (Re s * x) + (1/2) * (Re s * x)^2"
   3.285 +    using e  by (simp add: field_simps)
   3.286 +  then have "\<exists>xo>0. \<forall>x\<ge>xo. x / e < exp (Re s * x)"
   3.287 +    using assms
   3.288 +    by (force intro: less_le_trans [OF _ exp_lower_taylor_quadratic])
   3.289 +  then have "\<exists>xo>0. \<forall>x\<ge>xo. x < e * exp (Re s * x)"
   3.290 +    using e   by (auto simp: field_simps)
   3.291 +  with e show "\<exists>no. \<forall>n\<ge>no. norm (Ln (of_nat n) / of_nat n powr s) < e"
   3.292 +    apply (auto simp: norm_divide norm_powr_real divide_simps)
   3.293 +    apply (rule_tac x="nat (ceiling (exp xo))" in exI)
   3.294 +    apply clarify
   3.295 +    apply (drule_tac x="ln n" in spec)
   3.296 +    apply (auto simp: real_of_nat_def exp_less_mono nat_ceiling_le_eq not_le)
   3.297 +    apply (metis exp_less_mono exp_ln not_le of_nat_0_less_iff)
   3.298 +    done
   3.299 +qed
   3.300 +
   3.301 +lemma lim_Ln_over_n: "((\<lambda>n. Ln(of_nat n) / of_nat n) ---> 0) sequentially"
   3.302 +  using lim_Ln_over_power [of 1]
   3.303 +  by simp
   3.304 +
   3.305 +lemma Ln_Reals_eq: "x \<in> Reals \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
   3.306    using Ln_of_real by force
   3.307  
   3.308 +lemma powr_Reals_eq: "x \<in> Reals \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"
   3.309 +  by (simp add: powr_of_real)
   3.310 +
   3.311 +lemma lim_ln_over_power:
   3.312 +  fixes s :: real
   3.313 +  assumes "0 < s"
   3.314 +    shows "((\<lambda>n. ln n / (n powr s)) ---> 0) sequentially"
   3.315 +  using lim_Ln_over_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms
   3.316 +  apply (subst filterlim_sequentially_Suc [symmetric])
   3.317 +  apply (simp add: lim_sequentially dist_norm
   3.318 +          Ln_Reals_eq norm_powr_real_powr norm_divide real_of_nat_def)
   3.319 +  done
   3.320 +
   3.321 +lemma lim_ln_over_n: "((\<lambda>n. ln(real_of_nat n) / of_nat n) ---> 0) sequentially"
   3.322 +  using lim_ln_over_power [of 1, THEN filterlim_sequentially_Suc [THEN iffD2]]
   3.323 +  apply (subst filterlim_sequentially_Suc [symmetric])
   3.324 +  apply (simp add: lim_sequentially dist_norm real_of_nat_def)
   3.325 +  done
   3.326 +
   3.327 +lemma lim_1_over_complex_power:
   3.328 +  assumes "0 < Re s"
   3.329 +    shows "((\<lambda>n. 1 / (of_nat n powr s)) ---> 0) sequentially"
   3.330 +proof -
   3.331 +  have "\<forall>n>0. 3 \<le> n \<longrightarrow> 1 \<le> ln (real_of_nat n)"
   3.332 +    using ln3_gt_1
   3.333 +    by (force intro: order_trans [of _ "ln 3"] ln3_gt_1)
   3.334 +  moreover have "(\<lambda>n. cmod (Ln (of_nat n) / of_nat n powr s)) ----> 0"
   3.335 +    using lim_Ln_over_power [OF assms]
   3.336 +    by (metis tendsto_norm_zero_iff)
   3.337 +  ultimately show ?thesis
   3.338 +    apply (auto intro!: Lim_null_comparison [where g = "\<lambda>n. norm (Ln(of_nat n) / of_nat n powr s)"])
   3.339 +    apply (auto simp: norm_divide divide_simps eventually_sequentially)
   3.340 +    done
   3.341 +qed
   3.342 +
   3.343 +lemma lim_1_over_real_power:
   3.344 +  fixes s :: real
   3.345 +  assumes "0 < s"
   3.346 +    shows "((\<lambda>n. 1 / (of_nat n powr s)) ---> 0) sequentially"
   3.347 +  using lim_1_over_complex_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms
   3.348 +  apply (subst filterlim_sequentially_Suc [symmetric])
   3.349 +  apply (simp add: lim_sequentially dist_norm)
   3.350 +  apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide real_of_nat_def)
   3.351 +  done
   3.352 +
   3.353 +lemma lim_1_over_Ln: "((\<lambda>n. 1 / Ln(of_nat n)) ---> 0) sequentially"
   3.354 +proof (clarsimp simp add: lim_sequentially dist_norm norm_divide divide_simps)
   3.355 +  fix r::real
   3.356 +  assume "0 < r"
   3.357 +  have ir: "inverse (exp (inverse r)) > 0"
   3.358 +    by simp
   3.359 +  obtain n where n: "1 < of_nat n * inverse (exp (inverse r))"
   3.360 +    using ex_less_of_nat_mult [of _ 1, OF ir]
   3.361 +    by auto
   3.362 +  then have "exp (inverse r) < of_nat n"
   3.363 +    by (simp add: divide_simps)
   3.364 +  then have "ln (exp (inverse r)) < ln (of_nat n)"
   3.365 +    by (metis exp_gt_zero less_trans ln_exp ln_less_cancel_iff)
   3.366 +  with `0 < r` have "1 < r * ln (real_of_nat n)"
   3.367 +    by (simp add: field_simps)
   3.368 +  moreover have "n > 0" using n
   3.369 +    using neq0_conv by fastforce
   3.370 +  ultimately show "\<exists>no. \<forall>n. Ln (of_nat n) \<noteq> 0 \<longrightarrow> no \<le> n \<longrightarrow> 1 < r * cmod (Ln (of_nat n))"
   3.371 +    using n `0 < r`
   3.372 +    apply (rule_tac x=n in exI)
   3.373 +    apply (auto simp: divide_simps)
   3.374 +    apply (erule less_le_trans, auto)
   3.375 +    done
   3.376 +qed
   3.377 +
   3.378 +lemma lim_1_over_ln: "((\<lambda>n. 1 / ln(real_of_nat n)) ---> 0) sequentially"
   3.379 +  using lim_1_over_Ln [THEN filterlim_sequentially_Suc [THEN iffD2]] assms
   3.380 +  apply (subst filterlim_sequentially_Suc [symmetric])
   3.381 +  apply (simp add: lim_sequentially dist_norm)
   3.382 +  apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide real_of_nat_def)
   3.383 +  done
   3.384 +
   3.385  
   3.386  subsection{*Relation between Square Root and exp/ln, hence its derivative*}
   3.387  
     4.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Apr 28 16:23:05 2015 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Apr 28 16:23:38 2015 +0100
     4.3 @@ -28,7 +28,7 @@
     4.4  lemma square_continuous:
     4.5    fixes e :: real
     4.6    shows "e > 0 \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> \<bar>y * y - x * x\<bar> < e)"
     4.7 -  using isCont_power[OF isCont_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
     4.8 +  using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
     4.9    apply (auto simp add: power2_eq_square)
    4.10    apply (rule_tac x="s" in exI)
    4.11    apply auto
     5.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Apr 28 16:23:05 2015 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Apr 28 16:23:38 2015 +0100
     5.3 @@ -4804,7 +4804,7 @@
     5.4  
     5.5  lemmas continuous_within_id = continuous_ident
     5.6  
     5.7 -lemmas continuous_at_id = isCont_ident
     5.8 +lemmas continuous_at_id = continuous_ident
     5.9  
    5.10  lemma continuous_infdist[continuous_intros]:
    5.11    assumes "continuous F f"
     6.1 --- a/src/HOL/Probability/Borel_Space.thy	Tue Apr 28 16:23:05 2015 +0100
     6.2 +++ b/src/HOL/Probability/Borel_Space.thy	Tue Apr 28 16:23:38 2015 +0100
     6.3 @@ -1345,7 +1345,7 @@
     6.4        by (intro tendsto_infdist lim)
     6.5      show "\<And>i. (\<lambda>x. infdist (f i x) A) \<in> borel_measurable M"
     6.6        by (intro borel_measurable_continuous_on[where f="\<lambda>x. infdist x A"]
     6.7 -        continuous_at_imp_continuous_on ballI continuous_infdist isCont_ident) auto
     6.8 +        continuous_at_imp_continuous_on ballI continuous_infdist continuous_ident) auto
     6.9    qed
    6.10  
    6.11    show "g -` A \<inter> space M \<in> sets M"
     7.1 --- a/src/HOL/Set_Interval.thy	Tue Apr 28 16:23:05 2015 +0100
     7.2 +++ b/src/HOL/Set_Interval.thy	Tue Apr 28 16:23:38 2015 +0100
     7.3 @@ -1298,7 +1298,14 @@
     7.4    "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m<..u} = {l..u}"
     7.5  by auto
     7.6  
     7.7 -lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
     7.8 +lemma ivl_disj_un_two_touch:
     7.9 +  "[| (l::'a::linorder) < m; m < u |] ==> {l<..m} Un {m..<u} = {l<..<u}"
    7.10 +  "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {m..<u} = {l..<u}"
    7.11 +  "[| (l::'a::linorder) < m; m <= u |] ==> {l<..m} Un {m..u} = {l<..u}"
    7.12 +  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m..u} = {l..u}"
    7.13 +by auto
    7.14 +
    7.15 +lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two ivl_disj_un_two_touch
    7.16  
    7.17  subsubsection {* Disjoint Intersections *}
    7.18  
    7.19 @@ -1498,6 +1505,20 @@
    7.20    apply (simp_all add: setsum_add_nat_ivl add.commute atLeast0LessThan[symmetric])
    7.21    done
    7.22  
    7.23 +lemma setsum_triangle_reindex:
    7.24 +  fixes n :: nat
    7.25 +  shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
    7.26 +  apply (simp add: setsum.Sigma)
    7.27 +  apply (rule setsum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
    7.28 +  apply auto
    7.29 +  done
    7.30 +
    7.31 +lemma setsum_triangle_reindex_eq:
    7.32 +  fixes n :: nat
    7.33 +  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))"
    7.34 +using setsum_triangle_reindex [of f "Suc n"]
    7.35 +by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost)
    7.36 +
    7.37  subsection{* Shifting bounds *}
    7.38  
    7.39  lemma setsum_shift_bounds_nat_ivl:
     8.1 --- a/src/HOL/Topological_Spaces.thy	Tue Apr 28 16:23:05 2015 +0100
     8.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Apr 28 16:23:38 2015 +0100
     8.3 @@ -1479,14 +1479,6 @@
     8.4  lemma continuous_at_imp_continuous_on: "\<forall>x\<in>s. isCont f x \<Longrightarrow> continuous_on s f"
     8.5    by (auto intro: continuous_at_within simp: continuous_on_eq_continuous_within)
     8.6  
     8.7 -lemma isContI_continuous: "continuous (at x within UNIV) f \<Longrightarrow> isCont f x"
     8.8 -  by simp
     8.9 -
    8.10 -lemma isCont_ident[continuous_intros, simp]: "isCont (\<lambda>x. x) a"
    8.11 -  using continuous_ident by (rule isContI_continuous)
    8.12 -
    8.13 -lemmas isCont_const = continuous_const
    8.14 -
    8.15  lemma isCont_o2: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
    8.16    unfolding isCont_def by (rule tendsto_compose)
    8.17  
     9.1 --- a/src/HOL/Transcendental.thy	Tue Apr 28 16:23:05 2015 +0100
     9.2 +++ b/src/HOL/Transcendental.thy	Tue Apr 28 16:23:38 2015 +0100
     9.3 @@ -4781,6 +4781,11 @@
     9.4      using cos_gt_zero_pi [OF 1 2] by (simp add: arctan tan_add)
     9.5  qed
     9.6  
     9.7 +lemma arctan_double:
     9.8 +  assumes "\<bar>x\<bar> < 1"
     9.9 +  shows "2 * arctan x = arctan ((2*x) / (1 - x\<^sup>2))"
    9.10 +  by (metis assms arctan_add linear mult_2 not_less power2_eq_square)
    9.11 +
    9.12  theorem machin: "pi / 4 = 4 * arctan (1/5) - arctan (1 / 239)"
    9.13  proof -
    9.14    have "\<bar>1 / 5\<bar> < (1 :: real)" by auto
    9.15 @@ -4798,6 +4803,35 @@
    9.16    thus ?thesis unfolding arctan_one by algebra
    9.17  qed
    9.18  
    9.19 +lemma machin_Euler: "5 * arctan(1/7) + 2 * arctan(3/79) = pi/4"
    9.20 +proof -
    9.21 +  have 17: "\<bar>1/7\<bar> < (1 :: real)" by auto
    9.22 +  with arctan_double
    9.23 +  have "2 * arctan (1/7) = arctan (7/24)"  by auto
    9.24 +  moreover
    9.25 +  have "\<bar>7/24\<bar> < (1 :: real)" by auto
    9.26 +  with arctan_double
    9.27 +  have "2 * arctan (7/24) = arctan (336/527)"  by auto
    9.28 +  moreover
    9.29 +  have "\<bar>336/527\<bar> < (1 :: real)" by auto
    9.30 +  from arctan_add[OF less_imp_le[OF 17] this]
    9.31 +  have "arctan(1/7) + arctan (336/527) = arctan (2879/3353)"  by auto 
    9.32 +  ultimately have I: "5 * arctan(1/7) = arctan (2879/3353)"  by auto
    9.33 +  have 379: "\<bar>3/79\<bar> < (1 :: real)" by auto
    9.34 +  with arctan_double
    9.35 +  have II: "2 * arctan (3/79) = arctan (237/3116)"  by auto
    9.36 +  have *: "\<bar>2879/3353\<bar> < (1 :: real)" by auto
    9.37 +  have "\<bar>237/3116\<bar> < (1 :: real)" by auto
    9.38 +  from arctan_add[OF less_imp_le[OF *] this]
    9.39 +  have "arctan (2879/3353) + arctan (237/3116) = pi/4"
    9.40 +    by (simp add: arctan_one)
    9.41 +  then show ?thesis using I II
    9.42 +    by auto
    9.43 +qed
    9.44 +
    9.45 +(*But could also prove MACHIN_GAUSS:
    9.46 +  12 * arctan(1/18) + 8 * arctan(1/57) - 5 * arctan(1/239) = pi/4*)
    9.47 +
    9.48  
    9.49  subsection {* Introducing the inverse tangent power series *}
    9.50  
    9.51 @@ -5110,8 +5144,8 @@
    9.52        hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
    9.53        moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
    9.54          unfolding diff_conv_add_uminus divide_inverse
    9.55 -        by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan
    9.56 -          isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum
    9.57 +        by (auto intro!: isCont_add isCont_rabs continuous_ident isCont_minus isCont_arctan
    9.58 +          isCont_inverse isCont_mult isCont_power continuous_const isCont_setsum
    9.59            simp del: add_uminus_conv_diff)
    9.60        ultimately have "0 \<le> ?a 1 n - ?diff 1 n"
    9.61          by (rule LIM_less_bound)
    9.62 @@ -5282,8 +5316,57 @@
    9.63  qed
    9.64  
    9.65  
    9.66 -subsection{*Basics about polynomial functions: extremal behaviour and root counts*}
    9.67 -(*ALL COULD GO TO COMPLEX_MAIN OR EARLIER*)
    9.68 +subsection{*Basics about polynomial functions: products, extremal behaviour and root counts*}
    9.69 +
    9.70 +lemma pairs_le_eq_Sigma:
    9.71 +  fixes m::nat
    9.72 +  shows "{(i,j). i+j \<le> m} = Sigma (atMost m) (\<lambda>r. atMost (m-r))"
    9.73 +by auto
    9.74 +
    9.75 +lemma setsum_up_index_split:
    9.76 +    "(\<Sum>k\<le>m + n. f k) = (\<Sum>k\<le>m. f k) + (\<Sum>k = Suc m..m + n. f k)"
    9.77 +  by (metis atLeast0AtMost Suc_eq_plus1 le0 setsum_ub_add_nat)
    9.78 +
    9.79 +lemma Sigma_interval_disjoint:
    9.80 +  fixes w :: "'a::order"
    9.81 +  shows "(SIGMA i:A. {..v i}) \<inter> (SIGMA i:A.{v i<..w}) = {}"
    9.82 +    by auto
    9.83 +
    9.84 +lemma product_atMost_eq_Un:
    9.85 +  fixes m :: nat
    9.86 +  shows "A \<times> {..m} = (SIGMA i:A.{..m - i}) \<union> (SIGMA i:A.{m - i<..m})"
    9.87 +    by auto
    9.88 +
    9.89 +lemma polynomial_product: (*with thanks to Chaitanya Mangla*)
    9.90 +  fixes x:: "'a :: idom"
    9.91 +  assumes m: "\<And>i. i>m \<Longrightarrow> (a i) = 0" and n: "\<And>j. j>n \<Longrightarrow> (b j) = 0"
    9.92 +  shows "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) = 
    9.93 +         (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
    9.94 +proof -
    9.95 +  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))"
    9.96 +    by (rule setsum_product)
    9.97 +  also have "... = (\<Sum>i\<le>m + n. \<Sum>j\<le>n + m. a i * x ^ i * (b j * x ^ j))"
    9.98 +    using assms by (auto simp: setsum_up_index_split)
    9.99 +  also have "... = (\<Sum>r\<le>m + n. \<Sum>j\<le>m + n - r. a r * x ^ r * (b j * x ^ j))"
   9.100 +    apply (simp add: add_ac setsum.Sigma product_atMost_eq_Un)
   9.101 +    apply (clarsimp simp add: setsum_Un Sigma_interval_disjoint intro!: setsum.neutral)
   9.102 +    by (metis add_diff_assoc2 add.commute add_lessD1 leD m n nat_le_linear neqE)
   9.103 +  also have "... = (\<Sum>(i,j)\<in>{(i,j). i+j \<le> m+n}. (a i * x ^ i) * (b j * x ^ j))"
   9.104 +    by (auto simp: pairs_le_eq_Sigma setsum.Sigma)
   9.105 +  also have "... = (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
   9.106 +    apply (subst setsum_triangle_reindex_eq)  
   9.107 +    apply (auto simp: algebra_simps setsum_right_distrib intro!: setsum.cong)
   9.108 +    by (metis le_add_diff_inverse power_add)
   9.109 +  finally show ?thesis .
   9.110 +qed
   9.111 +
   9.112 +lemma polynomial_product_nat: 
   9.113 +  fixes x:: nat
   9.114 +  assumes m: "\<And>i. i>m \<Longrightarrow> (a i) = 0" and n: "\<And>j. j>n \<Longrightarrow> (b j) = 0"
   9.115 +  shows "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) = 
   9.116 +         (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
   9.117 +  using polynomial_product [of m a n b x] assms
   9.118 +  by (simp add: Int.zpower_int Int.zmult_int Int.int_setsum [symmetric])
   9.119  
   9.120  lemma polyfun_diff: (*COMPLEX_SUB_POLYFUN in HOL Light*)
   9.121      fixes x :: "'a::idom"
   9.122 @@ -5357,6 +5440,9 @@
   9.123    using polyfun_linear_factor [of c n a] assms
   9.124    by auto
   9.125  
   9.126 +(*The material of this section, up until this point, could go into a new theory of polynomials
   9.127 +  based on Main alone. The remaining material involves limits, continuity, series, etc.*)
   9.128 +
   9.129  lemma isCont_polynom:
   9.130    fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
   9.131    shows "isCont (\<lambda>w. \<Sum>i\<le>n. c i * w^i) a"