New material, mostly about limits. Consolidation.

--- a/src/HOL/Binomial.thy	Mon Apr 20 13:46:36 2015 +0100
+++ b/src/HOL/Binomial.thy	Tue Apr 21 17:19:00 2015 +0100
@@ -201,6 +201,13 @@
    apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0)
   done
 
+lemma binomial_le_pow2: "n choose k \<le> 2^n"
+  apply (induction n arbitrary: k)
+  apply (simp add: binomial.simps)
+  apply (case_tac k)
+  apply (auto simp: power_Suc)
+  by (simp add: add_le_mono mult_2)
+
 text{*The absorption property*}
 lemma Suc_times_binomial:
   "Suc k * (Suc n choose Suc k) = Suc n * (n choose k)"
@@ -701,6 +708,16 @@
   shows "0 < k \<Longrightarrow> a gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)"
   by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc)
 
+lemma gchoose_row_sum_weighted:
+  fixes r :: "'a::field_char_0"
+  shows "(\<Sum>k = 0..m. (r gchoose k) * (r/2 - of_nat k)) = of_nat(Suc m) / 2 * (r gchoose (Suc m))"
+proof (induct m)
+  case 0 show ?case by simp
+next
+  case (Suc m)
+  from Suc show ?case
+    by (simp add: algebra_simps distrib gbinomial_mult_1)
+qed
 
 lemma binomial_symmetric:
   assumes kn: "k \<le> n"

--- a/src/HOL/Library/BigO.thy	Mon Apr 20 13:46:36 2015 +0100
+++ b/src/HOL/Library/BigO.thy	Tue Apr 21 17:19:00 2015 +0100
@@ -870,7 +870,7 @@
   apply (drule bigo_LIMSEQ1)
   apply assumption
   apply (simp only: fun_diff_def)
-  apply (erule LIMSEQ_diff_approach_zero2)
+  apply (erule Lim_transform)
   apply assumption
   done
 

--- a/src/HOL/Library/Library.thy	Mon Apr 20 13:46:36 2015 +0100
+++ b/src/HOL/Library/Library.thy	Tue Apr 21 17:19:00 2015 +0100
@@ -44,7 +44,6 @@
   More_List
   Multiset_Order
   Numeral_Type
-  NthRoot_Limits
   OptionalSugar
   Option_ord
   Order_Continuity

--- a/src/HOL/Library/NthRoot_Limits.thy	Mon Apr 20 13:46:36 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,88 +0,0 @@
-theory NthRoot_Limits
-  imports Complex_Main
-begin
-
-lemma LIMSEQ_root: "(\<lambda>n. root n n) ----> 1"
-proof -
-  def x \<equiv> "\<lambda>n. root n n - 1"
-  have "x ----> sqrt 0"
-  proof (rule tendsto_sandwich[OF _ _ tendsto_const])
-    show "(\<lambda>x. sqrt (2 / x)) ----> sqrt 0"
-      by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
-         (simp_all add: at_infinity_eq_at_top_bot)
-    { fix n :: nat assume "2 < n"
-      have "1 + (real (n - 1) * n) / 2 * x n^2 = 1 + of_nat (n choose 2) * x n^2"
-        using `2 < n` unfolding gbinomial_def binomial_gbinomial
-        by (simp add: atLeast0AtMost atMost_Suc field_simps real_of_nat_diff numeral_2_eq_2 real_eq_of_nat[symmetric])
-      also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)"
-        by (simp add: x_def)
-      also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
-        using `2 < n` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
-      also have "\<dots> = (x n + 1) ^ n"
-        by (simp add: binomial_ring)
-      also have "\<dots> = n"
-        using `2 < n` by (simp add: x_def)
-      finally have "real (n - 1) * (real n / 2 * (x n)\<^sup>2) \<le> real (n - 1) * 1"
-        by simp
-      then have "(x n)\<^sup>2 \<le> 2 / real n"
-        using `2 < n` unfolding mult_le_cancel_left by (simp add: field_simps)
-      from real_sqrt_le_mono[OF this] have "x n \<le> sqrt (2 / real n)"
-        by simp }
-    then show "eventually (\<lambda>n. x n \<le> sqrt (2 / real n)) sequentially"
-      by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
-    show "eventually (\<lambda>n. sqrt 0 \<le> x n) sequentially"
-      by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def)
-  qed
-  from tendsto_add[OF this tendsto_const[of 1]] show ?thesis
-    by (simp add: x_def)
-qed
-
-lemma LIMSEQ_root_const:
-  assumes "0 < c"
-  shows "(\<lambda>n. root n c) ----> 1"
-proof -
-  { fix c :: real assume "1 \<le> c"
-    def x \<equiv> "\<lambda>n. root n c - 1"
-    have "x ----> 0"
-    proof (rule tendsto_sandwich[OF _ _ tendsto_const])
-      show "(\<lambda>n. c / n) ----> 0"
-        by (intro tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
-           (simp_all add: at_infinity_eq_at_top_bot)
-      { fix n :: nat assume "1 < n"
-        have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1"
-          using `1 < n` unfolding gbinomial_def binomial_gbinomial by (simp add: real_eq_of_nat[symmetric])
-        also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)"
-          by (simp add: x_def)
-        also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
-          using `1 < n` `1 \<le> c` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
-        also have "\<dots> = (x n + 1) ^ n"
-          by (simp add: binomial_ring)
-        also have "\<dots> = c"
-          using `1 < n` `1 \<le> c` by (simp add: x_def)
-        finally have "x n \<le> c / n"
-          using `1 \<le> c` `1 < n` by (simp add: field_simps) }
-      then show "eventually (\<lambda>n. x n \<le> c / n) sequentially"
-        by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
-      show "eventually (\<lambda>n. 0 \<le> x n) sequentially"
-        using `1 \<le> c` by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def)
-    qed
-    from tendsto_add[OF this tendsto_const[of 1]] have "(\<lambda>n. root n c) ----> 1"
-      by (simp add: x_def) }
-  note ge_1 = this
-
-  show ?thesis
-  proof cases
-    assume "1 \<le> c" with ge_1 show ?thesis by blast
-  next
-    assume "\<not> 1 \<le> c"
-    with `0 < c` have "1 \<le> 1 / c"
-      by simp
-    then have "(\<lambda>n. 1 / root n (1 / c)) ----> 1 / 1"
-      by (intro tendsto_divide tendsto_const ge_1 `1 \<le> 1 / c` one_neq_zero)
-    then show ?thesis
-      by (rule filterlim_cong[THEN iffD1, rotated 3])
-         (auto intro!: exI[of _ 1] simp: eventually_sequentially real_root_divide)
-  qed
-qed
-
-end

--- a/src/HOL/Limits.thy	Mon Apr 20 13:46:36 2015 +0100
+++ b/src/HOL/Limits.thy	Tue Apr 21 17:19:00 2015 +0100
@@ -396,7 +396,7 @@
 lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F"
   by (simp only: tendsto_iff Zfun_def dist_norm)
 
-lemma tendsto_0_le: "\<lbrakk>(f ---> 0) F; eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F\<rbrakk> 
+lemma tendsto_0_le: "\<lbrakk>(f ---> 0) F; eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F\<rbrakk>
                      \<Longrightarrow> (g ---> 0) F"
   by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff)
 
@@ -1134,7 +1134,7 @@
 
 *}
 
-lemma filterlim_tendsto_pos_mult_at_top: 
+lemma filterlim_tendsto_pos_mult_at_top:
   assumes f: "(f ---> c) F" and c: "0 < c"
   assumes g: "LIM x F. g x :> at_top"
   shows "LIM x F. (f x * g x :: real) :> at_top"
@@ -1156,7 +1156,7 @@
   qed
 qed
 
-lemma filterlim_at_top_mult_at_top: 
+lemma filterlim_at_top_mult_at_top:
   assumes f: "LIM x F. f x :> at_top"
   assumes g: "LIM x F. g x :> at_top"
   shows "LIM x F. (f x * g x :: real) :> at_top"
@@ -1202,7 +1202,7 @@
   shows "0 < n \<Longrightarrow> LIM x F. f x :> at_bot \<Longrightarrow> odd n \<Longrightarrow> LIM x F. (f x)^n :> at_bot"
   using filterlim_pow_at_top[of n "\<lambda>x. - f x" F] by (simp add: filterlim_uminus_at_bot)
 
-lemma filterlim_tendsto_add_at_top: 
+lemma filterlim_tendsto_add_at_top:
   assumes f: "(f ---> c) F"
   assumes g: "LIM x F. g x :> at_top"
   shows "LIM x F. (f x + g x :: real) :> at_top"
@@ -1225,7 +1225,7 @@
   unfolding divide_inverse
   by (rule filterlim_tendsto_pos_mult_at_top[OF f]) (rule filterlim_inverse_at_top[OF g])
 
-lemma filterlim_at_top_add_at_top: 
+lemma filterlim_at_top_add_at_top:
   assumes f: "LIM x F. f x :> at_top"
   assumes g: "LIM x F. g x :> at_top"
   shows "LIM x F. (f x + g x :: real) :> at_top"
@@ -1315,16 +1315,108 @@
   shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
   by (rule Bfun_inverse)
 
-lemma LIMSEQ_diff_approach_zero:
-  fixes L :: "'a::real_normed_vector"
-  shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
-  by (drule (1) tendsto_add, simp)
+text{* Transformation of limit. *}
+
+lemma eventually_at2:
+  "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
+  unfolding eventually_at dist_nz by auto
+
+lemma Lim_transform:
+  fixes a b :: "'a::real_normed_vector"
+  shows "\<lbrakk>(g ---> a) F; ((\<lambda>x. f x - g x) ---> 0) F\<rbrakk> \<Longrightarrow> (f ---> a) F"
+  using tendsto_add [of g a F "\<lambda>x. f x - g x" 0] by simp
+
+lemma Lim_transform2:
+  fixes a b :: "'a::real_normed_vector"
+  shows "\<lbrakk>(f ---> a) F; ((\<lambda>x. f x - g x) ---> 0) F\<rbrakk> \<Longrightarrow> (g ---> a) F"
+  by (erule Lim_transform) (simp add: tendsto_minus_cancel)
+
+lemma Lim_transform_eventually:
+  "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net \<Longrightarrow> (g ---> l) net"
+  apply (rule topological_tendstoI)
+  apply (drule (2) topological_tendstoD)
+  apply (erule (1) eventually_elim2, simp)
+  done
+
+lemma Lim_transform_within:
+  assumes "0 < d"
+    and "\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
+    and "(f ---> l) (at x within S)"
+  shows "(g ---> l) (at x within S)"
+proof (rule Lim_transform_eventually)
+  show "eventually (\<lambda>x. f x = g x) (at x within S)"
+    using assms(1,2) by (auto simp: dist_nz eventually_at)
+  show "(f ---> l) (at x within S)" by fact
+qed
+
+lemma Lim_transform_at:
+  assumes "0 < d"
+    and "\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
+    and "(f ---> l) (at x)"
+  shows "(g ---> l) (at x)"
+  using _ assms(3)
+proof (rule Lim_transform_eventually)
+  show "eventually (\<lambda>x. f x = g x) (at x)"
+    unfolding eventually_at2
+    using assms(1,2) by auto
+qed
+
+text{* Common case assuming being away from some crucial point like 0. *}
 
-lemma LIMSEQ_diff_approach_zero2:
-  fixes L :: "'a::real_normed_vector"
-  shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L"
-  by (drule (1) tendsto_diff, simp)
+lemma Lim_transform_away_within:
+  fixes a b :: "'a::t1_space"
+  assumes "a \<noteq> b"
+    and "\<forall>x\<in>S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
+    and "(f ---> l) (at a within S)"
+  shows "(g ---> l) (at a within S)"
+proof (rule Lim_transform_eventually)
+  show "(f ---> l) (at a within S)" by fact
+  show "eventually (\<lambda>x. f x = g x) (at a within S)"
+    unfolding eventually_at_topological
+    by (rule exI [where x="- {b}"], simp add: open_Compl assms)
+qed
+
+lemma Lim_transform_away_at:
+  fixes a b :: "'a::t1_space"
+  assumes ab: "a\<noteq>b"
+    and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
+    and fl: "(f ---> l) (at a)"
+  shows "(g ---> l) (at a)"
+  using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl by simp
+
+text{* Alternatively, within an open set. *}
 
+lemma Lim_transform_within_open:
+  assumes "open S" and "a \<in> S"
+    and "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"
+    and "(f ---> l) (at a)"
+  shows "(g ---> l) (at a)"
+proof (rule Lim_transform_eventually)
+  show "eventually (\<lambda>x. f x = g x) (at a)"
+    unfolding eventually_at_topological
+    using assms(1,2,3) by auto
+  show "(f ---> l) (at a)" by fact
+qed
+
+text{* A congruence rule allowing us to transform limits assuming not at point. *}
+
+(* FIXME: Only one congruence rule for tendsto can be used at a time! *)
+
+lemma Lim_cong_within(*[cong add]*):
+  assumes "a = b"
+    and "x = y"
+    and "S = T"
+    and "\<And>x. x \<noteq> b \<Longrightarrow> x \<in> T \<Longrightarrow> f x = g x"
+  shows "(f ---> x) (at a within S) \<longleftrightarrow> (g ---> y) (at b within T)"
+  unfolding tendsto_def eventually_at_topological
+  using assms by simp
+
+lemma Lim_cong_at(*[cong add]*):
+  assumes "a = b" "x = y"
+    and "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
+  shows "((\<lambda>x. f x) ---> x) (at a) \<longleftrightarrow> ((g ---> y) (at a))"
+  unfolding tendsto_def eventually_at_topological
+  using assms by simp
 text{*An unbounded sequence's inverse tends to 0*}
 
 lemma LIMSEQ_inverse_zero:
@@ -1684,7 +1776,7 @@
   "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
   by (fact continuous)
 
-lemmas isCont_scaleR [simp] = 
+lemmas isCont_scaleR [simp] =
   bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
 
 lemmas isCont_of_real [simp] =
@@ -1740,7 +1832,7 @@
 lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
 by (rule isUCont [THEN isUCont_Cauchy])
 
-lemma LIM_less_bound: 
+lemma LIM_less_bound:
   fixes f :: "real \<Rightarrow> real"
   assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
   shows "0 \<le> f x"
@@ -1804,7 +1896,7 @@
 
   show "P a b"
   proof (rule ccontr)
-    assume "\<not> P a b" 
+    assume "\<not> P a b"
     { fix n have "\<not> P (l n) (u n)"
       proof (induct n)
         case (Suc n) with trans[of "l n" "(l n + u n) / 2" "u n"] show ?case by auto
@@ -1911,7 +2003,7 @@
 lemma isCont_Lb_Ub:
   fixes f :: "real \<Rightarrow> real"
   assumes "a \<le> b" "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
-  shows "\<exists>L M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> L \<le> f x \<and> f x \<le> M) \<and> 
+  shows "\<exists>L M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> L \<le> f x \<and> f x \<le> M) \<and>
                (\<forall>y. L \<le> y \<and> y \<le> M \<longrightarrow> (\<exists>x. a \<le> x \<and> x \<le> b \<and> (f x = y)))"
 proof -
   obtain M where M: "a \<le> M" "M \<le> b" "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> f M"
@@ -1974,8 +2066,8 @@
 
 lemma isCont_inv_fun:
   fixes f g :: "real \<Rightarrow> real"
-  shows "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
-         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
+  shows "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;
+         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]
       ==> isCont g (f x)"
 by (rule isCont_inverse_function)
 

--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Apr 20 13:46:36 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Apr 21 17:19:00 2015 +0100
@@ -1263,9 +1263,6 @@
 
 subsection{*Complex Powers*}
 
-lemma powr_0 [simp]: "0 powr z = 0"
-  by (simp add: powr_def)
-
 lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
   by (simp add: powr_def)
 
@@ -1526,7 +1523,7 @@
 proof -
   have nz0: "1 + \<i>*z \<noteq> 0"
     using assms
-    by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2) 
+    by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2)
               less_irrefl minus_diff_eq mult.right_neutral right_minus_eq)
   have "z \<noteq> -\<i>" using assms
     by auto
@@ -1771,7 +1768,7 @@
   by (blast intro: isCont_o2 [OF _ isCont_Arcsin])
 
 lemma sin_Arcsin [simp]: "sin(Arcsin z) = z"
-proof -  
+proof -
   have "\<i>*z*2 + csqrt (1 - z\<^sup>2)*2 = 0 \<longleftrightarrow> (\<i>*z)*2 + csqrt (1 - z\<^sup>2)*2 = 0"
     by (simp add: algebra_simps)  --{*Cancelling a factor of 2*}
   moreover have "... \<longleftrightarrow> (\<i>*z) + csqrt (1 - z\<^sup>2) = 0"
@@ -1903,7 +1900,7 @@
 proof (cases "Im z = 0")
   case True
   then show ?thesis
