src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 64267 b9a1486e79be
parent 63941 f353674c2528
child 64394 141e1ed8d5a0
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Oct 16 22:43:51 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Oct 17 11:46:22 2016 +0200
     1.3 @@ -269,7 +269,7 @@
     1.4    fixes l::complex
     1.5    shows "f sums l \<Longrightarrow> (\<And>n. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
     1.6  unfolding sums_def
     1.7 -by (metis real_lim_sequentially setsum_in_Reals)
     1.8 +by (metis real_lim_sequentially sum_in_Reals)
     1.9  
    1.10  lemma Lim_null_comparison_Re:
    1.11    assumes "eventually (\<lambda>x. norm(f x) \<le> Re(g x)) F" "(g \<longlongrightarrow> 0) F" shows "(f \<longlongrightarrow> 0) F"
    1.12 @@ -335,7 +335,7 @@
    1.13       "op + c field_differentiable F"
    1.14    by (simp add: field_differentiable_add)
    1.15  
    1.16 -lemma field_differentiable_setsum [derivative_intros]:
    1.17 +lemma field_differentiable_sum [derivative_intros]:
    1.18    "(\<And>i. i \<in> I \<Longrightarrow> (f i) field_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) field_differentiable F"
    1.19    by (induct I rule: infinite_finite_induct)
    1.20       (auto intro: field_differentiable_add field_differentiable_const)
    1.21 @@ -502,9 +502,9 @@
    1.22    "f holomorphic_on s \<Longrightarrow> (\<lambda>z. (f z)^n) holomorphic_on s"
    1.23    unfolding holomorphic_on_def by (metis field_differentiable_power)
    1.24  
    1.25 -lemma holomorphic_on_setsum [holomorphic_intros]:
    1.26 -  "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) holomorphic_on s"
    1.27 -  unfolding holomorphic_on_def by (metis field_differentiable_setsum)
    1.28 +lemma holomorphic_on_sum [holomorphic_intros]:
    1.29 +  "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) holomorphic_on s"
    1.30 +  unfolding holomorphic_on_def by (metis field_differentiable_sum)
    1.31  
    1.32  lemma DERIV_deriv_iff_field_differentiable:
    1.33    "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
    1.34 @@ -788,8 +788,8 @@
    1.35    "f analytic_on s \<Longrightarrow> (\<lambda>z. (f z) ^ n) analytic_on s"
    1.36  by (induct n) (auto simp: analytic_on_const analytic_on_mult)
    1.37  
    1.38 -lemma analytic_on_setsum:
    1.39 -  "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on s) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) analytic_on s"
    1.40 +lemma analytic_on_sum:
    1.41 +  "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on s) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) analytic_on s"
    1.42    by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_const analytic_on_add)
    1.43  
    1.44  lemma deriv_left_inverse:
    1.45 @@ -951,7 +951,7 @@
    1.46        then have "cmod h * cmod ((\<Sum>i<n. f' i y) - g' y) \<le> cmod h * e"
    1.47          by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2)
    1.48        then show "cmod ((\<Sum>i<n. h * f' i y) - g' y * h) \<le> e * cmod h"
    1.49 -        by (simp add: norm_mult [symmetric] field_simps setsum_distrib_left)
    1.50 +        by (simp add: norm_mult [symmetric] field_simps sum_distrib_left)
    1.51      qed
    1.52    } note ** = this
    1.53    show ?thesis
    1.54 @@ -1064,9 +1064,9 @@
    1.55  
    1.56  subsection \<open>Taylor on Complex Numbers\<close>
    1.57  
    1.58 -lemma setsum_Suc_reindex:
    1.59 +lemma sum_Suc_reindex:
    1.60    fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
    1.61 -    shows  "setsum f {0..n} = f 0 - f (Suc n) + setsum (\<lambda>i. f (Suc i)) {0..n}"
    1.62 +    shows  "sum f {0..n} = f 0 - f (Suc n) + sum (\<lambda>i. f (Suc i)) {0..n}"
    1.63  by (induct n) auto
    1.64  
    1.65  lemma complex_taylor:
    1.66 @@ -1146,7 +1146,7 @@
    1.67    have "(\<Sum>i\<le>n. f i z * (z - z) ^ i / (fact i)) = (\<Sum>i\<le>n. (f i z / (fact i)) * 0 ^ i)"
    1.68      by simp
    1.69    also have "\<dots> = f 0 z / (fact 0)"
    1.70 -    by (subst setsum_zero_power) simp
    1.71 +    by (subst sum_zero_power) simp
    1.72    finally have "cmod (f 0 z - (\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i)))
    1.73                  \<le> cmod ((\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i)) -
    1.74                          (\<Sum>i\<le>n. f i z * (z - z) ^ i / (fact i)))"
    1.75 @@ -1203,7 +1203,7 @@
    1.76               (\<Sum>i = 0..n.
    1.77                   (f (Suc (Suc i)) u * ((z-u) ^ Suc i) - of_nat (Suc i) * (f (Suc i) u * (z-u) ^ i)) /
    1.78                   (fact (Suc i)))"
    1.79 -       by (subst setsum_Suc_reindex) simp
    1.80 +       by (subst sum_Suc_reindex) simp
    1.81      also have "... = f (Suc 0) u -
    1.82               (f (Suc (Suc n)) u * ((z-u) ^ Suc n) - (of_nat (Suc n)) * (z-u) ^ n * f (Suc n) u) /
    1.83               (fact (Suc n)) +
    1.84 @@ -1215,7 +1215,7 @@
    1.85               (f (Suc (Suc n)) u * (z-u) ^ Suc n - of_nat (Suc n) * (z-u) ^ n * f (Suc n) u) /
    1.86               (fact (Suc n)) +
    1.87               f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n)) - f (Suc 0) u"
    1.88 -      by (subst setsum_Suc_diff) auto
    1.89 +      by (subst sum_Suc_diff) auto
    1.90      also have "... = f (Suc n) u * (z-u) ^ n / (fact n)"
    1.91        by (simp only: algebra_simps diff_divide_distrib fact_cancel)
    1.92      finally have "(\<Sum>i = 0..n. (f (Suc i) u * (z - u) ^ i