src/HOL/Limits.thy
changeset 50330 d0b12171118e
parent 50327 bbea2e82871c
child 50331 4b6dc5077e98
     1.1 --- a/src/HOL/Limits.thy	Mon Dec 03 18:19:09 2012 +0100
     1.2 +++ b/src/HOL/Limits.thy	Mon Dec 03 18:19:11 2012 +0100
     1.3 @@ -280,6 +280,9 @@
     1.4  lemma filtermap_bot [simp]: "filtermap f bot = bot"
     1.5    by (simp add: filter_eq_iff eventually_filtermap)
     1.6  
     1.7 +lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
     1.8 +  by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)
     1.9 +
    1.10  subsection {* Order filters *}
    1.11  
    1.12  definition at_top :: "('a::order) filter"
    1.13 @@ -703,6 +706,13 @@
    1.14      by (auto simp: le_filter_def eventually_filtermap eventually_within elim!: allE[of _ "\<lambda>x. x \<in> S"])
    1.15  qed (auto intro: within_le order_trans simp: le_within_iff eventually_filtermap)
    1.16  
    1.17 +lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
    1.18 +  unfolding filterlim_def filtermap_filtermap ..
    1.19 +
    1.20 +lemma filterlim_sup:
    1.21 +  "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
    1.22 +  unfolding filterlim_def filtermap_sup by auto
    1.23 +
    1.24  abbreviation (in topological_space)
    1.25    tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
    1.26    "(f ---> l) F \<equiv> filterlim f (nhds l) F"
    1.27 @@ -915,6 +925,11 @@
    1.28    shows "((\<lambda>x. - f x) ---> - a) F \<Longrightarrow> (f ---> a) F"
    1.29    by (drule tendsto_minus, simp)
    1.30  
    1.31 +lemma tendsto_minus_cancel_left:
    1.32 +    "(f ---> - (y::_::real_normed_vector)) F \<longleftrightarrow> ((\<lambda>x. - f x) ---> y) F"
    1.33 +  using tendsto_minus_cancel[of f "- y" F]  tendsto_minus[of f "- y" F]
    1.34 +  by auto
    1.35 +
    1.36  lemma tendsto_diff [tendsto_intros]:
    1.37    fixes a b :: "'a::real_normed_vector"
    1.38    shows "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) F"
    1.39 @@ -1367,5 +1382,79 @@
    1.40      by eventually_elim simp
    1.41  qed
    1.42  
    1.43 +subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
    1.44 +
    1.45 +text {*
    1.46 +
    1.47 +This lemmas are useful for conversion between @{term "at x"} to @{term "at_left x"} and
    1.48 +@{term "at_right x"} and also @{term "at_right 0"}.
    1.49 +
    1.50 +*}
    1.51 +
    1.52 +lemma at_eq_sup_left_right: "at (x::real) = sup (at_left x) (at_right x)"
    1.53 +  by (auto simp: eventually_within at_def filter_eq_iff eventually_sup 
    1.54 +           elim: eventually_elim2 eventually_elim1)
    1.55 +
    1.56 +lemma filterlim_split_at_real:
    1.57 +  "filterlim f F (at_left x) \<Longrightarrow> filterlim f F (at_right x) \<Longrightarrow> filterlim f F (at (x::real))"
    1.58 +  by (subst at_eq_sup_left_right) (rule filterlim_sup)
    1.59 +
    1.60 +lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::real)"
    1.61 +  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
    1.62 +  by (intro allI ex_cong) (auto simp: dist_real_def field_simps)
    1.63 +
    1.64 +lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::real)"
    1.65 +  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
    1.66 +  apply (intro allI ex_cong)
    1.67 +  apply (auto simp: dist_real_def field_simps)
    1.68 +  apply (erule_tac x="-x" in allE)
    1.69 +  apply simp
    1.70 +  done
    1.71 +
    1.72 +lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::real)"
    1.73 +  unfolding at_def filtermap_nhds_shift[symmetric]
    1.74 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
    1.75 +
    1.76 +lemma filtermap_at_right_shift: "filtermap (\<lambda>x. x - d) (at_right a) = at_right (a - d::real)"
    1.77 +  unfolding filtermap_at_shift[symmetric]
    1.78 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
    1.79 +
    1.80 +lemma at_right_to_0: "at_right (a::real) = filtermap (\<lambda>x. x + a) (at_right 0)"
    1.81 +  using filtermap_at_right_shift[of "-a" 0] by simp
    1.82 +
    1.83 +lemma filterlim_at_right_to_0:
    1.84 +  "filterlim f F (at_right (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at_right 0)"
    1.85 +  unfolding filterlim_def filtermap_filtermap at_right_to_0[of a] ..
    1.86 +
    1.87 +lemma eventually_at_right_to_0:
    1.88 +  "eventually P (at_right (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at_right 0)"
    1.89 +  unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
    1.90 +
    1.91 +lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::real)"
    1.92 +  unfolding at_def filtermap_nhds_minus[symmetric]
    1.93 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
    1.94 +
    1.95 +lemma at_left_minus: "at_left (a::real) = filtermap (\<lambda>x. - x) (at_right (- a))"
    1.96 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
    1.97 +
    1.98 +lemma at_right_minus: "at_right (a::real) = filtermap (\<lambda>x. - x) (at_left (- a))"
    1.99 +  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
   1.100 +
   1.101 +lemma filterlim_at_left_to_right:
   1.102 +  "filterlim f F (at_left (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
   1.103 +  unfolding filterlim_def filtermap_filtermap at_left_minus[of a] ..
   1.104 +
   1.105 +lemma eventually_at_left_to_right:
   1.106 +  "eventually P (at_left (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (- x)) (at_right (-a))"
   1.107 +  unfolding at_left_minus[of a] by (simp add: eventually_filtermap)
   1.108 +
   1.109 +lemma filterlim_at_split:
   1.110 +  "filterlim f F (at (x::real)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)"
   1.111 +  by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)
   1.112 +
   1.113 +lemma eventually_at_split:
   1.114 +  "eventually P (at (x::real)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
   1.115 +  by (subst at_eq_sup_left_right) (simp add: eventually_sup)
   1.116 +
   1.117  end
   1.118