add filterlim rules for unary minus and inverse
authorhoelzl
Mon Dec 03 18:19:01 2012 +0100 (2012-12-03)
changeset 503233764d4620fb3
parent 50322 b06b95a5fda2
child 50324 0a1242d5e7d4
add filterlim rules for unary minus and inverse
src/HOL/Limits.thy
     1.1 --- a/src/HOL/Limits.thy	Mon Dec 03 18:18:59 2012 +0100
     1.2 +++ b/src/HOL/Limits.thy	Mon Dec 03 18:19:01 2012 +0100
     1.3 @@ -390,6 +390,12 @@
     1.4  lemma within_le: "F within S \<le> F"
     1.5    unfolding le_filter_def eventually_within by (auto elim: eventually_elim1)
     1.6  
     1.7 +lemma le_withinI: "F \<le> F' \<Longrightarrow> eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S"
     1.8 +  unfolding le_filter_def eventually_within by (auto elim: eventually_elim2)
     1.9 +
    1.10 +lemma le_within_iff: "eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S \<longleftrightarrow> F \<le> F'"
    1.11 +  by (blast intro: within_le le_withinI order_trans)
    1.12 +
    1.13  lemma eventually_nhds:
    1.14    "eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
    1.15  unfolding nhds_def
    1.16 @@ -629,6 +635,14 @@
    1.17  lemma filterlimI: "(\<And>P. eventually P F2 \<Longrightarrow> eventually (\<lambda>x. P (f x)) F1) \<Longrightarrow> (LIM x F1. f x :> F2)"
    1.18    by (auto simp: filterlim_def eventually_filtermap le_filter_def)
    1.19  
    1.20 +lemma filterlim_compose: 
    1.21 +  "filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1"
    1.22 +  unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans)
    1.23 +
    1.24 +lemma filterlim_mono: 
    1.25 +  "filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'"
    1.26 +  unfolding filterlim_def by (metis filtermap_mono order_trans)
    1.27 +
    1.28  abbreviation (in topological_space)
    1.29    tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
    1.30    "(f ---> l) F \<equiv> filterlim f (nhds l) F"
    1.31 @@ -734,36 +748,24 @@
    1.32    assumes "\<not> trivial_limit F" shows "((\<lambda>x. a) ---> b) F \<longleftrightarrow> a = b"
    1.33    by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const])
    1.34  
    1.35 +lemma tendsto_at_iff_tendsto_nhds:
    1.36 +  "(g ---> g l) (at l) \<longleftrightarrow> (g ---> g l) (nhds l)"
    1.37 +  unfolding tendsto_def at_def eventually_within
    1.38 +  by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
    1.39 +
    1.40  lemma tendsto_compose:
    1.41 -  assumes g: "(g ---> g l) (at l)"
    1.42 -  assumes f: "(f ---> l) F"
    1.43 -  shows "((\<lambda>x. g (f x)) ---> g l) F"
    1.44 -proof (rule topological_tendstoI)
    1.45 -  fix B assume B: "open B" "g l \<in> B"
    1.46 -  obtain A where A: "open A" "l \<in> A"
    1.47 -    and gB: "\<forall>y. y \<in> A \<longrightarrow> g y \<in> B"
    1.48 -    using topological_tendstoD [OF g B] B(2)
    1.49 -    unfolding eventually_at_topological by fast
    1.50 -  hence "\<forall>x. f x \<in> A \<longrightarrow> g (f x) \<in> B" by simp
    1.51 -  from this topological_tendstoD [OF f A]
    1.52 -  show "eventually (\<lambda>x. g (f x) \<in> B) F"
    1.53 -    by (rule eventually_mono)
    1.54 -qed
    1.55 +  "(g ---> g l) (at l) \<Longrightarrow> (f ---> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
    1.56 +  unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g])
    1.57  
    1.58  lemma tendsto_compose_eventually:
    1.59    assumes g: "(g ---> m) (at l)"
    1.60    assumes f: "(f ---> l) F"
    1.61    assumes inj: "eventually (\<lambda>x. f x \<noteq> l) F"
    1.62    shows "((\<lambda>x. g (f x)) ---> m) F"
    1.63 -proof (rule topological_tendstoI)
    1.64 -  fix B assume B: "open B" "m \<in> B"
    1.65 -  obtain A where A: "open A" "l \<in> A"
    1.66 -    and gB: "\<And>y. y \<in> A \<Longrightarrow> y \<noteq> l \<Longrightarrow> g y \<in> B"
    1.67 -    using topological_tendstoD [OF g B]
    1.68 -    unfolding eventually_at_topological by fast
    1.69 -  show "eventually (\<lambda>x. g (f x) \<in> B) F"
    1.70 -    using topological_tendstoD [OF f A] inj
    1.71 -    by (rule eventually_elim2) (simp add: gB)
    1.72 +proof -
    1.73 +  from f inj have "LIM x F. f x :> at l"
    1.74 +    unfolding filterlim_def at_def by (simp add: le_within_iff eventually_filtermap)
    1.75 +  from filterlim_compose[OF g this] show ?thesis .
    1.76  qed
    1.77  
    1.78  lemma metric_tendsto_imp_tendsto:
    1.79 @@ -1081,12 +1083,34 @@
    1.80    by (safe elim!: filterlimE intro!: filterlimI)
    1.81       (auto simp: eventually_at_top_dense elim!: eventually_elim1)
    1.82  
    1.83 +lemma filterlim_at_top_gt:
    1.84 +  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
    1.85 +  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z < f x) F)"
    1.86 +  unfolding filterlim_at_top
    1.87 +proof safe
    1.88 +  fix Z assume *: "\<forall>Z>c. eventually (\<lambda>x. Z < f x) F"
    1.89 +  from gt_ex[of "max Z c"] guess x ..
    1.90 +  with *[THEN spec, of x] show "eventually (\<lambda>x. Z < f x) F"
    1.91 +    by (auto elim!: eventually_elim1)
    1.92 +qed simp
    1.93 +
    1.94  lemma filterlim_at_bot: 
    1.95    fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
    1.96    shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x < Z) F)"
    1.97    by (safe elim!: filterlimE intro!: filterlimI)
    1.98       (auto simp: eventually_at_bot_dense elim!: eventually_elim1)
    1.99  
   1.100 +lemma filterlim_at_bot_lt:
   1.101 +  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
   1.102 +  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z > f x) F)"
   1.103 +  unfolding filterlim_at_bot
   1.104 +proof safe
   1.105 +  fix Z assume *: "\<forall>Z<c. eventually (\<lambda>x. Z > f x) F"
   1.106 +  from lt_ex[of "min Z c"] guess x ..
   1.107 +  with *[THEN spec, of x] show "eventually (\<lambda>x. Z > f x) F"
   1.108 +    by (auto elim!: eventually_elim1)
   1.109 +qed simp
   1.110 +
   1.111  lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top"
   1.112    unfolding filterlim_at_top
   1.113    apply (intro allI)
   1.114 @@ -1094,4 +1118,50 @@
   1.115    apply (auto simp: natceiling_le_eq)
   1.116    done
   1.117  
   1.118 +lemma filterlim_inverse_at_top_pos:
   1.119 +  "LIM x (nhds 0 within {0::real <..}). inverse x :> at_top"
   1.120 +  unfolding filterlim_at_top_gt[where c=0] eventually_within
   1.121 +proof safe
   1.122 +  fix Z :: real assume [arith]: "0 < Z"
   1.123 +  then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)"
   1.124 +    by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
   1.125 +  then show "eventually (\<lambda>x. x \<in> {0<..} \<longrightarrow> Z < inverse x) (nhds 0)"
   1.126 +    by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
   1.127 +qed
   1.128 +
   1.129 +lemma filterlim_inverse_at_top:
   1.130 +  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
   1.131 +  by (intro filterlim_compose[OF filterlim_inverse_at_top_pos])
   1.132 +     (simp add: filterlim_def eventually_filtermap le_within_iff)
   1.133 +
   1.134 +lemma filterlim_inverse_at_bot_neg:
   1.135 +  "LIM x (nhds 0 within {..< 0::real}). inverse x :> at_bot"
   1.136 +  unfolding filterlim_at_bot_lt[where c=0] eventually_within
   1.137 +proof safe
   1.138 +  fix Z :: real assume [arith]: "Z < 0"
   1.139 +  have "eventually (\<lambda>x. inverse Z < x) (nhds 0)"
   1.140 +    by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
   1.141 +  then show "eventually (\<lambda>x. x \<in> {..< 0} \<longrightarrow> inverse x < Z) (nhds 0)"
   1.142 +    by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
   1.143 +qed
   1.144 +
   1.145 +lemma filterlim_inverse_at_bot:
   1.146 +  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. f x < 0) F \<Longrightarrow> LIM x F. inverse (f x) :> at_bot"
   1.147 +  by (intro filterlim_compose[OF filterlim_inverse_at_bot_neg])
   1.148 +     (simp add: filterlim_def eventually_filtermap le_within_iff)
   1.149 +
   1.150 +lemma filterlim_uminus_at_top_at_bot: "LIM x at_bot. - x :: real :> at_top"
   1.151 +  unfolding filterlim_at_top eventually_at_bot_dense
   1.152 +  by (blast intro: less_minus_iff[THEN iffD1])
   1.153 +
   1.154 +lemma filterlim_uminus_at_top: "LIM x F. f x :> at_bot \<Longrightarrow> LIM x F. - (f x) :: real :> at_top"
   1.155 +  by (rule filterlim_compose[OF filterlim_uminus_at_top_at_bot])
   1.156 +
   1.157 +lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot"
   1.158 +  unfolding filterlim_at_bot eventually_at_top_dense
   1.159 +  by (blast intro: minus_less_iff[THEN iffD1])
   1.160 +
   1.161 +lemma filterlim_uminus_at_bot: "LIM x F. f x :> at_top \<Longrightarrow> LIM x F. - (f x) :: real :> at_bot"
   1.162 +  by (rule filterlim_compose[OF filterlim_uminus_at_bot_at_top])
   1.163 +
   1.164  end