--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Tue Nov 03 11:20:21 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Tue Nov 10 14:18:41 2015 +0000
@@ -19,7 +19,7 @@
shows "((op * c) has_derivative (op * c)) F"
by (rule has_derivative_mult_right [OF has_derivative_id])
-lemma has_derivative_of_real[derivative_intros, simp]:
+lemma has_derivative_of_real[derivative_intros, simp]:
"(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_derivative (\<lambda>x. of_real (f' x))) F"
using bounded_linear.has_derivative[OF bounded_linear_of_real] .
@@ -45,39 +45,39 @@
using bounded_linear.linear[OF bounded_linear_cnj] .
lemma tendsto_mult_left:
- fixes c::"'a::real_normed_algebra"
+ fixes c::"'a::real_normed_algebra"
shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. c * (f x)) ---> c * l) F"
by (rule tendsto_mult [OF tendsto_const])
lemma tendsto_mult_right:
- fixes c::"'a::real_normed_algebra"
+ fixes c::"'a::real_normed_algebra"
shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. (f x) * c) ---> l * c) F"
by (rule tendsto_mult [OF _ tendsto_const])
lemma tendsto_Re_upper:
- assumes "~ (trivial_limit F)"
- "(f ---> l) F"
+ assumes "~ (trivial_limit F)"
+ "(f ---> l) F"
"eventually (\<lambda>x. Re(f x) \<le> b) F"
shows "Re(l) \<le> b"
by (metis assms tendsto_le [OF _ tendsto_const] tendsto_Re)
lemma tendsto_Re_lower:
- assumes "~ (trivial_limit F)"
- "(f ---> l) F"
+ assumes "~ (trivial_limit F)"
+ "(f ---> l) F"
"eventually (\<lambda>x. b \<le> Re(f x)) F"
shows "b \<le> Re(l)"
by (metis assms tendsto_le [OF _ _ tendsto_const] tendsto_Re)
lemma tendsto_Im_upper:
- assumes "~ (trivial_limit F)"
- "(f ---> l) F"
+ assumes "~ (trivial_limit F)"
+ "(f ---> l) F"
"eventually (\<lambda>x. Im(f x) \<le> b) F"
shows "Im(l) \<le> b"
by (metis assms tendsto_le [OF _ tendsto_const] tendsto_Im)
lemma tendsto_Im_lower:
- assumes "~ (trivial_limit F)"
- "(f ---> l) F"
+ assumes "~ (trivial_limit F)"
+ "(f ---> l) F"
"eventually (\<lambda>x. b \<le> Im(f x)) F"
shows "b \<le> Im(l)"
by (metis assms tendsto_le [OF _ _ tendsto_const] tendsto_Im)
@@ -89,29 +89,29 @@
by auto
lemma continuous_mult_left:
- fixes c::"'a::real_normed_algebra"
+ fixes c::"'a::real_normed_algebra"
shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. c * f x)"
by (rule continuous_mult [OF continuous_const])
lemma continuous_mult_right:
- fixes c::"'a::real_normed_algebra"
+ fixes c::"'a::real_normed_algebra"
shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x * c)"
by (rule continuous_mult [OF _ continuous_const])
lemma continuous_on_mult_left:
- fixes c::"'a::real_normed_algebra"
+ fixes c::"'a::real_normed_algebra"
shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. c * f x)"
by (rule continuous_on_mult [OF continuous_on_const])
lemma continuous_on_mult_right:
- fixes c::"'a::real_normed_algebra"
+ fixes c::"'a::real_normed_algebra"
shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x * c)"
by (rule continuous_on_mult [OF _ continuous_on_const])
lemma uniformly_continuous_on_cmul_right [continuous_intros]:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)"
- using bounded_linear.uniformly_continuous_on[OF bounded_linear_mult_left] .
+ using bounded_linear.uniformly_continuous_on[OF bounded_linear_mult_left] .
lemma uniformly_continuous_on_cmul_left[continuous_intros]:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
@@ -141,7 +141,7 @@
lemma DERIV_zero_constant:
fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
shows "\<lbrakk>convex s;
- \<And>x. x\<in>s \<Longrightarrow> (f has_field_derivative 0) (at x within s)\<rbrakk>
+ \<And>x. x\<in>s \<Longrightarrow> (f has_field_derivative 0) (at x within s)\<rbrakk>
\<Longrightarrow> \<exists>c. \<forall>x \<in> s. f(x) = c"
by (auto simp: has_field_derivative_def lambda_zero intro: has_derivative_zero_constant)
@@ -162,7 +162,7 @@
and d0: "\<And>x. x\<in>s \<Longrightarrow> DERIV f x :> 0"
and "a \<in> s"
and "x \<in> s"
- shows "f x = f a"
+ shows "f x = f a"
by (rule has_derivative_zero_unique_connected [OF assms(2,1) _ assms(5,4)])
(metis has_field_derivative_def lambda_zero d0)
@@ -192,7 +192,7 @@
(*generalising DERIV_isconst_all, which requires type real (using the ordering)*)
lemma DERIV_zero_UNIV_unique:
fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
- shows "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
+ shows "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
by (metis DERIV_zero_unique UNIV_I assms convex_UNIV)
subsection \<open>Some limit theorems about real part of real series etc.\<close>
@@ -263,7 +263,7 @@
shows "(f ---> l) sequentially \<Longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
by (rule real_lim [where F=sequentially]) (auto simp: eventually_sequentially)
-lemma real_series:
+lemma real_series:
fixes l::complex
shows "f sums l \<Longrightarrow> (\<And>n. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
unfolding sums_def
@@ -276,7 +276,7 @@
subsection\<open>Holomorphic functions\<close>
definition complex_differentiable :: "[complex \<Rightarrow> complex, complex filter] \<Rightarrow> bool"
- (infixr "(complex'_differentiable)" 50)
+ (infixr "(complex'_differentiable)" 50)
where "f complex_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
lemma complex_differentiable_imp_continuous_at:
@@ -304,7 +304,7 @@
lemma complex_differentiable_const [derivative_intros]: "(\<lambda>z. c) complex_differentiable F"
unfolding complex_differentiable_def has_field_derivative_def
by (rule exI [where x=0])
- (metis has_derivative_const lambda_zero)
+ (metis has_derivative_const lambda_zero)
lemma complex_differentiable_ident [derivative_intros]: "(\<lambda>z. z) complex_differentiable F"
unfolding complex_differentiable_def has_field_derivative_def
@@ -343,14 +343,14 @@
by (metis DERIV_inverse_fun)
lemma complex_differentiable_mult [derivative_intros]:
- assumes "f complex_differentiable (at a within s)"
+ assumes "f complex_differentiable (at a within s)"
"g complex_differentiable (at a within s)"
shows "(\<lambda>z. f z * g z) complex_differentiable (at a within s)"
using assms unfolding complex_differentiable_def
by (metis DERIV_mult [of f _ a s g])
-
+
lemma complex_differentiable_divide [derivative_intros]:
- assumes "f complex_differentiable (at a within s)"
+ assumes "f complex_differentiable (at a within s)"
"g complex_differentiable (at a within s)"
"g a \<noteq> 0"
shows "(\<lambda>z. f z / g z) complex_differentiable (at a within s)"
@@ -358,7 +358,7 @@
by (metis DERIV_divide [of f _ a s g])
lemma complex_differentiable_power [derivative_intros]:
- assumes "f complex_differentiable (at a within s)"
+ assumes "f complex_differentiable (at a within s)"
shows "(\<lambda>z. f z ^ n) complex_differentiable (at a within s)"
using assms unfolding complex_differentiable_def
by (metis DERIV_power)
@@ -373,7 +373,7 @@
by (blast intro: has_derivative_transform_within)
lemma complex_differentiable_compose_within:
- assumes "f complex_differentiable (at a within s)"
+ assumes "f complex_differentiable (at a within s)"
"g complex_differentiable (at (f a) within f`s)"
shows "(g o f) complex_differentiable (at a within s)"
using assms unfolding complex_differentiable_def
@@ -385,7 +385,7 @@
by (metis complex_differentiable_at_within complex_differentiable_compose_within)
lemma complex_differentiable_within_open:
- "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f complex_differentiable at a within s \<longleftrightarrow>
+ "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f complex_differentiable at a within s \<longleftrightarrow>
f complex_differentiable at a"
unfolding complex_differentiable_def
by (metis at_within_open)
@@ -409,7 +409,7 @@
definition holomorphic_on :: "[complex \<Rightarrow> complex, complex set] \<Rightarrow> bool"
(infixl "(holomorphic'_on)" 50)
where "f holomorphic_on s \<equiv> \<forall>x\<in>s. f complex_differentiable (at x within s)"
-
+
named_theorems holomorphic_intros "structural introduction rules for holomorphic_on"
lemma holomorphic_on_empty [holomorphic_intros]: "f holomorphic_on {}"
@@ -419,9 +419,9 @@
"open s \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> (\<forall>x \<in> s. \<exists>f'. DERIV f x :> f')"
by (auto simp: holomorphic_on_def complex_differentiable_def has_field_derivative_def at_within_open [of _ s])
-lemma holomorphic_on_imp_continuous_on:
+lemma holomorphic_on_imp_continuous_on:
"f holomorphic_on s \<Longrightarrow> continuous_on s f"
- by (metis complex_differentiable_imp_continuous_at continuous_on_eq_continuous_within holomorphic_on_def)
+ by (metis complex_differentiable_imp_continuous_at continuous_on_eq_continuous_within holomorphic_on_def)
lemma holomorphic_on_subset:
"f holomorphic_on s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f holomorphic_on t"
@@ -505,19 +505,19 @@
by (metis DERIV_imp_deriv DERIV_const)
lemma complex_derivative_add:
- "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
+ "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
\<Longrightarrow> deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
by (auto intro!: DERIV_imp_deriv derivative_intros)
lemma complex_derivative_diff:
- "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
+ "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
\<Longrightarrow> deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
by (auto intro!: DERIV_imp_deriv derivative_intros)
lemma complex_derivative_mult:
- "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
+ "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
\<Longrightarrow> deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z"
unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
@@ -533,7 +533,7 @@
by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
lemma complex_derivative_transform_within_open:
- "\<lbrakk>f holomorphic_on s; g holomorphic_on s; open s; z \<in> s; \<And>w. w \<in> s \<Longrightarrow> f w = g w\<rbrakk>
+ "\<lbrakk>f holomorphic_on s; g holomorphic_on s; open s; z \<in> s; \<And>w. w \<in> s \<Longrightarrow> f w = g w\<rbrakk>
\<Longrightarrow> deriv f z = deriv g z"
unfolding holomorphic_on_def
by (rule DERIV_imp_deriv)
@@ -549,7 +549,7 @@
subsection\<open>Analyticity on a set\<close>
-definition analytic_on (infixl "(analytic'_on)" 50)
+definition analytic_on (infixl "(analytic'_on)" 50)
where
"f analytic_on s \<equiv> \<forall>x \<in> s. \<exists>e. 0 < e \<and> f holomorphic_on (ball x e)"
@@ -578,7 +578,7 @@
lemma analytic_on_UN: "f analytic_on (\<Union>i\<in>I. s i) \<longleftrightarrow> (\<forall>i\<in>I. f analytic_on (s i))"
by (auto simp: analytic_on_def)
-
+
lemma analytic_on_holomorphic:
"f analytic_on s \<longleftrightarrow> (\<exists>t. open t \<and> s \<subseteq> t \<and> f holomorphic_on t)"
(is "?lhs = ?rhs")
@@ -593,7 +593,7 @@
by (metis analytic_on_def)
next
fix t
- assume "open t" "s \<subseteq> t" "f analytic_on t"
+ assume "open t" "s \<subseteq> t" "f analytic_on t"
then show "f analytic_on s"
by (metis analytic_on_subset)
qed
@@ -625,17 +625,17 @@
then obtain e where e: "0 < e" and fh: "f holomorphic_on ball x e" using f
by (metis analytic_on_def)
obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball (f x) e'" using g
- by (metis analytic_on_def g image_eqI x)
+ by (metis analytic_on_def g image_eqI x)
have "isCont f x"
by (metis analytic_on_imp_differentiable_at complex_differentiable_imp_continuous_at f x)
with e' obtain d where d: "0 < d" and fd: "f ` ball x d \<subseteq> ball (f x) e'"
by (auto simp: continuous_at_ball)
- have "g \<circ> f holomorphic_on ball x (min d e)"
+ have "g \<circ> f holomorphic_on ball x (min d e)"
apply (rule holomorphic_on_compose)
apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
by (metis fd gh holomorphic_on_subset image_mono min.cobounded1 subset_ball)
then show "\<exists>e>0. g \<circ> f holomorphic_on ball x e"
- by (metis d e min_less_iff_conj)
+ by (metis d e min_less_iff_conj)
qed
lemma analytic_on_compose_gen:
@@ -658,9 +658,9 @@
then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f
by (metis analytic_on_def)
obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g
- by (metis analytic_on_def g z)
- have "(\<lambda>z. f z + g z) holomorphic_on ball z (min e e')"
- apply (rule holomorphic_on_add)
+ by (metis analytic_on_def g z)
+ have "(\<lambda>z. f z + g z) holomorphic_on ball z (min e e')"
+ apply (rule holomorphic_on_add)
apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
then show "\<exists>e>0. (\<lambda>z. f z + g z) holomorphic_on ball z e"
@@ -678,9 +678,9 @@
then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f
by (metis analytic_on_def)
obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g
- by (metis analytic_on_def g z)
- have "(\<lambda>z. f z - g z) holomorphic_on ball z (min e e')"
- apply (rule holomorphic_on_diff)
+ by (metis analytic_on_def g z)
+ have "(\<lambda>z. f z - g z) holomorphic_on ball z (min e e')"
+ apply (rule holomorphic_on_diff)
apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
then show "\<exists>e>0. (\<lambda>z. f z - g z) holomorphic_on ball z e"
@@ -698,9 +698,9 @@
then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f
by (metis analytic_on_def)
obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g
- by (metis analytic_on_def g z)
- have "(\<lambda>z. f z * g z) holomorphic_on ball z (min e e')"
- apply (rule holomorphic_on_mult)
+ by (metis analytic_on_def g z)
+ have "(\<lambda>z. f z * g z) holomorphic_on ball z (min e e')"
+ apply (rule holomorphic_on_mult)
apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
then show "\<exists>e>0. (\<lambda>z. f z * g z) holomorphic_on ball z e"
@@ -719,12 +719,12 @@
by (metis analytic_on_def)
have "continuous_on (ball z e) f"
by (metis fh holomorphic_on_imp_continuous_on)
- then obtain e' where e': "0 < e'" and nz': "\<And>y. dist z y < e' \<Longrightarrow> f y \<noteq> 0"
- by (metis Topology_Euclidean_Space.open_ball centre_in_ball continuous_on_open_avoid e z nz)
- have "(\<lambda>z. inverse (f z)) holomorphic_on ball z (min e e')"
+ then obtain e' where e': "0 < e'" and nz': "\<And>y. dist z y < e' \<Longrightarrow> f y \<noteq> 0"
+ by (metis Topology_Euclidean_Space.open_ball centre_in_ball continuous_on_open_avoid e z nz)
+ have "(\<lambda>z. inverse (f z)) holomorphic_on ball z (min e e')"
apply (rule holomorphic_on_inverse)
apply (metis fh holomorphic_on_subset min.cobounded2 min.commute subset_ball)
- by (metis nz' mem_ball min_less_iff_conj)
+ by (metis nz' mem_ball min_less_iff_conj)
then show "\<exists>e>0. (\<lambda>z. inverse (f z)) holomorphic_on ball z e"
by (metis e e' min_less_iff_conj)
qed
@@ -764,9 +764,9 @@
"f analytic_on {z} \<and> g analytic_on {z} \<longleftrightarrow>
(\<exists>s. open s \<and> z \<in> s \<and> f holomorphic_on s \<and> g holomorphic_on s)"
(is "?lhs = ?rhs")
-proof
+proof
assume ?lhs
- then obtain s t
+ then obtain s t
where st: "open s" "z \<in> s" "f holomorphic_on s"
"open t" "z \<in> t" "g holomorphic_on t"
by (auto simp: analytic_at)
@@ -776,14 +776,14 @@
apply (auto simp: Diff_subset holomorphic_on_subset)
done
next
- assume ?rhs
+ assume ?rhs
then show ?lhs
by (force simp add: analytic_at)
qed
subsection\<open>Combining theorems for derivative with ``analytic at'' hypotheses\<close>
-lemma
+lemma
assumes "f analytic_on {z}" "g analytic_on {z}"
shows complex_derivative_add_at: "deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
and complex_derivative_diff_at: "deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
@@ -826,14 +826,14 @@
and df: "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)"
and conv: "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<longrightarrow> x \<in> s \<longrightarrow> norm (f' n x - g' x) \<le> e"
and "\<exists>x l. x \<in> s \<and> ((\<lambda>n. f n x) ---> l) sequentially"
- shows "\<exists>g. \<forall>x \<in> s. ((\<lambda>n. f n x) ---> g x) sequentially \<and>
+ shows "\<exists>g. \<forall>x \<in> s. ((\<lambda>n. f n x) ---> g x) sequentially \<and>
(g has_field_derivative (g' x)) (at x within s)"
proof -
from assms obtain x l where x: "x \<in> s" and tf: "((\<lambda>n. f n x) ---> l) sequentially"
by blast
{ fix e::real assume e: "e > 0"
then obtain N where N: "\<forall>n\<ge>N. \<forall>x. x \<in> s \<longrightarrow> cmod (f' n x - g' x) \<le> e"
- by (metis conv)
+ by (metis conv)
have "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
proof (rule exI [of _ N], clarify)
fix n y h
@@ -863,7 +863,7 @@
fixes s :: "complex set"
assumes cvs: "convex s"
and df: "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)"
- and conv: "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<longrightarrow> x \<in> s
+ and conv: "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<longrightarrow> x \<in> s
\<longrightarrow> cmod ((\<Sum>i<n. f' i x) - g' x) \<le> e"
and "\<exists>x l. x \<in> s \<and> ((\<lambda>n. f n x) sums l)"
shows "\<exists>g. \<forall>x \<in> s. ((\<lambda>n. f n x) sums g x) \<and> ((g has_field_derivative g' x) (at x within s))"
@@ -871,9 +871,9 @@
from assms obtain x l where x: "x \<in> s" and sf: "((\<lambda>n. f n x) sums l)"
by blast
{ fix e::real assume e: "e > 0"
- then obtain N where N: "\<forall>n x. n \<ge> N \<longrightarrow> x \<in> s
+ then obtain N where N: "\<forall>n x. n \<ge> N \<longrightarrow> x \<in> s
\<longrightarrow> cmod ((\<Sum>i<n. f' i x) - g' x) \<le> e"
- by (metis conv)
+ by (metis conv)
have "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
proof (rule exI [of _ N], clarify)
fix n y h
@@ -979,7 +979,7 @@
\<Longrightarrow> DERIV g (f x) :> inverse (f')"
unfolding has_field_derivative_def
apply (rule has_derivative_inverse_strong [of s x f g ])
- using assms
+ using assms
by auto
lemma has_complex_derivative_inverse_strong_x:
@@ -993,7 +993,7 @@
\<Longrightarrow> DERIV g y :> inverse (f')"
unfolding has_field_derivative_def
apply (rule has_derivative_inverse_strong_x [of s g y f])
- using assms
+ using assms
by auto
subsection \<open>Taylor on Complex Numbers\<close>
@@ -1004,7 +1004,7 @@
by (induct n) auto
lemma complex_taylor:
- assumes s: "convex s"
+ assumes s: "convex s"
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)"
and B: "\<And>x. x \<in> s \<Longrightarrow> cmod (f (Suc n) x) \<le> B"
and w: "w \<in> s"
@@ -1019,14 +1019,14 @@
then have "u \<in> s"
by (metis wzs subsetD)
have "(\<Sum>i\<le>n. f i u * (- of_nat i * (z-u)^(i - 1)) / (fact i) +
- f (Suc i) u * (z-u)^i / (fact i)) =
+ f (Suc i) u * (z-u)^i / (fact i)) =
f (Suc n) u * (z-u) ^ n / (fact n)"
proof (induction n)
case 0 show ?case by simp
next
case (Suc n)
have "(\<Sum>i\<le>Suc n. f i u * (- of_nat i * (z-u) ^ (i - 1)) / (fact i) +
- f (Suc i) u * (z-u) ^ i / (fact i)) =
+ f (Suc i) u * (z-u) ^ i / (fact i)) =
f (Suc n) u * (z-u) ^ n / (fact n) +
f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n) / (fact (Suc n)) -
f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n) / (fact (Suc n))"
@@ -1056,7 +1056,7 @@
qed
finally show ?case .
qed
- then have "((\<lambda>v. (\<Sum>i\<le>n. f i v * (z - v)^i / (fact i)))
+ then have "((\<lambda>v. (\<Sum>i\<le>n. f i v * (z - v)^i / (fact i)))
has_field_derivative f (Suc n) u * (z-u) ^ n / (fact n))
(at u within s)"
apply (intro derivative_eq_intros)
@@ -1081,19 +1081,19 @@
by simp
also have "\<dots> = f 0 z / (fact 0)"
by (subst setsum_zero_power) simp
- finally have "cmod (f 0 z - (\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i)))
+ finally have "cmod (f 0 z - (\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i)))
\<le> cmod ((\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i)) -
(\<Sum>i\<le>n. f i z * (z - z) ^ i / (fact i)))"
by (simp add: norm_minus_commute)
also have "... \<le> B * cmod (z - w) ^ n / (fact n) * cmod (w - z)"
- apply (rule complex_differentiable_bound
+ apply (rule complex_differentiable_bound
[where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / (fact n)"
and s = "closed_segment w z", OF convex_closed_segment])
- apply (auto simp: ends_in_segment real_of_nat_def DERIV_subset [OF sum_deriv wzs]
+ apply (auto simp: ends_in_segment DERIV_subset [OF sum_deriv wzs]
norm_divide norm_mult norm_power divide_le_cancel cmod_bound)
done
also have "... \<le> B * cmod (z - w) ^ Suc n / (fact n)"
- by (simp add: algebra_simps norm_minus_commute real_of_nat_def)
+ by (simp add: algebra_simps norm_minus_commute)
finally show ?thesis .
qed
@@ -1142,7 +1142,7 @@
(f (Suc (Suc n)) u * ((z-u) ^ Suc n) - (of_nat (Suc n)) * (z-u) ^ n * f (Suc n) u) /
(fact (Suc n)) +
(\<Sum>i = 0..n.
- f (Suc (Suc i)) u * ((z-u) ^ Suc i) / (fact (Suc i)) -
+ f (Suc (Suc i)) u * ((z-u) ^ Suc i) / (fact (Suc i)) -
f (Suc i) u * (z-u) ^ i / (fact i))"
by (simp only: diff_divide_distrib fact_cancel ac_simps)
also have "... = f (Suc 0) u -
@@ -1152,7 +1152,7 @@
by (subst setsum_Suc_diff) auto
also have "... = f (Suc n) u * (z-u) ^ n / (fact n)"
by (simp only: algebra_simps diff_divide_distrib fact_cancel)
- finally have "(\<Sum>i = 0..n. (f (Suc i) u * (z - u) ^ i
+ finally have "(\<Sum>i = 0..n. (f (Suc i) u * (z - u) ^ i
- of_nat i * (f i u * (z-u) ^ (i - Suc 0))) / (fact i)) =
f (Suc n) u * (z - u) ^ n / (fact n)" .
then have "((\<lambda>u. \<Sum>i = 0..n. f i u * (z - u) ^ i / (fact i)) has_field_derivative