src/HOL/Limits.thy
 changeset 50347 77e3effa50b6 parent 50346 a75c6429c3c3 child 50419 3177d0374701
```     1.1 --- a/src/HOL/Limits.thy	Tue Dec 04 18:00:31 2012 +0100
1.2 +++ b/src/HOL/Limits.thy	Tue Dec 04 18:00:37 2012 +0100
1.3 @@ -413,6 +413,12 @@
1.4  lemma within_empty [simp]: "F within {} = bot"
1.5    unfolding filter_eq_iff eventually_within by simp
1.6
1.7 +lemma within_within_eq: "(F within S) within T = F within (S \<inter> T)"
1.8 +  by (auto simp: filter_eq_iff eventually_within elim: eventually_elim1)
1.9 +
1.10 +lemma at_within_eq: "at x within T = nhds x within (T - {x})"
1.11 +  unfolding at_def within_within_eq by (simp add: ac_simps Diff_eq)
1.12 +
1.13  lemma within_le: "F within S \<le> F"
1.14    unfolding le_filter_def eventually_within by (auto elim: eventually_elim1)
1.15
1.16 @@ -1345,37 +1351,79 @@
1.17    apply (auto simp: natceiling_le_eq)
1.18    done
1.19
1.20 -lemma filterlim_inverse_at_top_pos:
1.21 -  "LIM x (nhds 0 within {0::real <..}). inverse x :> at_top"
1.22 -  unfolding filterlim_at_top_gt[where c=0] eventually_within
1.23 -proof safe
1.24 -  fix Z :: real assume [arith]: "0 < Z"
1.25 -  then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)"
1.26 -    by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
1.27 -  then show "eventually (\<lambda>x. x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
1.28 -    by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
1.29 -qed
1.30 +subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
1.31 +
1.32 +text {*
1.33 +
1.34 +This lemmas are useful for conversion between @{term "at x"} to @{term "at_left x"} and
1.35 +@{term "at_right x"} and also @{term "at_right 0"}.
1.36 +
1.37 +*}
1.38 +
1.39 +lemma at_eq_sup_left_right: "at (x::real) = sup (at_left x) (at_right x)"
1.40 +  by (auto simp: eventually_within at_def filter_eq_iff eventually_sup
1.41 +           elim: eventually_elim2 eventually_elim1)
1.42 +
1.43 +lemma filterlim_split_at_real:
1.44 +  "filterlim f F (at_left x) \<Longrightarrow> filterlim f F (at_right x) \<Longrightarrow> filterlim f F (at (x::real))"
1.45 +  by (subst at_eq_sup_left_right) (rule filterlim_sup)
1.46
1.47 -lemma filterlim_inverse_at_top:
1.48 -  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
1.49 -  by (intro filterlim_compose[OF filterlim_inverse_at_top_pos])
1.50 -     (simp add: filterlim_def eventually_filtermap le_within_iff)
1.51 +lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::real)"
1.52 +  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
1.53 +  by (intro allI ex_cong) (auto simp: dist_real_def field_simps)
1.54 +
1.55 +lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::real)"
1.56 +  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
1.57 +  apply (intro allI ex_cong)
1.58 +  apply (auto simp: dist_real_def field_simps)
1.59 +  apply (erule_tac x="-x" in allE)
1.60 +  apply simp
1.61 +  done
1.62 +
1.63 +lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::real)"
1.64 +  unfolding at_def filtermap_nhds_shift[symmetric]
1.65 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
1.66 +
1.67 +lemma filtermap_at_right_shift: "filtermap (\<lambda>x. x - d) (at_right a) = at_right (a - d::real)"
1.68 +  unfolding filtermap_at_shift[symmetric]
1.69 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
1.70
1.71 -lemma filterlim_inverse_at_bot_neg:
1.72 -  "LIM x (nhds 0 within {..< 0::real}). inverse x :> at_bot"
1.73 -  unfolding filterlim_at_bot_lt[where c=0] eventually_within
1.74 -proof safe
1.75 -  fix Z :: real assume [arith]: "Z < 0"
1.76 -  have "eventually (\<lambda>x. inverse Z < x) (nhds 0)"
1.77 -    by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
1.78 -  then show "eventually (\<lambda>x. x \<in> {..< 0} \<longrightarrow> inverse x \<le> Z) (nhds 0)"
1.79 -    by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
1.80 -qed
1.81 +lemma at_right_to_0: "at_right (a::real) = filtermap (\<lambda>x. x + a) (at_right 0)"
1.82 +  using filtermap_at_right_shift[of "-a" 0] by simp
1.83 +
1.84 +lemma filterlim_at_right_to_0:
1.85 +  "filterlim f F (at_right (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at_right 0)"
1.86 +  unfolding filterlim_def filtermap_filtermap at_right_to_0[of a] ..
1.87 +
1.88 +lemma eventually_at_right_to_0:
1.89 +  "eventually P (at_right (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at_right 0)"
1.90 +  unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
1.91 +
1.92 +lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::real)"
1.93 +  unfolding at_def filtermap_nhds_minus[symmetric]
1.94 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
1.95 +
1.96 +lemma at_left_minus: "at_left (a::real) = filtermap (\<lambda>x. - x) (at_right (- a))"
1.97 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
1.98
1.99 -lemma filterlim_inverse_at_bot:
1.100 -  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. f x < 0) F \<Longrightarrow> LIM x F. inverse (f x) :> at_bot"
1.101 -  by (intro filterlim_compose[OF filterlim_inverse_at_bot_neg])
1.102 -     (simp add: filterlim_def eventually_filtermap le_within_iff)
1.103 +lemma at_right_minus: "at_right (a::real) = filtermap (\<lambda>x. - x) (at_left (- a))"
1.104 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
1.105 +
1.106 +lemma filterlim_at_left_to_right:
1.107 +  "filterlim f F (at_left (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
1.108 +  unfolding filterlim_def filtermap_filtermap at_left_minus[of a] ..
1.109 +
1.110 +lemma eventually_at_left_to_right:
1.111 +  "eventually P (at_left (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (- x)) (at_right (-a))"
1.112 +  unfolding at_left_minus[of a] by (simp add: eventually_filtermap)
1.113 +
1.114 +lemma filterlim_at_split:
1.115 +  "filterlim f F (at (x::real)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)"
1.116 +  by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)
1.117 +
1.118 +lemma eventually_at_split:
1.119 +  "eventually P (at (x::real)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
1.120 +  by (subst at_eq_sup_left_right) (simp add: eventually_sup)
1.121
1.122  lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)"
1.123    unfolding filter_eq_iff eventually_filtermap eventually_at_top_linorder eventually_at_bot_linorder
1.124 @@ -1406,6 +1454,30 @@
1.125  lemma filterlim_uminus_at_bot: "(LIM x F. f x :> at_bot) \<longleftrightarrow> (LIM x F. - (f x) :: real :> at_top)"
1.126    unfolding filterlim_uminus_at_top by simp
1.127
1.128 +lemma filterlim_inverse_at_top_right: "LIM x at_right (0::real). inverse x :> at_top"
1.129 +  unfolding filterlim_at_top_gt[where c=0] eventually_within at_def
1.130 +proof safe
1.131 +  fix Z :: real assume [arith]: "0 < Z"
1.132 +  then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)"
1.133 +    by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
1.134 +  then show "eventually (\<lambda>x. x \<in> - {0} \<longrightarrow> x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
1.135 +    by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
1.136 +qed
1.137 +
1.138 +lemma filterlim_inverse_at_top:
1.139 +  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
1.140 +  by (intro filterlim_compose[OF filterlim_inverse_at_top_right])
1.141 +     (simp add: filterlim_def eventually_filtermap le_within_iff at_def eventually_elim1)
1.142 +
1.143 +lemma filterlim_inverse_at_bot_neg:
1.144 +  "LIM x (at_left (0::real)). inverse x :> at_bot"
1.145 +  by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right)
1.146 +
1.147 +lemma filterlim_inverse_at_bot:
1.148 +  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. f x < 0) F \<Longrightarrow> LIM x F. inverse (f x) :> at_bot"
1.149 +  unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric]
1.150 +  by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric])
1.151 +
1.152  lemma tendsto_inverse_0:
1.153    fixes x :: "_ \<Rightarrow> 'a\<Colon>real_normed_div_algebra"
1.154    shows "(inverse ---> (0::'a)) at_infinity"
1.155 @@ -1422,6 +1494,39 @@
1.156    qed
1.157  qed
1.158
1.159 +lemma at_right_to_top: "(at_right (0::real)) = filtermap inverse at_top"
1.160 +proof (rule antisym)
1.161 +  have "(inverse ---> (0::real)) at_top"
1.162 +    by (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl)
1.163 +  then show "filtermap inverse at_top \<le> at_right (0::real)"
1.164 +    unfolding at_within_eq
1.165 +    by (intro le_withinI) (simp_all add: eventually_filtermap eventually_gt_at_top filterlim_def)
1.166 +next
1.167 +  have "filtermap inverse (filtermap inverse (at_right (0::real))) \<le> filtermap inverse at_top"
1.168 +    using filterlim_inverse_at_top_right unfolding filterlim_def by (rule filtermap_mono)
1.169 +  then show "at_right (0::real) \<le> filtermap inverse at_top"
1.170 +    by (simp add: filtermap_ident filtermap_filtermap)
1.171 +qed
1.172 +
1.173 +lemma eventually_at_right_to_top:
1.174 +  "eventually P (at_right (0::real)) \<longleftrightarrow> eventually (\<lambda>x. P (inverse x)) at_top"
1.175 +  unfolding at_right_to_top eventually_filtermap ..
1.176 +
1.177 +lemma filterlim_at_right_to_top:
1.178 +  "filterlim f F (at_right (0::real)) \<longleftrightarrow> (LIM x at_top. f (inverse x) :> F)"
1.179 +  unfolding filterlim_def at_right_to_top filtermap_filtermap ..
1.180 +
1.181 +lemma at_top_to_right: "at_top = filtermap inverse (at_right (0::real))"
1.182 +  unfolding at_right_to_top filtermap_filtermap inverse_inverse_eq filtermap_ident ..
1.183 +
1.184 +lemma eventually_at_top_to_right:
1.185 +  "eventually P at_top \<longleftrightarrow> eventually (\<lambda>x. P (inverse x)) (at_right (0::real))"
1.186 +  unfolding at_top_to_right eventually_filtermap ..
1.187 +
1.188 +lemma filterlim_at_top_to_right:
1.189 +  "filterlim f F at_top \<longleftrightarrow> (LIM x (at_right (0::real)). f (inverse x) :> F)"
1.190 +  unfolding filterlim_def at_top_to_right filtermap_filtermap ..
1.191 +
1.192  lemma filterlim_inverse_at_infinity:
1.193    fixes x :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
1.194    shows "filterlim inverse at_infinity (at (0::'a))"
1.195 @@ -1520,6 +1625,14 @@
1.196      by eventually_elim simp
1.197  qed
1.198
1.199 +lemma LIM_at_top_divide:
1.200 +  fixes f g :: "'a \<Rightarrow> real"
1.201 +  assumes f: "(f ---> a) F" "0 < a"
1.202 +  assumes g: "(g ---> 0) F" "eventually (\<lambda>x. 0 < g x) F"
1.203 +  shows "LIM x F. f x / g x :> at_top"
1.204 +  unfolding divide_inverse
1.205 +  by (rule filterlim_tendsto_pos_mult_at_top[OF f]) (rule filterlim_inverse_at_top[OF g])
1.206 +
1.208    assumes f: "LIM x F. f x :> at_top"
1.209    assumes g: "LIM x F. g x :> at_top"
1.210 @@ -1573,79 +1686,5 @@
1.211      by (auto simp: norm_power)
1.212  qed simp
1.213
1.214 -subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
1.215 -
1.216 -text {*
1.217 -
1.218 -This lemmas are useful for conversion between @{term "at x"} to @{term "at_left x"} and
1.219 -@{term "at_right x"} and also @{term "at_right 0"}.
1.220 -
1.221 -*}
1.222 -
1.223 -lemma at_eq_sup_left_right: "at (x::real) = sup (at_left x) (at_right x)"
1.224 -  by (auto simp: eventually_within at_def filter_eq_iff eventually_sup
1.225 -           elim: eventually_elim2 eventually_elim1)
1.226 -
1.227 -lemma filterlim_split_at_real:
1.228 -  "filterlim f F (at_left x) \<Longrightarrow> filterlim f F (at_right x) \<Longrightarrow> filterlim f F (at (x::real))"
1.229 -  by (subst at_eq_sup_left_right) (rule filterlim_sup)
1.230 -
1.231 -lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::real)"
1.232 -  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
1.233 -  by (intro allI ex_cong) (auto simp: dist_real_def field_simps)
1.234 -
1.235 -lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::real)"
1.236 -  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
1.237 -  apply (intro allI ex_cong)
1.238 -  apply (auto simp: dist_real_def field_simps)
1.239 -  apply (erule_tac x="-x" in allE)
1.240 -  apply simp
1.241 -  done
1.242 -
1.243 -lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::real)"
1.244 -  unfolding at_def filtermap_nhds_shift[symmetric]
1.245 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
1.246 -
1.247 -lemma filtermap_at_right_shift: "filtermap (\<lambda>x. x - d) (at_right a) = at_right (a - d::real)"
1.248 -  unfolding filtermap_at_shift[symmetric]
1.249 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
1.250 -
1.251 -lemma at_right_to_0: "at_right (a::real) = filtermap (\<lambda>x. x + a) (at_right 0)"
1.252 -  using filtermap_at_right_shift[of "-a" 0] by simp
1.253 -
1.254 -lemma filterlim_at_right_to_0:
1.255 -  "filterlim f F (at_right (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at_right 0)"
1.256 -  unfolding filterlim_def filtermap_filtermap at_right_to_0[of a] ..
1.257 -
1.258 -lemma eventually_at_right_to_0:
1.259 -  "eventually P (at_right (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at_right 0)"
1.260 -  unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
1.261 -
1.262 -lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::real)"
1.263 -  unfolding at_def filtermap_nhds_minus[symmetric]
1.264 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
1.265 -
1.266 -lemma at_left_minus: "at_left (a::real) = filtermap (\<lambda>x. - x) (at_right (- a))"
1.267 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
1.268 -
1.269 -lemma at_right_minus: "at_right (a::real) = filtermap (\<lambda>x. - x) (at_left (- a))"
1.270 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
1.271 -
1.272 -lemma filterlim_at_left_to_right:
1.273 -  "filterlim f F (at_left (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
1.274 -  unfolding filterlim_def filtermap_filtermap at_left_minus[of a] ..
1.275 -
1.276 -lemma eventually_at_left_to_right:
1.277 -  "eventually P (at_left (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (- x)) (at_right (-a))"
1.278 -  unfolding at_left_minus[of a] by (simp add: eventually_filtermap)
1.279 -
1.280 -lemma filterlim_at_split:
1.281 -  "filterlim f F (at (x::real)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)"
1.282 -  by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)
1.283 -
1.284 -lemma eventually_at_split:
1.285 -  "eventually P (at (x::real)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
1.286 -  by (subst at_eq_sup_left_right) (simp add: eventually_sup)
1.287 -
1.288  end
1.289
```