src/HOL/Deriv.thy
changeset 29166 c23b2d108612
parent 28952 15a4b2cf8c34
child 29169 6a5f1d8d7344
     1.1 --- a/src/HOL/Deriv.thy	Wed Dec 24 08:06:27 2008 -0800
     1.2 +++ b/src/HOL/Deriv.thy	Wed Dec 24 08:16:45 2008 -0800
     1.3 @@ -1722,4 +1722,60 @@
     1.4  apply (simp add: poly_entire del: pmult_Cons)
     1.5  done
     1.6  
     1.7 +
     1.8 +subsection {* Theorems about Limits *}
     1.9 +
    1.10 +(* need to rename second isCont_inverse *)
    1.11 +
    1.12 +lemma isCont_inv_fun:
    1.13 +  fixes f g :: "real \<Rightarrow> real"
    1.14 +  shows "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
    1.15 +         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
    1.16 +      ==> isCont g (f x)"
    1.17 +by (rule isCont_inverse_function)
    1.18 +
    1.19 +lemma isCont_inv_fun_inv:
    1.20 +  fixes f g :: "real \<Rightarrow> real"
    1.21 +  shows "[| 0 < d;  
    1.22 +         \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
    1.23 +         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
    1.24 +       ==> \<exists>e. 0 < e &  
    1.25 +             (\<forall>y. 0 < \<bar>y - f(x)\<bar> & \<bar>y - f(x)\<bar> < e --> f(g(y)) = y)"
    1.26 +apply (drule isCont_inj_range)
    1.27 +prefer 2 apply (assumption, assumption, auto)
    1.28 +apply (rule_tac x = e in exI, auto)
    1.29 +apply (rotate_tac 2)
    1.30 +apply (drule_tac x = y in spec, auto)
    1.31 +done
    1.32 +
    1.33 +
    1.34 +text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
    1.35 +lemma LIM_fun_gt_zero:
    1.36 +     "[| f -- c --> (l::real); 0 < l |]  
    1.37 +         ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> 0 < f x)"
    1.38 +apply (auto simp add: LIM_def)
    1.39 +apply (drule_tac x = "l/2" in spec, safe, force)
    1.40 +apply (rule_tac x = s in exI)
    1.41 +apply (auto simp only: abs_less_iff)
    1.42 +done
    1.43 +
    1.44 +lemma LIM_fun_less_zero:
    1.45 +     "[| f -- c --> (l::real); l < 0 |]  
    1.46 +      ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> f x < 0)"
    1.47 +apply (auto simp add: LIM_def)
    1.48 +apply (drule_tac x = "-l/2" in spec, safe, force)
    1.49 +apply (rule_tac x = s in exI)
    1.50 +apply (auto simp only: abs_less_iff)
    1.51 +done
    1.52 +
    1.53 +
    1.54 +lemma LIM_fun_not_zero:
    1.55 +     "[| f -- c --> (l::real); l \<noteq> 0 |] 
    1.56 +      ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> f x \<noteq> 0)"
    1.57 +apply (cut_tac x = l and y = 0 in linorder_less_linear, auto)
    1.58 +apply (drule LIM_fun_less_zero)
    1.59 +apply (drule_tac [3] LIM_fun_gt_zero)
    1.60 +apply force+
    1.61 +done
    1.62 +
    1.63  end