author paulson Thu, 19 Sep 2019 13:59:29 +0100 changeset 70725 e19c18b4a0dd parent 70724 65371451fde8 child 70726 91587befabfd
Four new results from Smooth_Manifolds/Analysis_More
```--- a/src/HOL/Analysis/Derivative.thy	Thu Sep 19 12:36:15 2019 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Thu Sep 19 13:59:29 2019 +0100
@@ -233,6 +233,12 @@
unfolding frechet_derivative_works has_derivative_def
by (auto intro: bounded_linear.linear)

+lemma frechet_derivative_const [simp]: "frechet_derivative (\<lambda>x. c) (at a) = (\<lambda>x. 0)"
+  using differentiable_const frechet_derivative_works has_derivative_const has_derivative_unique by blast
+
+lemma frechet_derivative_id [simp]: "frechet_derivative id (at a) = id"
+  using differentiable_def frechet_derivative_works has_derivative_id has_derivative_unique by blast
+

subsection \<open>Differentiability implies continuity\<close>

@@ -485,6 +491,11 @@
"(f has_derivative f') (at x) \<Longrightarrow> f' = frechet_derivative f (at x)"
using differentiable_def frechet_derivative_works has_derivative_unique by blast

+lemma frechet_derivative_compose:
+  "frechet_derivative (f o g) (at x) = frechet_derivative (f) (at (g x)) o frechet_derivative g (at x)"
+  if "g differentiable at x" "f differentiable at (g x)"
+  by (metis diff_chain_at frechet_derivative_at frechet_derivative_works that)
+
lemma frechet_derivative_within_cbox:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes "\<And>i. i\<in>Basis \<Longrightarrow> a\<bullet>i < b\<bullet>i"
@@ -494,6 +505,11 @@
using assms
by (metis Derivative.differentiableI frechet_derivative_unique_within_closed_interval frechet_derivative_works)

+lemma frechet_derivative_transform_within_open:
+  "frechet_derivative f (at x) = frechet_derivative g (at x)"
+  if "f differentiable at x" "open X" "x \<in> X" "\<And>x. x \<in> X \<Longrightarrow> f x = g x"
+  by (meson frechet_derivative_at frechet_derivative_works has_derivative_transform_within_open that)
+

subsection \<open>Derivatives of local minima and maxima are zero\<close>
```