# HG changeset patch
# User hoelzl
# Date 1354640437 -3600
# Node ID 77e3effa50b6710a414216383a6075eb7d7066d6
# Parent  a75c6429c3c36eabbba6a4c3ff41a808b9b4f928
prove tendsto_power_div_exp_0
* * *
missing rename

diff -r a75c6429c3c3 -r 77e3effa50b6 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Dec 04 18:00:31 2012 +0100
+++ b/src/HOL/Deriv.thy	Tue Dec 04 18:00:37 2012 +0100
@@ -1862,4 +1862,52 @@
   unfolding eventually_at_split filterlim_at_split
   by (auto intro!: lhopital_right_at_top[of g x g' f f'] lhopital_left_at_top[of g x g' f f'])
 
+lemma lhospital_at_top_at_top:
+  fixes f g :: "real \<Rightarrow> real"
+  assumes g_0: "LIM x at_top. g x :> at_top"
+  assumes g': "eventually (\<lambda>x. g' x \<noteq> 0) at_top"
+  assumes Df: "eventually (\<lambda>x. DERIV f x :> f' x) at_top"
+  assumes Dg: "eventually (\<lambda>x. DERIV g x :> g' x) at_top"
+  assumes lim: "((\<lambda> x. (f' x / g' x)) ---> x) at_top"
+  shows "((\<lambda> x. f x / g x) ---> x) at_top"
+  unfolding filterlim_at_top_to_right
+proof (rule lhopital_right_0_at_top)
+  let ?F = "\<lambda>x. f (inverse x)"
+  let ?G = "\<lambda>x. g (inverse x)"
+  let ?R = "at_right (0::real)"
+  let ?D = "\<lambda>f' x. f' (inverse x) * - (inverse x ^ Suc (Suc 0))"
+
+  show "LIM x ?R. ?G x :> at_top"
+    using g_0 unfolding filterlim_at_top_to_right .
+
+  show "eventually (\<lambda>x. DERIV ?G x  :> ?D g' x) ?R"
+    unfolding eventually_at_right_to_top
+    using Dg eventually_ge_at_top[where c="1::real"]
+    apply eventually_elim
+    apply (rule DERIV_cong)
+    apply (rule DERIV_chain'[where f=inverse])
+    apply (auto intro!:  DERIV_inverse)
+    done
+
+  show "eventually (\<lambda>x. DERIV ?F x  :> ?D f' x) ?R"
+    unfolding eventually_at_right_to_top
+    using Df eventually_ge_at_top[where c="1::real"]
+    apply eventually_elim
+    apply (rule DERIV_cong)
+    apply (rule DERIV_chain'[where f=inverse])
+    apply (auto intro!:  DERIV_inverse)
+    done
+
+  show "eventually (\<lambda>x. ?D g' x \<noteq> 0) ?R"
+    unfolding eventually_at_right_to_top
+    using g' eventually_ge_at_top[where c="1::real"]
+    by eventually_elim auto
+    
+  show "((\<lambda>x. ?D f' x / ?D g' x) ---> x) ?R"
+    unfolding filterlim_at_right_to_top
+    apply (intro filterlim_cong[THEN iffD2, OF refl refl _ lim])
+    using eventually_ge_at_top[where c="1::real"]
+    by eventually_elim simp
+qed
+
 end
diff -r a75c6429c3c3 -r 77e3effa50b6 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Dec 04 18:00:31 2012 +0100
+++ b/src/HOL/Limits.thy	Tue Dec 04 18:00:37 2012 +0100
@@ -413,6 +413,12 @@
 lemma within_empty [simp]: "F within {} = bot"
   unfolding filter_eq_iff eventually_within by simp
 
+lemma within_within_eq: "(F within S) within T = F within (S \<inter> T)"
+  by (auto simp: filter_eq_iff eventually_within elim: eventually_elim1)
+
+lemma at_within_eq: "at x within T = nhds x within (T - {x})"
+  unfolding at_def within_within_eq by (simp add: ac_simps Diff_eq)
+
 lemma within_le: "F within S \<le> F"
   unfolding le_filter_def eventually_within by (auto elim: eventually_elim1)
 
@@ -1345,37 +1351,79 @@
   apply (auto simp: natceiling_le_eq)
   done
 
-lemma filterlim_inverse_at_top_pos:
-  "LIM x (nhds 0 within {0::real <..}). inverse x :> at_top"
-  unfolding filterlim_at_top_gt[where c=0] eventually_within
-proof safe
-  fix Z :: real assume [arith]: "0 < Z"
-  then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)"
-    by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
-  then show "eventually (\<lambda>x. x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
-    by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
-qed
+subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
+
+text {*
+
+This lemmas are useful for conversion between @{term "at x"} to @{term "at_left x"} and
+@{term "at_right x"} and also @{term "at_right 0"}.
+
+*}
+
+lemma at_eq_sup_left_right: "at (x::real) = sup (at_left x) (at_right x)"
+  by (auto simp: eventually_within at_def filter_eq_iff eventually_sup 
+           elim: eventually_elim2 eventually_elim1)
+
+lemma filterlim_split_at_real:
+  "filterlim f F (at_left x) \<Longrightarrow> filterlim f F (at_right x) \<Longrightarrow> filterlim f F (at (x::real))"
+  by (subst at_eq_sup_left_right) (rule filterlim_sup)
 
-lemma filterlim_inverse_at_top:
-  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
-  by (intro filterlim_compose[OF filterlim_inverse_at_top_pos])
-     (simp add: filterlim_def eventually_filtermap le_within_iff)
+lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::real)"
+  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
+  by (intro allI ex_cong) (auto simp: dist_real_def field_simps)
+
+lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::real)"
+  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
+  apply (intro allI ex_cong)
+  apply (auto simp: dist_real_def field_simps)
+  apply (erule_tac x="-x" in allE)
+  apply simp
+  done
+
+lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::real)"
+  unfolding at_def filtermap_nhds_shift[symmetric]
+  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
+
+lemma filtermap_at_right_shift: "filtermap (\<lambda>x. x - d) (at_right a) = at_right (a - d::real)"
+  unfolding filtermap_at_shift[symmetric]
+  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
 
