# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1395416160 0
# Node ID 5d147e1e18d11173d4eb316420b20634c54ae2a4
# Parent  69a9dfe71aed821d1c67debe08ef6d6e31fb71ab
a few new lemmas and generalisations of old ones

diff -r 69a9dfe71aed -r 5d147e1e18d1 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/Complex.thy	Fri Mar 21 15:36:00 2014 +0000
@@ -399,6 +399,10 @@
     by (rule convergentI)
 qed
 
+declare
+  DERIV_power[where 'a=complex, THEN DERIV_cong,
+              unfolded of_nat_def[symmetric], DERIV_intros]
+
 
 subsection {* The Complex Number $i$ *}
 
diff -r 69a9dfe71aed -r 5d147e1e18d1 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/MacLaurin.thy	Fri Mar 21 15:36:00 2014 +0000
@@ -270,7 +270,7 @@
   show ?thesis
   proof (cases rule: linorder_cases)
     assume "x = 0" with `n \<noteq> 0` `diff 0 = f` DERIV
-    have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by (force simp add: Maclaurin_bi_le_lemma)
+    have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by (auto simp add: Maclaurin_bi_le_lemma)
     thus ?thesis ..
   next
     assume "x < 0"
diff -r 69a9dfe71aed -r 5d147e1e18d1 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri Mar 21 15:36:00 2014 +0000
@@ -36,6 +36,22 @@
   by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Im 
             continuous_on_cong continuous_on_id)
 
+lemma open_closed_segment: "u \<in> open_segment w z \<Longrightarrow> u \<in> closed_segment w z"
+  by (auto simp add: closed_segment_def open_segment_def)
+
+lemma has_derivative_Re [has_derivative_intros] : "(Re has_derivative Re) F"
+  by (auto simp add: has_derivative_def bounded_linear_Re)
+
+lemma has_derivative_Im [has_derivative_intros] : "(Im has_derivative Im) F"
+  by (auto simp add: has_derivative_def bounded_linear_Im)
+
+lemma fact_cancel:
+  fixes c :: "'a::real_field"
+  shows "of_nat (Suc n) * c / of_nat (fact (Suc n)) = c / of_nat (fact n)"
+  apply (subst frac_eq_eq [OF of_nat_fact_not_zero of_nat_fact_not_zero])
+  apply (simp add: algebra_simps of_nat_mult)
+  done
+
 lemma open_halfspace_Re_lt: "open {z. Re(z) < b}"
 proof -
   have "{z. Re(z) < b} = Re -`{..<b}"
@@ -1403,4 +1419,97 @@
   finally show ?thesis .
 qed
 
+text{* Something more like the traditional MVT for real components.*}
+lemma complex_mvt_line:
+  assumes "\<And>u. u \<in> closed_segment w z ==> (f has_field_derivative f'(u)) (at u)"
+    shows "\<exists>u. u \<in> open_segment w z \<and> Re(f z) - Re(f w) = Re(f'(u) * (z - w))"
+proof -
+  have twz: "\<And>t. (1 - t) *\<^sub>R w + t *\<^sub>R z = w + t *\<^sub>R (z - w)"
+    by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
+  show ?thesis
+    apply (cut_tac mvt_simple
+                     [of 0 1 "Re o f o (\<lambda>t. (1 - t) *\<^sub>R w +  t *\<^sub>R z)"
+                      "\<lambda>u. Re o (\<lambda>h. f'((1 - u) *\<^sub>R w + u *\<^sub>R z) * h) o (\<lambda>t. t *\<^sub>R (z - w))"])
+    apply auto
+    apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI)
+    apply (simp add: open_segment_def)
+    apply (auto simp add: twz)
+    apply (rule has_derivative_at_within)
+    apply (intro has_derivative_intros has_derivative_add [OF has_derivative_const, simplified])+
+    apply (rule assms [unfolded has_field_derivative_def])
+    apply (force simp add: twz closed_segment_def)
+    done
+qed
+
+lemma complex_taylor_mvt:
+  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))"
+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)) =
+          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)) +
+             (\<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)))"
+       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)) +
+             (\<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))"
+      by (simp only: diff_divide_distrib fact_cancel mult_ac)
+    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"
+      by (subst setsum_Suc_diff) auto
+    also have "... = f (Suc n) u * (z-u) ^ n / of_nat (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)"
+      apply (intro DERIV_intros)+
+      apply (force intro: u assms)
+      apply (rule refl)+
+      apply (auto simp: mult_ac)
+      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 (auto simp add: intro: open_closed_segment)
+    done
+qed
+
+text{*Relations among convergence and absolute convergence for power series.*}
+lemma abel_lemma:
+  fixes a :: "nat \<Rightarrow> 'a::real_normed_vector"
+  assumes r: "0 \<le> r" and r0: "r < r0" and M: "\<And>n. norm(a n) * r0^n \<le> M"
+    shows "summable (\<lambda>n. norm(a(n)) * r^n)"
+proof (rule summable_comparison_test' [of "\<lambda>n. M * (r / r0)^n"])
+  show "summable (\<lambda>n. M * (r / r0) ^ n)"
+    using assms 
+    by (auto simp add: summable_mult summable_geometric)
+  next
+    fix n
+    show "norm (norm (a n) * r ^ n) \<le> M * (r / r0) ^ n"
+      using r r0 M [of n]
+      apply (auto simp add: abs_mult field_simps power_divide)
+      apply (cases "r=0", simp)
+      apply (cases n, auto)
+      done
+qed
+
+
 end
diff -r 69a9dfe71aed -r 5d147e1e18d1 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/Set_Interval.thy	Fri Mar 21 15:36:00 2014 +0000
@@ -1468,9 +1468,14 @@
   finally show ?case .
 qed
 
-lemma setsum_last_plus: "n \<noteq> 0 \<Longrightarrow> (\<Sum>i = 0..n. f i) = f n + (\<Sum>i = 0..n - Suc 0. f i)"
-  using atLeastAtMostSuc_conv [of 0 "n - 1"]
-  by auto
+lemma setsum_last_plus: fixes n::nat shows "m <= n \<Longrightarrow> (\<Sum>i = m..n. f i) = f n + (\<Sum>i = m..<n. f i)"
+  by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost add_commute)
+
+lemma setsum_Suc_diff:
+  fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
+  assumes "m \<le> Suc n"
+  shows "(\<Sum>i = m..n. f(Suc i) - f i) = f (Suc n) - f m"
+using assms by (induct n) (auto simp: le_Suc_eq)
 
 lemma nested_setsum_swap:
      "(\<Sum>i = 0..n. (\<Sum>j = 0..<i. a i j)) = (\<Sum>j = 0..<n. \<Sum>i = Suc j..n. a i j)"
@@ -1486,6 +1491,12 @@
 apply (cases "finite A")
   by (induction A rule: finite_induct) auto
 
+lemma setsum_zero_power' [simp]:
+  fixes c :: "nat \<Rightarrow> 'a::field"
+  shows "(\<Sum>i\<in>A. c i * 0^i / d i) = (if finite A \<and> 0 \<in> A then c 0 / d 0 else 0)"
+  using setsum_zero_power [of "\<lambda>i. c i / d i" A]
+  by auto
+
 
 subsection {* The formula for geometric sums *}