--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Tue Mar 10 16:12:35 2015 +0000
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Mar 16 15:30:00 2015 +0000
@@ -8,6 +8,10 @@
imports "~~/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space"
begin
+
+lemma cmod_fact [simp]: "cmod (fact n) = fact n"
+ by (metis norm_of_nat of_nat_fact)
+
subsection{*General lemmas*}
lemma has_derivative_mult_right:
@@ -26,7 +30,7 @@
lemma fact_cancel:
fixes c :: "'a::real_field"
- shows "of_nat (Suc n) * c / of_nat (fact (Suc n)) = c / of_nat (fact n)"
+ shows "of_nat (Suc n) * c / (fact (Suc n)) = c / (fact n)"
by (simp add: of_nat_mult del: of_nat_Suc times_nat.simps)
lemma linear_times:
@@ -985,7 +989,7 @@
and B: "\<And>x. x \<in> s \<Longrightarrow> cmod (f (Suc n) x) \<le> B"
and w: "w \<in> s"
and z: "z \<in> s"
- shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / of_nat (fact i)))
+ shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i)))
\<le> B * cmod(z - w)^(Suc n) / fact n"
proof -
have wzs: "closed_segment w z \<subseteq> s" using assms
@@ -994,48 +998,46 @@
assume "u \<in> closed_segment w z"
then have "u \<in> s"
by (metis wzs subsetD)
- have "(\<Sum>i\<le>n. f i u * (- of_nat i * (z-u)^(i - 1)) / of_nat (fact i) +
- f (Suc i) u * (z-u)^i / of_nat (fact i)) =
- f (Suc n) u * (z-u) ^ n / of_nat (fact n)"
+ 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 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)) / of_nat (fact i) +
- f (Suc i) u * (z-u) ^ i / of_nat (fact i)) =
- f (Suc n) u * (z-u) ^ n / of_nat (fact n) +
- f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n) / of_nat (fact (Suc n)) -
- f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n) / of_nat (fact (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 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))"
using Suc by simp
- also have "... = f (Suc (Suc n)) u * (z-u) ^ Suc n / of_nat (fact (Suc n))"
+ also have "... = f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n))"
proof -
- have "of_nat(fact(Suc n)) *
- (f(Suc n) u *(z-u) ^ n / of_nat(fact n) +
- f(Suc(Suc n)) u *((z-u) *(z-u) ^ n) / of_nat(fact(Suc n)) -
- f(Suc n) u *((1 + of_nat n) *(z-u) ^ n) / of_nat(fact(Suc n))) =
- (of_nat(fact(Suc n)) *(f(Suc n) u *(z-u) ^ n)) / of_nat(fact n) +
- (of_nat(fact(Suc n)) *(f(Suc(Suc n)) u *((z-u) *(z-u) ^ n)) / of_nat(fact(Suc n))) -
- (of_nat(fact(Suc n)) *(f(Suc n) u *(of_nat(Suc n) *(z-u) ^ n))) / of_nat(fact(Suc n))"
- by (simp add: algebra_simps del: fact_Suc)
- also have "... =
- (of_nat (fact (Suc n)) * (f (Suc n) u * (z-u) ^ n)) / of_nat (fact n) +
- (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
- (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
- by (simp del: fact_Suc)
- also have "... =
- (of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) +
- (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
- (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
- by (simp only: fact_Suc of_nat_mult ac_simps) simp
+ have "(fact(Suc n)) *
+ (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))) =
+ ((fact(Suc n)) *(f(Suc n) u *(z-u) ^ n)) / (fact n) +
+ ((fact(Suc n)) *(f(Suc(Suc n)) u *((z-u) *(z-u) ^ n)) / (fact(Suc n))) -
+ ((fact(Suc n)) *(f(Suc n) u *(of_nat(Suc n) *(z-u) ^ n))) / (fact(Suc n))"
+ by (simp add: algebra_simps del: fact.simps)
+ also have "... = ((fact (Suc n)) * (f (Suc n) u * (z-u) ^ n)) / (fact n) +
+ (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
+ (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
+ by (simp del: fact.simps)
+ also have "... = (of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) +
+ (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
+ (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
+ by (simp only: fact.simps of_nat_mult ac_simps) simp
also have "... = f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)"
by (simp add: algebra_simps)
finally show ?thesis
- by (simp add: mult_left_cancel [where c = "of_nat (fact (Suc n))", THEN iffD1] del: fact_Suc)
+ by (simp add: mult_left_cancel [where c = "(fact (Suc n))", THEN iffD1] del: fact.simps)
qed
finally show ?case .
qed
- then have "((\<lambda>v. (\<Sum>i\<le>n. f i v * (z - v)^i / of_nat (fact i)))
- has_field_derivative f (Suc n) u * (z-u) ^ n / of_nat (fact n))
+ 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)
apply (blast intro: assms `u \<in> s`)
@@ -1055,22 +1057,22 @@
by (metis norm_ge_zero zero_le_power mult_right_mono B [OF us])
finally have "cmod (f (Suc n) u) * cmod (z - u) ^ n \<le> B * cmod (z - w) ^ n" .
} note cmod_bound = this
- have "(\<Sum>i\<le>n. f i z * (z - z) ^ i / of_nat (fact i)) = (\<Sum>i\<le>n. (f i z / of_nat (fact i)) * 0 ^ i)"
+ have "(\<Sum>i\<le>n. f i z * (z - z) ^ i / (fact i)) = (\<Sum>i\<le>n. (f i z / (fact i)) * 0 ^ i)"
by simp
- also have "\<dots> = f 0 z / of_nat (fact 0)"
+ 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 / of_nat (fact i)))
- \<le> cmod ((\<Sum>i\<le>n. f i w * (z - w) ^ i / of_nat (fact i)) -
- (\<Sum>i\<le>n. f i z * (z - z) ^ i / of_nat (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 / real_of_nat (fact n) * cmod (w - z)"
+ also have "... \<le> B * cmod (z - w) ^ n / (fact n) * cmod (w - z)"
apply (rule complex_differentiable_bound
- [where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / of_nat(fact n)"
+ [where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / (fact n)"
and s = "closed_segment w z", OF convex_segment])
apply (auto simp: ends_in_segment real_of_nat_def 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 / real (fact n)"
+ also have "... \<le> B * cmod (z - w) ^ Suc n / (fact n)"
by (simp add: algebra_simps norm_minus_commute real_of_nat_def)
finally show ?thesis .
qed
@@ -1102,40 +1104,40 @@
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)"
shows "\<exists>u. u \<in> closed_segment w z \<and>
Re (f 0 z) =
- Re ((\<Sum>i = 0..n. f i w * (z - w) ^ i / of_nat (fact i)) +
- (f (Suc n) u * (z-u)^n / of_nat (fact n)) * (z - w))"
+ Re ((\<Sum>i = 0..n. f i w * (z - w) ^ i / (fact i)) +
+ (f (Suc n) u * (z-u)^n / (fact n)) * (z - w))"
proof -
{ fix u
assume u: "u \<in> closed_segment w z"
have "(\<Sum>i = 0..n.
(f (Suc i) u * (z-u) ^ i - of_nat i * (f i u * (z-u) ^ (i - Suc 0))) /
- of_nat (fact i)) =
+ (fact i)) =
f (Suc 0) u -
(f (Suc (Suc n)) u * ((z-u) ^ Suc n) - (of_nat (Suc n)) * (z-u) ^ n * f (Suc n) u) /
- of_nat (fact (Suc n)) +
+ (fact (Suc n)) +
(\<Sum>i = 0..n.
(f (Suc (Suc i)) u * ((z-u) ^ Suc i) - of_nat (Suc i) * (f (Suc i) u * (z-u) ^ i)) /
- of_nat (fact (Suc i)))"
+ (fact (Suc i)))"
by (subst setsum_Suc_reindex) simp
also have "... = f (Suc 0) u -
(f (Suc (Suc n)) u * ((z-u) ^ Suc n) - (of_nat (Suc n)) * (z-u) ^ n * f (Suc n) u) /
- of_nat (fact (Suc n)) +
+ (fact (Suc n)) +
(\<Sum>i = 0..n.
- f (Suc (Suc i)) u * ((z-u) ^ Suc i) / of_nat (fact (Suc i)) -
- f (Suc i) u * (z-u) ^ i / of_nat (fact 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 -
(f (Suc (Suc n)) u * (z-u) ^ Suc n - of_nat (Suc n) * (z-u) ^ n * f (Suc n) u) /
- of_nat (fact (Suc n)) +
- f (Suc (Suc n)) u * (z-u) ^ Suc n / of_nat (fact (Suc n)) - f (Suc 0) u"
+ (fact (Suc n)) +
+ f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n)) - f (Suc 0) u"
by (subst setsum_Suc_diff) auto
- also have "... = f (Suc n) u * (z-u) ^ n / of_nat (fact n)"
+ 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
- - of_nat i * (f i u * (z-u) ^ (i - Suc 0))) / of_nat (fact i)) =
- f (Suc n) u * (z - u) ^ n / of_nat (fact n)" .
- then have "((\<lambda>u. \<Sum>i = 0..n. f i u * (z - u) ^ i / of_nat (fact i)) has_field_derivative
- f (Suc n) u * (z - u) ^ n / of_nat (fact n)) (at u)"
+ - 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
+ f (Suc n) u * (z - u) ^ n / (fact n)) (at u)"
apply (intro derivative_eq_intros)+
apply (force intro: u assms)
apply (rule refl)+
@@ -1143,8 +1145,8 @@
done
}
then show ?thesis
- apply (cut_tac complex_mvt_line [of w z "\<lambda>u. \<Sum>i = 0..n. f i u * (z-u) ^ i / of_nat (fact i)"
- "\<lambda>u. (f (Suc n) u * (z-u)^n / of_nat (fact n))"])
+ apply (cut_tac complex_mvt_line [of w z "\<lambda>u. \<Sum>i = 0..n. f i u * (z-u) ^ i / (fact i)"
+ "\<lambda>u. (f (Suc n) u * (z-u)^n / (fact n))"])
apply (auto simp add: intro: open_closed_segment)
done
qed