# HG changeset patch
# User noschinl
# Date 1323960939 -3600
# Node ID 8dcf6692433f33f295b3649f823bc5f81cd2596a
# Parent  66b419de5f38308a2b7e12dc255108cd8afcf42e
add lemmas about limits

diff -r 66b419de5f38 -r 8dcf6692433f src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Thu Dec 15 13:40:20 2011 +0100
+++ b/src/HOL/Limits.thy	Thu Dec 15 15:55:39 2011 +0100
@@ -101,6 +101,18 @@
   shows "eventually (\<lambda>i. R i) F"
   using assms by (auto elim!: eventually_rev_mp)
 
+lemma eventually_subst:
+  assumes "eventually (\<lambda>n. P n = Q n) F"
+  shows "eventually P F = eventually Q F" (is "?L = ?R")
+proof -
+  from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
+      and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F"
+    by (auto elim: eventually_elim1)
+  then show ?thesis by (auto elim: eventually_elim2)
+qed
+
+
+
 subsection {* Finer-than relation *}
 
 text {* @{term "F \<le> F'"} means that filter @{term F} is finer than
@@ -280,6 +292,11 @@
   unfolding le_filter_def eventually_sequentially
   by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)
 
+lemma eventually_sequentiallyI:
+  assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
+  shows "eventually P sequentially"
+using assms by (auto simp: eventually_sequentially)
+
 
 subsection {* Standard filters *}
 
@@ -537,6 +554,9 @@
   tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
   "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
 
+definition real_tendsto_inf :: "('a \<Rightarrow> real) \<Rightarrow> 'a filter \<Rightarrow> bool" where
+  "real_tendsto_inf f F \<equiv> \<forall>x. eventually (\<lambda>y. x < f y) F"
+
 ML {*
 structure Tendsto_Intros = Named_Thms
 (
@@ -673,6 +693,15 @@
     using le_less_trans by (rule eventually_elim2)
 qed
 
+lemma real_tendsto_inf_real: "real_tendsto_inf real sequentially"
+proof (unfold real_tendsto_inf_def, rule allI)
+  fix x show "eventually (\<lambda>y. x < real y) sequentially"
+    by (rule eventually_sequentiallyI[of "natceiling (x + 1)"])
+        (simp add: natceiling_le_eq)
+qed
+
+
+
 subsubsection {* Distance and norms *}
 
 lemma tendsto_dist [tendsto_intros]:
@@ -769,6 +798,22 @@
     by (simp add: tendsto_const)
 qed
 
+lemma real_tendsto_sandwich:
+  fixes f g h :: "'a \<Rightarrow> real"
+  assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
+  assumes lim: "(f ---> c) net" "(h ---> c) net"
+  shows "(g ---> c) net"
+proof -
+  have "((\<lambda>n. g n - f n) ---> 0) net"
+  proof (rule metric_tendsto_imp_tendsto)
+    show "eventually (\<lambda>n. dist (g n - f n) 0 \<le> dist (h n - f n) 0) net"
+      using ev by (rule eventually_elim2) (simp add: dist_real_def)
+    show "((\<lambda>n. h n - f n) ---> 0) net"
+      using tendsto_diff[OF lim(2,1)] by simp
+  qed
+  from tendsto_add[OF this lim(1)] show ?thesis by simp
+qed
+
 subsubsection {* Linear operators and multiplication *}
 
 lemma (in bounded_linear) tendsto:
diff -r 66b419de5f38 -r 8dcf6692433f src/HOL/Log.thy
--- a/src/HOL/Log.thy	Thu Dec 15 13:40:20 2011 +0100
+++ b/src/HOL/Log.thy	Thu Dec 15 15:55:39 2011 +0100
@@ -285,32 +285,40 @@
   finally show ?thesis .
 qed
 
-lemma LIMSEQ_neg_powr:
-  assumes s: "0 < s"
-  shows "(%x. (real x) powr - s) ----> 0"
-  apply (unfold LIMSEQ_iff)
-  apply clarsimp
-  apply (rule_tac x = "natfloor(r powr (1 / - s)) + 1" in exI)
-  apply clarify
-proof -
-  fix r fix n
-  assume r: "0 < r" and n: "natfloor (r powr (1 / - s)) + 1 <= n"
-  have "r powr (1 / - s) < real(natfloor(r powr (1 / - s))) + 1"
-    by (rule real_natfloor_add_one_gt)
-  also have "... = real(natfloor(r powr (1 / -s)) + 1)"
-    by simp
-  also have "... <= real n"
-    apply (subst real_of_nat_le_iff)
-    apply (rule n)
-    done
-  finally have "r powr (1 / - s) < real n".
-  then have "real n powr (- s) < (r powr (1 / - s)) powr - s" 
-    apply (intro powr_less_mono2_neg)
-    apply (auto simp add: s)
-    done
-  also have "... = r"
-    by (simp add: powr_powr s r less_imp_neq [THEN not_sym])
-  finally show "real n powr - s < r" .
+(* FIXME: generalize by replacing d by with g x and g ---> d? *)
+lemma tendsto_zero_powrI:
+  assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F"
+  assumes "0 < d"
+  shows "((\<lambda>x. f x powr d) ---> 0) F"
+proof (rule tendstoI)
+  fix e :: real assume "0 < e"
+  def Z \<equiv> "e powr (1 / d)"
+  with `0 < e` have "0 < Z" by simp
+  with assms have "eventually (\<lambda>x. 0 < f x \<and> dist (f x) 0 < Z) F"
+    by (intro eventually_conj tendstoD)
+  moreover
+  from assms have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> x powr d < Z powr d"
+    by (intro powr_less_mono2) (auto simp: dist_real_def)
+  with assms `0 < e` have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> dist (x powr d) 0 < e"
+    unfolding dist_real_def Z_def by (auto simp: powr_powr)
+  ultimately
+  show "eventually (\<lambda>x. dist (f x powr d) 0 < e) F" by (rule eventually_elim1)
+qed
+
+lemma tendsto_neg_powr:
+  assumes "s < 0" and "real_tendsto_inf f F"
+  shows "((\<lambda>x. f x powr s) ---> 0) F"
+proof (rule tendstoI)
+  fix e :: real assume "0 < e"
+  def Z \<equiv> "e powr (1 / s)"
+  from assms have "eventually (\<lambda>x. Z < f x) F" by (simp add: real_tendsto_inf_def)
+  moreover
+  from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s"
+    by (auto simp: Z_def intro!: powr_less_mono2_neg)
+  with assms `0 < e` have "\<And>x. Z < x \<Longrightarrow> dist (x powr s) 0 < e"
+    by (simp add: powr_powr Z_def dist_real_def)
+  ultimately
+  show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1)
 qed
 
 end