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.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.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
```