src/HOL/Limits.thy
changeset 62087 44841d07ef1d
parent 61976 3a27957ac658
child 62101 26c0a70f78a3
     1.1 --- a/src/HOL/Limits.thy	Wed Jan 06 16:17:50 2016 +0100
     1.2 +++ b/src/HOL/Limits.thy	Thu Jan 07 17:40:55 2016 +0000
     1.3 @@ -137,7 +137,7 @@
     1.4      by (auto elim!: allE[of _ n])
     1.5  qed
     1.6  
     1.7 -lemma Bseq_bdd_above': 
     1.8 +lemma Bseq_bdd_above':
     1.9    "Bseq (X::nat \<Rightarrow> 'a :: real_normed_vector) \<Longrightarrow> bdd_above (range (\<lambda>n. norm (X n)))"
    1.10  proof (elim BseqE, intro bdd_aboveI2)
    1.11    fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "norm (X n) \<le> K"
    1.12 @@ -152,7 +152,7 @@
    1.13  
    1.14  lemma Bseq_eventually_mono:
    1.15    assumes "eventually (\<lambda>n. norm (f n) \<le> norm (g n)) sequentially" "Bseq g"
    1.16 -  shows   "Bseq f" 
    1.17 +  shows   "Bseq f"
    1.18  proof -
    1.19    from assms(1) obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> norm (f n) \<le> norm (g n)"
    1.20      by (auto simp: eventually_at_top_linorder)
    1.21 @@ -162,7 +162,7 @@
    1.22      apply (rule max.coboundedI2, rule Max.coboundedI, auto) []
    1.23      apply (rule max.coboundedI1, force intro: order.trans[OF N K])
    1.24      done
    1.25 -  thus ?thesis by (blast intro: BseqI') 
    1.26 +  thus ?thesis by (blast intro: BseqI')
    1.27  qed
    1.28  
    1.29  lemma lemma_NBseq_def:
    1.30 @@ -243,7 +243,7 @@
    1.31  lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
    1.32    by (simp add: Bseq_def)
    1.33  
    1.34 -lemma Bseq_add: 
    1.35 +lemma Bseq_add:
    1.36    assumes "Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
    1.37    shows   "Bseq (\<lambda>x. f x + c)"
    1.38  proof -
    1.39 @@ -260,12 +260,12 @@
    1.40  lemma Bseq_add_iff: "Bseq (\<lambda>x. f x + c) \<longleftrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
    1.41    using Bseq_add[of f c] Bseq_add[of "\<lambda>x. f x + c" "-c"] by auto
    1.42  
    1.43 -lemma Bseq_mult: 
    1.44 +lemma Bseq_mult:
    1.45    assumes "Bseq (f :: nat \<Rightarrow> 'a :: real_normed_field)"
    1.46    assumes "Bseq (g :: nat \<Rightarrow> 'a :: real_normed_field)"
    1.47    shows   "Bseq (\<lambda>x. f x * g x)"
    1.48  proof -
    1.49 -  from assms obtain K1 K2 where K: "\<And>x. norm (f x) \<le> K1" "K1 > 0" "\<And>x. norm (g x) \<le> K2" "K2 > 0" 
    1.50 +  from assms obtain K1 K2 where K: "\<And>x. norm (f x) \<le> K1" "K1 > 0" "\<And>x. norm (g x) \<le> K2" "K2 > 0"
    1.51      unfolding Bseq_def by blast
    1.52    hence "\<And>x. norm (f x * g x) \<le> K1 * K2" by (auto simp: norm_mult intro!: mult_mono)
    1.53    thus ?thesis by (rule BseqI')
    1.54 @@ -794,7 +794,7 @@
    1.55  
    1.56  lemma tendsto_add_const_iff:
    1.57    "((\<lambda>x. c + f x :: 'a :: real_normed_vector) \<longlongrightarrow> c + d) F \<longleftrightarrow> (f \<longlongrightarrow> d) F"
    1.58 -  using tendsto_add[OF tendsto_const[of c], of f d] 
    1.59 +  using tendsto_add[OF tendsto_const[of c], of f d]
    1.60          tendsto_add[OF tendsto_const[of "-c"], of "\<lambda>x. c + f x" "c + d"] by auto
    1.61  
    1.62  
    1.63 @@ -1001,11 +1001,11 @@
    1.64  
    1.65  lemma not_tendsto_and_filterlim_at_infinity:
    1.66    assumes "F \<noteq> bot"
    1.67 -  assumes "(f \<longlongrightarrow> (c :: 'a :: real_normed_vector)) F" 
    1.68 +  assumes "(f \<longlongrightarrow> (c :: 'a :: real_normed_vector)) F"
    1.69    assumes "filterlim f at_infinity F"
    1.70    shows   False
    1.71  proof -
    1.72 -  from tendstoD[OF assms(2), of "1/2"] 
    1.73 +  from tendstoD[OF assms(2), of "1/2"]
    1.74      have "eventually (\<lambda>x. dist (f x) c < 1/2) F" by simp
    1.75    moreover from filterlim_at_infinity[of "norm c" f F] assms(3)
    1.76      have "eventually (\<lambda>x. norm (f x) \<ge> norm c + 1) F" by simp
    1.77 @@ -1037,7 +1037,7 @@
    1.78    thus ?thesis by eventually_elim auto
    1.79  qed
    1.80  
    1.81 -lemma tendsto_of_nat [tendsto_intros]: 
    1.82 +lemma tendsto_of_nat [tendsto_intros]:
    1.83    "filterlim (of_nat :: nat \<Rightarrow> 'a :: real_normed_algebra_1) at_infinity sequentially"
    1.84  proof (subst filterlim_at_infinity[OF order.refl], intro allI impI)
    1.85    fix r :: real assume r: "r > 0"
    1.86 @@ -1164,7 +1164,7 @@
    1.87    fix r :: real assume r: "r > 0"
    1.88    from assms(1) have "((\<lambda>x. norm (f x)) \<longlongrightarrow> norm c) F" by (rule tendsto_norm)
    1.89    hence "eventually (\<lambda>x. norm (f x) < norm c + 1) F" by (rule order_tendstoD) simp_all
    1.90 -  moreover from r have "r + norm c + 1 > 0" by (intro add_pos_nonneg) simp_all 
    1.91 +  moreover from r have "r + norm c + 1 > 0" by (intro add_pos_nonneg) simp_all
    1.92    with assms(2) have "eventually (\<lambda>x. norm (g x) \<ge> r + norm c + 1) F"
    1.93      unfolding filterlim_at_infinity[OF order_refl] by (elim allE[of _ "r + norm c + 1"]) simp_all
    1.94    ultimately show "eventually (\<lambda>x. norm (f x + g x) \<ge> r) F"
    1.95 @@ -1506,7 +1506,7 @@
    1.96  
    1.97  lemma eventually_at2:
    1.98    "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
    1.99 -  unfolding eventually_at dist_nz by auto
   1.100 +  unfolding eventually_at by auto
   1.101  
   1.102  lemma Lim_transform:
   1.103    fixes a b :: "'a::real_normed_vector"
   1.104 @@ -1526,28 +1526,16 @@
   1.105    done
   1.106  
   1.107  lemma Lim_transform_within:
   1.108 -  assumes "0 < d"
   1.109 -    and "\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
   1.110 -    and "(f \<longlongrightarrow> l) (at x within S)"
   1.111 +  assumes "(f \<longlongrightarrow> l) (at x within S)"
   1.112 +    and "0 < d"
   1.113 +    and "\<And>x'. \<lbrakk>x'\<in>S; 0 < dist x' x; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
   1.114    shows "(g \<longlongrightarrow> l) (at x within S)"
   1.115  proof (rule Lim_transform_eventually)
   1.116    show "eventually (\<lambda>x. f x = g x) (at x within S)"
   1.117 -    using assms(1,2) by (auto simp: dist_nz eventually_at)
   1.118 +    using assms by (auto simp: eventually_at)
   1.119    show "(f \<longlongrightarrow> l) (at x within S)" by fact
   1.120  qed
   1.121  
   1.122 -lemma Lim_transform_at:
   1.123 -  assumes "0 < d"
   1.124 -    and "\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
   1.125 -    and "(f \<longlongrightarrow> l) (at x)"
   1.126 -  shows "(g \<longlongrightarrow> l) (at x)"
   1.127 -  using _ assms(3)
   1.128 -proof (rule Lim_transform_eventually)
   1.129 -  show "eventually (\<lambda>x. f x = g x) (at x)"
   1.130 -    unfolding eventually_at2
   1.131 -    using assms(1,2) by auto
   1.132 -qed
   1.133 -
   1.134  text\<open>Common case assuming being away from some crucial point like 0.\<close>
   1.135  
   1.136  lemma Lim_transform_away_within:
   1.137 @@ -1574,15 +1562,15 @@
   1.138  text\<open>Alternatively, within an open set.\<close>
   1.139  
   1.140  lemma Lim_transform_within_open:
   1.141 -  assumes "open S" and "a \<in> S"
   1.142 -    and "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"
   1.143 -    and "(f \<longlongrightarrow> l) (at a)"
   1.144 -  shows "(g \<longlongrightarrow> l) (at a)"
   1.145 +  assumes "(f \<longlongrightarrow> l) (at a within T)"
   1.146 +    and "open s" and "a \<in> s"
   1.147 +    and "\<And>x. \<lbrakk>x\<in>s; x \<noteq> a\<rbrakk> \<Longrightarrow> f x = g x"
   1.148 +  shows "(g \<longlongrightarrow> l) (at a within T)"
   1.149  proof (rule Lim_transform_eventually)
   1.150 -  show "eventually (\<lambda>x. f x = g x) (at a)"
   1.151 +  show "eventually (\<lambda>x. f x = g x) (at a within T)"
   1.152      unfolding eventually_at_topological
   1.153 -    using assms(1,2,3) by auto
   1.154 -  show "(f \<longlongrightarrow> l) (at a)" by fact
   1.155 +    using assms by auto
   1.156 +  show "(f \<longlongrightarrow> l) (at a within T)" by fact
   1.157  qed
   1.158  
   1.159  text\<open>A congruence rule allowing us to transform limits assuming not at point.\<close>
   1.160 @@ -1642,7 +1630,7 @@
   1.161    fix n :: nat assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
   1.162    have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
   1.163    also note n
   1.164 -  finally show "dist (1 / of_nat n :: 'a) 0 < e" using e 
   1.165 +  finally show "dist (1 / of_nat n :: 'a) 0 < e" using e
   1.166      by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
   1.167  qed
   1.168  
   1.169 @@ -1660,9 +1648,9 @@
   1.170  
   1.171  lemma LIMSEQ_n_over_Suc_n: "(\<lambda>n. of_nat n / of_nat (Suc n) :: 'a :: real_normed_field) \<longlonglongrightarrow> 1"
   1.172  proof (rule Lim_transform_eventually)
   1.173 -  show "eventually (\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a) = 
   1.174 +  show "eventually (\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a) =
   1.175                          of_nat n / of_nat (Suc n)) sequentially"
   1.176 -    using eventually_gt_at_top[of "0::nat"] 
   1.177 +    using eventually_gt_at_top[of "0::nat"]
   1.178      by eventually_elim (simp add: field_simps del: of_nat_Suc)
   1.179    have "(\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a)) \<longlonglongrightarrow> inverse 1"
   1.180      by (intro tendsto_inverse LIMSEQ_Suc_n_over_n) simp_all
   1.181 @@ -1738,11 +1726,11 @@
   1.182    thus ?thesis by (auto simp: convergent_def)
   1.183  qed
   1.184  
   1.185 -lemma convergent_of_real: 
   1.186 +lemma convergent_of_real:
   1.187    "convergent f \<Longrightarrow> convergent (\<lambda>n. of_real (f n) :: 'a :: real_normed_algebra_1)"
   1.188    unfolding convergent_def by (blast intro!: tendsto_of_real)
   1.189  
   1.190 -lemma convergent_add_const_iff: 
   1.191 +lemma convergent_add_const_iff:
   1.192    "convergent (\<lambda>n. c + f n :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
   1.193  proof
   1.194    assume "convergent (\<lambda>n. c + f n)"
   1.195 @@ -1752,11 +1740,11 @@
   1.196    from convergent_add[OF convergent_const[of c] this] show "convergent (\<lambda>n. c + f n)" by simp
   1.197  qed
   1.198  
   1.199 -lemma convergent_add_const_right_iff: 
   1.200 +lemma convergent_add_const_right_iff:
   1.201    "convergent (\<lambda>n. f n + c :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
   1.202    using convergent_add_const_iff[of c f] by (simp add: add_ac)
   1.203  
   1.204 -lemma convergent_diff_const_right_iff: 
   1.205 +lemma convergent_diff_const_right_iff:
   1.206    "convergent (\<lambda>n. f n - c :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
   1.207    using convergent_add_const_right_iff[of f "-c"] by (simp add: add_ac)
   1.208  
   1.209 @@ -1772,7 +1760,7 @@
   1.210    shows   "convergent (\<lambda>n. c * f n :: 'a :: real_normed_field) \<longleftrightarrow> convergent f"
   1.211  proof
   1.212    assume "convergent (\<lambda>n. c * f n)"
   1.213 -  from assms convergent_mult[OF this convergent_const[of "inverse c"]] 
   1.214 +  from assms convergent_mult[OF this convergent_const[of "inverse c"]]
   1.215      show "convergent f" by (simp add: field_simps)
   1.216  next
   1.217    assume "convergent f"