src/HOL/Transcendental.thy
changeset 57275 0ddb5b755cdc
parent 57180 74c81a5b5a34
child 57418 6ab1c7cb0b8d
     1.1 --- a/src/HOL/Transcendental.thy	Wed Jun 18 15:23:40 2014 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Wed Jun 18 07:31:12 2014 +0200
     1.3 @@ -1303,29 +1303,42 @@
     1.4  lemma ln_less_zero: "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0"
     1.5    by simp
     1.6  
     1.7 -lemma isCont_ln: "0 < x \<Longrightarrow> isCont ln x"
     1.8 -  apply (subgoal_tac "isCont ln (exp (ln x))", simp)
     1.9 -  apply (rule isCont_inverse_function [where f=exp], simp_all)
    1.10 -  done
    1.11 +lemma ln_neg_is_const: "x \<le> 0 \<Longrightarrow> ln x = (THE x. False)"
    1.12 +  by (auto simp add: ln_def intro!: arg_cong[where f=The])
    1.13 +
    1.14 +lemma isCont_ln: assumes "x \<noteq> 0" shows "isCont ln x"
    1.15 +proof cases
    1.16 +  assume "0 < x"
    1.17 +  moreover then have "isCont ln (exp (ln x))"
    1.18 +    by (intro isCont_inv_fun[where d="\<bar>x\<bar>" and f=exp]) auto
    1.19 +  ultimately show ?thesis
    1.20 +    by simp
    1.21 +next
    1.22 +  assume "\<not> 0 < x" with `x \<noteq> 0` show "isCont ln x"
    1.23 +    unfolding isCont_def
    1.24 +    by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\<lambda>_. ln 0"])
    1.25 +       (auto simp: ln_neg_is_const not_less eventually_at dist_real_def
    1.26 +                intro!: tendsto_const exI[of _ "\<bar>x\<bar>"])
    1.27 +qed
    1.28  
    1.29  lemma tendsto_ln [tendsto_intros]:
    1.30 -  "(f ---> a) F \<Longrightarrow> 0 < a \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
    1.31 +  "(f ---> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
    1.32    by (rule isCont_tendsto_compose [OF isCont_ln])
    1.33  
    1.34  lemma continuous_ln:
    1.35 -  "continuous F f \<Longrightarrow> 0 < f (Lim F (\<lambda>x. x)) \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
    1.36 +  "continuous F f \<Longrightarrow> f (Lim F (\<lambda>x. x)) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
    1.37    unfolding continuous_def by (rule tendsto_ln)
    1.38  
    1.39  lemma isCont_ln' [continuous_intros]:
    1.40 -  "continuous (at x) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
    1.41 +  "continuous (at x) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
    1.42    unfolding continuous_at by (rule tendsto_ln)
    1.43  
    1.44  lemma continuous_within_ln [continuous_intros]:
    1.45 -  "continuous (at x within s) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
    1.46 +  "continuous (at x within s) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
    1.47    unfolding continuous_within by (rule tendsto_ln)
    1.48  
    1.49  lemma continuous_on_ln [continuous_intros]:
    1.50 -  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. 0 < f x) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
    1.51 +  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. f x \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
    1.52    unfolding continuous_on_def by (auto intro: tendsto_ln)
    1.53  
    1.54  lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
    1.55 @@ -1992,6 +2005,9 @@
    1.56  lemma ln_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> ln (root n b) =  ln b / n"
    1.57  by(simp add: root_powr_inverse ln_powr)
    1.58  
    1.59 +lemma ln_sqrt: "0 < x \<Longrightarrow> ln (sqrt x) = ln x / 2"
    1.60 +  by (simp add: ln_powr powr_numeral ln_powr[symmetric] mult_commute)
    1.61 +
    1.62  lemma log_root: "\<lbrakk> n > 0; a > 0 \<rbrakk> \<Longrightarrow> log b (root n a) =  log b a / n"
    1.63  by(simp add: log_def ln_root)
    1.64  
    1.65 @@ -2085,30 +2101,30 @@
    1.66  qed
    1.67  
    1.68  lemma tendsto_powr [tendsto_intros]:
    1.69 -  "\<lbrakk>(f ---> a) F; (g ---> b) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
    1.70 +  "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
    1.71    unfolding powr_def by (intro tendsto_intros)
    1.72  
    1.73  lemma continuous_powr:
    1.74    assumes "continuous F f"
    1.75      and "continuous F g"
    1.76 -    and "0 < f (Lim F (\<lambda>x. x))"
    1.77 +    and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
    1.78    shows "continuous F (\<lambda>x. (f x) powr (g x))"
    1.79    using assms unfolding continuous_def by (rule tendsto_powr)
    1.80  
    1.81  lemma continuous_at_within_powr[continuous_intros]:
    1.82    assumes "continuous (at a within s) f"
    1.83      and "continuous (at a within s) g"
    1.84 -    and "0 < f a"
    1.85 +    and "f a \<noteq> 0"
    1.86    shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x))"
    1.87    using assms unfolding continuous_within by (rule tendsto_powr)
    1.88  
    1.89  lemma isCont_powr[continuous_intros, simp]:
    1.90 -  assumes "isCont f a" "isCont g a" "0 < f a"
    1.91 +  assumes "isCont f a" "isCont g a" "f a \<noteq> 0"
    1.92    shows "isCont (\<lambda>x. (f x) powr g x) a"
    1.93    using assms unfolding continuous_at by (rule tendsto_powr)
    1.94  
    1.95  lemma continuous_on_powr[continuous_intros]:
    1.96 -  assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. 0 < f x"
    1.97 +  assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. f x \<noteq> 0"
    1.98    shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
    1.99    using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
   1.100  
   1.101 @@ -2150,6 +2166,53 @@
   1.102    show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1)
   1.103  qed
   1.104  
   1.105 +(* it is funny that this isn't in the library! It could go in Transcendental *)
   1.106 +lemma tendsto_exp_limit_at_right:
   1.107 +  fixes x :: real
   1.108 +  shows "((\<lambda>y. (1 + x * y) powr (1 / y)) ---> exp x) (at_right 0)"
   1.109 +proof cases
   1.110 +  assume "x \<noteq> 0"
   1.111 +
   1.112 +  have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)"
   1.113 +    by (auto intro!: derivative_eq_intros)
   1.114 +  then have "((\<lambda>y. ln (1 + x * y) / y) ---> x) (at 0)"
   1.115 +    by (auto simp add: has_field_derivative_def field_has_derivative_at) 
   1.116 +  then have *: "((\<lambda>y. exp (ln (1 + x * y) / y)) ---> exp x) (at 0)"
   1.117 +    by (rule tendsto_intros)
   1.118 +  then show ?thesis
   1.119 +  proof (rule filterlim_mono_eventually)
   1.120 +    show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)"
   1.121 +      unfolding eventually_at_right[OF zero_less_one]
   1.122 +      using `x \<noteq> 0` by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def)
   1.123 +  qed (simp_all add: at_eq_sup_left_right)
   1.124 +qed (simp add: tendsto_const)
   1.125 +
   1.126 +lemma tendsto_exp_limit_at_top:
   1.127 +  fixes x :: real
   1.128 +  shows "((\<lambda>y. (1 + x / y) powr y) ---> exp x) at_top"
   1.129 +  apply (subst filterlim_at_top_to_right)
   1.130 +  apply (simp add: inverse_eq_divide)
   1.131 +  apply (rule tendsto_exp_limit_at_right)
   1.132 +  done
   1.133 +
   1.134 +lemma tendsto_exp_limit_sequentially:
   1.135 +  fixes x :: real
   1.136 +  shows "(\<lambda>n. (1 + x / n) ^ n) ----> exp x"
   1.137 +proof (rule filterlim_mono_eventually)
   1.138 +  from reals_Archimedean2 [of "abs x"] obtain n :: nat where *: "real n > abs x" ..
   1.139 +  hence "eventually (\<lambda>n :: nat. 0 < 1 + x / real n) at_top"
   1.140 +    apply (intro eventually_sequentiallyI [of n])
   1.141 +    apply (case_tac "x \<ge> 0")
   1.142 +    apply (rule add_pos_nonneg, auto intro: divide_nonneg_nonneg)
   1.143 +    apply (subgoal_tac "x / real xa > -1")
   1.144 +    apply (auto simp add: field_simps)
   1.145 +    done
   1.146 +  then show "eventually (\<lambda>n. (1 + x / n) powr n = (1 + x / n) ^ n) at_top"
   1.147 +    by (rule eventually_elim1) (erule powr_realpow)
   1.148 +  show "(\<lambda>n. (1 + x / real n) powr real n) ----> exp x"
   1.149 +    by (rule filterlim_compose [OF tendsto_exp_limit_at_top filterlim_real_sequentially])
   1.150 +qed auto
   1.151 +
   1.152  subsection {* Sine and Cosine *}
   1.153  
   1.154  definition sin_coeff :: "nat \<Rightarrow> real" where
   1.155 @@ -2374,6 +2437,31 @@
   1.156    using cos_add [where x=x and y=x]
   1.157    by (simp add: power2_eq_square)
   1.158  
   1.159 +lemma sin_x_le_x: assumes x: "x \<ge> 0" shows "sin x \<le> x"
   1.160 +proof -
   1.161 +  let ?f = "\<lambda>x. x - sin x"
   1.162 +  from x have "?f x \<ge> ?f 0"
   1.163 +    apply (rule DERIV_nonneg_imp_nondecreasing)
   1.164 +    apply (intro allI impI exI[of _ "1 - cos x" for x])
   1.165 +    apply (auto intro!: derivative_eq_intros simp: field_simps)
   1.166 +    done
   1.167 +  thus "sin x \<le> x" by simp
   1.168 +qed
   1.169 +
   1.170 +lemma sin_x_ge_neg_x: assumes x: "x \<ge> 0" shows "sin x \<ge> - x"
   1.171 +proof -
   1.172 +  let ?f = "\<lambda>x. x + sin x"
   1.173 +  from x have "?f x \<ge> ?f 0"
   1.174 +    apply (rule DERIV_nonneg_imp_nondecreasing)
   1.175 +    apply (intro allI impI exI[of _ "1 + cos x" for x])
   1.176 +    apply (auto intro!: derivative_eq_intros simp: field_simps real_0_le_add_iff)
   1.177 +    done
   1.178 +  thus "sin x \<ge> -x" by simp
   1.179 +qed
   1.180 +
   1.181 +lemma abs_sin_x_le_abs_x: "\<bar>sin x\<bar> \<le> \<bar>x\<bar>"
   1.182 +  using sin_x_ge_neg_x [of x] sin_x_le_x [of x] sin_x_ge_neg_x [of "-x"] sin_x_le_x [of "-x"]
   1.183 +  by (auto simp: abs_real_def)
   1.184  
   1.185  subsection {* The Constant Pi *}
   1.186