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.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.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.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.201    "convergent (\<lambda>n. f n + c :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
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"