generalized tends over powr; added DERIV rule for powr
authorhoelzl
Thu May 07 15:34:28 2015 +0200 (2015-05-07)
changeset 60182e1ea5a6379c9
parent 60181 fc66055fbadf
child 60183 4cd4c204578c
generalized tends over powr; added DERIV rule for powr
src/HOL/Filter.thy
src/HOL/Limits.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Filter.thy	Wed May 06 15:04:38 2015 +0200
     1.2 +++ b/src/HOL/Filter.thy	Thu May 07 15:34:28 2015 +0200
     1.3 @@ -822,6 +822,11 @@
     1.4  lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
     1.5    by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
     1.6  
     1.7 +lemma filterlim_If:
     1.8 +  "LIM x inf F (principal {x. P x}). f x :> G \<Longrightarrow>
     1.9 +    LIM x inf F (principal {x. \<not> P x}). g x :> G \<Longrightarrow>
    1.10 +    LIM x F. if P x then f x else g x :> G"
    1.11 +  unfolding filterlim_iff eventually_inf_principal by (auto simp: eventually_conj_iff)
    1.12  
    1.13  subsection {* Limits to @{const at_top} and @{const at_bot} *}
    1.14  
     2.1 --- a/src/HOL/Limits.thy	Wed May 06 15:04:38 2015 +0200
     2.2 +++ b/src/HOL/Limits.thy	Thu May 07 15:34:28 2015 +0200
     2.3 @@ -1183,6 +1183,12 @@
     2.4    using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "\<lambda>x. - g x"] assms(3)
     2.5    unfolding filterlim_uminus_at_bot by simp
     2.6  
     2.7 +lemma filterlim_tendsto_neg_mult_at_bot:
     2.8 +  assumes c: "(f ---> c) F" "(c::real) < 0" and g: "filterlim g at_top F"
     2.9 +  shows "LIM x F. f x * g x :> at_bot"
    2.10 +  using c filterlim_tendsto_pos_mult_at_top[of "\<lambda>x. - f x" "- c" F, OF _ _ g]
    2.11 +  unfolding filterlim_uminus_at_bot tendsto_minus_cancel_left by simp
    2.12 +
    2.13  lemma filterlim_pow_at_top:
    2.14    fixes f :: "real \<Rightarrow> real"
    2.15    assumes "0 < n" and f: "LIM x F. f x :> at_top"
     3.1 --- a/src/HOL/Topological_Spaces.thy	Wed May 06 15:04:38 2015 +0200
     3.2 +++ b/src/HOL/Topological_Spaces.thy	Thu May 07 15:34:28 2015 +0200
     3.3 @@ -356,6 +356,10 @@
     3.4  lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
     3.5    unfolding trivial_limit_def eventually_nhds by simp
     3.6  
     3.7 +lemma (in t1_space) t1_space_nhds:
     3.8 +  "x \<noteq> y \<Longrightarrow> (\<forall>\<^sub>F x in nhds x. x \<noteq> y)"
     3.9 +  by (drule t1_space) (auto simp: eventually_nhds)
    3.10 +
    3.11  lemma at_within_eq: "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
    3.12    unfolding nhds_def at_within_def by (subst INF_inf_const2[symmetric]) (auto simp add: Diff_Int_distrib)
    3.13  
     4.1 --- a/src/HOL/Transcendental.thy	Wed May 06 15:04:38 2015 +0200
     4.2 +++ b/src/HOL/Transcendental.thy	Thu May 07 15:34:28 2015 +0200
     4.3 @@ -2458,31 +2458,15 @@
     4.4    finally show ?thesis .
     4.5  qed
     4.6  
     4.7 -lemma tendsto_powr [tendsto_intros]: 
     4.8 +lemma tendsto_powr [tendsto_intros]:
     4.9    fixes a::real 
    4.10    assumes f: "(f ---> a) F" and g: "(g ---> b) F" and a: "a \<noteq> 0"
    4.11    shows "((\<lambda>x. f x powr g x) ---> a powr b) F"
    4.12 -proof -
    4.13 -  { fix S :: "real set"
    4.14 -    obtain T where "open T" "a \<in> T" "0 \<notin> T"
    4.15 -      using t1_space a by blast
    4.16 -    then have "eventually (\<lambda>x. f x = 0 \<longrightarrow> 0 \<in> S) F"
    4.17 -      using f
    4.18 -      by (simp add: tendsto_def) (metis (mono_tags, lifting) eventually_mono)
    4.19 -  }
    4.20 -  moreover
    4.21 -  { fix S :: "real set"
    4.22 -    assume S: "open S" "exp (b * ln a) \<in> S"
    4.23 -    then have "((\<lambda>x. exp (g x * ln (f x))) ---> exp (b * ln a)) F"
    4.24 -    using f g a
    4.25 -      by (intro tendsto_intros) auto
    4.26 -    then have "eventually (\<lambda>x. f x \<noteq> 0 \<longrightarrow> exp (g x * ln (f x)) \<in> S) F"
    4.27 -      using f S
    4.28 -      by (simp add: tendsto_def) (metis (mono_tags, lifting) eventually_mono)
    4.29 -  }
    4.30 -  ultimately show ?thesis using assms
    4.31 -    by (simp add: powr_def tendsto_def eventually_conj_iff)
    4.32 -qed
    4.33 +  unfolding powr_def
    4.34 +proof (rule filterlim_If)
    4.35 +  from f show "((\<lambda>x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))"
    4.36 +    by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_elim1 dest: t1_space_nhds)
    4.37 +qed (insert f g a, auto intro!: tendsto_intros intro: tendsto_mono inf_le1)
    4.38  
    4.39  lemma continuous_powr:
    4.40    assumes "continuous F f"
    4.41 @@ -2508,45 +2492,68 @@
    4.42    shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
    4.43    using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
    4.44  
    4.45 -(* FIXME: generalize by replacing d by with g x and g ---> d? *)
    4.46 +lemma tendsto_powr2:
    4.47 +  fixes a::real
    4.48 +  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"
    4.49 +  shows "((\<lambda>x. f x powr g x) ---> a powr b) F"
    4.50 +  unfolding powr_def
    4.51 +proof (rule filterlim_If)
    4.52 +  from f show "((\<lambda>x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))"
    4.53 +    by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_elim1 dest: t1_space_nhds)
    4.54 +next
    4.55 +  { assume "a = 0"
    4.56 +    with f f_nonneg have "LIM x inf F (principal {x. f x \<noteq> 0}). f x :> at_right 0"
    4.57 +      by (auto simp add: filterlim_at eventually_inf_principal le_less 
    4.58 +               elim: eventually_elim1 intro: tendsto_mono inf_le1)
    4.59 +    then have "((\<lambda>x. exp (g x * ln (f x))) ---> 0) (inf F (principal {x. f x \<noteq> 0}))"
    4.60 +      by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_0]
    4.61 +                       filterlim_tendsto_pos_mult_at_bot[OF _ `0 < b`]
    4.62 +               intro: tendsto_mono inf_le1 g) }
    4.63 +  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}))"
    4.64 +    using f g by (auto intro!: tendsto_intros intro: tendsto_mono inf_le1)
    4.65 +qed
    4.66 +
    4.67 +lemma DERIV_powr:
    4.68 +  fixes r::real
    4.69 +  assumes g: "DERIV g x :> m" and pos: "g x > 0" and f: "DERIV f x :> r"
    4.70 +  shows  "DERIV (\<lambda>x. g x powr f x) x :> (g x powr f x) * (r * ln (g x) + m * f x / g x)"
    4.71 +proof -
    4.72 +  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)"
    4.73 +    using pos
    4.74 +    by (auto intro!: derivative_eq_intros g pos f simp: powr_def field_simps exp_diff)
    4.75 +  then show ?thesis
    4.76 +  proof (rule DERIV_cong_ev[OF refl _ refl, THEN iffD1, rotated])
    4.77 +    from DERIV_isCont[OF g] pos have "\<forall>\<^sub>F x in at x. 0 < g x"
    4.78 +      unfolding isCont_def by (rule order_tendstoD(1))
    4.79 +    with pos show "\<forall>\<^sub>F x in nhds x. exp (f x * ln (g x)) = g x powr f x"
    4.80 +      by (auto simp: eventually_at_filter powr_def elim: eventually_elim1)
    4.81 +  qed
    4.82 +qed
    4.83 +
    4.84 +lemma DERIV_fun_powr:
    4.85 +  fixes r::real
    4.86 +  assumes g: "DERIV g x :> m" and pos: "g x > 0"
    4.87 +  shows  "DERIV (\<lambda>x. (g x) powr r) x :> r * (g x) powr (r - of_nat 1) * m"
    4.88 +  using DERIV_powr[OF g pos DERIV_const, of r] pos
    4.89 +  by (simp add: powr_divide2[symmetric] field_simps)
    4.90 +
    4.91  lemma tendsto_zero_powrI:
    4.92 -  assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> (0::real)) F"
    4.93 -    and "0 < d"
    4.94 -  shows "((\<lambda>x. f x powr d) ---> 0) F"
    4.95 -proof (rule tendstoI)
    4.96 -  fix e :: real assume "0 < e"
    4.97 -  def Z \<equiv> "e powr (1 / d)"
    4.98 -  with `0 < e` have "0 < Z" by simp
    4.99 -  with assms have "eventually (\<lambda>x. 0 < f x \<and> dist (f x) 0 < Z) F"
   4.100 -    by (intro eventually_conj tendstoD)
   4.101 -  moreover
   4.102 -  from assms have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> x powr d < Z powr d"
   4.103 -    by (intro powr_less_mono2) (auto simp: dist_real_def)
   4.104 -  with assms `0 < e` have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> dist (x powr d) 0 < e"
   4.105 -    unfolding dist_real_def Z_def by (auto simp: powr_powr)
   4.106 -  ultimately
   4.107 -  show "eventually (\<lambda>x. dist (f x powr d) 0 < e) F" by (rule eventually_elim1)
   4.108 -qed
   4.109 +  assumes "(f ---> (0::real)) F" "(g ---> b) F" "\<forall>\<^sub>F x in F. 0 \<le> f x" "0 < b"
   4.110 +  shows "((\<lambda>x. f x powr g x) ---> 0) F"
   4.111 +  using tendsto_powr2[OF assms] by simp
   4.112  
   4.113  lemma tendsto_neg_powr:
   4.114    assumes "s < 0"
   4.115 -    and "LIM x F. f x :> at_top"
   4.116 +    and f: "LIM x F. f x :> at_top"
   4.117    shows "((\<lambda>x. f x powr s) ---> (0::real)) F"
   4.118 -proof (rule tendstoI)
   4.119 -  fix e :: real assume "0 < e"
   4.120 -  def Z \<equiv> "e powr (1 / s)"
   4.121 -  have "Z > 0"
   4.122 -    using Z_def `0 < e` by auto
   4.123 -  from assms have "eventually (\<lambda>x. Z < f x) F"
   4.124 -    by (simp add: filterlim_at_top_dense)
   4.125 -  moreover
   4.126 -  from assms have "\<And>x::real. Z < x \<Longrightarrow> x powr s < Z powr s"
   4.127 -    using `Z > 0`
   4.128 -    by (auto simp: Z_def intro!: powr_less_mono2_neg)
   4.129 -  with assms `0 < e` have "\<And>x. Z < x \<Longrightarrow> dist (x powr s) 0 < e"
   4.130 -    by (simp add: powr_powr Z_def dist_real_def)
   4.131 -  ultimately
   4.132 -  show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1)
   4.133 +proof -
   4.134 +  have "((\<lambda>x. exp (s * ln (f x))) ---> (0::real)) F" (is "?X")
   4.135 +    by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_top]
   4.136 +                     filterlim_tendsto_neg_mult_at_bot assms)
   4.137 +  also have "?X \<longleftrightarrow> ((\<lambda>x. f x powr s) ---> (0::real)) F"
   4.138 +    using f filterlim_at_top_dense[of f F]
   4.139 +    by (intro filterlim_cong[OF refl refl]) (auto simp: neq_iff powr_def elim: eventually_elim1)
   4.140 +  finally show ?thesis .
   4.141  qed
   4.142  
   4.143  lemma tendsto_exp_limit_at_right: