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