-    using assms 
+    using assms
     by (fastforce simp add: cmod_def Re_power2 Im_power2 algebra_simps abs_square_less_1 [symmetric])
 next
   case False

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 20 13:46:36 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Apr 21 17:19:00 2015 +0100
@@ -705,7 +705,7 @@
     apply (clarsimp simp add: less_diff_eq)
     by (metis dist_commute dist_triangle_lt)
   assume ?rhs then have 2: "S = U \<inter> T"
-    unfolding T_def 
+    unfolding T_def
     by auto (metis dist_self)
   from 1 2 show ?lhs
     unfolding openin_open open_dist by fast
@@ -1750,10 +1750,6 @@
 
 text {* Some property holds "sufficiently close" to the limit point. *}
 
-lemma eventually_at2:
-  "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
-  unfolding eventually_at dist_nz by auto
-
 lemma eventually_happens: "eventually P net \<Longrightarrow> trivial_limit net \<or> (\<exists>x. P x)"
   unfolding trivial_limit_def
   by (auto elim: eventually_rev_mp)
@@ -2051,100 +2047,6 @@
   shows "netlimit (at x within S) = x"
   using assms by (metis at_within_interior netlimit_at)
 
-text{* Transformation of limit. *}
-
-lemma Lim_transform:
-  fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
-  assumes "((\<lambda>x. f x - g x) ---> 0) net" "(f ---> l) net"
-  shows "(g ---> l) net"
-  using tendsto_diff [OF assms(2) assms(1)] by simp
-
-lemma Lim_transform_eventually:
-  "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net \<Longrightarrow> (g ---> l) net"
-  apply (rule topological_tendstoI)
-  apply (drule (2) topological_tendstoD)
-  apply (erule (1) eventually_elim2, simp)
-  done
-
-lemma Lim_transform_within:
-  assumes "0 < d"
-    and "\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
-    and "(f ---> l) (at x within S)"
-  shows "(g ---> l) (at x within S)"
-proof (rule Lim_transform_eventually)
-  show "eventually (\<lambda>x. f x = g x) (at x within S)"
-    using assms(1,2) by (auto simp: dist_nz eventually_at)
-  show "(f ---> l) (at x within S)" by fact
-qed
-
-lemma Lim_transform_at:
-  assumes "0 < d"
-    and "\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
-    and "(f ---> l) (at x)"
-  shows "(g ---> l) (at x)"
-  using _ assms(3)
-proof (rule Lim_transform_eventually)
-  show "eventually (\<lambda>x. f x = g x) (at x)"
-    unfolding eventually_at2
-    using assms(1,2) by auto
-qed
-
-text{* Common case assuming being away from some crucial point like 0. *}
-
-lemma Lim_transform_away_within:
-  fixes a b :: "'a::t1_space"
-  assumes "a \<noteq> b"
-    and "\<forall>x\<in>S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
-    and "(f ---> l) (at a within S)"
-  shows "(g ---> l) (at a within S)"
-proof (rule Lim_transform_eventually)
-  show "(f ---> l) (at a within S)" by fact
-  show "eventually (\<lambda>x. f x = g x) (at a within S)"
-    unfolding eventually_at_topological
-    by (rule exI [where x="- {b}"], simp add: open_Compl assms)
-qed
-
-lemma Lim_transform_away_at:
-  fixes a b :: "'a::t1_space"
-  assumes ab: "a\<noteq>b"
-    and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
-    and fl: "(f ---> l) (at a)"
-  shows "(g ---> l) (at a)"
-  using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl by simp
-
-text{* Alternatively, within an open set. *}
-
-lemma Lim_transform_within_open:
-  assumes "open S" and "a \<in> S"
-    and "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"
-    and "(f ---> l) (at a)"
-  shows "(g ---> l) (at a)"
-proof (rule Lim_transform_eventually)
-  show "eventually (\<lambda>x. f x = g x) (at a)"
-    unfolding eventually_at_topological
-    using assms(1,2,3) by auto
-  show "(f ---> l) (at a)" by fact
-qed
-
-text{* A congruence rule allowing us to transform limits assuming not at point. *}
-
-(* FIXME: Only one congruence rule for tendsto can be used at a time! *)
-
-lemma Lim_cong_within(*[cong add]*):
-  assumes "a = b"
-    and "x = y"
-    and "S = T"
-    and "\<And>x. x \<noteq> b \<Longrightarrow> x \<in> T \<Longrightarrow> f x = g x"
-  shows "(f ---> x) (at a within S) \<longleftrightarrow> (g ---> y) (at b within T)"
-  unfolding tendsto_def eventually_at_topological
-  using assms by simp
-
-lemma Lim_cong_at(*[cong add]*):
-  assumes "a = b" "x = y"
-    and "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
-  shows "((\<lambda>x. f x) ---> x) (at a) \<longleftrightarrow> ((g ---> y) (at a))"
-  unfolding tendsto_def eventually_at_topological
-  using assms by simp
 
 text{* Useful lemmas on closure and set of possible sequential limits.*}
 

--- a/src/HOL/NthRoot.thy	Mon Apr 20 13:46:36 2015 +0100
+++ b/src/HOL/NthRoot.thy	Tue Apr 21 17:19:00 2015 +0100
@@ -7,7 +7,7 @@
 section {* Nth Roots of Real Numbers *}
 
 theory NthRoot
-imports Deriv
+imports Deriv Binomial
 begin
 
 lemma abs_sgn_eq: "abs (sgn x :: real) = (if x = 0 then 0 else 1)"
@@ -644,6 +644,90 @@
   apply auto 
   done
   
+lemma LIMSEQ_root: "(\<lambda>n. root n n) ----> 1"
+proof -
+  def x \<equiv> "\<lambda>n. root n n - 1"
+  have "x ----> sqrt 0"
+  proof (rule tendsto_sandwich[OF _ _ tendsto_const])
+    show "(\<lambda>x. sqrt (2 / x)) ----> sqrt 0"
+      by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
+         (simp_all add: at_infinity_eq_at_top_bot)
+    { fix n :: nat assume "2 < n"
+      have "1 + (real (n - 1) * n) / 2 * x n^2 = 1 + of_nat (n choose 2) * x n^2"
+        using `2 < n` unfolding gbinomial_def binomial_gbinomial
+        by (simp add: atLeast0AtMost atMost_Suc field_simps real_of_nat_diff numeral_2_eq_2 real_eq_of_nat[symmetric])
+      also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)"
+        by (simp add: x_def)
+      also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
+        using `2 < n` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
+      also have "\<dots> = (x n + 1) ^ n"
+        by (simp add: binomial_ring)
+      also have "\<dots> = n"
+        using `2 < n` by (simp add: x_def)
+      finally have "real (n - 1) * (real n / 2 * (x n)\<^sup>2) \<le> real (n - 1) * 1"
+        by simp
+      then have "(x n)\<^sup>2 \<le> 2 / real n"
+        using `2 < n` unfolding mult_le_cancel_left by (simp add: field_simps)
+      from real_sqrt_le_mono[OF this] have "x n \<le> sqrt (2 / real n)"
+        by simp }
+    then show "eventually (\<lambda>n. x n \<le> sqrt (2 / real n)) sequentially"
+      by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
+    show "eventually (\<lambda>n. sqrt 0 \<le> x n) sequentially"
+      by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def)
+  qed
+  from tendsto_add[OF this tendsto_const[of 1]] show ?thesis
+    by (simp add: x_def)
+qed
+
+lemma LIMSEQ_root_const:
+  assumes "0 < c"
+  shows "(\<lambda>n. root n c) ----> 1"
+proof -
+  { fix c :: real assume "1 \<le> c"
+    def x \<equiv> "\<lambda>n. root n c - 1"
+    have "x ----> 0"
+    proof (rule tendsto_sandwich[OF _ _ tendsto_const])
+      show "(\<lambda>n. c / n) ----> 0"
+        by (intro tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
+           (simp_all add: at_infinity_eq_at_top_bot)
+      { fix n :: nat assume "1 < n"
+        have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1"
+          using `1 < n` unfolding gbinomial_def binomial_gbinomial by (simp add: real_eq_of_nat[symmetric])
+        also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)"
+          by (simp add: x_def)
+        also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
+          using `1 < n` `1 \<le> c` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
+        also have "\<dots> = (x n + 1) ^ n"
+          by (simp add: binomial_ring)
+        also have "\<dots> = c"
+          using `1 < n` `1 \<le> c` by (simp add: x_def)
+        finally have "x n \<le> c / n"
+          using `1 \<le> c` `1 < n` by (simp add: field_simps) }
+      then show "eventually (\<lambda>n. x n \<le> c / n) sequentially"
+        by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
+      show "eventually (\<lambda>n. 0 \<le> x n) sequentially"
+        using `1 \<le> c` by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def)
+    qed
+    from tendsto_add[OF this tendsto_const[of 1]] have "(\<lambda>n. root n c) ----> 1"
+      by (simp add: x_def) }
+  note ge_1 = this
+
+  show ?thesis
+  proof cases
+    assume "1 \<le> c" with ge_1 show ?thesis by blast
+  next
+    assume "\<not> 1 \<le> c"
+    with `0 < c` have "1 \<le> 1 / c"
+      by simp
+    then have "(\<lambda>n. 1 / root n (1 / c)) ----> 1 / 1"
+      by (intro tendsto_divide tendsto_const ge_1 `1 \<le> 1 / c` one_neq_zero)
+    then show ?thesis
+      by (rule filterlim_cong[THEN iffD1, rotated 3])
+         (auto intro!: exI[of _ 1] simp: eventually_sequentially real_root_divide)
+  qed
+qed
+
+
 text "Legacy theorem names:"
 lemmas real_root_pos2 = real_root_power_cancel
 lemmas real_root_pos_pos = real_root_gt_zero [THEN order_less_imp_le]

--- a/src/HOL/Number_Theory/Fib.thy	Mon Apr 20 13:46:36 2015 +0100
+++ b/src/HOL/Number_Theory/Fib.thy	Tue Apr 21 17:19:00 2015 +0100
@@ -11,11 +11,11 @@
 section {* Fib *}
 
 theory Fib
-imports Main "../GCD"
+imports Main "../GCD" "../Binomial"
 begin
 
 
-subsection {* Main definitions *}
+subsection {* Fibonacci numbers *}
 
 fun fib :: "nat \<Rightarrow> nat"
 where
@@ -23,7 +23,7 @@
   | fib1: "fib (Suc 0) = 1"
   | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
 
-subsection {* Fibonacci numbers *}
+subsection {* Basic Properties *}
 
 lemma fib_1 [simp]: "fib (1::nat) = 1"
   by (metis One_nat_def fib1)
@@ -41,6 +41,8 @@
 lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
   by (induct n rule: fib.induct) (auto simp add: )
 
+subsection {* A Few Elementary Results *}
+
 text {*
   \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
   much easier using integers, not natural numbers!
@@ -55,7 +57,7 @@
 using fib_Cassini_int [of n] by auto
 
 
-text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
+subsection {* Law 6.111 of Concrete Mathematics *}
 
 lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
   apply (induct n rule: fib.induct)
@@ -67,9 +69,7 @@
   apply (simp add: gcd_commute_nat [of "fib m"])
   apply (cases m)
   apply (auto simp add: fib_add)
-  apply (subst gcd_commute_nat)
-  apply (subst mult.commute)
-  apply (metis coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
+  apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
   done
 
 lemma gcd_fib_diff: "m \<le> n \<Longrightarrow>
@@ -109,5 +109,35 @@
     "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
   by (induct n rule: nat.induct) (auto simp add:  field_simps)
 
+subsection {* Fibonacci and Binomial Coefficients *}
+
+lemma setsum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)"
+  by (induct n) auto
+
+lemma setsum_choose_drop_zero:
+    "(\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k) choose (k - 1)) = (\<Sum>j = 0..n. (n-j) choose j)"
+  by (rule trans [OF setsum.cong setsum_drop_zero]) auto
+
+lemma ne_diagonal_fib:
+   "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
+proof (induct n rule: fib.induct)
+  case 1 show ?case by simp
+next
+  case 2 show ?case by simp
+next
+  case (3 n)
+  have "(\<Sum>k = 0..Suc n. Suc (Suc n) - k choose k) =
+        (\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k=0 then 0 else (Suc n - k choose (k - 1))))"
+    by (rule setsum.cong) (simp_all add: choose_reduce_nat)
+  also have "... = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
+                   (\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"
+    by (simp add: setsum.distrib)
+  also have "... = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
+                   (\<Sum>j = 0..n. n - j choose j)"
+    by (metis setsum_choose_drop_zero)
+  finally show ?case using 3
+    by simp
+qed
+
 end
 

--- a/src/HOL/Probability/Measure_Space.thy	Mon Apr 20 13:46:36 2015 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Tue Apr 21 17:19:00 2015 +0100
@@ -389,7 +389,7 @@
   ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
     by (simp add: zero_ereal_def)
   then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
-    by (rule LIMSEQ_diff_approach_zero2[OF tendsto_const])
+    by (rule Lim_transform[OF tendsto_const])
   then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
     using A by (subst (1 2) f') auto
 qed

--- a/src/HOL/Series.thy	Mon Apr 20 13:46:36 2015 +0100
+++ b/src/HOL/Series.thy	Tue Apr 21 17:19:00 2015 +0100
@@ -643,7 +643,7 @@
     by (simp only: setsum_diff finite_S1 S2_le_S1)
 
   with 1 have "(\<lambda>n. setsum ?g (?S2 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
-    by (rule LIMSEQ_diff_approach_zero2)
+    by (rule Lim_transform2)
   thus ?thesis by (simp only: sums_def setsum_triangle_reindex)
 qed
 

--- a/src/HOL/Transcendental.thy	Mon Apr 20 13:46:36 2015 +0100
+++ b/src/HOL/Transcendental.thy	Tue Apr 21 17:19:00 2015 +0100
@@ -104,7 +104,22 @@
   shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^i)"
 by (metis one_diff_power_eq' [of n x] nat_diff_setsum_reindex)
 
-text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
+lemma powser_zero:
+  fixes f :: "nat \<Rightarrow> 'a::real_normed_algebra_1"
+  shows "(\<Sum>n. f n * 0 ^ n) = f 0"
+proof -
+  have "(\<Sum>n<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
+    by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left)
+  thus ?thesis unfolding One_nat_def by simp
+qed
+
+lemma powser_sums_zero:
+  fixes a :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
+  shows "(\<lambda>n. a n * 0^n) sums a 0"
+    using sums_finite [of "{0}" "\<lambda>n. a n * 0 ^ n"]
+    by simp
+
+text{*Power series has a circle or radius of convergence: if it sums for @{term
   x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
 
 lemma powser_insidea:
@@ -167,6 +182,46 @@
       summable (\<lambda>n. f n * (z ^ n))"
   by (rule powser_insidea [THEN summable_norm_cancel])
 
+lemma powser_times_n_limit_0:
+  fixes x :: "'a::{real_normed_div_algebra,banach}"
+  assumes "norm x < 1"
+    shows "(\<lambda>n. of_nat n * x ^ n) ----> 0"
+proof -
+  have "norm x / (1 - norm x) \<ge> 0"
+    using assms
+    by (auto simp: divide_simps)
+  moreover obtain N where N: "norm x / (1 - norm x) < of_int N"
+    using ex_le_of_int
+    by (meson ex_less_of_int)
+  ultimately have N0: "N>0" 
+    by auto
+  then have *: "real (N + 1) * norm x / real N < 1"
+    using N assms
+    by (auto simp: field_simps)
+  { fix n::nat
+    assume "N \<le> int n"
+    then have "real N * real_of_nat (Suc n) \<le> real_of_nat n * real (1 + N)"
+      by (simp add: algebra_simps)
+    then have "(real N * real_of_nat (Suc n)) * (norm x * norm (x ^ n))
+               \<le> (real_of_nat n * real (1 + N)) * (norm x * norm (x ^ n))"
+      using N0 mult_mono by fastforce
+    then have "real N * (norm x * (real_of_nat (Suc n) * norm (x ^ n)))
+         \<le> real_of_nat n * (norm x * (real (1 + N) * norm (x ^ n)))"
+      by (simp add: algebra_simps)
+  } note ** = this
+  show ?thesis using *
+    apply (rule summable_LIMSEQ_zero [OF summable_ratio_test, where N1="nat N"])
+    apply (simp add: N0 norm_mult nat_le_iff field_simps power_Suc ** 
+                del: of_nat_Suc real_of_int_add)
+    done
+qed
+
+corollary lim_n_over_pown:
+  fixes x :: "'a::{real_normed_field,banach}"
+  shows "1 < norm x \<Longrightarrow> ((\<lambda>n. of_nat n / x^n) ---> 0) sequentially"
+using powser_times_n_limit_0 [of "inverse x"]
+by (simp add: norm_divide divide_simps)
+
 lemma sum_split_even_odd:
   fixes f :: "nat \<Rightarrow> real"
   shows
@@ -683,6 +738,132 @@
   qed
 qed
 
+subsection {* The Derivative of a Power Series Has the Same Radius of Convergence *}
+
+lemma termdiff_converges:
+  fixes x :: "'a::{real_normed_field,banach}"
+  assumes K: "norm x < K"
+      and sm: "\<And>x. norm x < K \<Longrightarrow> summable(\<lambda>n. c n * x ^ n)"
+    shows "summable (\<lambda>n. diffs c n * x ^ n)"
+proof (cases "x = 0")
+  case True then show ?thesis
+  using powser_sums_zero sums_summable by auto
+next
+  case False
+  then have "K>0"
+    using K less_trans zero_less_norm_iff by blast
+  then obtain r::real where r: "norm x < norm r" "norm r < K" "r>0"
+    using K False
+    by (auto simp: abs_less_iff add_pos_pos intro: that [of "(norm x + K) / 2"])
+  have "(\<lambda>n. of_nat n * (x / of_real r) ^ n) ----> 0"
+    using r by (simp add: norm_divide powser_times_n_limit_0 [of "x / of_real r"])
+  then obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> real_of_nat n * norm x ^ n < r ^ n"
+    using r unfolding LIMSEQ_iff
+    apply (drule_tac x=1 in spec)
+    apply (auto simp: norm_divide norm_mult norm_power field_simps)
+    done
+  have "summable (\<lambda>n. (of_nat n * c n) * x ^ n)"
+    apply (rule summable_comparison_test' [of "\<lambda>n. norm(c n * (of_real r) ^ n)" N])
+    apply (rule powser_insidea [OF sm [of "of_real ((r+K)/2)"]])
+    using N r norm_of_real [of "r+K", where 'a = 'a]
+    apply (auto simp add: norm_divide norm_mult norm_power )
+    using less_eq_real_def by fastforce
+  then have "summable (\<lambda>n. (of_nat (Suc n) * c(Suc n)) * x ^ Suc n)"
+    using summable_iff_shift [of "\<lambda>n. of_nat n * c n * x ^ n" 1]
+    by simp
+  then have "summable (\<lambda>n. (of_nat (Suc n) * c(Suc n)) * x ^ n)"
+    using False summable_mult2 [of "\<lambda>n. (of_nat (Suc n) * c(Suc n) * x ^ n) * x" "inverse x"]
+    by (simp add: mult.assoc) (auto simp: power_Suc mult_ac)
+  then show ?thesis 
+    by (simp add: diffs_def)
+qed
+
+lemma termdiff_converges_all:
+  fixes x :: "'a::{real_normed_field,banach}"
+  assumes "\<And>x. summable (\<lambda>n. c n * x^n)"
+    shows "summable (\<lambda>n. diffs c n * x^n)"
+  apply (rule termdiff_converges [where K = "1 + norm x"])
+  using assms
+  apply (auto simp: )
+  done
+
+lemma termdiffs_strong:
+  fixes K x :: "'a::{real_normed_field,banach}"
+  assumes sm: "summable (\<lambda>n. c n * K ^ n)"
+      and K: "norm x < norm K"
+  shows "DERIV (\<lambda>x. \<Sum>n. c n * x^n) x :> (\<Sum>n. diffs c n * x^n)"
+proof -
+  have [simp]: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K"
+    using K
+    apply (auto simp: norm_divide)
+    apply (rule le_less_trans [of _ "of_real (norm K) + of_real (norm x)"])
+    apply (auto simp: mult_2_right norm_triangle_mono)
+    done
+  have "summable (\<lambda>n. c n * (of_real (norm x + norm K) / 2) ^ n)"
+    apply (rule summable_norm_cancel [OF powser_insidea [OF sm]])
+    using K
+    apply (auto simp: algebra_simps)
+    done
+  moreover have "\<And>x. norm x < norm K \<Longrightarrow> summable (\<lambda>n. diffs c n * x ^ n)"
+    by (blast intro: sm termdiff_converges powser_inside)
+  moreover have "\<And>x. norm x < norm K \<Longrightarrow> summable (\<lambda>n. diffs(diffs c) n * x ^ n)"
+    by (blast intro: sm termdiff_converges powser_inside)
+  ultimately show ?thesis
+    apply (rule termdiffs [where K = "of_real (norm x + norm K) / 2"])
+    apply (auto simp: algebra_simps)
+    using K
+    apply (simp add: norm_divide)
+    apply (rule less_le_trans [of _ "of_real (norm K) + of_real (norm x)"])
+    apply (simp_all add: of_real_add [symmetric] del: of_real_add)
+    done
+qed
+
+lemma powser_limit_0: 
+  fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"
+  assumes s: "0 < s"
+      and sm: "\<And>x. norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)"
+    shows "(f ---> a 0) (at 0)"
+proof -
+  have "summable (\<lambda>n. a n * (of_real s / 2) ^ n)"
+    apply (rule sums_summable [where l = "f (of_real s / 2)", OF sm])
+    using s
+    apply (auto simp: norm_divide)
+    done
+  then have "((\<lambda>x. \<Sum>n. a n * x ^ n) has_field_derivative (\<Sum>n. diffs a n * 0 ^ n)) (at 0)"
+    apply (rule termdiffs_strong)
+    using s
+    apply (auto simp: norm_divide)
+    done
+  then have "isCont (\<lambda>x. \<Sum>n. a n * x ^ n) 0"
+    by (blast intro: DERIV_continuous)
+  then have "((\<lambda>x. \<Sum>n. a n * x ^ n) ---> a 0) (at 0)"
+    by (simp add: continuous_within powser_zero)
+  then show ?thesis 
+    apply (rule Lim_transform)
+    apply (auto simp add: LIM_eq)
+    apply (rule_tac x="s" in exI)
+    using s 
+    apply (auto simp: sm [THEN sums_unique])
+    done
+qed
+
+lemma powser_limit_0_strong: 
+  fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"
+  assumes s: "0 < s"
+      and sm: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)"
+    shows "(f ---> a 0) (at 0)"
+proof -
+  have *: "((\<lambda>x. if x = 0 then a 0 else f x) ---> a 0) (at 0)"
+    apply (rule powser_limit_0 [OF s])
+    apply (case_tac "x=0")
+    apply (auto simp add: powser_sums_zero sm)
+    done
+  show ?thesis
+    apply (subst LIM_equal [where g = "(\<lambda>x. if x = 0 then a 0 else f x)"])
+    apply (simp_all add: *)
+    done
+qed
+
 
 subsection {* Derivability of power series *}
 
@@ -1045,15 +1226,6 @@
 
 subsubsection {* Properties of the Exponential Function *}
 
-lemma powser_zero:
-  fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1}"
-  shows "(\<Sum>n. f n * 0 ^ n) = f 0"
-proof -
-  have "(\<Sum>n<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
-    by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left)
-  thus ?thesis unfolding One_nat_def by simp
-qed
-
 lemma exp_zero [simp]: "exp 0 = 1"
   unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero)
 
@@ -1293,6 +1465,9 @@
   -- {*exponentation via ln and exp*}
   where  [code del]: "x powr a \<equiv> if x = 0 then 0 else exp(a * ln x)"
 
+lemma powr_0 [simp]: "0 powr z = 0"
+  by (simp add: powr_def)
+
 
 instantiation real :: ln
 begin
@@ -1791,6 +1966,11 @@
   fixes x::real shows "0 < x \<Longrightarrow> ln x \<le> x - 1"
   using exp_ge_add_one_self[of "ln x"] by simp
 
+corollary ln_diff_le: 
+  fixes x::real 
+  shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x - ln y \<le> (x - y) / y"
+  by (simp add: ln_div [symmetric] diff_divide_distrib ln_le_minus_one)
+
 lemma ln_eq_minus_one:
   fixes x::real 
   assumes "0 < x" "ln x = x - 1"
@@ -2272,25 +2452,27 @@
 using powr_mono by fastforce
 
 lemma powr_less_mono2:
-  fixes x::real shows "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a"
+  fixes x::real shows "0 < a ==> 0 \<le> x ==> x < y ==> x powr a < y powr a"
   by (simp add: powr_def)
 
-
 lemma powr_less_mono2_neg:
   fixes x::real shows "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a"
   by (simp add: powr_def)
 
 lemma powr_mono2:
-  fixes x::real shows "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
+  fixes x::real shows "0 <= a ==> 0 \<le> x ==> x <= y ==> x powr a <= y powr a"
   apply (case_tac "a = 0", simp)
   apply (case_tac "x = y", simp)
-  apply (metis less_eq_real_def powr_less_mono2)
+  apply (metis dual_order.strict_iff_order powr_less_mono2)
   done
 
 lemma powr_inj:
   fixes x::real shows "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
   unfolding powr_def exp_inj_iff by simp
 
+lemma powr_half_sqrt: "0 \<le> x \<Longrightarrow> x powr (1/2) = sqrt x"
+  by (simp add: powr_def root_powr_inverse sqrt_def)
+
 lemma ln_powr_bound:
   fixes x::real shows "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
 by (metis exp_gt_zero linear ln_eq_zero_iff ln_exp ln_less_self ln_powr mult.commute mult_imp_le_div_pos not_less powr_gt_zero)
@@ -2316,28 +2498,31 @@
   finally show ?thesis .
 qed
 
-lemma tendsto_powr [tendsto_intros]:  (*FIXME a mess, suggests a general rule about exceptions*)
+lemma tendsto_powr [tendsto_intros]: 
   fixes a::real 
-  shows "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
-  apply (simp add: powr_def)
-  apply (simp add: tendsto_def)
-  apply (simp add: eventually_conj_iff )
-  apply safe
-  apply (case_tac "0 \<in> S")
-  apply (auto simp: )
-  apply (subgoal_tac "\<exists>T. open T & a : T & 0 \<notin> T")
-  apply clarify
-  apply (drule_tac x="T" in spec)
-  apply (simp add: )
-  apply (metis (mono_tags, lifting) eventually_mono)
-  apply (simp add: separation_t1)
-  apply (subgoal_tac "((\<lambda>x. exp (g x * ln (f x))) ---> exp (b * ln a)) F")
-  apply (simp add: tendsto_def)
-  apply (metis (mono_tags, lifting) eventually_mono)
-  apply (simp add: tendsto_def [symmetric])
-  apply (intro tendsto_intros)
-  apply (auto simp: )
-  done
+  assumes f: "(f ---> a) F" and g: "(g ---> b) F" and a: "a \<noteq> 0"
+  shows "((\<lambda>x. f x powr g x) ---> a powr b) F"
+proof -
+  { fix S :: "real set"
+    obtain T where "open T" "a \<in> T" "0 \<notin> T"
+      using t1_space a by blast
+    then have "eventually (\<lambda>x. f x = 0 \<longrightarrow> 0 \<in> S) F"
+      using f
+      by (simp add: tendsto_def) (metis (mono_tags, lifting) eventually_mono)
+  }
+  moreover
+  { fix S :: "real set"
+    assume S: "open S" "exp (b * ln a) \<in> S"
+    then have "((\<lambda>x. exp (g x * ln (f x))) ---> exp (b * ln a)) F"
+    using f g a
+      by (intro tendsto_intros) auto
+    then have "eventually (\<lambda>x. f x \<noteq> 0 \<longrightarrow> exp (g x * ln (f x)) \<in> S) F"
+      using f S
+      by (simp add: tendsto_def) (metis (mono_tags, lifting) eventually_mono)
+  }
+  ultimately show ?thesis using assms
+    by (simp add: powr_def tendsto_def eventually_conj_iff)
+qed
 
 lemma continuous_powr:
   assumes "continuous F f"