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.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.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.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.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
```