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 (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
--- 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"
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*}
--- 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
--- 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 @@
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:
--- 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 @@
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"