author paulson Tue, 28 Apr 2015 16:23:38 +0100 changeset 60150 bd773c47ad0b parent 60149 9b0825a00b1a child 60151 9023d59acce6
New material about complex transcendental functions (especially Ln, Arg) and polynomials
```--- 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 (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```
```--- 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 -```
```--- 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"

@@ -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"
+
+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
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)"

+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 (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)"
+
+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"
+  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)"
+  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*}
```
```--- 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 (rule_tac x="s" in exI)
apply auto```
```--- 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"```
```--- 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"```
```--- 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 @@
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 (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:```
```--- 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)
```
```--- 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 @@
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"
+  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"
-        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
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 (clarsimp simp add: setsum_Un Sigma_interval_disjoint intro!: setsum.neutral)
+  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)
+  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"```