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) =