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.207  lemma filterlim_at_top_add_at_top: 
   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