# HG changeset patch
# User hoelzl
# Date 1431005668 -7200
# Node ID e1ea5a6379c927760ab79ba8e56ddf3163cb4ec5
# Parent  fc66055fbadf47dcdf0364f90ceb317b2c90e3f0
generalized tends over powr; added DERIV rule for powr

diff -r fc66055fbadf -r e1ea5a6379c9 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Wed May 06 15:04:38 2015 +0200
+++ b/src/HOL/Filter.thy	Thu May 07 15:34:28 2015 +0200
@@ -822,6 +822,11 @@
 lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
   by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
 
+lemma filterlim_If:
+  "LIM x inf F (principal {x. P x}). f x :> G \<Longrightarrow>
+    LIM x inf F (principal {x. \<not> P x}). g x :> G \<Longrightarrow>
+    LIM x F. if P x then f x else g x :> G"
+  unfolding filterlim_iff eventually_inf_principal by (auto simp: eventually_conj_iff)
 
 subsection {* Limits to @{const at_top} and @{const at_bot} *}
 
diff -r fc66055fbadf -r e1ea5a6379c9 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Wed May 06 15:04:38 2015 +0200
+++ b/src/HOL/Limits.thy	Thu May 07 15:34:28 2015 +0200
@@ -1183,6 +1183,12 @@
   using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "\<lambda>x. - g x"] assms(3)
   unfolding filterlim_uminus_at_bot by simp
 
+lemma filterlim_tendsto_neg_mult_at_bot:
+  assumes c: "(f ---> c) F" "(c::real) < 0" and g: "filterlim g at_top F"
+  shows "LIM x F. f x * g x :> at_bot"
+  using c filterlim_tendsto_pos_mult_at_top[of "\<lambda>x. - f x" "- c" F, OF _ _ g]
+  unfolding filterlim_uminus_at_bot tendsto_minus_cancel_left by simp
+
 lemma filterlim_pow_at_top:
   fixes f :: "real \<Rightarrow> real"
   assumes "0 < n" and f: "LIM x F. f x :> at_top"
diff -r fc66055fbadf -r e1ea5a6379c9 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed May 06 15:04:38 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy	Thu May 07 15:34:28 2015 +0200
@@ -356,6 +356,10 @@
 lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
   unfolding trivial_limit_def eventually_nhds by simp
 
+lemma (in t1_space) t1_space_nhds:
+  "x \<noteq> y \<Longrightarrow> (\<forall>\<^sub>F x in nhds x. x \<noteq> y)"
+  by (drule t1_space) (auto simp: eventually_nhds)
+
 lemma at_within_eq: "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
   unfolding nhds_def at_within_def by (subst INF_inf_const2[symmetric]) (auto simp add: Diff_Int_distrib)
 
diff -r fc66055fbadf -r e1ea5a6379c9 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Wed May 06 15:04:38 2015 +0200
+++ b/src/HOL/Transcendental.thy	Thu May 07 15:34:28 2015 +0200
@@ -2458,31 +2458,15 @@
   finally show ?thesis .
 qed
 
-lemma tendsto_powr [tendsto_intros]: 
+lemma tendsto_powr [tendsto_intros]:
   fixes a::real 
   assumes f: "(f ---> a) F" and g: "(g ---> b) F" and a: "a \<noteq> 0"
   shows "((\<lambda>x. f x powr g x) ---> a powr b) F"
-proof -
-  { fix S :: "real set"
-    obtain T where "open T" "a \<in> T" "0 \<notin> T"
-      using t1_space a by blast
-    then have "eventually (\<lambda>x. f x = 0 \<longrightarrow> 0 \<in> S) F"
-      using f
-      by (simp add: tendsto_def) (metis (mono_tags, lifting) eventually_mono)
-  }
-  moreover
-  { fix S :: "real set"
-    assume S: "open S" "exp (b * ln a) \<in> S"
-    then have "((\<lambda>x. exp (g x * ln (f x))) ---> exp (b * ln a)) F"
-    using f g a
-      by (intro tendsto_intros) auto
-    then have "eventually (\<lambda>x. f x \<noteq> 0 \<longrightarrow> exp (g x * ln (f x)) \<in> S) F"
-      using f S
-      by (simp add: tendsto_def) (metis (mono_tags, lifting) eventually_mono)
-  }
-  ultimately show ?thesis using assms
-    by (simp add: powr_def tendsto_def eventually_conj_iff)
-qed
+  unfolding powr_def
+proof (rule filterlim_If)
+  from f show "((\<lambda>x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))"
+    by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_elim1 dest: t1_space_nhds)
+qed (insert f g a, auto intro!: tendsto_intros intro: tendsto_mono inf_le1)
 
 lemma continuous_powr:
   assumes "continuous F f"
@@ -2508,45 +2492,68 @@
   shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
   using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
 
-(* FIXME: generalize by replacing d by with g x and g ---> d? *)
+lemma tendsto_powr2:
+  fixes a::real
+  assumes f: "(f ---> a) F" and g: "(g ---> b) F" and f_nonneg: "\<forall>\<^sub>F x in F. 0 \<le> f x" and b: "0 < b"
+  shows "((\<lambda>x. f x powr g x) ---> a powr b) F"
+  unfolding powr_def
+proof (rule filterlim_If)
+  from f show "((\<lambda>x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))"
+    by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_elim1 dest: t1_space_nhds)
+next
+  { assume "a = 0"
+    with f f_nonneg have "LIM x inf F (principal {x. f x \<noteq> 0}). f x :> at_right 0"
+      by (auto simp add: filterlim_at eventually_inf_principal le_less 
+               elim: eventually_elim1 intro: tendsto_mono inf_le1)
+    then have "((\<lambda>x. exp (g x * ln (f x))) ---> 0) (inf F (principal {x. f x \<noteq> 0}))"
+      by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_0]
+                       filterlim_tendsto_pos_mult_at_bot[OF _ `0 < b`]
+               intro: tendsto_mono inf_le1 g) }
+  then show "((\<lambda>x. exp (g x * ln (f x))) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x \<noteq> 0}))"
+    using f g by (auto intro!: tendsto_intros intro: tendsto_mono inf_le1)
+qed
+
+lemma DERIV_powr:
+  fixes r::real
+  assumes g: "DERIV g x :> m" and pos: "g x > 0" and f: "DERIV f x :> r"
+  shows  "DERIV (\<lambda>x. g x powr f x) x :> (g x powr f x) * (r * ln (g x) + m * f x / g x)"
+proof -
+  have "DERIV (\<lambda>x. exp (f x * ln (g x))) x :> (g x powr f x) * (r * ln (g x) + m * f x / g x)"
+    using pos
+    by (auto intro!: derivative_eq_intros g pos f simp: powr_def field_simps exp_diff)
+  then show ?thesis
+  proof (rule DERIV_cong_ev[OF refl _ refl, THEN iffD1, rotated])
+    from DERIV_isCont[OF g] pos have "\<forall>\<^sub>F x in at x. 0 < g x"
+      unfolding isCont_def by (rule order_tendstoD(1))
+    with pos show "\<forall>\<^sub>F x in nhds x. exp (f x * ln (g x)) = g x powr f x"
+      by (auto simp: eventually_at_filter powr_def elim: eventually_elim1)
+  qed
+qed
+
+lemma DERIV_fun_powr:
+  fixes r::real
+  assumes g: "DERIV g x :> m" and pos: "g x > 0"
+  shows  "DERIV (\<lambda>x. (g x) powr r) x :> r * (g x) powr (r - of_nat 1) * m"
+  using DERIV_powr[OF g pos DERIV_const, of r] pos
+  by (simp add: powr_divide2[symmetric] field_simps)
+
 lemma tendsto_zero_powrI:
-  assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> (0::real)) F"
-    and "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
+  assumes "(f ---> (0::real)) F" "(g ---> b) F" "\<forall>\<^sub>F x in F. 0 \<le> f x" "0 < b"
+  shows "((\<lambda>x. f x powr g x) ---> 0) F"
+  using tendsto_powr2[OF assms] by simp
 
 lemma tendsto_neg_powr:
   assumes "s < 0"
-    and "LIM x F. f x :> at_top"
+    and f: "LIM x F. f x :> at_top"
   shows "((\<lambda>x. f x powr s) ---> (0::real)) F"
-proof (rule tendstoI)
-  fix e :: real assume "0 < e"
-  def Z \<equiv> "e powr (1 / s)"
-  have "Z > 0"
-    using Z_def `0 < e` by auto
-  from assms have "eventually (\<lambda>x. Z < f x) F"
-    by (simp add: filterlim_at_top_dense)
-  moreover
-  from assms have "\<And>x::real. Z < x \<Longrightarrow> x powr s < Z powr s"
-    using `Z > 0`
-    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)
+proof -
+  have "((\<lambda>x. exp (s * ln (f x))) ---> (0::real)) F" (is "?X")
+    by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_top]
+                     filterlim_tendsto_neg_mult_at_bot assms)
+  also have "?X \<longleftrightarrow> ((\<lambda>x. f x powr s) ---> (0::real)) F"
+    using f filterlim_at_top_dense[of f F]
+    by (intro filterlim_cong[OF refl refl]) (auto simp: neq_iff powr_def elim: eventually_elim1)
+  finally show ?thesis .
 qed
 
 lemma tendsto_exp_limit_at_right: