src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 66252 b73f94b366b7
parent 66089 def95e0bc529
child 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Jul 02 20:13:38 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Jul 04 09:36:25 2017 +0100
     1.3 @@ -23,10 +23,11 @@
     1.4    "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_derivative (\<lambda>x. of_real (f' x))) F"
     1.5    using bounded_linear.has_derivative[OF bounded_linear_of_real] .
     1.6  
     1.7 -lemma has_vector_derivative_real_complex:
     1.8 +lemma has_vector_derivative_real_field:
     1.9    "DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)"
    1.10    using has_derivative_compose[of of_real of_real a _ f "op * f'"]
    1.11    by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)
    1.12 +lemmas has_vector_derivative_real_complex = has_vector_derivative_real_field
    1.13  
    1.14  lemma fact_cancel:
    1.15    fixes c :: "'a::real_field"
    1.16 @@ -124,15 +125,9 @@
    1.17  using has_derivative_zero_connected_constant [OF assms(1-4)] assms
    1.18  by (metis DERIV_const has_derivative_const Diff_iff at_within_open frechet_derivative_at has_field_derivative_def)
    1.19  
    1.20 -lemma DERIV_zero_constant:
    1.21 -  fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
    1.22 -  shows    "\<lbrakk>convex s;
    1.23 -             \<And>x. x\<in>s \<Longrightarrow> (f has_field_derivative 0) (at x within s)\<rbrakk>
    1.24 -             \<Longrightarrow> \<exists>c. \<forall>x \<in> s. f(x) = c"
    1.25 -  by (auto simp: has_field_derivative_def lambda_zero intro: has_derivative_zero_constant)
    1.26 +lemmas DERIV_zero_constant = has_field_derivative_zero_constant
    1.27  
    1.28  lemma DERIV_zero_unique:
    1.29 -  fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
    1.30    assumes "convex s"
    1.31        and d0: "\<And>x. x\<in>s \<Longrightarrow> (f has_field_derivative 0) (at x within s)"
    1.32        and "a \<in> s"
    1.33 @@ -142,7 +137,6 @@
    1.34       (metis d0 has_field_derivative_imp_has_derivative lambda_zero)
    1.35  
    1.36  lemma DERIV_zero_connected_unique:
    1.37 -  fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
    1.38    assumes "connected s"
    1.39        and "open s"
    1.40        and d0: "\<And>x. x\<in>s \<Longrightarrow> DERIV f x :> 0"
    1.41 @@ -177,9 +171,8 @@
    1.42  
    1.43  (*generalising DERIV_isconst_all, which requires type real (using the ordering)*)
    1.44  lemma DERIV_zero_UNIV_unique:
    1.45 -  fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
    1.46 -  shows "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
    1.47 -by (metis DERIV_zero_unique UNIV_I convex_UNIV)
    1.48 +  "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
    1.49 +  by (metis DERIV_zero_unique UNIV_I convex_UNIV)
    1.50  
    1.51  subsection \<open>Some limit theorems about real part of real series etc.\<close>
    1.52  
    1.53 @@ -854,7 +847,7 @@
    1.54  
    1.55  
    1.56  lemma field_differentiable_series:
    1.57 -  fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
    1.58 +  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach} \<Rightarrow> 'a"
    1.59    assumes "convex s" "open s"
    1.60    assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
    1.61    assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
    1.62 @@ -879,7 +872,7 @@
    1.63  qed
    1.64  
    1.65  lemma field_differentiable_series':
    1.66 -  fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
    1.67 +  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach} \<Rightarrow> 'a"
    1.68    assumes "convex s" "open s"
    1.69    assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
    1.70    assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
    1.71 @@ -890,7 +883,7 @@
    1.72  subsection\<open>Bound theorem\<close>
    1.73  
    1.74  lemma field_differentiable_bound:
    1.75 -  fixes s :: "complex set"
    1.76 +  fixes s :: "'a::real_normed_field set"
    1.77    assumes cvs: "convex s"
    1.78        and df:  "\<And>z. z \<in> s \<Longrightarrow> (f has_field_derivative f' z) (at z within s)"
    1.79        and dn:  "\<And>z. z \<in> s \<Longrightarrow> norm (f' z) \<le> B"
    1.80 @@ -905,8 +898,7 @@
    1.81  
    1.82  subsection\<open>Inverse function theorem for complex derivatives\<close>
    1.83  
    1.84 -lemma has_complex_derivative_inverse_basic:
    1.85 -  fixes f :: "complex \<Rightarrow> complex"
    1.86 +lemma has_field_derivative_inverse_basic:
    1.87    shows "DERIV f (g y) :> f' \<Longrightarrow>
    1.88          f' \<noteq> 0 \<Longrightarrow>
    1.89          continuous (at y) g \<Longrightarrow>
    1.90 @@ -919,8 +911,10 @@
    1.91    apply (auto simp:  bounded_linear_mult_right)
    1.92    done
    1.93  
    1.94 -lemma has_complex_derivative_inverse_strong:
    1.95 -  fixes f :: "complex \<Rightarrow> complex"
    1.96 +lemmas has_complex_derivative_inverse_basic = has_field_derivative_inverse_basic
    1.97 +
    1.98 +lemma has_field_derivative_inverse_strong:
    1.99 +  fixes f :: "'a::{euclidean_space,real_normed_field} \<Rightarrow> 'a"
   1.100    shows "DERIV f x :> f' \<Longrightarrow>
   1.101           f' \<noteq> 0 \<Longrightarrow>
   1.102           open s \<Longrightarrow>
   1.103 @@ -931,9 +925,10 @@
   1.104    unfolding has_field_derivative_def
   1.105    apply (rule has_derivative_inverse_strong [of s x f g ])
   1.106    by auto
   1.107 +lemmas has_complex_derivative_inverse_strong = has_field_derivative_inverse_strong
   1.108  
   1.109 -lemma has_complex_derivative_inverse_strong_x:
   1.110 -  fixes f :: "complex \<Rightarrow> complex"
   1.111 +lemma has_field_derivative_inverse_strong_x:
   1.112 +  fixes f :: "'a::{euclidean_space,real_normed_field} \<Rightarrow> 'a"
   1.113    shows  "DERIV f (g y) :> f' \<Longrightarrow>
   1.114            f' \<noteq> 0 \<Longrightarrow>
   1.115            open s \<Longrightarrow>
   1.116 @@ -944,6 +939,7 @@
   1.117    unfolding has_field_derivative_def
   1.118    apply (rule has_derivative_inverse_strong_x [of s g y f])
   1.119    by auto
   1.120 +lemmas has_complex_derivative_inverse_strong_x = has_field_derivative_inverse_strong_x
   1.121  
   1.122  subsection \<open>Taylor on Complex Numbers\<close>
   1.123  
   1.124 @@ -952,14 +948,14 @@
   1.125      shows  "sum f {0..n} = f 0 - f (Suc n) + sum (\<lambda>i. f (Suc i)) {0..n}"
   1.126  by (induct n) auto
   1.127  
   1.128 -lemma complex_taylor:
   1.129 +lemma field_taylor:
   1.130    assumes s: "convex s"
   1.131        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.132 -      and B: "\<And>x. x \<in> s \<Longrightarrow> cmod (f (Suc n) x) \<le> B"
   1.133 +      and B: "\<And>x. x \<in> s \<Longrightarrow> norm (f (Suc n) x) \<le> B"
   1.134        and w: "w \<in> s"
   1.135        and z: "z \<in> s"
   1.136 -    shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i)))
   1.137 -          \<le> B * cmod(z - w)^(Suc n) / fact n"
   1.138 +    shows "norm(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i)))
   1.139 +          \<le> B * norm(z - w)^(Suc n) / fact n"
   1.140  proof -
   1.141    have wzs: "closed_segment w z \<subseteq> s" using assms
   1.142      by (metis convex_contains_segment)
   1.143 @@ -1018,34 +1014,45 @@
   1.144      assume u: "u \<in> closed_segment w z"
   1.145      then have us: "u \<in> s"
   1.146        by (metis wzs subsetD)
   1.147 -    have "cmod (f (Suc n) u) * cmod (z - u) ^ n \<le> cmod (f (Suc n) u) * cmod (u - z) ^ n"
   1.148 +    have "norm (f (Suc n) u) * norm (z - u) ^ n \<le> norm (f (Suc n) u) * norm (u - z) ^ n"
   1.149        by (metis norm_minus_commute order_refl)
   1.150 -    also have "... \<le> cmod (f (Suc n) u) * cmod (z - w) ^ n"
   1.151 +    also have "... \<le> norm (f (Suc n) u) * norm (z - w) ^ n"
   1.152        by (metis mult_left_mono norm_ge_zero power_mono segment_bound [OF u])
   1.153 -    also have "... \<le> B * cmod (z - w) ^ n"
   1.154 +    also have "... \<le> B * norm (z - w) ^ n"
   1.155        by (metis norm_ge_zero zero_le_power mult_right_mono  B [OF us])
   1.156 -    finally have "cmod (f (Suc n) u) * cmod (z - u) ^ n \<le> B * cmod (z - w) ^ n" .
   1.157 +    finally have "norm (f (Suc n) u) * norm (z - u) ^ n \<le> B * norm (z - w) ^ n" .
   1.158    } note cmod_bound = this
   1.159    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.160      by simp
   1.161    also have "\<dots> = f 0 z / (fact 0)"
   1.162      by (subst sum_zero_power) simp
   1.163 -  finally have "cmod (f 0 z - (\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i)))
   1.164 -                \<le> cmod ((\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i)) -
   1.165 +  finally have "norm (f 0 z - (\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i)))
   1.166 +                \<le> norm ((\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i)) -
   1.167                          (\<Sum>i\<le>n. f i z * (z - z) ^ i / (fact i)))"
   1.168      by (simp add: norm_minus_commute)
   1.169 -  also have "... \<le> B * cmod (z - w) ^ n / (fact n) * cmod (w - z)"
   1.170 +  also have "... \<le> B * norm (z - w) ^ n / (fact n) * norm (w - z)"
   1.171      apply (rule field_differentiable_bound
   1.172        [where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / (fact n)"
   1.173           and s = "closed_segment w z", OF convex_closed_segment])
   1.174      apply (auto simp: ends_in_segment DERIV_subset [OF sum_deriv wzs]
   1.175                    norm_divide norm_mult norm_power divide_le_cancel cmod_bound)
   1.176      done
   1.177 -  also have "...  \<le> B * cmod (z - w) ^ Suc n / (fact n)"
   1.178 +  also have "...  \<le> B * norm (z - w) ^ Suc n / (fact n)"
   1.179      by (simp add: algebra_simps norm_minus_commute)
   1.180    finally show ?thesis .
   1.181  qed
   1.182  
   1.183 +lemma complex_taylor:
   1.184 +  assumes s: "convex s"
   1.185 +      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.186 +      and B: "\<And>x. x \<in> s \<Longrightarrow> cmod (f (Suc n) x) \<le> B"
   1.187 +      and w: "w \<in> s"
   1.188 +      and z: "z \<in> s"
   1.189 +    shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i)))
   1.190 +          \<le> B * cmod(z - w)^(Suc n) / fact n"
   1.191 +  using assms by (rule field_taylor)
   1.192 +
   1.193 +
   1.194  text\<open>Something more like the traditional MVT for real components\<close>
   1.195  
   1.196  lemma complex_mvt_line: