src/HOL/Log.thy
changeset 45892 8dcf6692433f
parent 41550 efa734d9b221
child 45915 0e5a87b772f9
     1.1 --- a/src/HOL/Log.thy	Thu Dec 15 13:40:20 2011 +0100
     1.2 +++ b/src/HOL/Log.thy	Thu Dec 15 15:55:39 2011 +0100
     1.3 @@ -285,32 +285,40 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 -lemma LIMSEQ_neg_powr:
     1.8 -  assumes s: "0 < s"
     1.9 -  shows "(%x. (real x) powr - s) ----> 0"
    1.10 -  apply (unfold LIMSEQ_iff)
    1.11 -  apply clarsimp
    1.12 -  apply (rule_tac x = "natfloor(r powr (1 / - s)) + 1" in exI)
    1.13 -  apply clarify
    1.14 -proof -
    1.15 -  fix r fix n
    1.16 -  assume r: "0 < r" and n: "natfloor (r powr (1 / - s)) + 1 <= n"
    1.17 -  have "r powr (1 / - s) < real(natfloor(r powr (1 / - s))) + 1"
    1.18 -    by (rule real_natfloor_add_one_gt)
    1.19 -  also have "... = real(natfloor(r powr (1 / -s)) + 1)"
    1.20 -    by simp
    1.21 -  also have "... <= real n"
    1.22 -    apply (subst real_of_nat_le_iff)
    1.23 -    apply (rule n)
    1.24 -    done
    1.25 -  finally have "r powr (1 / - s) < real n".
    1.26 -  then have "real n powr (- s) < (r powr (1 / - s)) powr - s" 
    1.27 -    apply (intro powr_less_mono2_neg)
    1.28 -    apply (auto simp add: s)
    1.29 -    done
    1.30 -  also have "... = r"
    1.31 -    by (simp add: powr_powr s r less_imp_neq [THEN not_sym])
    1.32 -  finally show "real n powr - s < r" .
    1.33 +(* FIXME: generalize by replacing d by with g x and g ---> d? *)
    1.34 +lemma tendsto_zero_powrI:
    1.35 +  assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F"
    1.36 +  assumes "0 < d"
    1.37 +  shows "((\<lambda>x. f x powr d) ---> 0) F"
    1.38 +proof (rule tendstoI)
    1.39 +  fix e :: real assume "0 < e"
    1.40 +  def Z \<equiv> "e powr (1 / d)"
    1.41 +  with `0 < e` have "0 < Z" by simp
    1.42 +  with assms have "eventually (\<lambda>x. 0 < f x \<and> dist (f x) 0 < Z) F"
    1.43 +    by (intro eventually_conj tendstoD)
    1.44 +  moreover
    1.45 +  from assms have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> x powr d < Z powr d"
    1.46 +    by (intro powr_less_mono2) (auto simp: dist_real_def)
    1.47 +  with assms `0 < e` have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> dist (x powr d) 0 < e"
    1.48 +    unfolding dist_real_def Z_def by (auto simp: powr_powr)
    1.49 +  ultimately
    1.50 +  show "eventually (\<lambda>x. dist (f x powr d) 0 < e) F" by (rule eventually_elim1)
    1.51 +qed
    1.52 +
    1.53 +lemma tendsto_neg_powr:
    1.54 +  assumes "s < 0" and "real_tendsto_inf f F"
    1.55 +  shows "((\<lambda>x. f x powr s) ---> 0) F"
    1.56 +proof (rule tendstoI)
    1.57 +  fix e :: real assume "0 < e"
    1.58 +  def Z \<equiv> "e powr (1 / s)"
    1.59 +  from assms have "eventually (\<lambda>x. Z < f x) F" by (simp add: real_tendsto_inf_def)
    1.60 +  moreover
    1.61 +  from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s"
    1.62 +    by (auto simp: Z_def intro!: powr_less_mono2_neg)
    1.63 +  with assms `0 < e` have "\<And>x. Z < x \<Longrightarrow> dist (x powr s) 0 < e"
    1.64 +    by (simp add: powr_powr Z_def dist_real_def)
    1.65 +  ultimately
    1.66 +  show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1)
    1.67  qed
    1.68  
    1.69  end