src/HOL/Transcendental.thy
changeset 51478 270b21f3ae0a
parent 51477 2990382dc066
child 51481 ef949192e5d6
     1.1 --- a/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -881,6 +881,12 @@
     1.4    "(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F"
     1.5    by (rule isCont_tendsto_compose [OF isCont_exp])
     1.6  
     1.7 +lemma continuous_exp [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
     1.8 +  unfolding continuous_def by (rule tendsto_exp)
     1.9 +
    1.10 +lemma continuous_on_exp [continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
    1.11 +  unfolding continuous_on_def by (auto intro: tendsto_exp)
    1.12 +
    1.13  subsubsection {* Properties of the Exponential Function *}
    1.14  
    1.15  lemma powser_zero:
    1.16 @@ -1169,6 +1175,22 @@
    1.17    "\<lbrakk>(f ---> a) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
    1.18    by (rule isCont_tendsto_compose [OF isCont_ln])
    1.19  
    1.20 +lemma continuous_ln:
    1.21 +  "continuous F f \<Longrightarrow> 0 < f (Lim F (\<lambda>x. x)) \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
    1.22 +  unfolding continuous_def by (rule tendsto_ln)
    1.23 +
    1.24 +lemma isCont_ln' [continuous_intros]:
    1.25 +  "continuous (at x) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
    1.26 +  unfolding continuous_at by (rule tendsto_ln)
    1.27 +
    1.28 +lemma continuous_within_ln [continuous_intros]:
    1.29 +  "continuous (at x within s) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
    1.30 +  unfolding continuous_within by (rule tendsto_ln)
    1.31 +
    1.32 +lemma continuous_on_ln [continuous_on_intros]:
    1.33 +  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. 0 < f x) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
    1.34 +  unfolding continuous_on_def by (auto intro: tendsto_ln)
    1.35 +
    1.36  lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
    1.37    apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
    1.38    apply (erule DERIV_cong [OF DERIV_exp exp_ln])
    1.39 @@ -1449,6 +1471,22 @@
    1.40    "(f ---> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) ---> cos a) F"
    1.41    by (rule isCont_tendsto_compose [OF isCont_cos])
    1.42  
    1.43 +lemma continuous_sin [continuous_intros]:
    1.44 +  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
    1.45 +  unfolding continuous_def by (rule tendsto_sin)
    1.46 +
    1.47 +lemma continuous_on_sin [continuous_on_intros]:
    1.48 +  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
    1.49 +  unfolding continuous_on_def by (auto intro: tendsto_sin)
    1.50 +
    1.51 +lemma continuous_cos [continuous_intros]:
    1.52 +  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
    1.53 +  unfolding continuous_def by (rule tendsto_cos)
    1.54 +
    1.55 +lemma continuous_on_cos [continuous_on_intros]:
    1.56 +  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
    1.57 +  unfolding continuous_on_def by (auto intro: tendsto_cos)
    1.58 +
    1.59  declare
    1.60    DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
    1.61    DERIV_ln_divide[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
    1.62 @@ -2076,6 +2114,22 @@
    1.63    "\<lbrakk>(f ---> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) ---> tan a) F"
    1.64    by (rule isCont_tendsto_compose [OF isCont_tan])
    1.65  
    1.66 +lemma continuous_tan:
    1.67 +  "continuous F f \<Longrightarrow> cos (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. tan (f x))"
    1.68 +  unfolding continuous_def by (rule tendsto_tan)
    1.69 +
    1.70 +lemma isCont_tan'' [continuous_intros]:
    1.71 +  "continuous (at x) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. tan (f x))"
    1.72 +  unfolding continuous_at by (rule tendsto_tan)
    1.73 +
    1.74 +lemma continuous_within_tan [continuous_intros]:
    1.75 +  "continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
    1.76 +  unfolding continuous_within by (rule tendsto_tan)
    1.77 +
    1.78 +lemma continuous_on_tan [continuous_on_intros]:
    1.79 +  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. cos (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. tan (f x))"
    1.80 +  unfolding continuous_on_def by (auto intro: tendsto_tan)
    1.81 +
    1.82  lemma LIM_cos_div_sin: "(%x. cos(x)/sin(x)) -- pi/2 --> 0"
    1.83    by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
    1.84  
    1.85 @@ -2403,7 +2457,7 @@
    1.86  lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0"
    1.87    using arctan_eq_iff [of x 0] by simp
    1.88  
    1.89 -lemma isCont_inverse_function2:
    1.90 +lemma isCont_inverse_function2: (* generalize with continuous_on *)
    1.91    fixes f g :: "real \<Rightarrow> real" shows
    1.92    "\<lbrakk>a < x; x < b;
    1.93      \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
    1.94 @@ -2414,7 +2468,7 @@
    1.95  apply (simp_all add: abs_le_iff)
    1.96  done
    1.97  
    1.98 -lemma isCont_arcsin: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arcsin x"
    1.99 +lemma isCont_arcsin: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arcsin x" (* generalize with continuous_on {-1 .. 1} *)
   1.100  apply (subgoal_tac "isCont arcsin (sin (arcsin x))", simp)
   1.101  apply (rule isCont_inverse_function2 [where f=sin])
   1.102  apply (erule (1) arcsin_lt_bounded [THEN conjunct1])
   1.103 @@ -2422,7 +2476,7 @@
   1.104  apply (fast intro: arcsin_sin, simp)
   1.105  done
   1.106  
   1.107 -lemma isCont_arccos: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arccos x"
   1.108 +lemma isCont_arccos: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arccos x" (* generalize with continuous_on {-1 .. 1} *)
   1.109  apply (subgoal_tac "isCont arccos (cos (arccos x))", simp)
   1.110  apply (rule isCont_inverse_function2 [where f=cos])
   1.111  apply (erule (1) arccos_lt_bounded [THEN conjunct1])
   1.112 @@ -2439,6 +2493,15 @@
   1.113  apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le)
   1.114  done
   1.115  
   1.116 +lemma tendsto_arctan [tendsto_intros]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. arctan (f x)) ---> arctan x) F"
   1.117 +  by (rule isCont_tendsto_compose [OF isCont_arctan])
   1.118 +
   1.119 +lemma continuous_arctan [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. arctan (f x))"
   1.120 +  unfolding continuous_def by (rule tendsto_arctan)
   1.121 +
   1.122 +lemma continuous_on_arctan [continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
   1.123 +  unfolding continuous_on_def by (auto intro: tendsto_arctan)
   1.124 +  
   1.125  lemma DERIV_arcsin:
   1.126    "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<twosuperior>))"
   1.127  apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])