src/HOL/Analysis/Complex_Analysis_Basics.thy
 changeset 69529 4ab9657b3257 parent 69508 2a4c8a2a3f8e child 70136 f03a01a18c6e
```     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Dec 28 19:01:35 2018 +0100
1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat Dec 29 15:43:53 2018 +0100
1.3 @@ -972,7 +972,7 @@
1.4      shows  "sum f {0..n} = f 0 - f (Suc n) + sum (\<lambda>i. f (Suc i)) {0..n}"
1.5  by (induct n) auto
1.6
1.7 -lemma field_taylor:
1.8 +lemma field_Taylor:
1.9    assumes S: "convex S"
1.10        and f: "\<And>i x. x \<in> S \<Longrightarrow> i \<le> n \<Longrightarrow> (f i has_field_derivative f (Suc i) x) (at x within S)"
1.11        and B: "\<And>x. x \<in> S \<Longrightarrow> norm (f (Suc n) x) \<le> B"
1.12 @@ -1066,7 +1066,7 @@
1.13    finally show ?thesis .
1.14  qed
1.15
1.16 -lemma complex_taylor:
1.17 +lemma complex_Taylor:
1.18    assumes S: "convex S"
1.19        and f: "\<And>i x. x \<in> S \<Longrightarrow> i \<le> n \<Longrightarrow> (f i has_field_derivative f (Suc i) x) (at x within S)"
1.20        and B: "\<And>x. x \<in> S \<Longrightarrow> cmod (f (Suc n) x) \<le> B"
1.21 @@ -1074,7 +1074,7 @@
1.22        and z: "z \<in> S"
1.23      shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i)))
1.24            \<le> B * cmod(z - w)^(Suc n) / fact n"
1.25 -  using assms by (rule field_taylor)
1.26 +  using assms by (rule field_Taylor)
1.27
1.28
1.29  text\<open>Something more like the traditional MVT for real components\<close>
1.30 @@ -1099,7 +1099,7 @@
1.31      done
1.32  qed
1.33
1.34 -lemma complex_taylor_mvt:
1.35 +lemma complex_Taylor_mvt:
1.36    assumes "\<And>i x. \<lbrakk>x \<in> closed_segment w z; i \<le> n\<rbrakk> \<Longrightarrow> ((f i) has_field_derivative f (Suc i) x) (at x)"
1.37      shows "\<exists>u. u \<in> closed_segment w z \<and>
1.38              Re (f 0 z) =
```