src/HOL/Limits.thy
 changeset 51641 cd05e9fcc63d parent 51531 f415febf4234 child 51642 400ec5ae7f8f
```     1.1 --- a/src/HOL/Limits.thy	Mon Apr 08 21:01:59 2013 +0200
1.2 +++ b/src/HOL/Limits.thy	Tue Apr 09 14:04:41 2013 +0200
1.3 @@ -12,10 +12,6 @@
1.4  imports Real_Vector_Spaces
1.5  begin
1.6
1.7 -(* Unfortunately eventually_within was overwritten by Multivariate_Analysis.
1.8 -   Hence it was references as Limits.eventually_within, but now it is Basic_Topology.eventually_within *)
1.9 -lemmas eventually_within = eventually_within
1.10 -
1.11  subsection {* Filter going to infinity norm *}
1.12
1.13  definition at_infinity :: "'a::real_normed_vector filter" where
1.14 @@ -910,25 +906,36 @@
1.15
1.16  lemmas filterlim_split_at_real = filterlim_split_at[where 'a=real]
1.17
1.18 -lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::real)"
1.19 -  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
1.20 -  by (intro allI ex_cong) (auto simp: dist_real_def field_simps)
1.21 +lemma filtermap_homeomorph:
1.22 +  assumes f: "continuous (at a) f"
1.23 +  assumes g: "continuous (at (f a)) g"
1.24 +  assumes bij1: "\<forall>x. f (g x) = x" and bij2: "\<forall>x. g (f x) = x"
1.25 +  shows "filtermap f (nhds a) = nhds (f a)"
1.26 +  unfolding filter_eq_iff eventually_filtermap eventually_nhds
1.27 +proof safe
1.28 +  fix P S assume S: "open S" "f a \<in> S" and P: "\<forall>x\<in>S. P x"
1.29 +  from continuous_within_topological[THEN iffD1, rule_format, OF f S] P
1.30 +  show "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P (f x))" by auto
1.31 +next
1.32 +  fix P S assume S: "open S" "a \<in> S" and P: "\<forall>x\<in>S. P (f x)"
1.33 +  with continuous_within_topological[THEN iffD1, rule_format, OF g, of S] bij2
1.34 +  obtain A where "open A" "f a \<in> A" "(\<forall>y\<in>A. g y \<in> S)"
1.35 +    by (metis UNIV_I)
1.36 +  with P bij1 show "\<exists>S. open S \<and> f a \<in> S \<and> (\<forall>x\<in>S. P x)"
1.37 +    by (force intro!: exI[of _ A])
1.38 +qed
1.39
1.40 -lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::real)"
1.41 -  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
1.42 -  apply (intro allI ex_cong)
1.43 -  apply (auto simp: dist_real_def field_simps)
1.44 -  apply (erule_tac x="-x" in allE)
1.45 -  apply simp
1.46 -  done
1.47 +lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::'a::real_normed_vector)"
1.48 +  by (rule filtermap_homeomorph[where g="\<lambda>x. x + d"]) (auto intro: continuous_intros)
1.49
1.50 -lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::real)"
1.51 -  unfolding at_def filtermap_nhds_shift[symmetric]
1.52 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
1.53 +lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::'a::real_normed_vector)"
1.54 +  by (rule filtermap_homeomorph[where g=uminus]) (auto intro: continuous_minus)
1.55 +
1.56 +lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::'a::real_normed_vector)"
1.57 +  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])
1.58
1.59  lemma filtermap_at_right_shift: "filtermap (\<lambda>x. x - d) (at_right a) = at_right (a - d::real)"
1.60 -  unfolding filtermap_at_shift[symmetric]
1.61 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
1.62 +  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])
1.63
1.64  lemma at_right_to_0: "at_right (a::real) = filtermap (\<lambda>x. x + a) (at_right 0)"
1.65    using filtermap_at_right_shift[of "-a" 0] by simp
1.66 @@ -941,15 +948,14 @@
1.67    "eventually P (at_right (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at_right 0)"
1.68    unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
1.69
1.70 -lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::real)"
1.71 -  unfolding at_def filtermap_nhds_minus[symmetric]
1.72 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
1.73 +lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::'a::real_normed_vector)"
1.74 +  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
1.75
1.76  lemma at_left_minus: "at_left (a::real) = filtermap (\<lambda>x. - x) (at_right (- a))"
1.77 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
1.78 +  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
1.79
1.80  lemma at_right_minus: "at_right (a::real) = filtermap (\<lambda>x. - x) (at_left (- a))"
1.81 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
1.82 +  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
1.83
1.84  lemma filterlim_at_left_to_right:
1.85    "filterlim f F (at_left (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
1.86 @@ -989,19 +995,19 @@
1.87    unfolding filterlim_uminus_at_top by simp
1.88
1.89  lemma filterlim_inverse_at_top_right: "LIM x at_right (0::real). inverse x :> at_top"
1.90 -  unfolding filterlim_at_top_gt[where c=0] eventually_within at_def
1.91 +  unfolding filterlim_at_top_gt[where c=0] eventually_at_filter
1.92  proof safe
1.93    fix Z :: real assume [arith]: "0 < Z"
1.94    then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)"
1.95      by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
1.96 -  then show "eventually (\<lambda>x. x \<in> - {0} \<longrightarrow> x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
1.97 +  then show "eventually (\<lambda>x. x \<noteq> 0 \<longrightarrow> x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
1.98      by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
1.99  qed
1.100
1.101  lemma filterlim_inverse_at_top:
1.102    "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
1.103    by (intro filterlim_compose[OF filterlim_inverse_at_top_right])
1.104 -     (simp add: filterlim_def eventually_filtermap le_within_iff at_def eventually_elim1)
1.105 +     (simp add: filterlim_def eventually_filtermap eventually_elim1 at_within_def le_principal)
1.106
1.107  lemma filterlim_inverse_at_bot_neg:
1.108    "LIM x (at_left (0::real)). inverse x :> at_bot"
1.109 @@ -1033,8 +1039,7 @@
1.110    have "(inverse ---> (0::real)) at_top"
1.111      by (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl)
1.112    then show "filtermap inverse at_top \<le> at_right (0::real)"
1.113 -    unfolding at_within_eq
1.114 -    by (intro le_withinI) (simp_all add: eventually_filtermap eventually_gt_at_top filterlim_def)
1.115 +    by (simp add: le_principal eventually_filtermap eventually_gt_at_top filterlim_def at_within_def)
1.116  next
1.117    have "filtermap inverse (filtermap inverse (at_right (0::real))) \<le> filtermap inverse at_top"
1.118      using filterlim_inverse_at_top_right unfolding filterlim_def by (rule filtermap_mono)
1.119 @@ -1082,9 +1087,9 @@
1.120    then have "filtermap inverse (filtermap g F) \<le> filtermap inverse at_infinity"
1.121      by (rule filtermap_mono)
1.122    also have "\<dots> \<le> at 0"
1.123 -    using tendsto_inverse_0
1.124 -    by (auto intro!: le_withinI exI[of _ 1]
1.125 -             simp: eventually_filtermap eventually_at_infinity filterlim_def at_def)
1.126 +    using tendsto_inverse_0[where 'a='b]
1.127 +    by (auto intro!: exI[of _ 1]
1.128 +             simp: le_principal eventually_filtermap filterlim_def at_within_def eventually_at_infinity)
1.129    finally show "filtermap inverse (filtermap g F) \<le> at 0" .
1.130  next
1.131    assume "filtermap inverse (filtermap g F) \<le> at 0"
1.132 @@ -1094,9 +1099,8 @@
1.133      by (auto intro: order_trans simp: filterlim_def filtermap_filtermap)
1.134  qed
1.135
1.136 -lemma tendsto_inverse_0_at_top:
1.137 -  "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
1.138 - by (metis at_top_le_at_infinity filterlim_at filterlim_inverse_at_iff filterlim_mono order_refl)
1.139 +lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
1.140 + by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
1.141
1.142  text {*
1.143
1.144 @@ -1516,13 +1520,7 @@
1.145  lemma LIM_offset:
1.146    fixes a :: "'a::real_normed_vector"
1.147    shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
1.148 -apply (rule topological_tendstoI)
1.149 -apply (drule (2) topological_tendstoD)
1.150 -apply (simp only: eventually_at dist_norm)
1.151 -apply (clarify, rule_tac x=d in exI, safe)
1.152 -apply (drule_tac x="x + k" in spec)
1.153 -apply (simp add: algebra_simps)
1.154 -done
1.155 +  unfolding filtermap_at_shift[symmetric, of a k] filterlim_def filtermap_filtermap by simp
1.156
1.157  lemma LIM_offset_zero:
1.158    fixes a :: "'a::real_normed_vector"
1.159 @@ -1717,7 +1715,7 @@
1.160    show "(f ---> f x) (at_left x)"
1.161      using `isCont f x` by (simp add: filterlim_at_split isCont_def)
1.162    show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
1.163 -    using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"])
1.164 +    using ev by (auto simp: eventually_at dist_real_def intro!: exI[of _ "x - b"])
1.165  qed simp
1.166
1.167
```