New material, mostly about limits. Consolidation.
authorpaulson <lp15@cam.ac.uk>
Tue Apr 21 17:19:00 2015 +0100 (2015-04-21)
changeset 60141833adf7db7d8
parent 60140 a948ee5fb5f4
child 60142 3275dddf356f
child 60144 50eb4fdd5860
New material, mostly about limits. Consolidation.
src/HOL/Binomial.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Library.thy
src/HOL/Library/NthRoot_Limits.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NthRoot.thy
src/HOL/Number_Theory/Fib.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Series.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Binomial.thy	Mon Apr 20 13:46:36 2015 +0100
     1.2 +++ b/src/HOL/Binomial.thy	Tue Apr 21 17:19:00 2015 +0100
     1.3 @@ -201,6 +201,13 @@
     1.4     apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0)
     1.5    done
     1.6  
     1.7 +lemma binomial_le_pow2: "n choose k \<le> 2^n"
     1.8 +  apply (induction n arbitrary: k)
     1.9 +  apply (simp add: binomial.simps)
    1.10 +  apply (case_tac k)
    1.11 +  apply (auto simp: power_Suc)
    1.12 +  by (simp add: add_le_mono mult_2)
    1.13 +
    1.14  text{*The absorption property*}
    1.15  lemma Suc_times_binomial:
    1.16    "Suc k * (Suc n choose Suc k) = Suc n * (n choose k)"
    1.17 @@ -701,6 +708,16 @@
    1.18    shows "0 < k \<Longrightarrow> a gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)"
    1.19    by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc)
    1.20  
    1.21 +lemma gchoose_row_sum_weighted:
    1.22 +  fixes r :: "'a::field_char_0"
    1.23 +  shows "(\<Sum>k = 0..m. (r gchoose k) * (r/2 - of_nat k)) = of_nat(Suc m) / 2 * (r gchoose (Suc m))"
    1.24 +proof (induct m)
    1.25 +  case 0 show ?case by simp
    1.26 +next
    1.27 +  case (Suc m)
    1.28 +  from Suc show ?case
    1.29 +    by (simp add: algebra_simps distrib gbinomial_mult_1)
    1.30 +qed
    1.31  
    1.32  lemma binomial_symmetric:
    1.33    assumes kn: "k \<le> n"
     2.1 --- a/src/HOL/Library/BigO.thy	Mon Apr 20 13:46:36 2015 +0100
     2.2 +++ b/src/HOL/Library/BigO.thy	Tue Apr 21 17:19:00 2015 +0100
     2.3 @@ -870,7 +870,7 @@
     2.4    apply (drule bigo_LIMSEQ1)
     2.5    apply assumption
     2.6    apply (simp only: fun_diff_def)
     2.7 -  apply (erule LIMSEQ_diff_approach_zero2)
     2.8 +  apply (erule Lim_transform)
     2.9    apply assumption
    2.10    done
    2.11  
     3.1 --- a/src/HOL/Library/Library.thy	Mon Apr 20 13:46:36 2015 +0100
     3.2 +++ b/src/HOL/Library/Library.thy	Tue Apr 21 17:19:00 2015 +0100
     3.3 @@ -44,7 +44,6 @@
     3.4    More_List
     3.5    Multiset_Order
     3.6    Numeral_Type
     3.7 -  NthRoot_Limits
     3.8    OptionalSugar
     3.9    Option_ord
    3.10    Order_Continuity
     4.1 --- a/src/HOL/Library/NthRoot_Limits.thy	Mon Apr 20 13:46:36 2015 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,88 +0,0 @@
     4.4 -theory NthRoot_Limits
     4.5 -  imports Complex_Main
     4.6 -begin
     4.7 -
     4.8 -lemma LIMSEQ_root: "(\<lambda>n. root n n) ----> 1"
     4.9 -proof -
    4.10 -  def x \<equiv> "\<lambda>n. root n n - 1"
    4.11 -  have "x ----> sqrt 0"
    4.12 -  proof (rule tendsto_sandwich[OF _ _ tendsto_const])
    4.13 -    show "(\<lambda>x. sqrt (2 / x)) ----> sqrt 0"
    4.14 -      by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
    4.15 -         (simp_all add: at_infinity_eq_at_top_bot)
    4.16 -    { fix n :: nat assume "2 < n"
    4.17 -      have "1 + (real (n - 1) * n) / 2 * x n^2 = 1 + of_nat (n choose 2) * x n^2"
    4.18 -        using `2 < n` unfolding gbinomial_def binomial_gbinomial
    4.19 -        by (simp add: atLeast0AtMost atMost_Suc field_simps real_of_nat_diff numeral_2_eq_2 real_eq_of_nat[symmetric])
    4.20 -      also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)"
    4.21 -        by (simp add: x_def)
    4.22 -      also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
    4.23 -        using `2 < n` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
    4.24 -      also have "\<dots> = (x n + 1) ^ n"
    4.25 -        by (simp add: binomial_ring)
    4.26 -      also have "\<dots> = n"
    4.27 -        using `2 < n` by (simp add: x_def)
    4.28 -      finally have "real (n - 1) * (real n / 2 * (x n)\<^sup>2) \<le> real (n - 1) * 1"
    4.29 -        by simp
    4.30 -      then have "(x n)\<^sup>2 \<le> 2 / real n"
    4.31 -        using `2 < n` unfolding mult_le_cancel_left by (simp add: field_simps)
    4.32 -      from real_sqrt_le_mono[OF this] have "x n \<le> sqrt (2 / real n)"
    4.33 -        by simp }
    4.34 -    then show "eventually (\<lambda>n. x n \<le> sqrt (2 / real n)) sequentially"
    4.35 -      by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
    4.36 -    show "eventually (\<lambda>n. sqrt 0 \<le> x n) sequentially"
    4.37 -      by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def)
    4.38 -  qed
    4.39 -  from tendsto_add[OF this tendsto_const[of 1]] show ?thesis
    4.40 -    by (simp add: x_def)
    4.41 -qed
    4.42 -
    4.43 -lemma LIMSEQ_root_const:
    4.44 -  assumes "0 < c"
    4.45 -  shows "(\<lambda>n. root n c) ----> 1"
    4.46 -proof -
    4.47 -  { fix c :: real assume "1 \<le> c"
    4.48 -    def x \<equiv> "\<lambda>n. root n c - 1"
    4.49 -    have "x ----> 0"
    4.50 -    proof (rule tendsto_sandwich[OF _ _ tendsto_const])
    4.51 -      show "(\<lambda>n. c / n) ----> 0"
    4.52 -        by (intro tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
    4.53 -           (simp_all add: at_infinity_eq_at_top_bot)
    4.54 -      { fix n :: nat assume "1 < n"
    4.55 -        have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1"
    4.56 -          using `1 < n` unfolding gbinomial_def binomial_gbinomial by (simp add: real_eq_of_nat[symmetric])
    4.57 -        also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)"
    4.58 -          by (simp add: x_def)
    4.59 -        also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
    4.60 -          using `1 < n` `1 \<le> c` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
    4.61 -        also have "\<dots> = (x n + 1) ^ n"
    4.62 -          by (simp add: binomial_ring)
    4.63 -        also have "\<dots> = c"
    4.64 -          using `1 < n` `1 \<le> c` by (simp add: x_def)
    4.65 -        finally have "x n \<le> c / n"
    4.66 -          using `1 \<le> c` `1 < n` by (simp add: field_simps) }
    4.67 -      then show "eventually (\<lambda>n. x n \<le> c / n) sequentially"
    4.68 -        by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
    4.69 -      show "eventually (\<lambda>n. 0 \<le> x n) sequentially"
    4.70 -        using `1 \<le> c` by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def)
    4.71 -    qed
    4.72 -    from tendsto_add[OF this tendsto_const[of 1]] have "(\<lambda>n. root n c) ----> 1"
    4.73 -      by (simp add: x_def) }
    4.74 -  note ge_1 = this
    4.75 -
    4.76 -  show ?thesis
    4.77 -  proof cases
    4.78 -    assume "1 \<le> c" with ge_1 show ?thesis by blast
    4.79 -  next
    4.80 -    assume "\<not> 1 \<le> c"
    4.81 -    with `0 < c` have "1 \<le> 1 / c"
    4.82 -      by simp
    4.83 -    then have "(\<lambda>n. 1 / root n (1 / c)) ----> 1 / 1"
    4.84 -      by (intro tendsto_divide tendsto_const ge_1 `1 \<le> 1 / c` one_neq_zero)
    4.85 -    then show ?thesis
    4.86 -      by (rule filterlim_cong[THEN iffD1, rotated 3])
    4.87 -         (auto intro!: exI[of _ 1] simp: eventually_sequentially real_root_divide)
    4.88 -  qed
    4.89 -qed
    4.90 -
    4.91 -end
     5.1 --- a/src/HOL/Limits.thy	Mon Apr 20 13:46:36 2015 +0100
     5.2 +++ b/src/HOL/Limits.thy	Tue Apr 21 17:19:00 2015 +0100
     5.3 @@ -396,7 +396,7 @@
     5.4  lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F"
     5.5    by (simp only: tendsto_iff Zfun_def dist_norm)
     5.6  
     5.7 -lemma tendsto_0_le: "\<lbrakk>(f ---> 0) F; eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F\<rbrakk> 
     5.8 +lemma tendsto_0_le: "\<lbrakk>(f ---> 0) F; eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F\<rbrakk>
     5.9                       \<Longrightarrow> (g ---> 0) F"
    5.10    by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff)
    5.11  
    5.12 @@ -1134,7 +1134,7 @@
    5.13  
    5.14  *}
    5.15  
    5.16 -lemma filterlim_tendsto_pos_mult_at_top: 
    5.17 +lemma filterlim_tendsto_pos_mult_at_top:
    5.18    assumes f: "(f ---> c) F" and c: "0 < c"
    5.19    assumes g: "LIM x F. g x :> at_top"
    5.20    shows "LIM x F. (f x * g x :: real) :> at_top"
    5.21 @@ -1156,7 +1156,7 @@
    5.22    qed
    5.23  qed
    5.24  
    5.25 -lemma filterlim_at_top_mult_at_top: 
    5.26 +lemma filterlim_at_top_mult_at_top:
    5.27    assumes f: "LIM x F. f x :> at_top"
    5.28    assumes g: "LIM x F. g x :> at_top"
    5.29    shows "LIM x F. (f x * g x :: real) :> at_top"
    5.30 @@ -1202,7 +1202,7 @@
    5.31    shows "0 < n \<Longrightarrow> LIM x F. f x :> at_bot \<Longrightarrow> odd n \<Longrightarrow> LIM x F. (f x)^n :> at_bot"
    5.32    using filterlim_pow_at_top[of n "\<lambda>x. - f x" F] by (simp add: filterlim_uminus_at_bot)
    5.33  
    5.34 -lemma filterlim_tendsto_add_at_top: 
    5.35 +lemma filterlim_tendsto_add_at_top:
    5.36    assumes f: "(f ---> c) F"
    5.37    assumes g: "LIM x F. g x :> at_top"
    5.38    shows "LIM x F. (f x + g x :: real) :> at_top"
    5.39 @@ -1225,7 +1225,7 @@
    5.40    unfolding divide_inverse
    5.41    by (rule filterlim_tendsto_pos_mult_at_top[OF f]) (rule filterlim_inverse_at_top[OF g])
    5.42  
    5.43 -lemma filterlim_at_top_add_at_top: 
    5.44 +lemma filterlim_at_top_add_at_top:
    5.45    assumes f: "LIM x F. f x :> at_top"
    5.46    assumes g: "LIM x F. g x :> at_top"
    5.47    shows "LIM x F. (f x + g x :: real) :> at_top"
    5.48 @@ -1315,16 +1315,108 @@
    5.49    shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
    5.50    by (rule Bfun_inverse)
    5.51  
    5.52 -lemma LIMSEQ_diff_approach_zero:
    5.53 -  fixes L :: "'a::real_normed_vector"
    5.54 -  shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
    5.55 -  by (drule (1) tendsto_add, simp)
    5.56 +text{* Transformation of limit. *}
    5.57 +
    5.58 +lemma eventually_at2:
    5.59 +  "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
    5.60 +  unfolding eventually_at dist_nz by auto
    5.61 +
    5.62 +lemma Lim_transform:
    5.63 +  fixes a b :: "'a::real_normed_vector"
    5.64 +  shows "\<lbrakk>(g ---> a) F; ((\<lambda>x. f x - g x) ---> 0) F\<rbrakk> \<Longrightarrow> (f ---> a) F"
    5.65 +  using tendsto_add [of g a F "\<lambda>x. f x - g x" 0] by simp
    5.66 +
    5.67 +lemma Lim_transform2:
    5.68 +  fixes a b :: "'a::real_normed_vector"
    5.69 +  shows "\<lbrakk>(f ---> a) F; ((\<lambda>x. f x - g x) ---> 0) F\<rbrakk> \<Longrightarrow> (g ---> a) F"
    5.70 +  by (erule Lim_transform) (simp add: tendsto_minus_cancel)
    5.71 +
    5.72 +lemma Lim_transform_eventually:
    5.73 +  "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net \<Longrightarrow> (g ---> l) net"
    5.74 +  apply (rule topological_tendstoI)
    5.75 +  apply (drule (2) topological_tendstoD)
    5.76 +  apply (erule (1) eventually_elim2, simp)
    5.77 +  done
    5.78 +
    5.79 +lemma Lim_transform_within:
    5.80 +  assumes "0 < d"
    5.81 +    and "\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
    5.82 +    and "(f ---> l) (at x within S)"
    5.83 +  shows "(g ---> l) (at x within S)"
    5.84 +proof (rule Lim_transform_eventually)
    5.85 +  show "eventually (\<lambda>x. f x = g x) (at x within S)"
    5.86 +    using assms(1,2) by (auto simp: dist_nz eventually_at)
    5.87 +  show "(f ---> l) (at x within S)" by fact
    5.88 +qed
    5.89 +
    5.90 +lemma Lim_transform_at:
    5.91 +  assumes "0 < d"
    5.92 +    and "\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
    5.93 +    and "(f ---> l) (at x)"
    5.94 +  shows "(g ---> l) (at x)"
    5.95 +  using _ assms(3)
    5.96 +proof (rule Lim_transform_eventually)
    5.97 +  show "eventually (\<lambda>x. f x = g x) (at x)"
    5.98 +    unfolding eventually_at2
    5.99 +    using assms(1,2) by auto
   5.100 +qed
   5.101 +
   5.102 +text{* Common case assuming being away from some crucial point like 0. *}
   5.103  
   5.104 -lemma LIMSEQ_diff_approach_zero2:
   5.105 -  fixes L :: "'a::real_normed_vector"
   5.106 -  shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L"
   5.107 -  by (drule (1) tendsto_diff, simp)
   5.108 +lemma Lim_transform_away_within:
   5.109 +  fixes a b :: "'a::t1_space"
   5.110 +  assumes "a \<noteq> b"
   5.111 +    and "\<forall>x\<in>S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   5.112 +    and "(f ---> l) (at a within S)"
   5.113 +  shows "(g ---> l) (at a within S)"
   5.114 +proof (rule Lim_transform_eventually)
   5.115 +  show "(f ---> l) (at a within S)" by fact
   5.116 +  show "eventually (\<lambda>x. f x = g x) (at a within S)"
   5.117 +    unfolding eventually_at_topological
   5.118 +    by (rule exI [where x="- {b}"], simp add: open_Compl assms)
   5.119 +qed
   5.120 +
   5.121 +lemma Lim_transform_away_at:
   5.122 +  fixes a b :: "'a::t1_space"
   5.123 +  assumes ab: "a\<noteq>b"
   5.124 +    and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   5.125 +    and fl: "(f ---> l) (at a)"
   5.126 +  shows "(g ---> l) (at a)"
   5.127 +  using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl by simp
   5.128 +
   5.129 +text{* Alternatively, within an open set. *}
   5.130  
   5.131 +lemma Lim_transform_within_open:
   5.132 +  assumes "open S" and "a \<in> S"
   5.133 +    and "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"
   5.134 +    and "(f ---> l) (at a)"
   5.135 +  shows "(g ---> l) (at a)"
   5.136 +proof (rule Lim_transform_eventually)
   5.137 +  show "eventually (\<lambda>x. f x = g x) (at a)"
   5.138 +    unfolding eventually_at_topological
   5.139 +    using assms(1,2,3) by auto
   5.140 +  show "(f ---> l) (at a)" by fact
   5.141 +qed
   5.142 +
   5.143 +text{* A congruence rule allowing us to transform limits assuming not at point. *}
   5.144 +
   5.145 +(* FIXME: Only one congruence rule for tendsto can be used at a time! *)
   5.146 +
   5.147 +lemma Lim_cong_within(*[cong add]*):
   5.148 +  assumes "a = b"
   5.149 +    and "x = y"
   5.150 +    and "S = T"
   5.151 +    and "\<And>x. x \<noteq> b \<Longrightarrow> x \<in> T \<Longrightarrow> f x = g x"
   5.152 +  shows "(f ---> x) (at a within S) \<longleftrightarrow> (g ---> y) (at b within T)"
   5.153 +  unfolding tendsto_def eventually_at_topological
   5.154 +  using assms by simp
   5.155 +
   5.156 +lemma Lim_cong_at(*[cong add]*):
   5.157 +  assumes "a = b" "x = y"
   5.158 +    and "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
   5.159 +  shows "((\<lambda>x. f x) ---> x) (at a) \<longleftrightarrow> ((g ---> y) (at a))"
   5.160 +  unfolding tendsto_def eventually_at_topological
   5.161 +  using assms by simp
   5.162  text{*An unbounded sequence's inverse tends to 0*}
   5.163  
   5.164  lemma LIMSEQ_inverse_zero:
   5.165 @@ -1684,7 +1776,7 @@
   5.166    "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
   5.167    by (fact continuous)
   5.168  
   5.169 -lemmas isCont_scaleR [simp] = 
   5.170 +lemmas isCont_scaleR [simp] =
   5.171    bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
   5.172  
   5.173  lemmas isCont_of_real [simp] =
   5.174 @@ -1740,7 +1832,7 @@
   5.175  lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   5.176  by (rule isUCont [THEN isUCont_Cauchy])
   5.177  
   5.178 -lemma LIM_less_bound: 
   5.179 +lemma LIM_less_bound:
   5.180    fixes f :: "real \<Rightarrow> real"
   5.181    assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
   5.182    shows "0 \<le> f x"
   5.183 @@ -1804,7 +1896,7 @@
   5.184  
   5.185    show "P a b"
   5.186    proof (rule ccontr)
   5.187 -    assume "\<not> P a b" 
   5.188 +    assume "\<not> P a b"
   5.189      { fix n have "\<not> P (l n) (u n)"
   5.190        proof (induct n)
   5.191          case (Suc n) with trans[of "l n" "(l n + u n) / 2" "u n"] show ?case by auto
   5.192 @@ -1911,7 +2003,7 @@
   5.193  lemma isCont_Lb_Ub:
   5.194    fixes f :: "real \<Rightarrow> real"
   5.195    assumes "a \<le> b" "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
   5.196 -  shows "\<exists>L M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> L \<le> f x \<and> f x \<le> M) \<and> 
   5.197 +  shows "\<exists>L M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> L \<le> f x \<and> f x \<le> M) \<and>
   5.198                 (\<forall>y. L \<le> y \<and> y \<le> M \<longrightarrow> (\<exists>x. a \<le> x \<and> x \<le> b \<and> (f x = y)))"
   5.199  proof -
   5.200    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"
   5.201 @@ -1974,8 +2066,8 @@
   5.202  
   5.203  lemma isCont_inv_fun:
   5.204    fixes f g :: "real \<Rightarrow> real"
   5.205 -  shows "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
   5.206 -         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
   5.207 +  shows "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;
   5.208 +         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]
   5.209        ==> isCont g (f x)"
   5.210  by (rule isCont_inverse_function)
   5.211  
     6.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Apr 20 13:46:36 2015 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Apr 21 17:19:00 2015 +0100
     6.3 @@ -1263,9 +1263,6 @@
     6.4  
     6.5  subsection{*Complex Powers*}
     6.6  
     6.7 -lemma powr_0 [simp]: "0 powr z = 0"
     6.8 -  by (simp add: powr_def)
     6.9 -
    6.10  lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
    6.11    by (simp add: powr_def)
    6.12  
    6.13 @@ -1526,7 +1523,7 @@
    6.14  proof -
    6.15    have nz0: "1 + \<i>*z \<noteq> 0"
    6.16      using assms
    6.17 -    by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2) 
    6.18 +    by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2)
    6.19                less_irrefl minus_diff_eq mult.right_neutral right_minus_eq)
    6.20    have "z \<noteq> -\<i>" using assms
    6.21      by auto
    6.22 @@ -1771,7 +1768,7 @@
    6.23    by (blast intro: isCont_o2 [OF _ isCont_Arcsin])
    6.24  
    6.25  lemma sin_Arcsin [simp]: "sin(Arcsin z) = z"
    6.26 -proof -  
    6.27 +proof -
    6.28    have "\<i>*z*2 + csqrt (1 - z\<^sup>2)*2 = 0 \<longleftrightarrow> (\<i>*z)*2 + csqrt (1 - z\<^sup>2)*2 = 0"
    6.29      by (simp add: algebra_simps)  --{*Cancelling a factor of 2*}
    6.30    moreover have "... \<longleftrightarrow> (\<i>*z) + csqrt (1 - z\<^sup>2) = 0"
    6.31 @@ -1903,7 +1900,7 @@
    6.32  proof (cases "Im z = 0")
    6.33    case True
    6.34    then show ?thesis
    6.35 -    using assms 
    6.36 +    using assms
    6.37      by (fastforce simp add: cmod_def Re_power2 Im_power2 algebra_simps abs_square_less_1 [symmetric])
    6.38  next
    6.39    case False
     7.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 20 13:46:36 2015 +0100
     7.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Apr 21 17:19:00 2015 +0100
     7.3 @@ -705,7 +705,7 @@
     7.4      apply (clarsimp simp add: less_diff_eq)
     7.5      by (metis dist_commute dist_triangle_lt)
     7.6    assume ?rhs then have 2: "S = U \<inter> T"
     7.7 -    unfolding T_def 
     7.8 +    unfolding T_def
     7.9      by auto (metis dist_self)
    7.10    from 1 2 show ?lhs
    7.11      unfolding openin_open open_dist by fast
    7.12 @@ -1750,10 +1750,6 @@
    7.13  
    7.14  text {* Some property holds "sufficiently close" to the limit point. *}
    7.15  
    7.16 -lemma eventually_at2:
    7.17 -  "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
    7.18 -  unfolding eventually_at dist_nz by auto
    7.19 -
    7.20  lemma eventually_happens: "eventually P net \<Longrightarrow> trivial_limit net \<or> (\<exists>x. P x)"
    7.21    unfolding trivial_limit_def
    7.22    by (auto elim: eventually_rev_mp)
    7.23 @@ -2051,100 +2047,6 @@
    7.24    shows "netlimit (at x within S) = x"
    7.25    using assms by (metis at_within_interior netlimit_at)
    7.26  
    7.27 -text{* Transformation of limit. *}
    7.28 -
    7.29 -lemma Lim_transform:
    7.30 -  fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
    7.31 -  assumes "((\<lambda>x. f x - g x) ---> 0) net" "(f ---> l) net"
    7.32 -  shows "(g ---> l) net"
    7.33 -  using tendsto_diff [OF assms(2) assms(1)] by simp
    7.34 -
    7.35 -lemma Lim_transform_eventually:
    7.36 -  "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net \<Longrightarrow> (g ---> l) net"
    7.37 -  apply (rule topological_tendstoI)
    7.38 -  apply (drule (2) topological_tendstoD)
    7.39 -  apply (erule (1) eventually_elim2, simp)
    7.40 -  done
    7.41 -
    7.42 -lemma Lim_transform_within:
    7.43 -  assumes "0 < d"
    7.44 -    and "\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
    7.45 -    and "(f ---> l) (at x within S)"
    7.46 -  shows "(g ---> l) (at x within S)"
    7.47 -proof (rule Lim_transform_eventually)
    7.48 -  show "eventually (\<lambda>x. f x = g x) (at x within S)"
    7.49 -    using assms(1,2) by (auto simp: dist_nz eventually_at)
    7.50 -  show "(f ---> l) (at x within S)" by fact
    7.51 -qed
    7.52 -
    7.53 -lemma Lim_transform_at:
    7.54 -  assumes "0 < d"
    7.55 -    and "\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
    7.56 -    and "(f ---> l) (at x)"
    7.57 -  shows "(g ---> l) (at x)"
    7.58 -  using _ assms(3)
    7.59 -proof (rule Lim_transform_eventually)
    7.60 -  show "eventually (\<lambda>x. f x = g x) (at x)"
    7.61 -    unfolding eventually_at2
    7.62 -    using assms(1,2) by auto
    7.63 -qed
    7.64 -
    7.65 -text{* Common case assuming being away from some crucial point like 0. *}
    7.66 -
    7.67 -lemma Lim_transform_away_within:
    7.68 -  fixes a b :: "'a::t1_space"
    7.69 -  assumes "a \<noteq> b"
    7.70 -    and "\<forall>x\<in>S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
    7.71 -    and "(f ---> l) (at a within S)"
    7.72 -  shows "(g ---> l) (at a within S)"
    7.73 -proof (rule Lim_transform_eventually)
    7.74 -  show "(f ---> l) (at a within S)" by fact
    7.75 -  show "eventually (\<lambda>x. f x = g x) (at a within S)"
    7.76 -    unfolding eventually_at_topological
    7.77 -    by (rule exI [where x="- {b}"], simp add: open_Compl assms)
    7.78 -qed
    7.79 -
    7.80 -lemma Lim_transform_away_at:
    7.81 -  fixes a b :: "'a::t1_space"
    7.82 -  assumes ab: "a\<noteq>b"
    7.83 -    and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
    7.84 -    and fl: "(f ---> l) (at a)"
    7.85 -  shows "(g ---> l) (at a)"
    7.86 -  using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl by simp
    7.87 -
    7.88 -text{* Alternatively, within an open set. *}
    7.89 -
    7.90 -lemma Lim_transform_within_open:
    7.91 -  assumes "open S" and "a \<in> S"
    7.92 -    and "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"
    7.93 -    and "(f ---> l) (at a)"
    7.94 -  shows "(g ---> l) (at a)"
    7.95 -proof (rule Lim_transform_eventually)
    7.96 -  show "eventually (\<lambda>x. f x = g x) (at a)"
    7.97 -    unfolding eventually_at_topological
    7.98 -    using assms(1,2,3) by auto
    7.99 -  show "(f ---> l) (at a)" by fact
   7.100 -qed
   7.101 -
   7.102 -text{* A congruence rule allowing us to transform limits assuming not at point. *}
   7.103 -
   7.104 -(* FIXME: Only one congruence rule for tendsto can be used at a time! *)
   7.105 -
   7.106 -lemma Lim_cong_within(*[cong add]*):
   7.107 -  assumes "a = b"
   7.108 -    and "x = y"
   7.109 -    and "S = T"
   7.110 -    and "\<And>x. x \<noteq> b \<Longrightarrow> x \<in> T \<Longrightarrow> f x = g x"
   7.111 -  shows "(f ---> x) (at a within S) \<longleftrightarrow> (g ---> y) (at b within T)"
   7.112 -  unfolding tendsto_def eventually_at_topological
   7.113 -  using assms by simp
   7.114 -
   7.115 -lemma Lim_cong_at(*[cong add]*):
   7.116 -  assumes "a = b" "x = y"
   7.117 -    and "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
   7.118 -  shows "((\<lambda>x. f x) ---> x) (at a) \<longleftrightarrow> ((g ---> y) (at a))"
   7.119 -  unfolding tendsto_def eventually_at_topological
   7.120 -  using assms by simp
   7.121  
   7.122  text{* Useful lemmas on closure and set of possible sequential limits.*}
   7.123  
     8.1 --- a/src/HOL/NthRoot.thy	Mon Apr 20 13:46:36 2015 +0100
     8.2 +++ b/src/HOL/NthRoot.thy	Tue Apr 21 17:19:00 2015 +0100
     8.3 @@ -7,7 +7,7 @@
     8.4  section {* Nth Roots of Real Numbers *}
     8.5  
     8.6  theory NthRoot
     8.7 -imports Deriv
     8.8 +imports Deriv Binomial
     8.9  begin
    8.10  
    8.11  lemma abs_sgn_eq: "abs (sgn x :: real) = (if x = 0 then 0 else 1)"
    8.12 @@ -644,6 +644,90 @@
    8.13    apply auto 
    8.14    done
    8.15    
    8.16 +lemma LIMSEQ_root: "(\<lambda>n. root n n) ----> 1"
    8.17 +proof -
    8.18 +  def x \<equiv> "\<lambda>n. root n n - 1"
    8.19 +  have "x ----> sqrt 0"
    8.20 +  proof (rule tendsto_sandwich[OF _ _ tendsto_const])
    8.21 +    show "(\<lambda>x. sqrt (2 / x)) ----> sqrt 0"
    8.22 +      by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
    8.23 +         (simp_all add: at_infinity_eq_at_top_bot)
    8.24 +    { fix n :: nat assume "2 < n"
    8.25 +      have "1 + (real (n - 1) * n) / 2 * x n^2 = 1 + of_nat (n choose 2) * x n^2"
    8.26 +        using `2 < n` unfolding gbinomial_def binomial_gbinomial
    8.27 +        by (simp add: atLeast0AtMost atMost_Suc field_simps real_of_nat_diff numeral_2_eq_2 real_eq_of_nat[symmetric])
    8.28 +      also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)"
    8.29 +        by (simp add: x_def)
    8.30 +      also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
    8.31 +        using `2 < n` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
    8.32 +      also have "\<dots> = (x n + 1) ^ n"
    8.33 +        by (simp add: binomial_ring)
    8.34 +      also have "\<dots> = n"
    8.35 +        using `2 < n` by (simp add: x_def)
    8.36 +      finally have "real (n - 1) * (real n / 2 * (x n)\<^sup>2) \<le> real (n - 1) * 1"
    8.37 +        by simp
    8.38 +      then have "(x n)\<^sup>2 \<le> 2 / real n"
    8.39 +        using `2 < n` unfolding mult_le_cancel_left by (simp add: field_simps)
    8.40 +      from real_sqrt_le_mono[OF this] have "x n \<le> sqrt (2 / real n)"
    8.41 +        by simp }
    8.42 +    then show "eventually (\<lambda>n. x n \<le> sqrt (2 / real n)) sequentially"
    8.43 +      by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
    8.44 +    show "eventually (\<lambda>n. sqrt 0 \<le> x n) sequentially"
    8.45 +      by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def)
    8.46 +  qed
    8.47 +  from tendsto_add[OF this tendsto_const[of 1]] show ?thesis
    8.48 +    by (simp add: x_def)
    8.49 +qed
    8.50 +
    8.51 +lemma LIMSEQ_root_const:
    8.52 +  assumes "0 < c"
    8.53 +  shows "(\<lambda>n. root n c) ----> 1"
    8.54 +proof -
    8.55 +  { fix c :: real assume "1 \<le> c"
    8.56 +    def x \<equiv> "\<lambda>n. root n c - 1"
    8.57 +    have "x ----> 0"
    8.58 +    proof (rule tendsto_sandwich[OF _ _ tendsto_const])
    8.59 +      show "(\<lambda>n. c / n) ----> 0"
    8.60 +        by (intro tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
    8.61 +           (simp_all add: at_infinity_eq_at_top_bot)
    8.62 +      { fix n :: nat assume "1 < n"
    8.63 +        have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1"
    8.64 +          using `1 < n` unfolding gbinomial_def binomial_gbinomial by (simp add: real_eq_of_nat[symmetric])
    8.65 +        also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)"
    8.66 +          by (simp add: x_def)
    8.67 +        also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
    8.68 +          using `1 < n` `1 \<le> c` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
    8.69 +        also have "\<dots> = (x n + 1) ^ n"
    8.70 +          by (simp add: binomial_ring)
    8.71 +        also have "\<dots> = c"
    8.72 +          using `1 < n` `1 \<le> c` by (simp add: x_def)
    8.73 +        finally have "x n \<le> c / n"
    8.74 +          using `1 \<le> c` `1 < n` by (simp add: field_simps) }
    8.75 +      then show "eventually (\<lambda>n. x n \<le> c / n) sequentially"
    8.76 +        by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
    8.77 +      show "eventually (\<lambda>n. 0 \<le> x n) sequentially"
    8.78 +        using `1 \<le> c` by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def)
    8.79 +    qed
    8.80 +    from tendsto_add[OF this tendsto_const[of 1]] have "(\<lambda>n. root n c) ----> 1"
    8.81 +      by (simp add: x_def) }
    8.82 +  note ge_1 = this
    8.83 +
    8.84 +  show ?thesis
    8.85 +  proof cases
    8.86 +    assume "1 \<le> c" with ge_1 show ?thesis by blast
    8.87 +  next
    8.88 +    assume "\<not> 1 \<le> c"
    8.89 +    with `0 < c` have "1 \<le> 1 / c"
    8.90 +      by simp
    8.91 +    then have "(\<lambda>n. 1 / root n (1 / c)) ----> 1 / 1"
    8.92 +      by (intro tendsto_divide tendsto_const ge_1 `1 \<le> 1 / c` one_neq_zero)
    8.93 +    then show ?thesis
    8.94 +      by (rule filterlim_cong[THEN iffD1, rotated 3])
    8.95 +         (auto intro!: exI[of _ 1] simp: eventually_sequentially real_root_divide)
    8.96 +  qed
    8.97 +qed
    8.98 +
    8.99 +
   8.100  text "Legacy theorem names:"
   8.101  lemmas real_root_pos2 = real_root_power_cancel
   8.102  lemmas real_root_pos_pos = real_root_gt_zero [THEN order_less_imp_le]
     9.1 --- a/src/HOL/Number_Theory/Fib.thy	Mon Apr 20 13:46:36 2015 +0100
     9.2 +++ b/src/HOL/Number_Theory/Fib.thy	Tue Apr 21 17:19:00 2015 +0100
     9.3 @@ -11,11 +11,11 @@
     9.4  section {* Fib *}
     9.5  
     9.6  theory Fib
     9.7 -imports Main "../GCD"
     9.8 +imports Main "../GCD" "../Binomial"
     9.9  begin
    9.10  
    9.11  
    9.12 -subsection {* Main definitions *}
    9.13 +subsection {* Fibonacci numbers *}
    9.14  
    9.15  fun fib :: "nat \<Rightarrow> nat"
    9.16  where
    9.17 @@ -23,7 +23,7 @@
    9.18    | fib1: "fib (Suc 0) = 1"
    9.19    | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
    9.20  
    9.21 -subsection {* Fibonacci numbers *}
    9.22 +subsection {* Basic Properties *}
    9.23  
    9.24  lemma fib_1 [simp]: "fib (1::nat) = 1"
    9.25    by (metis One_nat_def fib1)
    9.26 @@ -41,6 +41,8 @@
    9.27  lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
    9.28    by (induct n rule: fib.induct) (auto simp add: )
    9.29  
    9.30 +subsection {* A Few Elementary Results *}
    9.31 +
    9.32  text {*
    9.33    \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
    9.34    much easier using integers, not natural numbers!
    9.35 @@ -55,7 +57,7 @@
    9.36  using fib_Cassini_int [of n] by auto
    9.37  
    9.38  
    9.39 -text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
    9.40 +subsection {* Law 6.111 of Concrete Mathematics *}
    9.41  
    9.42  lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
    9.43    apply (induct n rule: fib.induct)
    9.44 @@ -67,9 +69,7 @@
    9.45    apply (simp add: gcd_commute_nat [of "fib m"])
    9.46    apply (cases m)
    9.47    apply (auto simp add: fib_add)
    9.48 -  apply (subst gcd_commute_nat)
    9.49 -  apply (subst mult.commute)
    9.50 -  apply (metis coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
    9.51 +  apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
    9.52    done
    9.53  
    9.54  lemma gcd_fib_diff: "m \<le> n \<Longrightarrow>
    9.55 @@ -109,5 +109,35 @@
    9.56      "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
    9.57    by (induct n rule: nat.induct) (auto simp add:  field_simps)
    9.58  
    9.59 +subsection {* Fibonacci and Binomial Coefficients *}
    9.60 +
    9.61 +lemma setsum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)"
    9.62 +  by (induct n) auto
    9.63 +
    9.64 +lemma setsum_choose_drop_zero:
    9.65 +    "(\<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)"
    9.66 +  by (rule trans [OF setsum.cong setsum_drop_zero]) auto
    9.67 +
    9.68 +lemma ne_diagonal_fib:
    9.69 +   "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
    9.70 +proof (induct n rule: fib.induct)
    9.71 +  case 1 show ?case by simp
    9.72 +next
    9.73 +  case 2 show ?case by simp
    9.74 +next
    9.75 +  case (3 n)
    9.76 +  have "(\<Sum>k = 0..Suc n. Suc (Suc n) - k choose k) =
    9.77 +        (\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k=0 then 0 else (Suc n - k choose (k - 1))))"
    9.78 +    by (rule setsum.cong) (simp_all add: choose_reduce_nat)
    9.79 +  also have "... = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
    9.80 +                   (\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"
    9.81 +    by (simp add: setsum.distrib)
    9.82 +  also have "... = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
    9.83 +                   (\<Sum>j = 0..n. n - j choose j)"
    9.84 +    by (metis setsum_choose_drop_zero)
    9.85 +  finally show ?case using 3
    9.86 +    by simp
    9.87 +qed
    9.88 +
    9.89  end
    9.90  
    10.1 --- a/src/HOL/Probability/Measure_Space.thy	Mon Apr 20 13:46:36 2015 +0100
    10.2 +++ b/src/HOL/Probability/Measure_Space.thy	Tue Apr 21 17:19:00 2015 +0100
    10.3 @@ -389,7 +389,7 @@
    10.4    ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
    10.5      by (simp add: zero_ereal_def)
    10.6    then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
    10.7 -    by (rule LIMSEQ_diff_approach_zero2[OF tendsto_const])
    10.8 +    by (rule Lim_transform[OF tendsto_const])
    10.9    then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
   10.10      using A by (subst (1 2) f') auto
   10.11  qed
    11.1 --- a/src/HOL/Series.thy	Mon Apr 20 13:46:36 2015 +0100
    11.2 +++ b/src/HOL/Series.thy	Tue Apr 21 17:19:00 2015 +0100
    11.3 @@ -643,7 +643,7 @@
    11.4      by (simp only: setsum_diff finite_S1 S2_le_S1)
    11.5  
    11.6    with 1 have "(\<lambda>n. setsum ?g (?S2 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
    11.7 -    by (rule LIMSEQ_diff_approach_zero2)
    11.8 +    by (rule Lim_transform2)
    11.9    thus ?thesis by (simp only: sums_def setsum_triangle_reindex)
   11.10  qed
   11.11  
    12.1 --- a/src/HOL/Transcendental.thy	Mon Apr 20 13:46:36 2015 +0100
    12.2 +++ b/src/HOL/Transcendental.thy	Tue Apr 21 17:19:00 2015 +0100
    12.3 @@ -104,7 +104,22 @@
    12.4    shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^i)"
    12.5  by (metis one_diff_power_eq' [of n x] nat_diff_setsum_reindex)
    12.6  
    12.7 -text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
    12.8 +lemma powser_zero:
    12.9 +  fixes f :: "nat \<Rightarrow> 'a::real_normed_algebra_1"
   12.10 +  shows "(\<Sum>n. f n * 0 ^ n) = f 0"
   12.11 +proof -
   12.12 +  have "(\<Sum>n<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
   12.13 +    by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left)
   12.14 +  thus ?thesis unfolding One_nat_def by simp
   12.15 +qed
   12.16 +
   12.17 +lemma powser_sums_zero:
   12.18 +  fixes a :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
   12.19 +  shows "(\<lambda>n. a n * 0^n) sums a 0"
   12.20 +    using sums_finite [of "{0}" "\<lambda>n. a n * 0 ^ n"]
   12.21 +    by simp
   12.22 +
   12.23 +text{*Power series has a circle or radius of convergence: if it sums for @{term
   12.24    x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
   12.25  
   12.26  lemma powser_insidea:
   12.27 @@ -167,6 +182,46 @@
   12.28        summable (\<lambda>n. f n * (z ^ n))"
   12.29    by (rule powser_insidea [THEN summable_norm_cancel])
   12.30  
   12.31 +lemma powser_times_n_limit_0:
   12.32 +  fixes x :: "'a::{real_normed_div_algebra,banach}"
   12.33 +  assumes "norm x < 1"
   12.34 +    shows "(\<lambda>n. of_nat n * x ^ n) ----> 0"
   12.35 +proof -
   12.36 +  have "norm x / (1 - norm x) \<ge> 0"
   12.37 +    using assms
   12.38 +    by (auto simp: divide_simps)
   12.39 +  moreover obtain N where N: "norm x / (1 - norm x) < of_int N"
   12.40 +    using ex_le_of_int
   12.41 +    by (meson ex_less_of_int)
   12.42 +  ultimately have N0: "N>0" 
   12.43 +    by auto
   12.44 +  then have *: "real (N + 1) * norm x / real N < 1"
   12.45 +    using N assms
   12.46 +    by (auto simp: field_simps)
   12.47 +  { fix n::nat
   12.48 +    assume "N \<le> int n"
   12.49 +    then have "real N * real_of_nat (Suc n) \<le> real_of_nat n * real (1 + N)"
   12.50 +      by (simp add: algebra_simps)
   12.51 +    then have "(real N * real_of_nat (Suc n)) * (norm x * norm (x ^ n))
   12.52 +               \<le> (real_of_nat n * real (1 + N)) * (norm x * norm (x ^ n))"
   12.53 +      using N0 mult_mono by fastforce
   12.54 +    then have "real N * (norm x * (real_of_nat (Suc n) * norm (x ^ n)))
   12.55 +         \<le> real_of_nat n * (norm x * (real (1 + N) * norm (x ^ n)))"
   12.56 +      by (simp add: algebra_simps)
   12.57 +  } note ** = this
   12.58 +  show ?thesis using *
   12.59 +    apply (rule summable_LIMSEQ_zero [OF summable_ratio_test, where N1="nat N"])
   12.60 +    apply (simp add: N0 norm_mult nat_le_iff field_simps power_Suc ** 
   12.61 +                del: of_nat_Suc real_of_int_add)
   12.62 +    done
   12.63 +qed
   12.64 +
   12.65 +corollary lim_n_over_pown:
   12.66 +  fixes x :: "'a::{real_normed_field,banach}"
   12.67 +  shows "1 < norm x \<Longrightarrow> ((\<lambda>n. of_nat n / x^n) ---> 0) sequentially"
   12.68 +using powser_times_n_limit_0 [of "inverse x"]
   12.69 +by (simp add: norm_divide divide_simps)
   12.70 +
   12.71  lemma sum_split_even_odd:
   12.72    fixes f :: "nat \<Rightarrow> real"
   12.73    shows
   12.74 @@ -683,6 +738,132 @@
   12.75    qed
   12.76  qed
   12.77  
   12.78 +subsection {* The Derivative of a Power Series Has the Same Radius of Convergence *}
   12.79 +
   12.80 +lemma termdiff_converges:
   12.81 +  fixes x :: "'a::{real_normed_field,banach}"
   12.82 +  assumes K: "norm x < K"
   12.83 +      and sm: "\<And>x. norm x < K \<Longrightarrow> summable(\<lambda>n. c n * x ^ n)"
   12.84 +    shows "summable (\<lambda>n. diffs c n * x ^ n)"
   12.85 +proof (cases "x = 0")
   12.86 +  case True then show ?thesis
   12.87 +  using powser_sums_zero sums_summable by auto
   12.88 +next
   12.89 +  case False
   12.90 +  then have "K>0"
   12.91 +    using K less_trans zero_less_norm_iff by blast
   12.92 +  then obtain r::real where r: "norm x < norm r" "norm r < K" "r>0"
   12.93 +    using K False
   12.94 +    by (auto simp: abs_less_iff add_pos_pos intro: that [of "(norm x + K) / 2"])
   12.95 +  have "(\<lambda>n. of_nat n * (x / of_real r) ^ n) ----> 0"
   12.96 +    using r by (simp add: norm_divide powser_times_n_limit_0 [of "x / of_real r"])
   12.97 +  then obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> real_of_nat n * norm x ^ n < r ^ n"
   12.98 +    using r unfolding LIMSEQ_iff
   12.99 +    apply (drule_tac x=1 in spec)
  12.100 +    apply (auto simp: norm_divide norm_mult norm_power field_simps)
  12.101 +    done
  12.102 +  have "summable (\<lambda>n. (of_nat n * c n) * x ^ n)"
  12.103 +    apply (rule summable_comparison_test' [of "\<lambda>n. norm(c n * (of_real r) ^ n)" N])
  12.104 +    apply (rule powser_insidea [OF sm [of "of_real ((r+K)/2)"]])
  12.105 +    using N r norm_of_real [of "r+K", where 'a = 'a]
  12.106 +    apply (auto simp add: norm_divide norm_mult norm_power )
  12.107 +    using less_eq_real_def by fastforce
  12.108 +  then have "summable (\<lambda>n. (of_nat (Suc n) * c(Suc n)) * x ^ Suc n)"
  12.109 +    using summable_iff_shift [of "\<lambda>n. of_nat n * c n * x ^ n" 1]
  12.110 +    by simp
  12.111 +  then have "summable (\<lambda>n. (of_nat (Suc n) * c(Suc n)) * x ^ n)"
  12.112 +    using False summable_mult2 [of "\<lambda>n. (of_nat (Suc n) * c(Suc n) * x ^ n) * x" "inverse x"]
  12.113 +    by (simp add: mult.assoc) (auto simp: power_Suc mult_ac)
  12.114 +  then show ?thesis 
  12.115 +    by (simp add: diffs_def)
  12.116 +qed
  12.117 +
  12.118 +lemma termdiff_converges_all:
  12.119 +  fixes x :: "'a::{real_normed_field,banach}"
  12.120 +  assumes "\<And>x. summable (\<lambda>n. c n * x^n)"
  12.121 +    shows "summable (\<lambda>n. diffs c n * x^n)"
  12.122 +  apply (rule termdiff_converges [where K = "1 + norm x"])
  12.123 +  using assms
  12.124 +  apply (auto simp: )
  12.125 +  done
  12.126 +
  12.127 +lemma termdiffs_strong:
  12.128 +  fixes K x :: "'a::{real_normed_field,banach}"
  12.129 +  assumes sm: "summable (\<lambda>n. c n * K ^ n)"
  12.130 +      and K: "norm x < norm K"
  12.131 +  shows "DERIV (\<lambda>x. \<Sum>n. c n * x^n) x :> (\<Sum>n. diffs c n * x^n)"
  12.132 +proof -
  12.133 +  have [simp]: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K"
  12.134 +    using K
  12.135 +    apply (auto simp: norm_divide)
  12.136 +    apply (rule le_less_trans [of _ "of_real (norm K) + of_real (norm x)"])
  12.137 +    apply (auto simp: mult_2_right norm_triangle_mono)
  12.138 +    done
  12.139 +  have "summable (\<lambda>n. c n * (of_real (norm x + norm K) / 2) ^ n)"
  12.140 +    apply (rule summable_norm_cancel [OF powser_insidea [OF sm]])
  12.141 +    using K
  12.142 +    apply (auto simp: algebra_simps)
  12.143 +    done
  12.144 +  moreover have "\<And>x. norm x < norm K \<Longrightarrow> summable (\<lambda>n. diffs c n * x ^ n)"
  12.145 +    by (blast intro: sm termdiff_converges powser_inside)
  12.146 +  moreover have "\<And>x. norm x < norm K \<Longrightarrow> summable (\<lambda>n. diffs(diffs c) n * x ^ n)"
  12.147 +    by (blast intro: sm termdiff_converges powser_inside)
  12.148 +  ultimately show ?thesis
  12.149 +    apply (rule termdiffs [where K = "of_real (norm x + norm K) / 2"])
  12.150 +    apply (auto simp: algebra_simps)
  12.151 +    using K
  12.152 +    apply (simp add: norm_divide)
  12.153 +    apply (rule less_le_trans [of _ "of_real (norm K) + of_real (norm x)"])
  12.154 +    apply (simp_all add: of_real_add [symmetric] del: of_real_add)
  12.155 +    done
  12.156 +qed
  12.157 +
  12.158 +lemma powser_limit_0: 
  12.159 +  fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"
  12.160 +  assumes s: "0 < s"
  12.161 +      and sm: "\<And>x. norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)"
  12.162 +    shows "(f ---> a 0) (at 0)"
  12.163 +proof -
  12.164 +  have "summable (\<lambda>n. a n * (of_real s / 2) ^ n)"
  12.165 +    apply (rule sums_summable [where l = "f (of_real s / 2)", OF sm])
  12.166 +    using s
  12.167 +    apply (auto simp: norm_divide)
  12.168 +    done
  12.169 +  then have "((\<lambda>x. \<Sum>n. a n * x ^ n) has_field_derivative (\<Sum>n. diffs a n * 0 ^ n)) (at 0)"
  12.170 +    apply (rule termdiffs_strong)
  12.171 +    using s
  12.172 +    apply (auto simp: norm_divide)
  12.173 +    done
  12.174 +  then have "isCont (\<lambda>x. \<Sum>n. a n * x ^ n) 0"
  12.175 +    by (blast intro: DERIV_continuous)
  12.176 +  then have "((\<lambda>x. \<Sum>n. a n * x ^ n) ---> a 0) (at 0)"
  12.177 +    by (simp add: continuous_within powser_zero)
  12.178 +  then show ?thesis 
  12.179 +    apply (rule Lim_transform)
  12.180 +    apply (auto simp add: LIM_eq)
  12.181 +    apply (rule_tac x="s" in exI)
  12.182 +    using s 
  12.183 +    apply (auto simp: sm [THEN sums_unique])
  12.184 +    done
  12.185 +qed
  12.186 +
  12.187 +lemma powser_limit_0_strong: 
  12.188 +  fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"
  12.189 +  assumes s: "0 < s"
  12.190 +      and sm: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)"
  12.191 +    shows "(f ---> a 0) (at 0)"
  12.192 +proof -
  12.193 +  have *: "((\<lambda>x. if x = 0 then a 0 else f x) ---> a 0) (at 0)"
  12.194 +    apply (rule powser_limit_0 [OF s])
  12.195 +    apply (case_tac "x=0")
  12.196 +    apply (auto simp add: powser_sums_zero sm)
  12.197 +    done
  12.198 +  show ?thesis
  12.199 +    apply (subst LIM_equal [where g = "(\<lambda>x. if x = 0 then a 0 else f x)"])
  12.200 +    apply (simp_all add: *)
  12.201 +    done
  12.202 +qed
  12.203 +
  12.204  
  12.205  subsection {* Derivability of power series *}
  12.206  
  12.207 @@ -1045,15 +1226,6 @@
  12.208  
  12.209  subsubsection {* Properties of the Exponential Function *}
  12.210  
  12.211 -lemma powser_zero:
  12.212 -  fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1}"
  12.213 -  shows "(\<Sum>n. f n * 0 ^ n) = f 0"
  12.214 -proof -
  12.215 -  have "(\<Sum>n<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
  12.216 -    by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left)
  12.217 -  thus ?thesis unfolding One_nat_def by simp
  12.218 -qed
  12.219 -
  12.220  lemma exp_zero [simp]: "exp 0 = 1"
  12.221    unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero)
  12.222  
  12.223 @@ -1293,6 +1465,9 @@
  12.224    -- {*exponentation via ln and exp*}
  12.225    where  [code del]: "x powr a \<equiv> if x = 0 then 0 else exp(a * ln x)"
  12.226  
  12.227 +lemma powr_0 [simp]: "0 powr z = 0"
  12.228 +  by (simp add: powr_def)
  12.229 +
  12.230  
  12.231  instantiation real :: ln
  12.232  begin
  12.233 @@ -1791,6 +1966,11 @@
  12.234    fixes x::real shows "0 < x \<Longrightarrow> ln x \<le> x - 1"
  12.235    using exp_ge_add_one_self[of "ln x"] by simp
  12.236  
  12.237 +corollary ln_diff_le: 
  12.238 +  fixes x::real 
  12.239 +  shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x - ln y \<le> (x - y) / y"
  12.240 +  by (simp add: ln_div [symmetric] diff_divide_distrib ln_le_minus_one)
  12.241 +
  12.242  lemma ln_eq_minus_one:
  12.243    fixes x::real 
  12.244    assumes "0 < x" "ln x = x - 1"
  12.245 @@ -2272,25 +2452,27 @@
  12.246  using powr_mono by fastforce
  12.247  
  12.248  lemma powr_less_mono2:
  12.249 -  fixes x::real shows "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a"
  12.250 +  fixes x::real shows "0 < a ==> 0 \<le> x ==> x < y ==> x powr a < y powr a"
  12.251    by (simp add: powr_def)
  12.252  
  12.253 -
  12.254  lemma powr_less_mono2_neg:
  12.255    fixes x::real shows "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a"
  12.256    by (simp add: powr_def)
  12.257  
  12.258  lemma powr_mono2:
  12.259 -  fixes x::real shows "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
  12.260 +  fixes x::real shows "0 <= a ==> 0 \<le> x ==> x <= y ==> x powr a <= y powr a"
  12.261    apply (case_tac "a = 0", simp)
  12.262    apply (case_tac "x = y", simp)
  12.263 -  apply (metis less_eq_real_def powr_less_mono2)
  12.264 +  apply (metis dual_order.strict_iff_order powr_less_mono2)
  12.265    done
  12.266  
  12.267  lemma powr_inj:
  12.268    fixes x::real shows "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
  12.269    unfolding powr_def exp_inj_iff by simp
  12.270  
  12.271 +lemma powr_half_sqrt: "0 \<le> x \<Longrightarrow> x powr (1/2) = sqrt x"
  12.272 +  by (simp add: powr_def root_powr_inverse sqrt_def)
  12.273 +
  12.274  lemma ln_powr_bound:
  12.275    fixes x::real shows "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
  12.276  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)
  12.277 @@ -2316,28 +2498,31 @@
  12.278    finally show ?thesis .
  12.279  qed
  12.280  
  12.281 -lemma tendsto_powr [tendsto_intros]:  (*FIXME a mess, suggests a general rule about exceptions*)
  12.282 +lemma tendsto_powr [tendsto_intros]: 
  12.283    fixes a::real 
  12.284 -  shows "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
  12.285 -  apply (simp add: powr_def)
  12.286 -  apply (simp add: tendsto_def)
  12.287 -  apply (simp add: eventually_conj_iff )
  12.288 -  apply safe
  12.289 -  apply (case_tac "0 \<in> S")
  12.290 -  apply (auto simp: )
  12.291 -  apply (subgoal_tac "\<exists>T. open T & a : T & 0 \<notin> T")
  12.292 -  apply clarify
  12.293 -  apply (drule_tac x="T" in spec)
  12.294 -  apply (simp add: )
  12.295 -  apply (metis (mono_tags, lifting) eventually_mono)
  12.296 -  apply (simp add: separation_t1)
  12.297 -  apply (subgoal_tac "((\<lambda>x. exp (g x * ln (f x))) ---> exp (b * ln a)) F")
  12.298 -  apply (simp add: tendsto_def)
  12.299 -  apply (metis (mono_tags, lifting) eventually_mono)
  12.300 -  apply (simp add: tendsto_def [symmetric])
  12.301 -  apply (intro tendsto_intros)
  12.302 -  apply (auto simp: )
  12.303 -  done
  12.304 +  assumes f: "(f ---> a) F" and g: "(g ---> b) F" and a: "a \<noteq> 0"
  12.305 +  shows "((\<lambda>x. f x powr g x) ---> a powr b) F"
  12.306 +proof -
  12.307 +  { fix S :: "real set"
  12.308 +    obtain T where "open T" "a \<in> T" "0 \<notin> T"
  12.309 +      using t1_space a by blast
  12.310 +    then have "eventually (\<lambda>x. f x = 0 \<longrightarrow> 0 \<in> S) F"
  12.311 +      using f
  12.312 +      by (simp add: tendsto_def) (metis (mono_tags, lifting) eventually_mono)
  12.313 +  }
  12.314 +  moreover
  12.315 +  { fix S :: "real set"
  12.316 +    assume S: "open S" "exp (b * ln a) \<in> S"
  12.317 +    then have "((\<lambda>x. exp (g x * ln (f x))) ---> exp (b * ln a)) F"
  12.318 +    using f g a
  12.319 +      by (intro tendsto_intros) auto
  12.320 +    then have "eventually (\<lambda>x. f x \<noteq> 0 \<longrightarrow> exp (g x * ln (f x)) \<in> S) F"
  12.321 +      using f S
  12.322 +      by (simp add: tendsto_def) (metis (mono_tags, lifting) eventually_mono)
  12.323 +  }
  12.324 +  ultimately show ?thesis using assms
  12.325 +    by (simp add: powr_def tendsto_def eventually_conj_iff)
  12.326 +qed
  12.327  
  12.328  lemma continuous_powr:
  12.329    assumes "continuous F f"