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