author paulson Tue Apr 28 16:23:38 2015 +0100 (2015-04-28) changeset 60150 bd773c47ad0b parent 60149 9b0825a00b1a child 60151 9023d59acce6
New material about complex transcendental functions (especially Ln, Arg) and polynomials
```     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.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.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.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.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.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.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.101 +    apply (clarsimp simp add: setsum_Un Sigma_interval_disjoint intro!: setsum.neutral)
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.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"
```