-lemma filterlim_inverse_at_bot_neg:
-  "LIM x (nhds 0 within {..< 0::real}). inverse x :> at_bot"
-  unfolding filterlim_at_bot_lt[where c=0] eventually_within
-proof safe
-  fix Z :: real assume [arith]: "Z < 0"
-  have "eventually (\<lambda>x. inverse Z < x) (nhds 0)"
-    by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
-  then show "eventually (\<lambda>x. x \<in> {..< 0} \<longrightarrow> inverse x \<le> Z) (nhds 0)"
-    by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
-qed
+lemma at_right_to_0: "at_right (a::real) = filtermap (\<lambda>x. x + a) (at_right 0)"
+  using filtermap_at_right_shift[of "-a" 0] by simp
+
+lemma filterlim_at_right_to_0:
+  "filterlim f F (at_right (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at_right 0)"
+  unfolding filterlim_def filtermap_filtermap at_right_to_0[of a] ..
+
+lemma eventually_at_right_to_0:
+  "eventually P (at_right (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at_right 0)"
+  unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
+
+lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::real)"
+  unfolding at_def filtermap_nhds_minus[symmetric]
+  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
+
+lemma at_left_minus: "at_left (a::real) = filtermap (\<lambda>x. - x) (at_right (- a))"
+  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
 
-lemma filterlim_inverse_at_bot:
-  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. f x < 0) F \<Longrightarrow> LIM x F. inverse (f x) :> at_bot"
-  by (intro filterlim_compose[OF filterlim_inverse_at_bot_neg])
-     (simp add: filterlim_def eventually_filtermap le_within_iff)
+lemma at_right_minus: "at_right (a::real) = filtermap (\<lambda>x. - x) (at_left (- a))"
+  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
+
+lemma filterlim_at_left_to_right:
+  "filterlim f F (at_left (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
+  unfolding filterlim_def filtermap_filtermap at_left_minus[of a] ..
+
+lemma eventually_at_left_to_right:
+  "eventually P (at_left (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (- x)) (at_right (-a))"
+  unfolding at_left_minus[of a] by (simp add: eventually_filtermap)
+
+lemma filterlim_at_split:
+  "filterlim f F (at (x::real)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)"
+  by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)
+
+lemma eventually_at_split:
+  "eventually P (at (x::real)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
+  by (subst at_eq_sup_left_right) (simp add: eventually_sup)
 
 lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)"
   unfolding filter_eq_iff eventually_filtermap eventually_at_top_linorder eventually_at_bot_linorder
@@ -1406,6 +1454,30 @@
 lemma filterlim_uminus_at_bot: "(LIM x F. f x :> at_bot) \<longleftrightarrow> (LIM x F. - (f x) :: real :> at_top)"
   unfolding filterlim_uminus_at_top by simp
 
+lemma filterlim_inverse_at_top_right: "LIM x at_right (0::real). inverse x :> at_top"
+  unfolding filterlim_at_top_gt[where c=0] eventually_within at_def
+proof safe
+  fix Z :: real assume [arith]: "0 < Z"
+  then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)"
+    by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
+  then show "eventually (\<lambda>x. x \<in> - {0} \<longrightarrow> x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
+    by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
+qed
+
+lemma filterlim_inverse_at_top:
+  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
+  by (intro filterlim_compose[OF filterlim_inverse_at_top_right])
+     (simp add: filterlim_def eventually_filtermap le_within_iff at_def eventually_elim1)
+
+lemma filterlim_inverse_at_bot_neg:
+  "LIM x (at_left (0::real)). inverse x :> at_bot"
+  by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right)
+
+lemma filterlim_inverse_at_bot:
+  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. f x < 0) F \<Longrightarrow> LIM x F. inverse (f x) :> at_bot"
+  unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric]
+  by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric])
+
 lemma tendsto_inverse_0:
   fixes x :: "_ \<Rightarrow> 'a\<Colon>real_normed_div_algebra"
   shows "(inverse ---> (0::'a)) at_infinity"
@@ -1422,6 +1494,39 @@
   qed
 qed
 
+lemma at_right_to_top: "(at_right (0::real)) = filtermap inverse at_top"
+proof (rule antisym)
+  have "(inverse ---> (0::real)) at_top"
+    by (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl)
+  then show "filtermap inverse at_top \<le> at_right (0::real)"
+    unfolding at_within_eq
+    by (intro le_withinI) (simp_all add: eventually_filtermap eventually_gt_at_top filterlim_def)
+next
+  have "filtermap inverse (filtermap inverse (at_right (0::real))) \<le> filtermap inverse at_top"
+    using filterlim_inverse_at_top_right unfolding filterlim_def by (rule filtermap_mono)
+  then show "at_right (0::real) \<le> filtermap inverse at_top"
+    by (simp add: filtermap_ident filtermap_filtermap)
+qed
+
+lemma eventually_at_right_to_top:
+  "eventually P (at_right (0::real)) \<longleftrightarrow> eventually (\<lambda>x. P (inverse x)) at_top"
+  unfolding at_right_to_top eventually_filtermap ..
+
+lemma filterlim_at_right_to_top:
+  "filterlim f F (at_right (0::real)) \<longleftrightarrow> (LIM x at_top. f (inverse x) :> F)"
+  unfolding filterlim_def at_right_to_top filtermap_filtermap ..
+
+lemma at_top_to_right: "at_top = filtermap inverse (at_right (0::real))"
+  unfolding at_right_to_top filtermap_filtermap inverse_inverse_eq filtermap_ident ..
+
+lemma eventually_at_top_to_right:
+  "eventually P at_top \<longleftrightarrow> eventually (\<lambda>x. P (inverse x)) (at_right (0::real))"
+  unfolding at_top_to_right eventually_filtermap ..
+
+lemma filterlim_at_top_to_right:
+  "filterlim f F at_top \<longleftrightarrow> (LIM x (at_right (0::real)). f (inverse x) :> F)"
+  unfolding filterlim_def at_top_to_right filtermap_filtermap ..
+
 lemma filterlim_inverse_at_infinity:
   fixes x :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
   shows "filterlim inverse at_infinity (at (0::'a))"
@@ -1520,6 +1625,14 @@
     by eventually_elim simp
 qed
 
+lemma LIM_at_top_divide:
+  fixes f g :: "'a \<Rightarrow> real"
+  assumes f: "(f ---> a) F" "0 < a"
+  assumes g: "(g ---> 0) F" "eventually (\<lambda>x. 0 < g x) F"
+  shows "LIM x F. f x / g x :> at_top"
+  unfolding divide_inverse
+  by (rule filterlim_tendsto_pos_mult_at_top[OF f]) (rule filterlim_inverse_at_top[OF g])
+
 lemma filterlim_at_top_add_at_top: 
   assumes f: "LIM x F. f x :> at_top"
   assumes g: "LIM x F. g x :> at_top"
@@ -1573,79 +1686,5 @@
     by (auto simp: norm_power)
 qed simp
 
-subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
-
-text {*
-
-This lemmas are useful for conversion between @{term "at x"} to @{term "at_left x"} and
-@{term "at_right x"} and also @{term "at_right 0"}.
-
-*}
-
-lemma at_eq_sup_left_right: "at (x::real) = sup (at_left x) (at_right x)"
-  by (auto simp: eventually_within at_def filter_eq_iff eventually_sup 
-           elim: eventually_elim2 eventually_elim1)
-
-lemma filterlim_split_at_real:
-  "filterlim f F (at_left x) \<Longrightarrow> filterlim f F (at_right x) \<Longrightarrow> filterlim f F (at (x::real))"
-  by (subst at_eq_sup_left_right) (rule filterlim_sup)
-
-lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::real)"
-  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
-  by (intro allI ex_cong) (auto simp: dist_real_def field_simps)
-
-lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::real)"
-  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
-  apply (intro allI ex_cong)
-  apply (auto simp: dist_real_def field_simps)
-  apply (erule_tac x="-x" in allE)
-  apply simp
-  done
-
-lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::real)"
-  unfolding at_def filtermap_nhds_shift[symmetric]
-  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
-
-lemma filtermap_at_right_shift: "filtermap (\<lambda>x. x - d) (at_right a) = at_right (a - d::real)"
-  unfolding filtermap_at_shift[symmetric]
-  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
-
-lemma at_right_to_0: "at_right (a::real) = filtermap (\<lambda>x. x + a) (at_right 0)"
-  using filtermap_at_right_shift[of "-a" 0] by simp
-
-lemma filterlim_at_right_to_0:
-  "filterlim f F (at_right (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at_right 0)"
-  unfolding filterlim_def filtermap_filtermap at_right_to_0[of a] ..
-
-lemma eventually_at_right_to_0:
-  "eventually P (at_right (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at_right 0)"
-  unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
-
-lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::real)"
-  unfolding at_def filtermap_nhds_minus[symmetric]
-  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
-
-lemma at_left_minus: "at_left (a::real) = filtermap (\<lambda>x. - x) (at_right (- a))"
-  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
-
-lemma at_right_minus: "at_right (a::real) = filtermap (\<lambda>x. - x) (at_left (- a))"
-  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
-
-lemma filterlim_at_left_to_right:
-  "filterlim f F (at_left (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
-  unfolding filterlim_def filtermap_filtermap at_left_minus[of a] ..
-
-lemma eventually_at_left_to_right:
-  "eventually P (at_left (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (- x)) (at_right (-a))"
-  unfolding at_left_minus[of a] by (simp add: eventually_filtermap)
-
-lemma filterlim_at_split:
-  "filterlim f F (at (x::real)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)"
-  by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)
-
-lemma eventually_at_split:
-  "eventually P (at (x::real)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
-  by (subst at_eq_sup_left_right) (simp add: eventually_sup)
-
 end
 
diff -r a75c6429c3c3 -r 77e3effa50b6 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Dec 04 18:00:31 2012 +0100
+++ b/src/HOL/Transcendental.thy	Tue Dec 04 18:00:37 2012 +0100
@@ -1339,6 +1339,28 @@
   by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
      (auto intro: eventually_gt_at_top)
 
+lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) ---> (0::real)) at_top"
+proof (induct k)
+  show "((\<lambda>x. x ^ 0 / exp x) ---> (0::real)) at_top"
+    by (simp add: inverse_eq_divide[symmetric])
+       (metis filterlim_compose[OF tendsto_inverse_0] exp_at_top filterlim_mono
+              at_top_le_at_infinity order_refl)
+next
+  case (Suc k)
+  show ?case
+  proof (rule lhospital_at_top_at_top)
+    show "eventually (\<lambda>x. DERIV (\<lambda>x. x ^ Suc k) x :> (real (Suc k) * x^k)) at_top"
+      by eventually_elim (intro DERIV_intros, simp, simp)
+    show "eventually (\<lambda>x. DERIV exp x :> exp x) at_top"
+      by eventually_elim (auto intro!: DERIV_intros)
+    show "eventually (\<lambda>x. exp x \<noteq> 0) at_top"
+      by auto
+    from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"]
+    show "((\<lambda>x. real (Suc k) * x ^ k / exp x) ---> 0) at_top"
+      by simp
+  qed (rule exp_at_top)
+qed
+
 subsection {* Sine and Cosine *}
 
 definition sin_coeff :: "nat \<Rightarrow> real" where