--- a/src/HOL/Multivariate_Analysis/Derivative.thy Wed Sep 02 23:31:41 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Sep 03 20:27:53 2015 +0100
@@ -138,7 +138,7 @@
qed
lemma DERIV_caratheodory_within:
- "(f has_field_derivative l) (at x within s) \<longleftrightarrow>
+ "(f has_field_derivative l) (at x within s) \<longleftrightarrow>
(\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within s) g \<and> g x = l)"
(is "?lhs = ?rhs")
proof
@@ -209,6 +209,15 @@
using has_derivative_at_within
by blast
+lemma differentiable_at_imp_differentiable_on:
+ "(\<And>x. x \<in> s \<Longrightarrow> f differentiable at x) \<Longrightarrow> f differentiable_on s"
+ by (metis differentiable_at_withinI differentiable_on_def)
+
+corollary differentiable_iff_scaleR:
+ fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
+ shows "f differentiable F \<longleftrightarrow> (\<exists>d. (f has_derivative (\<lambda>x. x *\<^sub>R d)) F)"
+ by (auto simp: differentiable_def dest: has_derivative_linear linear_imp_scaleR)
+
lemma differentiable_within_open: (* TODO: delete *)
assumes "a \<in> s"
and "open s"
@@ -2241,6 +2250,24 @@
apply auto
done
+lemma has_vector_derivative_id_at [simp]: "vector_derivative (\<lambda>x. x) (at a) = 1"
+ by (simp add: vector_derivative_at)
+
+lemma vector_derivative_minus_at [simp]:
+ "f differentiable at a
+ \<Longrightarrow> vector_derivative (\<lambda>x. - f x) (at a) = - vector_derivative f (at a)"
+ by (simp add: vector_derivative_at has_vector_derivative_minus vector_derivative_works [symmetric])
+
+lemma vector_derivative_add_at [simp]:
+ "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
+ \<Longrightarrow> vector_derivative (\<lambda>x. f x + g x) (at a) = vector_derivative f (at a) + vector_derivative g (at a)"
+ by (simp add: vector_derivative_at has_vector_derivative_add vector_derivative_works [symmetric])
+
+lemma vector_derivative_diff_at [simp]:
+ "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
+ \<Longrightarrow> vector_derivative (\<lambda>x. f x - g x) (at a) = vector_derivative f (at a) - vector_derivative g (at a)"
+ by (simp add: vector_derivative_at has_vector_derivative_diff vector_derivative_works [symmetric])
+
lemma vector_derivative_within_closed_interval:
assumes "a < b"
and "x \<in> cbox a b"