author immler Tue Jul 04 09:36:25 2017 +0100 (22 months ago) changeset 66252 b73f94b366b7 parent 66251 cd935b7cb3fb child 66253 a0cc7ebc7751
some generalizations complex=>real_normed_field
```     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.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:
```
```     2.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Jul 02 20:13:38 2017 +0200
2.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jul 04 09:36:25 2017 +0100
2.3 @@ -582,6 +582,35 @@
2.4
2.5  declare power_Suc [simp del]
2.6
2.7 +lemma Taylor_exp_field:
2.8 +  fixes z::"'a::{banach,real_normed_field}"
2.9 +  shows "norm (exp z - (\<Sum>i\<le>n. z ^ i / fact i)) \<le> exp (norm z) * (norm z ^ Suc n) / fact n"
2.10 +proof (rule field_taylor[of _ n "\<lambda>k. exp" "exp (norm z)" 0 z, simplified])
2.11 +  show "convex (closed_segment 0 z)"
2.12 +    by (rule convex_closed_segment [of 0 z])
2.13 +next
2.14 +  fix k x
2.15 +  assume "x \<in> closed_segment 0 z" "k \<le> n"
2.16 +  show "(exp has_field_derivative exp x) (at x within closed_segment 0 z)"
2.17 +    using DERIV_exp DERIV_subset by blast
2.18 +next
2.19 +  fix x
2.20 +  assume x: "x \<in> closed_segment 0 z"
2.21 +  have "norm (exp x) \<le> exp (norm x)"
2.22 +    by (rule norm_exp)
2.23 +  also have "norm x \<le> norm z"
2.24 +    using x by (auto simp: closed_segment_def intro!: mult_left_le_one_le)
2.25 +  finally show "norm (exp x) \<le> exp (norm z)"
2.26 +    by simp
2.27 +next
2.28 +  show "0 \<in> closed_segment 0 z"
2.29 +    by (auto simp: closed_segment_def)
2.30 +next
2.31 +  show "z \<in> closed_segment 0 z"
2.32 +    apply (simp add: closed_segment_def scaleR_conv_of_real)
2.33 +    using of_real_1 zero_le_one by blast
2.34 +qed
2.35 +
2.36  lemma Taylor_exp:
2.37    "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
2.38  proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
```