moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
authorhoelzl
Wed Apr 02 18:35:01 2014 +0200 (2014-04-02)
changeset 563692704ca85be98
parent 56368 0646f63a02b7
child 56370 7c717ba55a0b
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
NEWS
src/HOL/Complex.thy
src/HOL/Deriv.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Series.thy
     1.1 --- a/NEWS	Wed Apr 02 17:47:56 2014 +0200
     1.2 +++ b/NEWS	Wed Apr 02 18:35:01 2014 +0200
     1.3 @@ -563,6 +563,11 @@
     1.4      explicit set-comprehensions with eucl_less for other (half-) open
     1.5      intervals.
     1.6  
     1.7 +  - renamed theorems:
     1.8 +    derivative_linear         ~>  has_derivative_bounded_linear
     1.9 +    derivative_is_linear      ~>  has_derivative_linear
    1.10 +    bounded_linear_imp_linear ~>  bounded_linear.linear
    1.11 +
    1.12  
    1.13  *** Scala ***
    1.14  
     2.1 --- a/src/HOL/Complex.thy	Wed Apr 02 17:47:56 2014 +0200
     2.2 +++ b/src/HOL/Complex.thy	Wed Apr 02 18:35:01 2014 +0200
     2.3 @@ -339,6 +339,21 @@
     2.4  lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x"
     2.5    by (cases x) simp
     2.6  
     2.7 +
     2.8 +lemma abs_sqrt_wlog:
     2.9 +  fixes x::"'a::linordered_idom"
    2.10 +  assumes "\<And>x::'a. x \<ge> 0 \<Longrightarrow> P x (x\<^sup>2)" shows "P \<bar>x\<bar> (x\<^sup>2)"
    2.11 +by (metis abs_ge_zero assms power2_abs)
    2.12 +
    2.13 +lemma complex_abs_le_norm: "\<bar>Re z\<bar> + \<bar>Im z\<bar> \<le> sqrt 2 * norm z"
    2.14 +  unfolding complex_norm_def
    2.15 +  apply (rule abs_sqrt_wlog [where x="Re z"])
    2.16 +  apply (rule abs_sqrt_wlog [where x="Im z"])
    2.17 +  apply (rule power2_le_imp_le)
    2.18 +  apply (simp_all add: power2_sum add_commute sum_squares_bound real_sqrt_mult [symmetric])
    2.19 +  done
    2.20 +
    2.21 +
    2.22  text {* Properties of complex signum. *}
    2.23  
    2.24  lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
    2.25 @@ -370,6 +385,20 @@
    2.26  lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re]
    2.27  lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im]
    2.28  
    2.29 +lemma continuous_Re: "continuous_on X Re"
    2.30 +  by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Re 
    2.31 +            continuous_on_cong continuous_on_id)
    2.32 +
    2.33 +lemma continuous_Im: "continuous_on X Im"
    2.34 +  by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Im 
    2.35 +            continuous_on_cong continuous_on_id)
    2.36 +
    2.37 +lemma has_derivative_Re [has_derivative_intros] : "(Re has_derivative Re) F"
    2.38 +  by (auto simp add: has_derivative_def bounded_linear_Re tendsto_const)
    2.39 +
    2.40 +lemma has_derivative_Im [has_derivative_intros] : "(Im has_derivative Im) F"
    2.41 +  by (auto simp add: has_derivative_def bounded_linear_Im tendsto_const)
    2.42 +
    2.43  lemma tendsto_Complex [tendsto_intros]:
    2.44    assumes "(f ---> a) F" and "(g ---> b) F"
    2.45    shows "((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) F"
    2.46 @@ -387,6 +416,20 @@
    2.47         (simp add: dist_norm real_sqrt_sum_squares_less)
    2.48  qed
    2.49  
    2.50 +
    2.51 +lemma tendsto_complex_iff:
    2.52 +  "(f ---> x) F \<longleftrightarrow> (((\<lambda>x. Re (f x)) ---> Re x) F \<and> ((\<lambda>x. Im (f x)) ---> Im x) F)"
    2.53 +proof -
    2.54 +  have f: "f = (\<lambda>x. Complex (Re (f x)) (Im (f x)))" and x: "x = Complex (Re x) (Im x)"
    2.55 +    by simp_all
    2.56 +  show ?thesis
    2.57 +    apply (subst f)
    2.58 +    apply (subst x)
    2.59 +    apply (intro iffI tendsto_Complex conjI)
    2.60 +    apply (simp_all add: tendsto_Re tendsto_Im)
    2.61 +    done
    2.62 +qed
    2.63 +
    2.64  instance complex :: banach
    2.65  proof
    2.66    fix X :: "nat \<Rightarrow> complex"
    2.67 @@ -489,6 +532,9 @@
    2.68  lemma complex_cnj_add: "cnj (x + y) = cnj x + cnj y"
    2.69    by (simp add: complex_eq_iff)
    2.70  
    2.71 +lemma cnj_setsum: "cnj (setsum f s) = (\<Sum>x\<in>s. cnj (f x))"
    2.72 +  by (induct s rule: infinite_finite_induct) (auto simp: complex_cnj_add)
    2.73 +
    2.74  lemma complex_cnj_diff: "cnj (x - y) = cnj x - cnj y"
    2.75    by (simp add: complex_eq_iff)
    2.76  
    2.77 @@ -501,6 +547,9 @@
    2.78  lemma complex_cnj_mult: "cnj (x * y) = cnj x * cnj y"
    2.79    by (simp add: complex_eq_iff)
    2.80  
    2.81 +lemma cnj_setprod: "cnj (setprod f s) = (\<Prod>x\<in>s. cnj (f x))"
    2.82 +  by (induct s rule: infinite_finite_induct) (auto simp: complex_cnj_mult)
    2.83 +
    2.84  lemma complex_cnj_inverse: "cnj (inverse x) = inverse (cnj x)"
    2.85    by (simp add: complex_inverse_def)
    2.86  
    2.87 @@ -562,6 +611,12 @@
    2.88  lemmas isCont_cnj [simp] =
    2.89    bounded_linear.isCont [OF bounded_linear_cnj]
    2.90  
    2.91 +lemma lim_cnj: "((\<lambda>x. cnj(f x)) ---> cnj l) F \<longleftrightarrow> (f ---> l) F"
    2.92 +  by (simp add: tendsto_iff dist_complex_def Complex.complex_cnj_diff [symmetric])
    2.93 +
    2.94 +lemma sums_cnj: "((\<lambda>x. cnj(f x)) sums cnj l) \<longleftrightarrow> (f sums l)"
    2.95 +  by (simp add: sums_def lim_cnj cnj_setsum [symmetric])
    2.96 +
    2.97  
    2.98  subsection{*Basic Lemmas*}
    2.99  
   2.100 @@ -641,31 +696,43 @@
   2.101    by (metis im_complex_div_gt_0 not_le)
   2.102  
   2.103  lemma Re_setsum: "Re(setsum f s) = setsum (%x. Re(f x)) s"
   2.104 -apply (cases "finite s")
   2.105 -  by (induct s rule: finite_induct) auto
   2.106 +  by (induct s rule: infinite_finite_induct) auto
   2.107  
   2.108  lemma Im_setsum: "Im(setsum f s) = setsum (%x. Im(f x)) s"
   2.109 -apply (cases "finite s")
   2.110 -  by (induct s rule: finite_induct) auto
   2.111 +  by (induct s rule: infinite_finite_induct) auto
   2.112 +
   2.113 +lemma sums_complex_iff: "f sums x \<longleftrightarrow> ((\<lambda>x. Re (f x)) sums Re x) \<and> ((\<lambda>x. Im (f x)) sums Im x)"
   2.114 +  unfolding sums_def tendsto_complex_iff Im_setsum Re_setsum ..
   2.115 +  
   2.116 +lemma sums_Re: "f sums a \<Longrightarrow> (\<lambda>x. Re (f x)) sums Re a"
   2.117 +  unfolding sums_complex_iff by blast
   2.118 +
   2.119 +lemma sums_Im: "f sums a \<Longrightarrow> (\<lambda>x. Im (f x)) sums Im a"
   2.120 +  unfolding sums_complex_iff by blast
   2.121 +
   2.122 +lemma summable_complex_iff: "summable f \<longleftrightarrow> summable (\<lambda>x. Re (f x)) \<and>  summable (\<lambda>x. Im (f x))"
   2.123 +  unfolding summable_def sums_complex_iff[abs_def] by (metis Im.simps Re.simps)
   2.124 +
   2.125 +lemma summable_complex_of_real [simp]: "summable (\<lambda>n. complex_of_real (f n)) \<longleftrightarrow> summable f"
   2.126 +  unfolding summable_complex_iff by simp
   2.127 +
   2.128 +lemma summable_Re: "summable f \<Longrightarrow> summable (\<lambda>x. Re (f x))"
   2.129 +  unfolding summable_complex_iff by blast
   2.130 +
   2.131 +lemma summable_Im: "summable f \<Longrightarrow> summable (\<lambda>x. Im (f x))"
   2.132 +  unfolding summable_complex_iff by blast
   2.133  
   2.134  lemma Complex_setsum': "setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0"
   2.135 -apply (cases "finite s")
   2.136 -  by (induct s rule: finite_induct) auto
   2.137 +  by (induct s rule: infinite_finite_induct) auto
   2.138  
   2.139  lemma Complex_setsum: "Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s"
   2.140    by (metis Complex_setsum')
   2.141  
   2.142 -lemma cnj_setsum: "cnj (setsum f s) = setsum (%x. cnj (f x)) s"
   2.143 -apply (cases "finite s")
   2.144 -  by (induct s rule: finite_induct) (auto simp: complex_cnj_add)
   2.145 -
   2.146  lemma of_real_setsum: "of_real (setsum f s) = setsum (%x. of_real(f x)) s"
   2.147 -apply (cases "finite s")
   2.148 -  by (induct s rule: finite_induct) auto
   2.149 +  by (induct s rule: infinite_finite_induct) auto
   2.150  
   2.151  lemma of_real_setprod: "of_real (setprod f s) = setprod (%x. of_real(f x)) s"
   2.152 -apply (cases "finite s")
   2.153 -  by (induct s rule: finite_induct) auto
   2.154 +  by (induct s rule: infinite_finite_induct) auto
   2.155  
   2.156  lemma Reals_cnj_iff: "z \<in> \<real> \<longleftrightarrow> cnj z = z"
   2.157  by (metis Reals_cases Reals_of_real complex.exhaust complex.inject complex_cnj 
   2.158 @@ -677,6 +744,27 @@
   2.159  lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm(z) = abs(Re z)"
   2.160    by (metis Re_complex_of_real Reals_cases norm_of_real)
   2.161  
   2.162 +lemma complex_is_Real_iff: "z \<in> \<real> \<longleftrightarrow> Im z = 0"
   2.163 +  by (metis Complex_in_Reals Im_complex_of_real Reals_cases complex_surj)
   2.164 +
   2.165 +lemma series_comparison_complex:
   2.166 +  fixes f:: "nat \<Rightarrow> 'a::banach"
   2.167 +  assumes sg: "summable g"
   2.168 +     and "\<And>n. g n \<in> \<real>" "\<And>n. Re (g n) \<ge> 0"
   2.169 +     and fg: "\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> norm(g n)"
   2.170 +  shows "summable f"
   2.171 +proof -
   2.172 +  have g: "\<And>n. cmod (g n) = Re (g n)" using assms
   2.173 +    by (metis abs_of_nonneg in_Reals_norm)
   2.174 +  show ?thesis
   2.175 +    apply (rule summable_comparison_test' [where g = "\<lambda>n. norm (g n)" and N=N])
   2.176 +    using sg
   2.177 +    apply (auto simp: summable_def)
   2.178 +    apply (rule_tac x="Re s" in exI)
   2.179 +    apply (auto simp: g sums_Re)
   2.180 +    apply (metis fg g)
   2.181 +    done
   2.182 +qed
   2.183  
   2.184  subsection{*Finally! Polar Form for Complex Numbers*}
   2.185  
   2.186 @@ -888,4 +976,5 @@
   2.187  lemmas complex_Re_Im_cancel_iff = complex_eq_iff
   2.188  lemmas complex_equality = complex_eqI
   2.189  
   2.190 +
   2.191  end
     3.1 --- a/src/HOL/Deriv.thy	Wed Apr 02 17:47:56 2014 +0200
     3.2 +++ b/src/HOL/Deriv.thy	Wed Apr 02 18:35:01 2014 +0200
     3.3 @@ -61,6 +61,9 @@
     3.4  lemma has_derivative_bounded_linear: "(f has_derivative f') F \<Longrightarrow> bounded_linear f'"
     3.5    by (simp add: has_derivative_def)
     3.6  
     3.7 +lemma has_derivative_linear: "(f has_derivative f') F \<Longrightarrow> linear f'"
     3.8 +  using bounded_linear.linear[OF has_derivative_bounded_linear] .
     3.9 +
    3.10  lemma has_derivative_ident[has_derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
    3.11    by (simp add: has_derivative_def tendsto_const)
    3.12  
     4.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Apr 02 17:47:56 2014 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Apr 02 18:35:01 2014 +0200
     4.3 @@ -10,46 +10,10 @@
     4.4  
     4.5  subsection {*Complex number lemmas *}
     4.6  
     4.7 -lemma abs_sqrt_wlog:
     4.8 -  fixes x::"'a::linordered_idom"
     4.9 -  assumes "!!x::'a. x\<ge>0 \<Longrightarrow> P x (x\<^sup>2)" shows "P \<bar>x\<bar> (x\<^sup>2)"
    4.10 -by (metis abs_ge_zero assms power2_abs)
    4.11 -
    4.12 -lemma complex_abs_le_norm: "abs(Re z) + abs(Im z) \<le> sqrt(2) * norm z"
    4.13 -proof (cases z)
    4.14 -  case (Complex x y)
    4.15 -  show ?thesis
    4.16 -    apply (rule power2_le_imp_le)
    4.17 -    apply (auto simp: real_sqrt_mult [symmetric] Complex)
    4.18 -    apply (rule abs_sqrt_wlog [where x=x])
    4.19 -    apply (rule abs_sqrt_wlog [where x=y])
    4.20 -    apply (simp add: power2_sum add_commute sum_squares_bound)
    4.21 -    done
    4.22 -qed
    4.23 -
    4.24 -lemma continuous_Re: "continuous_on X Re"
    4.25 -  by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Re 
    4.26 -            continuous_on_cong continuous_on_id)
    4.27 -
    4.28 -lemma continuous_Im: "continuous_on X Im"
    4.29 -  by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Im 
    4.30 -            continuous_on_cong continuous_on_id)
    4.31 -
    4.32 -lemma open_closed_segment: "u \<in> open_segment w z \<Longrightarrow> u \<in> closed_segment w z"
    4.33 -  by (auto simp add: closed_segment_def open_segment_def)
    4.34 -
    4.35 -lemma has_derivative_Re [has_derivative_intros] : "(Re has_derivative Re) F"
    4.36 -  by (auto simp add: has_derivative_def bounded_linear_Re)
    4.37 -
    4.38 -lemma has_derivative_Im [has_derivative_intros] : "(Im has_derivative Im) F"
    4.39 -  by (auto simp add: has_derivative_def bounded_linear_Im)
    4.40 -
    4.41  lemma fact_cancel:
    4.42    fixes c :: "'a::real_field"
    4.43    shows "of_nat (Suc n) * c / of_nat (fact (Suc n)) = c / of_nat (fact n)"
    4.44 -  apply (subst frac_eq_eq [OF of_nat_fact_not_zero of_nat_fact_not_zero])
    4.45 -  apply (simp add: algebra_simps of_nat_mult)
    4.46 -  done
    4.47 +  by (simp add: of_nat_mult del: of_nat_Suc times_nat.simps)
    4.48  
    4.49  lemma
    4.50    shows open_halfspace_Re_lt: "open {z. Re(z) < b}"
    4.51 @@ -65,9 +29,6 @@
    4.52    by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re
    4.53              isCont_Im isCont_ident isCont_const)+
    4.54  
    4.55 -lemma complex_is_Real_iff: "z \<in> \<real> \<longleftrightarrow> Im z = 0"
    4.56 -  by (metis Complex_in_Reals Im_complex_of_real Reals_cases complex_surj)
    4.57 -
    4.58  lemma closed_complex_Reals: "closed (Reals :: complex set)"
    4.59  proof -
    4.60    have "(Reals :: complex set) = {z. Im z = 0}"
    4.61 @@ -78,16 +39,15 @@
    4.62  
    4.63  
    4.64  lemma linear_times:
    4.65 -  fixes c::"'a::{real_algebra,real_vector}" shows "linear (\<lambda>x. c * x)"
    4.66 +  fixes c::"'a::real_algebra" shows "linear (\<lambda>x. c * x)"
    4.67    by (auto simp: linearI distrib_left)
    4.68  
    4.69  lemma bilinear_times:
    4.70 -  fixes c::"'a::{real_algebra,real_vector}" shows "bilinear (\<lambda>x y::'a. x*y)"
    4.71 -  unfolding bilinear_def
    4.72 -  by (auto simp: distrib_left distrib_right intro!: linearI)
    4.73 +  fixes c::"'a::real_algebra" shows "bilinear (\<lambda>x y::'a. x*y)"
    4.74 +  by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI)
    4.75  
    4.76  lemma linear_cnj: "linear cnj"
    4.77 -  by (auto simp: linearI cnj_def)
    4.78 +  using bounded_linear.linear[OF bounded_linear_cnj] .
    4.79  
    4.80  lemma tendsto_mult_left:
    4.81    fixes c::"'a::real_normed_algebra" 
    4.82 @@ -152,7 +112,7 @@
    4.83  lemma uniformly_continuous_on_cmul_right [continuous_on_intros]:
    4.84    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
    4.85    shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)"
    4.86 -  by (metis bounded_linear.uniformly_continuous_on[of "\<lambda>x. x * c"] bounded_linear_mult_left) 
    4.87 +  using bounded_linear.uniformly_continuous_on[OF bounded_linear_mult_left] . 
    4.88  
    4.89  lemma uniformly_continuous_on_cmul_left[continuous_on_intros]:
    4.90    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
    4.91 @@ -164,8 +124,7 @@
    4.92    by (rule continuous_norm [OF continuous_ident])
    4.93  
    4.94  lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm"
    4.95 -  by (metis continuous_on_eq continuous_on_id continuous_on_norm)
    4.96 -
    4.97 +  by (intro continuous_on_id continuous_on_norm)
    4.98  
    4.99  subsection{*DERIV stuff*}
   4.100  
   4.101 @@ -184,8 +143,7 @@
   4.102        and "\<forall>x\<in>(s - k). DERIV f x :> 0"
   4.103      obtains c where "\<And>x. x \<in> s \<Longrightarrow> f(x) = c"
   4.104  using has_derivative_zero_connected_constant [OF assms(1-4)] assms
   4.105 -by (metis DERIV_const Derivative.has_derivative_const Diff_iff at_within_open 
   4.106 -          frechet_derivative_at has_field_derivative_def)
   4.107 +by (metis DERIV_const has_derivative_const Diff_iff at_within_open frechet_derivative_at has_field_derivative_def)
   4.108  
   4.109  lemma DERIV_zero_constant:
   4.110    fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
   4.111 @@ -255,7 +213,7 @@
   4.112      obtains c where "(f has_derivative (\<lambda>x. x * c)) F"
   4.113  proof -
   4.114    obtain c where "f' = (\<lambda>x. x * c)"
   4.115 -    by (metis assms derivative_linear real_bounded_linear)
   4.116 +    by (metis assms has_derivative_bounded_linear real_bounded_linear)
   4.117    then show ?thesis
   4.118      by (metis assms that)
   4.119  qed
   4.120 @@ -336,15 +294,14 @@
   4.121  lemma complex_differentiable_const:
   4.122    "(\<lambda>z. c) complex_differentiable F"
   4.123    unfolding complex_differentiable_def has_field_derivative_def
   4.124 -  apply (rule exI [where x=0])
   4.125 -  by (metis Derivative.has_derivative_const lambda_zero) 
   4.126 +  by (rule exI [where x=0])
   4.127 +     (metis has_derivative_const lambda_zero) 
   4.128  
   4.129  lemma complex_differentiable_id:
   4.130    "(\<lambda>z. z) complex_differentiable F"
   4.131    unfolding complex_differentiable_def has_field_derivative_def
   4.132 -  apply (rule exI [where x=1])
   4.133 -  apply (simp add: lambda_one [symmetric])
   4.134 -  done
   4.135 +  by (rule exI [where x=1])
   4.136 +     (simp add: lambda_one [symmetric])
   4.137  
   4.138  lemma complex_differentiable_minus:
   4.139      "f complex_differentiable F \<Longrightarrow> (\<lambda>z. -(f z)) complex_differentiable F"
   4.140 @@ -484,10 +441,9 @@
   4.141    by (metis DERIV_power)
   4.142  
   4.143  lemma holomorphic_on_setsum:
   4.144 -  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s)
   4.145 -           \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) holomorphic_on s"
   4.146 +  "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) holomorphic_on s"
   4.147    unfolding holomorphic_on_def
   4.148 -  apply (induct I rule: finite_induct) 
   4.149 +  apply (induct I rule: infinite_finite_induct) 
   4.150    apply (force intro: DERIV_const DERIV_add)+
   4.151    done
   4.152  
   4.153 @@ -580,9 +536,6 @@
   4.154  
   4.155  subsection{*Caratheodory characterization.*}
   4.156  
   4.157 -(*REPLACE the original version. BUT IN WHICH FILE??*)
   4.158 -thm Deriv.CARAT_DERIV
   4.159 -
   4.160  lemma complex_differentiable_caratheodory_at:
   4.161    "f complex_differentiable (at z) \<longleftrightarrow>
   4.162           (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
   4.163 @@ -796,9 +749,8 @@
   4.164  by (induct n) (auto simp: analytic_on_const analytic_on_mult)
   4.165  
   4.166  lemma analytic_on_setsum:
   4.167 -  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on s)
   4.168 -           \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) analytic_on s"
   4.169 -  by (induct I rule: finite_induct) (auto simp: analytic_on_const analytic_on_add)
   4.170 +  "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on s) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) analytic_on s"
   4.171 +  by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_const analytic_on_add)
   4.172  
   4.173  subsection{*analyticity at a point.*}
   4.174  
   4.175 @@ -1025,12 +977,6 @@
   4.176  
   4.177  subsection{*Further useful properties of complex conjugation*}
   4.178  
   4.179 -lemma lim_cnj: "((\<lambda>x. cnj(f x)) ---> cnj l) F \<longleftrightarrow> (f ---> l) F"
   4.180 -  by (simp add: tendsto_iff dist_complex_def Complex.complex_cnj_diff [symmetric])
   4.181 -
   4.182 -lemma sums_cnj: "((\<lambda>x. cnj(f x)) sums cnj l) \<longleftrightarrow> (f sums l)"
   4.183 -  by (simp add: sums_def lim_cnj cnj_setsum [symmetric])
   4.184 -
   4.185  lemma continuous_within_cnj: "continuous (at z within s) cnj"
   4.186  by (metis bounded_linear_cnj linear_continuous_within)
   4.187  
   4.188 @@ -1043,12 +989,11 @@
   4.189    fixes l::complex
   4.190    assumes "(f ---> l) F" and "~(trivial_limit F)" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
   4.191    shows  "l \<in> \<real>"
   4.192 -proof (rule Lim_in_closed_set)
   4.193 -  show "closed (\<real>::complex set)"
   4.194 -    by (rule closed_complex_Reals)
   4.195 +proof (rule Lim_in_closed_set[OF closed_complex_Reals _ assms(2,1)])
   4.196    show "eventually (\<lambda>x. f x \<in> \<real>) F"
   4.197      using assms(3, 4) by (auto intro: eventually_mono)
   4.198 -qed fact+
   4.199 +qed
   4.200 +
   4.201  lemma real_lim_sequentially:
   4.202    fixes l::complex
   4.203    shows "(f ---> l) sequentially \<Longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
   4.204 @@ -1079,66 +1024,11 @@
   4.205  using assms unfolding summable_def
   4.206  by (blast intro: sums_vec_nth)
   4.207  
   4.208 -lemma sums_Re:
   4.209 -  assumes "f sums a"
   4.210 -  shows "(\<lambda>x. Re (f x)) sums Re a"
   4.211 -using assms 
   4.212 -by (auto simp: sums_def Re_setsum [symmetric] isCont_tendsto_compose [of a Re])
   4.213 -
   4.214 -lemma sums_Im:
   4.215 -  assumes "f sums a"
   4.216 -  shows "(\<lambda>x. Im (f x)) sums Im a"
   4.217 -using assms 
   4.218 -by (auto simp: sums_def Im_setsum [symmetric] isCont_tendsto_compose [of a Im])
   4.219 -
   4.220 -lemma summable_Re:
   4.221 -  assumes "summable f"
   4.222 -  shows "summable (\<lambda>x. Re (f x))"
   4.223 -using assms unfolding summable_def
   4.224 -by (blast intro: sums_Re)
   4.225 -
   4.226 -lemma summable_Im:
   4.227 -  assumes "summable f"
   4.228 -  shows "summable (\<lambda>x. Im (f x))"
   4.229 -using assms unfolding summable_def
   4.230 -by (blast intro: sums_Im)
   4.231 -
   4.232 -lemma series_comparison_complex:
   4.233 -  fixes f:: "nat \<Rightarrow> 'a::banach"
   4.234 -  assumes sg: "summable g"
   4.235 -     and "\<And>n. g n \<in> \<real>" "\<And>n. Re (g n) \<ge> 0"
   4.236 -     and fg: "\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> norm(g n)"
   4.237 -  shows "summable f"
   4.238 -proof -
   4.239 -  have g: "\<And>n. cmod (g n) = Re (g n)" using assms
   4.240 -    by (metis abs_of_nonneg in_Reals_norm)
   4.241 -  show ?thesis
   4.242 -    apply (rule summable_comparison_test' [where g = "\<lambda>n. norm (g n)" and N=N])
   4.243 -    using sg
   4.244 -    apply (auto simp: summable_def)
   4.245 -    apply (rule_tac x="Re s" in exI)
   4.246 -    apply (auto simp: g sums_Re)
   4.247 -    apply (metis fg g)
   4.248 -    done
   4.249 -qed
   4.250 -
   4.251 -lemma summable_complex_of_real [simp]:
   4.252 -  "summable (\<lambda>n. complex_of_real (f n)) = summable f"
   4.253 -apply (auto simp: Series.summable_Cauchy)  
   4.254 -apply (drule_tac x = e in spec, auto)
   4.255 -apply (rule_tac x=N in exI)
   4.256 -apply (auto simp: of_real_setsum [symmetric])
   4.257 -done
   4.258 -
   4.259 -
   4.260 -
   4.261 -
   4.262  lemma setsum_Suc_reindex:
   4.263    fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
   4.264      shows  "setsum f {0..n} = f 0 - f (Suc n) + setsum (\<lambda>i. f (Suc i)) {0..n}"
   4.265  by (induct n) auto
   4.266  
   4.267 -
   4.268  text{*A kind of complex Taylor theorem.*}
   4.269  lemma complex_taylor:
   4.270    assumes s: "convex s" 
   4.271 @@ -1238,22 +1128,22 @@
   4.272  
   4.273  text{* Something more like the traditional MVT for real components.*}
   4.274  lemma complex_mvt_line:
   4.275 -  assumes "\<And>u. u \<in> closed_segment w z ==> (f has_field_derivative f'(u)) (at u)"
   4.276 +  assumes "\<And>u. u \<in> closed_segment w z \<Longrightarrow> (f has_field_derivative f'(u)) (at u)"
   4.277      shows "\<exists>u. u \<in> open_segment w z \<and> Re(f z) - Re(f w) = Re(f'(u) * (z - w))"
   4.278  proof -
   4.279    have twz: "\<And>t. (1 - t) *\<^sub>R w + t *\<^sub>R z = w + t *\<^sub>R (z - w)"
   4.280      by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
   4.281 +  note assms[unfolded has_field_derivative_def, has_derivative_intros]
   4.282    show ?thesis
   4.283      apply (cut_tac mvt_simple
   4.284                       [of 0 1 "Re o f o (\<lambda>t. (1 - t) *\<^sub>R w +  t *\<^sub>R z)"
   4.285                        "\<lambda>u. Re o (\<lambda>h. f'((1 - u) *\<^sub>R w + u *\<^sub>R z) * h) o (\<lambda>t. t *\<^sub>R (z - w))"])
   4.286      apply auto
   4.287      apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI)
   4.288 -    apply (simp add: open_segment_def)
   4.289 -    apply (auto simp add: twz)
   4.290 -    apply (rule has_derivative_at_within)
   4.291 -    apply (intro has_derivative_intros has_derivative_add [OF has_derivative_const, simplified])+
   4.292 -    apply (rule assms [unfolded has_field_derivative_def])
   4.293 +    apply (auto simp add: open_segment_def twz) []
   4.294 +    apply (intro has_derivative_eq_intros has_derivative_at_within)
   4.295 +    apply simp_all
   4.296 +    apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib)
   4.297      apply (force simp add: twz closed_segment_def)
   4.298      done
   4.299  qed
   4.300 @@ -1309,24 +1199,4 @@
   4.301      done
   4.302  qed
   4.303  
   4.304 -text{*Relations among convergence and absolute convergence for power series.*}
   4.305 -lemma abel_lemma:
   4.306 -  fixes a :: "nat \<Rightarrow> 'a::real_normed_vector"
   4.307 -  assumes r: "0 \<le> r" and r0: "r < r0" and M: "\<And>n. norm(a n) * r0^n \<le> M"
   4.308 -    shows "summable (\<lambda>n. norm(a(n)) * r^n)"
   4.309 -proof (rule summable_comparison_test' [of "\<lambda>n. M * (r / r0)^n"])
   4.310 -  show "summable (\<lambda>n. M * (r / r0) ^ n)"
   4.311 -    using assms 
   4.312 -    by (auto simp add: summable_mult summable_geometric)
   4.313 -  next
   4.314 -    fix n
   4.315 -    show "norm (norm (a n) * r ^ n) \<le> M * (r / r0) ^ n"
   4.316 -      using r r0 M [of n]
   4.317 -      apply (auto simp add: abs_mult field_simps power_divide)
   4.318 -      apply (cases "r=0", simp)
   4.319 -      apply (cases n, auto)
   4.320 -      done
   4.321 -qed
   4.322 -
   4.323 -
   4.324  end
     5.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Apr 02 17:47:56 2014 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Apr 02 18:35:01 2014 +0200
     5.3 @@ -5875,14 +5875,6 @@
     5.4      by (induct set: finite, simp, simp add: convex_hull_set_plus)
     5.5  qed simp
     5.6  
     5.7 -lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
     5.8 -proof -
     5.9 -  assume "bounded_linear f"
    5.10 -  then interpret f: bounded_linear f .
    5.11 -  show "linear f"
    5.12 -    by (simp add: f.add f.scaleR linear_iff)
    5.13 -qed
    5.14 -
    5.15  lemma convex_hull_eq_real_cbox:
    5.16    fixes x y :: real assumes "x \<le> y"
    5.17    shows "convex hull {x, y} = cbox x y"
    5.18 @@ -6295,6 +6287,9 @@
    5.19  
    5.20  lemmas segment = open_segment_def closed_segment_def
    5.21  
    5.22 +lemma open_closed_segment: "u \<in> open_segment w z \<Longrightarrow> u \<in> closed_segment w z"
    5.23 +  by (auto simp add: closed_segment_def open_segment_def)
    5.24 +
    5.25  definition "starlike s \<longleftrightarrow> (\<exists>a\<in>s. \<forall>x\<in>s. closed_segment a x \<subseteq> s)"
    5.26  
    5.27  lemma midpoint_refl: "midpoint x x = x"
     6.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Apr 02 17:47:56 2014 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Apr 02 18:35:01 2014 +0200
     6.3 @@ -9,16 +9,6 @@
     6.4  imports Brouwer_Fixpoint Operator_Norm
     6.5  begin
     6.6  
     6.7 -lemma bounded_linear_imp_linear: (* TODO: move elsewhere *)
     6.8 -  assumes "bounded_linear f"
     6.9 -  shows "linear f"
    6.10 -proof -
    6.11 -  interpret f: bounded_linear f
    6.12 -    using assms .
    6.13 -  show ?thesis
    6.14 -    by (simp add: f.add f.scaleR linear_iff)
    6.15 -qed
    6.16 -
    6.17  lemma netlimit_at_vector: (* TODO: move *)
    6.18    fixes a :: "'a::real_normed_vector"
    6.19    shows "netlimit (at a) = a"
    6.20 @@ -37,22 +27,15 @@
    6.21  (* Because I do not want to type this all the time *)
    6.22  lemmas linear_linear = linear_conv_bounded_linear[symmetric]
    6.23  
    6.24 -lemma derivative_linear[dest]: "(f has_derivative f') net \<Longrightarrow> bounded_linear f'"
    6.25 -  unfolding has_derivative_def by auto
    6.26 -
    6.27 -lemma derivative_is_linear: "(f has_derivative f') net \<Longrightarrow> linear f'"
    6.28 -  by (rule derivative_linear [THEN bounded_linear_imp_linear])
    6.29 +declare has_derivative_bounded_linear[dest]
    6.30  
    6.31  subsection {* Derivatives *}
    6.32  
    6.33  subsubsection {* Combining theorems. *}
    6.34  
    6.35  lemmas has_derivative_id = has_derivative_ident
    6.36 -lemmas has_derivative_const = has_derivative_const
    6.37  lemmas has_derivative_neg = has_derivative_minus
    6.38 -lemmas has_derivative_add = has_derivative_add
    6.39  lemmas has_derivative_sub = has_derivative_diff
    6.40 -lemmas has_derivative_setsum = has_derivative_setsum
    6.41  lemmas scaleR_right_has_derivative = has_derivative_scaleR_right
    6.42  lemmas scaleR_left_has_derivative = has_derivative_scaleR_left
    6.43  lemmas inner_right_has_derivative = has_derivative_inner_right
    6.44 @@ -176,11 +159,6 @@
    6.45      by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
    6.46  qed
    6.47  
    6.48 -lemma CARAT_DERIV: (*FIXME: REPLACES THE ONE IN Deriv.thy*)
    6.49 -  "(DERIV f x :> l) \<longleftrightarrow> (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> g x = l)"
    6.50 -by (rule DERIV_caratheodory_within)
    6.51 -
    6.52 -
    6.53  subsubsection {* Limit transformation for derivatives *}
    6.54  
    6.55  lemma has_derivative_transform_within:
    6.56 @@ -275,7 +253,7 @@
    6.57  
    6.58  lemma linear_frechet_derivative: "f differentiable net \<Longrightarrow> linear (frechet_derivative f net)"
    6.59    unfolding frechet_derivative_works has_derivative_def
    6.60 -  by (auto intro: bounded_linear_imp_linear)
    6.61 +  by (auto intro: bounded_linear.linear)
    6.62  
    6.63  
    6.64  subsection {* Differentiability implies continuity *}
    6.65 @@ -322,14 +300,14 @@
    6.66      (\<forall>e>0. \<exists>d>0. \<forall>y\<in>s. norm(y - x) < d \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> e * norm (y - x))"
    6.67    unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
    6.68      eventually_at dist_norm diff_add_eq_diff_diff
    6.69 -  by (force simp add: linear_0 bounded_linear_imp_linear pos_divide_le_eq)
    6.70 +  by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq)
    6.71  
    6.72  lemma has_derivative_within_alt2:
    6.73    "(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and>
    6.74      (\<forall>e>0. eventually (\<lambda>y. norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)) (at x within s))"
    6.75    unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
    6.76      eventually_at dist_norm diff_add_eq_diff_diff
    6.77 -  by (force simp add: linear_0 bounded_linear_imp_linear pos_divide_le_eq)
    6.78 +  by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq)
    6.79  
    6.80  lemma has_derivative_at_alt:
    6.81    "(f has_derivative f') (at x) \<longleftrightarrow>
    6.82 @@ -372,6 +350,7 @@
    6.83  
    6.84  subsection {* Uniqueness of derivative *}
    6.85  
    6.86 +
    6.87  text {*
    6.88   The general result is a bit messy because we need approachability of the
    6.89   limit point from any direction. But OK for nontrivial intervals etc.
    6.90 @@ -854,7 +833,7 @@
    6.91    proof -
    6.92      case goal1
    6.93      have "norm (f' x y) \<le> onorm (f' x) * norm y"
    6.94 -      by (rule onorm[OF derivative_linear[OF assms(2)[rule_format,OF goal1]]])
    6.95 +      by (rule onorm[OF has_derivative_bounded_linear[OF assms(2)[rule_format,OF goal1]]])
    6.96      also have "\<dots> \<le> B * norm y"
    6.97        apply (rule mult_right_mono)
    6.98        using assms(3)[rule_format,OF goal1]
    6.99 @@ -881,7 +860,7 @@
   6.100  lemma has_derivative_zero_constant:
   6.101    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
   6.102    assumes "convex s"
   6.103 -    and "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)"
   6.104 +    and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)"
   6.105    shows "\<exists>c. \<forall>x\<in>s. f x = c"
   6.106  proof -
   6.107    { fix x y assume "x \<in> s" "y \<in> s"
   6.108 @@ -896,14 +875,34 @@
   6.109  lemma has_derivative_zero_unique:
   6.110    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
   6.111    assumes "convex s"
   6.112 -    and "a \<in> s"
   6.113 -    and "f a = c"
   6.114 -    and "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)"
   6.115 -    and "x \<in> s"
   6.116 -  shows "f x = c"
   6.117 -  using has_derivative_zero_constant[OF assms(1,4)]
   6.118 -  using assms(2-3,5)
   6.119 -  by auto
   6.120 +    and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)"
   6.121 +    and "x \<in> s" "y \<in> s"
   6.122 +  shows "f x = f y"
   6.123 +  using has_derivative_zero_constant[OF assms(1,2)] assms(3-) by force
   6.124 +
   6.125 +lemma has_derivative_zero_unique_connected:
   6.126 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
   6.127 +  assumes "open s" "connected s"
   6.128 +  assumes f: "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>x. 0)) (at x)"
   6.129 +  assumes "x \<in> s" "y \<in> s"
   6.130 +  shows "f x = f y"
   6.131 +proof (rule connected_local_const[where f=f, OF `connected s` `x\<in>s` `y\<in>s`])
   6.132 +  show "\<forall>a\<in>s. eventually (\<lambda>b. f a = f b) (at a within s)"
   6.133 +  proof
   6.134 +    fix a assume "a \<in> s"
   6.135 +    with `open s` obtain e where "0 < e" "ball a e \<subseteq> s"
   6.136 +      by (rule openE)
   6.137 +    then have "\<exists>c. \<forall>x\<in>ball a e. f x = c"
   6.138 +      by (intro has_derivative_zero_constant)
   6.139 +         (auto simp: at_within_open[OF _ open_ball] f convex_ball)
   6.140 +    with `0<e` have "\<forall>x\<in>ball a e. f a = f x"
   6.141 +      by auto
   6.142 +    then show "eventually (\<lambda>b. f a = f b) (at a within s)"
   6.143 +      using `0<e` unfolding eventually_at_topological
   6.144 +      by (intro exI[of _ "ball a e"]) auto
   6.145 +  qed
   6.146 +qed
   6.147 +
   6.148  
   6.149  
   6.150  subsection {* Differentiability of inverse function (most basic form) *}
   6.151 @@ -1546,11 +1545,11 @@
   6.152            apply (rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
   6.153            apply (rule has_derivative_at_within)
   6.154            using assms(5) and `u \<in> s` `a \<in> s`
   6.155 -          apply (auto intro!: has_derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] derivative_linear)
   6.156 +          apply (auto intro!: has_derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] has_derivative_bounded_linear)
   6.157            done
   6.158          have **: "bounded_linear (\<lambda>x. f' u x - f' a x)" "bounded_linear (\<lambda>x. f' a x - f' u x)"
   6.159            apply (rule_tac[!] bounded_linear_sub)
   6.160 -          apply (rule_tac[!] derivative_linear)
   6.161 +          apply (rule_tac[!] has_derivative_bounded_linear)
   6.162            using assms(5) `u \<in> s` `a \<in> s`
   6.163            apply auto
   6.164            done
   6.165 @@ -1773,18 +1772,18 @@
   6.166      proof
   6.167        fix x' y z :: 'a
   6.168        fix c :: real
   6.169 -      note lin = assms(2)[rule_format,OF `x\<in>s`,THEN derivative_linear]
   6.170 +      note lin = assms(2)[rule_format,OF `x\<in>s`,THEN has_derivative_bounded_linear]
   6.171        show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'"
   6.172          apply (rule tendsto_unique[OF trivial_limit_sequentially])
   6.173          apply (rule lem3[rule_format])
   6.174 -        unfolding lin[THEN bounded_linear_imp_linear, THEN linear_cmul]
   6.175 +        unfolding lin[THEN bounded_linear.linear, THEN linear_cmul]
   6.176          apply (intro tendsto_intros)
   6.177          apply (rule lem3[rule_format])
   6.178          done
   6.179        show "g' x (y + z) = g' x y + g' x z"
   6.180          apply (rule tendsto_unique[OF trivial_limit_sequentially])
   6.181          apply (rule lem3[rule_format])
   6.182 -        unfolding lin[THEN bounded_linear_imp_linear, THEN linear_add]
   6.183 +        unfolding lin[THEN bounded_linear.linear, THEN linear_add]
   6.184          apply (rule tendsto_add)
   6.185          apply (rule lem3[rule_format])+
   6.186          done
     7.1 --- a/src/HOL/Real_Vector_Spaces.thy	Wed Apr 02 17:47:56 2014 +0200
     7.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Apr 02 18:35:01 2014 +0200
     7.3 @@ -752,6 +752,12 @@
     7.4    shows "norm (setsum f A) \<le> (\<Sum>i\<in>A. norm (f i))"
     7.5    by (induct A rule: infinite_finite_induct) (auto intro: norm_triangle_mono)
     7.6  
     7.7 +lemma setsum_norm_le:
     7.8 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
     7.9 +  assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
    7.10 +  shows "norm (setsum f S) \<le> setsum g S"
    7.11 +  by (rule order_trans [OF norm_setsum setsum_mono]) (simp add: fg)
    7.12 +
    7.13  lemma abs_norm_cancel [simp]:
    7.14    fixes a :: "'a::real_normed_vector"
    7.15    shows "\<bar>norm a\<bar> = norm a"
    7.16 @@ -1158,6 +1164,8 @@
    7.17    show ?thesis by (auto intro: order_less_imp_le)
    7.18  qed
    7.19  
    7.20 +lemma linear: "linear f" ..
    7.21 +
    7.22  end
    7.23  
    7.24  lemma bounded_linear_intro:
     8.1 --- a/src/HOL/Series.thy	Wed Apr 02 17:47:56 2014 +0200
     8.2 +++ b/src/HOL/Series.thy	Wed Apr 02 18:35:01 2014 +0200
     8.3 @@ -463,7 +463,7 @@
     8.4  
     8.5  (*A better argument order*)
     8.6  lemma summable_comparison_test': "summable g \<Longrightarrow> (\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> g n) \<Longrightarrow> summable f"
     8.7 -by (rule summable_comparison_test) auto
     8.8 +  by (rule summable_comparison_test) auto
     8.9  
    8.10  subsection {* The Ratio Test*}
    8.11  
    8.12 @@ -502,6 +502,27 @@
    8.13  
    8.14  end
    8.15  
    8.16 +text{*Relations among convergence and absolute convergence for power series.*}
    8.17 +
    8.18 +lemma abel_lemma:
    8.19 +  fixes a :: "nat \<Rightarrow> 'a::real_normed_vector"
    8.20 +  assumes r: "0 \<le> r" and r0: "r < r0" and M: "\<And>n. norm (a n) * r0^n \<le> M"
    8.21 +    shows "summable (\<lambda>n. norm (a n) * r^n)"
    8.22 +proof (rule summable_comparison_test')
    8.23 +  show "summable (\<lambda>n. M * (r / r0) ^ n)"
    8.24 +    using assms 
    8.25 +    by (auto simp add: summable_mult summable_geometric)
    8.26 +next
    8.27 +  fix n
    8.28 +  show "norm (norm (a n) * r ^ n) \<le> M * (r / r0) ^ n"
    8.29 +    using r r0 M [of n]
    8.30 +    apply (auto simp add: abs_mult field_simps power_divide)
    8.31 +    apply (cases "r=0", simp)
    8.32 +    apply (cases n, auto)
    8.33 +    done
    8.34 +qed
    8.35 +
    8.36 +
    8.37  text{*Summability of geometric series for real algebras*}
    8.38  
    8.39  lemma complete_algebra_summable_geometric: