src/HOL/Multivariate_Analysis/Derivative.thy
changeset 43338 a150d16bf77c
parent 41970 47d6e13d1710
child 44081 730f7cced3a6
     1.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Jun 09 11:50:16 2011 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Jun 09 11:50:16 2011 +0200
     1.3 @@ -105,6 +105,22 @@
     1.4    "a \<in> s \<Longrightarrow> open s \<Longrightarrow> ((f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a))"
     1.5    by (simp only: at_within_interior interior_open)
     1.6  
     1.7 +lemma has_derivative_right:
     1.8 +  fixes f :: "real \<Rightarrow> real" and y :: "real"
     1.9 +  shows "(f has_derivative (op * y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
    1.10 +    ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x <..} \<inter> I))"
    1.11 +proof -
    1.12 +  have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) ---> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
    1.13 +    ((\<lambda>t. (f t - f x) / (t - x) - y) ---> 0) (at x within ({x<..} \<inter> I))"
    1.14 +    by (intro Lim_cong_within) (auto simp add: divide.diff divide.add)
    1.15 +  also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t - f x) / (t - x)) ---> y) (at x within ({x<..} \<inter> I))"
    1.16 +    by (simp add: Lim_null[symmetric])
    1.17 +  also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x<..} \<inter> I))"
    1.18 +    by (intro Lim_cong_within) (simp_all add: times_divide_eq field_simps)
    1.19 +  finally show ?thesis
    1.20 +    by (simp add: mult.bounded_linear_right has_derivative_within)
    1.21 +qed
    1.22 +
    1.23  lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
    1.24  proof -
    1.25    assume "bounded_linear f"